source: extracted/bitVectorTrie.mli @ 2746

Last change on this file since 2746 was 2649, checked in by sacerdot, 7 years ago

...

File size: 3.5 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Extranat
14
15open Vector
16
17open Div_and_mod
18
19open Jmeq
20
21open Russell
22
23open List
24
25open Util
26
27open FoldStuff
28
29open Bool
30
31open Relations
32
33open Nat
34
35open BitVector
36
37type 'a bitVectorTrie =
38| Leaf of 'a
39| Node of Nat.nat * 'a bitVectorTrie * 'a bitVectorTrie
40| Stub of Nat.nat
41
42val bitVectorTrie_rect_Type4 :
43  ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
44  -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2
45
46val bitVectorTrie_rect_Type3 :
47  ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
48  -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2
49
50val bitVectorTrie_rect_Type2 :
51  ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
52  -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2
53
54val bitVectorTrie_rect_Type1 :
55  ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
56  -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2
57
58val bitVectorTrie_rect_Type0 :
59  ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
60  -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2
61
62val bitVectorTrie_inv_rect_Type4 :
63  Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat -> 'a1
64  bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __ ->
65  'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2
66
67val bitVectorTrie_inv_rect_Type3 :
68  Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat -> 'a1
69  bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __ ->
70  'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2
71
72val bitVectorTrie_inv_rect_Type2 :
73  Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat -> 'a1
74  bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __ ->
75  'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2
76
77val bitVectorTrie_inv_rect_Type1 :
78  Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat -> 'a1
79  bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __ ->
80  'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2
81
82val bitVectorTrie_inv_rect_Type0 :
83  Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat -> 'a1
84  bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __ ->
85  'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2
86
87val bitVectorTrie_discr :
88  Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> __
89
90val bitVectorTrie_jmdiscr :
91  Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> __
92
93val fold0 :
94  Nat.nat -> (BitVector.bitVector -> 'a1 -> 'a2 -> 'a2) -> 'a1 bitVectorTrie
95  -> 'a2 -> 'a2
96
97val bvtfold_aux :
98  (BitVector.bitVector -> 'a1 -> 'a2 -> 'a2) -> 'a2 -> Nat.nat -> 'a1
99  bitVectorTrie -> BitVector.bitVector -> 'a2
100
101val lookup_opt :
102  Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> 'a1 Types.option
103
104val member0 :
105  Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> Bool.bool
106
107val lookup :
108  Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> 'a1 -> 'a1
109
110val prepare_trie_for_insertion :
111  Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie
112
113val insert :
114  Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie -> 'a1
115  bitVectorTrie
116
117val update :
118  Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie -> 'a1
119  bitVectorTrie Types.option
120
121val merge :
122  Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie
123
Note: See TracBrowser for help on using the repository browser.