source: extracted/globalenvs.ml @ 2649

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

...

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