source: extracted/globalenvs.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: 21.4 KB
Line 
1open Preamble
2
3open ErrorMessages
4
5open Option
6
7open Setoids
8
9open Monad
10
11open Jmeq
12
13open Russell
14
15open Positive
16
17open PreIdentifiers
18
19open Bool
20
21open Relations
22
23open Nat
24
25open List
26
27open Hints_declaration
28
29open Core_notation
30
31open Pts
32
33open Logic
34
35open Types
36
37open Errors
38
39open Proper
40
41open PositiveMap
42
43open Deqsets
44
45open Extralib
46
47open Lists
48
49open Identifiers
50
51open Exp
52
53open Arithmetic
54
55open Vector
56
57open Div_and_mod
58
59open Util
60
61open FoldStuff
62
63open BitVector
64
65open Extranat
66
67open Integers
68
69open AST
70
71open Coqlib
72
73open Values
74
75open FrontEndVal
76
77open Hide
78
79open ByteValues
80
81open Division
82
83open Z
84
85open BitVectorZ
86
87open Pointers
88
89open GenMem
90
91open FrontEndMem
92
93type 'f genv_t = { functions : 'f PositiveMap.positive_map;
94                   nextfunction : Positive.pos;
95                   symbols : Pointers.block Identifiers.identifier_map }
96
97(** val genv_t_rect_Type4 :
98    ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
99    Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
100let rec genv_t_rect_Type4 h_mk_genv_t x_6504 =
101  let { functions = functions0; nextfunction = nextfunction0; symbols =
102    symbols0 } = x_6504
103  in
104  h_mk_genv_t functions0 nextfunction0 symbols0 __
105
106(** val genv_t_rect_Type5 :
107    ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
108    Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
109let rec genv_t_rect_Type5 h_mk_genv_t x_6506 =
110  let { functions = functions0; nextfunction = nextfunction0; symbols =
111    symbols0 } = x_6506
112  in
113  h_mk_genv_t functions0 nextfunction0 symbols0 __
114
115(** val genv_t_rect_Type3 :
116    ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
117    Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
118let rec genv_t_rect_Type3 h_mk_genv_t x_6508 =
119  let { functions = functions0; nextfunction = nextfunction0; symbols =
120    symbols0 } = x_6508
121  in
122  h_mk_genv_t functions0 nextfunction0 symbols0 __
123
124(** val genv_t_rect_Type2 :
125    ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
126    Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
127let rec genv_t_rect_Type2 h_mk_genv_t x_6510 =
128  let { functions = functions0; nextfunction = nextfunction0; symbols =
129    symbols0 } = x_6510
130  in
131  h_mk_genv_t functions0 nextfunction0 symbols0 __
132
133(** val genv_t_rect_Type1 :
134    ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
135    Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
136let rec genv_t_rect_Type1 h_mk_genv_t x_6512 =
137  let { functions = functions0; nextfunction = nextfunction0; symbols =
138    symbols0 } = x_6512
139  in
140  h_mk_genv_t functions0 nextfunction0 symbols0 __
141
142(** val genv_t_rect_Type0 :
143    ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
144    Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
145let rec genv_t_rect_Type0 h_mk_genv_t x_6514 =
146  let { functions = functions0; nextfunction = nextfunction0; symbols =
147    symbols0 } = x_6514
148  in
149  h_mk_genv_t functions0 nextfunction0 symbols0 __
150
151(** val functions : 'a1 genv_t -> 'a1 PositiveMap.positive_map **)
152let rec functions xxx =
153  xxx.functions
154
155(** val nextfunction : 'a1 genv_t -> Positive.pos **)
156let rec nextfunction xxx =
157  xxx.nextfunction
158
159(** val symbols : 'a1 genv_t -> Pointers.block Identifiers.identifier_map **)
160let rec symbols xxx =
161  xxx.symbols
162
163(** val genv_t_inv_rect_Type4 :
164    'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
165    Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2 **)
166let genv_t_inv_rect_Type4 hterm h1 =
167  let hcut = genv_t_rect_Type4 h1 hterm in hcut __
168
169(** val genv_t_inv_rect_Type3 :
170    'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
171    Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2 **)
172let genv_t_inv_rect_Type3 hterm h1 =
173  let hcut = genv_t_rect_Type3 h1 hterm in hcut __
174
175(** val genv_t_inv_rect_Type2 :
176    'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
177    Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2 **)
178let genv_t_inv_rect_Type2 hterm h1 =
179  let hcut = genv_t_rect_Type2 h1 hterm in hcut __
180
181(** val genv_t_inv_rect_Type1 :
182    'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
183    Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2 **)
184let genv_t_inv_rect_Type1 hterm h1 =
185  let hcut = genv_t_rect_Type1 h1 hterm in hcut __
186
187(** val genv_t_inv_rect_Type0 :
188    'a1 genv_t -> ('a1 PositiveMap.positive_map -> Positive.pos ->
189    Pointers.block Identifiers.identifier_map -> __ -> __ -> 'a2) -> 'a2 **)
190let genv_t_inv_rect_Type0 hterm h1 =
191  let hcut = genv_t_rect_Type0 h1 hterm in hcut __
192
193(** val genv_t_discr : 'a1 genv_t -> 'a1 genv_t -> __ **)
194let genv_t_discr x y =
195  Logic.eq_rect_Type2 x
196    (let { functions = a0; nextfunction = a10; symbols = a2 } = x in
197    Obj.magic (fun _ dH -> dH __ __ __ __)) y
198
199(** val genv_t_jmdiscr : 'a1 genv_t -> 'a1 genv_t -> __ **)
200let genv_t_jmdiscr x y =
201  Logic.eq_rect_Type2 x
202    (let { functions = a0; nextfunction = a10; symbols = a2 } = x in
203    Obj.magic (fun _ dH -> dH __ __ __ __)) y
204
205(** val drop_fn : AST.ident -> 'a1 genv_t -> 'a1 genv_t **)
206let drop_fn id g0 =
207  let fns =
208    match Identifiers.lookup0 PreIdentifiers.SymbolTag g0.symbols id with
209    | Types.None -> g0.functions
210    | Types.Some b' ->
211      (match Pointers.block_id b' with
212       | Z.OZ -> g0.functions
213       | Z.Pos x -> g0.functions
214       | Z.Neg p -> PositiveMap.pm_set p Types.None g0.functions)
215  in
216  { functions = fns; nextfunction = g0.nextfunction; symbols =
217  (Identifiers.remove PreIdentifiers.SymbolTag g0.symbols id) }
218
219(** val add_funct :
220    (AST.ident, 'a1) Types.prod -> 'a1 genv_t -> 'a1 genv_t **)
221let add_funct name_fun g0 =
222  let blk_id = g0.nextfunction in
223  let b = Z.Neg blk_id in
224  let g' = drop_fn name_fun.Types.fst g0 in
225  { functions = (PositiveMap.insert blk_id name_fun.Types.snd g'.functions);
226  nextfunction = (Positive.succ blk_id); symbols =
227  (Identifiers.add PreIdentifiers.SymbolTag g'.symbols name_fun.Types.fst b) }
228
229(** val add_symbol :
230    AST.ident -> Pointers.block -> 'a1 genv_t -> 'a1 genv_t **)
231let add_symbol name b g0 =
232  let g' = drop_fn name g0 in
233  { functions = g'.functions; nextfunction = g'.nextfunction; symbols =
234  (Identifiers.add PreIdentifiers.SymbolTag g'.symbols name b) }
235
236(** val empty_mem : GenMem.mem1 **)
237let empty_mem =
238  GenMem.empty
239
240(** val empty0 : 'a1 genv_t **)
241let empty0 =
242  { functions = PositiveMap.Pm_leaf; nextfunction =
243    (Positive.succ_pos_of_nat (Nat.S (Nat.S Nat.O))); symbols =
244    (Identifiers.empty_map PreIdentifiers.SymbolTag) }
245
246(** val add_functs :
247    'a1 genv_t -> (AST.ident, 'a1) Types.prod List.list -> 'a1 genv_t **)
248let add_functs init fns =
249  List.foldr add_funct init fns
250
251(** val find_symbol :
252    'a1 genv_t -> AST.ident -> Pointers.block Types.option **)
253let find_symbol ge =
254  Identifiers.lookup0 PreIdentifiers.SymbolTag ge.symbols
255
256(** val store_init_data :
257    'a1 genv_t -> GenMem.mem1 -> Pointers.block -> Z.z -> AST.init_data ->
258    GenMem.mem1 Types.option **)
259let store_init_data ge m b p id =
260  let ptr = { Pointers.pblock = b; Pointers.poff =
261    (BitVectorZ.bitvector_of_Z Pointers.offset_size p) }
262  in
263  (match id with
264   | AST.Init_int8 n ->
265     FrontEndMem.store (AST.ASTint (AST.I8, AST.Unsigned)) m ptr (Values.Vint
266       (AST.I8, n))
267   | AST.Init_int16 n ->
268     FrontEndMem.store (AST.ASTint (AST.I16, AST.Unsigned)) m ptr
269       (Values.Vint (AST.I16, n))
270   | AST.Init_int32 n ->
271     FrontEndMem.store (AST.ASTint (AST.I32, AST.Unsigned)) m ptr
272       (Values.Vint (AST.I32, n))
273   | AST.Init_space n -> Types.Some m
274   | AST.Init_null -> FrontEndMem.store AST.ASTptr m ptr Values.Vnull
275   | AST.Init_addrof (symb, ofs) ->
276     (match find_symbol ge symb with
277      | Types.None -> Types.None
278      | Types.Some b' ->
279        FrontEndMem.store AST.ASTptr m ptr (Values.Vptr { Pointers.pblock =
280          b'; Pointers.poff =
281          (Pointers.shift_offset (AST.bitsize_of_intsize AST.I16)
282            Pointers.zero_offset (AST.repr0 AST.I16 ofs)) })))
283
284(** val size_init_data : AST.init_data -> Nat.nat **)
285let size_init_data = function
286| AST.Init_int8 x -> Nat.S Nat.O
287| AST.Init_int16 x -> Nat.S (Nat.S Nat.O)
288| AST.Init_int32 x -> Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))
289| AST.Init_space n -> Nat.max n Nat.O
290| AST.Init_null -> AST.size_pointer
291| AST.Init_addrof (x, x0) -> AST.size_pointer
292
293(** val store_init_data_list :
294    'a1 genv_t -> GenMem.mem1 -> Pointers.block -> Z.z -> AST.init_data
295    List.list -> GenMem.mem1 Types.option **)
296let rec store_init_data_list ge m b p = function
297| List.Nil -> Types.Some m
298| List.Cons (id, idl') ->
299  (match store_init_data ge m b p id with
300   | Types.None -> Types.None
301   | Types.Some m' ->
302     store_init_data_list ge m' b
303       (Z.zplus p (Z.z_of_nat (size_init_data id))) idl')
304
305(** val size_init_data_list : AST.init_data List.list -> Nat.nat **)
306let size_init_data_list i_data =
307  List.foldr (fun i_data0 sz -> Nat.plus (size_init_data i_data0) sz) Nat.O
308    i_data
309
310(** val add_globals :
311    ('a2 -> AST.init_data List.list) -> ('a1 genv_t, GenMem.mem1) Types.prod
312    -> ((AST.ident, AST.region) Types.prod, 'a2) Types.prod List.list -> ('a1
313    genv_t, GenMem.mem1) Types.prod **)
314let add_globals extract_init init_env vars =
315  Util.foldl (fun g_st id_init ->
316    let { Types.fst = eta1792; Types.snd = init_info } = id_init in
317    let { Types.fst = id; Types.snd = r } = eta1792 in
318    let init = extract_init init_info in
319    let { Types.fst = g0; Types.snd = st } = g_st in
320    let { Types.fst = st'; Types.snd = b } =
321      GenMem.alloc st Z.OZ (Z.z_of_nat (size_init_data_list init))
322    in
323    let g' = add_symbol id b g0 in { Types.fst = g'; Types.snd = st' })
324    init_env vars
325
326(** val init_globals :
327    ('a2 -> AST.init_data List.list) -> 'a1 genv_t -> GenMem.mem1 ->
328    ((AST.ident, AST.region) Types.prod, 'a2) Types.prod List.list ->
329    GenMem.mem1 Errors.res **)
330let init_globals extract_init g0 m vars =
331  Util.foldl (fun st id_init ->
332    let { Types.fst = eta1793; Types.snd = init_info } = id_init in
333    let { Types.fst = id; Types.snd = r } = eta1793 in
334    let init = extract_init init_info in
335    Obj.magic
336      (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic st) (fun st0 ->
337        match find_symbol g0 id with
338        | Types.None ->
339          Obj.magic (Errors.Error
340            (Errors.msg ErrorMessages.InitDataStoreFailed))
341        | Types.Some b ->
342          Obj.magic
343            (Errors.opt_to_res (Errors.msg ErrorMessages.InitDataStoreFailed)
344              (store_init_data_list g0 st0 b Z.OZ init))))) (Errors.OK m)
345    vars
346
347(** val globalenv_allocmem :
348    ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> ('a1
349    genv_t, GenMem.mem1) Types.prod **)
350let globalenv_allocmem init_info p =
351  add_globals init_info { Types.fst = (add_functs empty0 p.AST.prog_funct);
352    Types.snd = empty_mem } p.AST.prog_vars
353
354(** val globalenv :
355    ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> 'a1 genv_t **)
356let globalenv i p =
357  (globalenv_allocmem i p).Types.fst
358
359(** val globalenv_noinit : ('a1, Nat.nat) AST.program -> 'a1 genv_t **)
360let globalenv_noinit p =
361  globalenv (fun n -> List.Cons ((AST.Init_space n), List.Nil)) p
362
363(** val init_mem :
364    ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> GenMem.mem1
365    Errors.res **)
366let init_mem i p =
367  let { Types.fst = g0; Types.snd = m } = globalenv_allocmem i p in
368  init_globals i g0 m p.AST.prog_vars
369
370(** val alloc_mem : ('a1, Nat.nat) AST.program -> GenMem.mem1 **)
371let alloc_mem p =
372  (globalenv_allocmem (fun n -> List.Cons ((AST.Init_space n), List.Nil)) p).Types.snd
373
374(** val find_funct_ptr : 'a1 genv_t -> Pointers.block -> 'a1 Types.option **)
375let find_funct_ptr ge b =
376  match Pointers.block_region b with
377  | AST.XData -> Types.None
378  | AST.Code ->
379    (match Pointers.block_id b with
380     | Z.OZ -> Types.None
381     | Z.Pos x -> Types.None
382     | Z.Neg p -> PositiveMap.lookup_opt p ge.functions)
383
384(** val find_funct : 'a1 genv_t -> Values.val0 -> 'a1 Types.option **)
385let find_funct ge = function
386| Values.Vundef -> Types.None
387| Values.Vint (x, x0) -> Types.None
388| Values.Vnull -> Types.None
389| Values.Vptr ptr ->
390  (match Pointers.eq_offset ptr.Pointers.poff Pointers.zero_offset with
391   | Bool.True -> find_funct_ptr ge ptr.Pointers.pblock
392   | Bool.False -> Types.None)
393
394(** val symbol_for_block :
395    'a1 genv_t -> Pointers.block -> AST.ident Types.option **)
396let symbol_for_block genv b =
397  Types.option_map Types.fst
398    (Identifiers.find0 PreIdentifiers.SymbolTag genv.symbols (fun id b' ->
399      Pointers.eq_block b b'))
400
401(** val symbol_of_function_block :
402    'a1 genv_t -> Pointers.block -> AST.ident **)
403let symbol_of_function_block ge b =
404  (match symbol_for_block ge b with
405   | Types.None -> (fun _ -> assert false (* absurd case *))
406   | Types.Some id -> (fun _ -> id)) __
407
408(** val nat_plus_pos : Nat.nat -> Positive.pos -> Positive.pos **)
409let rec nat_plus_pos n p =
410  match n with
411  | Nat.O -> p
412  | Nat.S m -> Positive.succ (nat_plus_pos m p)
413
414(** val alloc_pair :
415    GenMem.mem1 -> GenMem.mem1 -> Z.z -> Z.z -> Z.z -> Z.z -> (GenMem.mem1 ->
416    GenMem.mem1 -> Pointers.block -> __ -> 'a1) -> 'a1 **)
417let alloc_pair clearme m' l h l' h' x =
418  (let { GenMem.blocks = ct; GenMem.nextblock = nx } = clearme in
419  (fun clearme0 ->
420  let { GenMem.blocks = ct'; GenMem.nextblock = nx' } = clearme0 in
421  (fun l0 h0 l'0 h'0 _ _ ->
422  Extralib.eq_rect_Type0_r1 nx' (fun _ h1 ->
423    h1 { GenMem.blocks =
424      (GenMem.update_block { GenMem.blocks = ct; GenMem.nextblock =
425        nx' }.GenMem.nextblock (GenMem.empty_block l0 h0) { GenMem.blocks =
426        ct; GenMem.nextblock = nx' }.GenMem.blocks); GenMem.nextblock =
427      (Z.zsucc { GenMem.blocks = ct; GenMem.nextblock =
428        nx' }.GenMem.nextblock) } { GenMem.blocks =
429      (GenMem.update_block { GenMem.blocks = ct'; GenMem.nextblock =
430        nx' }.GenMem.nextblock (GenMem.empty_block l'0 h'0) { GenMem.blocks =
431        ct'; GenMem.nextblock = nx' }.GenMem.blocks); GenMem.nextblock =
432      (Z.zsucc { GenMem.blocks = ct'; GenMem.nextblock =
433        nx' }.GenMem.nextblock) } { GenMem.blocks = ct; GenMem.nextblock =
434      nx' }.GenMem.nextblock __) nx __))) m' l h l' h' __ __ x
435
436(** val prod_jmdiscr0 :
437    ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod -> __ **)
438let prod_jmdiscr0 x y =
439  Logic.eq_rect_Type2 x
440    (let { Types.fst = a0; Types.snd = a10 } = x in
441    Obj.magic (fun _ dH -> dH __ __)) y
442
443(** val related_globals_rect_Type4 :
444    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> 'a3) ->
445    'a3 **)
446let rec related_globals_rect_Type4 t ge ge' h_mk_related_globals =
447  h_mk_related_globals __ __ __
448
449(** val related_globals_rect_Type5 :
450    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> 'a3) ->
451    'a3 **)
452let rec related_globals_rect_Type5 t ge ge' h_mk_related_globals =
453  h_mk_related_globals __ __ __
454
455(** val related_globals_rect_Type3 :
456    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> 'a3) ->
457    'a3 **)
458let rec related_globals_rect_Type3 t ge ge' h_mk_related_globals =
459  h_mk_related_globals __ __ __
460
461(** val related_globals_rect_Type2 :
462    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> 'a3) ->
463    'a3 **)
464let rec related_globals_rect_Type2 t ge ge' h_mk_related_globals =
465  h_mk_related_globals __ __ __
466
467(** val related_globals_rect_Type1 :
468    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> 'a3) ->
469    'a3 **)
470let rec related_globals_rect_Type1 t ge ge' h_mk_related_globals =
471  h_mk_related_globals __ __ __
472
473(** val related_globals_rect_Type0 :
474    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> 'a3) ->
475    'a3 **)
476let rec related_globals_rect_Type0 t ge ge' h_mk_related_globals =
477  h_mk_related_globals __ __ __
478
479(** val related_globals_inv_rect_Type4 :
480    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
481    -> 'a3 **)
482let related_globals_inv_rect_Type4 x3 x4 x5 h1 =
483  let hcut = related_globals_rect_Type4 x3 x4 x5 h1 in hcut __
484
485(** val related_globals_inv_rect_Type3 :
486    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
487    -> 'a3 **)
488let related_globals_inv_rect_Type3 x3 x4 x5 h1 =
489  let hcut = related_globals_rect_Type3 x3 x4 x5 h1 in hcut __
490
491(** val related_globals_inv_rect_Type2 :
492    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
493    -> 'a3 **)
494let related_globals_inv_rect_Type2 x3 x4 x5 h1 =
495  let hcut = related_globals_rect_Type2 x3 x4 x5 h1 in hcut __
496
497(** val related_globals_inv_rect_Type1 :
498    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
499    -> 'a3 **)
500let related_globals_inv_rect_Type1 x3 x4 x5 h1 =
501  let hcut = related_globals_rect_Type1 x3 x4 x5 h1 in hcut __
502
503(** val related_globals_inv_rect_Type0 :
504    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
505    -> 'a3 **)
506let related_globals_inv_rect_Type0 x3 x4 x5 h1 =
507  let hcut = related_globals_rect_Type0 x3 x4 x5 h1 in hcut __
508
509(** val related_globals_discr :
510    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
511let related_globals_discr a3 a4 a5 =
512  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
513
514(** val related_globals_jmdiscr :
515    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
516let related_globals_jmdiscr a3 a4 a5 =
517  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
518
519(** val related_globals_gen_rect_Type4 :
520    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
521    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
522    __ -> __ -> 'a3) -> 'a3 **)
523let rec related_globals_gen_rect_Type4 tag t ge ge' h_mk_related_globals_gen =
524  h_mk_related_globals_gen __ __ __
525
526(** val related_globals_gen_rect_Type5 :
527    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
528    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
529    __ -> __ -> 'a3) -> 'a3 **)
530let rec related_globals_gen_rect_Type5 tag t ge ge' h_mk_related_globals_gen =
531  h_mk_related_globals_gen __ __ __
532
533(** val related_globals_gen_rect_Type3 :
534    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
535    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
536    __ -> __ -> 'a3) -> 'a3 **)
537let rec related_globals_gen_rect_Type3 tag t ge ge' h_mk_related_globals_gen =
538  h_mk_related_globals_gen __ __ __
539
540(** val related_globals_gen_rect_Type2 :
541    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
542    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
543    __ -> __ -> 'a3) -> 'a3 **)
544let rec related_globals_gen_rect_Type2 tag t ge ge' h_mk_related_globals_gen =
545  h_mk_related_globals_gen __ __ __
546
547(** val related_globals_gen_rect_Type1 :
548    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
549    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
550    __ -> __ -> 'a3) -> 'a3 **)
551let rec related_globals_gen_rect_Type1 tag t ge ge' h_mk_related_globals_gen =
552  h_mk_related_globals_gen __ __ __
553
554(** val related_globals_gen_rect_Type0 :
555    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
556    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
557    __ -> __ -> 'a3) -> 'a3 **)
558let rec related_globals_gen_rect_Type0 tag t ge ge' h_mk_related_globals_gen =
559  h_mk_related_globals_gen __ __ __
560
561(** val related_globals_gen_inv_rect_Type4 :
562    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
563    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
564    __ -> __ -> __ -> 'a3) -> 'a3 **)
565let related_globals_gen_inv_rect_Type4 x1 x4 x5 x6 h1 =
566  let hcut = related_globals_gen_rect_Type4 x1 x4 x5 x6 h1 in hcut __
567
568(** val related_globals_gen_inv_rect_Type3 :
569    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
570    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
571    __ -> __ -> __ -> 'a3) -> 'a3 **)
572let related_globals_gen_inv_rect_Type3 x1 x4 x5 x6 h1 =
573  let hcut = related_globals_gen_rect_Type3 x1 x4 x5 x6 h1 in hcut __
574
575(** val related_globals_gen_inv_rect_Type2 :
576    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
577    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
578    __ -> __ -> __ -> 'a3) -> 'a3 **)
579let related_globals_gen_inv_rect_Type2 x1 x4 x5 x6 h1 =
580  let hcut = related_globals_gen_rect_Type2 x1 x4 x5 x6 h1 in hcut __
581
582(** val related_globals_gen_inv_rect_Type1 :
583    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
584    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
585    __ -> __ -> __ -> 'a3) -> 'a3 **)
586let related_globals_gen_inv_rect_Type1 x1 x4 x5 x6 h1 =
587  let hcut = related_globals_gen_rect_Type1 x1 x4 x5 x6 h1 in hcut __
588
589(** val related_globals_gen_inv_rect_Type0 :
590    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
591    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
592    __ -> __ -> __ -> 'a3) -> 'a3 **)
593let related_globals_gen_inv_rect_Type0 x1 x4 x5 x6 h1 =
594  let hcut = related_globals_gen_rect_Type0 x1 x4 x5 x6 h1 in hcut __
595
596(** val related_globals_gen_discr :
597    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
598    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
599let related_globals_gen_discr a1 a4 a5 a6 =
600  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
601
602(** val related_globals_gen_jmdiscr :
603    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
604    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
605let related_globals_gen_jmdiscr a1 a4 a5 a6 =
606  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
607
608open Extra_bool
609
Note: See TracBrowser for help on using the repository browser.