27 open Hints_declaration
93 type 'f genv_t = { functions : 'f PositiveMap.positive_map;
94 nextfunction : Positive.pos;
95 symbols : Pointers.block Identifiers.identifier_map }
97 (** val genv_t_rect_Type4 :
98 ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
99 Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
100 let rec genv_t_rect_Type4 h_mk_genv_t x_6621 =
101 let { functions = functions0; nextfunction = nextfunction0; symbols =
104 h_mk_genv_t functions0 nextfunction0 symbols0 __
106 (** val genv_t_rect_Type5 :
107 ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
108 Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
109 let rec genv_t_rect_Type5 h_mk_genv_t x_6623 =
110 let { functions = functions0; nextfunction = nextfunction0; symbols =
113 h_mk_genv_t functions0 nextfunction0 symbols0 __
115 (** val genv_t_rect_Type3 :
116 ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
117 Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
118 let rec genv_t_rect_Type3 h_mk_genv_t x_6625 =
119 let { functions = functions0; nextfunction = nextfunction0; symbols =
122 h_mk_genv_t functions0 nextfunction0 symbols0 __
124 (** val genv_t_rect_Type2 :
125 ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
126 Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
127 let rec genv_t_rect_Type2 h_mk_genv_t x_6627 =
128 let { functions = functions0; nextfunction = nextfunction0; symbols =
131 h_mk_genv_t functions0 nextfunction0 symbols0 __
133 (** val genv_t_rect_Type1 :
134 ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
135 Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
136 let rec genv_t_rect_Type1 h_mk_genv_t x_6629 =
137 let { functions = functions0; nextfunction = nextfunction0; symbols =
140 h_mk_genv_t functions0 nextfunction0 symbols0 __
142 (** val genv_t_rect_Type0 :
143 ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
144 Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
145 let rec genv_t_rect_Type0 h_mk_genv_t x_6631 =
146 let { functions = functions0; nextfunction = nextfunction0; symbols =
149 h_mk_genv_t functions0 nextfunction0 symbols0 __
151 (** val functions : 'a1 genv_t -> 'a1 PositiveMap.positive_map **)
152 let rec functions xxx =
155 (** val nextfunction : 'a1 genv_t -> Positive.pos **)
156 let rec nextfunction xxx =
159 (** val symbols : 'a1 genv_t -> Pointers.block Identifiers.identifier_map **)
160 let rec symbols xxx =
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 **)
166 let genv_t_inv_rect_Type4 hterm h1 =
167 let hcut = genv_t_rect_Type4 h1 hterm in hcut __
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 **)
172 let genv_t_inv_rect_Type3 hterm h1 =
173 let hcut = genv_t_rect_Type3 h1 hterm in hcut __
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 **)
178 let genv_t_inv_rect_Type2 hterm h1 =
179 let hcut = genv_t_rect_Type2 h1 hterm in hcut __
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 **)
184 let genv_t_inv_rect_Type1 hterm h1 =
185 let hcut = genv_t_rect_Type1 h1 hterm in hcut __
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 **)
190 let genv_t_inv_rect_Type0 hterm h1 =
191 let hcut = genv_t_rect_Type0 h1 hterm in hcut __
193 (** val genv_t_discr : 'a1 genv_t -> 'a1 genv_t -> __ **)
194 let 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
199 (** val genv_t_jmdiscr : 'a1 genv_t -> 'a1 genv_t -> __ **)
200 let 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
205 (** val drop_fn : AST.ident -> 'a1 genv_t -> 'a1 genv_t **)
208 match Identifiers.lookup PreIdentifiers.SymbolTag g.symbols id with
209 | Types.None -> g.functions
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)
216 { functions = fns; nextfunction = g.nextfunction; symbols =
217 (Identifiers.remove PreIdentifiers.SymbolTag g.symbols id) }
220 (AST.ident, 'a1) Types.prod -> 'a1 genv_t -> 'a1 genv_t **)
221 let 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) }
230 AST.ident -> Pointers.block -> 'a1 genv_t -> 'a1 genv_t **)
231 let 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) }
236 (** val empty_mem : GenMem.mem **)
240 (** val empty : 'a1 genv_t **)
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) }
247 'a1 genv_t -> (AST.ident, 'a1) Types.prod List.list -> 'a1 genv_t **)
248 let add_functs init fns =
249 List.foldr add_funct init fns
251 (** val find_symbol :
252 'a1 genv_t -> AST.ident -> Pointers.block Types.option **)
254 Identifiers.lookup PreIdentifiers.SymbolTag ge.symbols
256 (** val store_init_data :
257 'a1 genv_t -> GenMem.mem -> Pointers.block -> Z.z -> AST.init_data ->
258 GenMem.mem Types.option **)
259 let 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) }
265 FrontEndMem.store (AST.ASTint (AST.I8, AST.Unsigned)) m ptr (Values.Vint
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
279 FrontEndMem.store AST.ASTptr m ptr (Values.Vptr { Pointers.pblock =
281 (Pointers.shift_offset (AST.bitsize_of_intsize AST.I16)
282 Pointers.zero_offset (AST.repr AST.I16 ofs)) })))
284 (** val size_init_data : AST.init_data -> Nat.nat **)
285 let 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
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 **)
296 let 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
302 store_init_data_list ge m' b
303 (Z.zplus p (Z.z_of_nat (size_init_data id))) idl')
305 (** val size_init_data_list : AST.init_data List.list -> Nat.nat **)
306 let size_init_data_list i_data =
307 List.foldr (fun i_data0 sz -> Nat.plus (size_init_data i_data0) sz) Nat.O
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 **)
314 let 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))
323 let g' = add_symbol id b g in { Types.fst = g'; Types.snd = st' })
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 **)
330 let 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
336 (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic st) (fun st0 ->
337 match find_symbol g id with
339 Obj.magic (Errors.Error
340 (Errors.msg ErrorMessages.InitDataStoreFailed))
343 (Errors.opt_to_res (Errors.msg ErrorMessages.InitDataStoreFailed)
344 (store_init_data_list g st0 b Z.OZ init))))) (Errors.OK m) vars
346 (** val globalenv_allocmem :
347 ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> ('a1
348 genv_t, GenMem.mem) Types.prod **)
349 let 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
354 ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> 'a1 genv_t **)
356 (globalenv_allocmem i p).Types.fst
358 (** val globalenv_noinit : ('a1, Nat.nat) AST.program -> 'a1 genv_t **)
359 let globalenv_noinit p =
360 globalenv (fun n -> List.Cons ((AST.Init_space n), List.Nil)) p
363 ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> GenMem.mem
366 let { Types.fst = g; Types.snd = m } = globalenv_allocmem i p in
367 init_globals i g m p.AST.prog_vars
369 (** val alloc_mem : ('a1, Nat.nat) AST.program -> GenMem.mem **)
371 (globalenv_allocmem (fun n -> List.Cons ((AST.Init_space n), List.Nil)) p).Types.snd
373 (** val find_funct_ptr : 'a1 genv_t -> Pointers.block -> 'a1 Types.option **)
374 let find_funct_ptr ge b =
375 match Pointers.block_region b with
376 | AST.XData -> Types.None
378 (match Pointers.block_id b with
380 | Z.Pos x -> Types.None
381 | Z.Neg p -> PositiveMap.lookup_opt p ge.functions)
383 (** val find_funct : 'a1 genv_t -> Values.val0 -> 'a1 Types.option **)
384 let find_funct ge = function
385 | Values.Vundef -> Types.None
386 | Values.Vint (x, x0) -> Types.None
387 | Values.Vnull -> Types.None
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)
393 (** val symbol_for_block :
394 'a1 genv_t -> Pointers.block -> AST.ident Types.option **)
395 let 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'))
400 (** val symbol_of_function_block :
401 'a1 genv_t -> Pointers.block -> AST.ident **)
402 let 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)) __
407 (** val symbol_of_function_block' :
408 'a1 genv_t -> Pointers.block -> 'a1 -> AST.ident **)
409 let symbol_of_function_block' ge b f =
410 symbol_of_function_block ge b
412 (** val find_funct_ptr_id :
413 'a1 genv_t -> Pointers.block -> ('a1, AST.ident) Types.prod Types.option **)
414 let find_funct_ptr_id ge b =
415 (match find_funct_ptr ge b with
416 | Types.None -> (fun _ -> Types.None)
418 (fun _ -> Types.Some { Types.fst = f; Types.snd =
419 (symbol_of_function_block' ge b f) })) __
421 (** val opt_eq_from_res__o__ffpi_drop__o__inject :
422 Errors.errmsg -> Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __
424 let opt_eq_from_res__o__ffpi_drop__o__inject x0 x2 x3 x4 x5 =
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 **)
430 let dpi1__o__opt_eq_from_res__o__ffpi_drop__o__inject x0 x2 x3 x4 x5 x8 =
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 **)
436 let eject__o__opt_eq_from_res__o__ffpi_drop__o__inject x0 x2 x3 x4 x5 x8 =
439 (** val jmeq_to_eq__o__ffpi_drop__o__inject :
440 Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 **)
441 let jmeq_to_eq__o__ffpi_drop__o__inject x1 x2 x3 x4 =
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 -> __
447 let jmeq_to_eq__o__opt_eq_from_res__o__ffpi_drop__o__inject x0 x2 x3 x4 x5 =
450 (** val dpi1__o__ffpi_drop__o__inject :
451 Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> (__, 'a2) Types.dPair
453 let dpi1__o__ffpi_drop__o__inject x1 x2 x3 x4 x7 =
456 (** val eject__o__ffpi_drop__o__inject :
457 Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 -> __
459 let eject__o__ffpi_drop__o__inject x1 x2 x3 x4 x7 =
462 (** val ffpi_drop__o__inject :
463 Pointers.block -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 **)
464 let ffpi_drop__o__inject x1 x2 x3 x4 =
467 (** val symbol_of_function_val : 'a1 genv_t -> Values.val0 -> AST.ident **)
468 let symbol_of_function_val ge v =
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 *))
474 (fun _ -> symbol_of_function_block ge p.Pointers.pblock)) __
476 (** val symbol_of_function_val' :
477 'a1 genv_t -> Values.val0 -> 'a1 -> AST.ident **)
478 let symbol_of_function_val' ge v f =
479 symbol_of_function_val ge v
481 (** val find_funct_id :
482 'a1 genv_t -> Values.val0 -> ('a1, AST.ident) Types.prod Types.option **)
483 let find_funct_id ge v =
484 (match find_funct ge v with
485 | Types.None -> (fun _ -> Types.None)
487 (fun _ -> Types.Some { Types.fst = f; Types.snd =
488 (symbol_of_function_val' ge v f) })) __
490 (** val opt_eq_from_res__o__ffi_drop__o__inject :
491 Errors.errmsg -> Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __
493 let opt_eq_from_res__o__ffi_drop__o__inject x0 x2 x3 x4 x5 =
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 **)
499 let dpi1__o__opt_eq_from_res__o__ffi_drop__o__inject x0 x2 x3 x4 x5 x8 =
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 **)
505 let eject__o__opt_eq_from_res__o__ffi_drop__o__inject x0 x2 x3 x4 x5 x8 =
508 (** val jmeq_to_eq__o__ffi_drop__o__inject :
509 Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 **)
510 let jmeq_to_eq__o__ffi_drop__o__inject x1 x2 x3 x4 =
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 -> __
516 let jmeq_to_eq__o__opt_eq_from_res__o__ffi_drop__o__inject x0 x2 x3 x4 x5 =
519 (** val dpi1__o__ffi_drop__o__inject :
520 Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> (__, 'a2) Types.dPair ->
522 let dpi1__o__ffi_drop__o__inject x1 x2 x3 x4 x7 =
525 (** val eject__o__ffi_drop__o__inject :
526 Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 -> __
528 let eject__o__ffi_drop__o__inject x1 x2 x3 x4 x7 =
531 (** val ffi_drop__o__inject :
532 Values.val0 -> AST.ident -> 'a1 genv_t -> 'a1 -> __ Types.sig0 **)
533 let ffi_drop__o__inject x1 x2 x3 x4 =
536 (** val nat_plus_pos : Nat.nat -> Positive.pos -> Positive.pos **)
537 let rec nat_plus_pos n p =
540 | Nat.S m -> Positive.succ (nat_plus_pos m p)
543 GenMem.mem -> GenMem.mem -> Z.z -> Z.z -> Z.z -> Z.z -> (GenMem.mem ->
544 GenMem.mem -> Pointers.block -> __ -> 'a1) -> 'a1 **)
545 let alloc_pair clearme m' l h l' h' x =
546 (let { GenMem.blocks = ct; GenMem.nextblock = nx } = clearme in
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 ->
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
564 (** val prod_jmdiscr :
565 ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod -> __ **)
566 let 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
571 (** val related_globals_rect_Type4 :
572 ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
574 let rec related_globals_rect_Type4 t ge ge' h_mk_related_globals =
575 h_mk_related_globals __ __ __ __
577 (** val related_globals_rect_Type5 :
578 ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
580 let rec related_globals_rect_Type5 t ge ge' h_mk_related_globals =
581 h_mk_related_globals __ __ __ __
583 (** val related_globals_rect_Type3 :
584 ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
586 let rec related_globals_rect_Type3 t ge ge' h_mk_related_globals =
587 h_mk_related_globals __ __ __ __
589 (** val related_globals_rect_Type2 :
590 ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
592 let rec related_globals_rect_Type2 t ge ge' h_mk_related_globals =
593 h_mk_related_globals __ __ __ __
595 (** val related_globals_rect_Type1 :
596 ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
598 let rec related_globals_rect_Type1 t ge ge' h_mk_related_globals =
599 h_mk_related_globals __ __ __ __
601 (** val related_globals_rect_Type0 :
602 ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
604 let rec related_globals_rect_Type0 t ge ge' h_mk_related_globals =
605 h_mk_related_globals __ __ __ __
607 (** val related_globals_inv_rect_Type4 :
608 ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
610 let related_globals_inv_rect_Type4 x3 x4 x5 h1 =
611 let hcut = related_globals_rect_Type4 x3 x4 x5 h1 in hcut __
613 (** val related_globals_inv_rect_Type3 :
614 ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
616 let related_globals_inv_rect_Type3 x3 x4 x5 h1 =
617 let hcut = related_globals_rect_Type3 x3 x4 x5 h1 in hcut __
619 (** val related_globals_inv_rect_Type2 :
620 ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
622 let related_globals_inv_rect_Type2 x3 x4 x5 h1 =
623 let hcut = related_globals_rect_Type2 x3 x4 x5 h1 in hcut __
625 (** val related_globals_inv_rect_Type1 :
626 ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
628 let related_globals_inv_rect_Type1 x3 x4 x5 h1 =
629 let hcut = related_globals_rect_Type1 x3 x4 x5 h1 in hcut __
631 (** val related_globals_inv_rect_Type0 :
632 ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
634 let related_globals_inv_rect_Type0 x3 x4 x5 h1 =
635 let hcut = related_globals_rect_Type0 x3 x4 x5 h1 in hcut __
637 (** val related_globals_discr :
638 ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
639 let related_globals_discr a3 a4 a5 =
640 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __
642 (** val related_globals_jmdiscr :
643 ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
644 let related_globals_jmdiscr a3 a4 a5 =
645 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __
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 **)
651 let rec related_globals_gen_rect_Type4 tag t ge ge' h_mk_related_globals_gen =
652 h_mk_related_globals_gen __ __ __ __
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 **)
658 let rec related_globals_gen_rect_Type5 tag t ge ge' h_mk_related_globals_gen =
659 h_mk_related_globals_gen __ __ __ __
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 **)
665 let rec related_globals_gen_rect_Type3 tag t ge ge' h_mk_related_globals_gen =
666 h_mk_related_globals_gen __ __ __ __
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 **)
672 let rec related_globals_gen_rect_Type2 tag t ge ge' h_mk_related_globals_gen =
673 h_mk_related_globals_gen __ __ __ __
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 **)
679 let rec related_globals_gen_rect_Type1 tag t ge ge' h_mk_related_globals_gen =
680 h_mk_related_globals_gen __ __ __ __
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 **)
686 let rec related_globals_gen_rect_Type0 tag t ge ge' h_mk_related_globals_gen =
687 h_mk_related_globals_gen __ __ __ __
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 **)
693 let 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 __
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 **)
700 let 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 __
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 **)
707 let 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 __
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 **)
714 let 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 __
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 **)
721 let 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 __
724 (** val related_globals_gen_discr :
725 PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
726 Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
727 let related_globals_gen_discr a1 a4 a5 a6 =
728 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __
730 (** val related_globals_gen_jmdiscr :
731 PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
732 Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
733 let related_globals_gen_jmdiscr a1 a4 a5 a6 =
734 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __