source: driver/extracted/globalenvs.ml @ 3106

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

New extraction.

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_6621 =
101  let { functions = functions0; nextfunction = nextfunction0; symbols =
102    symbols0 } = x_6621
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_6623 =
110  let { functions = functions0; nextfunction = nextfunction0; symbols =
111    symbols0 } = x_6623
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_6625 =
119  let { functions = functions0; nextfunction = nextfunction0; symbols =
120    symbols0 } = x_6625
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_6627 =
128  let { functions = functions0; nextfunction = nextfunction0; symbols =
129    symbols0 } = x_6627
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_6629 =
137  let { functions = functions0; nextfunction = nextfunction0; symbols =
138    symbols0 } = x_6629
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_6631 =
146  let { functions = functions0; nextfunction = nextfunction0; symbols =
147    symbols0 } = x_6631
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 g =
207  let fns =
208    match Identifiers.lookup PreIdentifiers.SymbolTag g.symbols id with
209    | Types.None -> g.functions
210    | Types.Some b' ->
211      (match Pointers.block_id b' with
212       | Z.OZ -> g.functions
213       | Z.Pos x -> g.functions
214       | Z.Neg p -> PositiveMap.pm_set p Types.None g.functions)
215  in
216  { functions = fns; nextfunction = g.nextfunction; symbols =
217  (Identifiers.remove PreIdentifiers.SymbolTag g.symbols id) }
218
219(** val add_funct :
220    (AST.ident, 'a1) Types.prod -> 'a1 genv_t -> 'a1 genv_t **)
221let add_funct name_fun g =
222  let blk_id = g.nextfunction in
223  let b = Z.Neg blk_id in
224  let g' = drop_fn name_fun.Types.fst g 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 g =
232  let g' = drop_fn name g in
233  { functions = g'.functions; nextfunction = g'.nextfunction; symbols =
234  (Identifiers.add PreIdentifiers.SymbolTag g'.symbols name b) }
235
236(** val empty_mem : GenMem.mem **)
237let empty_mem =
238  GenMem.empty
239
240(** val empty : 'a1 genv_t **)
241let empty =
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.lookup PreIdentifiers.SymbolTag ge.symbols
255
256(** val store_init_data :
257    'a1 genv_t -> GenMem.mem -> Pointers.block -> Z.z -> AST.init_data ->
258    GenMem.mem 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.repr 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.mem -> Pointers.block -> Z.z -> AST.init_data
295    List.list -> GenMem.mem 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.mem) Types.prod
312    -> ((AST.ident, AST.region) Types.prod, 'a2) Types.prod List.list -> ('a1
313    genv_t, GenMem.mem) Types.prod **)
314let add_globals extract_init init_env vars =
315  Util.foldl (fun g_st id_init ->
316    let { Types.fst = eta1367; Types.snd = init_info } = id_init in
317    let { Types.fst = id; Types.snd = r } = eta1367 in
318    let init = extract_init init_info in
319    let { Types.fst = g; 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 g 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.mem ->
328    ((AST.ident, AST.region) Types.prod, 'a2) Types.prod List.list ->
329    GenMem.mem Errors.res **)
330let init_globals extract_init g m vars =
331  Util.foldl (fun st id_init ->
332    let { Types.fst = eta1368; Types.snd = init_info } = id_init in
333    let { Types.fst = id; Types.snd = r } = eta1368 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 g 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 g st0 b Z.OZ init))))) (Errors.OK m) vars
345
346(** val globalenv_allocmem :
347    ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> ('a1
348    genv_t, GenMem.mem) Types.prod **)
349let globalenv_allocmem init_info p =
350  add_globals init_info { Types.fst = (add_functs empty p.AST.prog_funct);
351    Types.snd = empty_mem } p.AST.prog_vars
352
353(** val globalenv :
354    ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> 'a1 genv_t **)
355let globalenv i p =
356  (globalenv_allocmem i p).Types.fst
357
358(** val globalenv_noinit : ('a1, Nat.nat) AST.program -> 'a1 genv_t **)
359let globalenv_noinit p =
360  globalenv (fun n -> List.Cons ((AST.Init_space n), List.Nil)) p
361
362(** val init_mem :
363    ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> GenMem.mem
364    Errors.res **)
365let init_mem i p =
366  let { Types.fst = g; Types.snd = m } = globalenv_allocmem i p in
367  init_globals i g m p.AST.prog_vars
368
369(** val alloc_mem : ('a1, Nat.nat) AST.program -> GenMem.mem **)
370let alloc_mem p =
371  (globalenv_allocmem (fun n -> List.Cons ((AST.Init_space n), List.Nil)) p).Types.snd
372
373(** val find_funct_ptr : 'a1 genv_t -> Pointers.block -> 'a1 Types.option **)
374let find_funct_ptr ge b =
375  match Pointers.block_region b with
376  | AST.XData -> Types.None
377  | AST.Code ->
378    (match Pointers.block_id b with
379     | Z.OZ -> Types.None
380     | Z.Pos x -> Types.None
381     | Z.Neg p -> PositiveMap.lookup_opt p ge.functions)
382
383(** val find_funct : 'a1 genv_t -> Values.val0 -> 'a1 Types.option **)
384let find_funct ge = function
385| Values.Vundef -> Types.None
386| Values.Vint (x, x0) -> Types.None
387| Values.Vnull -> Types.None
388| Values.Vptr ptr ->
389  (match Pointers.eq_offset ptr.Pointers.poff Pointers.zero_offset with
390   | Bool.True -> find_funct_ptr ge ptr.Pointers.pblock
391   | Bool.False -> Types.None)
392
393(** val symbol_for_block :
394    'a1 genv_t -> Pointers.block -> AST.ident Types.option **)
395let symbol_for_block genv b =
396  Types.option_map Types.fst
397    (Identifiers.find PreIdentifiers.SymbolTag genv.symbols (fun id b' ->
398      Pointers.eq_block b b'))
399
400(** val symbol_of_function_block :
401    'a1 genv_t -> Pointers.block -> AST.ident **)
402let symbol_of_function_block ge b =
403  (match symbol_for_block ge b with
404   | Types.None -> (fun _ -> assert false (* absurd case *))
405   | Types.Some id -> (fun _ -> id)) __
406
407(** val symbol_of_function_block' :
408    'a1 genv_t -> Pointers.block -> 'a1 -> AST.ident **)
409let symbol_of_function_block' ge b f =
410  symbol_of_function_block ge b
411
412(** val find_funct_ptr_id :
413    'a1 genv_t -> Pointers.block -> ('a1, AST.ident) Types.prod Types.option **)
414let find_funct_ptr_id ge b =
415  (match find_funct_ptr ge b with
416   | Types.None -> (fun _ -> Types.None)
417   | Types.Some f ->
418     (fun _ -> Types.Some { Types.fst = f; Types.snd =
419       (symbol_of_function_block' ge b f) })) __
420
421(** val opt_eq_from_res__o__ffpi_drop__o__inject :
422    Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __
423    Types.sig0 **)
424let opt_eq_from_res__o__ffpi_drop__o__inject x0 x2 x3 x4 x5 =
425  __
426
427(** val dpi1__o__opt_eq_from_res__o__ffpi_drop__o__inject :
428    Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> (__,
429    'a2) Types.dPair -> __ Types.sig0 **)
430let dpi1__o__opt_eq_from_res__o__ffpi_drop__o__inject x0 x2 x3 x4 x5 x8 =
431  __
432
433(** val eject__o__opt_eq_from_res__o__ffpi_drop__o__inject :
434    Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __
435    Types.sig0 -> __ Types.sig0 **)
436let eject__o__opt_eq_from_res__o__ffpi_drop__o__inject x0 x2 x3 x4 x5 x8 =
437  __
438
439(** val jmeq_to_eq__o__ffpi_drop__o__inject :
440    Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 **)
441let jmeq_to_eq__o__ffpi_drop__o__inject x1 x2 x3 x4 =
442  __
443
444(** val jmeq_to_eq__o__opt_eq_from_res__o__ffpi_drop__o__inject :
445    Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __
446    Types.sig0 **)
447let jmeq_to_eq__o__opt_eq_from_res__o__ffpi_drop__o__inject x0 x2 x3 x4 x5 =
448  __
449
450(** val dpi1__o__ffpi_drop__o__inject :
451    Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> (__, 'a2) Types.dPair
452    -> __ Types.sig0 **)
453let dpi1__o__ffpi_drop__o__inject x1 x2 x3 x4 x7 =
454  __
455
456(** val eject__o__ffpi_drop__o__inject :
457    Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 -> __
458    Types.sig0 **)
459let eject__o__ffpi_drop__o__inject x1 x2 x3 x4 x7 =
460  __
461
462(** val ffpi_drop__o__inject :
463    Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 **)
464let ffpi_drop__o__inject x1 x2 x3 x4 =
465  __
466
467(** val symbol_of_function_val : 'a1 genv_t -> Values.val0 -> AST.ident **)
468let symbol_of_function_val ge v =
469  (match v with
470   | Values.Vundef -> (fun _ -> assert false (* absurd case *))
471   | Values.Vint (x, x0) -> (fun _ -> assert false (* absurd case *))
472   | Values.Vnull -> (fun _ -> assert false (* absurd case *))
473   | Values.Vptr p ->
474     (fun _ -> symbol_of_function_block ge p.Pointers.pblock)) __
475
476(** val symbol_of_function_val' :
477    'a1 genv_t -> Values.val0 -> 'a1 -> AST.ident **)
478let symbol_of_function_val' ge v f =
479  symbol_of_function_val ge v
480
481(** val find_funct_id :
482    'a1 genv_t -> Values.val0 -> ('a1, AST.ident) Types.prod Types.option **)
483let find_funct_id ge v =
484  (match find_funct ge v with
485   | Types.None -> (fun _ -> Types.None)
486   | Types.Some f ->
487     (fun _ -> Types.Some { Types.fst = f; Types.snd =
488       (symbol_of_function_val' ge v f) })) __
489
490(** val opt_eq_from_res__o__ffi_drop__o__inject :
491    Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __
492    Types.sig0 **)
493let opt_eq_from_res__o__ffi_drop__o__inject x0 x2 x3 x4 x5 =
494  __
495
496(** val dpi1__o__opt_eq_from_res__o__ffi_drop__o__inject :
497    Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> (__,
498    'a2) Types.dPair -> __ Types.sig0 **)
499let dpi1__o__opt_eq_from_res__o__ffi_drop__o__inject x0 x2 x3 x4 x5 x8 =
500  __
501
502(** val eject__o__opt_eq_from_res__o__ffi_drop__o__inject :
503    Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __
504    Types.sig0 -> __ Types.sig0 **)
505let eject__o__opt_eq_from_res__o__ffi_drop__o__inject x0 x2 x3 x4 x5 x8 =
506  __
507
508(** val jmeq_to_eq__o__ffi_drop__o__inject :
509    Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 **)
510let jmeq_to_eq__o__ffi_drop__o__inject x1 x2 x3 x4 =
511  __
512
513(** val jmeq_to_eq__o__opt_eq_from_res__o__ffi_drop__o__inject :
514    Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __
515    Types.sig0 **)
516let jmeq_to_eq__o__opt_eq_from_res__o__ffi_drop__o__inject x0 x2 x3 x4 x5 =
517  __
518
519(** val dpi1__o__ffi_drop__o__inject :
520    Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> (__, 'a2) Types.dPair ->
521    __ Types.sig0 **)
522let dpi1__o__ffi_drop__o__inject x1 x2 x3 x4 x7 =
523  __
524
525(** val eject__o__ffi_drop__o__inject :
526    Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 -> __
527    Types.sig0 **)
528let eject__o__ffi_drop__o__inject x1 x2 x3 x4 x7 =
529  __
530
531(** val ffi_drop__o__inject :
532    Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 **)
533let ffi_drop__o__inject x1 x2 x3 x4 =
534  __
535
536(** val nat_plus_pos : Nat.nat -> Positive.pos -> Positive.pos **)
537let rec nat_plus_pos n p =
538  match n with
539  | Nat.O -> p
540  | Nat.S m -> Positive.succ (nat_plus_pos m p)
541
542(** val alloc_pair :
543    GenMem.mem -> GenMem.mem -> Z.z -> Z.z -> Z.z -> Z.z -> (GenMem.mem ->
544    GenMem.mem -> Pointers.block -> __ -> 'a1) -> 'a1 **)
545let alloc_pair clearme m' l h l' h' x =
546  (let { GenMem.blocks = ct; GenMem.nextblock = nx } = clearme in
547  (fun clearme0 ->
548  let { GenMem.blocks = ct'; GenMem.nextblock = nx' } = clearme0 in
549  (fun l0 h0 l'0 h'0 _ _ ->
550  Extralib.eq_rect_Type0_r nx' (fun _ h1 ->
551    h1 { GenMem.blocks =
552      (GenMem.update_block { GenMem.blocks = ct; GenMem.nextblock =
553        nx' }.GenMem.nextblock (GenMem.empty_block l0 h0) { GenMem.blocks =
554        ct; GenMem.nextblock = nx' }.GenMem.blocks); GenMem.nextblock =
555      (Z.zsucc { GenMem.blocks = ct; GenMem.nextblock =
556        nx' }.GenMem.nextblock) } { GenMem.blocks =
557      (GenMem.update_block { GenMem.blocks = ct'; GenMem.nextblock =
558        nx' }.GenMem.nextblock (GenMem.empty_block l'0 h'0) { GenMem.blocks =
559        ct'; GenMem.nextblock = nx' }.GenMem.blocks); GenMem.nextblock =
560      (Z.zsucc { GenMem.blocks = ct'; GenMem.nextblock =
561        nx' }.GenMem.nextblock) } { GenMem.blocks = ct; GenMem.nextblock =
562      nx' }.GenMem.nextblock __) nx __))) m' l h l' h' __ __ x
563
564(** val prod_jmdiscr :
565    ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod -> __ **)
566let prod_jmdiscr x y =
567  Logic.eq_rect_Type2 x
568    (let { Types.fst = a0; Types.snd = a10 } = x in
569    Obj.magic (fun _ dH -> dH __ __)) y
570
571(** val related_globals_rect_Type4 :
572    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
573    -> 'a3 **)
574let rec related_globals_rect_Type4 t ge ge' h_mk_related_globals =
575  h_mk_related_globals __ __ __ __
576
577(** val related_globals_rect_Type5 :
578    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
579    -> 'a3 **)
580let rec related_globals_rect_Type5 t ge ge' h_mk_related_globals =
581  h_mk_related_globals __ __ __ __
582
583(** val related_globals_rect_Type3 :
584    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
585    -> 'a3 **)
586let rec related_globals_rect_Type3 t ge ge' h_mk_related_globals =
587  h_mk_related_globals __ __ __ __
588
589(** val related_globals_rect_Type2 :
590    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
591    -> 'a3 **)
592let rec related_globals_rect_Type2 t ge ge' h_mk_related_globals =
593  h_mk_related_globals __ __ __ __
594
595(** val related_globals_rect_Type1 :
596    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
597    -> 'a3 **)
598let rec related_globals_rect_Type1 t ge ge' h_mk_related_globals =
599  h_mk_related_globals __ __ __ __
600
601(** val related_globals_rect_Type0 :
602    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
603    -> 'a3 **)
604let rec related_globals_rect_Type0 t ge ge' h_mk_related_globals =
605  h_mk_related_globals __ __ __ __
606
607(** val related_globals_inv_rect_Type4 :
608    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
609    -> 'a3) -> 'a3 **)
610let related_globals_inv_rect_Type4 x3 x4 x5 h1 =
611  let hcut = related_globals_rect_Type4 x3 x4 x5 h1 in hcut __
612
613(** val related_globals_inv_rect_Type3 :
614    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
615    -> 'a3) -> 'a3 **)
616let related_globals_inv_rect_Type3 x3 x4 x5 h1 =
617  let hcut = related_globals_rect_Type3 x3 x4 x5 h1 in hcut __
618
619(** val related_globals_inv_rect_Type2 :
620    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
621    -> 'a3) -> 'a3 **)
622let related_globals_inv_rect_Type2 x3 x4 x5 h1 =
623  let hcut = related_globals_rect_Type2 x3 x4 x5 h1 in hcut __
624
625(** val related_globals_inv_rect_Type1 :
626    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
627    -> 'a3) -> 'a3 **)
628let related_globals_inv_rect_Type1 x3 x4 x5 h1 =
629  let hcut = related_globals_rect_Type1 x3 x4 x5 h1 in hcut __
630
631(** val related_globals_inv_rect_Type0 :
632    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
633    -> 'a3) -> 'a3 **)
634let related_globals_inv_rect_Type0 x3 x4 x5 h1 =
635  let hcut = related_globals_rect_Type0 x3 x4 x5 h1 in hcut __
636
637(** val related_globals_discr :
638    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
639let related_globals_discr a3 a4 a5 =
640  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __
641
642(** val related_globals_jmdiscr :
643    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
644let related_globals_jmdiscr a3 a4 a5 =
645  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __
646
647(** val related_globals_gen_rect_Type4 :
648    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
649    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
650    __ -> __ -> __ -> 'a3) -> 'a3 **)
651let rec related_globals_gen_rect_Type4 tag t ge ge' h_mk_related_globals_gen =
652  h_mk_related_globals_gen __ __ __ __
653
654(** val related_globals_gen_rect_Type5 :
655    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
656    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
657    __ -> __ -> __ -> 'a3) -> 'a3 **)
658let rec related_globals_gen_rect_Type5 tag t ge ge' h_mk_related_globals_gen =
659  h_mk_related_globals_gen __ __ __ __
660
661(** val related_globals_gen_rect_Type3 :
662    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
663    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
664    __ -> __ -> __ -> 'a3) -> 'a3 **)
665let rec related_globals_gen_rect_Type3 tag t ge ge' h_mk_related_globals_gen =
666  h_mk_related_globals_gen __ __ __ __
667
668(** val related_globals_gen_rect_Type2 :
669    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
670    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
671    __ -> __ -> __ -> 'a3) -> 'a3 **)
672let rec related_globals_gen_rect_Type2 tag t ge ge' h_mk_related_globals_gen =
673  h_mk_related_globals_gen __ __ __ __
674
675(** val related_globals_gen_rect_Type1 :
676    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
677    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
678    __ -> __ -> __ -> 'a3) -> 'a3 **)
679let rec related_globals_gen_rect_Type1 tag t ge ge' h_mk_related_globals_gen =
680  h_mk_related_globals_gen __ __ __ __
681
682(** val related_globals_gen_rect_Type0 :
683    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
684    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
685    __ -> __ -> __ -> 'a3) -> 'a3 **)
686let rec related_globals_gen_rect_Type0 tag t ge ge' h_mk_related_globals_gen =
687  h_mk_related_globals_gen __ __ __ __
688
689(** val related_globals_gen_inv_rect_Type4 :
690    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
691    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
692    __ -> __ -> __ -> __ -> 'a3) -> 'a3 **)
693let related_globals_gen_inv_rect_Type4 x1 x4 x5 x6 h1 =
694  let hcut = related_globals_gen_rect_Type4 x1 x4 x5 x6 h1 in hcut __
695
696(** val related_globals_gen_inv_rect_Type3 :
697    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
698    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
699    __ -> __ -> __ -> __ -> 'a3) -> 'a3 **)
700let related_globals_gen_inv_rect_Type3 x1 x4 x5 x6 h1 =
701  let hcut = related_globals_gen_rect_Type3 x1 x4 x5 x6 h1 in hcut __
702
703(** val related_globals_gen_inv_rect_Type2 :
704    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
705    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
706    __ -> __ -> __ -> __ -> 'a3) -> 'a3 **)
707let related_globals_gen_inv_rect_Type2 x1 x4 x5 x6 h1 =
708  let hcut = related_globals_gen_rect_Type2 x1 x4 x5 x6 h1 in hcut __
709
710(** val related_globals_gen_inv_rect_Type1 :
711    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
712    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
713    __ -> __ -> __ -> __ -> 'a3) -> 'a3 **)
714let related_globals_gen_inv_rect_Type1 x1 x4 x5 x6 h1 =
715  let hcut = related_globals_gen_rect_Type1 x1 x4 x5 x6 h1 in hcut __
716
717(** val related_globals_gen_inv_rect_Type0 :
718    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
719    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
720    __ -> __ -> __ -> __ -> 'a3) -> 'a3 **)
721let related_globals_gen_inv_rect_Type0 x1 x4 x5 x6 h1 =
722  let hcut = related_globals_gen_rect_Type0 x1 x4 x5 x6 h1 in hcut __
723
724(** val related_globals_gen_discr :
725    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
726    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
727let related_globals_gen_discr a1 a4 a5 a6 =
728  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __
729
730(** val related_globals_gen_jmdiscr :
731    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
732    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
733let related_globals_gen_jmdiscr a1 a4 a5 a6 =
734  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __
735
736open Extra_bool
737
Note: See TracBrowser for help on using the repository browser.