source: extracted/positiveMap.ml @ 2716

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

...

File size: 12.7 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Bool
14
15open Relations
16
17open Nat
18
19open Positive
20
21open Div_and_mod
22
23open Jmeq
24
25open Russell
26
27open List
28
29open Util
30
31type 'a positive_map =
32| Pm_leaf
33| Pm_node of 'a Types.option * 'a positive_map * 'a positive_map
34
35(** val positive_map_rect_Type4 :
36    'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2
37    -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 **)
38let rec positive_map_rect_Type4 h_pm_leaf h_pm_node = function
39| Pm_leaf -> h_pm_leaf
40| Pm_node (x_3092, x_3091, x_3090) ->
41  h_pm_node x_3092 x_3091 x_3090
42    (positive_map_rect_Type4 h_pm_leaf h_pm_node x_3091)
43    (positive_map_rect_Type4 h_pm_leaf h_pm_node x_3090)
44
45(** val positive_map_rect_Type3 :
46    'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2
47    -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 **)
48let rec positive_map_rect_Type3 h_pm_leaf h_pm_node = function
49| Pm_leaf -> h_pm_leaf
50| Pm_node (x_3104, x_3103, x_3102) ->
51  h_pm_node x_3104 x_3103 x_3102
52    (positive_map_rect_Type3 h_pm_leaf h_pm_node x_3103)
53    (positive_map_rect_Type3 h_pm_leaf h_pm_node x_3102)
54
55(** val positive_map_rect_Type2 :
56    'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2
57    -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 **)
58let rec positive_map_rect_Type2 h_pm_leaf h_pm_node = function
59| Pm_leaf -> h_pm_leaf
60| Pm_node (x_3110, x_3109, x_3108) ->
61  h_pm_node x_3110 x_3109 x_3108
62    (positive_map_rect_Type2 h_pm_leaf h_pm_node x_3109)
63    (positive_map_rect_Type2 h_pm_leaf h_pm_node x_3108)
64
65(** val positive_map_rect_Type1 :
66    'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2
67    -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 **)
68let rec positive_map_rect_Type1 h_pm_leaf h_pm_node = function
69| Pm_leaf -> h_pm_leaf
70| Pm_node (x_3116, x_3115, x_3114) ->
71  h_pm_node x_3116 x_3115 x_3114
72    (positive_map_rect_Type1 h_pm_leaf h_pm_node x_3115)
73    (positive_map_rect_Type1 h_pm_leaf h_pm_node x_3114)
74
75(** val positive_map_rect_Type0 :
76    'a2 -> ('a1 Types.option -> 'a1 positive_map -> 'a1 positive_map -> 'a2
77    -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 **)
78let rec positive_map_rect_Type0 h_pm_leaf h_pm_node = function
79| Pm_leaf -> h_pm_leaf
80| Pm_node (x_3122, x_3121, x_3120) ->
81  h_pm_node x_3122 x_3121 x_3120
82    (positive_map_rect_Type0 h_pm_leaf h_pm_node x_3121)
83    (positive_map_rect_Type0 h_pm_leaf h_pm_node x_3120)
84
85(** val positive_map_inv_rect_Type4 :
86    'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map
87    -> 'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **)
88let positive_map_inv_rect_Type4 hterm h1 h2 =
89  let hcut = positive_map_rect_Type4 h1 h2 hterm in hcut __
90
91(** val positive_map_inv_rect_Type3 :
92    'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map
93    -> 'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **)
94let positive_map_inv_rect_Type3 hterm h1 h2 =
95  let hcut = positive_map_rect_Type3 h1 h2 hterm in hcut __
96
97(** val positive_map_inv_rect_Type2 :
98    'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map
99    -> 'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **)
100let positive_map_inv_rect_Type2 hterm h1 h2 =
101  let hcut = positive_map_rect_Type2 h1 h2 hterm in hcut __
102
103(** val positive_map_inv_rect_Type1 :
104    'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map
105    -> 'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **)
106let positive_map_inv_rect_Type1 hterm h1 h2 =
107  let hcut = positive_map_rect_Type1 h1 h2 hterm in hcut __
108
109(** val positive_map_inv_rect_Type0 :
110    'a1 positive_map -> (__ -> 'a2) -> ('a1 Types.option -> 'a1 positive_map
111    -> 'a1 positive_map -> (__ -> 'a2) -> (__ -> 'a2) -> __ -> 'a2) -> 'a2 **)
112let positive_map_inv_rect_Type0 hterm h1 h2 =
113  let hcut = positive_map_rect_Type0 h1 h2 hterm in hcut __
114
115(** val positive_map_discr : 'a1 positive_map -> 'a1 positive_map -> __ **)
116let positive_map_discr x y =
117  Logic.eq_rect_Type2 x
118    (match x with
119     | Pm_leaf -> Obj.magic (fun _ dH -> dH)
120     | Pm_node (a0, a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
121
122(** val positive_map_jmdiscr : 'a1 positive_map -> 'a1 positive_map -> __ **)
123let positive_map_jmdiscr x y =
124  Logic.eq_rect_Type2 x
125    (match x with
126     | Pm_leaf -> Obj.magic (fun _ dH -> dH)
127     | Pm_node (a0, a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
128
129(** val lookup_opt : Positive.pos -> 'a1 positive_map -> 'a1 Types.option **)
130let rec lookup_opt b = function
131| Pm_leaf -> Types.None
132| Pm_node (a, l, r) ->
133  (match b with
134   | Positive.One -> a
135   | Positive.P1 tl -> lookup_opt tl r
136   | Positive.P0 tl -> lookup_opt tl l)
137
138(** val lookup : Positive.pos -> 'a1 positive_map -> 'a1 -> 'a1 **)
139let lookup b t x =
140  match lookup_opt b t with
141  | Types.None -> x
142  | Types.Some r -> r
143
144(** val pm_set :
145    Positive.pos -> 'a1 Types.option -> 'a1 positive_map -> 'a1 positive_map **)
146let rec pm_set b a t =
147  match b with
148  | Positive.One ->
149    (match t with
150     | Pm_leaf -> Pm_node (a, Pm_leaf, Pm_leaf)
151     | Pm_node (x, l, r) -> Pm_node (a, l, r))
152  | Positive.P1 tl ->
153    (match t with
154     | Pm_leaf -> Pm_node (Types.None, Pm_leaf, (pm_set tl a Pm_leaf))
155     | Pm_node (x, l, r) -> Pm_node (x, l, (pm_set tl a r)))
156  | Positive.P0 tl ->
157    (match t with
158     | Pm_leaf -> Pm_node (Types.None, (pm_set tl a Pm_leaf), Pm_leaf)
159     | Pm_node (x, l, r) -> Pm_node (x, (pm_set tl a l), r))
160
161(** val insert :
162    Positive.pos -> 'a1 -> 'a1 positive_map -> 'a1 positive_map **)
163let insert p a =
164  pm_set p (Types.Some a)
165
166(** val update :
167    Positive.pos -> 'a1 -> 'a1 positive_map -> 'a1 positive_map Types.option **)
168let rec update b a t =
169  match b with
170  | Positive.One ->
171    (match t with
172     | Pm_leaf -> Types.None
173     | Pm_node (x, l, r) ->
174       Types.option_map (fun x0 -> Pm_node ((Types.Some a), l, r)) x)
175  | Positive.P1 tl ->
176    (match t with
177     | Pm_leaf -> Types.None
178     | Pm_node (x, l, r) ->
179       Types.option_map (fun r5 -> Pm_node (x, l, r5)) (update tl a r))
180  | Positive.P0 tl ->
181    (match t with
182     | Pm_leaf -> Types.None
183     | Pm_node (x, l, r) ->
184       Types.option_map (fun l0 -> Pm_node (x, l0, r)) (update tl a l))
185
186(** val fold0 :
187    (Positive.pos -> 'a1 -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 -> 'a2 **)
188let rec fold0 f t b =
189  match t with
190  | Pm_leaf -> b
191  | Pm_node (a, l, r) ->
192    let b0 =
193      match a with
194      | Types.None -> b
195      | Types.Some a0 -> f Positive.One a0 b
196    in
197    let b1 = fold0 (fun x -> f (Positive.P0 x)) l b0 in
198    fold0 (fun x -> f (Positive.P1 x)) r b1
199
200(** val domain_of_pm : 'a1 positive_map -> Types.unit0 positive_map **)
201let domain_of_pm t =
202  fold0 (fun p a b -> insert p Types.It b) t Pm_leaf
203
204open Setoids
205
206open Monad
207
208open Option
209
210(** val is_none : 'a1 Types.option -> Bool.bool **)
211let is_none = function
212| Types.None -> Bool.True
213| Types.Some x -> Bool.False
214
215(** val is_pm_leaf : 'a1 positive_map -> Bool.bool **)
216let is_pm_leaf = function
217| Pm_leaf -> Bool.True
218| Pm_node (x, x0, x1) -> Bool.False
219
220(** val map_opt :
221    ('a1 -> 'a2 Types.option) -> 'a1 positive_map -> 'a2 positive_map **)
222let rec map_opt f = function
223| Pm_leaf -> Pm_leaf
224| Pm_node (a, l, r) ->
225  let a' =
226    Monad.m_bind0 (Monad.max_def Option.option0) (Obj.magic a) (fun x ->
227      Obj.magic f x)
228  in
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'))
232           (is_pm_leaf r') with
233   | Bool.True -> Pm_leaf
234   | Bool.False -> Pm_node ((Obj.magic a'), l', r'))
235
236(** val map0 : ('a1 -> 'a2) -> 'a1 positive_map -> 'a2 positive_map **)
237let map0 f =
238  map_opt (fun x -> Types.Some (f x))
239
240(** val merge :
241    ('a1 Types.option -> 'a2 Types.option -> 'a3 Types.option) -> 'a1
242    positive_map -> 'a2 positive_map -> 'a3 positive_map **)
243let rec merge choice a b =
244  match a with
245  | Pm_leaf -> map_opt (fun x -> choice Types.None (Types.Some x)) b
246  | Pm_node (o, l, r) ->
247    (match b with
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'')))
257
258(** val domain_size : 'a1 positive_map -> Nat.nat **)
259let rec domain_size = function
260| Pm_leaf -> Nat.O
261| Pm_node (a, l, r) ->
262  Nat.plus
263    (Nat.plus
264      (match a with
265       | Types.None -> Nat.O
266       | Types.Some x -> Nat.S Nat.O) (domain_size l)) (domain_size r)
267
268(** val pm_all_aux :
269    'a1 positive_map -> 'a1 positive_map -> (Positive.pos -> Positive.pos) ->
270    (Positive.pos -> 'a1 -> __ -> Bool.bool) -> Bool.bool **)
271let rec pm_all_aux m t pre x =
272  (match t with
273   | Pm_leaf -> (fun _ x0 -> Bool.True)
274   | Pm_node (a, l, r) ->
275     (fun _ f ->
276       Bool.andb
277         (Bool.andb (pm_all_aux m l (fun x0 -> pre (Positive.P0 x0)) f)
278           ((match a with
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
282
283(** val pm_all :
284    'a1 positive_map -> (Positive.pos -> 'a1 -> __ -> Bool.bool) -> Bool.bool **)
285let pm_all m f =
286  pm_all_aux m m (fun x -> x) f
287
288(** val pm_choose :
289    'a1 positive_map -> ((Positive.pos, 'a1) Types.prod, 'a1 positive_map)
290    Types.prod Types.option **)
291let rec pm_choose = function
292| Pm_leaf -> Types.None
293| Pm_node (a, l, r) ->
294  (match pm_choose l with
295   | Types.None ->
296     (match pm_choose r with
297      | Types.None ->
298        (match a with
299         | Types.None -> Types.None
300         | Types.Some a0 ->
301           Types.Some { Types.fst = { Types.fst = Positive.One; Types.snd =
302             a0 }; Types.snd = Pm_leaf })
303      | Types.Some x ->
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)) })
307   | Types.Some x ->
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)) })
311
312(** val pm_try_remove :
313    Positive.pos -> 'a1 positive_map -> ('a1, 'a1 positive_map) Types.prod
314    Types.option **)
315let rec pm_try_remove b t =
316  match b with
317  | Positive.One ->
318    (match t with
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)
323  | Positive.P1 tl ->
324    (match t with
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))
329  | Positive.P0 tl ->
330    (match t with
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))
335
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 **)
339let rec pm_fold_inf_aux t f t' pre b =
340  (match t' with
341   | Pm_leaf -> (fun _ -> b)
342   | Pm_node (a, l, r) ->
343     (fun _ ->
344       let b0 =
345         (match a with
346          | Types.None -> (fun _ -> b)
347          | Types.Some a0 -> (fun _ -> f (pre Positive.One) a0 __ b)) __
348       in
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)) __
351
352(** val pm_fold_inf :
353    'a1 positive_map -> (Positive.pos -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a2 ->
354    'a2 **)
355let pm_fold_inf t f b =
356  pm_fold_inf_aux t f t (fun x -> x) b
357
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 **)
361let rec pm_find_aux pre t p =
362  match t with
363  | Pm_leaf -> Types.None
364  | Pm_node (a, l, r) ->
365    let x =
366      match a with
367      | Types.None -> Types.None
368      | Types.Some a0 ->
369        (match p (pre Positive.One) a0 with
370         | Bool.True ->
371           Types.Some { Types.fst = (pre Positive.One); Types.snd = a0 }
372         | Bool.False -> Types.None)
373    in
374    (match x with
375     | 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)
380
381(** val pm_find :
382    'a1 positive_map -> (Positive.pos -> 'a1 -> Bool.bool) -> (Positive.pos,
383    'a1) Types.prod Types.option **)
384let pm_find x x0 =
385  pm_find_aux (fun x1 -> x1) x x0
386
Note: See TracBrowser for help on using the repository browser.