open Preamble open Extra_bool open Coqlib open Values open FrontEndVal open Hide open ByteValues open Division open Z open BitVectorZ open Pointers open GenMem open FrontEndMem open Proper open PositiveMap open Deqsets open Extralib open Lists open Identifiers open Exp open Arithmetic open Vector open Div_and_mod open Util open FoldStuff open BitVector open Extranat open Integers open AST open ErrorMessages open Option open Setoids open Monad open Jmeq open Russell open Positive open PreIdentifiers open Bool open Relations open Nat open List open Hints_declaration open Core_notation open Pts open Logic open Types open Errors open Globalenvs open CostLabel open Events open IOMonad open IO open BEMem open String open Sets open Listb open LabelledObjects open BitVectorTrie open Graphs open I8051 open Order open Registers open BackEndOps open Joint open I8051bis open ExtraGlobalenvs type 'f genv_gen = { ge : 'f AST.fundef Globalenvs.genv_t; stack_sizes : (AST.ident -> Nat.nat Types.option); premain : 'f; pc_from_label : (Pointers.block Types.sig0 -> 'f -> Graphs.label -> ByteValues.program_counter Types.option) } (** val genv_gen_rect_Type4 : AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> 'a2) -> 'a1 genv_gen -> 'a2 **) let rec genv_gen_rect_Type4 globals h_mk_genv_gen x_24476 = let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0; pc_from_label = pc_from_label0 } = x_24476 in h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0 (** val genv_gen_rect_Type5 : AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> 'a2) -> 'a1 genv_gen -> 'a2 **) let rec genv_gen_rect_Type5 globals h_mk_genv_gen x_24478 = let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0; pc_from_label = pc_from_label0 } = x_24478 in h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0 (** val genv_gen_rect_Type3 : AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> 'a2) -> 'a1 genv_gen -> 'a2 **) let rec genv_gen_rect_Type3 globals h_mk_genv_gen x_24480 = let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0; pc_from_label = pc_from_label0 } = x_24480 in h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0 (** val genv_gen_rect_Type2 : AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> 'a2) -> 'a1 genv_gen -> 'a2 **) let rec genv_gen_rect_Type2 globals h_mk_genv_gen x_24482 = let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0; pc_from_label = pc_from_label0 } = x_24482 in h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0 (** val genv_gen_rect_Type1 : AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> 'a2) -> 'a1 genv_gen -> 'a2 **) let rec genv_gen_rect_Type1 globals h_mk_genv_gen x_24484 = let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0; pc_from_label = pc_from_label0 } = x_24484 in h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0 (** val genv_gen_rect_Type0 : AST.ident List.list -> ('a1 AST.fundef Globalenvs.genv_t -> __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> 'a2) -> 'a1 genv_gen -> 'a2 **) let rec genv_gen_rect_Type0 globals h_mk_genv_gen x_24486 = let { ge = ge0; stack_sizes = stack_sizes0; premain = premain0; pc_from_label = pc_from_label0 } = x_24486 in h_mk_genv_gen ge0 __ stack_sizes0 premain0 pc_from_label0 (** val ge : AST.ident List.list -> 'a1 genv_gen -> 'a1 AST.fundef Globalenvs.genv_t **) let rec ge globals xxx = xxx.ge (** val stack_sizes : AST.ident List.list -> 'a1 genv_gen -> AST.ident -> Nat.nat Types.option **) let rec stack_sizes globals xxx = xxx.stack_sizes (** val premain : AST.ident List.list -> 'a1 genv_gen -> 'a1 **) let rec premain globals xxx = xxx.premain (** val pc_from_label : AST.ident List.list -> 'a1 genv_gen -> Pointers.block Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option **) let rec pc_from_label globals xxx = xxx.pc_from_label (** val genv_gen_inv_rect_Type4 : AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t -> __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> __ -> 'a2) -> 'a2 **) let genv_gen_inv_rect_Type4 x2 hterm h1 = let hcut = genv_gen_rect_Type4 x2 h1 hterm in hcut __ (** val genv_gen_inv_rect_Type3 : AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t -> __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> __ -> 'a2) -> 'a2 **) let genv_gen_inv_rect_Type3 x2 hterm h1 = let hcut = genv_gen_rect_Type3 x2 h1 hterm in hcut __ (** val genv_gen_inv_rect_Type2 : AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t -> __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> __ -> 'a2) -> 'a2 **) let genv_gen_inv_rect_Type2 x2 hterm h1 = let hcut = genv_gen_rect_Type2 x2 h1 hterm in hcut __ (** val genv_gen_inv_rect_Type1 : AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t -> __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> __ -> 'a2) -> 'a2 **) let genv_gen_inv_rect_Type1 x2 hterm h1 = let hcut = genv_gen_rect_Type1 x2 h1 hterm in hcut __ (** val genv_gen_inv_rect_Type0 : AST.ident List.list -> 'a1 genv_gen -> ('a1 AST.fundef Globalenvs.genv_t -> __ -> (AST.ident -> Nat.nat Types.option) -> 'a1 -> (Pointers.block Types.sig0 -> 'a1 -> Graphs.label -> ByteValues.program_counter Types.option) -> __ -> 'a2) -> 'a2 **) let genv_gen_inv_rect_Type0 x2 hterm h1 = let hcut = genv_gen_rect_Type0 x2 h1 hterm in hcut __ (** val genv_gen_discr : AST.ident List.list -> 'a1 genv_gen -> 'a1 genv_gen -> __ **) let genv_gen_discr a2 x y = Logic.eq_rect_Type2 x (let { ge = a0; stack_sizes = a20; premain = a3; pc_from_label = a4 } = x in Obj.magic (fun _ dH -> dH __ __ __ __ __)) y (** val genv_gen_jmdiscr : AST.ident List.list -> 'a1 genv_gen -> 'a1 genv_gen -> __ **) let genv_gen_jmdiscr a2 x y = Logic.eq_rect_Type2 x (let { ge = a0; stack_sizes = a20; premain = a3; pc_from_label = a4 } = x in Obj.magic (fun _ dH -> dH __ __ __ __ __)) y (** val dpi1__o__ge__o__inject : AST.ident List.list -> ('a1 genv_gen, 'a2) Types.dPair -> 'a1 AST.fundef Globalenvs.genv_t Types.sig0 **) let dpi1__o__ge__o__inject x1 x4 = x4.Types.dpi1.ge (** val eject__o__ge__o__inject : AST.ident List.list -> 'a1 genv_gen Types.sig0 -> 'a1 AST.fundef Globalenvs.genv_t Types.sig0 **) let eject__o__ge__o__inject x1 x4 = (Types.pi1 x4).ge (** val ge__o__inject : AST.ident List.list -> 'a1 genv_gen -> 'a1 AST.fundef Globalenvs.genv_t Types.sig0 **) let ge__o__inject x1 x3 = x3.ge (** val dpi1__o__ge : AST.ident List.list -> ('a1 genv_gen, 'a2) Types.dPair -> 'a1 AST.fundef Globalenvs.genv_t **) let dpi1__o__ge x1 x3 = x3.Types.dpi1.ge (** val eject__o__ge : AST.ident List.list -> 'a1 genv_gen Types.sig0 -> 'a1 AST.fundef Globalenvs.genv_t **) let eject__o__ge x1 x3 = (Types.pi1 x3).ge (** val pre_main_id : AST.ident **) let pre_main_id = Positive.One (** val fetch_function : AST.ident List.list -> 'a1 genv_gen -> Pointers.block Types.sig0 -> (AST.ident, 'a1 AST.fundef) Types.prod Errors.res **) let fetch_function g ge0 bl = match Z.eqZb (Pointers.block_id (Types.pi1 bl)) (Z.zopp (Z.z_of_nat (Nat.S Nat.O))) with | Bool.True -> Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = pre_main_id; Types.snd = (AST.Internal ge0.premain) }) | Bool.False -> Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction), List.Nil)) (Obj.magic (Monad.m_bind0 (Monad.max_def Option.option) (Obj.magic (Globalenvs.symbol_for_block ge0.ge (Types.pi1 bl))) (fun id -> Monad.m_bind0 (Monad.max_def Option.option) (Obj.magic (Globalenvs.find_funct_ptr ge0.ge (Types.pi1 bl))) (fun fd -> Monad.m_return0 (Monad.max_def Option.option) { Types.fst = id; Types.snd = fd })))) (** val fetch_internal_function : AST.ident List.list -> 'a1 genv_gen -> Pointers.block Types.sig0 -> (AST.ident, 'a1) Types.prod Errors.res **) let fetch_internal_function g ge0 bl = Obj.magic (Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic (fetch_function g ge0 bl)) (fun id fd -> match fd with | AST.Internal ifd -> Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = id; Types.snd = ifd } | AST.External x -> Obj.magic (Errors.Error (List.Cons ((Errors.MSG ErrorMessages.BadFunction), List.Nil))))) (** val code_block_of_block : Pointers.block -> Pointers.block Types.sig0 Types.option **) let code_block_of_block bl = (match Pointers.block_region bl with | AST.XData -> (fun _ -> Types.None) | AST.Code -> (fun _ -> Types.Some bl)) __ (** val block_of_funct_id : 'a1 Globalenvs.genv_t -> PreIdentifiers.identifier -> Pointers.block Types.sig0 Errors.res **) let block_of_funct_id ge0 id = Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction), (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil)))) (Obj.magic (Monad.m_bind0 (Monad.max_def Option.option) (Obj.magic (Globalenvs.find_symbol ge0 id)) (fun bl -> Obj.magic (code_block_of_block bl)))) (** val gen_pc_from_label : AST.ident List.list -> 'a1 genv_gen -> AST.ident -> Graphs.label -> ByteValues.program_counter Errors.res **) let gen_pc_from_label g ge0 id lbl = Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (block_of_funct_id ge0.ge id)) (fun bl -> Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic (fetch_internal_function g ge0 bl)) (fun ignore f_def -> Obj.magic (Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.LabelNotFound), (List.Cons ((Errors.CTX (PreIdentifiers.LabelTag, lbl)), List.Nil)))) (ge0.pc_from_label bl f_def lbl))))) type genv = Joint.joint_closed_internal_function genv_gen type sem_state_params = { empty_framesT : __; empty_regsT : (ByteValues.xpointer -> __); load_sp : (__ -> ByteValues.xpointer Errors.res); save_sp : (__ -> ByteValues.xpointer -> __) } (** val sem_state_params_rect_Type4 : (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) -> 'a1) -> sem_state_params -> 'a1 **) let rec sem_state_params_rect_Type4 h_mk_sem_state_params x_24507 = let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp = load_sp0; save_sp = save_sp0 } = x_24507 in h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0 (** val sem_state_params_rect_Type5 : (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) -> 'a1) -> sem_state_params -> 'a1 **) let rec sem_state_params_rect_Type5 h_mk_sem_state_params x_24509 = let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp = load_sp0; save_sp = save_sp0 } = x_24509 in h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0 (** val sem_state_params_rect_Type3 : (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) -> 'a1) -> sem_state_params -> 'a1 **) let rec sem_state_params_rect_Type3 h_mk_sem_state_params x_24511 = let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp = load_sp0; save_sp = save_sp0 } = x_24511 in h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0 (** val sem_state_params_rect_Type2 : (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) -> 'a1) -> sem_state_params -> 'a1 **) let rec sem_state_params_rect_Type2 h_mk_sem_state_params x_24513 = let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp = load_sp0; save_sp = save_sp0 } = x_24513 in h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0 (** val sem_state_params_rect_Type1 : (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) -> 'a1) -> sem_state_params -> 'a1 **) let rec sem_state_params_rect_Type1 h_mk_sem_state_params x_24515 = let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp = load_sp0; save_sp = save_sp0 } = x_24515 in h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0 (** val sem_state_params_rect_Type0 : (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) -> 'a1) -> sem_state_params -> 'a1 **) let rec sem_state_params_rect_Type0 h_mk_sem_state_params x_24517 = let { empty_framesT = empty_framesT0; empty_regsT = empty_regsT0; load_sp = load_sp0; save_sp = save_sp0 } = x_24517 in h_mk_sem_state_params __ empty_framesT0 __ empty_regsT0 load_sp0 save_sp0 type framesT = __ (** val empty_framesT : sem_state_params -> __ **) let rec empty_framesT xxx = xxx.empty_framesT type regsT = __ (** val empty_regsT : sem_state_params -> ByteValues.xpointer -> __ **) let rec empty_regsT xxx = xxx.empty_regsT (** val load_sp : sem_state_params -> __ -> ByteValues.xpointer Errors.res **) let rec load_sp xxx = xxx.load_sp (** val save_sp : sem_state_params -> __ -> ByteValues.xpointer -> __ **) let rec save_sp xxx = xxx.save_sp (** val sem_state_params_inv_rect_Type4 : sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) -> __ -> 'a1) -> 'a1 **) let sem_state_params_inv_rect_Type4 hterm h1 = let hcut = sem_state_params_rect_Type4 h1 hterm in hcut __ (** val sem_state_params_inv_rect_Type3 : sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) -> __ -> 'a1) -> 'a1 **) let sem_state_params_inv_rect_Type3 hterm h1 = let hcut = sem_state_params_rect_Type3 h1 hterm in hcut __ (** val sem_state_params_inv_rect_Type2 : sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) -> __ -> 'a1) -> 'a1 **) let sem_state_params_inv_rect_Type2 hterm h1 = let hcut = sem_state_params_rect_Type2 h1 hterm in hcut __ (** val sem_state_params_inv_rect_Type1 : sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) -> __ -> 'a1) -> 'a1 **) let sem_state_params_inv_rect_Type1 hterm h1 = let hcut = sem_state_params_rect_Type1 h1 hterm in hcut __ (** val sem_state_params_inv_rect_Type0 : sem_state_params -> (__ -> __ -> __ -> (ByteValues.xpointer -> __) -> (__ -> ByteValues.xpointer Errors.res) -> (__ -> ByteValues.xpointer -> __) -> __ -> 'a1) -> 'a1 **) let sem_state_params_inv_rect_Type0 hterm h1 = let hcut = sem_state_params_rect_Type0 h1 hterm in hcut __ (** val sem_state_params_jmdiscr : sem_state_params -> sem_state_params -> __ **) let sem_state_params_jmdiscr x y = Logic.eq_rect_Type2 x (let { empty_framesT = a1; empty_regsT = a3; load_sp = a4; save_sp = a5 } = x in Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y type internal_stack = | Empty_is | One_is of ByteValues.beval | Both_is of ByteValues.beval * ByteValues.beval (** val internal_stack_rect_Type4 : 'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval -> 'a1) -> internal_stack -> 'a1 **) let rec internal_stack_rect_Type4 h_empty_is h_one_is h_both_is = function | Empty_is -> h_empty_is | One_is x_24543 -> h_one_is x_24543 | Both_is (x_24545, x_24544) -> h_both_is x_24545 x_24544 (** val internal_stack_rect_Type5 : 'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval -> 'a1) -> internal_stack -> 'a1 **) let rec internal_stack_rect_Type5 h_empty_is h_one_is h_both_is = function | Empty_is -> h_empty_is | One_is x_24550 -> h_one_is x_24550 | Both_is (x_24552, x_24551) -> h_both_is x_24552 x_24551 (** val internal_stack_rect_Type3 : 'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval -> 'a1) -> internal_stack -> 'a1 **) let rec internal_stack_rect_Type3 h_empty_is h_one_is h_both_is = function | Empty_is -> h_empty_is | One_is x_24557 -> h_one_is x_24557 | Both_is (x_24559, x_24558) -> h_both_is x_24559 x_24558 (** val internal_stack_rect_Type2 : 'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval -> 'a1) -> internal_stack -> 'a1 **) let rec internal_stack_rect_Type2 h_empty_is h_one_is h_both_is = function | Empty_is -> h_empty_is | One_is x_24564 -> h_one_is x_24564 | Both_is (x_24566, x_24565) -> h_both_is x_24566 x_24565 (** val internal_stack_rect_Type1 : 'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval -> 'a1) -> internal_stack -> 'a1 **) let rec internal_stack_rect_Type1 h_empty_is h_one_is h_both_is = function | Empty_is -> h_empty_is | One_is x_24571 -> h_one_is x_24571 | Both_is (x_24573, x_24572) -> h_both_is x_24573 x_24572 (** val internal_stack_rect_Type0 : 'a1 -> (ByteValues.beval -> 'a1) -> (ByteValues.beval -> ByteValues.beval -> 'a1) -> internal_stack -> 'a1 **) let rec internal_stack_rect_Type0 h_empty_is h_one_is h_both_is = function | Empty_is -> h_empty_is | One_is x_24578 -> h_one_is x_24578 | Both_is (x_24580, x_24579) -> h_both_is x_24580 x_24579 (** val internal_stack_inv_rect_Type4 : internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) -> (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1 **) let internal_stack_inv_rect_Type4 hterm h1 h2 h3 = let hcut = internal_stack_rect_Type4 h1 h2 h3 hterm in hcut __ (** val internal_stack_inv_rect_Type3 : internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) -> (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1 **) let internal_stack_inv_rect_Type3 hterm h1 h2 h3 = let hcut = internal_stack_rect_Type3 h1 h2 h3 hterm in hcut __ (** val internal_stack_inv_rect_Type2 : internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) -> (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1 **) let internal_stack_inv_rect_Type2 hterm h1 h2 h3 = let hcut = internal_stack_rect_Type2 h1 h2 h3 hterm in hcut __ (** val internal_stack_inv_rect_Type1 : internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) -> (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1 **) let internal_stack_inv_rect_Type1 hterm h1 h2 h3 = let hcut = internal_stack_rect_Type1 h1 h2 h3 hterm in hcut __ (** val internal_stack_inv_rect_Type0 : internal_stack -> (__ -> 'a1) -> (ByteValues.beval -> __ -> 'a1) -> (ByteValues.beval -> ByteValues.beval -> __ -> 'a1) -> 'a1 **) let internal_stack_inv_rect_Type0 hterm h1 h2 h3 = let hcut = internal_stack_rect_Type0 h1 h2 h3 hterm in hcut __ (** val internal_stack_discr : internal_stack -> internal_stack -> __ **) let internal_stack_discr x y = Logic.eq_rect_Type2 x (match x with | Empty_is -> Obj.magic (fun _ dH -> dH) | One_is a0 -> Obj.magic (fun _ dH -> dH __) | Both_is (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y (** val internal_stack_jmdiscr : internal_stack -> internal_stack -> __ **) let internal_stack_jmdiscr x y = Logic.eq_rect_Type2 x (match x with | Empty_is -> Obj.magic (fun _ dH -> dH) | One_is a0 -> Obj.magic (fun _ dH -> dH __) | Both_is (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y (** val is_push : internal_stack -> ByteValues.beval -> internal_stack Errors.res **) let is_push is bv = match is with | Empty_is -> Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) (One_is bv)) | One_is bv' -> Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) (Both_is (bv', bv))) | Both_is (x, x0) -> Errors.Error (List.Cons ((Errors.MSG ErrorMessages.InternalStackFull), List.Nil)) (** val is_pop : internal_stack -> (ByteValues.beval, internal_stack) Types.prod Errors.res **) let is_pop = function | Empty_is -> Errors.Error (List.Cons ((Errors.MSG ErrorMessages.InternalStackEmpty), List.Nil)) | One_is bv' -> Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = bv'; Types.snd = Empty_is }) | Both_is (bv, bv') -> Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = bv'; Types.snd = (One_is bv) }) type state = { st_frms : __ Types.option; istack : internal_stack; carry : ByteValues.bebit; regs : __; m : BEMem.bemem; stack_usage : Nat.nat } (** val state_rect_Type4 : sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **) let rec state_rect_Type4 semp h_mk_state x_24628 = let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0; m = m0; stack_usage = stack_usage0 } = x_24628 in h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0 (** val state_rect_Type5 : sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **) let rec state_rect_Type5 semp h_mk_state x_24630 = let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0; m = m0; stack_usage = stack_usage0 } = x_24630 in h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0 (** val state_rect_Type3 : sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **) let rec state_rect_Type3 semp h_mk_state x_24632 = let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0; m = m0; stack_usage = stack_usage0 } = x_24632 in h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0 (** val state_rect_Type2 : sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **) let rec state_rect_Type2 semp h_mk_state x_24634 = let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0; m = m0; stack_usage = stack_usage0 } = x_24634 in h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0 (** val state_rect_Type1 : sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **) let rec state_rect_Type1 semp h_mk_state x_24636 = let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0; m = m0; stack_usage = stack_usage0 } = x_24636 in h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0 (** val state_rect_Type0 : sem_state_params -> (__ Types.option -> internal_stack -> ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> 'a1) -> state -> 'a1 **) let rec state_rect_Type0 semp h_mk_state x_24638 = let { st_frms = st_frms0; istack = istack0; carry = carry0; regs = regs0; m = m0; stack_usage = stack_usage0 } = x_24638 in h_mk_state st_frms0 istack0 carry0 regs0 m0 stack_usage0 (** val st_frms : sem_state_params -> state -> __ Types.option **) let rec st_frms semp xxx = xxx.st_frms (** val istack : sem_state_params -> state -> internal_stack **) let rec istack semp xxx = xxx.istack (** val carry : sem_state_params -> state -> ByteValues.bebit **) let rec carry semp xxx = xxx.carry (** val regs : sem_state_params -> state -> __ **) let rec regs semp xxx = xxx.regs (** val m : sem_state_params -> state -> BEMem.bemem **) let rec m semp xxx = xxx.m (** val stack_usage : sem_state_params -> state -> Nat.nat **) let rec stack_usage semp xxx = xxx.stack_usage (** val state_inv_rect_Type4 : sem_state_params -> state -> (__ Types.option -> internal_stack -> ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1 **) let state_inv_rect_Type4 x1 hterm h1 = let hcut = state_rect_Type4 x1 h1 hterm in hcut __ (** val state_inv_rect_Type3 : sem_state_params -> state -> (__ Types.option -> internal_stack -> ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1 **) let state_inv_rect_Type3 x1 hterm h1 = let hcut = state_rect_Type3 x1 h1 hterm in hcut __ (** val state_inv_rect_Type2 : sem_state_params -> state -> (__ Types.option -> internal_stack -> ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1 **) let state_inv_rect_Type2 x1 hterm h1 = let hcut = state_rect_Type2 x1 h1 hterm in hcut __ (** val state_inv_rect_Type1 : sem_state_params -> state -> (__ Types.option -> internal_stack -> ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1 **) let state_inv_rect_Type1 x1 hterm h1 = let hcut = state_rect_Type1 x1 h1 hterm in hcut __ (** val state_inv_rect_Type0 : sem_state_params -> state -> (__ Types.option -> internal_stack -> ByteValues.bebit -> __ -> BEMem.bemem -> Nat.nat -> __ -> 'a1) -> 'a1 **) let state_inv_rect_Type0 x1 hterm h1 = let hcut = state_rect_Type0 x1 h1 hterm in hcut __ (** val state_jmdiscr : sem_state_params -> state -> state -> __ **) let state_jmdiscr a1 x y = Logic.eq_rect_Type2 x (let { st_frms = a0; istack = a10; carry = a2; regs = a3; m = a4; stack_usage = a5 } = x in Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y (** val sp : sem_state_params -> state -> ByteValues.xpointer Errors.res **) let sp p st = p.load_sp st.regs type state_pc = { st_no_pc : state; pc : ByteValues.program_counter; last_pop : ByteValues.program_counter } (** val state_pc_rect_Type4 : sem_state_params -> (state -> ByteValues.program_counter -> ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **) let rec state_pc_rect_Type4 semp h_mk_state_pc x_24654 = let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_24654 in h_mk_state_pc st_no_pc0 pc0 last_pop0 (** val state_pc_rect_Type5 : sem_state_params -> (state -> ByteValues.program_counter -> ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **) let rec state_pc_rect_Type5 semp h_mk_state_pc x_24656 = let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_24656 in h_mk_state_pc st_no_pc0 pc0 last_pop0 (** val state_pc_rect_Type3 : sem_state_params -> (state -> ByteValues.program_counter -> ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **) let rec state_pc_rect_Type3 semp h_mk_state_pc x_24658 = let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_24658 in h_mk_state_pc st_no_pc0 pc0 last_pop0 (** val state_pc_rect_Type2 : sem_state_params -> (state -> ByteValues.program_counter -> ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **) let rec state_pc_rect_Type2 semp h_mk_state_pc x_24660 = let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_24660 in h_mk_state_pc st_no_pc0 pc0 last_pop0 (** val state_pc_rect_Type1 : sem_state_params -> (state -> ByteValues.program_counter -> ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **) let rec state_pc_rect_Type1 semp h_mk_state_pc x_24662 = let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_24662 in h_mk_state_pc st_no_pc0 pc0 last_pop0 (** val state_pc_rect_Type0 : sem_state_params -> (state -> ByteValues.program_counter -> ByteValues.program_counter -> 'a1) -> state_pc -> 'a1 **) let rec state_pc_rect_Type0 semp h_mk_state_pc x_24664 = let { st_no_pc = st_no_pc0; pc = pc0; last_pop = last_pop0 } = x_24664 in h_mk_state_pc st_no_pc0 pc0 last_pop0 (** val st_no_pc : sem_state_params -> state_pc -> state **) let rec st_no_pc semp xxx = xxx.st_no_pc (** val pc : sem_state_params -> state_pc -> ByteValues.program_counter **) let rec pc semp xxx = xxx.pc (** val last_pop : sem_state_params -> state_pc -> ByteValues.program_counter **) let rec last_pop semp xxx = xxx.last_pop (** val state_pc_inv_rect_Type4 : sem_state_params -> state_pc -> (state -> ByteValues.program_counter -> ByteValues.program_counter -> __ -> 'a1) -> 'a1 **) let state_pc_inv_rect_Type4 x1 hterm h1 = let hcut = state_pc_rect_Type4 x1 h1 hterm in hcut __ (** val state_pc_inv_rect_Type3 : sem_state_params -> state_pc -> (state -> ByteValues.program_counter -> ByteValues.program_counter -> __ -> 'a1) -> 'a1 **) let state_pc_inv_rect_Type3 x1 hterm h1 = let hcut = state_pc_rect_Type3 x1 h1 hterm in hcut __ (** val state_pc_inv_rect_Type2 : sem_state_params -> state_pc -> (state -> ByteValues.program_counter -> ByteValues.program_counter -> __ -> 'a1) -> 'a1 **) let state_pc_inv_rect_Type2 x1 hterm h1 = let hcut = state_pc_rect_Type2 x1 h1 hterm in hcut __ (** val state_pc_inv_rect_Type1 : sem_state_params -> state_pc -> (state -> ByteValues.program_counter -> ByteValues.program_counter -> __ -> 'a1) -> 'a1 **) let state_pc_inv_rect_Type1 x1 hterm h1 = let hcut = state_pc_rect_Type1 x1 h1 hterm in hcut __ (** val state_pc_inv_rect_Type0 : sem_state_params -> state_pc -> (state -> ByteValues.program_counter -> ByteValues.program_counter -> __ -> 'a1) -> 'a1 **) let state_pc_inv_rect_Type0 x1 hterm h1 = let hcut = state_pc_rect_Type0 x1 h1 hterm in hcut __ (** val state_pc_discr : sem_state_params -> state_pc -> state_pc -> __ **) let state_pc_discr a1 x y = Logic.eq_rect_Type2 x (let { st_no_pc = a0; pc = a10; last_pop = a2 } = x in Obj.magic (fun _ dH -> dH __ __ __)) y (** val state_pc_jmdiscr : sem_state_params -> state_pc -> state_pc -> __ **) let state_pc_jmdiscr a1 x y = Logic.eq_rect_Type2 x (let { st_no_pc = a0; pc = a10; last_pop = a2 } = x in Obj.magic (fun _ dH -> dH __ __ __)) y (** val dpi1__o__st_no_pc__o__inject : sem_state_params -> (state_pc, 'a1) Types.dPair -> state Types.sig0 **) let dpi1__o__st_no_pc__o__inject x0 x3 = x3.Types.dpi1.st_no_pc (** val eject__o__st_no_pc__o__inject : sem_state_params -> state_pc Types.sig0 -> state Types.sig0 **) let eject__o__st_no_pc__o__inject x0 x3 = (Types.pi1 x3).st_no_pc (** val st_no_pc__o__inject : sem_state_params -> state_pc -> state Types.sig0 **) let st_no_pc__o__inject x0 x2 = x2.st_no_pc (** val dpi1__o__st_no_pc : sem_state_params -> (state_pc, 'a1) Types.dPair -> state **) let dpi1__o__st_no_pc x0 x2 = x2.Types.dpi1.st_no_pc (** val eject__o__st_no_pc : sem_state_params -> state_pc Types.sig0 -> state **) let eject__o__st_no_pc x0 x2 = (Types.pi1 x2).st_no_pc (** val init_pc : ByteValues.program_counter **) let init_pc = { ByteValues.pc_block = (Z.zopp (Z.z_of_nat (Nat.S Nat.O))); ByteValues.pc_offset = Positive.One } (** val null_pc : Positive.pos -> ByteValues.program_counter **) let null_pc pos = { ByteValues.pc_block = Pointers.dummy_block_code; ByteValues.pc_offset = pos } (** val set_m : sem_state_params -> BEMem.bemem -> state -> state **) let set_m p m0 st = { st_frms = st.st_frms; istack = st.istack; carry = st.carry; regs = st.regs; m = m0; stack_usage = st.stack_usage } (** val set_regs : sem_state_params -> __ -> state -> state **) let set_regs p regs0 st = { st_frms = st.st_frms; istack = st.istack; carry = st.carry; regs = regs0; m = st.m; stack_usage = st.stack_usage } (** val set_sp : sem_state_params -> ByteValues.xpointer -> state -> state **) let set_sp p sp0 st = let regs' = p.save_sp st.regs sp0 in { st_frms = st.st_frms; istack = st.istack; carry = st.carry; regs = regs'; m = st.m; stack_usage = st.stack_usage } (** val set_carry : sem_state_params -> ByteValues.bebit -> state -> state **) let set_carry p carry0 st = { st_frms = st.st_frms; istack = st.istack; carry = carry0; regs = st.regs; m = st.m; stack_usage = st.stack_usage } (** val set_istack : sem_state_params -> internal_stack -> state -> state **) let set_istack p is st = { st_frms = st.st_frms; istack = is; carry = st.carry; regs = st.regs; m = st.m; stack_usage = st.stack_usage } (** val set_pc : sem_state_params -> ByteValues.program_counter -> state_pc -> state_pc **) let set_pc p pc0 st = { st_no_pc = st.st_no_pc; pc = pc0; last_pop = st.last_pop } (** val set_no_pc : sem_state_params -> state -> state_pc -> state_pc **) let set_no_pc p s st = { st_no_pc = s; pc = st.pc; last_pop = st.last_pop } (** val set_last_pop : sem_state_params -> state -> ByteValues.program_counter -> state_pc **) let set_last_pop p st pc0 = { st_no_pc = st; pc = pc0; last_pop = pc0 } (** val set_frms : sem_state_params -> __ -> state -> state **) let set_frms p frms st = { st_frms = (Types.Some frms); istack = st.istack; carry = st.carry; regs = st.regs; m = st.m; stack_usage = st.stack_usage } type call_kind = | PTR | ID (** val call_kind_rect_Type4 : 'a1 -> 'a1 -> call_kind -> 'a1 **) let rec call_kind_rect_Type4 h_PTR h_ID = function | PTR -> h_PTR | ID -> h_ID (** val call_kind_rect_Type5 : 'a1 -> 'a1 -> call_kind -> 'a1 **) let rec call_kind_rect_Type5 h_PTR h_ID = function | PTR -> h_PTR | ID -> h_ID (** val call_kind_rect_Type3 : 'a1 -> 'a1 -> call_kind -> 'a1 **) let rec call_kind_rect_Type3 h_PTR h_ID = function | PTR -> h_PTR | ID -> h_ID (** val call_kind_rect_Type2 : 'a1 -> 'a1 -> call_kind -> 'a1 **) let rec call_kind_rect_Type2 h_PTR h_ID = function | PTR -> h_PTR | ID -> h_ID (** val call_kind_rect_Type1 : 'a1 -> 'a1 -> call_kind -> 'a1 **) let rec call_kind_rect_Type1 h_PTR h_ID = function | PTR -> h_PTR | ID -> h_ID (** val call_kind_rect_Type0 : 'a1 -> 'a1 -> call_kind -> 'a1 **) let rec call_kind_rect_Type0 h_PTR h_ID = function | PTR -> h_PTR | ID -> h_ID (** val call_kind_inv_rect_Type4 : call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let call_kind_inv_rect_Type4 hterm h1 h2 = let hcut = call_kind_rect_Type4 h1 h2 hterm in hcut __ (** val call_kind_inv_rect_Type3 : call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let call_kind_inv_rect_Type3 hterm h1 h2 = let hcut = call_kind_rect_Type3 h1 h2 hterm in hcut __ (** val call_kind_inv_rect_Type2 : call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let call_kind_inv_rect_Type2 hterm h1 h2 = let hcut = call_kind_rect_Type2 h1 h2 hterm in hcut __ (** val call_kind_inv_rect_Type1 : call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let call_kind_inv_rect_Type1 hterm h1 h2 = let hcut = call_kind_rect_Type1 h1 h2 hterm in hcut __ (** val call_kind_inv_rect_Type0 : call_kind -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let call_kind_inv_rect_Type0 hterm h1 h2 = let hcut = call_kind_rect_Type0 h1 h2 hterm in hcut __ (** val call_kind_discr : call_kind -> call_kind -> __ **) let call_kind_discr x y = Logic.eq_rect_Type2 x (match x with | PTR -> Obj.magic (fun _ dH -> dH) | ID -> Obj.magic (fun _ dH -> dH)) y (** val call_kind_jmdiscr : call_kind -> call_kind -> __ **) let call_kind_jmdiscr x y = Logic.eq_rect_Type2 x (match x with | PTR -> Obj.magic (fun _ dH -> dH) | ID -> Obj.magic (fun _ dH -> dH)) y (** val kind_of_call : Joint.unserialized_params -> (AST.ident, (__, __) Types.prod) Types.sum -> call_kind **) let kind_of_call p = function | Types.Inl x -> ID | Types.Inr x -> PTR type 'f sem_unserialized_params = { st_pars : sem_state_params; acca_store_ : (__ -> ByteValues.beval -> __ -> __ Errors.res); acca_retrieve_ : (__ -> __ -> ByteValues.beval Errors.res); acca_arg_retrieve_ : (__ -> __ -> ByteValues.beval Errors.res); accb_store_ : (__ -> ByteValues.beval -> __ -> __ Errors.res); accb_retrieve_ : (__ -> __ -> ByteValues.beval Errors.res); accb_arg_retrieve_ : (__ -> __ -> ByteValues.beval Errors.res); dpl_store_ : (__ -> ByteValues.beval -> __ -> __ Errors.res); dpl_retrieve_ : (__ -> __ -> ByteValues.beval Errors.res); dpl_arg_retrieve_ : (__ -> __ -> ByteValues.beval Errors.res); dph_store_ : (__ -> ByteValues.beval -> __ -> __ Errors.res); dph_retrieve_ : (__ -> __ -> ByteValues.beval Errors.res); dph_arg_retrieve_ : (__ -> __ -> ByteValues.beval Errors.res); snd_arg_retrieve_ : (__ -> __ -> ByteValues.beval Errors.res); pair_reg_move_ : (__ -> __ -> __ Errors.res); save_frame : (call_kind -> __ -> state_pc -> state Errors.res); setup_call : (Nat.nat -> __ -> __ -> state -> state Errors.res); fetch_external_args : (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res); set_result : (Values.val0 List.list -> __ -> state -> state Errors.res); call_args_for_main : __; call_dest_for_main : __; read_result : (AST.ident List.list -> 'f AST.fundef Globalenvs.genv_t -> __ -> state -> ByteValues.beval List.list Errors.res); eval_ext_seq : (AST.ident List.list -> 'f genv_gen -> __ -> AST.ident -> state -> state Errors.res); pop_frame : (AST.ident List.list -> 'f genv_gen -> AST.ident -> __ -> state -> (state, ByteValues.program_counter) Types.prod Errors.res) } (** val sem_unserialized_params_rect_Type4 : Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) -> (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state, ByteValues.program_counter) Types.prod Errors.res) -> 'a2) -> 'a1 sem_unserialized_params -> 'a2 **) let rec sem_unserialized_params_rect_Type4 uns_pars h_mk_sem_unserialized_params x_24719 = let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ = acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ = accb_store_0; accb_retrieve_ = accb_retrieve_0; accb_arg_retrieve_ = accb_arg_retrieve_0; dpl_store_ = dpl_store_0; dpl_retrieve_ = dpl_retrieve_0; dpl_arg_retrieve_ = dpl_arg_retrieve_0; dph_store_ = dph_store_0; dph_retrieve_ = dph_retrieve_0; dph_arg_retrieve_ = dph_arg_retrieve_0; snd_arg_retrieve_ = snd_arg_retrieve_0; pair_reg_move_ = pair_reg_move_0; save_frame = save_frame0; setup_call = setup_call0; fetch_external_args = fetch_external_args0; set_result = set_result0; call_args_for_main = call_args_for_main0; call_dest_for_main = call_dest_for_main0; read_result = read_result0; eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_24719 in h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0 acca_arg_retrieve_0 accb_store_0 accb_retrieve_0 accb_arg_retrieve_0 dpl_store_0 dpl_retrieve_0 dpl_arg_retrieve_0 dph_store_0 dph_retrieve_0 dph_arg_retrieve_0 snd_arg_retrieve_0 pair_reg_move_0 save_frame0 setup_call0 fetch_external_args0 set_result0 call_args_for_main0 call_dest_for_main0 read_result0 eval_ext_seq0 pop_frame0 (** val sem_unserialized_params_rect_Type5 : Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) -> (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state, ByteValues.program_counter) Types.prod Errors.res) -> 'a2) -> 'a1 sem_unserialized_params -> 'a2 **) let rec sem_unserialized_params_rect_Type5 uns_pars h_mk_sem_unserialized_params x_24721 = let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ = acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ = accb_store_0; accb_retrieve_ = accb_retrieve_0; accb_arg_retrieve_ = accb_arg_retrieve_0; dpl_store_ = dpl_store_0; dpl_retrieve_ = dpl_retrieve_0; dpl_arg_retrieve_ = dpl_arg_retrieve_0; dph_store_ = dph_store_0; dph_retrieve_ = dph_retrieve_0; dph_arg_retrieve_ = dph_arg_retrieve_0; snd_arg_retrieve_ = snd_arg_retrieve_0; pair_reg_move_ = pair_reg_move_0; save_frame = save_frame0; setup_call = setup_call0; fetch_external_args = fetch_external_args0; set_result = set_result0; call_args_for_main = call_args_for_main0; call_dest_for_main = call_dest_for_main0; read_result = read_result0; eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_24721 in h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0 acca_arg_retrieve_0 accb_store_0 accb_retrieve_0 accb_arg_retrieve_0 dpl_store_0 dpl_retrieve_0 dpl_arg_retrieve_0 dph_store_0 dph_retrieve_0 dph_arg_retrieve_0 snd_arg_retrieve_0 pair_reg_move_0 save_frame0 setup_call0 fetch_external_args0 set_result0 call_args_for_main0 call_dest_for_main0 read_result0 eval_ext_seq0 pop_frame0 (** val sem_unserialized_params_rect_Type3 : Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) -> (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state, ByteValues.program_counter) Types.prod Errors.res) -> 'a2) -> 'a1 sem_unserialized_params -> 'a2 **) let rec sem_unserialized_params_rect_Type3 uns_pars h_mk_sem_unserialized_params x_24723 = let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ = acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ = accb_store_0; accb_retrieve_ = accb_retrieve_0; accb_arg_retrieve_ = accb_arg_retrieve_0; dpl_store_ = dpl_store_0; dpl_retrieve_ = dpl_retrieve_0; dpl_arg_retrieve_ = dpl_arg_retrieve_0; dph_store_ = dph_store_0; dph_retrieve_ = dph_retrieve_0; dph_arg_retrieve_ = dph_arg_retrieve_0; snd_arg_retrieve_ = snd_arg_retrieve_0; pair_reg_move_ = pair_reg_move_0; save_frame = save_frame0; setup_call = setup_call0; fetch_external_args = fetch_external_args0; set_result = set_result0; call_args_for_main = call_args_for_main0; call_dest_for_main = call_dest_for_main0; read_result = read_result0; eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_24723 in h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0 acca_arg_retrieve_0 accb_store_0 accb_retrieve_0 accb_arg_retrieve_0 dpl_store_0 dpl_retrieve_0 dpl_arg_retrieve_0 dph_store_0 dph_retrieve_0 dph_arg_retrieve_0 snd_arg_retrieve_0 pair_reg_move_0 save_frame0 setup_call0 fetch_external_args0 set_result0 call_args_for_main0 call_dest_for_main0 read_result0 eval_ext_seq0 pop_frame0 (** val sem_unserialized_params_rect_Type2 : Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) -> (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state, ByteValues.program_counter) Types.prod Errors.res) -> 'a2) -> 'a1 sem_unserialized_params -> 'a2 **) let rec sem_unserialized_params_rect_Type2 uns_pars h_mk_sem_unserialized_params x_24725 = let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ = acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ = accb_store_0; accb_retrieve_ = accb_retrieve_0; accb_arg_retrieve_ = accb_arg_retrieve_0; dpl_store_ = dpl_store_0; dpl_retrieve_ = dpl_retrieve_0; dpl_arg_retrieve_ = dpl_arg_retrieve_0; dph_store_ = dph_store_0; dph_retrieve_ = dph_retrieve_0; dph_arg_retrieve_ = dph_arg_retrieve_0; snd_arg_retrieve_ = snd_arg_retrieve_0; pair_reg_move_ = pair_reg_move_0; save_frame = save_frame0; setup_call = setup_call0; fetch_external_args = fetch_external_args0; set_result = set_result0; call_args_for_main = call_args_for_main0; call_dest_for_main = call_dest_for_main0; read_result = read_result0; eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_24725 in h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0 acca_arg_retrieve_0 accb_store_0 accb_retrieve_0 accb_arg_retrieve_0 dpl_store_0 dpl_retrieve_0 dpl_arg_retrieve_0 dph_store_0 dph_retrieve_0 dph_arg_retrieve_0 snd_arg_retrieve_0 pair_reg_move_0 save_frame0 setup_call0 fetch_external_args0 set_result0 call_args_for_main0 call_dest_for_main0 read_result0 eval_ext_seq0 pop_frame0 (** val sem_unserialized_params_rect_Type1 : Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) -> (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state, ByteValues.program_counter) Types.prod Errors.res) -> 'a2) -> 'a1 sem_unserialized_params -> 'a2 **) let rec sem_unserialized_params_rect_Type1 uns_pars h_mk_sem_unserialized_params x_24727 = let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ = acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ = accb_store_0; accb_retrieve_ = accb_retrieve_0; accb_arg_retrieve_ = accb_arg_retrieve_0; dpl_store_ = dpl_store_0; dpl_retrieve_ = dpl_retrieve_0; dpl_arg_retrieve_ = dpl_arg_retrieve_0; dph_store_ = dph_store_0; dph_retrieve_ = dph_retrieve_0; dph_arg_retrieve_ = dph_arg_retrieve_0; snd_arg_retrieve_ = snd_arg_retrieve_0; pair_reg_move_ = pair_reg_move_0; save_frame = save_frame0; setup_call = setup_call0; fetch_external_args = fetch_external_args0; set_result = set_result0; call_args_for_main = call_args_for_main0; call_dest_for_main = call_dest_for_main0; read_result = read_result0; eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_24727 in h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0 acca_arg_retrieve_0 accb_store_0 accb_retrieve_0 accb_arg_retrieve_0 dpl_store_0 dpl_retrieve_0 dpl_arg_retrieve_0 dph_store_0 dph_retrieve_0 dph_arg_retrieve_0 snd_arg_retrieve_0 pair_reg_move_0 save_frame0 setup_call0 fetch_external_args0 set_result0 call_args_for_main0 call_dest_for_main0 read_result0 eval_ext_seq0 pop_frame0 (** val sem_unserialized_params_rect_Type0 : Joint.unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) -> (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state, ByteValues.program_counter) Types.prod Errors.res) -> 'a2) -> 'a1 sem_unserialized_params -> 'a2 **) let rec sem_unserialized_params_rect_Type0 uns_pars h_mk_sem_unserialized_params x_24729 = let { st_pars = st_pars0; acca_store_ = acca_store_0; acca_retrieve_ = acca_retrieve_0; acca_arg_retrieve_ = acca_arg_retrieve_0; accb_store_ = accb_store_0; accb_retrieve_ = accb_retrieve_0; accb_arg_retrieve_ = accb_arg_retrieve_0; dpl_store_ = dpl_store_0; dpl_retrieve_ = dpl_retrieve_0; dpl_arg_retrieve_ = dpl_arg_retrieve_0; dph_store_ = dph_store_0; dph_retrieve_ = dph_retrieve_0; dph_arg_retrieve_ = dph_arg_retrieve_0; snd_arg_retrieve_ = snd_arg_retrieve_0; pair_reg_move_ = pair_reg_move_0; save_frame = save_frame0; setup_call = setup_call0; fetch_external_args = fetch_external_args0; set_result = set_result0; call_args_for_main = call_args_for_main0; call_dest_for_main = call_dest_for_main0; read_result = read_result0; eval_ext_seq = eval_ext_seq0; pop_frame = pop_frame0 } = x_24729 in h_mk_sem_unserialized_params st_pars0 acca_store_0 acca_retrieve_0 acca_arg_retrieve_0 accb_store_0 accb_retrieve_0 accb_arg_retrieve_0 dpl_store_0 dpl_retrieve_0 dpl_arg_retrieve_0 dph_store_0 dph_retrieve_0 dph_arg_retrieve_0 snd_arg_retrieve_0 pair_reg_move_0 save_frame0 setup_call0 fetch_external_args0 set_result0 call_args_for_main0 call_dest_for_main0 read_result0 eval_ext_seq0 pop_frame0 (** val st_pars : Joint.unserialized_params -> 'a1 sem_unserialized_params -> sem_state_params **) let rec st_pars uns_pars xxx = xxx.st_pars (** val acca_store_ : Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> ByteValues.beval -> __ -> __ Errors.res **) let rec acca_store_ uns_pars xxx = xxx.acca_store_ (** val acca_retrieve_ : Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ -> ByteValues.beval Errors.res **) let rec acca_retrieve_ uns_pars xxx = xxx.acca_retrieve_ (** val acca_arg_retrieve_ : Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ -> ByteValues.beval Errors.res **) let rec acca_arg_retrieve_ uns_pars xxx = xxx.acca_arg_retrieve_ (** val accb_store_ : Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> ByteValues.beval -> __ -> __ Errors.res **) let rec accb_store_ uns_pars xxx = xxx.accb_store_ (** val accb_retrieve_ : Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ -> ByteValues.beval Errors.res **) let rec accb_retrieve_ uns_pars xxx = xxx.accb_retrieve_ (** val accb_arg_retrieve_ : Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ -> ByteValues.beval Errors.res **) let rec accb_arg_retrieve_ uns_pars xxx = xxx.accb_arg_retrieve_ (** val dpl_store_ : Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> ByteValues.beval -> __ -> __ Errors.res **) let rec dpl_store_ uns_pars xxx = xxx.dpl_store_ (** val dpl_retrieve_ : Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ -> ByteValues.beval Errors.res **) let rec dpl_retrieve_ uns_pars xxx = xxx.dpl_retrieve_ (** val dpl_arg_retrieve_ : Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ -> ByteValues.beval Errors.res **) let rec dpl_arg_retrieve_ uns_pars xxx = xxx.dpl_arg_retrieve_ (** val dph_store_ : Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> ByteValues.beval -> __ -> __ Errors.res **) let rec dph_store_ uns_pars xxx = xxx.dph_store_ (** val dph_retrieve_ : Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ -> ByteValues.beval Errors.res **) let rec dph_retrieve_ uns_pars xxx = xxx.dph_retrieve_ (** val dph_arg_retrieve_ : Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ -> ByteValues.beval Errors.res **) let rec dph_arg_retrieve_ uns_pars xxx = xxx.dph_arg_retrieve_ (** val snd_arg_retrieve_ : Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ -> ByteValues.beval Errors.res **) let rec snd_arg_retrieve_ uns_pars xxx = xxx.snd_arg_retrieve_ (** val pair_reg_move_ : Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> __ -> __ Errors.res **) let rec pair_reg_move_ uns_pars xxx = xxx.pair_reg_move_ (** val save_frame : Joint.unserialized_params -> 'a1 sem_unserialized_params -> call_kind -> __ -> state_pc -> state Errors.res **) let rec save_frame uns_pars xxx = xxx.save_frame (** val setup_call : Joint.unserialized_params -> 'a1 sem_unserialized_params -> Nat.nat -> __ -> __ -> state -> state Errors.res **) let rec setup_call uns_pars xxx = xxx.setup_call (** val fetch_external_args : Joint.unserialized_params -> 'a1 sem_unserialized_params -> AST.external_function -> state -> __ -> Values.val0 List.list Errors.res **) let rec fetch_external_args uns_pars xxx = xxx.fetch_external_args (** val set_result : Joint.unserialized_params -> 'a1 sem_unserialized_params -> Values.val0 List.list -> __ -> state -> state Errors.res **) let rec set_result uns_pars xxx = xxx.set_result (** val call_args_for_main : Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ **) let rec call_args_for_main uns_pars xxx = xxx.call_args_for_main (** val call_dest_for_main : Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ **) let rec call_dest_for_main uns_pars xxx = xxx.call_dest_for_main (** val read_result : Joint.unserialized_params -> 'a1 sem_unserialized_params -> AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state -> ByteValues.beval List.list Errors.res **) let rec read_result uns_pars xxx = xxx.read_result (** val eval_ext_seq : Joint.unserialized_params -> 'a1 sem_unserialized_params -> AST.ident List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state Errors.res **) let rec eval_ext_seq uns_pars xxx = xxx.eval_ext_seq (** val pop_frame : Joint.unserialized_params -> 'a1 sem_unserialized_params -> AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state, ByteValues.program_counter) Types.prod Errors.res **) let rec pop_frame uns_pars xxx = xxx.pop_frame (** val sem_unserialized_params_inv_rect_Type4 : Joint.unserialized_params -> 'a1 sem_unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) -> (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state, ByteValues.program_counter) Types.prod Errors.res) -> __ -> 'a2) -> 'a2 **) let sem_unserialized_params_inv_rect_Type4 x1 hterm h1 = let hcut = sem_unserialized_params_rect_Type4 x1 h1 hterm in hcut __ (** val sem_unserialized_params_inv_rect_Type3 : Joint.unserialized_params -> 'a1 sem_unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) -> (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state, ByteValues.program_counter) Types.prod Errors.res) -> __ -> 'a2) -> 'a2 **) let sem_unserialized_params_inv_rect_Type3 x1 hterm h1 = let hcut = sem_unserialized_params_rect_Type3 x1 h1 hterm in hcut __ (** val sem_unserialized_params_inv_rect_Type2 : Joint.unserialized_params -> 'a1 sem_unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) -> (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state, ByteValues.program_counter) Types.prod Errors.res) -> __ -> 'a2) -> 'a2 **) let sem_unserialized_params_inv_rect_Type2 x1 hterm h1 = let hcut = sem_unserialized_params_rect_Type2 x1 h1 hterm in hcut __ (** val sem_unserialized_params_inv_rect_Type1 : Joint.unserialized_params -> 'a1 sem_unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) -> (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state, ByteValues.program_counter) Types.prod Errors.res) -> __ -> 'a2) -> 'a2 **) let sem_unserialized_params_inv_rect_Type1 x1 hterm h1 = let hcut = sem_unserialized_params_rect_Type1 x1 h1 hterm in hcut __ (** val sem_unserialized_params_inv_rect_Type0 : Joint.unserialized_params -> 'a1 sem_unserialized_params -> (sem_state_params -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> ByteValues.beval -> __ -> __ Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> ByteValues.beval Errors.res) -> (__ -> __ -> __ Errors.res) -> (call_kind -> __ -> state_pc -> state Errors.res) -> (Nat.nat -> __ -> __ -> state -> state Errors.res) -> (AST.external_function -> state -> __ -> Values.val0 List.list Errors.res) -> (Values.val0 List.list -> __ -> state -> state Errors.res) -> __ -> __ -> (AST.ident List.list -> 'a1 AST.fundef Globalenvs.genv_t -> __ -> state -> ByteValues.beval List.list Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> __ -> AST.ident -> state -> state Errors.res) -> (AST.ident List.list -> 'a1 genv_gen -> AST.ident -> __ -> state -> (state, ByteValues.program_counter) Types.prod Errors.res) -> __ -> 'a2) -> 'a2 **) let sem_unserialized_params_inv_rect_Type0 x1 hterm h1 = let hcut = sem_unserialized_params_rect_Type0 x1 h1 hterm in hcut __ (** val sem_unserialized_params_jmdiscr : Joint.unserialized_params -> 'a1 sem_unserialized_params -> 'a1 sem_unserialized_params -> __ **) let sem_unserialized_params_jmdiscr a1 x y = Logic.eq_rect_Type2 x (let { st_pars = a0; acca_store_ = a10; acca_retrieve_ = a20; acca_arg_retrieve_ = a3; accb_store_ = a4; accb_retrieve_ = a5; accb_arg_retrieve_ = a6; dpl_store_ = a7; dpl_retrieve_ = a8; dpl_arg_retrieve_ = a9; dph_store_ = a100; dph_retrieve_ = a11; dph_arg_retrieve_ = a12; snd_arg_retrieve_ = a13; pair_reg_move_ = a14; save_frame = a15; setup_call = a16; fetch_external_args = a17; set_result = a18; call_args_for_main = a19; call_dest_for_main = a200; read_result = a21; eval_ext_seq = a22; pop_frame = a23 } = x in Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __ __)) y (** val helper_def_retrieve : (Joint.unserialized_params -> __ -> __ sem_unserialized_params -> __ -> 'a1 -> ByteValues.beval Errors.res) -> Joint.unserialized_params -> 'a2 sem_unserialized_params -> state -> 'a1 -> ByteValues.beval Errors.res **) let helper_def_retrieve f up p st = Obj.magic f up __ p st.regs (** val helper_def_store : (Joint.unserialized_params -> __ -> __ sem_unserialized_params -> 'a1 -> ByteValues.beval -> __ -> __ Errors.res) -> Joint.unserialized_params -> 'a2 sem_unserialized_params -> 'a1 -> ByteValues.beval -> state -> state Errors.res **) let helper_def_store f up p x v st = Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic f up __ p x v st.regs) (fun r -> Monad.m_return0 (Monad.max_def Errors.res0) (set_regs p.st_pars r st))) (** val acca_retrieve : Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ -> ByteValues.beval Errors.res **) let acca_retrieve up p x x0 = helper_def_retrieve (fun x1 _ -> acca_retrieve_ x1) up p x x0 (** val acca_store : Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> ByteValues.beval -> state -> state Errors.res **) let acca_store up p x x0 x1 = helper_def_store (fun x2 _ -> acca_store_ x2) up p x x0 x1 (** val acca_arg_retrieve : Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ -> ByteValues.beval Errors.res **) let acca_arg_retrieve up p x x0 = helper_def_retrieve (fun x1 _ -> acca_arg_retrieve_ x1) up p x x0 (** val accb_store : Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> ByteValues.beval -> state -> state Errors.res **) let accb_store up p x x0 x1 = helper_def_store (fun x2 _ -> accb_store_ x2) up p x x0 x1 (** val accb_retrieve : Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ -> ByteValues.beval Errors.res **) let accb_retrieve up p x x0 = helper_def_retrieve (fun x1 _ -> accb_retrieve_ x1) up p x x0 (** val accb_arg_retrieve : Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ -> ByteValues.beval Errors.res **) let accb_arg_retrieve up p x x0 = helper_def_retrieve (fun x1 _ -> accb_arg_retrieve_ x1) up p x x0 (** val dpl_store : Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> ByteValues.beval -> state -> state Errors.res **) let dpl_store up p x x0 x1 = helper_def_store (fun x2 _ -> dpl_store_ x2) up p x x0 x1 (** val dpl_retrieve : Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ -> ByteValues.beval Errors.res **) let dpl_retrieve up p x x0 = helper_def_retrieve (fun x1 _ -> dpl_retrieve_ x1) up p x x0 (** val dpl_arg_retrieve : Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ -> ByteValues.beval Errors.res **) let dpl_arg_retrieve up p x x0 = helper_def_retrieve (fun x1 _ -> dpl_arg_retrieve_ x1) up p x x0 (** val dph_store : Joint.unserialized_params -> 'a1 sem_unserialized_params -> __ -> ByteValues.beval -> state -> state Errors.res **) let dph_store up p x x0 x1 = helper_def_store (fun x2 _ -> dph_store_ x2) up p x x0 x1 (** val dph_retrieve : Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ -> ByteValues.beval Errors.res **) let dph_retrieve up p x x0 = helper_def_retrieve (fun x1 _ -> dph_retrieve_ x1) up p x x0 (** val dph_arg_retrieve : Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ -> ByteValues.beval Errors.res **) let dph_arg_retrieve up p x x0 = helper_def_retrieve (fun x1 _ -> dph_arg_retrieve_ x1) up p x x0 (** val snd_arg_retrieve : Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ -> ByteValues.beval Errors.res **) let snd_arg_retrieve up p x x0 = helper_def_retrieve (fun x1 _ -> snd_arg_retrieve_ x1) up p x x0 (** val pair_reg_move : Joint.unserialized_params -> 'a1 sem_unserialized_params -> state -> __ -> __ **) let pair_reg_move up p st pm = Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (p.pair_reg_move_ st.regs pm)) (fun r -> Monad.m_return0 (Monad.max_def Errors.res0) (set_regs p.st_pars r st)) (** val push : sem_state_params -> state -> ByteValues.beval -> state Errors.res **) let push p st v = Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (is_push st.istack v)) (fun is -> Monad.m_return0 (Monad.max_def Errors.res0) (set_istack p is st))) (** val pop : sem_state_params -> state -> (ByteValues.beval, state) Types.prod Errors.res **) let pop p st = Obj.magic (Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic (is_pop st.istack)) (fun bv is -> Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = bv; Types.snd = (set_istack p is st) })) (** val push_ra : sem_state_params -> state -> ByteValues.program_counter -> state Errors.res **) let push_ra p st l = let { Types.fst = addrl; Types.snd = addrh } = ByteValues.beval_pair_of_pc l in Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (push p st addrl)) (fun st' -> Obj.magic (push p st' addrh))) (** val pop_ra : sem_state_params -> state -> (state, ByteValues.program_counter) Types.prod Errors.res **) let pop_ra p st = Obj.magic (Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic (pop p st)) (fun addrh st' -> Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic (pop p st')) (fun addrl st'' -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (ByteValues.pc_of_bevals (List.Cons (addrl, (List.Cons (addrh, List.Nil)))))) (fun pr -> Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = st''; Types.snd = pr })))) type serialized_params = { spp : Joint.params; msu_pars : Joint.joint_closed_internal_function sem_unserialized_params; offset_of_point : (__ -> Positive.pos); point_of_offset : (Positive.pos -> __) } (** val serialized_params_rect_Type4 : (Joint.params -> Joint.joint_closed_internal_function sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **) let rec serialized_params_rect_Type4 h_mk_serialized_params x_24799 = let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0; point_of_offset = point_of_offset0 } = x_24799 in h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __ (** val serialized_params_rect_Type5 : (Joint.params -> Joint.joint_closed_internal_function sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **) let rec serialized_params_rect_Type5 h_mk_serialized_params x_24801 = let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0; point_of_offset = point_of_offset0 } = x_24801 in h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __ (** val serialized_params_rect_Type3 : (Joint.params -> Joint.joint_closed_internal_function sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **) let rec serialized_params_rect_Type3 h_mk_serialized_params x_24803 = let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0; point_of_offset = point_of_offset0 } = x_24803 in h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __ (** val serialized_params_rect_Type2 : (Joint.params -> Joint.joint_closed_internal_function sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **) let rec serialized_params_rect_Type2 h_mk_serialized_params x_24805 = let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0; point_of_offset = point_of_offset0 } = x_24805 in h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __ (** val serialized_params_rect_Type1 : (Joint.params -> Joint.joint_closed_internal_function sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **) let rec serialized_params_rect_Type1 h_mk_serialized_params x_24807 = let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0; point_of_offset = point_of_offset0 } = x_24807 in h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __ (** val serialized_params_rect_Type0 : (Joint.params -> Joint.joint_closed_internal_function sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) -> __ -> __ -> 'a1) -> serialized_params -> 'a1 **) let rec serialized_params_rect_Type0 h_mk_serialized_params x_24809 = let { spp = spp0; msu_pars = msu_pars0; offset_of_point = offset_of_point0; point_of_offset = point_of_offset0 } = x_24809 in h_mk_serialized_params spp0 msu_pars0 offset_of_point0 point_of_offset0 __ __ (** val spp : serialized_params -> Joint.params **) let rec spp xxx = xxx.spp (** val msu_pars : serialized_params -> Joint.joint_closed_internal_function sem_unserialized_params **) let rec msu_pars xxx = xxx.msu_pars (** val offset_of_point : serialized_params -> __ -> Positive.pos **) let rec offset_of_point xxx = xxx.offset_of_point (** val point_of_offset : serialized_params -> Positive.pos -> __ **) let rec point_of_offset xxx = xxx.point_of_offset (** val serialized_params_inv_rect_Type4 : serialized_params -> (Joint.params -> Joint.joint_closed_internal_function sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) -> __ -> __ -> __ -> 'a1) -> 'a1 **) let serialized_params_inv_rect_Type4 hterm h1 = let hcut = serialized_params_rect_Type4 h1 hterm in hcut __ (** val serialized_params_inv_rect_Type3 : serialized_params -> (Joint.params -> Joint.joint_closed_internal_function sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) -> __ -> __ -> __ -> 'a1) -> 'a1 **) let serialized_params_inv_rect_Type3 hterm h1 = let hcut = serialized_params_rect_Type3 h1 hterm in hcut __ (** val serialized_params_inv_rect_Type2 : serialized_params -> (Joint.params -> Joint.joint_closed_internal_function sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) -> __ -> __ -> __ -> 'a1) -> 'a1 **) let serialized_params_inv_rect_Type2 hterm h1 = let hcut = serialized_params_rect_Type2 h1 hterm in hcut __ (** val serialized_params_inv_rect_Type1 : serialized_params -> (Joint.params -> Joint.joint_closed_internal_function sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) -> __ -> __ -> __ -> 'a1) -> 'a1 **) let serialized_params_inv_rect_Type1 hterm h1 = let hcut = serialized_params_rect_Type1 h1 hterm in hcut __ (** val serialized_params_inv_rect_Type0 : serialized_params -> (Joint.params -> Joint.joint_closed_internal_function sem_unserialized_params -> (__ -> Positive.pos) -> (Positive.pos -> __) -> __ -> __ -> __ -> 'a1) -> 'a1 **) let serialized_params_inv_rect_Type0 hterm h1 = let hcut = serialized_params_rect_Type0 h1 hterm in hcut __ (** val serialized_params_jmdiscr : serialized_params -> serialized_params -> __ **) let serialized_params_jmdiscr x y = Logic.eq_rect_Type2 x (let { spp = a0; msu_pars = a1; offset_of_point = a2; point_of_offset = a3 } = x in Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y (** val spp__o__stmt_pars : serialized_params -> Joint.stmt_params **) let spp__o__stmt_pars x0 = x0.spp.Joint.stmt_pars (** val spp__o__stmt_pars__o__uns_pars : serialized_params -> Joint.uns_params **) let spp__o__stmt_pars__o__uns_pars x0 = Joint.stmt_pars__o__uns_pars x0.spp (** val spp__o__stmt_pars__o__uns_pars__o__u_pars : serialized_params -> Joint.unserialized_params **) let spp__o__stmt_pars__o__uns_pars__o__u_pars x0 = Joint.stmt_pars__o__uns_pars__o__u_pars x0.spp (** val msu_pars__o__st_pars : serialized_params -> sem_state_params **) let msu_pars__o__st_pars x0 = x0.msu_pars.st_pars type sem_params = { spp' : serialized_params; pre_main_generator : (Joint.joint_program -> Joint.joint_closed_internal_function) } (** val sem_params_rect_Type4 : (serialized_params -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **) let rec sem_params_rect_Type4 h_mk_sem_params x_24827 = let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_24827 in h_mk_sem_params spp'0 pre_main_generator0 (** val sem_params_rect_Type5 : (serialized_params -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **) let rec sem_params_rect_Type5 h_mk_sem_params x_24829 = let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_24829 in h_mk_sem_params spp'0 pre_main_generator0 (** val sem_params_rect_Type3 : (serialized_params -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **) let rec sem_params_rect_Type3 h_mk_sem_params x_24831 = let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_24831 in h_mk_sem_params spp'0 pre_main_generator0 (** val sem_params_rect_Type2 : (serialized_params -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **) let rec sem_params_rect_Type2 h_mk_sem_params x_24833 = let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_24833 in h_mk_sem_params spp'0 pre_main_generator0 (** val sem_params_rect_Type1 : (serialized_params -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **) let rec sem_params_rect_Type1 h_mk_sem_params x_24835 = let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_24835 in h_mk_sem_params spp'0 pre_main_generator0 (** val sem_params_rect_Type0 : (serialized_params -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) -> sem_params -> 'a1 **) let rec sem_params_rect_Type0 h_mk_sem_params x_24837 = let { spp' = spp'0; pre_main_generator = pre_main_generator0 } = x_24837 in h_mk_sem_params spp'0 pre_main_generator0 (** val spp' : sem_params -> serialized_params **) let rec spp' xxx = xxx.spp' (** val pre_main_generator : sem_params -> Joint.joint_program -> Joint.joint_closed_internal_function **) let rec pre_main_generator xxx = xxx.pre_main_generator (** val sem_params_inv_rect_Type4 : sem_params -> (serialized_params -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **) let sem_params_inv_rect_Type4 hterm h1 = let hcut = sem_params_rect_Type4 h1 hterm in hcut __ (** val sem_params_inv_rect_Type3 : sem_params -> (serialized_params -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **) let sem_params_inv_rect_Type3 hterm h1 = let hcut = sem_params_rect_Type3 h1 hterm in hcut __ (** val sem_params_inv_rect_Type2 : sem_params -> (serialized_params -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **) let sem_params_inv_rect_Type2 hterm h1 = let hcut = sem_params_rect_Type2 h1 hterm in hcut __ (** val sem_params_inv_rect_Type1 : sem_params -> (serialized_params -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **) let sem_params_inv_rect_Type1 hterm h1 = let hcut = sem_params_rect_Type1 h1 hterm in hcut __ (** val sem_params_inv_rect_Type0 : sem_params -> (serialized_params -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **) let sem_params_inv_rect_Type0 hterm h1 = let hcut = sem_params_rect_Type0 h1 hterm in hcut __ (** val sem_params_jmdiscr : sem_params -> sem_params -> __ **) let sem_params_jmdiscr x y = Logic.eq_rect_Type2 x (let { spp' = a0; pre_main_generator = a1 } = x in Obj.magic (fun _ dH -> dH __ __)) y (** val spp'__o__msu_pars : sem_params -> Joint.joint_closed_internal_function sem_unserialized_params **) let spp'__o__msu_pars x0 = x0.spp'.msu_pars (** val spp'__o__msu_pars__o__st_pars : sem_params -> sem_state_params **) let spp'__o__msu_pars__o__st_pars x0 = msu_pars__o__st_pars x0.spp' (** val spp'__o__spp : sem_params -> Joint.params **) let spp'__o__spp x0 = x0.spp'.spp (** val spp'__o__spp__o__stmt_pars : sem_params -> Joint.stmt_params **) let spp'__o__spp__o__stmt_pars x0 = spp__o__stmt_pars x0.spp' (** val spp'__o__spp__o__stmt_pars__o__uns_pars : sem_params -> Joint.uns_params **) let spp'__o__spp__o__stmt_pars__o__uns_pars x0 = spp__o__stmt_pars__o__uns_pars x0.spp' (** val spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars : sem_params -> Joint.unserialized_params **) let spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 = spp__o__stmt_pars__o__uns_pars__o__u_pars x0.spp' (** val pc_of_point : sem_params -> Pointers.block Types.sig0 -> __ -> ByteValues.program_counter **) let pc_of_point p bl pt = { ByteValues.pc_block = bl; ByteValues.pc_offset = (p.spp'.offset_of_point pt) } (** val point_of_pc : sem_params -> ByteValues.program_counter -> __ **) let point_of_pc p ptr = p.spp'.point_of_offset ptr.ByteValues.pc_offset (** val fetch_statement : sem_params -> AST.ident List.list -> genv -> ByteValues.program_counter -> ((AST.ident, Joint.joint_closed_internal_function) Types.prod, Joint.joint_statement) Types.prod Errors.res **) let fetch_statement p globals ge0 ptr = Obj.magic (Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic (fetch_internal_function globals ge0 ptr.ByteValues.pc_block)) (fun id fn -> let pt = point_of_pc p ptr in Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Errors.opt_to_res (Errors.msg ErrorMessages.ProgramCounterOutOfCode) ((spp'__o__spp p).Joint.stmt_at globals (Types.pi1 fn).Joint.joint_if_code pt))) (fun stmt -> Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = { Types.fst = id; Types.snd = fn }; Types.snd = stmt }))) (** val pc_of_label : sem_params -> AST.ident List.list -> genv -> Pointers.block Types.sig0 -> Graphs.label -> ByteValues.program_counter Errors.res **) let pc_of_label p globals ge0 bl lbl = Obj.magic (Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic (fetch_internal_function globals ge0 bl)) (fun i fn -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.LabelNotFound), (List.Cons ((Errors.CTX (PreIdentifiers.LabelTag, lbl)), List.Nil)))) ((spp'__o__spp p).Joint.point_of_label globals (Types.pi1 fn).Joint.joint_if_code lbl))) (fun pt -> Monad.m_return0 (Monad.max_def Errors.res0) { ByteValues.pc_block = bl; ByteValues.pc_offset = (p.spp'.offset_of_point pt) }))) (** val succ_pc : sem_params -> ByteValues.program_counter -> __ -> ByteValues.program_counter **) let succ_pc p ptr nxt = let curr = point_of_pc p ptr in pc_of_point p ptr.ByteValues.pc_block ((spp'__o__spp p).Joint.point_of_succ curr nxt) (** val goto : sem_params -> AST.ident List.list -> genv -> Graphs.label -> state_pc -> state_pc Errors.res **) let goto p globals ge0 l st = Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (pc_of_label p globals ge0 st.pc.ByteValues.pc_block l)) (fun newpc -> Monad.m_return0 (Monad.max_def Errors.res0) (set_pc (spp'__o__msu_pars__o__st_pars p) newpc st))) (** val next : sem_params -> __ -> state_pc -> state_pc **) let next p l st = let newpc = succ_pc p st.pc l in set_pc (spp'__o__msu_pars__o__st_pars p) newpc st (** val next_of_call_pc : sem_params -> AST.ident List.list -> genv -> ByteValues.program_counter -> __ Errors.res **) let next_of_call_pc p globals ge0 pc0 = Obj.magic (Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic (fetch_statement p globals ge0 pc0)) (fun id_fn stmt -> match stmt with | Joint.Sequential (s, nxt) -> (match s with | Joint.COST_LABEL x -> Obj.magic (Errors.Error (List.Cons ((Errors.MSG ErrorMessages.NoSuccessor), List.Nil))) | Joint.CALL (x, x0, x1) -> Monad.m_return0 (Monad.max_def Errors.res0) nxt | Joint.COND (x, x0) -> Obj.magic (Errors.Error (List.Cons ((Errors.MSG ErrorMessages.NoSuccessor), List.Nil))) | Joint.Step_seq x -> Obj.magic (Errors.Error (List.Cons ((Errors.MSG ErrorMessages.NoSuccessor), List.Nil)))) | Joint.Final x -> Obj.magic (Errors.Error (List.Cons ((Errors.MSG ErrorMessages.NoSuccessor), List.Nil))) | Joint.FCOND (x0, x1, x2) -> Obj.magic (Errors.Error (List.Cons ((Errors.MSG ErrorMessages.NoSuccessor), List.Nil))))) (** val eval_seq_no_pc : sem_params -> AST.ident List.list -> genv -> AST.ident -> Joint.joint_seq -> state -> state Errors.res **) let eval_seq_no_pc p globals ge0 curr_id seq st = match seq with | Joint.COMMENT x -> Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st) | Joint.MOVE dst_src -> Obj.magic (pair_reg_move (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp) p.spp'.msu_pars st dst_src) | Joint.POP dst -> Obj.magic (Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic (pop (spp'__o__msu_pars__o__st_pars p) st)) (fun v st' -> Obj.magic (acca_store (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp) (spp'__o__msu_pars p) dst v st'))) | Joint.PUSH src -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (acca_arg_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp) p.spp'.msu_pars st src)) (fun v -> Obj.magic (push (spp'__o__msu_pars__o__st_pars p) st v))) | Joint.ADDRESS (id, off, ldest, hdest) -> let addr_block = Option.opt_safe (Globalenvs.find_symbol ge0.ge id) in let { Types.fst = laddr; Types.snd = haddr } = ByteValues.beval_pair_of_pointer { Pointers.pblock = addr_block; Pointers.poff = off } in Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (dpl_store (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p) p.spp'.msu_pars ldest laddr st)) (fun st' -> Obj.magic (dph_store (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p) p.spp'.msu_pars hdest haddr st'))) | Joint.OPACCS (op, dacc_a_reg, dacc_b_reg, sacc_a_reg, sacc_b_reg) -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (acca_arg_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp) p.spp'.msu_pars st sacc_a_reg)) (fun v1 -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (accb_arg_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp) p.spp'.msu_pars st sacc_b_reg)) (fun v2 -> Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic (BackEndOps.be_opaccs op v1 v2)) (fun v1' v2' -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (acca_store (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p) p.spp'.msu_pars dacc_a_reg v1' st)) (fun st' -> Obj.magic (accb_store (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p) p.spp'.msu_pars dacc_b_reg v2' st')))))) | Joint.OP1 (op, dacc_a, sacc_a) -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (acca_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp) p.spp'.msu_pars st sacc_a)) (fun v -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (BackEndOps.be_op1 op v)) (fun v' -> Obj.magic (acca_store (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p) p.spp'.msu_pars dacc_a v' st)))) | Joint.OP2 (op, dacc_a, sacc_a, src) -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (acca_arg_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp) p.spp'.msu_pars st sacc_a)) (fun v1 -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (snd_arg_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp) p.spp'.msu_pars st src)) (fun v2 -> Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic (BackEndOps.be_op2 st.carry op v1 v2)) (fun v' carry0 -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (acca_store (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p) p.spp'.msu_pars dacc_a v' st)) (fun st' -> Monad.m_return0 (Monad.max_def Errors.res0) (set_carry p.spp'.msu_pars.st_pars carry0 st')))))) | Joint.CLEAR_CARRY -> Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) (set_carry (spp'__o__msu_pars__o__st_pars p) (ByteValues.BBbit Bool.False) st)) | Joint.SET_CARRY -> Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) (set_carry (spp'__o__msu_pars__o__st_pars p) (ByteValues.BBbit Bool.True) st)) | Joint.LOAD (dst, addrl, addrh) -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (dph_arg_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp) p.spp'.msu_pars st addrh)) (fun vaddrh -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (dpl_arg_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp) p.spp'.msu_pars st addrl)) (fun vaddrl -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (BEMem.pointer_of_address { Types.fst = vaddrl; Types.snd = vaddrh })) (fun vaddr -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Errors.opt_to_res (Errors.msg ErrorMessages.FailedLoad) (GenMem.beloadv st.m vaddr))) (fun v -> Obj.magic (acca_store (spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars p) p.spp'.msu_pars dst v st)))))) | Joint.STORE (addrl, addrh, src) -> Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (dph_arg_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp) p.spp'.msu_pars st addrh)) (fun vaddrh -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (dpl_arg_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp) p.spp'.msu_pars st addrl)) (fun vaddrl -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (BEMem.pointer_of_address { Types.fst = vaddrl; Types.snd = vaddrh })) (fun vaddr -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (acca_arg_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp) p.spp'.msu_pars st src)) (fun v -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Errors.opt_to_res (Errors.msg ErrorMessages.FailedStore) (GenMem.bestorev st.m vaddr v))) (fun m' -> Monad.m_return0 (Monad.max_def Errors.res0) (set_m (spp'__o__msu_pars__o__st_pars p) m' st))))))) | Joint.Extension_seq c -> p.spp'.msu_pars.eval_ext_seq globals ge0 c curr_id st (** val block_of_call : sem_params -> AST.ident List.list -> genv -> (PreIdentifiers.identifier, (__, __) Types.prod) Types.sum -> state -> __ **) let block_of_call p globals ge0 f st = Monad.m_bind0 (Monad.max_def Errors.res0) (match f with | Types.Inl id -> Obj.magic (Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction), (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, id)), List.Nil)))) (Globalenvs.find_symbol ge0.ge id)) | Types.Inr addr -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (dpl_arg_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp) p.spp'.msu_pars st addr.Types.fst)) (fun addr_l -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (dph_arg_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp) p.spp'.msu_pars st addr.Types.snd)) (fun addr_h -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (ByteValues.pointer_of_bevals (List.Cons (addr_l, (List.Cons (addr_h, List.Nil)))))) (fun ptr -> match BitVector.eq_bv Pointers.offset_size (BitVector.zero Pointers.offset_size) (Pointers.offv ptr.Pointers.poff) with | Bool.True -> Monad.m_return0 (Monad.max_def Errors.res0) ptr.Pointers.pblock | Bool.False -> Obj.magic (Errors.Error (List.Cons ((Errors.MSG ErrorMessages.BadFunction), (List.Cons ((Errors.MSG ErrorMessages.BadPointer), List.Nil))))))))) (fun bl -> Obj.magic (Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadFunction), (List.Cons ((Errors.MSG ErrorMessages.BadPointer), List.Nil)))) (code_block_of_block bl))) (** val eval_external_call : sem_params -> AST.external_function -> __ -> __ -> state -> __ **) let eval_external_call p fn args dest st = Monad.m_bind0 (Monad.max_def IOMonad.iOMonad) (let x = IOMonad.err_to_io ((spp'__o__msu_pars p).fetch_external_args fn st args) in Obj.magic x) (fun params -> Monad.m_bind0 (Monad.max_def IOMonad.iOMonad) (let x = IOMonad.err_to_io (IO.check_eventval_list params fn.AST.ef_sig.AST.sig_args) in Obj.magic x) (fun evargs -> Monad.m_bind0 (Monad.max_def IOMonad.iOMonad) (Obj.magic (IO.do_io fn.AST.ef_id evargs (AST.proj_sig_res fn.AST.ef_sig))) (fun evres -> let vs = List.Cons ((IO.mk_val (AST.proj_sig_res fn.AST.ef_sig) evres), List.Nil) in Obj.magic (IOMonad.err_to_io ((spp'__o__msu_pars p).set_result vs dest st))))) (** val increment_stack_usage : sem_state_params -> Nat.nat -> state -> state **) let increment_stack_usage p n st = { st_frms = st.st_frms; istack = st.istack; carry = st.carry; regs = st.regs; m = st.m; stack_usage = (Nat.plus n st.stack_usage) } (** val decrement_stack_usage : sem_state_params -> Nat.nat -> state -> state **) let decrement_stack_usage p n st = { st_frms = st.st_frms; istack = st.istack; carry = st.carry; regs = st.regs; m = st.m; stack_usage = (Nat.minus st.stack_usage n) } (** val eval_internal_call : sem_params -> AST.ident List.list -> genv -> PreIdentifiers.identifier -> Joint.joint_internal_function -> __ -> state -> __ **) let eval_internal_call p globals ge0 i fn args st = Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.MissingStackSize), (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, i)), List.Nil)))) (ge0.stack_sizes i))) (fun stack_size -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (p.spp'.msu_pars.setup_call stack_size fn.Joint.joint_if_params args st)) (fun st' -> Monad.m_return0 (Monad.max_def Errors.res0) (increment_stack_usage p.spp'.msu_pars.st_pars stack_size st'))) (** val is_inl : ('a1, 'a2) Types.sum -> Bool.bool **) let is_inl = function | Types.Inl x0 -> Bool.True | Types.Inr x0 -> Bool.False (** val eval_call : sem_params -> AST.ident List.list -> genv -> (PreIdentifiers.identifier, (__, __) Types.prod) Types.sum -> __ -> __ -> __ -> state_pc -> __ **) let eval_call p globals ge0 f args dest nxt st = Monad.m_bind0 (Monad.max_def IOMonad.iOMonad) (let x = IOMonad.err_to_io (Obj.magic (block_of_call p globals ge0 f st.st_no_pc)) in Obj.magic x) (fun bl -> Monad.m_bind2 (Monad.max_def IOMonad.iOMonad) (let x = IOMonad.err_to_io (fetch_function globals ge0 bl) in Obj.magic x) (fun i fd -> match fd with | AST.Internal ifd -> Obj.magic (IOMonad.err_to_io (Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (p.spp'.msu_pars.save_frame (kind_of_call (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp) f) dest st)) (fun st' -> Monad.m_bind0 (Monad.max_def Errors.res0) (eval_internal_call p globals ge0 i (Types.pi1 ifd) args st') (fun st'' -> let pc0 = pc_of_point p bl (Types.pi1 ifd).Joint.joint_if_entry in Monad.m_return0 (Monad.max_def Errors.res0) { st_no_pc = st''; pc = pc0; last_pop = st.last_pop }))))) | AST.External efd -> Monad.m_bind0 (Monad.max_def IOMonad.iOMonad) (eval_external_call p efd args dest st.st_no_pc) (fun st' -> Monad.m_return0 (Monad.max_def IOMonad.iOMonad) { st_no_pc = st'; pc = (succ_pc p st.pc nxt); last_pop = st.last_pop }))) (** val eval_statement_no_pc : sem_params -> AST.ident List.list -> genv -> AST.ident -> Joint.joint_statement -> state -> state Errors.res **) let eval_statement_no_pc p globals ge0 curr_id s st = match s with | Joint.Sequential (s0, next0) -> (match s0 with | Joint.COST_LABEL x -> Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st) | Joint.CALL (x, x0, x1) -> Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st) | Joint.COND (x, x0) -> Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st) | Joint.Step_seq s1 -> eval_seq_no_pc p globals ge0 curr_id s1 st) | Joint.Final x -> Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st) | Joint.FCOND (x0, x1, x2) -> Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) st) (** val eval_return : sem_params -> AST.ident List.list -> genv -> PreIdentifiers.identifier -> __ -> state -> __ **) let eval_return p globals ge0 curr_id curr_ret st = Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.MissingStackSize), (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, curr_id)), List.Nil)))) (ge0.stack_sizes curr_id))) (fun stack_size -> Monad.m_bind2 (Monad.max_def Errors.res0) (Obj.magic (p.spp'.msu_pars.pop_frame globals ge0 curr_id curr_ret st)) (fun st' call_pc -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (next_of_call_pc p globals ge0 call_pc)) (fun nxt -> let st'' = set_last_pop p.spp'.msu_pars.st_pars (decrement_stack_usage p.spp'.msu_pars.st_pars stack_size st') call_pc in Monad.m_return0 (Monad.max_def Errors.res0) (next p nxt st'')))) (** val eval_tailcall : sem_params -> AST.ident List.list -> genv -> (PreIdentifiers.identifier, (__, __) Types.prod) Types.sum -> __ -> PreIdentifiers.identifier -> __ -> state_pc -> __ **) let eval_tailcall p globals ge0 f args curr_f curr_ret st = Monad.m_bind0 (Monad.max_def IOMonad.iOMonad) (let x = IOMonad.err_to_io (Obj.magic (block_of_call p globals ge0 f st.st_no_pc)) in Obj.magic x) (fun bl -> Monad.m_bind2 (Monad.max_def IOMonad.iOMonad) (let x = IOMonad.err_to_io (fetch_function globals ge0 bl) in Obj.magic x) (fun i fd -> match fd with | AST.Internal ifd -> Obj.magic (IOMonad.err_to_io (Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.MissingStackSize), (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, curr_f)), List.Nil)))) (ge0.stack_sizes curr_f))) (fun stack_size -> let st' = decrement_stack_usage (spp'__o__msu_pars__o__st_pars p) stack_size st.st_no_pc in Monad.m_bind0 (Monad.max_def Errors.res0) (eval_internal_call p globals ge0 i (Types.pi1 ifd) args st') (fun st'' -> let pc0 = pc_of_point p bl (Types.pi1 ifd).Joint.joint_if_entry in Monad.m_return0 (Monad.max_def Errors.res0) { st_no_pc = st''; pc = pc0; last_pop = st.last_pop }))))) | AST.External efd -> Monad.m_bind0 (Monad.max_def IOMonad.iOMonad) (eval_external_call p efd args curr_ret st.st_no_pc) (fun st' -> Obj.magic (IOMonad.err_to_io (Obj.magic (eval_return p globals ge0 curr_f curr_ret st.st_no_pc)))))) (** val eval_statement_advance : sem_params -> AST.ident List.list -> genv -> AST.ident -> Joint.joint_closed_internal_function -> Joint.joint_statement -> state_pc -> (IO.io_out, IO.io_in, state_pc) IOMonad.iO **) let eval_statement_advance p g ge0 curr_id curr_fn s st = match s with | Joint.Sequential (s0, nxt) -> (match s0 with | Joint.COST_LABEL x -> Obj.magic (Monad.m_return0 (Monad.max_def IOMonad.iOMonad) (next p nxt st)) | Joint.CALL (f, args, dest) -> Obj.magic (eval_call p g ge0 f args dest nxt st) | Joint.COND (a, l) -> IOMonad.err_to_io (Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (acca_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp) p.spp'.msu_pars st.st_no_pc a)) (fun v -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (ByteValues.bool_of_beval v)) (fun b -> match b with | Bool.True -> Obj.magic (goto p g ge0 l st) | Bool.False -> Monad.m_return0 (Monad.max_def Errors.res0) (next p nxt st))))) | Joint.Step_seq x -> Obj.magic (Monad.m_return0 (Monad.max_def IOMonad.iOMonad) (next p nxt st))) | Joint.Final s0 -> let curr_ret = (Types.pi1 curr_fn).Joint.joint_if_result in (match s0 with | Joint.GOTO l -> IOMonad.err_to_io (goto p g ge0 l st) | Joint.RETURN -> IOMonad.err_to_io (Obj.magic (eval_return p g ge0 curr_id curr_ret st.st_no_pc)) | Joint.TAILCALL (f, args) -> Obj.magic (eval_tailcall p g ge0 f args curr_id curr_ret st)) | Joint.FCOND (a, lbltrue, lblfalse) -> IOMonad.err_to_io (Obj.magic (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (acca_retrieve (Joint.stmt_pars__o__uns_pars__o__u_pars p.spp'.spp) p.spp'.msu_pars st.st_no_pc a)) (fun v -> Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic (ByteValues.bool_of_beval v)) (fun b -> match b with | Bool.True -> Obj.magic (goto p g ge0 lbltrue st) | Bool.False -> Obj.magic (goto p g ge0 lblfalse st))))) (** val eval_state : sem_params -> AST.ident List.list -> genv -> state_pc -> (IO.io_out, IO.io_in, state_pc) IOMonad.iO **) let eval_state p globals ge0 st = Obj.magic (Monad.m_bind3 (Monad.max_def IOMonad.iOMonad) (let x = IOMonad.err_to_io (fetch_statement p globals ge0 st.pc) in Obj.magic x) (fun id fn s -> Monad.m_bind0 (Monad.max_def IOMonad.iOMonad) (let x = IOMonad.err_to_io (eval_statement_no_pc p globals ge0 id s st.st_no_pc) in Obj.magic x) (fun st' -> let st'' = set_no_pc (spp'__o__msu_pars__o__st_pars p) st' st in Obj.magic (eval_statement_advance p globals ge0 id fn s st''))))