source: extracted/identifiers.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: 17.9 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_3083 =
54  let next_identifier = x_3083 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_3085 =
59  let next_identifier = x_3085 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_3087 =
64  let next_identifier = x_3087 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_3089 =
69  let next_identifier = x_3089 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_3091 =
74  let next_identifier = x_3091 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_3093 =
79  let next_identifier = x_3093 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 'x 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 'x 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_3255 =
224  let x_3256 = x_3255 in h_an_id_map x_3256
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_3258 =
230  let x_3259 = x_3258 in h_an_id_map x_3259
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_3261 =
236  let x_3262 = x_3261 in h_an_id_map x_3262
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_3264 =
242  let x_3265 = x_3264 in h_an_id_map x_3265
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_3267 =
248  let x_3268 = x_3267 in h_an_id_map x_3268
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_3270 =
254  let x_3271 = x_3270 in h_an_id_map x_3271
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 'x 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 dpi1__o__id_set_from_list__o__inject :
468    PreIdentifiers.identifierTag -> (PreIdentifiers.identifier List.list,
469    'a1) Types.dPair -> Types.unit0 identifier_map Types.sig0 **)
470let dpi1__o__id_set_from_list__o__inject x0 x3 =
471  set_from_list x0 x3.Types.dpi1
472
473(** val eject__o__id_set_from_list__o__inject :
474    PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list
475    Types.sig0 -> Types.unit0 identifier_map Types.sig0 **)
476let eject__o__id_set_from_list__o__inject x0 x3 =
477  set_from_list x0 (Types.pi1 x3)
478
479(** val id_set_from_list__o__inject :
480    PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
481    Types.unit0 identifier_map Types.sig0 **)
482let id_set_from_list__o__inject x0 x2 =
483  set_from_list x0 x2
484
485(** val dpi1__o__id_set_from_list :
486    PreIdentifiers.identifierTag -> (PreIdentifiers.identifier List.list,
487    'a1) Types.dPair -> Types.unit0 identifier_map **)
488let dpi1__o__id_set_from_list x0 x2 =
489  set_from_list x0 x2.Types.dpi1
490
491(** val eject__o__id_set_from_list :
492    PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list
493    Types.sig0 -> Types.unit0 identifier_map **)
494let eject__o__id_set_from_list x0 x2 =
495  set_from_list x0 (Types.pi1 x2)
496
497(** val choose :
498    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
499    ((PreIdentifiers.identifier, 'a1) Types.prod, 'a1 identifier_map)
500    Types.prod Types.option **)
501let choose tag m =
502  match PositiveMap.pm_choose (let m' = m in m') with
503  | Types.None -> Types.None
504  | Types.Some x ->
505    Types.Some { Types.fst = { Types.fst = x.Types.fst.Types.fst; Types.snd =
506      x.Types.fst.Types.snd }; Types.snd = x.Types.snd }
507
508(** val try_remove :
509    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
510    PreIdentifiers.identifier -> ('a1, 'a1 identifier_map) Types.prod
511    Types.option **)
512let try_remove tag m id =
513  match PositiveMap.pm_try_remove (let id' = id in id') (let m' = m in m') with
514  | Types.None -> Types.None
515  | Types.Some x ->
516    Types.Some { Types.fst = x.Types.fst; Types.snd = x.Types.snd }
517
518(** val id_set_of_map :
519    PreIdentifiers.identifierTag -> 'a1 identifier_map -> identifier_set **)
520let id_set_of_map tag m =
521  PositiveMap.map0 (fun x -> Types.It) (let m' = m in m')
522
523(** val set_of_list :
524    PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
525    identifier_set **)
526let set_of_list tag l =
527  Util.foldl (fun s id -> add_set tag s id) (empty_set tag) l
528
529(** val domain_of_map :
530    PreIdentifiers.identifierTag -> 'a1 identifier_map -> identifier_set **)
531let domain_of_map tag m =
532  PositiveMap.domain_of_pm (let m0 = m in m0)
533
Note: See TracBrowser for help on using the repository browser.