source: extracted/positiveMap.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: 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
31open Setoids
32
33open Monad
34
35open Option
36
37type 'a positive_map =
38| Pm_leaf
39| Pm_node of 'a Types.option * 'a positive_map * 'a positive_map
40
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 **)
44let rec positive_map_rect_Type4 h_pm_leaf h_pm_node = function
45| Pm_leaf -> h_pm_leaf
46| Pm_node (x_3144, x_3143, x_3142) ->
47  h_pm_node x_3144 x_3143 x_3142
48    (positive_map_rect_Type4 h_pm_leaf h_pm_node x_3143)
49    (positive_map_rect_Type4 h_pm_leaf h_pm_node x_3142)
50
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 **)
54let rec positive_map_rect_Type3 h_pm_leaf h_pm_node = function
55| Pm_leaf -> h_pm_leaf
56| Pm_node (x_3156, x_3155, x_3154) ->
57  h_pm_node x_3156 x_3155 x_3154
58    (positive_map_rect_Type3 h_pm_leaf h_pm_node x_3155)
59    (positive_map_rect_Type3 h_pm_leaf h_pm_node x_3154)
60
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 **)
64let rec positive_map_rect_Type2 h_pm_leaf h_pm_node = function
65| Pm_leaf -> h_pm_leaf
66| Pm_node (x_3162, x_3161, x_3160) ->
67  h_pm_node x_3162 x_3161 x_3160
68    (positive_map_rect_Type2 h_pm_leaf h_pm_node x_3161)
69    (positive_map_rect_Type2 h_pm_leaf h_pm_node x_3160)
70
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 **)
74let rec positive_map_rect_Type1 h_pm_leaf h_pm_node = function
75| Pm_leaf -> h_pm_leaf
76| Pm_node (x_3168, x_3167, x_3166) ->
77  h_pm_node x_3168 x_3167 x_3166
78    (positive_map_rect_Type1 h_pm_leaf h_pm_node x_3167)
79    (positive_map_rect_Type1 h_pm_leaf h_pm_node x_3166)
80
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 **)
84let rec positive_map_rect_Type0 h_pm_leaf h_pm_node = function
85| Pm_leaf -> h_pm_leaf
86| Pm_node (x_3174, x_3173, x_3172) ->
87  h_pm_node x_3174 x_3173 x_3172
88    (positive_map_rect_Type0 h_pm_leaf h_pm_node x_3173)
89    (positive_map_rect_Type0 h_pm_leaf h_pm_node x_3172)
90
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 **)
94let positive_map_inv_rect_Type4 hterm h1 h2 =
95  let hcut = positive_map_rect_Type4 h1 h2 hterm in hcut __
96
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 **)
100let positive_map_inv_rect_Type3 hterm h1 h2 =
101  let hcut = positive_map_rect_Type3 h1 h2 hterm in hcut __
102
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 **)
106let positive_map_inv_rect_Type2 hterm h1 h2 =
107  let hcut = positive_map_rect_Type2 h1 h2 hterm in hcut __
108
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 **)
112let positive_map_inv_rect_Type1 hterm h1 h2 =
113  let hcut = positive_map_rect_Type1 h1 h2 hterm in hcut __
114
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 **)
118let positive_map_inv_rect_Type0 hterm h1 h2 =
119  let hcut = positive_map_rect_Type0 h1 h2 hterm in hcut __
120
121(** val positive_map_discr : 'a1 positive_map -> 'a1 positive_map -> __ **)
122let positive_map_discr x y =
123  Logic.eq_rect_Type2 x
124    (match x with
125     | Pm_leaf -> Obj.magic (fun _ dH -> dH)
126     | Pm_node (a0, a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
127
128(** val positive_map_jmdiscr : 'a1 positive_map -> 'a1 positive_map -> __ **)
129let positive_map_jmdiscr x y =
130  Logic.eq_rect_Type2 x
131    (match x with
132     | Pm_leaf -> Obj.magic (fun _ dH -> dH)
133     | Pm_node (a0, a10, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
134
135(** val lookup_opt : Positive.pos -> 'a1 positive_map -> 'a1 Types.option **)
136let rec lookup_opt b = function
137| Pm_leaf -> Types.None
138| Pm_node (a, l, r) ->
139  (match b with
140   | Positive.One -> a
141   | Positive.P1 tl -> lookup_opt tl r
142   | Positive.P0 tl -> lookup_opt tl l)
143
144(** val lookup : Positive.pos -> 'a1 positive_map -> 'a1 -> 'a1 **)
145let lookup b t x =
146  match lookup_opt b t with
147  | Types.None -> x
148  | Types.Some r -> r
149
150(** val pm_set :
151    Positive.pos -> 'a1 Types.option -> 'a1 positive_map -> 'a1 positive_map **)
152let rec pm_set b a t =
153  match b with
154  | Positive.One ->
155    (match t with
156     | Pm_leaf -> Pm_node (a, Pm_leaf, Pm_leaf)
157     | Pm_node (x, l, r) -> Pm_node (a, l, r))
158  | Positive.P1 tl ->
159    (match t with
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)))
162  | Positive.P0 tl ->
163    (match t with
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))
166
167(** val insert :
168    Positive.pos -> 'a1 -> 'a1 positive_map -> 'a1 positive_map **)
169let insert p a =
170  pm_set p (Types.Some a)
171
172(** val update :
173    Positive.pos -> 'a1 -> 'a1 positive_map -> 'a1 positive_map Types.option **)
174let rec update b a t =
175  match b with
176  | Positive.One ->
177    (match t with
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)
181  | Positive.P1 tl ->
182    (match t with
183     | Pm_leaf -> Types.None
184     | Pm_node (x, l, r) ->
185       Types.option_map (fun r5 -> Pm_node (x, l, r5)) (update tl a r))
186  | Positive.P0 tl ->
187    (match t with
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))
191
192(** val fold0 :
193    (Positive.pos -> 'a1 -> 'a2 -> 'a2) -> 'a1 positive_map -> 'a2 -> 'a2 **)
194let rec fold0 f t b =
195  match t with
196  | Pm_leaf -> b
197  | Pm_node (a, l, r) ->
198    let b0 =
199      match a with
200      | Types.None -> b
201      | Types.Some a0 -> f Positive.One a0 b
202    in
203    let b1 = fold0 (fun x -> f (Positive.P0 x)) l b0 in
204    fold0 (fun x -> f (Positive.P1 x)) r b1
205
206(** val domain_of_pm : 'a1 positive_map -> Types.unit0 positive_map **)
207let domain_of_pm t =
208  fold0 (fun p a b -> insert p Types.It b) t Pm_leaf
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.