open Preamble open Types open Hints_declaration open Core_notation open Pts open Logic open Jmeq open Russell open Exp open Setoids open Monad open Option open Extranat open Vector open Div_and_mod open List open Util open FoldStuff open Bool open Relations open Nat open BitVector open Arithmetic open BitVectorTrie open String open Integers open AST open LabelledObjects open Proper open PositiveMap open Deqsets open ErrorMessages open PreIdentifiers open Errors open Extralib open Lists open Positive open Identifiers open CostLabel open ASM (** val inefficient_address_of_label : ASM.labelled_instruction List.list -> ASM.identifier -> Nat.nat **) let inefficient_address_of_label instr_list id = LabelledObjects.index_of (LabelledObjects.instruction_matches_identifier PreIdentifiers.ASMTag id) instr_list type label_map = Nat.nat Identifiers.identifier_map (** val create_label_cost_map0 : ASM.labelled_instruction List.list -> (label_map, ASM.costlabel_map) Types.prod Types.sig0 **) let create_label_cost_map0 program = (Types.pi1 (FoldStuff.foldl_strong program (fun prefix x tl _ labels_costs_ppc -> (let { Types.fst = eta19; Types.snd = ppc } = Types.pi1 labels_costs_ppc in (fun _ -> (let { Types.fst = labels; Types.snd = costs } = eta19 in (fun _ -> (let { Types.fst = label; Types.snd = instr } = x in (fun _ -> let labels1 = match label with | Types.None -> labels | Types.Some l -> Identifiers.add PreIdentifiers.ASMTag labels l ppc in let costs1 = match instr with | ASM.Instruction x0 -> costs | ASM.Comment x0 -> costs | ASM.Cost cost -> BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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)))))))))))))))) (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)))))))))))))))) ppc) cost costs | ASM.Jmp x0 -> costs | ASM.Jnz (x0, x1, x2) -> costs | ASM.Call x0 -> costs | ASM.Mov (x0, x1, x2) -> costs in { Types.fst = { Types.fst = labels1; Types.snd = costs1 }; Types.snd = (Nat.S ppc) })) __)) __)) __) { Types.fst = { Types.fst = (Identifiers.empty_map PreIdentifiers.ASMTag); Types.snd = (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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))))))))))))))))) }; Types.snd = Nat.O })).Types.fst (** val create_label_cost_map : ASM.labelled_instruction List.list -> (label_map, ASM.costlabel_map) Types.prod **) let create_label_cost_map program = Types.pi1 (create_label_cost_map0 program) (** val address_of_word_labels : ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.word **) let address_of_word_labels program id = let labels = (create_label_cost_map program).Types.fst in let address_of_label = fun l -> Identifiers.lookup_def PreIdentifiers.ASMTag labels l Nat.O in 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)))))))))))))))) (address_of_label id) (** val prod_inv_rect_Type0 : ('a1, 'a2) Types.prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **) let prod_inv_rect_Type0 clearme = let { Types.fst = fst; Types.snd = snd } = clearme in (fun auto -> auto fst snd __) (** val fetch0 : BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word -> BitVector.byte -> ((ASM.instruction, BitVector.word) Types.prod, Nat.nat) Types.prod **) let fetch0 pmem pc v = let { Types.fst = b; Types.snd = v0 } = Vector.head (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))) v in (match b with | Bool.True -> let { Types.fst = b0; Types.snd = v1 } = Vector.head (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) v0 in (match b0 with | Bool.True -> let { Types.fst = b1; Types.snd = v2 } = Vector.head (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) v1 in (match b1 with | Bool.True -> let { Types.fst = b2; Types.snd = v3 } = Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2 in (match b2 with | Bool.True -> let { Types.fst = b3; Types.snd = v4 } = Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3 in (match b3 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst = (ASM.REGISTER v4); Types.snd = ASM.ACC_A }))))))); Types.snd = pc }; Types.snd = (Nat.S Nat.O) } | Bool.False -> let { Types.fst = b4; Types.snd = v5 } = Vector.head (Nat.S (Nat.S Nat.O)) v4 in (match b4 with | Bool.True -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst = (ASM.INDIRECT (Vector.from_singl v6)); Types.snd = ASM.ACC_A }))))))); Types.snd = pc }; Types.snd = (Nat.S Nat.O) } | Bool.False -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst = (ASM.DIRECT b10); Types.snd = ASM.ACC_A })))))); Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) }) | Bool.False -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.CPL ASM.ACC_A)); Types.snd = pc }; Types.snd = (Nat.S Nat.O) })) | Bool.False -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOVX (Types.Inr { Types.fst = (ASM.EXT_INDIRECT (Vector.from_singl v6)); Types.snd = ASM.ACC_A }))); Types.snd = pc }; Types.snd = (Nat.S (Nat.S Nat.O)) } | Bool.False -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.ACALL (ASM.ADDR11 (Vector.append (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)))))))) (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)))))) b10))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) }) | Bool.False -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOVX (Types.Inr { Types.fst = ASM.EXT_INDIRECT_DPTR; Types.snd = ASM.ACC_A }))); Types.snd = pc }; Types.snd = (Nat.S (Nat.S Nat.O)) })))) | Bool.False -> let { Types.fst = b3; Types.snd = v4 } = Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3 in (match b3 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.REGISTER v4) }))))))); Types.snd = pc }; Types.snd = (Nat.S Nat.O) } | Bool.False -> let { Types.fst = b4; Types.snd = v5 } = Vector.head (Nat.S (Nat.S Nat.O)) v4 in (match b4 with | Bool.True -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.INDIRECT (Vector.from_singl v6)) }))))))); Types.snd = pc }; Types.snd = (Nat.S Nat.O) } | Bool.False -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.DIRECT b10) }))))))); Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) }) | Bool.False -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.CLR ASM.ACC_A)); Types.snd = pc }; Types.snd = (Nat.S Nat.O) })) | Bool.False -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOVX (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.EXT_INDIRECT (Vector.from_singl v6)) }))); Types.snd = pc }; Types.snd = (Nat.S (Nat.S Nat.O)) } | Bool.False -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.AJMP (ASM.ADDR11 (Vector.append (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)))))))) (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)))))) b10))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) }) | Bool.False -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOVX (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = ASM.EXT_INDIRECT_DPTR }))); Types.snd = pc }; Types.snd = (Nat.S (Nat.S Nat.O)) }))))) | Bool.False -> let { Types.fst = b2; Types.snd = v3 } = Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2 in (match b2 with | Bool.True -> let { Types.fst = b3; Types.snd = v4 } = Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3 in (match b3 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.DJNZ ((ASM.REGISTER v4), (ASM.RELATIVE b10)))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) }) | Bool.False -> let { Types.fst = b4; Types.snd = v5 } = Vector.head (Nat.S (Nat.S Nat.O)) v4 in (match b4 with | Bool.True -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.XCHD (ASM.ACC_A, (ASM.INDIRECT (Vector.from_singl v6))))); Types.snd = pc }; Types.snd = (Nat.S Nat.O) } | Bool.False -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> prod_inv_rect_Type0 (ASM.next pmem pc0) (fun pc1 b20 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.DJNZ ((ASM.DIRECT b10), (ASM.RELATIVE b20)))); Types.snd = pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) })) | Bool.False -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.DA ASM.ACC_A)); Types.snd = pc }; Types.snd = (Nat.S Nat.O) })) | Bool.False -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.SETB ASM.CARRY)); Types.snd = pc }; Types.snd = (Nat.S Nat.O) } | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.SETB (ASM.BIT_ADDR b10))); Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) })) | Bool.False -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.ACALL (ASM.ADDR11 (Vector.append (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)))))))) (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)))))) b10))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) }) | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.POP (ASM.DIRECT b10))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) }))))) | Bool.False -> let { Types.fst = b3; Types.snd = v4 } = Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3 in (match b3 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.XCH (ASM.ACC_A, (ASM.REGISTER v4)))); Types.snd = pc }; Types.snd = (Nat.S Nat.O) } | Bool.False -> let { Types.fst = b4; Types.snd = v5 } = Vector.head (Nat.S (Nat.S Nat.O)) v4 in (match b4 with | Bool.True -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.XCH (ASM.ACC_A, (ASM.INDIRECT (Vector.from_singl v6))))); Types.snd = pc }; Types.snd = (Nat.S Nat.O) } | Bool.False -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.XCH (ASM.ACC_A, (ASM.DIRECT b10)))); Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) }) | Bool.False -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.SWAP ASM.ACC_A)); Types.snd = pc }; Types.snd = (Nat.S Nat.O) })) | Bool.False -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.CLR ASM.CARRY)); Types.snd = pc }; Types.snd = (Nat.S Nat.O) } | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.CLR (ASM.BIT_ADDR b10))); Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) })) | Bool.False -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.AJMP (ASM.ADDR11 (Vector.append (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)))))))) (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)))))) b10))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) }) | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.PUSH (ASM.DIRECT b10))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) }))))))) | Bool.False -> let { Types.fst = b1; Types.snd = v2 } = Vector.head (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) v1 in (match b1 with | Bool.True -> let { Types.fst = b2; Types.snd = v3 } = Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2 in (match b2 with | Bool.True -> let { Types.fst = b3; Types.snd = v4 } = Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3 in (match b3 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> prod_inv_rect_Type0 (ASM.next pmem pc0) (fun pc1 b20 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.CJNE ((Types.Inr { Types.fst = (ASM.REGISTER v4); Types.snd = (ASM.DATA b10) }), (ASM.RELATIVE b20)))); Types.snd = pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) })) | Bool.False -> let { Types.fst = b4; Types.snd = v5 } = Vector.head (Nat.S (Nat.S Nat.O)) v4 in (match b4 with | Bool.True -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> prod_inv_rect_Type0 (ASM.next pmem pc0) (fun pc1 b20 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.CJNE ((Types.Inr { Types.fst = (ASM.INDIRECT (Vector.from_singl v6)); Types.snd = (ASM.DATA b10) }), (ASM.RELATIVE b20)))); Types.snd = pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) })) | Bool.False -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> prod_inv_rect_Type0 (ASM.next pmem pc0) (fun pc1 b20 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.CJNE ((Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.DIRECT b10) }), (ASM.RELATIVE b20)))); Types.snd = pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) })) | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> prod_inv_rect_Type0 (ASM.next pmem pc0) (fun pc1 b20 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.CJNE ((Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.DATA b10) }), (ASM.RELATIVE b20)))); Types.snd = pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) })))) | Bool.False -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.CPL ASM.CARRY)); Types.snd = pc }; Types.snd = (Nat.S Nat.O) } | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.CPL (ASM.BIT_ADDR b10))); Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) })) | Bool.False -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.ACALL (ASM.ADDR11 (Vector.append (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)))))))) (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)))))) b10))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) }) | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ANL (Types.Inr { Types.fst = ASM.CARRY; Types.snd = (ASM.N_BIT_ADDR b10) }))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) }))))) | Bool.False -> let { Types.fst = b3; Types.snd = v4 } = Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3 in (match b3 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst = (ASM.REGISTER v4); Types.snd = (ASM.DIRECT b10) }))))))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) }) | Bool.False -> let { Types.fst = b4; Types.snd = v5 } = Vector.head (Nat.S (Nat.S Nat.O)) v4 in (match b4 with | Bool.True -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst = (ASM.INDIRECT (Vector.from_singl v6)); Types.snd = (ASM.DIRECT b10) }))))))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) }) | Bool.False -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MUL (ASM.ACC_A, ASM.ACC_B))); Types.snd = pc }; Types.snd = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) }) | Bool.False -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.INC ASM.DPTR)); Types.snd = pc }; Types.snd = (Nat.S (Nat.S Nat.O)) } | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inr { Types.fst = ASM.CARRY; Types.snd = (ASM.BIT_ADDR b10) })))); Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) })) | Bool.False -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.AJMP (ASM.ADDR11 (Vector.append (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)))))))) (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)))))) b10))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) }) | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ORL (Types.Inr { Types.fst = ASM.CARRY; Types.snd = (ASM.N_BIT_ADDR b10) }))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) })))))) | Bool.False -> let { Types.fst = b2; Types.snd = v3 } = Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2 in (match b2 with | Bool.True -> let { Types.fst = b3; Types.snd = v4 } = Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3 in (match b3 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.SUBB (ASM.ACC_A, (ASM.REGISTER v4)))); Types.snd = pc }; Types.snd = (Nat.S Nat.O) } | Bool.False -> let { Types.fst = b4; Types.snd = v5 } = Vector.head (Nat.S (Nat.S Nat.O)) v4 in (match b4 with | Bool.True -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.SUBB (ASM.ACC_A, (ASM.INDIRECT (Vector.from_singl v6))))); Types.snd = pc }; Types.snd = (Nat.S Nat.O) } | Bool.False -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.SUBB (ASM.ACC_A, (ASM.DIRECT b10)))); Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) }) | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.SUBB (ASM.ACC_A, (ASM.DATA b10)))); Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) }))) | Bool.False -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> { Types.fst = { Types.fst = (ASM.MOVC (ASM.ACC_A, ASM.ACC_DPTR)); Types.snd = pc }; Types.snd = (Nat.S (Nat.S Nat.O)) } | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV (Types.Inr { Types.fst = (ASM.BIT_ADDR b10); Types.snd = ASM.CARRY }))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) })) | Bool.False -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.ACALL (ASM.ADDR11 (Vector.append (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)))))))) (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)))))) b10))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) }) | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> prod_inv_rect_Type0 (ASM.next pmem pc0) (fun pc1 b20 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inr { Types.fst = ASM.DPTR; Types.snd = (ASM.DATA16 (Vector.append (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)))))))) b10 b20)) }))))); Types.snd = pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) })))))) | Bool.False -> let { Types.fst = b3; Types.snd = v4 } = Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3 in (match b3 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst = (ASM.DIRECT b10); Types.snd = (ASM.REGISTER v4) })))))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) }) | Bool.False -> let { Types.fst = b4; Types.snd = v5 } = Vector.head (Nat.S (Nat.S Nat.O)) v4 in (match b4 with | Bool.True -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst = (ASM.DIRECT b10); Types.snd = (ASM.INDIRECT (Vector.from_singl v6)) })))))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) }) | Bool.False -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> prod_inv_rect_Type0 (ASM.next pmem pc0) (fun pc1 b20 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst = (ASM.DIRECT b10); Types.snd = (ASM.DIRECT b20) })))))); Types.snd = pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) })) | Bool.False -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.DIV (ASM.ACC_A, ASM.ACC_B))); Types.snd = pc }; Types.snd = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) })) | Bool.False -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> { Types.fst = { Types.fst = (ASM.MOVC (ASM.ACC_A, ASM.ACC_PC)); Types.snd = pc }; Types.snd = (Nat.S (Nat.S Nat.O)) } | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ANL (Types.Inr { Types.fst = ASM.CARRY; Types.snd = (ASM.BIT_ADDR b10) }))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) })) | Bool.False -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.AJMP (ASM.ADDR11 (Vector.append (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)))))))) (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)))))) b10))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) }) | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.SJMP (ASM.RELATIVE b10)); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) })))))))) | Bool.False -> let { Types.fst = b0; Types.snd = v1 } = Vector.head (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) v0 in (match b0 with | Bool.True -> let { Types.fst = b1; Types.snd = v2 } = Vector.head (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) v1 in (match b1 with | Bool.True -> let { Types.fst = b2; Types.snd = v3 } = Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2 in (match b2 with | Bool.True -> let { Types.fst = b3; Types.snd = v4 } = Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3 in (match b3 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst = (ASM.REGISTER v4); Types.snd = (ASM.DATA b10) }))))))); Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) }) | Bool.False -> let { Types.fst = b4; Types.snd = v5 } = Vector.head (Nat.S (Nat.S Nat.O)) v4 in (match b4 with | Bool.True -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst = (ASM.INDIRECT (Vector.from_singl v6)); Types.snd = (ASM.DATA b10) }))))))); Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) }) | Bool.False -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> prod_inv_rect_Type0 (ASM.next pmem pc0) (fun pc1 b20 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst = (ASM.DIRECT b10); Types.snd = (ASM.DATA b20) })))))); Types.snd = pc1 }; Types.snd = (Nat.S (Nat.S (Nat.S Nat.O))) })) | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.DATA b10) }))))))); Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) }))) | Bool.False -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.JMP ASM.ACC_DPTR)); Types.snd = pc }; Types.snd = (Nat.S (Nat.S Nat.O)) } | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ORL (Types.Inr { Types.fst = ASM.CARRY; Types.snd = (ASM.BIT_ADDR b10) }))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) })) | Bool.False -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.ACALL (ASM.ADDR11 (Vector.append (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)))))))) (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)))))) b10))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) }) | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.JNZ (ASM.RELATIVE b10))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) }))))) | Bool.False -> let { Types.fst = b3; Types.snd = v4 } = Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3 in (match b3 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.XRL (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.REGISTER v4) }))); Types.snd = pc }; Types.snd = (Nat.S Nat.O) } | Bool.False -> let { Types.fst = b4; Types.snd = v5 } = Vector.head (Nat.S (Nat.S Nat.O)) v4 in (match b4 with | Bool.True -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.XRL (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.INDIRECT (Vector.from_singl v6)) }))); Types.snd = pc }; Types.snd = (Nat.S Nat.O) } | Bool.False -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.XRL (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.DIRECT b10) }))); Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) }) | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.XRL (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.DATA b10) }))); Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) }))) | Bool.False -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> prod_inv_rect_Type0 (ASM.next pmem pc0) (fun pc1 b20 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.XRL (Types.Inr { Types.fst = (ASM.DIRECT b10); Types.snd = (ASM.DATA b20) }))); Types.snd = pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) })) | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.XRL (Types.Inr { Types.fst = (ASM.DIRECT b10); Types.snd = ASM.ACC_A }))); Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) })) | Bool.False -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.AJMP (ASM.ADDR11 (Vector.append (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)))))))) (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)))))) b10))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) }) | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.JZ (ASM.RELATIVE b10))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) })))))) | Bool.False -> let { Types.fst = b2; Types.snd = v3 } = Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2 in (match b2 with | Bool.True -> let { Types.fst = b3; Types.snd = v4 } = Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3 in (match b3 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ANL (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.REGISTER v4) })))); Types.snd = pc }; Types.snd = (Nat.S Nat.O) } | Bool.False -> let { Types.fst = b4; Types.snd = v5 } = Vector.head (Nat.S (Nat.S Nat.O)) v4 in (match b4 with | Bool.True -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ANL (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.INDIRECT (Vector.from_singl v6)) })))); Types.snd = pc }; Types.snd = (Nat.S Nat.O) } | Bool.False -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ANL (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.DIRECT b10) })))); Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) }) | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ANL (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.DATA b10) })))); Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) }))) | Bool.False -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> prod_inv_rect_Type0 (ASM.next pmem pc0) (fun pc1 b20 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ANL (Types.Inl (Types.Inr { Types.fst = (ASM.DIRECT b10); Types.snd = (ASM.DATA b20) })))); Types.snd = pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) })) | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ANL (Types.Inl (Types.Inr { Types.fst = (ASM.DIRECT b10); Types.snd = ASM.ACC_A })))); Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) })) | Bool.False -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.ACALL (ASM.ADDR11 (Vector.append (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)))))))) (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)))))) b10))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) }) | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.JNC (ASM.RELATIVE b10))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) }))))) | Bool.False -> let { Types.fst = b3; Types.snd = v4 } = Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3 in (match b3 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ORL (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.REGISTER v4) })))); Types.snd = pc }; Types.snd = (Nat.S Nat.O) } | Bool.False -> let { Types.fst = b4; Types.snd = v5 } = Vector.head (Nat.S (Nat.S Nat.O)) v4 in (match b4 with | Bool.True -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ORL (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.INDIRECT (Vector.from_singl v6)) })))); Types.snd = pc }; Types.snd = (Nat.S Nat.O) } | Bool.False -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ORL (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.DIRECT b10) })))); Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) }) | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ORL (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = (ASM.DATA b10) })))); Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) }))) | Bool.False -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> prod_inv_rect_Type0 (ASM.next pmem pc0) (fun pc1 b20 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ORL (Types.Inl (Types.Inr { Types.fst = (ASM.DIRECT b10); Types.snd = (ASM.DATA b20) })))); Types.snd = pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) })) | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ORL (Types.Inl (Types.Inr { Types.fst = (ASM.DIRECT b10); Types.snd = ASM.ACC_A })))); Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) })) | Bool.False -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.AJMP (ASM.ADDR11 (Vector.append (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)))))))) (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)))))) b10))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) }) | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.JC (ASM.RELATIVE b10))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) }))))))) | Bool.False -> let { Types.fst = b1; Types.snd = v2 } = Vector.head (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) v1 in (match b1 with | Bool.True -> let { Types.fst = b2; Types.snd = v3 } = Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2 in (match b2 with | Bool.True -> let { Types.fst = b3; Types.snd = v4 } = Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3 in (match b3 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ADDC (ASM.ACC_A, (ASM.REGISTER v4)))); Types.snd = pc }; Types.snd = (Nat.S Nat.O) } | Bool.False -> let { Types.fst = b4; Types.snd = v5 } = Vector.head (Nat.S (Nat.S Nat.O)) v4 in (match b4 with | Bool.True -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ADDC (ASM.ACC_A, (ASM.INDIRECT (Vector.from_singl v6))))); Types.snd = pc }; Types.snd = (Nat.S Nat.O) } | Bool.False -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ADDC (ASM.ACC_A, (ASM.DIRECT b10)))); Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) }) | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ADDC (ASM.ACC_A, (ASM.DATA b10)))); Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) }))) | Bool.False -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.RLC ASM.ACC_A)); Types.snd = pc }; Types.snd = (Nat.S Nat.O) } | Bool.False -> { Types.fst = { Types.fst = (ASM.RealInstruction ASM.RETI); Types.snd = pc }; Types.snd = (Nat.S (Nat.S Nat.O)) }) | Bool.False -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.ACALL (ASM.ADDR11 (Vector.append (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)))))))) (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)))))) b10))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) }) | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> prod_inv_rect_Type0 (ASM.next pmem pc0) (fun pc1 b20 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.JNB ((ASM.BIT_ADDR b10), (ASM.RELATIVE b20)))); Types.snd = pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) })))))) | Bool.False -> let { Types.fst = b3; Types.snd = v4 } = Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3 in (match b3 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ADD (ASM.ACC_A, (ASM.REGISTER v4)))); Types.snd = pc }; Types.snd = (Nat.S Nat.O) } | Bool.False -> let { Types.fst = b4; Types.snd = v5 } = Vector.head (Nat.S (Nat.S Nat.O)) v4 in (match b4 with | Bool.True -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ADD (ASM.ACC_A, (ASM.INDIRECT (Vector.from_singl v6))))); Types.snd = pc }; Types.snd = (Nat.S Nat.O) } | Bool.False -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ADD (ASM.ACC_A, (ASM.DIRECT b10)))); Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) }) | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ADD (ASM.ACC_A, (ASM.DATA b10)))); Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) }))) | Bool.False -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.RL ASM.ACC_A)); Types.snd = pc }; Types.snd = (Nat.S Nat.O) } | Bool.False -> { Types.fst = { Types.fst = (ASM.RealInstruction ASM.RET); Types.snd = pc }; Types.snd = (Nat.S (Nat.S Nat.O)) }) | Bool.False -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.AJMP (ASM.ADDR11 (Vector.append (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)))))))) (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)))))) b10))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) }) | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> prod_inv_rect_Type0 (ASM.next pmem pc0) (fun pc1 b20 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.JB ((ASM.BIT_ADDR b10), (ASM.RELATIVE b20)))); Types.snd = pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) }))))))) | Bool.False -> let { Types.fst = b2; Types.snd = v3 } = Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2 in (match b2 with | Bool.True -> let { Types.fst = b3; Types.snd = v4 } = Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3 in (match b3 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.DEC (ASM.REGISTER v4))); Types.snd = pc }; Types.snd = (Nat.S Nat.O) } | Bool.False -> let { Types.fst = b4; Types.snd = v5 } = Vector.head (Nat.S (Nat.S Nat.O)) v4 in (match b4 with | Bool.True -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.DEC (ASM.INDIRECT (Vector.from_singl v6)))); Types.snd = pc }; Types.snd = (Nat.S Nat.O) } | Bool.False -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.DEC (ASM.DIRECT b10))); Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) }) | Bool.False -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.DEC ASM.ACC_A)); Types.snd = pc }; Types.snd = (Nat.S Nat.O) })) | Bool.False -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.RRC ASM.ACC_A)); Types.snd = pc }; Types.snd = (Nat.S Nat.O) } | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> prod_inv_rect_Type0 (ASM.next pmem pc0) (fun pc1 b20 _ -> { Types.fst = { Types.fst = (ASM.LCALL (ASM.ADDR16 (Vector.append (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)))))))) b10 b20))); Types.snd = pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) }))) | Bool.False -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.ACALL (ASM.ADDR11 (Vector.append (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)))))))) (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)))))) b10))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) }) | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> prod_inv_rect_Type0 (ASM.next pmem pc0) (fun pc1 b20 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.JBC ((ASM.BIT_ADDR b10), (ASM.RELATIVE b20)))); Types.snd = pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) })))))) | Bool.False -> let { Types.fst = b3; Types.snd = v4 } = Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3 in (match b3 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.INC (ASM.REGISTER v4))); Types.snd = pc }; Types.snd = (Nat.S Nat.O) } | Bool.False -> let { Types.fst = b4; Types.snd = v5 } = Vector.head (Nat.S (Nat.S Nat.O)) v4 in (match b4 with | Bool.True -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.INC (ASM.INDIRECT (Vector.from_singl v6)))); Types.snd = pc }; Types.snd = (Nat.S Nat.O) } | Bool.False -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.INC (ASM.DIRECT b10))); Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) }) | Bool.False -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.INC ASM.ACC_A)); Types.snd = pc }; Types.snd = (Nat.S Nat.O) })) | Bool.False -> let { Types.fst = b5; Types.snd = v6 } = Vector.head (Nat.S Nat.O) v5 in (match b5 with | Bool.True -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.RR ASM.ACC_A)); Types.snd = pc }; Types.snd = (Nat.S Nat.O) } | Bool.False -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> prod_inv_rect_Type0 (ASM.next pmem pc0) (fun pc1 b20 _ -> { Types.fst = { Types.fst = (ASM.LJMP (ASM.ADDR16 (Vector.append (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)))))))) b10 b20))); Types.snd = pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) }))) | Bool.False -> let { Types.fst = b6; Types.snd = v7 } = Vector.head Nat.O v6 in (match b6 with | Bool.True -> prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ -> { Types.fst = { Types.fst = (ASM.AJMP (ASM.ADDR11 (Vector.append (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)))))))) (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)))))) b10))); Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) }) | Bool.False -> { Types.fst = { Types.fst = (ASM.RealInstruction ASM.NOP); Types.snd = pc }; Types.snd = (Nat.S Nat.O) })))))))) (** val fetch : BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word -> ((ASM.instruction, BitVector.word) Types.prod, Nat.nat) Types.prod **) let fetch pmem pc = let { Types.fst = word; Types.snd = byte } = ASM.next pmem pc in fetch0 pmem word byte