source: extracted/identifiers.ml @ 2601

Last change on this file since 2601 was 2601, checked in by sacerdot, 8 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: 15.8 KB
Line 
1open Preamble
2
3open Hints_declaration
4
5open Core_notation
6
7open Pts
8
9open Logic
10
11open Types
12
13open Char
14
15open Bool
16
17open Relations
18
19open Nat
20
21open List
22
23open String
24
25open Positive
26
27open Setoids
28
29open Monad
30
31open Option
32
33open Div_and_mod
34
35open Jmeq
36
37open Russell
38
39open Util
40
41open Lists
42
43open Extralib
44
45open PreIdentifiers
46
47open Errors
48
49type universe =
50  Positive.pos
51  (* singleton inductive, whose constructor was mk_universe *)
52
53(** val universe_rect_Type4 :
54    String.string -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
55let rec universe_rect_Type4 tag h_mk_universe x_2108 =
56  let next_identifier = x_2108 in h_mk_universe next_identifier
57
58(** val universe_rect_Type5 :
59    String.string -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
60let rec universe_rect_Type5 tag h_mk_universe x_2110 =
61  let next_identifier = x_2110 in h_mk_universe next_identifier
62
63(** val universe_rect_Type3 :
64    String.string -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
65let rec universe_rect_Type3 tag h_mk_universe x_2112 =
66  let next_identifier = x_2112 in h_mk_universe next_identifier
67
68(** val universe_rect_Type2 :
69    String.string -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
70let rec universe_rect_Type2 tag h_mk_universe x_2114 =
71  let next_identifier = x_2114 in h_mk_universe next_identifier
72
73(** val universe_rect_Type1 :
74    String.string -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
75let rec universe_rect_Type1 tag h_mk_universe x_2116 =
76  let next_identifier = x_2116 in h_mk_universe next_identifier
77
78(** val universe_rect_Type0 :
79    String.string -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
80let rec universe_rect_Type0 tag h_mk_universe x_2118 =
81  let next_identifier = x_2118 in h_mk_universe next_identifier
82
83(** val next_identifier : String.string -> universe -> Positive.pos **)
84let rec next_identifier tag xxx =
85  let yyy = xxx in yyy
86
87(** val universe_inv_rect_Type4 :
88    String.string -> universe -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
89let universe_inv_rect_Type4 x1 hterm h1 =
90  let hcut = universe_rect_Type4 x1 h1 hterm in hcut __
91
92(** val universe_inv_rect_Type3 :
93    String.string -> universe -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
94let universe_inv_rect_Type3 x1 hterm h1 =
95  let hcut = universe_rect_Type3 x1 h1 hterm in hcut __
96
97(** val universe_inv_rect_Type2 :
98    String.string -> universe -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
99let universe_inv_rect_Type2 x1 hterm h1 =
100  let hcut = universe_rect_Type2 x1 h1 hterm in hcut __
101
102(** val universe_inv_rect_Type1 :
103    String.string -> universe -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
104let universe_inv_rect_Type1 x1 hterm h1 =
105  let hcut = universe_rect_Type1 x1 h1 hterm in hcut __
106
107(** val universe_inv_rect_Type0 :
108    String.string -> universe -> (Positive.pos -> __ -> 'a1) -> 'a1 **)
109let universe_inv_rect_Type0 x1 hterm h1 =
110  let hcut = universe_rect_Type0 x1 h1 hterm in hcut __
111
112(** val universe_discr : String.string -> universe -> universe -> __ **)
113let universe_discr a1 x y =
114  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
115
116(** val universe_jmdiscr : String.string -> universe -> universe -> __ **)
117let universe_jmdiscr a1 x y =
118  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
119
120(** val new_universe : String.string -> universe **)
121let new_universe tag =
122  Positive.One
123
124(** val fresh :
125    String.string -> universe -> (PreIdentifiers.identifier, universe)
126    Types.prod **)
127let rec fresh tag u =
128  let id = next_identifier tag u in
129  { Types.fst = id; Types.snd = (Positive.succ id) }
130
131type fresh_for_univ = __
132
133type env_fresh_for_univ = __
134
135(** val eq_identifier :
136    String.string -> PreIdentifiers.identifier -> PreIdentifiers.identifier
137    -> Bool.bool **)
138let eq_identifier t l r =
139  let l' = l in let r' = r in Positive.eqb0 l' r'
140
141(** val eq_identifier_elim :
142    String.string -> PreIdentifiers.identifier -> PreIdentifiers.identifier
143    -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
144let eq_identifier_elim t clearme =
145  let x = clearme in
146  (fun clearme0 ->
147  let y = clearme0 in
148  (fun t0 f -> Positive.eqb_elim x y (fun _ -> t0 __) (fun _ -> f __)))
149
150open Deqsets
151
152(** val deq_identifier : String.string -> Deqsets.deqSet **)
153let deq_identifier tag =
154  Obj.magic (eq_identifier tag)
155
156(** val word_of_identifier :
157    String.string -> PreIdentifiers.identifier -> Positive.pos **)
158let word_of_identifier t l =
159  let l' = l in l'
160
161(** val identifier_eq :
162    String.string -> PreIdentifiers.identifier -> PreIdentifiers.identifier
163    -> (__, __) Types.sum **)
164let identifier_eq tag clearme =
165  let x = clearme in
166  (fun clearme0 ->
167  let y = clearme0 in
168  (match Positive.eqb0 x y with
169   | Bool.True -> (fun _ -> Types.Inl __)
170   | Bool.False -> (fun _ -> Types.Inr __)) __)
171
172(** val identifier_of_nat :
173    String.string -> Nat.nat -> PreIdentifiers.identifier **)
174let identifier_of_nat tag n =
175  Positive.succ_pos_of_nat n
176
177type distinct_env = __
178
179(** val duplicateVariable : String.string **)
180let duplicateVariable = "duplicate variable"
181  (*failwith "AXIOM TO BE REALIZED"*)
182
183(** val check_member_env :
184    String.string -> PreIdentifiers.identifier -> (PreIdentifiers.identifier,
185    'a1) Types.prod List.list -> __ Errors.res **)
186let rec check_member_env tag id = function
187| List.Nil -> Errors.OK __
188| List.Cons (hd0, tl) ->
189  (match identifier_eq tag id hd0.Types.fst with
190   | Types.Inl _ ->
191     Errors.Error (List.Cons ((Errors.MSG duplicateVariable), (List.Cons
192       ((Errors.CTX (tag, id)), List.Nil))))
193   | Types.Inr _ ->
194     Obj.magic
195       (Monad.m_bind0 (Monad.max_def Errors.res0)
196         (Obj.magic (check_member_env tag id tl)) (fun _ ->
197         Obj.magic (Errors.OK __))))
198
199(** val check_distinct_env :
200    String.string -> (PreIdentifiers.identifier, 'a1) Types.prod List.list ->
201    __ Errors.res **)
202let rec check_distinct_env tag = function
203| List.Nil -> Errors.OK __
204| List.Cons (hd0, tl) ->
205  Obj.magic
206    (Monad.m_bind0 (Monad.max_def Errors.res0)
207      (Obj.magic (check_member_env tag hd0.Types.fst tl)) (fun _ ->
208      Monad.m_bind0 (Monad.max_def Errors.res0)
209        (Obj.magic (check_distinct_env tag tl)) (fun _ ->
210        Obj.magic (Errors.OK __))))
211
212open PositiveMap
213
214type 'a identifier_map =
215  'a PositiveMap.positive_map
216  (* singleton inductive, whose constructor was an_id_map *)
217
218(** val identifier_map_rect_Type4 :
219    String.string -> ('a1 PositiveMap.positive_map -> 'a2) -> 'a1
220    identifier_map -> 'a2 **)
221let rec identifier_map_rect_Type4 tag h_an_id_map x_2280 =
222  let x_2281 = x_2280 in h_an_id_map x_2281
223
224(** val identifier_map_rect_Type5 :
225    String.string -> ('a1 PositiveMap.positive_map -> 'a2) -> 'a1
226    identifier_map -> 'a2 **)
227let rec identifier_map_rect_Type5 tag h_an_id_map x_2283 =
228  let x_2284 = x_2283 in h_an_id_map x_2284
229
230(** val identifier_map_rect_Type3 :
231    String.string -> ('a1 PositiveMap.positive_map -> 'a2) -> 'a1
232    identifier_map -> 'a2 **)
233let rec identifier_map_rect_Type3 tag h_an_id_map x_2286 =
234  let x_2287 = x_2286 in h_an_id_map x_2287
235
236(** val identifier_map_rect_Type2 :
237    String.string -> ('a1 PositiveMap.positive_map -> 'a2) -> 'a1
238    identifier_map -> 'a2 **)
239let rec identifier_map_rect_Type2 tag h_an_id_map x_2289 =
240  let x_2290 = x_2289 in h_an_id_map x_2290
241
242(** val identifier_map_rect_Type1 :
243    String.string -> ('a1 PositiveMap.positive_map -> 'a2) -> 'a1
244    identifier_map -> 'a2 **)
245let rec identifier_map_rect_Type1 tag h_an_id_map x_2292 =
246  let x_2293 = x_2292 in h_an_id_map x_2293
247
248(** val identifier_map_rect_Type0 :
249    String.string -> ('a1 PositiveMap.positive_map -> 'a2) -> 'a1
250    identifier_map -> 'a2 **)
251let rec identifier_map_rect_Type0 tag h_an_id_map x_2295 =
252  let x_2296 = x_2295 in h_an_id_map x_2296
253
254(** val identifier_map_inv_rect_Type4 :
255    String.string -> 'a1 identifier_map -> ('a1 PositiveMap.positive_map ->
256    __ -> 'a2) -> 'a2 **)
257let identifier_map_inv_rect_Type4 x1 hterm h1 =
258  let hcut = identifier_map_rect_Type4 x1 h1 hterm in hcut __
259
260(** val identifier_map_inv_rect_Type3 :
261    String.string -> 'a1 identifier_map -> ('a1 PositiveMap.positive_map ->
262    __ -> 'a2) -> 'a2 **)
263let identifier_map_inv_rect_Type3 x1 hterm h1 =
264  let hcut = identifier_map_rect_Type3 x1 h1 hterm in hcut __
265
266(** val identifier_map_inv_rect_Type2 :
267    String.string -> 'a1 identifier_map -> ('a1 PositiveMap.positive_map ->
268    __ -> 'a2) -> 'a2 **)
269let identifier_map_inv_rect_Type2 x1 hterm h1 =
270  let hcut = identifier_map_rect_Type2 x1 h1 hterm in hcut __
271
272(** val identifier_map_inv_rect_Type1 :
273    String.string -> 'a1 identifier_map -> ('a1 PositiveMap.positive_map ->
274    __ -> 'a2) -> 'a2 **)
275let identifier_map_inv_rect_Type1 x1 hterm h1 =
276  let hcut = identifier_map_rect_Type1 x1 h1 hterm in hcut __
277
278(** val identifier_map_inv_rect_Type0 :
279    String.string -> 'a1 identifier_map -> ('a1 PositiveMap.positive_map ->
280    __ -> 'a2) -> 'a2 **)
281let identifier_map_inv_rect_Type0 x1 hterm h1 =
282  let hcut = identifier_map_rect_Type0 x1 h1 hterm in hcut __
283
284(** val identifier_map_discr :
285    String.string -> 'a1 identifier_map -> 'a1 identifier_map -> __ **)
286let identifier_map_discr a1 x y =
287  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
288
289(** val identifier_map_jmdiscr :
290    String.string -> 'a1 identifier_map -> 'a1 identifier_map -> __ **)
291let identifier_map_jmdiscr a1 x y =
292  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
293
294(** val empty_map : String.string -> 'a1 identifier_map **)
295let empty_map tag =
296  PositiveMap.Pm_leaf
297
298(** val lookup0 :
299    String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1
300    Types.option **)
301let rec lookup0 tag m l =
302  PositiveMap.lookup_opt (let l' = l in l') (let m' = m in m')
303
304(** val lookup_def :
305    String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1
306    -> 'a1 **)
307let lookup_def tag m l d =
308  match lookup0 tag m l with
309  | Types.None -> d
310  | Types.Some x -> x
311
312(** val member0 :
313    String.string -> 'a1 identifier_map -> PreIdentifiers.identifier ->
314    Bool.bool **)
315let member0 tag m l =
316  match lookup0 tag m l with
317  | Types.None -> Bool.False
318  | Types.Some x -> Bool.True
319
320(** val lookup_safe :
321    String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1 **)
322let lookup_safe tag m i =
323  (match lookup0 tag m i with
324   | Types.None -> (fun _ -> assert false (* absurd case *))
325   | Types.Some x -> (fun _ -> x)) __
326
327(** val add :
328    String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1
329    -> 'a1 identifier_map **)
330let rec add tag m l a =
331  PositiveMap.insert (let l' = l in l') a (let m' = m in m')
332
333(** val elements :
334    String.string -> 'a1 identifier_map -> (PreIdentifiers.identifier, 'a1)
335    Types.prod List.list **)
336let elements tag m =
337  PositiveMap.fold0 (fun l a el -> List.Cons ({ Types.fst = l; Types.snd =
338    a }, el)) (let m' = m in m') List.Nil
339
340(** val idmap_all :
341    String.string -> 'a1 identifier_map -> (PreIdentifiers.identifier -> 'a1
342    -> __ -> Bool.bool) -> Bool.bool **)
343let idmap_all tag m f =
344  PositiveMap.pm_all (let m' = m in m') (fun p a _ -> f p a __)
345
346(** val missingId : String.string **)
347let missingId = "missing id"
348  (*failwith "AXIOM TO BE REALIZED"*)
349
350(** val update0 :
351    String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1
352    -> 'a1 identifier_map Errors.res **)
353let update0 tag m l a =
354  match PositiveMap.update (let l' = l in l') a (let m' = m in m') with
355  | Types.None ->
356    Errors.Error (List.Cons ((Errors.MSG missingId), (List.Cons ((Errors.CTX
357      (tag, l)), List.Nil))))
358  | Types.Some m' -> Errors.OK m'
359
360(** val remove :
361    String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1
362    identifier_map **)
363let remove tag m id =
364  PositiveMap.pm_set (let p = id in p) Types.None (let m0 = m in m0)
365
366(** val foldi0 :
367    String.string -> (PreIdentifiers.identifier -> 'a1 -> 'a2 -> 'a2) -> 'a1
368    identifier_map -> 'a2 -> 'a2 **)
369let foldi0 tag f m b =
370  let m' = m in PositiveMap.fold0 (fun bv -> f bv) m' b
371
372(** val fold_inf :
373    String.string -> 'a1 identifier_map -> (PreIdentifiers.identifier -> 'a1
374    -> __ -> 'a2 -> 'a2) -> 'a2 -> 'a2 **)
375let fold_inf tag m =
376  let m' = m in
377  (fun f b -> PositiveMap.pm_fold_inf m' (fun bv a _ -> f bv a __) b)
378
379(** val find0 :
380    String.string -> 'a1 identifier_map -> (PreIdentifiers.identifier -> 'a1
381    -> Bool.bool) -> (PreIdentifiers.identifier, 'a1) Types.prod Types.option **)
382let find0 tag m p =
383  let m' = m in
384  Types.option_map (fun x -> { Types.fst = x.Types.fst; Types.snd =
385    x.Types.snd }) (PositiveMap.pm_find m' (fun id -> p id))
386
387(** val lookup_present :
388    String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1 **)
389let lookup_present tag m id =
390  (match lookup0 tag m id with
391   | Types.None -> (fun _ -> assert false (* absurd case *))
392   | Types.Some a -> (fun _ -> a)) __
393
394(** val update_present :
395    String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> 'a1
396    -> 'a1 identifier_map **)
397let update_present tag m l a =
398  let l' = let l' = l in l' in
399  let m' = let m' = m in m' in
400  let u' = PositiveMap.update l' a m' in
401  (match u' with
402   | Types.None -> (fun _ -> assert false (* absurd case *))
403   | Types.Some m'0 -> (fun _ -> m'0)) __
404
405type fresh_for_map = __
406
407type identifier_set = Types.unit0 identifier_map
408
409(** val empty_set : String.string -> identifier_set **)
410let empty_set tag =
411  empty_map tag
412
413(** val add_set :
414    String.string -> identifier_set -> PreIdentifiers.identifier ->
415    identifier_set **)
416let add_set tag s i =
417  add tag s i Types.It
418
419(** val singleton_set :
420    String.string -> PreIdentifiers.identifier -> identifier_set **)
421let singleton_set tag i =
422  add_set tag (empty_set tag) i
423
424(** val union_set :
425    String.string -> 'a1 identifier_map -> 'a2 identifier_map ->
426    identifier_set **)
427let rec union_set tag s s' =
428  PositiveMap.merge (fun o o' ->
429    match o with
430    | Types.None ->
431      Obj.magic
432        (Monad.m_bind0 (Monad.max_def Option.option0) (Obj.magic o')
433          (fun x -> Monad.m_return0 (Monad.max_def Option.option0) Types.It))
434    | Types.Some x -> Types.Some Types.It) (let s0 = s in s0)
435    (let s1 = s' in s1)
436
437(** val minus_set :
438    String.string -> 'a1 identifier_map -> 'a2 identifier_map -> 'a1
439    identifier_map **)
440let rec minus_set tag s s' =
441  PositiveMap.merge (fun o o' ->
442    match o' with
443    | Types.None -> o
444    | Types.Some x -> Types.None) (let s0 = s in s0) (let s1 = s' in s1)
445
446(** val identifierSet : String.string -> Setoids.setoid **)
447let identifierSet tag =
448  Setoids.Mk_Setoid
449
450(** val id_map_size : String.string -> 'a1 identifier_map -> Nat.nat **)
451let id_map_size tag s =
452  let p = s in PositiveMap.domain_size p
453
454open Proper
455
456(** val set_from_list :
457    String.string -> PreIdentifiers.identifier List.list -> Types.unit0
458    identifier_map **)
459let set_from_list tag =
460  Util.foldl (add_set tag) (empty_set tag)
461
462(** val choose :
463    String.string -> 'a1 identifier_map -> ((PreIdentifiers.identifier, 'a1)
464    Types.prod, 'a1 identifier_map) Types.prod Types.option **)
465let choose tag m =
466  match PositiveMap.pm_choose (let m' = m in m') with
467  | Types.None -> Types.None
468  | Types.Some x ->
469    Types.Some { Types.fst = { Types.fst = x.Types.fst.Types.fst; Types.snd =
470      x.Types.fst.Types.snd }; Types.snd = x.Types.snd }
471
472(** val try_remove :
473    String.string -> 'a1 identifier_map -> PreIdentifiers.identifier -> ('a1,
474    'a1 identifier_map) Types.prod Types.option **)
475let try_remove tag m id =
476  match PositiveMap.pm_try_remove (let id' = id in id') (let m' = m in m') with
477  | Types.None -> Types.None
478  | Types.Some x ->
479    Types.Some { Types.fst = x.Types.fst; Types.snd = x.Types.snd }
480
481(** val id_set_of_map :
482    String.string -> 'a1 identifier_map -> identifier_set **)
483let id_set_of_map tag m =
484  PositiveMap.map0 (fun x -> Types.It) (let m' = m in m')
485
486(** val set_of_list :
487    String.string -> PreIdentifiers.identifier List.list -> identifier_set **)
488let set_of_list tag l =
489  Util.foldl (fun s id -> add_set tag s id) (empty_set tag) l
490
491(** val domain_of_map :
492    String.string -> 'a1 identifier_map -> identifier_set **)
493let domain_of_map tag m =
494  PositiveMap.domain_of_pm (let m0 = m in m0)
495
Note: See TracBrowser for help on using the repository browser.