43 type 'a bitVectorTrie =
45 | Node of Nat.nat * 'a bitVectorTrie * 'a bitVectorTrie
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 **)
51 let 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)
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 **)
62 let 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)
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 **)
73 let 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)
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 **)
84 let 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)
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 **)
95 let 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)
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 **)
107 let bitVectorTrie_inv_rect_Type4 x2 hterm h1 h2 h3 =
108 let hcut = bitVectorTrie_rect_Type4 h1 h2 h3 x2 hterm in hcut __ __
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 **)
114 let bitVectorTrie_inv_rect_Type3 x2 hterm h1 h2 h3 =
115 let hcut = bitVectorTrie_rect_Type3 h1 h2 h3 x2 hterm in hcut __ __
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 **)
121 let bitVectorTrie_inv_rect_Type2 x2 hterm h1 h2 h3 =
122 let hcut = bitVectorTrie_rect_Type2 h1 h2 h3 x2 hterm in hcut __ __
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 **)
128 let bitVectorTrie_inv_rect_Type1 x2 hterm h1 h2 h3 =
129 let hcut = bitVectorTrie_rect_Type1 h1 h2 h3 x2 hterm in hcut __ __
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 **)
135 let bitVectorTrie_inv_rect_Type0 x2 hterm h1 h2 h3 =
136 let hcut = bitVectorTrie_rect_Type0 h1 h2 h3 x2 hterm in hcut __ __
138 (** val bitVectorTrie_discr :
139 Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> __ **)
140 let bitVectorTrie_discr a2 x y =
141 Logic.eq_rect_Type2 x
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
147 (** val bitVectorTrie_jmdiscr :
148 Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> __ **)
149 let bitVectorTrie_jmdiscr a2 x y =
150 Logic.eq_rect_Type2 x
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
157 Nat.nat -> (BitVector.bitVector -> 'a1 -> 'a2 -> 'a2) -> 'a1
158 bitVectorTrie -> 'a2 -> 'a2 **)
159 let rec fold n f t b =
161 | Leaf l -> (fun _ -> f (BitVector.zero n) l b)
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)) __
168 (** val bvtfold_aux :
169 (BitVector.bitVector -> 'a1 -> 'a2 -> 'a2) -> 'a2 -> Nat.nat -> 'a1
170 bitVectorTrie -> BitVector.bitVector -> 'a2 **)
171 let rec bvtfold_aux f seed n x x0 =
176 | Leaf l -> (fun _ -> f path l seed)
177 | Node (n', l, r) -> (fun _ -> assert false (* absurd case *))
178 | Stub s -> (fun _ -> seed)) __)
182 | Leaf l -> (fun _ -> assert false (* absurd case *))
183 | Node (n'', l, r) ->
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
197 Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> 'a1 Types.option **)
198 let rec lookup_opt n b t =
200 | Leaf l -> (fun x -> Types.Some l)
203 lookup_opt h (Vector.tail h b0)
204 (match Vector.head' h b0 with
207 | Stub x -> (fun x0 -> Types.None)) b
210 Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> Bool.bool **)
212 match lookup_opt n b t with
213 | Types.None -> Bool.False
214 | Types.Some x -> Bool.True
217 Nat.nat -> BitVector.bitVector -> 'a1 bitVectorTrie -> 'a1 -> 'a1 **)
218 let rec lookup n b t a =
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) ->
227 | Leaf l -> (fun _ -> assert false (* absurd case *))
230 | Bool.True -> (fun _ -> lookup h tl r a)
231 | Bool.False -> (fun _ -> lookup h tl l a))
232 | Stub s -> (fun _ -> a))) __
234 (** val prepare_trie_for_insertion :
235 Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie **)
236 let rec prepare_trie_for_insertion n b a =
238 | Vector.VEmpty -> Leaf a
239 | Vector.VCons (o, hd, tl) ->
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)))
245 Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie -> 'a1
247 let rec insert n b a =
249 | Vector.VEmpty -> (fun x -> Leaf a)
250 | Vector.VCons (o, hd, tl) ->
253 | Leaf l -> (fun _ -> assert false (* absurd case *))
257 | Bool.True -> Node (o, l, (insert o tl a r))
258 | Bool.False -> Node (o, (insert o tl a l), r))
261 prepare_trie_for_insertion (Nat.S o) (Vector.VCons (o, hd, tl)) a))
265 Nat.nat -> BitVector.bitVector -> 'a1 -> 'a1 bitVectorTrie -> 'a1
266 bitVectorTrie Types.option **)
267 let rec update n b a =
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) ->
278 | Leaf l -> (fun _ -> assert false (* absurd case *))
283 Types.option_map (fun v -> Node (o, l, v)) (update o tl a r)
285 Types.option_map (fun v -> Node (o, v, r)) (update o tl a l))
286 | Stub p -> (fun _ -> Types.None)) __)
289 Nat.nat -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie -> 'a1 bitVectorTrie **)
290 let rec merge n = function
295 | Node (x, x0, x1) -> Leaf l
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)
308 type strong_decidable = (__, __) Types.sum
310 (** val strong_decidable_in_codomain :
311 Deqsets.deqSet -> Nat.nat -> __ bitVectorTrie -> __ -> strong_decidable **)
312 let 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 ->
317 | Types.Inl _ -> Types.Inl __
320 | Types.Inl _ -> Types.Inl __
321 | Types.Inr _ -> Types.Inr __)) (fun n0 a0 -> Types.Inr __) n m