37 type 'a positive_map =
39 | Pm_node of 'a Types.option * 'a positive_map * 'a positive_map
41 (** val positive_map_rect_Type4 :
42 'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2
43 -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 **)
44 let rec positive_map_rect_Type4 h_pm_leaf h_pm_node = function
45 | Pm_leaf -> h_pm_leaf
46 | Pm_node (x_3300, x_3299, x_3298) ->
47 h_pm_node x_3300 x_3299 x_3298
48 (positive_map_rect_Type4 h_pm_leaf h_pm_node x_3299)
49 (positive_map_rect_Type4 h_pm_leaf h_pm_node x_3298)
51 (** val positive_map_rect_Type3 :
52 'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2
53 -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 **)
54 let rec positive_map_rect_Type3 h_pm_leaf h_pm_node = function
55 | Pm_leaf -> h_pm_leaf
56 | Pm_node (x_3312, x_3311, x_3310) ->
57 h_pm_node x_3312 x_3311 x_3310
58 (positive_map_rect_Type3 h_pm_leaf h_pm_node x_3311)
59 (positive_map_rect_Type3 h_pm_leaf h_pm_node x_3310)
61 (** val positive_map_rect_Type2 :
62 'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2
63 -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 **)
64 let rec positive_map_rect_Type2 h_pm_leaf h_pm_node = function
65 | Pm_leaf -> h_pm_leaf
66 | Pm_node (x_3318, x_3317, x_3316) ->
67 h_pm_node x_3318 x_3317 x_3316
68 (positive_map_rect_Type2 h_pm_leaf h_pm_node x_3317)
69 (positive_map_rect_Type2 h_pm_leaf h_pm_node x_3316)
71 (** val positive_map_rect_Type1 :
72 'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2
73 -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 **)
74 let rec positive_map_rect_Type1 h_pm_leaf h_pm_node = function
75 | Pm_leaf -> h_pm_leaf
76 | Pm_node (x_3324, x_3323, x_3322) ->
77 h_pm_node x_3324 x_3323 x_3322
78 (positive_map_rect_Type1 h_pm_leaf h_pm_node x_3323)
79 (positive_map_rect_Type1 h_pm_leaf h_pm_node x_3322)
81 (** val positive_map_rect_Type0 :
82 'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2
83 -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 **)
84 let rec positive_map_rect_Type0 h_pm_leaf h_pm_node = function
85 | Pm_leaf -> h_pm_leaf
86 | Pm_node (x_3330, x_3329, x_3328) ->
87 h_pm_node x_3330 x_3329 x_3328
88 (positive_map_rect_Type0 h_pm_leaf h_pm_node x_3329)
89 (positive_map_rect_Type0 h_pm_leaf h_pm_node x_3328)
91 (** val positive_map_inv_rect_Type4 :
92 'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map
93 -> 'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **)
94 let positive_map_inv_rect_Type4 hterm h1 h2 =
95 let hcut = positive_map_rect_Type4 h1 h2 hterm in hcut __
97 (** val positive_map_inv_rect_Type3 :
98 'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map
99 -> 'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **)
100 let positive_map_inv_rect_Type3 hterm h1 h2 =
101 let hcut = positive_map_rect_Type3 h1 h2 hterm in hcut __
103 (** val positive_map_inv_rect_Type2 :
104 'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map
105 -> 'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **)
106 let positive_map_inv_rect_Type2 hterm h1 h2 =
107 let hcut = positive_map_rect_Type2 h1 h2 hterm in hcut __
109 (** val positive_map_inv_rect_Type1 :
110 'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map
111 -> 'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **)
112 let positive_map_inv_rect_Type1 hterm h1 h2 =
113 let hcut = positive_map_rect_Type1 h1 h2 hterm in hcut __
115 (** val positive_map_inv_rect_Type0 :
116 'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map
117 -> 'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **)
118 let positive_map_inv_rect_Type0 hterm h1 h2 =
119 let hcut = positive_map_rect_Type0 h1 h2 hterm in hcut __
121 (** val positive_map_discr : 'a1 positive_map -> 'a1 positive_map -> __ **)
122 let positive_map_discr x y =
123 Logic.eq_rect_Type2 x
125 | Pm_leaf -> Obj.magic (fun _ dH -> dH)
126 | Pm_node (a0, a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
128 (** val positive_map_jmdiscr : 'a1 positive_map -> 'a1 positive_map -> __ **)
129 let positive_map_jmdiscr x y =
130 Logic.eq_rect_Type2 x
132 | Pm_leaf -> Obj.magic (fun _ dH -> dH)
133 | Pm_node (a0, a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
135 (** val lookup_opt : Positive.pos -> 'a1 positive_map -> 'a1 Types.option **)
136 let rec lookup_opt b = function
137 | Pm_leaf -> Types.None
138 | Pm_node (a, l, r) ->
141 | Positive.P1 tl -> lookup_opt tl r
142 | Positive.P0 tl -> lookup_opt tl l)
144 (** val lookup : Positive.pos -> 'a1 positive_map -> 'a1 -> 'a1 **)
146 match lookup_opt b t with
151 Positive.pos -> 'a1 Types.option -> 'a1 positive_map -> 'a1 positive_map **)
152 let rec pm_set b a t =
156 | Pm_leaf -> Pm_node (a, Pm_leaf, Pm_leaf)
157 | Pm_node (x, l, r) -> Pm_node (a, l, r))
160 | Pm_leaf -> Pm_node (Types.None, Pm_leaf, (pm_set tl a Pm_leaf))
161 | Pm_node (x, l, r) -> Pm_node (x, l, (pm_set tl a r)))
164 | Pm_leaf -> Pm_node (Types.None, (pm_set tl a Pm_leaf), Pm_leaf)
165 | Pm_node (x, l, r) -> Pm_node (x, (pm_set tl a l), r))
168 Positive.pos -> 'a1 -> 'a1 positive_map -> 'a1 positive_map **)
170 pm_set p (Types.Some a)
173 Positive.pos -> 'a1 -> 'a1 positive_map -> 'a1 positive_map Types.option **)
174 let rec update b a t =
178 | Pm_leaf -> Types.None
179 | Pm_node (x, l, r) ->
180 Types.option_map (fun x0 -> Pm_node ((Types.Some a), l, r)) x)
183 | Pm_leaf -> Types.None
184 | Pm_node (x, l, r) ->
185 Types.option_map (fun r0 -> Pm_node (x, l, r0)) (update tl a r))
188 | Pm_leaf -> Types.None
189 | Pm_node (x, l, r) ->
190 Types.option_map (fun l0 -> Pm_node (x, l0, r)) (update tl a l))
193 (Positive.pos -> 'a1 -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 -> 'a2 **)
197 | Pm_node (a, l, r) ->
201 | Types.Some a0 -> f Positive.One a0 b
203 let b1 = fold (fun x -> f (Positive.P0 x)) l b0 in
204 fold (fun x -> f (Positive.P1 x)) r b1
206 (** val domain_of_pm : 'a1 positive_map -> Types.unit0 positive_map **)
208 fold (fun p a b -> insert p Types.It b) t Pm_leaf
210 (** val is_none : 'a1 Types.option -> Bool.bool **)
211 let is_none = function
212 | Types.None -> Bool.True
213 | Types.Some x -> Bool.False
215 (** val is_pm_leaf : 'a1 positive_map -> Bool.bool **)
216 let is_pm_leaf = function
217 | Pm_leaf -> Bool.True
218 | Pm_node (x, x0, x1) -> Bool.False
221 ('a1 -> 'a2 Types.option) -> 'a1 positive_map -> 'a2 positive_map **)
222 let rec map_opt f = function
224 | Pm_node (a, l, r) ->
226 Monad.m_bind0 (Monad.max_def Option.option) (Obj.magic a) (fun x ->
229 let l' = map_opt f l in
230 let r' = map_opt f r in
231 (match Bool.andb (Bool.andb (is_none (Obj.magic a')) (is_pm_leaf l'))
233 | Bool.True -> Pm_leaf
234 | Bool.False -> Pm_node ((Obj.magic a'), l', r'))
236 (** val map : ('a1 -> 'a2) -> 'a1 positive_map -> 'a2 positive_map **)
238 map_opt (fun x -> Types.Some (f x))
241 ('a1 Types.option -> 'a2 Types.option -> 'a3 Types.option) -> 'a1
242 positive_map -> 'a2 positive_map -> 'a3 positive_map **)
243 let rec merge choice a b =
245 | Pm_leaf -> map_opt (fun x -> choice Types.None (Types.Some x)) b
246 | Pm_node (o, l, r) ->
248 | Pm_leaf -> map_opt (fun x -> choice (Types.Some x) Types.None) a
249 | Pm_node (o', l', r') ->
250 let o'' = choice o o' in
251 let l'' = merge choice l l' in
252 let r'' = merge choice r r' in
253 (match Bool.andb (Bool.andb (is_none o'') (is_pm_leaf l''))
254 (is_pm_leaf r'') with
255 | Bool.True -> Pm_leaf
256 | Bool.False -> Pm_node (o'', l'', r'')))
258 (** val domain_size : 'a1 positive_map -> Nat.nat **)
259 let rec domain_size = function
261 | Pm_node (a, l, r) ->
265 | Types.None -> Nat.O
266 | Types.Some x -> Nat.S Nat.O) (domain_size l)) (domain_size r)
269 'a1 positive_map -> 'a1 positive_map -> (Positive.pos -> Positive.pos) ->
270 (Positive.pos -> 'a1 -> __ -> Bool.bool) -> Bool.bool **)
271 let rec pm_all_aux m t pre x =
273 | Pm_leaf -> (fun _ x0 -> Bool.True)
274 | Pm_node (a, l, r) ->
277 (Bool.andb (pm_all_aux m l (fun x0 -> pre (Positive.P0 x0)) f)
279 | Types.None -> (fun _ -> Bool.True)
280 | Types.Some a' -> (fun _ -> f (pre Positive.One) a' __)) __))
281 (pm_all_aux m r (fun x0 -> pre (Positive.P1 x0)) f))) __ x
284 'a1 positive_map -> (Positive.pos -> 'a1 -> __ -> Bool.bool) -> Bool.bool **)
286 pm_all_aux m m (fun x -> x) f
289 'a1 positive_map -> ((Positive.pos, 'a1) Types.prod, 'a1 positive_map)
290 Types.prod Types.option **)
291 let rec pm_choose = function
292 | Pm_leaf -> Types.None
293 | Pm_node (a, l, r) ->
294 (match pm_choose l with
296 (match pm_choose r with
299 | Types.None -> Types.None
301 Types.Some { Types.fst = { Types.fst = Positive.One; Types.snd =
302 a0 }; Types.snd = Pm_leaf })
304 Types.Some { Types.fst = { Types.fst = (Positive.P1
305 x.Types.fst.Types.fst); Types.snd = x.Types.fst.Types.snd };
306 Types.snd = (Pm_node (a, l, x.Types.snd)) })
308 Types.Some { Types.fst = { Types.fst = (Positive.P0
309 x.Types.fst.Types.fst); Types.snd = x.Types.fst.Types.snd };
310 Types.snd = (Pm_node (a, x.Types.snd, r)) })
312 (** val pm_try_remove :
313 Positive.pos -> 'a1 positive_map -> ('a1, 'a1 positive_map) Types.prod
315 let rec pm_try_remove b t =
319 | Pm_leaf -> Types.None
320 | Pm_node (x, l, r) ->
321 Types.option_map (fun x0 -> { Types.fst = x0; Types.snd = (Pm_node
322 (Types.None, l, r)) }) x)
325 | Pm_leaf -> Types.None
326 | Pm_node (x, l, r) ->
327 Types.option_map (fun xr -> { Types.fst = xr.Types.fst; Types.snd =
328 (Pm_node (x, l, xr.Types.snd)) }) (pm_try_remove tl r))
331 | Pm_leaf -> Types.None
332 | Pm_node (x, l, r) ->
333 Types.option_map (fun xl -> { Types.fst = xl.Types.fst; Types.snd =
334 (Pm_node (x, xl.Types.snd, r)) }) (pm_try_remove tl l))
336 (** val pm_fold_inf_aux :
337 'a1 positive_map -> (Positive.pos -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a1
338 positive_map -> (Positive.pos -> Positive.pos) -> 'a2 -> 'a2 **)
339 let rec pm_fold_inf_aux t f t' pre b =
341 | Pm_leaf -> (fun _ -> b)
342 | Pm_node (a, l, r) ->
346 | Types.None -> (fun _ -> b)
347 | Types.Some a0 -> (fun _ -> f (pre Positive.One) a0 __ b)) __
349 let b1 = pm_fold_inf_aux t f l (fun x -> pre (Positive.P0 x)) b0 in
350 pm_fold_inf_aux t f r (fun x -> pre (Positive.P1 x)) b1)) __
352 (** val pm_fold_inf :
353 'a1 positive_map -> (Positive.pos -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a2 ->
355 let pm_fold_inf t f b =
356 pm_fold_inf_aux t f t (fun x -> x) b
358 (** val pm_find_aux :
359 (Positive.pos -> Positive.pos) -> 'a1 positive_map -> (Positive.pos ->
360 'a1 -> Bool.bool) -> (Positive.pos, 'a1) Types.prod Types.option **)
361 let rec pm_find_aux pre t p =
363 | Pm_leaf -> Types.None
364 | Pm_node (a, l, r) ->
367 | Types.None -> Types.None
369 (match p (pre Positive.One) a0 with
371 Types.Some { Types.fst = (pre Positive.One); Types.snd = a0 }
372 | Bool.False -> Types.None)
376 (match pm_find_aux (fun x0 -> pre (Positive.P0 x0)) l p with
377 | Types.None -> pm_find_aux (fun x0 -> pre (Positive.P1 x0)) r p
378 | Types.Some y -> Types.Some y)
379 | Types.Some x0 -> Types.Some x0)
382 'a1 positive_map -> (Positive.pos -> 'a1 -> Bool.bool) -> (Positive.pos,
383 'a1) Types.prod Types.option **)
385 pm_find_aux (fun x1 -> x1) x x0