open Preamble open Deqsets open Setoids open Monad open Option open Extranat open Vector open Div_and_mod open Jmeq open Russell open List open Util open FoldStuff open Bool open Relations open Nat open BitVector open Hints_declaration open Core_notation open Pts open Logic open Types open BitVectorTrie open BitVectorTrieSet open State open String open Exp open Arithmetic open Integers open AST open LabelledObjects open Proper open PositiveMap open ErrorMessages open PreIdentifiers open Errors open Extralib open Lists open Positive open Identifiers open CostLabel open ASM open Extra_bool open Coqlib open Values open FrontEndVal open GenMem open FrontEndMem open Globalenvs open Sets open Listb open Graphs open I8051 open Order open Registers open Hide open Division open Z open BitVectorZ open Pointers open ByteValues open BackEndOps open Joint open Joint_LTL_LIN open LIN type aSM_universe = { id_univ : Identifiers.universe; current_funct : AST.ident; ident_map : ASM.identifier Identifiers.identifier_map; label_map : ASM.identifier Identifiers.identifier_map Identifiers.identifier_map; fresh_cost_label : Positive.pos } (** val aSM_universe_rect_Type4 : (Identifiers.universe -> AST.ident -> ASM.identifier Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **) let rec aSM_universe_rect_Type4 h_mk_ASM_universe x_588 = let { id_univ = id_univ0; current_funct = current_funct0; ident_map = ident_map0; label_map = label_map0; fresh_cost_label = fresh_cost_label0 } = x_588 in h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 fresh_cost_label0 (** val aSM_universe_rect_Type5 : (Identifiers.universe -> AST.ident -> ASM.identifier Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **) let rec aSM_universe_rect_Type5 h_mk_ASM_universe x_590 = let { id_univ = id_univ0; current_funct = current_funct0; ident_map = ident_map0; label_map = label_map0; fresh_cost_label = fresh_cost_label0 } = x_590 in h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 fresh_cost_label0 (** val aSM_universe_rect_Type3 : (Identifiers.universe -> AST.ident -> ASM.identifier Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **) let rec aSM_universe_rect_Type3 h_mk_ASM_universe x_592 = let { id_univ = id_univ0; current_funct = current_funct0; ident_map = ident_map0; label_map = label_map0; fresh_cost_label = fresh_cost_label0 } = x_592 in h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 fresh_cost_label0 (** val aSM_universe_rect_Type2 : (Identifiers.universe -> AST.ident -> ASM.identifier Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **) let rec aSM_universe_rect_Type2 h_mk_ASM_universe x_594 = let { id_univ = id_univ0; current_funct = current_funct0; ident_map = ident_map0; label_map = label_map0; fresh_cost_label = fresh_cost_label0 } = x_594 in h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 fresh_cost_label0 (** val aSM_universe_rect_Type1 : (Identifiers.universe -> AST.ident -> ASM.identifier Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **) let rec aSM_universe_rect_Type1 h_mk_ASM_universe x_596 = let { id_univ = id_univ0; current_funct = current_funct0; ident_map = ident_map0; label_map = label_map0; fresh_cost_label = fresh_cost_label0 } = x_596 in h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 fresh_cost_label0 (** val aSM_universe_rect_Type0 : (Identifiers.universe -> AST.ident -> ASM.identifier Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map Identifiers.identifier_map -> Positive.pos -> 'a1) -> aSM_universe -> 'a1 **) let rec aSM_universe_rect_Type0 h_mk_ASM_universe x_598 = let { id_univ = id_univ0; current_funct = current_funct0; ident_map = ident_map0; label_map = label_map0; fresh_cost_label = fresh_cost_label0 } = x_598 in h_mk_ASM_universe id_univ0 current_funct0 ident_map0 label_map0 fresh_cost_label0 (** val id_univ : aSM_universe -> Identifiers.universe **) let rec id_univ xxx = xxx.id_univ (** val current_funct : aSM_universe -> AST.ident **) let rec current_funct xxx = xxx.current_funct (** val ident_map : aSM_universe -> ASM.identifier Identifiers.identifier_map **) let rec ident_map xxx = xxx.ident_map (** val label_map : aSM_universe -> ASM.identifier Identifiers.identifier_map Identifiers.identifier_map **) let rec label_map xxx = xxx.label_map (** val fresh_cost_label : aSM_universe -> Positive.pos **) let rec fresh_cost_label xxx = xxx.fresh_cost_label (** val aSM_universe_inv_rect_Type4 : aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1 **) let aSM_universe_inv_rect_Type4 hterm h1 = let hcut = aSM_universe_rect_Type4 h1 hterm in hcut __ (** val aSM_universe_inv_rect_Type3 : aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1 **) let aSM_universe_inv_rect_Type3 hterm h1 = let hcut = aSM_universe_rect_Type3 h1 hterm in hcut __ (** val aSM_universe_inv_rect_Type2 : aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1 **) let aSM_universe_inv_rect_Type2 hterm h1 = let hcut = aSM_universe_rect_Type2 h1 hterm in hcut __ (** val aSM_universe_inv_rect_Type1 : aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1 **) let aSM_universe_inv_rect_Type1 hterm h1 = let hcut = aSM_universe_rect_Type1 h1 hterm in hcut __ (** val aSM_universe_inv_rect_Type0 : aSM_universe -> (Identifiers.universe -> AST.ident -> ASM.identifier Identifiers.identifier_map -> ASM.identifier Identifiers.identifier_map Identifiers.identifier_map -> Positive.pos -> __ -> 'a1) -> 'a1 **) let aSM_universe_inv_rect_Type0 hterm h1 = let hcut = aSM_universe_rect_Type0 h1 hterm in hcut __ (** val aSM_universe_discr : aSM_universe -> aSM_universe -> __ **) let aSM_universe_discr x y = Logic.eq_rect_Type2 x (let { id_univ = a0; current_funct = a1; ident_map = a2; label_map = a3; fresh_cost_label = a4 } = x in Obj.magic (fun _ dH -> dH __ __ __ __ __)) y (** val aSM_universe_jmdiscr : aSM_universe -> aSM_universe -> __ **) let aSM_universe_jmdiscr x y = Logic.eq_rect_Type2 x (let { id_univ = a0; current_funct = a1; ident_map = a2; label_map = a3; fresh_cost_label = a4 } = x in Obj.magic (fun _ dH -> dH __ __ __ __ __)) y (** val report_cost : CostLabel.costlabel -> Types.unit0 Monad.smax_def__o__monad **) let report_cost cl = Obj.magic (fun u -> let clw = Identifiers.word_of_identifier PreIdentifiers.CostTag cl in (match Positive.leb u.fresh_cost_label clw with | Bool.True -> { Types.fst = { id_univ = u.id_univ; current_funct = u.current_funct; ident_map = u.ident_map; label_map = u.label_map; fresh_cost_label = (Positive.succ clw) }; Types.snd = Types.It } | Bool.False -> { Types.fst = u; Types.snd = Types.It })) (** val identifier_of_label : Graphs.label -> ASM.identifier Monad.smax_def__o__monad **) let identifier_of_label l = Obj.magic (fun u -> let current = u.current_funct in let lmap = Identifiers.lookup_def PreIdentifiers.SymbolTag u.label_map current (Identifiers.empty_map PreIdentifiers.LabelTag) in let { Types.fst = eta2825; Types.snd = lmap0 } = match Identifiers.lookup PreIdentifiers.LabelTag lmap l with | Types.None -> let { Types.fst = id; Types.snd = univ } = Identifiers.fresh PreIdentifiers.ASMTag u.id_univ in { Types.fst = { Types.fst = id; Types.snd = univ }; Types.snd = (Identifiers.add PreIdentifiers.LabelTag lmap l id) } | Types.Some id -> { Types.fst = { Types.fst = id; Types.snd = u.id_univ }; Types.snd = lmap } in let { Types.fst = id; Types.snd = univ } = eta2825 in { Types.fst = { id_univ = univ; current_funct = current; ident_map = u.ident_map; label_map = (Identifiers.add PreIdentifiers.SymbolTag u.label_map current lmap0); fresh_cost_label = u.fresh_cost_label }; Types.snd = id }) (** val identifier_of_ident : AST.ident -> ASM.identifier Monad.smax_def__o__monad **) let identifier_of_ident i = Obj.magic (fun u -> let imap = u.ident_map in let res = match Identifiers.lookup PreIdentifiers.SymbolTag imap i with | Types.None -> let { Types.fst = id; Types.snd = univ } = Identifiers.fresh PreIdentifiers.ASMTag u.id_univ in { Types.fst = { Types.fst = id; Types.snd = univ }; Types.snd = (Identifiers.add PreIdentifiers.SymbolTag imap i id) } | Types.Some id -> { Types.fst = { Types.fst = id; Types.snd = u.id_univ }; Types.snd = imap } in let id = res.Types.fst.Types.fst in let univ = res.Types.fst.Types.snd in let imap0 = res.Types.snd in { Types.fst = { id_univ = univ; current_funct = u.current_funct; ident_map = imap0; label_map = u.label_map; fresh_cost_label = u.fresh_cost_label }; Types.snd = id }) (** val new_ASM_universe : Joint.joint_program -> aSM_universe **) let new_ASM_universe p = { id_univ = Positive.One; current_funct = Positive.One; ident_map = (Identifiers.empty_map PreIdentifiers.SymbolTag); label_map = (Identifiers.empty_map PreIdentifiers.SymbolTag); fresh_cost_label = Positive.One } (** val start_funct_translation : AST.ident List.list -> AST.ident List.list -> (AST.ident, Joint.joint_function) Types.prod -> Types.unit0 Monad.smax_def__o__monad **) let start_funct_translation g functs id_f = Obj.magic (fun u -> { Types.fst = { id_univ = u.id_univ; current_funct = id_f.Types.fst; ident_map = u.ident_map; label_map = u.label_map; fresh_cost_label = u.fresh_cost_label }; Types.snd = Types.It }) (** val aSM_fresh : ASM.identifier Monad.smax_def__o__monad **) let aSM_fresh = Obj.magic (fun u -> let { Types.fst = id; Types.snd = univ } = Identifiers.fresh PreIdentifiers.ASMTag u.id_univ in { Types.fst = { id_univ = univ; current_funct = u.current_funct; ident_map = u.ident_map; label_map = u.label_map; fresh_cost_label = u.fresh_cost_label }; Types.snd = id }) (** val register_address : I8051.register -> ASM.subaddressing_mode **) let register_address r = (match r with | I8051.Register00 -> (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty))))))) | I8051.Register01 -> (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty))))))) | I8051.Register02 -> (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty))))))) | I8051.Register03 -> (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty))))))) | I8051.Register04 -> (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty))))))) | I8051.Register05 -> (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty))))))) | I8051.Register06 -> (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty))))))) | I8051.Register07 -> (fun _ -> ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty))))))) | I8051.Register10 -> (fun _ -> ASM.DIRECT (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) | I8051.Register11 -> (fun _ -> ASM.DIRECT (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) | I8051.Register12 -> (fun _ -> ASM.DIRECT (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) | I8051.Register13 -> (fun _ -> ASM.DIRECT (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) | I8051.Register14 -> (fun _ -> ASM.DIRECT (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) | I8051.Register15 -> (fun _ -> ASM.DIRECT (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) | I8051.Register16 -> (fun _ -> ASM.DIRECT (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) | I8051.Register17 -> (fun _ -> ASM.DIRECT (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) | I8051.Register20 -> (fun _ -> ASM.DIRECT (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) | I8051.Register21 -> (fun _ -> ASM.DIRECT (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) | I8051.Register22 -> (fun _ -> ASM.DIRECT (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) | I8051.Register23 -> (fun _ -> ASM.DIRECT (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) | I8051.Register24 -> (fun _ -> ASM.DIRECT (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) | I8051.Register25 -> (fun _ -> ASM.DIRECT (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) | I8051.Register26 -> (fun _ -> ASM.DIRECT (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) | I8051.Register27 -> (fun _ -> ASM.DIRECT (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) | I8051.Register30 -> (fun _ -> ASM.DIRECT (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) | I8051.Register31 -> (fun _ -> ASM.DIRECT (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) | I8051.Register32 -> (fun _ -> ASM.DIRECT (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) | I8051.Register33 -> (fun _ -> ASM.DIRECT (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) | I8051.Register34 -> (fun _ -> ASM.DIRECT (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) | I8051.Register35 -> (fun _ -> ASM.DIRECT (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) | I8051.Register36 -> (fun _ -> ASM.DIRECT (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) | I8051.Register37 -> (fun _ -> ASM.DIRECT (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r))) | I8051.RegisterA -> (fun _ -> ASM.ACC_A) | I8051.RegisterB -> (fun _ -> ASM.DIRECT (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) | I8051.RegisterDPL -> (fun _ -> ASM.DIRECT (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) | I8051.RegisterDPH -> (fun _ -> ASM.DIRECT (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) | I8051.RegisterCarry -> (fun _ -> ASM.DIRECT (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (I8051.nat_of_register r)))) __ (** val vector_cast : Nat.nat -> Nat.nat -> 'a1 -> 'a1 Vector.vector -> 'a1 Vector.vector **) let vector_cast n m dflt v = Util.if_then_else_safe (Nat.leb n m) (fun _ -> Vector.append (Nat.minus m n) n (Vector.replicate (Nat.minus m n) dflt) v) (fun _ -> (Vector.vsplit (Nat.minus n m) m v).Types.snd) (** val arg_address : Joint.hdw_argument -> ASM.subaddressing_mode **) let arg_address = function | Joint.Reg r -> let x = ASM.subaddressing_modeel__o__mk_subaddressing_mode (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Registr, Vector.VEmpty)))))) (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Registr, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))))))) (register_address r) in x | Joint.Imm v -> let x = ASM.DATA v in x type lin_statement = Joint.joint_statement LabelledObjects.labelled_obj (** val data_of_int : BitVector.byte -> ASM.addressing_mode **) let data_of_int bv = ASM.DATA bv (** val data16_of_int : Nat.nat -> ASM.addressing_mode **) let data16_of_int bv = ASM.DATA16 (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) bv) (** val accumulator_address : ASM.addressing_mode **) let accumulator_address = ASM.DIRECT (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (** val asm_other_bit : ASM.addressing_mode **) let asm_other_bit = ASM.BIT_ADDR Joint.zero_byte (** val one_word : BitVector.word **) let one_word = Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))) (Nat.S Nat.O) (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty)) (** val translate_statements : AST.ident List.list -> Joint.joint_statement -> ASM.pseudo_instruction Monad.smax_def__o__monad **) let translate_statements globals = function | Joint.Sequential (instr, x) -> (match instr with | Joint.COST_LABEL lbl -> Monad.m_bind0 (Monad.smax_def State.state_monad) (report_cost lbl) (fun x0 -> Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Cost lbl)) | Joint.CALL (f, x0, x1) -> (match f with | Types.Inl id -> Monad.m_bind0 (Monad.smax_def State.state_monad) (identifier_of_ident id) (fun id' -> Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Call (ASM.toASM_ident PreIdentifiers.ASMTag id'))) | Types.Inr x2 -> Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction (ASM.JMP ASM.ACC_DPTR))) | Joint.COND (x0, lbl) -> Monad.m_bind0 (Monad.smax_def State.state_monad) (identifier_of_label lbl) (fun l -> Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction (ASM.JNZ l))) | Joint.Step_seq instr' -> (match instr' with | Joint.COMMENT comment -> Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Comment comment) | Joint.MOVE regs -> Monad.m_return0 (Monad.smax_def State.state_monad) (match Obj.magic regs with | Joint_LTL_LIN.From_acc (reg, x0) -> (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Registr, Vector.VEmpty)))))) (register_address reg) with | ASM.DIRECT d -> (fun _ -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst = (ASM.DIRECT d); Types.snd = ASM.ACC_A })))))) | ASM.INDIRECT x1 -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x1 -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER r -> (fun _ -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst = (ASM.REGISTER r); Types.snd = ASM.ACC_A }))))))) | ASM.ACC_A -> (fun _ -> ASM.Instruction ASM.NOP) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x1 -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x1 -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.CARRY -> (fun _ -> assert false (* absurd case *)) | ASM.BIT_ADDR x1 -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x1 -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x1 -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x1 -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x1 -> (fun _ -> assert false (* absurd case *))) __ | Joint_LTL_LIN.To_acc (x0, reg) -> (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Registr, Vector.VEmpty)))))) (register_address reg) with | ASM.DIRECT d -> (fun _ -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.DIRECT d) }))))))) | ASM.INDIRECT x1 -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x1 -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER r -> (fun _ -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.REGISTER r) }))))))) | ASM.ACC_A -> (fun _ -> ASM.Instruction ASM.NOP) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x1 -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x1 -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.CARRY -> (fun _ -> assert false (* absurd case *)) | ASM.BIT_ADDR x1 -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x1 -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x1 -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x1 -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x1 -> (fun _ -> assert false (* absurd case *))) __ | Joint_LTL_LIN.Int_to_reg (reg, b) -> (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Registr, Vector.VEmpty)))))) (register_address reg) with | ASM.DIRECT d -> (fun _ -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst = (ASM.DIRECT d); Types.snd = (ASM.DATA b) })))))) | ASM.INDIRECT x0 -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x0 -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER r -> (fun _ -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst = (ASM.REGISTER r); Types.snd = (ASM.DATA b) }))))))) | ASM.ACC_A -> (fun _ -> match BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) b with | Bool.True -> ASM.Instruction (ASM.CLR ASM.ACC_A) | Bool.False -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.DATA b) }))))))) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x0 -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x0 -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.CARRY -> (fun _ -> assert false (* absurd case *)) | ASM.BIT_ADDR x0 -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x0 -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x0 -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x0 -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x0 -> (fun _ -> assert false (* absurd case *))) __ | Joint_LTL_LIN.Int_to_acc (x0, b) -> (match BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) b with | Bool.True -> ASM.Instruction (ASM.CLR ASM.ACC_A) | Bool.False -> ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.DATA b) })))))))) | Joint.POP x0 -> Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction (ASM.POP accumulator_address)) | Joint.PUSH x0 -> Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction (ASM.PUSH accumulator_address)) | Joint.ADDRESS (id, off, x0, x1) -> Monad.m_bind0 (Monad.smax_def State.state_monad) (identifier_of_ident id) (fun id0 -> Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Mov ((Types.Inl ASM.DPTR), id0, off))) | Joint.OPACCS (accs, x0, x1, x2, x3) -> Monad.m_return0 (Monad.smax_def State.state_monad) (match accs with | BackEndOps.Mul -> ASM.Instruction (ASM.MUL (ASM.ACC_A, ASM.ACC_B)) | BackEndOps.DivuModu -> ASM.Instruction (ASM.DIV (ASM.ACC_A, ASM.ACC_B))) | Joint.OP1 (op1, x0, x1) -> Monad.m_return0 (Monad.smax_def State.state_monad) (match op1 with | BackEndOps.Cmpl -> ASM.Instruction (ASM.CPL ASM.ACC_A) | BackEndOps.Inc -> ASM.Instruction (ASM.INC ASM.ACC_A) | BackEndOps.Rl -> ASM.Instruction (ASM.RL ASM.ACC_A)) | Joint.OP2 (op2, x0, x1, reg) -> Monad.m_return0 (Monad.smax_def State.state_monad) ((match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Registr, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))))))) (arg_address (Obj.magic reg)) with | ASM.DIRECT d -> (fun _ -> match op2 with | BackEndOps.Add -> ASM.Instruction (ASM.ADD (ASM.ACC_A, (ASM.DIRECT d))) | BackEndOps.Addc -> ASM.Instruction (ASM.ADDC (ASM.ACC_A, (ASM.DIRECT d))) | BackEndOps.Sub -> ASM.Instruction (ASM.SUBB (ASM.ACC_A, (ASM.DIRECT d))) | BackEndOps.And -> ASM.Instruction (ASM.ANL (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.DIRECT d) }))) | BackEndOps.Or -> ASM.Instruction (ASM.ORL (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.DIRECT d) }))) | BackEndOps.Xor -> ASM.Instruction (ASM.XRL (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.DIRECT d) }))) | ASM.INDIRECT x2 -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x2 -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER r -> (fun _ -> match op2 with | BackEndOps.Add -> ASM.Instruction (ASM.ADD (ASM.ACC_A, (ASM.REGISTER r))) | BackEndOps.Addc -> ASM.Instruction (ASM.ADDC (ASM.ACC_A, (ASM.REGISTER r))) | BackEndOps.Sub -> ASM.Instruction (ASM.SUBB (ASM.ACC_A, (ASM.REGISTER r))) | BackEndOps.And -> ASM.Instruction (ASM.ANL (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.REGISTER r) }))) | BackEndOps.Or -> ASM.Instruction (ASM.ORL (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.REGISTER r) }))) | BackEndOps.Xor -> ASM.Instruction (ASM.XRL (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.REGISTER r) }))) | ASM.ACC_A -> (fun _ -> match op2 with | BackEndOps.Add -> ASM.Instruction (ASM.ADD (ASM.ACC_A, accumulator_address)) | BackEndOps.Addc -> ASM.Instruction (ASM.ADDC (ASM.ACC_A, accumulator_address)) | BackEndOps.Sub -> ASM.Instruction (ASM.SUBB (ASM.ACC_A, accumulator_address)) | BackEndOps.And -> ASM.Instruction ASM.NOP | BackEndOps.Or -> ASM.Instruction ASM.NOP | BackEndOps.Xor -> ASM.Instruction (ASM.CLR ASM.ACC_A)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA b -> (fun _ -> match op2 with | BackEndOps.Add -> ASM.Instruction (ASM.ADD (ASM.ACC_A, (ASM.DATA b))) | BackEndOps.Addc -> ASM.Instruction (ASM.ADDC (ASM.ACC_A, (ASM.DATA b))) | BackEndOps.Sub -> ASM.Instruction (ASM.SUBB (ASM.ACC_A, (ASM.DATA b))) | BackEndOps.And -> ASM.Instruction (ASM.ANL (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.DATA b) }))) | BackEndOps.Or -> ASM.Instruction (ASM.ORL (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.DATA b) }))) | BackEndOps.Xor -> ASM.Instruction (ASM.XRL (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.DATA b) }))) | ASM.DATA16 x2 -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.CARRY -> (fun _ -> assert false (* absurd case *)) | ASM.BIT_ADDR x2 -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x2 -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x2 -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x2 -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x2 -> (fun _ -> assert false (* absurd case *))) __) | Joint.CLEAR_CARRY -> Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction (ASM.CLR ASM.CARRY)) | Joint.SET_CARRY -> Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction (ASM.SETB ASM.CARRY)) | Joint.LOAD (x0, x1, x2) -> Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction (ASM.MOVX (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = ASM.EXT_INDIRECT_DPTR }))) | Joint.STORE (x0, x1, x2) -> Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction (ASM.MOVX (Types.Inr { Types.fst = ASM.EXT_INDIRECT_DPTR; Types.snd = ASM.ACC_A }))) | Joint.Extension_seq ext -> (match Obj.magic ext with | Joint_LTL_LIN.SAVE_CARRY -> Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction (ASM.MOV (Types.Inr { Types.fst = asm_other_bit; Types.snd = ASM.CARRY }))) | Joint_LTL_LIN.RESTORE_CARRY -> Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction (ASM.MOV (Types.Inl (Types.Inr { Types.fst = ASM.CARRY; Types.snd = asm_other_bit })))) | Joint_LTL_LIN.LOW_ADDRESS lbl -> Monad.m_bind0 (Monad.smax_def State.state_monad) (identifier_of_label lbl) (fun lbl' -> Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Mov ((Types.Inr { Types.fst = (register_address I8051.RegisterA); Types.snd = ASM.LOW }), lbl', one_word))) | Joint_LTL_LIN.HIGH_ADDRESS lbl -> Monad.m_bind0 (Monad.smax_def State.state_monad) (identifier_of_label lbl) (fun lbl' -> Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Mov ((Types.Inr { Types.fst = (register_address I8051.RegisterA); Types.snd = ASM.HIGH }), lbl', one_word)))))) | Joint.Final instr -> (match instr with | Joint.GOTO lbl -> Monad.m_bind0 (Monad.smax_def State.state_monad) (identifier_of_label lbl) (fun lbl' -> Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Jmp (ASM.toASM_ident PreIdentifiers.ASMTag lbl'))) | Joint.RETURN -> Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Instruction ASM.RET) | Joint.TAILCALL (x, x0) -> assert false (* absurd case *)) | Joint.FCOND (x0, lbl_true, lbl_false) -> Monad.m_bind0 (Monad.smax_def State.state_monad) (identifier_of_label lbl_true) (fun l1 -> Monad.m_bind0 (Monad.smax_def State.state_monad) (identifier_of_label lbl_false) (fun l2 -> Monad.m_return0 (Monad.smax_def State.state_monad) (ASM.Jnz (ASM.ACC_A, l1, l2)))) (** val build_translated_statement : AST.ident List.list -> lin_statement -> __ **) let build_translated_statement globals statement = Monad.m_bind0 (Monad.smax_def State.state_monad) (translate_statements globals statement.Types.snd) (fun stmt -> match statement.Types.fst with | Types.None -> Monad.m_return0 (Monad.smax_def State.state_monad) { Types.fst = Types.None; Types.snd = stmt } | Types.Some lbl -> Monad.m_bind0 (Monad.smax_def State.state_monad) (identifier_of_label lbl) (fun lbl' -> Monad.m_return0 (Monad.smax_def State.state_monad) { Types.fst = (Types.Some lbl'); Types.snd = stmt })) (** val translate_code : AST.ident List.list -> lin_statement List.list -> __ **) let translate_code globals code = Monad.m_list_map (Monad.smax_def State.state_monad) (build_translated_statement globals) code (** val translate_fun_def : AST.ident List.list -> AST.ident List.list -> (AST.ident, Joint.joint_function) Types.prod -> __ **) let translate_fun_def globals functions id_def = Monad.m_bind0 (Monad.smax_def State.state_monad) (start_funct_translation globals functions id_def) (fun x -> match id_def.Types.snd with | AST.Internal int -> let code = (Types.pi1 int).Joint.joint_if_code in Monad.m_bind0 (Monad.smax_def State.state_monad) (identifier_of_ident id_def.Types.fst) (fun id -> Monad.m_bind0 (Monad.smax_def State.state_monad) (translate_code (List.append functions globals) (Obj.magic code)) (fun code' -> match code' with | List.Nil -> Monad.m_return0 (Monad.smax_def State.state_monad) (List.Cons ({ Types.fst = (Types.Some id); Types.snd = (ASM.Instruction ASM.RET) }, List.Nil)) | List.Cons (hd, tl) -> (match hd.Types.fst with | Types.None -> Monad.m_return0 (Monad.smax_def State.state_monad) (List.Cons ({ Types.fst = (Types.Some id); Types.snd = hd.Types.snd }, tl)) | Types.Some x0 -> Monad.m_return0 (Monad.smax_def State.state_monad) (List.Cons ({ Types.fst = (Types.Some id); Types.snd = (ASM.Instruction ASM.NOP) }, (List.Cons (hd, tl))))))) | AST.External x0 -> Monad.m_return0 (Monad.smax_def State.state_monad) List.Nil) type init_mutable = { virtual_dptr : (ASM.identifier, Z.z) Types.prod; actual_dptr : (ASM.identifier, Z.z) Types.prod; built_code : ASM.labelled_instruction List.list List.list; built_preamble : (ASM.identifier, BitVector.word) Types.prod List.list } (** val init_mutable_rect_Type4 : ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod -> ASM.labelled_instruction List.list List.list -> (ASM.identifier, BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **) let rec init_mutable_rect_Type4 h_mk_init_mutable x_614 = let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built_code = built_code0; built_preamble = built_preamble0 } = x_614 in h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0 (** val init_mutable_rect_Type5 : ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod -> ASM.labelled_instruction List.list List.list -> (ASM.identifier, BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **) let rec init_mutable_rect_Type5 h_mk_init_mutable x_616 = let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built_code = built_code0; built_preamble = built_preamble0 } = x_616 in h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0 (** val init_mutable_rect_Type3 : ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod -> ASM.labelled_instruction List.list List.list -> (ASM.identifier, BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **) let rec init_mutable_rect_Type3 h_mk_init_mutable x_618 = let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built_code = built_code0; built_preamble = built_preamble0 } = x_618 in h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0 (** val init_mutable_rect_Type2 : ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod -> ASM.labelled_instruction List.list List.list -> (ASM.identifier, BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **) let rec init_mutable_rect_Type2 h_mk_init_mutable x_620 = let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built_code = built_code0; built_preamble = built_preamble0 } = x_620 in h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0 (** val init_mutable_rect_Type1 : ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod -> ASM.labelled_instruction List.list List.list -> (ASM.identifier, BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **) let rec init_mutable_rect_Type1 h_mk_init_mutable x_622 = let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built_code = built_code0; built_preamble = built_preamble0 } = x_622 in h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0 (** val init_mutable_rect_Type0 : ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod -> ASM.labelled_instruction List.list List.list -> (ASM.identifier, BitVector.word) Types.prod List.list -> 'a1) -> init_mutable -> 'a1 **) let rec init_mutable_rect_Type0 h_mk_init_mutable x_624 = let { virtual_dptr = virtual_dptr0; actual_dptr = actual_dptr0; built_code = built_code0; built_preamble = built_preamble0 } = x_624 in h_mk_init_mutable virtual_dptr0 actual_dptr0 built_code0 built_preamble0 (** val virtual_dptr : init_mutable -> (ASM.identifier, Z.z) Types.prod **) let rec virtual_dptr xxx = xxx.virtual_dptr (** val actual_dptr : init_mutable -> (ASM.identifier, Z.z) Types.prod **) let rec actual_dptr xxx = xxx.actual_dptr (** val built_code : init_mutable -> ASM.labelled_instruction List.list List.list **) let rec built_code xxx = xxx.built_code (** val built_preamble : init_mutable -> (ASM.identifier, BitVector.word) Types.prod List.list **) let rec built_preamble xxx = xxx.built_preamble (** val init_mutable_inv_rect_Type4 : init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod -> ASM.labelled_instruction List.list List.list -> (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) -> 'a1 **) let init_mutable_inv_rect_Type4 hterm h1 = let hcut = init_mutable_rect_Type4 h1 hterm in hcut __ (** val init_mutable_inv_rect_Type3 : init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod -> ASM.labelled_instruction List.list List.list -> (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) -> 'a1 **) let init_mutable_inv_rect_Type3 hterm h1 = let hcut = init_mutable_rect_Type3 h1 hterm in hcut __ (** val init_mutable_inv_rect_Type2 : init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod -> ASM.labelled_instruction List.list List.list -> (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) -> 'a1 **) let init_mutable_inv_rect_Type2 hterm h1 = let hcut = init_mutable_rect_Type2 h1 hterm in hcut __ (** val init_mutable_inv_rect_Type1 : init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod -> ASM.labelled_instruction List.list List.list -> (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) -> 'a1 **) let init_mutable_inv_rect_Type1 hterm h1 = let hcut = init_mutable_rect_Type1 h1 hterm in hcut __ (** val init_mutable_inv_rect_Type0 : init_mutable -> ((ASM.identifier, Z.z) Types.prod -> (ASM.identifier, Z.z) Types.prod -> ASM.labelled_instruction List.list List.list -> (ASM.identifier, BitVector.word) Types.prod List.list -> __ -> 'a1) -> 'a1 **) let init_mutable_inv_rect_Type0 hterm h1 = let hcut = init_mutable_rect_Type0 h1 hterm in hcut __ (** val init_mutable_discr : init_mutable -> init_mutable -> __ **) let init_mutable_discr x y = Logic.eq_rect_Type2 x (let { virtual_dptr = a0; actual_dptr = a1; built_code = a2; built_preamble = a3 } = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y (** val init_mutable_jmdiscr : init_mutable -> init_mutable -> __ **) let init_mutable_jmdiscr x y = Logic.eq_rect_Type2 x (let { virtual_dptr = a0; actual_dptr = a1; built_code = a2; built_preamble = a3 } = x in Obj.magic (fun _ dH -> dH __ __ __ __)) y (** val store_byte_or_Identifier : (BitVector.byte, (ASM.word_side, ASM.identifier) Types.prod) Types.sum -> init_mutable -> init_mutable **) let store_byte_or_Identifier by mut = let { virtual_dptr = virt; actual_dptr = act; built_code = acc1; built_preamble = acc2 } = mut in let pre = match Identifiers.eq_identifier PreIdentifiers.ASMTag virt.Types.fst act.Types.fst with | Bool.True -> let off = Z.zminus virt.Types.snd act.Types.snd in (match Z.eqZb off Z.OZ with | Bool.True -> List.Nil | Bool.False -> (match Z.eqZb off (Z.z_of_nat (Nat.S Nat.O)) with | Bool.True -> List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction (ASM.INC ASM.DPTR)) }, List.Nil) | Bool.False -> List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Mov ((Types.Inl ASM.DPTR), virt.Types.fst, (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) virt.Types.snd))) }, List.Nil))) | Bool.False -> List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Mov ((Types.Inl ASM.DPTR), virt.Types.fst, (BitVectorZ.bitvector_of_Z (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) virt.Types.snd))) }, List.Nil) in let post = match by with | Types.Inl by0 -> { Types.fst = Types.None; Types.snd = (ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.DATA by0) }))))))) } | Types.Inr si_id -> { Types.fst = Types.None; Types.snd = (ASM.Mov ((Types.Inr { Types.fst = ASM.ACC_A; Types.snd = si_id.Types.fst }), si_id.Types.snd, (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))))) } in { virtual_dptr = { Types.fst = virt.Types.fst; Types.snd = (Z.zsucc virt.Types.snd) }; actual_dptr = virt; built_code = (List.Cons ((List.append pre (List.Cons (post, (List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction (ASM.MOVX (Types.Inr { Types.fst = ASM.EXT_INDIRECT_DPTR; Types.snd = ASM.ACC_A }))) }, List.Nil))))), acc1)); built_preamble = acc2 } (** val do_store_init_data : init_mutable Monad.smax_def__o__monad -> AST.init_data -> init_mutable Monad.smax_def__o__monad **) let do_store_init_data m_mut data = Monad.m_bind0 (Monad.smax_def State.state_monad) m_mut (fun mut -> let store_byte = fun by -> store_byte_or_Identifier (Types.Inl by) in let store_Identifier = fun side id -> store_byte_or_Identifier (Types.Inr { Types.fst = side; Types.snd = id }) in (match data with | AST.Init_int8 n -> Monad.m_return0 (Monad.smax_def State.state_monad) (store_byte n mut) | AST.Init_int16 n -> let { Types.fst = by0; Types.snd = by1 } = Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) n in Monad.m_return0 (Monad.smax_def State.state_monad) (store_byte by1 (store_byte by0 mut)) | AST.Init_int32 n -> let { Types.fst = by0; Types.snd = n0 } = Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))))))))))) n in let { Types.fst = by1; Types.snd = n1 } = Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) n0 in let { Types.fst = by2; Types.snd = by3 } = Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) n1 in Monad.m_return0 (Monad.smax_def State.state_monad) (store_byte by3 (store_byte by2 (store_byte by1 (store_byte by0 mut)))) | AST.Init_space n -> let { Types.fst = virt_id; Types.snd = virt_off } = mut.virtual_dptr in Monad.m_return0 (Monad.smax_def State.state_monad) { virtual_dptr = { Types.fst = virt_id; Types.snd = (Z.zplus (Z.z_of_nat n) virt_off) }; actual_dptr = mut.actual_dptr; built_code = mut.built_code; built_preamble = mut.built_preamble } | AST.Init_null -> let z = BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) in Monad.m_return0 (Monad.smax_def State.state_monad) (store_byte z (store_byte z mut)) | AST.Init_addrof (symb, ofs) -> Monad.m_bind0 (Monad.smax_def State.state_monad) (identifier_of_ident symb) (fun id -> Monad.m_return0 (Monad.smax_def State.state_monad) (store_Identifier ASM.HIGH id (store_Identifier ASM.LOW id mut))))) (** val do_store_global : init_mutable Monad.smax_def__o__monad -> ((AST.ident, AST.region) Types.prod, AST.init_data List.list) Types.prod -> init_mutable Monad.smax_def__o__monad **) let do_store_global m_mut id_reg_data = Monad.m_bind0 (Monad.smax_def State.state_monad) m_mut (fun mut -> let { Types.fst = eta2842; Types.snd = data } = id_reg_data in let { Types.fst = id; Types.snd = reg } = eta2842 in Monad.m_bind0 (Monad.smax_def State.state_monad) (identifier_of_ident id) (fun id0 -> let mut0 = { virtual_dptr = { Types.fst = id0; Types.snd = Z.OZ }; actual_dptr = mut.actual_dptr; built_code = mut.built_code; built_preamble = (List.Cons ({ Types.fst = id0; Types.snd = (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))))))))) (Globalenvs.size_init_data_list data)) }, mut.built_preamble)) } in Util.foldl do_store_init_data (Monad.m_return0 (Monad.smax_def State.state_monad) mut0) data)) (** val reversed_flatten_aux : 'a1 List.list -> 'a1 List.list List.list -> 'a1 List.list **) let rec reversed_flatten_aux acc = function | List.Nil -> acc | List.Cons (hd, tl) -> reversed_flatten_aux (List.append hd acc) tl (** val translate_premain : LIN.lin_program -> ASM.identifier -> (ASM.labelled_instruction List.list, (ASM.identifier, BitVector.word) Types.prod List.list) Types.prod Monad.smax_def__o__monad **) let translate_premain p exit_label = Monad.m_bind0 (Monad.smax_def State.state_monad) (identifier_of_ident p.Joint.joint_prog.AST.prog_main) (fun main -> Monad.m_bind0 (Monad.smax_def State.state_monad) State.state_get (fun u -> let dummy_dptr = { Types.fst = Positive.One; Types.snd = (Z.zopp (Z.z_of_nat (Nat.S Nat.O))) } in let mut = { virtual_dptr = dummy_dptr; actual_dptr = dummy_dptr; built_code = List.Nil; built_preamble = List.Nil } in Monad.m_bind0 (Monad.smax_def State.state_monad) (Util.foldl do_store_global (Monad.m_return0 (Monad.smax_def State.state_monad) mut) p.Joint.joint_prog.AST.prog_vars) (fun globals_init -> let { Types.fst = sph; Types.snd = spl } = Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (BitVectorZ.bitvector_of_Z (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Z.zopp (Z.z_of_nat (Nat.S (Joint.globals_stacksize (Joint.lin_params_to_params LIN.lIN) p))))) in let init_isp = ASM.DATA (Vector.append (Nat.S (Nat.S Nat.O)) (Nat.plus (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (BitVector.zero (Nat.S (Nat.S Nat.O))) (Vector.append (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty)))) (BitVector.maximum (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))) in let isp_direct = ASM.DIRECT (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))) (Nat.S Nat.O) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty))) in let reg_spl = ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty)))))) in let reg_sph = ASM.REGISTER (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty)))))) in Monad.m_return0 (Monad.smax_def State.state_monad) { Types.fst = (List.append (List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Cost p.Joint.init_cost_label) }, (List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst = isp_direct; Types.snd = init_isp })))))) }, (List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst = reg_spl; Types.snd = (ASM.DATA spl) }))))))) }, (List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Instruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst = reg_sph; Types.snd = (ASM.DATA sph) }))))))) }, List.Nil)))))))) (List.append (reversed_flatten_aux List.Nil globals_init.built_code) (List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Call main) }, (List.Cons ({ Types.fst = (Types.Some exit_label); Types.snd = (ASM.Cost u.fresh_cost_label) }, (List.Cons ({ Types.fst = Types.None; Types.snd = (ASM.Jmp exit_label) }, List.Nil)))))))); Types.snd = globals_init.built_preamble }))) (** val get_symboltable : (ASM.identifier, AST.ident) Types.prod List.list Monad.smax_def__o__monad **) let get_symboltable = Obj.magic (fun u -> let imap = u.ident_map in let f = fun iold inew x -> List.Cons ({ Types.fst = inew; Types.snd = iold }, x) in { Types.fst = u; Types.snd = (Identifiers.foldi PreIdentifiers.SymbolTag f imap List.Nil) }) (** val lin_to_asm : LIN.lin_program -> ASM.pseudo_assembly_program Types.option **) let lin_to_asm p = State.state_run (new_ASM_universe p) (let add_translation = fun acc id_def -> Monad.m_bind0 (Monad.smax_def State.state_monad) (translate_fun_def p.Joint.jp_functions (List.map (fun x -> x.Types.fst.Types.fst) p.Joint.joint_prog.AST.prog_vars) id_def) (fun code -> Monad.m_bind0 (Monad.smax_def State.state_monad) acc (fun acc0 -> Monad.m_return0 (Monad.smax_def State.state_monad) (List.append code acc0))) in Monad.m_bind0 (Monad.smax_def State.state_monad) aSM_fresh (fun exit_label -> Monad.m_bind0 (Monad.smax_def State.state_monad) (Util.foldl add_translation (Monad.m_return0 (Monad.smax_def State.state_monad) List.Nil) p.Joint.joint_prog.AST.prog_funct) (fun code -> Monad.m_bind0 (Monad.smax_def State.state_monad) get_symboltable (fun symboltable -> Monad.m_bind2 (Monad.smax_def State.state_monad) (translate_premain p exit_label) (fun init preamble -> Monad.m_return0 (Monad.smax_def State.state_monad) (let code0 = List.append init code in Monad.m_bind0 (Monad.max_def Option.option) (Obj.magic (ASM.code_size_opt code0)) (fun _ -> Monad.m_return0 (Monad.max_def Option.option) { ASM.preamble = preamble; ASM.code = code0; ASM.renamed_symbols = symboltable; ASM.final_label = exit_label })))))))