source: extracted/identifiers.ml @ 2827

Last change on this file since 2827 was 2827, checked in by sacerdot, 8 years ago

Everything extracted again.

File size: 17.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_3226 =
54  let next_identifier = x_3226 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_3228 =
59  let next_identifier = x_3228 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_3230 =
64  let next_identifier = x_3230 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_3232 =
69  let next_identifier = x_3232 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_3234 =
74  let next_identifier = x_3234 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_3236 =
79  let next_identifier = x_3236 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
137(** val eq_identifier :
138    PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
139    PreIdentifiers.identifier -> Bool.bool **)
140let eq_identifier t l r =
141  let l' = l in let r' = r in Positive.eqb l' r'
142
143(** val eq_identifier_elim :
144    PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
145    PreIdentifiers.identifier -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
146let eq_identifier_elim t clearme =
147  let x = clearme in
148  (fun clearme0 ->
149  let y = clearme0 in
150  (fun t0 f -> Positive.eqb_elim x y (fun _ -> t0 __) (fun _ -> f __)))
151
152open Deqsets
153
154(** val deq_identifier : PreIdentifiers.identifierTag -> Deqsets.deqSet **)
155let deq_identifier tag =
156  Obj.magic (eq_identifier tag)
157
158(** val word_of_identifier :
159    PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> Positive.pos **)
160let word_of_identifier t l =
161  let l' = l in l'
162
163(** val identifier_eq :
164    PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
165    PreIdentifiers.identifier -> (__, __) Types.sum **)
166let identifier_eq tag clearme =
167  let x = clearme in
168  (fun clearme0 ->
169  let y = clearme0 in
170  (match Positive.eqb x y with
171   | Bool.True -> (fun _ -> Types.Inl __)
172   | Bool.False -> (fun _ -> Types.Inr __)) __)
173
174(** val identifier_of_nat :
175    PreIdentifiers.identifierTag -> Nat.nat -> PreIdentifiers.identifier **)
176let identifier_of_nat tag n =
177  Positive.succ_pos_of_nat n
178
179(** val check_member_env :
180    PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
181    (PreIdentifiers.identifier, 'a1) Types.prod List.list -> __ Errors.res **)
182let rec check_member_env tag id = function
183| List.Nil -> Errors.OK __
184| List.Cons (hd, tl) ->
185  (match identifier_eq tag id hd.Types.fst with
186   | Types.Inl _ ->
187     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.DuplicateVariable),
188       (List.Cons ((Errors.CTX (tag, id)), List.Nil))))
189   | Types.Inr _ ->
190     Obj.magic
191       (Monad.m_bind0 (Monad.max_def Errors.res0)
192         (Obj.magic (check_member_env tag id tl)) (fun _ ->
193         Obj.magic (Errors.OK __))))
194
195(** val check_distinct_env :
196    PreIdentifiers.identifierTag -> (PreIdentifiers.identifier, 'a1)
197    Types.prod List.list -> __ Errors.res **)
198let rec check_distinct_env tag = function
199| List.Nil -> Errors.OK __
200| List.Cons (hd, tl) ->
201  Obj.magic
202    (Monad.m_bind0 (Monad.max_def Errors.res0)
203      (Obj.magic (check_member_env tag hd.Types.fst tl)) (fun _ ->
204      Monad.m_bind0 (Monad.max_def Errors.res0)
205        (Obj.magic (check_distinct_env tag tl)) (fun _ ->
206        Obj.magic (Errors.OK __))))
207
208open PositiveMap
209
210type 'a identifier_map =
211  'a PositiveMap.positive_map
212  (* singleton inductive, whose constructor was an_id_map *)
213
214(** val identifier_map_rect_Type4 :
215    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
216    'a1 identifier_map -> 'a2 **)
217let rec identifier_map_rect_Type4 tag h_an_id_map x_3398 =
218  let x_3399 = x_3398 in h_an_id_map x_3399
219
220(** val identifier_map_rect_Type5 :
221    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
222    'a1 identifier_map -> 'a2 **)
223let rec identifier_map_rect_Type5 tag h_an_id_map x_3401 =
224  let x_3402 = x_3401 in h_an_id_map x_3402
225
226(** val identifier_map_rect_Type3 :
227    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
228    'a1 identifier_map -> 'a2 **)
229let rec identifier_map_rect_Type3 tag h_an_id_map x_3404 =
230  let x_3405 = x_3404 in h_an_id_map x_3405
231
232(** val identifier_map_rect_Type2 :
233    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
234    'a1 identifier_map -> 'a2 **)
235let rec identifier_map_rect_Type2 tag h_an_id_map x_3407 =
236  let x_3408 = x_3407 in h_an_id_map x_3408
237
238(** val identifier_map_rect_Type1 :
239    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
240    'a1 identifier_map -> 'a2 **)
241let rec identifier_map_rect_Type1 tag h_an_id_map x_3410 =
242  let x_3411 = x_3410 in h_an_id_map x_3411
243
244(** val identifier_map_rect_Type0 :
245    PreIdentifiers.identifierTag -> ('a1 PositiveMap.positive_map -> 'a2) ->
246    'a1 identifier_map -> 'a2 **)
247let rec identifier_map_rect_Type0 tag h_an_id_map x_3413 =
248  let x_3414 = x_3413 in h_an_id_map x_3414
249
250(** val identifier_map_inv_rect_Type4 :
251    PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
252    PositiveMap.positive_map -> __ -> 'a2) -> 'a2 **)
253let identifier_map_inv_rect_Type4 x1 hterm h1 =
254  let hcut = identifier_map_rect_Type4 x1 h1 hterm in hcut __
255
256(** val identifier_map_inv_rect_Type3 :
257    PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
258    PositiveMap.positive_map -> __ -> 'a2) -> 'a2 **)
259let identifier_map_inv_rect_Type3 x1 hterm h1 =
260  let hcut = identifier_map_rect_Type3 x1 h1 hterm in hcut __
261
262(** val identifier_map_inv_rect_Type2 :
263    PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
264    PositiveMap.positive_map -> __ -> 'a2) -> 'a2 **)
265let identifier_map_inv_rect_Type2 x1 hterm h1 =
266  let hcut = identifier_map_rect_Type2 x1 h1 hterm in hcut __
267
268(** val identifier_map_inv_rect_Type1 :
269    PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
270    PositiveMap.positive_map -> __ -> 'a2) -> 'a2 **)
271let identifier_map_inv_rect_Type1 x1 hterm h1 =
272  let hcut = identifier_map_rect_Type1 x1 h1 hterm in hcut __
273
274(** val identifier_map_inv_rect_Type0 :
275    PreIdentifiers.identifierTag -> 'a1 identifier_map -> ('a1
276    PositiveMap.positive_map -> __ -> 'a2) -> 'a2 **)
277let identifier_map_inv_rect_Type0 x1 hterm h1 =
278  let hcut = identifier_map_rect_Type0 x1 h1 hterm in hcut __
279
280(** val identifier_map_discr :
281    PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a1 identifier_map
282    -> __ **)
283let identifier_map_discr a1 x y =
284  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
285
286(** val identifier_map_jmdiscr :
287    PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a1 identifier_map
288    -> __ **)
289let identifier_map_jmdiscr a1 x y =
290  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
291
292(** val empty_map : PreIdentifiers.identifierTag -> 'a1 identifier_map **)
293let empty_map tag =
294  PositiveMap.Pm_leaf
295
296(** val lookup :
297    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
298    PreIdentifiers.identifier -> 'a1 Types.option **)
299let rec lookup tag m l =
300  PositiveMap.lookup_opt (let l' = l in l') (let m' = m in m')
301
302(** val lookup_def :
303    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
304    PreIdentifiers.identifier -> 'a1 -> 'a1 **)
305let lookup_def tag m l d =
306  match lookup tag m l with
307  | Types.None -> d
308  | Types.Some x -> x
309
310(** val member :
311    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
312    PreIdentifiers.identifier -> Bool.bool **)
313let member tag m l =
314  match lookup tag m l with
315  | Types.None -> Bool.False
316  | Types.Some x -> Bool.True
317
318(** val lookup_safe :
319    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
320    PreIdentifiers.identifier -> 'a1 **)
321let lookup_safe tag m i =
322  (match lookup tag m i with
323   | Types.None -> (fun _ -> assert false (* absurd case *))
324   | Types.Some x -> (fun _ -> x)) __
325
326(** val add :
327    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
328    PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map **)
329let rec add tag m l a =
330  PositiveMap.insert (let l' = l in l') a (let m' = m in m')
331
332(** val elements :
333    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
334    (PreIdentifiers.identifier, 'a1) Types.prod List.list **)
335let elements tag m =
336  PositiveMap.fold (fun l a el -> List.Cons ({ Types.fst = l; Types.snd =
337    a }, el)) (let m' = m in m') List.Nil
338
339(** val idmap_all :
340    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
341    (PreIdentifiers.identifier -> 'a1 -> __ -> Bool.bool) -> Bool.bool **)
342let idmap_all tag m f =
343  PositiveMap.pm_all (let m' = m in m') (fun p a _ -> f p a __)
344
345(** val update :
346    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
347    PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map Errors.res **)
348let update tag m l a =
349  match PositiveMap.update (let l' = l in l') a (let m' = m in m') with
350  | Types.None ->
351    Errors.Error (List.Cons ((Errors.MSG ErrorMessages.MissingId), (List.Cons
352      ((Errors.CTX (tag, l)), List.Nil))))
353  | Types.Some m' -> Errors.OK m'
354
355(** val remove :
356    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
357    PreIdentifiers.identifier -> 'a1 identifier_map **)
358let remove tag m id =
359  PositiveMap.pm_set (let p = id in p) Types.None (let m0 = m in m0)
360
361(** val foldi :
362    PreIdentifiers.identifierTag -> (PreIdentifiers.identifier -> 'a1 -> 'a2
363    -> 'a2) -> 'a1 identifier_map -> 'a2 -> 'a2 **)
364let foldi tag f m b =
365  let m' = m in PositiveMap.fold (fun bv -> f bv) m' b
366
367(** val fold_inf :
368    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
369    (PreIdentifiers.identifier -> 'a1 -> __ -> 'a2 -> 'a2) -> 'a2 -> 'a2 **)
370let fold_inf tag m =
371  let m' = m in
372  (fun f b -> PositiveMap.pm_fold_inf m' (fun bv a _ -> f bv a __) b)
373
374(** val find :
375    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
376    (PreIdentifiers.identifier -> 'a1 -> Bool.bool) ->
377    (PreIdentifiers.identifier, 'a1) Types.prod Types.option **)
378let find tag m p =
379  let m' = m in
380  Types.option_map (fun x -> { Types.fst = x.Types.fst; Types.snd =
381    x.Types.snd }) (PositiveMap.pm_find m' (fun id -> p id))
382
383(** val lookup_present :
384    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
385    PreIdentifiers.identifier -> 'a1 **)
386let lookup_present tag m id =
387  (match lookup tag m id with
388   | Types.None -> (fun _ -> assert false (* absurd case *))
389   | Types.Some a -> (fun _ -> a)) __
390
391(** val update_present :
392    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
393    PreIdentifiers.identifier -> 'a1 -> 'a1 identifier_map **)
394let update_present tag m l a =
395  let l' = let l' = l in l' in
396  let m' = let m' = m in m' in
397  let u' = PositiveMap.update l' a m' in
398  (match u' with
399   | Types.None -> (fun _ -> assert false (* absurd case *))
400   | Types.Some m'0 -> (fun _ -> m'0)) __
401
402type identifier_set = Types.unit0 identifier_map
403
404(** val empty_set : PreIdentifiers.identifierTag -> identifier_set **)
405let empty_set tag =
406  empty_map tag
407
408(** val add_set :
409    PreIdentifiers.identifierTag -> identifier_set ->
410    PreIdentifiers.identifier -> identifier_set **)
411let add_set tag s i =
412  add tag s i Types.It
413
414(** val singleton_set :
415    PreIdentifiers.identifierTag -> PreIdentifiers.identifier ->
416    identifier_set **)
417let singleton_set tag i =
418  add_set tag (empty_set tag) i
419
420(** val union_set :
421    PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a2 identifier_map
422    -> identifier_set **)
423let rec union_set tag s s' =
424  PositiveMap.merge (fun o o' ->
425    match o with
426    | Types.None ->
427      Obj.magic
428        (Monad.m_bind0 (Monad.max_def Option.option) (Obj.magic o') (fun x ->
429          Monad.m_return0 (Monad.max_def Option.option) Types.It))
430    | Types.Some x -> Types.Some Types.It) (let s0 = s in s0)
431    (let s1 = s' in s1)
432
433(** val minus_set :
434    PreIdentifiers.identifierTag -> 'a1 identifier_map -> 'a2 identifier_map
435    -> 'a1 identifier_map **)
436let rec minus_set tag s s' =
437  PositiveMap.merge (fun o o' ->
438    match o' with
439    | Types.None -> o
440    | Types.Some x -> Types.None) (let s0 = s in s0) (let s1 = s' in s1)
441
442(** val identifierSet : PreIdentifiers.identifierTag -> Setoids.setoid **)
443let identifierSet tag =
444  Setoids.Mk_Setoid
445
446(** val id_map_size :
447    PreIdentifiers.identifierTag -> 'a1 identifier_map -> Nat.nat **)
448let id_map_size tag s =
449  let p = s in PositiveMap.domain_size p
450
451open Proper
452
453(** val set_from_list :
454    PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
455    Types.unit0 identifier_map **)
456let set_from_list tag =
457  Util.foldl (add_set tag) (empty_set tag)
458
459(** val dpi1__o__id_set_from_list__o__inject :
460    PreIdentifiers.identifierTag -> (PreIdentifiers.identifier List.list,
461    'a1) Types.dPair -> Types.unit0 identifier_map Types.sig0 **)
462let dpi1__o__id_set_from_list__o__inject x0 x3 =
463  set_from_list x0 x3.Types.dpi1
464
465(** val eject__o__id_set_from_list__o__inject :
466    PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list
467    Types.sig0 -> Types.unit0 identifier_map Types.sig0 **)
468let eject__o__id_set_from_list__o__inject x0 x3 =
469  set_from_list x0 (Types.pi1 x3)
470
471(** val id_set_from_list__o__inject :
472    PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
473    Types.unit0 identifier_map Types.sig0 **)
474let id_set_from_list__o__inject x0 x2 =
475  set_from_list x0 x2
476
477(** val dpi1__o__id_set_from_list :
478    PreIdentifiers.identifierTag -> (PreIdentifiers.identifier List.list,
479    'a1) Types.dPair -> Types.unit0 identifier_map **)
480let dpi1__o__id_set_from_list x0 x2 =
481  set_from_list x0 x2.Types.dpi1
482
483(** val eject__o__id_set_from_list :
484    PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list
485    Types.sig0 -> Types.unit0 identifier_map **)
486let eject__o__id_set_from_list x0 x2 =
487  set_from_list x0 (Types.pi1 x2)
488
489(** val choose :
490    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
491    ((PreIdentifiers.identifier, 'a1) Types.prod, 'a1 identifier_map)
492    Types.prod Types.option **)
493let choose tag m =
494  match PositiveMap.pm_choose (let m' = m in m') with
495  | Types.None -> Types.None
496  | Types.Some x ->
497    Types.Some { Types.fst = { Types.fst = x.Types.fst.Types.fst; Types.snd =
498      x.Types.fst.Types.snd }; Types.snd = x.Types.snd }
499
500(** val try_remove :
501    PreIdentifiers.identifierTag -> 'a1 identifier_map ->
502    PreIdentifiers.identifier -> ('a1, 'a1 identifier_map) Types.prod
503    Types.option **)
504let try_remove tag m id =
505  match PositiveMap.pm_try_remove (let id' = id in id') (let m' = m in m') with
506  | Types.None -> Types.None
507  | Types.Some x ->
508    Types.Some { Types.fst = x.Types.fst; Types.snd = x.Types.snd }
509
510(** val id_set_of_map :
511    PreIdentifiers.identifierTag -> 'a1 identifier_map -> identifier_set **)
512let id_set_of_map tag m =
513  PositiveMap.map (fun x -> Types.It) (let m' = m in m')
514
515(** val set_of_list :
516    PreIdentifiers.identifierTag -> PreIdentifiers.identifier List.list ->
517    identifier_set **)
518let set_of_list tag l =
519  Util.foldl (fun s id -> add_set tag s id) (empty_set tag) l
520
521(** val domain_of_map :
522    PreIdentifiers.identifierTag -> 'a1 identifier_map -> identifier_set **)
523let domain_of_map tag m =
524  PositiveMap.domain_of_pm (let m0 = m in m0)
525
Note: See TracBrowser for help on using the repository browser.