source: extracted/globalenvs.ml @ 2746

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

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File size: 26.2 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_6530 =
101  let { functions = functions0; nextfunction = nextfunction0; symbols =
102    symbols0 } = x_6530
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_6532 =
110  let { functions = functions0; nextfunction = nextfunction0; symbols =
111    symbols0 } = x_6532
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_6534 =
119  let { functions = functions0; nextfunction = nextfunction0; symbols =
120    symbols0 } = x_6534
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_6536 =
128  let { functions = functions0; nextfunction = nextfunction0; symbols =
129    symbols0 } = x_6536
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_6538 =
137  let { functions = functions0; nextfunction = nextfunction0; symbols =
138    symbols0 } = x_6538
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_6540 =
146  let { functions = functions0; nextfunction = nextfunction0; symbols =
147    symbols0 } = x_6540
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 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 opt_eq_from_res__o__ffpi_drop__o__inject :
423    Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __
424    Types.sig0 **)
425let opt_eq_from_res__o__ffpi_drop__o__inject x0 x2 x3 x4 x5 =
426  __
427
428(** val dpi1__o__opt_eq_from_res__o__ffpi_drop__o__inject :
429    Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> (__,
430    'a2) Types.dPair -> __ Types.sig0 **)
431let dpi1__o__opt_eq_from_res__o__ffpi_drop__o__inject x0 x2 x3 x4 x5 x8 =
432  __
433
434(** val eject__o__opt_eq_from_res__o__ffpi_drop__o__inject :
435    Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __
436    Types.sig0 -> __ Types.sig0 **)
437let eject__o__opt_eq_from_res__o__ffpi_drop__o__inject x0 x2 x3 x4 x5 x8 =
438  __
439
440(** val jmeq_to_eq__o__ffpi_drop__o__inject :
441    Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 **)
442let jmeq_to_eq__o__ffpi_drop__o__inject x1 x2 x3 x4 =
443  __
444
445(** val jmeq_to_eq__o__opt_eq_from_res__o__ffpi_drop__o__inject :
446    Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __
447    Types.sig0 **)
448let jmeq_to_eq__o__opt_eq_from_res__o__ffpi_drop__o__inject x0 x2 x3 x4 x5 =
449  __
450
451(** val dpi1__o__ffpi_drop__o__inject :
452    Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> (__, 'a2) Types.dPair
453    -> __ Types.sig0 **)
454let dpi1__o__ffpi_drop__o__inject x1 x2 x3 x4 x7 =
455  __
456
457(** val eject__o__ffpi_drop__o__inject :
458    Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 -> __
459    Types.sig0 **)
460let eject__o__ffpi_drop__o__inject x1 x2 x3 x4 x7 =
461  __
462
463(** val ffpi_drop__o__inject :
464    Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 **)
465let ffpi_drop__o__inject x1 x2 x3 x4 =
466  __
467
468(** val symbol_of_function_val : 'a1 genv_t -> Values.val0 -> AST.ident **)
469let symbol_of_function_val ge v =
470  (match v with
471   | Values.Vundef -> (fun _ -> assert false (* absurd case *))
472   | Values.Vint (x, x0) -> (fun _ -> assert false (* absurd case *))
473   | Values.Vnull -> (fun _ -> assert false (* absurd case *))
474   | Values.Vptr p ->
475     (fun _ -> symbol_of_function_block ge p.Pointers.pblock)) __
476
477(** val symbol_of_function_val' :
478    'a1 genv_t -> Values.val0 -> 'a1 -> AST.ident **)
479let symbol_of_function_val' ge v f =
480  symbol_of_function_val ge v
481
482(** val find_funct_id :
483    'a1 genv_t -> Values.val0 -> ('a1, AST.ident) Types.prod Types.option **)
484let find_funct_id ge v =
485  (match find_funct ge v with
486   | Types.None -> (fun _ -> Types.None)
487   | Types.Some f ->
488     (fun _ -> Types.Some { Types.fst = f; Types.snd =
489       (symbol_of_function_val' ge v f) })) __
490
491(** val opt_eq_from_res__o__ffi_drop__o__inject :
492    Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __
493    Types.sig0 **)
494let opt_eq_from_res__o__ffi_drop__o__inject x0 x2 x3 x4 x5 =
495  __
496
497(** val dpi1__o__opt_eq_from_res__o__ffi_drop__o__inject :
498    Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> (__,
499    'a2) Types.dPair -> __ Types.sig0 **)
500let dpi1__o__opt_eq_from_res__o__ffi_drop__o__inject x0 x2 x3 x4 x5 x8 =
501  __
502
503(** val eject__o__opt_eq_from_res__o__ffi_drop__o__inject :
504    Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __
505    Types.sig0 -> __ Types.sig0 **)
506let eject__o__opt_eq_from_res__o__ffi_drop__o__inject x0 x2 x3 x4 x5 x8 =
507  __
508
509(** val jmeq_to_eq__o__ffi_drop__o__inject :
510    Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 **)
511let jmeq_to_eq__o__ffi_drop__o__inject x1 x2 x3 x4 =
512  __
513
514(** val jmeq_to_eq__o__opt_eq_from_res__o__ffi_drop__o__inject :
515    Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __
516    Types.sig0 **)
517let jmeq_to_eq__o__opt_eq_from_res__o__ffi_drop__o__inject x0 x2 x3 x4 x5 =
518  __
519
520(** val dpi1__o__ffi_drop__o__inject :
521    Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> (__, 'a2) Types.dPair ->
522    __ Types.sig0 **)
523let dpi1__o__ffi_drop__o__inject x1 x2 x3 x4 x7 =
524  __
525
526(** val eject__o__ffi_drop__o__inject :
527    Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 -> __
528    Types.sig0 **)
529let eject__o__ffi_drop__o__inject x1 x2 x3 x4 x7 =
530  __
531
532(** val ffi_drop__o__inject :
533    Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 **)
534let ffi_drop__o__inject x1 x2 x3 x4 =
535  __
536
537(** val nat_plus_pos : Nat.nat -> Positive.pos -> Positive.pos **)
538let rec nat_plus_pos n p =
539  match n with
540  | Nat.O -> p
541  | Nat.S m -> Positive.succ (nat_plus_pos m p)
542
543(** val alloc_pair :
544    GenMem.mem1 -> GenMem.mem1 -> Z.z -> Z.z -> Z.z -> Z.z -> (GenMem.mem1 ->
545    GenMem.mem1 -> Pointers.block -> __ -> 'a1) -> 'a1 **)
546let alloc_pair clearme m' l h l' h' x =
547  (let { GenMem.blocks = ct; GenMem.nextblock = nx } = clearme in
548  (fun clearme0 ->
549  let { GenMem.blocks = ct'; GenMem.nextblock = nx' } = clearme0 in
550  (fun l0 h0 l'0 h'0 _ _ ->
551  Extralib.eq_rect_Type0_r1 nx' (fun _ h1 ->
552    h1 { GenMem.blocks =
553      (GenMem.update_block { GenMem.blocks = ct; GenMem.nextblock =
554        nx' }.GenMem.nextblock (GenMem.empty_block l0 h0) { GenMem.blocks =
555        ct; GenMem.nextblock = nx' }.GenMem.blocks); GenMem.nextblock =
556      (Z.zsucc { GenMem.blocks = ct; GenMem.nextblock =
557        nx' }.GenMem.nextblock) } { GenMem.blocks =
558      (GenMem.update_block { GenMem.blocks = ct'; GenMem.nextblock =
559        nx' }.GenMem.nextblock (GenMem.empty_block l'0 h'0) { GenMem.blocks =
560        ct'; GenMem.nextblock = nx' }.GenMem.blocks); GenMem.nextblock =
561      (Z.zsucc { GenMem.blocks = ct'; GenMem.nextblock =
562        nx' }.GenMem.nextblock) } { GenMem.blocks = ct; GenMem.nextblock =
563      nx' }.GenMem.nextblock __) nx __))) m' l h l' h' __ __ x
564
565(** val prod_jmdiscr0 :
566    ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod -> __ **)
567let prod_jmdiscr0 x y =
568  Logic.eq_rect_Type2 x
569    (let { Types.fst = a0; Types.snd = a10 } = x in
570    Obj.magic (fun _ dH -> dH __ __)) y
571
572(** val related_globals_rect_Type4 :
573    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
574    -> 'a3 **)
575let rec related_globals_rect_Type4 t ge ge' h_mk_related_globals =
576  h_mk_related_globals __ __ __ __
577
578(** val related_globals_rect_Type5 :
579    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
580    -> 'a3 **)
581let rec related_globals_rect_Type5 t ge ge' h_mk_related_globals =
582  h_mk_related_globals __ __ __ __
583
584(** val related_globals_rect_Type3 :
585    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
586    -> 'a3 **)
587let rec related_globals_rect_Type3 t ge ge' h_mk_related_globals =
588  h_mk_related_globals __ __ __ __
589
590(** val related_globals_rect_Type2 :
591    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
592    -> 'a3 **)
593let rec related_globals_rect_Type2 t ge ge' h_mk_related_globals =
594  h_mk_related_globals __ __ __ __
595
596(** val related_globals_rect_Type1 :
597    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
598    -> 'a3 **)
599let rec related_globals_rect_Type1 t ge ge' h_mk_related_globals =
600  h_mk_related_globals __ __ __ __
601
602(** val related_globals_rect_Type0 :
603    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
604    -> 'a3 **)
605let rec related_globals_rect_Type0 t ge ge' h_mk_related_globals =
606  h_mk_related_globals __ __ __ __
607
608(** val related_globals_inv_rect_Type4 :
609    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
610    -> 'a3) -> 'a3 **)
611let related_globals_inv_rect_Type4 x3 x4 x5 h1 =
612  let hcut = related_globals_rect_Type4 x3 x4 x5 h1 in hcut __
613
614(** val related_globals_inv_rect_Type3 :
615    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
616    -> 'a3) -> 'a3 **)
617let related_globals_inv_rect_Type3 x3 x4 x5 h1 =
618  let hcut = related_globals_rect_Type3 x3 x4 x5 h1 in hcut __
619
620(** val related_globals_inv_rect_Type2 :
621    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
622    -> 'a3) -> 'a3 **)
623let related_globals_inv_rect_Type2 x3 x4 x5 h1 =
624  let hcut = related_globals_rect_Type2 x3 x4 x5 h1 in hcut __
625
626(** val related_globals_inv_rect_Type1 :
627    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
628    -> 'a3) -> 'a3 **)
629let related_globals_inv_rect_Type1 x3 x4 x5 h1 =
630  let hcut = related_globals_rect_Type1 x3 x4 x5 h1 in hcut __
631
632(** val related_globals_inv_rect_Type0 :
633    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
634    -> 'a3) -> 'a3 **)
635let related_globals_inv_rect_Type0 x3 x4 x5 h1 =
636  let hcut = related_globals_rect_Type0 x3 x4 x5 h1 in hcut __
637
638(** val related_globals_discr :
639    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
640let related_globals_discr a3 a4 a5 =
641  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __
642
643(** val related_globals_jmdiscr :
644    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
645let related_globals_jmdiscr a3 a4 a5 =
646  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __
647
648(** val related_globals_gen_rect_Type4 :
649    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
650    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
651    __ -> __ -> __ -> 'a3) -> 'a3 **)
652let rec related_globals_gen_rect_Type4 tag t ge ge' h_mk_related_globals_gen =
653  h_mk_related_globals_gen __ __ __ __
654
655(** val related_globals_gen_rect_Type5 :
656    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
657    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
658    __ -> __ -> __ -> 'a3) -> 'a3 **)
659let rec related_globals_gen_rect_Type5 tag t ge ge' h_mk_related_globals_gen =
660  h_mk_related_globals_gen __ __ __ __
661
662(** val related_globals_gen_rect_Type3 :
663    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
664    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
665    __ -> __ -> __ -> 'a3) -> 'a3 **)
666let rec related_globals_gen_rect_Type3 tag t ge ge' h_mk_related_globals_gen =
667  h_mk_related_globals_gen __ __ __ __
668
669(** val related_globals_gen_rect_Type2 :
670    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
671    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
672    __ -> __ -> __ -> 'a3) -> 'a3 **)
673let rec related_globals_gen_rect_Type2 tag t ge ge' h_mk_related_globals_gen =
674  h_mk_related_globals_gen __ __ __ __
675
676(** val related_globals_gen_rect_Type1 :
677    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
678    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
679    __ -> __ -> __ -> 'a3) -> 'a3 **)
680let rec related_globals_gen_rect_Type1 tag t ge ge' h_mk_related_globals_gen =
681  h_mk_related_globals_gen __ __ __ __
682
683(** val related_globals_gen_rect_Type0 :
684    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
685    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
686    __ -> __ -> __ -> 'a3) -> 'a3 **)
687let rec related_globals_gen_rect_Type0 tag t ge ge' h_mk_related_globals_gen =
688  h_mk_related_globals_gen __ __ __ __
689
690(** val related_globals_gen_inv_rect_Type4 :
691    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
692    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
693    __ -> __ -> __ -> __ -> 'a3) -> 'a3 **)
694let related_globals_gen_inv_rect_Type4 x1 x4 x5 x6 h1 =
695  let hcut = related_globals_gen_rect_Type4 x1 x4 x5 x6 h1 in hcut __
696
697(** val related_globals_gen_inv_rect_Type3 :
698    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
699    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
700    __ -> __ -> __ -> __ -> 'a3) -> 'a3 **)
701let related_globals_gen_inv_rect_Type3 x1 x4 x5 x6 h1 =
702  let hcut = related_globals_gen_rect_Type3 x1 x4 x5 x6 h1 in hcut __
703
704(** val related_globals_gen_inv_rect_Type2 :
705    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
706    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
707    __ -> __ -> __ -> __ -> 'a3) -> 'a3 **)
708let related_globals_gen_inv_rect_Type2 x1 x4 x5 x6 h1 =
709  let hcut = related_globals_gen_rect_Type2 x1 x4 x5 x6 h1 in hcut __
710
711(** val related_globals_gen_inv_rect_Type1 :
712    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
713    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
714    __ -> __ -> __ -> __ -> 'a3) -> 'a3 **)
715let related_globals_gen_inv_rect_Type1 x1 x4 x5 x6 h1 =
716  let hcut = related_globals_gen_rect_Type1 x1 x4 x5 x6 h1 in hcut __
717
718(** val related_globals_gen_inv_rect_Type0 :
719    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
720    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
721    __ -> __ -> __ -> __ -> 'a3) -> 'a3 **)
722let related_globals_gen_inv_rect_Type0 x1 x4 x5 x6 h1 =
723  let hcut = related_globals_gen_rect_Type0 x1 x4 x5 x6 h1 in hcut __
724
725(** val related_globals_gen_discr :
726    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
727    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
728let related_globals_gen_discr a1 a4 a5 a6 =
729  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __
730
731(** val related_globals_gen_jmdiscr :
732    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
733    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
734let related_globals_gen_jmdiscr a1 a4 a5 a6 =
735  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __
736
737open Extra_bool
738
Note: See TracBrowser for help on using the repository browser.