source: extracted/identifiers.ml @ 2729

Last change on this file since 2729 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
RevLine 
[2601]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
[2649]35open List
36
[2601]37open Lists
38
39open Extralib
40
[2649]41open ErrorMessages
42
[2601]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 :
[2649]52    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
[2717]53let rec universe_rect_Type4 tag h_mk_universe x_3057 =
54  let next_identifier = x_3057 in h_mk_universe next_identifier
[2601]55
56(** val universe_rect_Type5 :
[2649]57    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
[2717]58let rec universe_rect_Type5 tag h_mk_universe x_3059 =
59  let next_identifier = x_3059 in h_mk_universe next_identifier
[2601]60
61(** val universe_rect_Type3 :
[2649]62    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
[2717]63let rec universe_rect_Type3 tag h_mk_universe x_3061 =
64  let next_identifier = x_3061 in h_mk_universe next_identifier
[2601]65
66(** val universe_rect_Type2 :
[2649]67    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
[2717]68let rec universe_rect_Type2 tag h_mk_universe x_3063 =
69  let next_identifier = x_3063 in h_mk_universe next_identifier
[2601]70
71(** val universe_rect_Type1 :
[2649]72    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
[2717]73let rec universe_rect_Type1 tag h_mk_universe x_3065 =
74  let next_identifier = x_3065 in h_mk_universe next_identifier
[2601]75
76(** val universe_rect_Type0 :
[2649]77    PreIdentifiers.identifierTag -> (Positive.pos -> 'a1) -> universe -> 'a1 **)
[2717]78let rec universe_rect_Type0 tag h_mk_universe x_3067 =
79  let next_identifier = x_3067 in h_mk_universe next_identifier
[2601]80
[2649]81(** val next_identifier :
82    PreIdentifiers.identifierTag -> universe -> Positive.pos **)
[2601]83let rec next_identifier tag xxx =
84  let yyy = xxx in yyy
85
86(** val universe_inv_rect_Type4 :
[2649]87    PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1)
88    -> 'a1 **)
[2601]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 :
[2649]93    PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1)
94    -> 'a1 **)
[2601]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 :
[2649]99    PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1)
100    -> 'a1 **)
[2601]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 :
[2649]105    PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1)
106    -> 'a1 **)
[2601]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 :
[2649]111    PreIdentifiers.identifierTag -> universe -> (Positive.pos -> __ -> 'a1)
112    -> 'a1 **)
[2601]113let universe_inv_rect_Type0 x1 hterm h1 =
114  let hcut = universe_rect_Type0 x1 h1 hterm in hcut __
115
[2649]116(** val universe_discr :
117    PreIdentifiers.identifierTag -> universe -> universe -> __ **)
[2601]118let universe_discr a1 x y =
119  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
120
[2649]121(** val universe_jmdiscr :
122    PreIdentifiers.identifierTag -> universe -> universe -> __ **)
[2601]123let universe_jmdiscr a1 x y =
124  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
125
[2649]126(** val new_universe : PreIdentifiers.identifierTag -> universe **)
[2601]127let new_universe tag =
128  Positive.One
129
130(** val fresh :
[2649]131    PreIdentifiers.identifierTag -> universe -> (PreIdentifiers.identifier,
132    universe) Types.prod **)
[2601]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 :
[2649]142    PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
143    PreIdentifiers.identifier -> Bool.bool **)
[2601]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 :
[2649]148    PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
149    PreIdentifiers.identifier -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
[2601]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
[2649]158(** val deq_identifier : PreIdentifiers.identifierTag -> Deqsets.deqSet **)
[2601]159let deq_identifier tag =
160  Obj.magic (eq_identifier tag)
161
162(** val word_of_identifier :
[2649]163    PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> Positive.pos **)
[2601]164let word_of_identifier t l =
165  let l' = l in l'
166
167(** val identifier_eq :
[2649]168    PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
169    PreIdentifiers.identifier -> (__, __) Types.sum **)
[2601]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 :
[2649]179    PreIdentifiers.identifierTag -> Nat.nat -> PreIdentifiers.identifier **)
[2601]180let identifier_of_nat tag n =
181  Positive.succ_pos_of_nat n
182
183type distinct_env = __
184
185(** val check_member_env :
[2649]186    PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
187    (PreIdentifiers.identifier, 'a1) Types.prod List.list -> __ Errors.res **)
[2601]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 _ ->
[2649]193     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.DuplicateVariable),
194       (List.Cons ((Errors.CTX (tag, id)), List.Nil))))
[2601]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 :
[2649]202    PreIdentifiers.identifierTag -> (PreIdentifiers.identifier, 'a1)
203    Types.prod List.list -> __ Errors.res **)
[2601]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 :
[2649]221    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
222    'a1 identifier_map -> 'a2 **)
[2717]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
[2601]225
226(** val identifier_map_rect_Type5 :
[2649]227    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
228    'a1 identifier_map -> 'a2 **)
[2717]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
[2601]231
232(** val identifier_map_rect_Type3 :
[2649]233    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
234    'a1 identifier_map -> 'a2 **)
[2717]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
[2601]237
238(** val identifier_map_rect_Type2 :
[2649]239    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
240    'a1 identifier_map -> 'a2 **)
[2717]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
[2601]243
244(** val identifier_map_rect_Type1 :
[2649]245    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
246    'a1 identifier_map -> 'a2 **)
[2717]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
[2601]249
250(** val identifier_map_rect_Type0 :
[2649]251    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
252    'a1 identifier_map -> 'a2 **)
[2717]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
[2601]255
256(** val identifier_map_inv_rect_Type4 :
[2649]257    PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
258    PositiveMap.positive_map -> __ -> 'a2) -> 'a2 **)
[2601]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 :
[2649]263    PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
264    PositiveMap.positive_map -> __ -> 'a2) -> 'a2 **)
[2601]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 :
[2649]269    PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
270    PositiveMap.positive_map -> __ -> 'a2) -> 'a2 **)
[2601]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 :
[2649]275    PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
276    PositiveMap.positive_map -> __ -> 'a2) -> 'a2 **)
[2601]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 :
[2649]281    PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
282    PositiveMap.positive_map -> __ -> 'a2) -> 'a2 **)
[2601]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 :
[2649]287    PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a1 identifier_map
288    -> __ **)
[2601]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 :
[2649]293    PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a1 identifier_map
294    -> __ **)
[2601]295let identifier_map_jmdiscr a1 x y =
296  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
297
[2649]298(** val empty_map : PreIdentifiers.identifierTag -> 'a1 identifier_map **)
[2601]299let empty_map tag =
300  PositiveMap.Pm_leaf
301
302(** val lookup0 :
[2649]303    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
304    PreIdentifiers.identifier -> 'a1 Types.option **)
[2601]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 :
[2649]309    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
310    PreIdentifiers.identifier -> 'a1 -> 'a1 **)
[2601]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 :
[2649]317    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
318    PreIdentifiers.identifier -> Bool.bool **)
[2601]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 :
[2649]325    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
326    PreIdentifiers.identifier -> 'a1 **)
[2601]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 :
[2649]333    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
334    PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map **)
[2601]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 :
[2649]339    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
340    (PreIdentifiers.identifier, 'a1) Types.prod List.list **)
[2601]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 :
[2649]346    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
347    (PreIdentifiers.identifier -> 'a1 -> __ -> Bool.bool) -> Bool.bool **)
[2601]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 :
[2649]352    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
353    PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map Errors.res **)
[2601]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 ->
[2649]357    Errors.Error (List.Cons ((Errors.MSG ErrorMessages.MissingId), (List.Cons
358      ((Errors.CTX (tag, l)), List.Nil))))
[2601]359  | Types.Some m' -> Errors.OK m'
360
361(** val remove :
[2649]362    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
363    PreIdentifiers.identifier -> 'a1 identifier_map **)
[2601]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 :
[2649]368    PreIdentifiers.identifierTag -> (PreIdentifiers.identifier -> 'a1 -> 'a2
369    -> 'a2) -> 'a1 identifier_map -> 'a2 -> 'a2 **)
[2601]370let foldi0 tag f m b =
371  let m' = m in PositiveMap.fold0 (fun bv -> f bv) m' b
372
373(** val fold_inf :
[2649]374    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
375    (PreIdentifiers.identifier -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a2 -> 'a2 **)
[2601]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 :
[2649]381    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
382    (PreIdentifiers.identifier -> 'a1 -> Bool.bool) ->
383    (PreIdentifiers.identifier, 'a1) Types.prod Types.option **)
[2601]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 :
[2649]390    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
391    PreIdentifiers.identifier -> 'a1 **)
[2601]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 :
[2649]398    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
399    PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map **)
[2601]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
[2649]412(** val empty_set : PreIdentifiers.identifierTag -> identifier_set **)
[2601]413let empty_set tag =
414  empty_map tag
415
416(** val add_set :
[2649]417    PreIdentifiers.identifierTag -> identifier_set ->
418    PreIdentifiers.identifier -> identifier_set **)
[2601]419let add_set tag s i =
420  add tag s i Types.It
421
422(** val singleton_set :
[2649]423    PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
424    identifier_set **)
[2601]425let singleton_set tag i =
426  add_set tag (empty_set tag) i
427
428(** val union_set :
[2649]429    PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a2 identifier_map
430    -> identifier_set **)
[2601]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 :
[2649]442    PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a2 identifier_map
443    -> 'a1 identifier_map **)
[2601]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
[2649]450(** val identifierSet : PreIdentifiers.identifierTag -> Setoids.setoid **)
[2601]451let identifierSet tag =
452  Setoids.Mk_Setoid
453
[2649]454(** val id_map_size :
455    PreIdentifiers.identifierTag -> 'a1 identifier_map -> Nat.nat **)
[2601]456let id_map_size tag s =
457  let p = s in PositiveMap.domain_size p
458
459open Proper
460
461(** val set_from_list :
[2649]462    PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
463    Types.unit0 identifier_map **)
[2601]464let set_from_list tag =
465  Util.foldl (add_set tag) (empty_set tag)
466
467(** val choose :
[2649]468    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
469    ((PreIdentifiers.identifier, 'a1) Types.prod, 'a1 identifier_map)
470    Types.prod Types.option **)
[2601]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 :
[2649]479    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
480    PreIdentifiers.identifier -> ('a1, 'a1 identifier_map) Types.prod
481    Types.option **)
[2601]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 :
[2649]489    PreIdentifiers.identifierTag -> 'a1 identifier_map -> identifier_set **)
[2601]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 :
[2649]494    PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
495    identifier_set **)
[2601]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 :
[2649]500    PreIdentifiers.identifierTag -> 'a1 identifier_map -> identifier_set **)
[2601]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.