source: extracted/identifiers.ml @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

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