source: extracted/globalenvs.ml @ 2730

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

Exported again.

File size: 23.0 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_2466 =
101  let { functions = functions0; nextfunction = nextfunction0; symbols =
102    symbols0 } = x_2466
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_2468 =
110  let { functions = functions0; nextfunction = nextfunction0; symbols =
111    symbols0 } = x_2468
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_2470 =
119  let { functions = functions0; nextfunction = nextfunction0; symbols =
120    symbols0 } = x_2470
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_2472 =
128  let { functions = functions0; nextfunction = nextfunction0; symbols =
129    symbols0 } = x_2472
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_2474 =
137  let { functions = functions0; nextfunction = nextfunction0; symbols =
138    symbols0 } = x_2474
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_2476 =
146  let { functions = functions0; nextfunction = nextfunction0; symbols =
147    symbols0 } = x_2476
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 = eta860; Types.snd = init_info } = id_init in
317    let { Types.fst = id; Types.snd = r } = eta860 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 = eta861; Types.snd = init_info } = id_init in
333    let { Types.fst = id; Types.snd = r } = eta861 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 symbol_of_function_block' :
409    'a1 genv_t -> Pointers.block -> 'a1 -> AST.ident **)
410let symbol_of_function_block' ge b f =
411  symbol_of_function_block ge b
412
413(** val find_funct_ptr_id :
414    'a1 genv_t -> Pointers.block -> ('a1, AST.ident) Types.prod Types.option **)
415let find_funct_ptr_id ge b =
416  (match find_funct_ptr ge b with
417   | Types.None -> (fun _ -> Types.None)
418   | Types.Some f ->
419     (fun _ -> Types.Some { Types.fst = f; Types.snd =
420       (symbol_of_function_block' ge b f) })) __
421
422(** val symbol_of_function_val : 'a1 genv_t -> Values.val0 -> AST.ident **)
423let symbol_of_function_val ge v =
424  (match v with
425   | Values.Vundef -> (fun _ -> assert false (* absurd case *))
426   | Values.Vint (x, x0) -> (fun _ -> assert false (* absurd case *))
427   | Values.Vnull -> (fun _ -> assert false (* absurd case *))
428   | Values.Vptr p ->
429     (fun _ -> symbol_of_function_block ge p.Pointers.pblock)) __
430
431(** val symbol_of_function_val' :
432    'a1 genv_t -> Values.val0 -> 'a1 -> AST.ident **)
433let symbol_of_function_val' ge v f =
434  symbol_of_function_val ge v
435
436(** val find_funct_id :
437    'a1 genv_t -> Values.val0 -> ('a1, AST.ident) Types.prod Types.option **)
438let find_funct_id ge v =
439  (match find_funct ge v with
440   | Types.None -> (fun _ -> Types.None)
441   | Types.Some f ->
442     (fun _ -> Types.Some { Types.fst = f; Types.snd =
443       (symbol_of_function_val' ge v f) })) __
444
445(** val nat_plus_pos : Nat.nat -> Positive.pos -> Positive.pos **)
446let rec nat_plus_pos n p =
447  match n with
448  | Nat.O -> p
449  | Nat.S m -> Positive.succ (nat_plus_pos m p)
450
451(** val alloc_pair :
452    GenMem.mem1 -> GenMem.mem1 -> Z.z -> Z.z -> Z.z -> Z.z -> (GenMem.mem1 ->
453    GenMem.mem1 -> Pointers.block -> __ -> 'a1) -> 'a1 **)
454let alloc_pair clearme m' l h l' h' x =
455  (let { GenMem.blocks = ct; GenMem.nextblock = nx } = clearme in
456  (fun clearme0 ->
457  let { GenMem.blocks = ct'; GenMem.nextblock = nx' } = clearme0 in
458  (fun l0 h0 l'0 h'0 _ _ ->
459  Extralib.eq_rect_Type0_r1 nx' (fun _ h1 ->
460    h1 { GenMem.blocks =
461      (GenMem.update_block { GenMem.blocks = ct; GenMem.nextblock =
462        nx' }.GenMem.nextblock (GenMem.empty_block l0 h0) { GenMem.blocks =
463        ct; GenMem.nextblock = nx' }.GenMem.blocks); GenMem.nextblock =
464      (Z.zsucc { GenMem.blocks = ct; GenMem.nextblock =
465        nx' }.GenMem.nextblock) } { GenMem.blocks =
466      (GenMem.update_block { GenMem.blocks = ct'; GenMem.nextblock =
467        nx' }.GenMem.nextblock (GenMem.empty_block l'0 h'0) { GenMem.blocks =
468        ct'; GenMem.nextblock = nx' }.GenMem.blocks); GenMem.nextblock =
469      (Z.zsucc { GenMem.blocks = ct'; GenMem.nextblock =
470        nx' }.GenMem.nextblock) } { GenMem.blocks = ct; GenMem.nextblock =
471      nx' }.GenMem.nextblock __) nx __))) m' l h l' h' __ __ x
472
473(** val prod_jmdiscr0 :
474    ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod -> __ **)
475let prod_jmdiscr0 x y =
476  Logic.eq_rect_Type2 x
477    (let { Types.fst = a0; Types.snd = a10 } = x in
478    Obj.magic (fun _ dH -> dH __ __)) y
479
480(** val related_globals_rect_Type4 :
481    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
482    -> 'a3 **)
483let rec related_globals_rect_Type4 t ge ge' h_mk_related_globals =
484  h_mk_related_globals __ __ __ __
485
486(** val related_globals_rect_Type5 :
487    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
488    -> 'a3 **)
489let rec related_globals_rect_Type5 t ge ge' h_mk_related_globals =
490  h_mk_related_globals __ __ __ __
491
492(** val related_globals_rect_Type3 :
493    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
494    -> 'a3 **)
495let rec related_globals_rect_Type3 t ge ge' h_mk_related_globals =
496  h_mk_related_globals __ __ __ __
497
498(** val related_globals_rect_Type2 :
499    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
500    -> 'a3 **)
501let rec related_globals_rect_Type2 t ge ge' h_mk_related_globals =
502  h_mk_related_globals __ __ __ __
503
504(** val related_globals_rect_Type1 :
505    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
506    -> 'a3 **)
507let rec related_globals_rect_Type1 t ge ge' h_mk_related_globals =
508  h_mk_related_globals __ __ __ __
509
510(** val related_globals_rect_Type0 :
511    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
512    -> 'a3 **)
513let rec related_globals_rect_Type0 t ge ge' h_mk_related_globals =
514  h_mk_related_globals __ __ __ __
515
516(** val related_globals_inv_rect_Type4 :
517    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
518    -> 'a3) -> 'a3 **)
519let related_globals_inv_rect_Type4 x3 x4 x5 h1 =
520  let hcut = related_globals_rect_Type4 x3 x4 x5 h1 in hcut __
521
522(** val related_globals_inv_rect_Type3 :
523    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
524    -> 'a3) -> 'a3 **)
525let related_globals_inv_rect_Type3 x3 x4 x5 h1 =
526  let hcut = related_globals_rect_Type3 x3 x4 x5 h1 in hcut __
527
528(** val related_globals_inv_rect_Type2 :
529    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
530    -> 'a3) -> 'a3 **)
531let related_globals_inv_rect_Type2 x3 x4 x5 h1 =
532  let hcut = related_globals_rect_Type2 x3 x4 x5 h1 in hcut __
533
534(** val related_globals_inv_rect_Type1 :
535    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
536    -> 'a3) -> 'a3 **)
537let related_globals_inv_rect_Type1 x3 x4 x5 h1 =
538  let hcut = related_globals_rect_Type1 x3 x4 x5 h1 in hcut __
539
540(** val related_globals_inv_rect_Type0 :
541    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
542    -> 'a3) -> 'a3 **)
543let related_globals_inv_rect_Type0 x3 x4 x5 h1 =
544  let hcut = related_globals_rect_Type0 x3 x4 x5 h1 in hcut __
545
546(** val related_globals_discr :
547    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
548let related_globals_discr a3 a4 a5 =
549  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __
550
551(** val related_globals_jmdiscr :
552    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
553let related_globals_jmdiscr a3 a4 a5 =
554  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __
555
556(** val related_globals_gen_rect_Type4 :
557    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
558    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
559    __ -> __ -> __ -> 'a3) -> 'a3 **)
560let rec related_globals_gen_rect_Type4 tag t ge ge' h_mk_related_globals_gen =
561  h_mk_related_globals_gen __ __ __ __
562
563(** val related_globals_gen_rect_Type5 :
564    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
565    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
566    __ -> __ -> __ -> 'a3) -> 'a3 **)
567let rec related_globals_gen_rect_Type5 tag t ge ge' h_mk_related_globals_gen =
568  h_mk_related_globals_gen __ __ __ __
569
570(** val related_globals_gen_rect_Type3 :
571    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
572    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
573    __ -> __ -> __ -> 'a3) -> 'a3 **)
574let rec related_globals_gen_rect_Type3 tag t ge ge' h_mk_related_globals_gen =
575  h_mk_related_globals_gen __ __ __ __
576
577(** val related_globals_gen_rect_Type2 :
578    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
579    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
580    __ -> __ -> __ -> 'a3) -> 'a3 **)
581let rec related_globals_gen_rect_Type2 tag t ge ge' h_mk_related_globals_gen =
582  h_mk_related_globals_gen __ __ __ __
583
584(** val related_globals_gen_rect_Type1 :
585    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
586    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
587    __ -> __ -> __ -> 'a3) -> 'a3 **)
588let rec related_globals_gen_rect_Type1 tag t ge ge' h_mk_related_globals_gen =
589  h_mk_related_globals_gen __ __ __ __
590
591(** val related_globals_gen_rect_Type0 :
592    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
593    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
594    __ -> __ -> __ -> 'a3) -> 'a3 **)
595let rec related_globals_gen_rect_Type0 tag t ge ge' h_mk_related_globals_gen =
596  h_mk_related_globals_gen __ __ __ __
597
598(** val related_globals_gen_inv_rect_Type4 :
599    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
600    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
601    __ -> __ -> __ -> __ -> 'a3) -> 'a3 **)
602let related_globals_gen_inv_rect_Type4 x1 x4 x5 x6 h1 =
603  let hcut = related_globals_gen_rect_Type4 x1 x4 x5 x6 h1 in hcut __
604
605(** val related_globals_gen_inv_rect_Type3 :
606    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
607    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
608    __ -> __ -> __ -> __ -> 'a3) -> 'a3 **)
609let related_globals_gen_inv_rect_Type3 x1 x4 x5 x6 h1 =
610  let hcut = related_globals_gen_rect_Type3 x1 x4 x5 x6 h1 in hcut __
611
612(** val related_globals_gen_inv_rect_Type2 :
613    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
614    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
615    __ -> __ -> __ -> __ -> 'a3) -> 'a3 **)
616let related_globals_gen_inv_rect_Type2 x1 x4 x5 x6 h1 =
617  let hcut = related_globals_gen_rect_Type2 x1 x4 x5 x6 h1 in hcut __
618
619(** val related_globals_gen_inv_rect_Type1 :
620    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
621    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
622    __ -> __ -> __ -> __ -> 'a3) -> 'a3 **)
623let related_globals_gen_inv_rect_Type1 x1 x4 x5 x6 h1 =
624  let hcut = related_globals_gen_rect_Type1 x1 x4 x5 x6 h1 in hcut __
625
626(** val related_globals_gen_inv_rect_Type0 :
627    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
628    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
629    __ -> __ -> __ -> __ -> 'a3) -> 'a3 **)
630let related_globals_gen_inv_rect_Type0 x1 x4 x5 x6 h1 =
631  let hcut = related_globals_gen_rect_Type0 x1 x4 x5 x6 h1 in hcut __
632
633(** val related_globals_gen_discr :
634    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
635    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
636let related_globals_gen_discr a1 a4 a5 a6 =
637  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __
638
639(** val related_globals_gen_jmdiscr :
640    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
641    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
642let related_globals_gen_jmdiscr a1 a4 a5 a6 =
643  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __
644
645open Extra_bool
646
Note: See TracBrowser for help on using the repository browser.