source: driver/extracted/bitVectorTrie.ml

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

New extraction

File size: 11.1 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Setoids
14
15open Monad
16
17open Option
18
19open Extranat
20
21open Vector
22
23open Div_and_mod
24
25open Jmeq
26
27open Russell
28
29open List
30
31open Util
32
33open FoldStuff
34
35open Bool
36
37open Relations
38
39open Nat
40
41open BitVector
42
43type 'a bitVectorTrie =
44| Leaf of 'a
45| Node of Nat.nat * 'a bitVectorTrie * 'a bitVectorTrie
46| Stub of Nat.nat
47
48(** val bitVectorTrie_rect_Type4 :
49    ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
50    -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2 **)
51let rec bitVectorTrie_rect_Type4 h_Leaf h_Node h_Stub x_14760 = function
52| Leaf x_14762 -> h_Leaf x_14762
53| Node (n, x_14764, x_14763) ->
54  h_Node n x_14764 x_14763
55    (bitVectorTrie_rect_Type4 h_Leaf h_Node h_Stub n x_14764)
56    (bitVectorTrie_rect_Type4 h_Leaf h_Node h_Stub n x_14763)
57| Stub n -> h_Stub n
58
59(** val bitVectorTrie_rect_Type3 :
60    ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
61    -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2 **)
62let rec bitVectorTrie_rect_Type3 h_Leaf h_Node h_Stub x_14776 = function
63| Leaf x_14778 -> h_Leaf x_14778
64| Node (n, x_14780, x_14779) ->
65  h_Node n x_14780 x_14779
66    (bitVectorTrie_rect_Type3 h_Leaf h_Node h_Stub n x_14780)
67    (bitVectorTrie_rect_Type3 h_Leaf h_Node h_Stub n x_14779)
68| Stub n -> h_Stub n
69
70(** val bitVectorTrie_rect_Type2 :
71    ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
72    -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2 **)
73let rec bitVectorTrie_rect_Type2 h_Leaf h_Node h_Stub x_14784 = function
74| Leaf x_14786 -> h_Leaf x_14786
75| Node (n, x_14788, x_14787) ->
76  h_Node n x_14788 x_14787
77    (bitVectorTrie_rect_Type2 h_Leaf h_Node h_Stub n x_14788)
78    (bitVectorTrie_rect_Type2 h_Leaf h_Node h_Stub n x_14787)
79| Stub n -> h_Stub n
80
81(** val bitVectorTrie_rect_Type1 :
82    ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
83    -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2 **)
84let rec bitVectorTrie_rect_Type1 h_Leaf h_Node h_Stub x_14792 = function
85| Leaf x_14794 -> h_Leaf x_14794
86| Node (n, x_14796, x_14795) ->
87  h_Node n x_14796 x_14795
88    (bitVectorTrie_rect_Type1 h_Leaf h_Node h_Stub n x_14796)
89    (bitVectorTrie_rect_Type1 h_Leaf h_Node h_Stub n x_14795)
90| Stub n -> h_Stub n
91
92(** val bitVectorTrie_rect_Type0 :
93    ('a1 -> 'a2) -> (Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a2
94    -> 'a2 -> 'a2) -> (Nat.nat -> 'a2) -> Nat.nat -> 'a1 bitVectorTrie -> 'a2 **)
95let rec bitVectorTrie_rect_Type0 h_Leaf h_Node h_Stub x_14800 = function
96| Leaf x_14802 -> h_Leaf x_14802
97| Node (n, x_14804, x_14803) ->
98  h_Node n x_14804 x_14803
99    (bitVectorTrie_rect_Type0 h_Leaf h_Node h_Stub n x_14804)
100    (bitVectorTrie_rect_Type0 h_Leaf h_Node h_Stub n x_14803)
101| Stub n -> h_Stub n
102
103(** val bitVectorTrie_inv_rect_Type4 :
104    Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat ->
105    'a1 bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __
106    -> 'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2 **)
107let bitVectorTrie_inv_rect_Type4 x2 hterm h1 h2 h3 =
108  let hcut = bitVectorTrie_rect_Type4 h1 h2 h3 x2 hterm in hcut __ __
109
110(** val bitVectorTrie_inv_rect_Type3 :
111    Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat ->
112    'a1 bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __
113    -> 'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2 **)
114let bitVectorTrie_inv_rect_Type3 x2 hterm h1 h2 h3 =
115  let hcut = bitVectorTrie_rect_Type3 h1 h2 h3 x2 hterm in hcut __ __
116
117(** val bitVectorTrie_inv_rect_Type2 :
118    Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat ->
119    'a1 bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __
120    -> 'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2 **)
121let bitVectorTrie_inv_rect_Type2 x2 hterm h1 h2 h3 =
122  let hcut = bitVectorTrie_rect_Type2 h1 h2 h3 x2 hterm in hcut __ __
123
124(** val bitVectorTrie_inv_rect_Type1 :
125    Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat ->
126    'a1 bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __
127    -> 'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2 **)
128let bitVectorTrie_inv_rect_Type1 x2 hterm h1 h2 h3 =
129  let hcut = bitVectorTrie_rect_Type1 h1 h2 h3 x2 hterm in hcut __ __
130
131(** val bitVectorTrie_inv_rect_Type0 :
132    Nat.nat -> 'a1 bitVectorTrie -> ('a1 -> __ -> __ -> 'a2) -> (Nat.nat ->
133    'a1 bitVectorTrie -> 'a1 bitVectorTrie -> (__ -> __ -> 'a2) -> (__ -> __
134    -> 'a2) -> __ -> __ -> 'a2) -> (Nat.nat -> __ -> __ -> 'a2) -> 'a2 **)
135let bitVectorTrie_inv_rect_Type0 x2 hterm h1 h2 h3 =
136  let hcut = bitVectorTrie_rect_Type0 h1 h2 h3 x2 hterm in hcut __ __
137
138(** val bitVectorTrie_discr :
139    Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> __ **)
140let bitVectorTrie_discr a2 x y =
141  Logic.eq_rect_Type2 x
142    (match x with
143     | Leaf a0 -> Obj.magic (fun _ dH -> dH __)
144     | Node (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
145     | Stub a0 -> Obj.magic (fun _ dH -> dH __)) y
146
147(** val bitVectorTrie_jmdiscr :
148    Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> __ **)
149let bitVectorTrie_jmdiscr a2 x y =
150  Logic.eq_rect_Type2 x
151    (match x with
152     | Leaf a0 -> Obj.magic (fun _ dH -> dH __)
153     | Node (a0, a10, a20) -> Obj.magic (fun _ dH -> dH __ __ __)
154     | Stub a0 -> Obj.magic (fun _ dH -> dH __)) y
155
156(** val fold :
157    Nat.nat -> (BitVector.bitVector -> 'a1 -> 'a2 -> 'a2) -> 'a1
158    bitVectorTrie -> 'a2 -> 'a2 **)
159let rec fold n f t b =
160  (match t with
161   | Leaf l -> (fun _ -> f (BitVector.zero n) l b)
162   | Node (h, l, r) ->
163     (fun _ ->
164       fold h (fun x -> f (Vector.VCons (h, Bool.False, x))) l
165         (fold h (fun x -> f (Vector.VCons (h, Bool.True, x))) r b))
166   | Stub x -> (fun _ -> b)) __
167
168(** val bvtfold_aux :
169    (BitVector.bitVector -> 'a1 -> 'a2 -> 'a2) -> 'a2 -> Nat.nat -> 'a1
170    bitVectorTrie -> BitVector.bitVector -> 'a2 **)
171let rec bvtfold_aux f seed n x x0 =
172  (match n with
173   | Nat.O ->
174     (fun _ trie path ->
175       (match trie with
176        | Leaf l -> (fun _ -> f path l seed)
177        | Node (n', l, r) -> (fun _ -> assert false (* absurd case *))
178        | Stub s -> (fun _ -> seed)) __)
179   | Nat.S n' ->
180     (fun _ trie path ->
181       (match trie with
182        | Leaf l -> (fun _ -> assert false (* absurd case *))
183        | Node (n'', l, r) ->
184          (fun _ ->
185            bvtfold_aux f
186              (bvtfold_aux f seed n' l (Vector.VCons
187                ((Nat.minus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
188                   (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
189                   (Nat.S Nat.O)))))))))))))))) (Nat.S n')), Bool.False,
190                path))) n' r (Vector.VCons
191              ((Nat.minus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
192                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
193                 (Nat.S Nat.O)))))))))))))))) (Nat.S n')), Bool.True, path)))
194        | Stub s -> (fun _ -> seed)) __)) __ x x0
195
196(** val lookup_opt :
197    Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> 'a1 Types.option **)
198let rec lookup_opt n b t =
199  (match t with
200   | Leaf l -> (fun x -> Types.Some l)
201   | Node (h, l, r) ->
202     (fun b0 ->
203       lookup_opt h (Vector.tail h b0)
204         (match Vector.head' h b0 with
205          | Bool.True -> r
206          | Bool.False -> l))
207   | Stub x -> (fun x0 -> Types.None)) b
208
209(** val member :
210    Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> Bool.bool **)
211let member n b t =
212  match lookup_opt n b t with
213  | Types.None -> Bool.False
214  | Types.Some x -> Bool.True
215
216(** val lookup :
217    Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> 'a1 -> 'a1 **)
218let rec lookup n b t a =
219  (match b with
220   | Vector.VEmpty ->
221     (match t with
222      | Leaf l -> (fun _ -> l)
223      | Node (h, l, r) -> (fun _ -> assert false (* absurd case *))
224      | Stub s -> (fun _ -> a))
225   | Vector.VCons (o, hd, tl) ->
226     (match t with
227      | Leaf l -> (fun _ -> assert false (* absurd case *))
228      | Node (h, l, r) ->
229        (match hd with
230         | Bool.True -> (fun _ -> lookup h tl r a)
231         | Bool.False -> (fun _ -> lookup h tl l a))
232      | Stub s -> (fun _ -> a))) __
233
234(** val prepare_trie_for_insertion :
235    Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie **)
236let rec prepare_trie_for_insertion n b a =
237  match b with
238  | Vector.VEmpty -> Leaf a
239  | Vector.VCons (o, hd, tl) ->
240    (match hd with
241     | Bool.True -> Node (o, (Stub o), (prepare_trie_for_insertion o tl a))
242     | Bool.False -> Node (o, (prepare_trie_for_insertion o tl a), (Stub o)))
243
244(** val insert :
245    Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie -> 'a1
246    bitVectorTrie **)
247let rec insert n b a =
248  match b with
249  | Vector.VEmpty -> (fun x -> Leaf a)
250  | Vector.VCons (o, hd, tl) ->
251    (fun t ->
252      (match t with
253       | Leaf l -> (fun _ -> assert false (* absurd case *))
254       | Node (p, l, r) ->
255         (fun _ ->
256           match hd with
257           | Bool.True -> Node (o, l, (insert o tl a r))
258           | Bool.False -> Node (o, (insert o tl a l), r))
259       | Stub p ->
260         (fun _ ->
261           prepare_trie_for_insertion (Nat.S o) (Vector.VCons (o, hd, tl)) a))
262        __)
263
264(** val update :
265    Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie -> 'a1
266    bitVectorTrie Types.option **)
267let rec update n b a =
268  match b with
269  | Vector.VEmpty ->
270    (fun t ->
271      (match t with
272       | Leaf x -> (fun _ -> Types.Some (Leaf a))
273       | Node (x, x0, x1) -> (fun _ -> assert false (* absurd case *))
274       | Stub x -> (fun _ -> Types.None)) __)
275  | Vector.VCons (o, hd, tl) ->
276    (fun t ->
277      (match t with
278       | Leaf l -> (fun _ -> assert false (* absurd case *))
279       | Node (p, l, r) ->
280         (fun _ ->
281           match hd with
282           | Bool.True ->
283             Types.option_map (fun v -> Node (o, l, v)) (update o tl a r)
284           | Bool.False ->
285             Types.option_map (fun v -> Node (o, v, r)) (update o tl a l))
286       | Stub p -> (fun _ -> Types.None)) __)
287
288(** val merge :
289    Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie **)
290let rec merge n = function
291| Leaf l ->
292  (fun c ->
293    match c with
294    | Leaf a -> Leaf a
295    | Node (x, x0, x1) -> Leaf l
296    | Stub x -> Leaf l)
297| Node (p, l, r) ->
298  (fun c ->
299    (match c with
300     | Leaf x -> (fun _ -> Obj.magic Nat.nat_discr Nat.O (Nat.S p) __)
301     | Node (p', l', r') ->
302       (fun _ -> Node (p, (merge p l l'), (merge p r r')))
303     | Stub x -> (fun _ -> Node (p, l, r))) __)
304| Stub x -> (fun c -> c)
305
306open Deqsets
307
308type strong_decidable = (__, __) Types.sum
309
310(** val strong_decidable_in_codomain :
311    Deqsets.deqSet -> Nat.nat -> __ bitVectorTrie -> __ -> strong_decidable **)
312let strong_decidable_in_codomain a n m =
313  bitVectorTrie_rect_Type0 (fun a' a0 ->
314    Bool.bool_inv_rect_Type0 (Deqsets.eqb a a' a0) (fun _ -> Types.Inl __)
315      (fun _ -> Types.Inr __)) (fun n0 l r hl hr a0 ->
316    match hl a0 with
317    | Types.Inl _ -> Types.Inl __
318    | Types.Inr _ ->
319      (match hr a0 with
320       | Types.Inl _ -> Types.Inl __
321       | Types.Inr _ -> Types.Inr __)) (fun n0 a0 -> Types.Inr __) n m
322
Note: See TracBrowser for help on using the repository browser.