source: extracted/bitVectorTrie.ml @ 2746

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

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

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_4072 = function
46| Leaf x_4074 -> h_Leaf x_4074
47| Node (n, x_4076, x_4075) ->
48  h_Node n x_4076 x_4075
49    (bitVectorTrie_rect_Type4 h_Leaf h_Node h_Stub n x_4076)
50    (bitVectorTrie_rect_Type4 h_Leaf h_Node h_Stub n x_4075)
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_4088 = function
57| Leaf x_4090 -> h_Leaf x_4090
58| Node (n, x_4092, x_4091) ->
59  h_Node n x_4092 x_4091
60    (bitVectorTrie_rect_Type3 h_Leaf h_Node h_Stub n x_4092)
61    (bitVectorTrie_rect_Type3 h_Leaf h_Node h_Stub n x_4091)
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_4096 = function
68| Leaf x_4098 -> h_Leaf x_4098
69| Node (n, x_4100, x_4099) ->
70  h_Node n x_4100 x_4099
71    (bitVectorTrie_rect_Type2 h_Leaf h_Node h_Stub n x_4100)
72    (bitVectorTrie_rect_Type2 h_Leaf h_Node h_Stub n x_4099)
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_4104 = function
79| Leaf x_4106 -> h_Leaf x_4106
80| Node (n, x_4108, x_4107) ->
81  h_Node n x_4108 x_4107
82    (bitVectorTrie_rect_Type1 h_Leaf h_Node h_Stub n x_4108)
83    (bitVectorTrie_rect_Type1 h_Leaf h_Node h_Stub n x_4107)
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_4112 = function
90| Leaf x_4114 -> h_Leaf x_4114
91| Node (n, x_4116, x_4115) ->
92  h_Node n x_4116 x_4115
93    (bitVectorTrie_rect_Type0 h_Leaf h_Node h_Stub n x_4116)
94    (bitVectorTrie_rect_Type0 h_Leaf h_Node h_Stub n x_4115)
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.