source: extracted/positiveMap.ml @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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_2169, x_2168, x_2167) ->
41  h_pm_node x_2169 x_2168 x_2167
42    (positive_map_rect_Type4 h_pm_leaf h_pm_node x_2168)
43    (positive_map_rect_Type4 h_pm_leaf h_pm_node x_2167)
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_2181, x_2180, x_2179) ->
51  h_pm_node x_2181 x_2180 x_2179
52    (positive_map_rect_Type3 h_pm_leaf h_pm_node x_2180)
53    (positive_map_rect_Type3 h_pm_leaf h_pm_node x_2179)
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_2187, x_2186, x_2185) ->
61  h_pm_node x_2187 x_2186 x_2185
62    (positive_map_rect_Type2 h_pm_leaf h_pm_node x_2186)
63    (positive_map_rect_Type2 h_pm_leaf h_pm_node x_2185)
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_2193, x_2192, x_2191) ->
71  h_pm_node x_2193 x_2192 x_2191
72    (positive_map_rect_Type1 h_pm_leaf h_pm_node x_2192)
73    (positive_map_rect_Type1 h_pm_leaf h_pm_node x_2191)
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_2199, x_2198, x_2197) ->
81  h_pm_node x_2199 x_2198 x_2197
82    (positive_map_rect_Type0 h_pm_leaf h_pm_node x_2198)
83    (positive_map_rect_Type0 h_pm_leaf h_pm_node x_2197)
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.