source: extracted/bitVectorTrie.ml @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File size: 10.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
42(** val bitVectorTrie_rect_Type4 :
43    ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
44    -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2 **)
45let rec bitVectorTrie_rect_Type4 h_Leaf h_Node h_Stub x_4046 = function
46| Leaf x_4048 -> h_Leaf x_4048
47| Node (n, x_4050, x_4049) ->
48  h_Node n x_4050 x_4049
49    (bitVectorTrie_rect_Type4 h_Leaf h_Node h_Stub n x_4050)
50    (bitVectorTrie_rect_Type4 h_Leaf h_Node h_Stub n x_4049)
51| Stub n -> h_Stub n
52
53(** val bitVectorTrie_rect_Type3 :
54    ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
55    -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2 **)
56let rec bitVectorTrie_rect_Type3 h_Leaf h_Node h_Stub x_4062 = function
57| Leaf x_4064 -> h_Leaf x_4064
58| Node (n, x_4066, x_4065) ->
59  h_Node n x_4066 x_4065
60    (bitVectorTrie_rect_Type3 h_Leaf h_Node h_Stub n x_4066)
61    (bitVectorTrie_rect_Type3 h_Leaf h_Node h_Stub n x_4065)
62| Stub n -> h_Stub n
63
64(** val bitVectorTrie_rect_Type2 :
65    ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
66    -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2 **)
67let rec bitVectorTrie_rect_Type2 h_Leaf h_Node h_Stub x_4070 = function
68| Leaf x_4072 -> h_Leaf x_4072
69| Node (n, x_4074, x_4073) ->
70  h_Node n x_4074 x_4073
71    (bitVectorTrie_rect_Type2 h_Leaf h_Node h_Stub n x_4074)
72    (bitVectorTrie_rect_Type2 h_Leaf h_Node h_Stub n x_4073)
73| Stub n -> h_Stub n
74
75(** val bitVectorTrie_rect_Type1 :
76    ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
77    -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2 **)
78let rec bitVectorTrie_rect_Type1 h_Leaf h_Node h_Stub x_4078 = function
79| Leaf x_4080 -> h_Leaf x_4080
80| Node (n, x_4082, x_4081) ->
81  h_Node n x_4082 x_4081
82    (bitVectorTrie_rect_Type1 h_Leaf h_Node h_Stub n x_4082)
83    (bitVectorTrie_rect_Type1 h_Leaf h_Node h_Stub n x_4081)
84| Stub n -> h_Stub n
85
86(** val bitVectorTrie_rect_Type0 :
87    ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
88    -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2 **)
89let rec bitVectorTrie_rect_Type0 h_Leaf h_Node h_Stub x_4086 = function
90| Leaf x_4088 -> h_Leaf x_4088
91| Node (n, x_4090, x_4089) ->
92  h_Node n x_4090 x_4089
93    (bitVectorTrie_rect_Type0 h_Leaf h_Node h_Stub n x_4090)
94    (bitVectorTrie_rect_Type0 h_Leaf h_Node h_Stub n x_4089)
95| Stub n -> h_Stub n
96
97(** val bitVectorTrie_inv_rect_Type4 :
98    Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat ->
99    'a1 bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __
100    -> 'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2 **)
101let bitVectorTrie_inv_rect_Type4 x2 hterm h1 h2 h3 =
102  let hcut = bitVectorTrie_rect_Type4 h1 h2 h3 x2 hterm in hcut __ __
103
104(** val bitVectorTrie_inv_rect_Type3 :
105    Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat ->
106    'a1 bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __
107    -> 'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2 **)
108let bitVectorTrie_inv_rect_Type3 x2 hterm h1 h2 h3 =
109  let hcut = bitVectorTrie_rect_Type3 h1 h2 h3 x2 hterm in hcut __ __
110
111(** val bitVectorTrie_inv_rect_Type2 :
112    Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat ->
113    'a1 bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __
114    -> 'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2 **)
115let bitVectorTrie_inv_rect_Type2 x2 hterm h1 h2 h3 =
116  let hcut = bitVectorTrie_rect_Type2 h1 h2 h3 x2 hterm in hcut __ __
117
118(** val bitVectorTrie_inv_rect_Type1 :
119    Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat ->
120    'a1 bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __
121    -> 'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2 **)
122let bitVectorTrie_inv_rect_Type1 x2 hterm h1 h2 h3 =
123  let hcut = bitVectorTrie_rect_Type1 h1 h2 h3 x2 hterm in hcut __ __
124
125(** val bitVectorTrie_inv_rect_Type0 :
126    Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat ->
127    'a1 bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __
128    -> 'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2 **)
129let bitVectorTrie_inv_rect_Type0 x2 hterm h1 h2 h3 =
130  let hcut = bitVectorTrie_rect_Type0 h1 h2 h3 x2 hterm in hcut __ __
131
132(** val bitVectorTrie_discr :
133    Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> __ **)
134let bitVectorTrie_discr a2 x y =
135  Logic.eq_rect_Type2 x
136    (match x with
137     | Leaf a0 -> Obj.magic (fun _ dH -> dH __)
138     | Node (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
139     | Stub a0 -> Obj.magic (fun _ dH -> dH __)) y
140
141(** val bitVectorTrie_jmdiscr :
142    Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> __ **)
143let bitVectorTrie_jmdiscr a2 x y =
144  Logic.eq_rect_Type2 x
145    (match x with
146     | Leaf a0 -> Obj.magic (fun _ dH -> dH __)
147     | Node (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
148     | Stub a0 -> Obj.magic (fun _ dH -> dH __)) y
149
150(** val fold0 :
151    Nat.nat -> (BitVector.bitVector -> 'a1 -> 'a2 -> 'a2) -> 'a1
152    bitVectorTrie -> 'a2 -> 'a2 **)
153let rec fold0 n f t b =
154  (match t with
155   | Leaf l -> (fun _ -> f (BitVector.zero n) l b)
156   | Node (h, l, r) ->
157     (fun _ ->
158       fold0 h (fun x -> f (Vector.VCons (h, Bool.False, x))) l
159         (fold0 h (fun x -> f (Vector.VCons (h, Bool.True, x))) r b))
160   | Stub x -> (fun _ -> b)) __
161
162(** val bvtfold_aux :
163    (BitVector.bitVector -> 'a1 -> 'a2 -> 'a2) -> 'a2 -> Nat.nat -> 'a1
164    bitVectorTrie -> BitVector.bitVector -> 'a2 **)
165let rec bvtfold_aux f seed n x x0 =
166  (match n with
167   | Nat.O ->
168     (fun _ trie path ->
169       (match trie with
170        | Leaf l -> (fun _ -> f path l seed)
171        | Node (n', l, r) -> (fun _ -> assert false (* absurd case *))
172        | Stub s -> (fun _ -> seed)) __)
173   | Nat.S n' ->
174     (fun _ trie path ->
175       (match trie with
176        | Leaf l -> (fun _ -> assert false (* absurd case *))
177        | Node (n'', l, r) ->
178          (fun _ ->
179            bvtfold_aux f
180              (bvtfold_aux f seed n' l (Vector.VCons
181                ((Nat.minus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
182                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
183                   (Nat.S Nat.O)))))))))))))))) (Nat.S n')), Bool.False,
184                path))) n' r (Vector.VCons
185              ((Nat.minus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
186                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
187                 (Nat.S Nat.O)))))))))))))))) (Nat.S n')), Bool.True, path)))
188        | Stub s -> (fun _ -> seed)) __)) __ x x0
189
190(** val lookup_opt :
191    Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> 'a1 Types.option **)
192let rec lookup_opt n b t =
193  (match t with
194   | Leaf l -> (fun x -> Types.Some l)
195   | Node (h, l, r) ->
196     (fun b0 ->
197       lookup_opt h (Vector.tail0 h b0)
198         (match Vector.head' h b0 with
199          | Bool.True -> r
200          | Bool.False -> l))
201   | Stub x -> (fun x0 -> Types.None)) b
202
203(** val member0 :
204    Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> Bool.bool **)
205let member0 n b t =
206  match lookup_opt n b t with
207  | Types.None -> Bool.False
208  | Types.Some x -> Bool.True
209
210(** val lookup :
211    Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> 'a1 -> 'a1 **)
212let rec lookup n b t a =
213  (match b with
214   | Vector.VEmpty ->
215     (match t with
216      | Leaf l -> (fun _ -> l)
217      | Node (h, l, r) -> (fun _ -> assert false (* absurd case *))
218      | Stub s -> (fun _ -> a))
219   | Vector.VCons (o, hd0, tl) ->
220     (match t with
221      | Leaf l -> (fun _ -> assert false (* absurd case *))
222      | Node (h, l, r) ->
223        (match hd0 with
224         | Bool.True -> (fun _ -> lookup h tl r a)
225         | Bool.False -> (fun _ -> lookup h tl l a))
226      | Stub s -> (fun _ -> a))) __
227
228(** val prepare_trie_for_insertion :
229    Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie **)
230let rec prepare_trie_for_insertion n b a =
231  match b with
232  | Vector.VEmpty -> Leaf a
233  | Vector.VCons (o, hd0, tl) ->
234    (match hd0 with
235     | Bool.True -> Node (o, (Stub o), (prepare_trie_for_insertion o tl a))
236     | Bool.False -> Node (o, (prepare_trie_for_insertion o tl a), (Stub o)))
237
238(** val insert :
239    Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie -> 'a1
240    bitVectorTrie **)
241let rec insert n b a =
242  match b with
243  | Vector.VEmpty -> (fun x -> Leaf a)
244  | Vector.VCons (o, hd0, tl) ->
245    (fun t ->
246      (match t with
247       | Leaf l -> (fun _ -> assert false (* absurd case *))
248       | Node (p, l, r) ->
249         (fun _ ->
250           match hd0 with
251           | Bool.True -> Node (o, l, (insert o tl a r))
252           | Bool.False -> Node (o, (insert o tl a l), r))
253       | Stub p ->
254         (fun _ ->
255           prepare_trie_for_insertion (Nat.S o) (Vector.VCons (o, hd0, tl)) a))
256        __)
257
258(** val update :
259    Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie -> 'a1
260    bitVectorTrie Types.option **)
261let rec update n b a =
262  match b with
263  | Vector.VEmpty ->
264    (fun t ->
265      (match t with
266       | Leaf x -> (fun _ -> Types.Some (Leaf a))
267       | Node (x, x0, x1) -> (fun _ -> assert false (* absurd case *))
268       | Stub x -> (fun _ -> Types.None)) __)
269  | Vector.VCons (o, hd0, tl) ->
270    (fun t ->
271      (match t with
272       | Leaf l -> (fun _ -> assert false (* absurd case *))
273       | Node (p, l, r) ->
274         (fun _ ->
275           match hd0 with
276           | Bool.True ->
277             Types.option_map (fun v -> Node (o, l, v)) (update o tl a r)
278           | Bool.False ->
279             Types.option_map (fun v -> Node (o, v, r)) (update o tl a l))
280       | Stub p -> (fun _ -> Types.None)) __)
281
282(** val merge :
283    Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie **)
284let rec merge n = function
285| Leaf l ->
286  (fun c ->
287    match c with
288    | Leaf a -> Leaf a
289    | Node (x, x0, x1) -> Leaf l
290    | Stub x -> Leaf l)
291| Node (p, l, r) ->
292  (fun c ->
293    (match c with
294     | Leaf x -> (fun _ -> Obj.magic Nat.nat_discr Nat.O (Nat.S p) __)
295     | Node (p', l', r') ->
296       (fun _ -> Node (p, (merge p l l'), (merge p r r')))
297     | Stub x -> (fun _ -> Node (p, l, r))) __)
298| Stub x -> (fun c -> c)
299
Note: See TracBrowser for help on using the repository browser.