open Preamble open Div_and_mod open Jmeq open Russell open Util open Bool open Relations open Nat open List open Hints_declaration open Core_notation open Pts open Logic open Types open Extralib open BitVectorTrie open String open Integers open AST open LabelledObjects open Proper open PositiveMap open Deqsets open ErrorMessages open PreIdentifiers open Errors open Lists open Positive open Identifiers open CostLabel open ASM open Exp open Setoids open Monad open Option open Extranat open Vector open FoldStuff open BitVector open Arithmetic open Fetch open Status type jump_length = | Short_jump | Absolute_jump | Long_jump (** val jump_length_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1 **) let rec jump_length_rect_Type4 h_short_jump h_absolute_jump h_long_jump = function | Short_jump -> h_short_jump | Absolute_jump -> h_absolute_jump | Long_jump -> h_long_jump (** val jump_length_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1 **) let rec jump_length_rect_Type5 h_short_jump h_absolute_jump h_long_jump = function | Short_jump -> h_short_jump | Absolute_jump -> h_absolute_jump | Long_jump -> h_long_jump (** val jump_length_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1 **) let rec jump_length_rect_Type3 h_short_jump h_absolute_jump h_long_jump = function | Short_jump -> h_short_jump | Absolute_jump -> h_absolute_jump | Long_jump -> h_long_jump (** val jump_length_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1 **) let rec jump_length_rect_Type2 h_short_jump h_absolute_jump h_long_jump = function | Short_jump -> h_short_jump | Absolute_jump -> h_absolute_jump | Long_jump -> h_long_jump (** val jump_length_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1 **) let rec jump_length_rect_Type1 h_short_jump h_absolute_jump h_long_jump = function | Short_jump -> h_short_jump | Absolute_jump -> h_absolute_jump | Long_jump -> h_long_jump (** val jump_length_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1 **) let rec jump_length_rect_Type0 h_short_jump h_absolute_jump h_long_jump = function | Short_jump -> h_short_jump | Absolute_jump -> h_absolute_jump | Long_jump -> h_long_jump (** val jump_length_inv_rect_Type4 : jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let jump_length_inv_rect_Type4 hterm h1 h2 h3 = let hcut = jump_length_rect_Type4 h1 h2 h3 hterm in hcut __ (** val jump_length_inv_rect_Type3 : jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let jump_length_inv_rect_Type3 hterm h1 h2 h3 = let hcut = jump_length_rect_Type3 h1 h2 h3 hterm in hcut __ (** val jump_length_inv_rect_Type2 : jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let jump_length_inv_rect_Type2 hterm h1 h2 h3 = let hcut = jump_length_rect_Type2 h1 h2 h3 hterm in hcut __ (** val jump_length_inv_rect_Type1 : jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let jump_length_inv_rect_Type1 hterm h1 h2 h3 = let hcut = jump_length_rect_Type1 h1 h2 h3 hterm in hcut __ (** val jump_length_inv_rect_Type0 : jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **) let jump_length_inv_rect_Type0 hterm h1 h2 h3 = let hcut = jump_length_rect_Type0 h1 h2 h3 hterm in hcut __ (** val jump_length_discr : jump_length -> jump_length -> __ **) let jump_length_discr x y = Logic.eq_rect_Type2 x (match x with | Short_jump -> Obj.magic (fun _ dH -> dH) | Absolute_jump -> Obj.magic (fun _ dH -> dH) | Long_jump -> Obj.magic (fun _ dH -> dH)) y (** val jump_length_jmdiscr : jump_length -> jump_length -> __ **) let jump_length_jmdiscr x y = Logic.eq_rect_Type2 x (match x with | Short_jump -> Obj.magic (fun _ dH -> dH) | Absolute_jump -> Obj.magic (fun _ dH -> dH) | Long_jump -> Obj.magic (fun _ dH -> dH)) y (** val short_jump_cond : BitVector.word -> BitVector.word -> (Bool.bool, BitVector.bitVector) Types.prod **) let short_jump_cond pc_plus_jmp_length addr = let { Types.fst = result; Types.snd = flags } = Arithmetic.sub_16_with_carry addr pc_plus_jmp_length Bool.False in let { Types.fst = upper; Types.snd = lower } = Vector.vsplit (Nat.S (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.O))))))) result in (match Vector.get_index' (Nat.S (Nat.S Nat.O)) Nat.O flags with | Bool.True -> { Types.fst = (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) upper (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.True, (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))))))))))))))))))); Types.snd = (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, lower)) } | Bool.False -> { Types.fst = (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) upper (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))); Types.snd = (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, lower)) }) (** val absolute_jump_cond : BitVector.word -> BitVector.word -> (Bool.bool, BitVector.bitVector) Types.prod **) let absolute_jump_cond pc_plus_jmp_length addr = let { Types.fst = fst_5_addr; Types.snd = rest_addr } = Vector.vsplit (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.O))))))))))) addr in let { Types.fst = fst_5_pc; Types.snd = rest_pc } = Vector.vsplit (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.O))))))))))) pc_plus_jmp_length in { Types.fst = (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) fst_5_addr fst_5_pc); Types.snd = rest_addr } (** val assembly_preinstruction : ('a1 -> BitVector.byte) -> 'a1 ASM.preinstruction -> Bool.bool Vector.vector List.list **) let assembly_preinstruction addr_of = function | ASM.ADD (addr1, addr2) -> (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))))))) addr2 with | ASM.DIRECT b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.INDIRECT i1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, i1, Vector.VEmpty)))))))))))))))), List.Nil)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER r -> (fun _ -> List.Cons ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))) r), List.Nil)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ | ASM.ADDC (addr1, addr2) -> (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))))))) addr2 with | ASM.DIRECT b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.INDIRECT i1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, i1, Vector.VEmpty)))))))))))))))), List.Nil)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER r -> (fun _ -> List.Cons ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))) r), List.Nil)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ | ASM.SUBB (addr1, addr2) -> (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))))))) addr2 with | ASM.DIRECT b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.INDIRECT i1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, i1, Vector.VEmpty)))))))))))))))), List.Nil)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER r -> (fun _ -> List.Cons ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))) r), List.Nil)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ | ASM.INC addr -> (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Dptr, Vector.VEmpty)))))))))) addr with | ASM.DIRECT b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.INDIRECT i1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, i1, Vector.VEmpty)))))))))))))))), List.Nil)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER r -> (fun _ -> List.Cons ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))) r), List.Nil)) | ASM.ACC_A -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), List.Nil)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), List.Nil)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ | ASM.DEC addr -> (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.Registr, (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty)))))))) addr with | ASM.DIRECT b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.INDIRECT i1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, i1, Vector.VEmpty)))))))))))))))), List.Nil)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER r -> (fun _ -> List.Cons ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))) r), List.Nil)) | ASM.ACC_A -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), List.Nil)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ | ASM.MUL (addr1, addr2) -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), List.Nil) | ASM.DIV (addr1, addr2) -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), List.Nil) | ASM.DA addr -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), List.Nil) | ASM.JC addr -> let b1 = addr_of addr in List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil))) | ASM.JNC addr -> let b1 = addr_of addr in List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil))) | ASM.JB (addr1, addr2) -> let b2 = addr_of addr2 in (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty)) addr1 with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, (List.Cons (b2, List.Nil)))))) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ | ASM.JNB (addr1, addr2) -> let b2 = addr_of addr2 in (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty)) addr1 with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, (List.Cons (b2, List.Nil)))))) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ | ASM.JBC (addr1, addr2) -> let b2 = addr_of addr2 in (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty)) addr1 with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, (List.Cons (b2, List.Nil)))))) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ | ASM.JZ addr -> let b1 = addr_of addr in List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil))) | ASM.JNZ addr -> let b1 = addr_of addr in List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil))) | ASM.CJNE (addrs, addr3) -> let b3 = addr_of addr3 in (match addrs with | Types.Inl addrs0 -> let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))) addr2 with | ASM.DIRECT b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, (List.Cons (b3, List.Nil)))))) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, (List.Cons (b3, List.Nil)))))) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ | Types.Inr addrs0 -> let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in let b2 = (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)) addr2 with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA b2 -> (fun _ -> b2) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ in (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O), ASM.Registr, (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty)))) addr1 with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT i1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, i1, Vector.VEmpty)))))))))))))))), (List.Cons (b2, (List.Cons (b3, List.Nil)))))) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER r -> (fun _ -> List.Cons ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))) r), (List.Cons (b2, (List.Cons (b3, List.Nil)))))) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __) | ASM.DJNZ (addr1, addr2) -> let b2 = addr_of addr2 in (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O), ASM.Registr, (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)))) addr1 with | ASM.DIRECT b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, (List.Cons (b2, List.Nil)))))) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER r -> (fun _ -> List.Cons ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.True, (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)))))))))) r), (List.Cons (b2, List.Nil)))) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ | ASM.ANL addrs -> (match addrs with | Types.Inl addrs0 -> (match addrs0 with | Types.Inl addrs1 -> let { Types.fst = addr1; Types.snd = addr2 } = addrs1 in (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))))))) addr2 with | ASM.DIRECT b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.INDIRECT i1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, i1, Vector.VEmpty)))))))))))))))), List.Nil)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER r -> (fun _ -> List.Cons ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.True, (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)))))))))) r), List.Nil)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ | Types.Inr addrs1 -> let { Types.fst = addr1; Types.snd = addr2 } = addrs1 in let b1 = (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)) addr1 with | ASM.DIRECT b1 -> (fun _ -> b1) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ in (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O), ASM.Acc_a, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))) addr2 with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA b2 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, (List.Cons (b2, List.Nil)))))) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __) | Types.Inr addrs0 -> let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O), ASM.Bit_addr, (Vector.VCons (Nat.O, ASM.N_bit_addr, Vector.VEmpty)))) addr2 with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.N_BIT_ADDR b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __) | ASM.ORL addrs -> (match addrs with | Types.Inl addrs0 -> (match addrs0 with | Types.Inl addrs1 -> let { Types.fst = addr1; Types.snd = addr2 } = addrs1 in (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Data, (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty)))))))) addr2 with | ASM.DIRECT b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.INDIRECT i1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, i1, Vector.VEmpty)))))))))))))))), List.Nil)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER r -> (fun _ -> List.Cons ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.True, (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)))))))))) r), List.Nil)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ | Types.Inr addrs1 -> let { Types.fst = addr1; Types.snd = addr2 } = addrs1 in let b1 = (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)) addr1 with | ASM.DIRECT b1 -> (fun _ -> b1) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ in (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O), ASM.Acc_a, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))) addr2 with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA b2 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, (List.Cons (b2, List.Nil)))))) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __) | Types.Inr addrs0 -> let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O), ASM.Bit_addr, (Vector.VCons (Nat.O, ASM.N_bit_addr, Vector.VEmpty)))) addr2 with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.N_BIT_ADDR b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __) | ASM.XRL addrs -> (match addrs with | Types.Inl addrs0 -> let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Data, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Registr, (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty)))))))) addr2 with | ASM.DIRECT b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.INDIRECT i1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, i1, Vector.VEmpty)))))))))))))))), List.Nil)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER r -> (fun _ -> List.Cons ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.True, (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)))))))))) r), List.Nil)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ | Types.Inr addrs0 -> let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in let b1 = (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)) addr1 with | ASM.DIRECT b1 -> (fun _ -> b1) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ in (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O), ASM.Acc_a, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))) addr2 with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA b2 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, (List.Cons (b2, List.Nil)))))) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __) | ASM.CLR addr -> (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.Carry, (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty)))))) addr with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), List.Nil)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), List.Nil)) | ASM.BIT_ADDR b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ | ASM.CPL addr -> (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.Carry, (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty)))))) addr with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), List.Nil)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), List.Nil)) | ASM.BIT_ADDR b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ | ASM.RL addr -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), List.Nil) | ASM.RLC addr -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), List.Nil) | ASM.RR addr -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), List.Nil) | ASM.RRC addr -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), List.Nil) | ASM.SWAP addr -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), List.Nil) | ASM.MOV addrs -> (match addrs with | Types.Inl addrs0 -> (match addrs0 with | Types.Inl addrs1 -> (match addrs1 with | Types.Inl addrs2 -> (match addrs2 with | Types.Inl addrs3 -> (match addrs3 with | Types.Inl addrs4 -> let { Types.fst = addr1; Types.snd = addr2 } = addrs4 in (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))))))) addr2 with | ASM.DIRECT b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.INDIRECT i1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, i1, Vector.VEmpty)))))))))))))))), List.Nil)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER r -> (fun _ -> List.Cons ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.True, (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)))))))))) r), List.Nil)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ | Types.Inr addrs4 -> let { Types.fst = addr1; Types.snd = addr2 } = addrs4 in (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O), ASM.Registr, (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty)))) addr1 with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT i1 -> (fun _ -> (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.Data, Vector.VEmpty)))))) addr2 with | ASM.DIRECT b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, i1, Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.INDIRECT x0 -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x0 -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x0 -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, i1, Vector.VEmpty)))))))))))))))), List.Nil)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, i1, Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil)))) | 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 *))) __) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER r -> (fun _ -> (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.Data, Vector.VEmpty)))))) addr2 with | ASM.DIRECT b1 -> (fun _ -> List.Cons ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))) r), (List.Cons (b1, List.Nil)))) | ASM.INDIRECT x0 -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x0 -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x0 -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> List.Cons ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.True, (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)))))))))) r), List.Nil)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA b1 -> (fun _ -> List.Cons ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.True, (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)))))))))) r), (List.Cons (b1, List.Nil)))) | 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 *))) __) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __) | Types.Inr addrs3 -> let { Types.fst = addr1; Types.snd = addr2 } = addrs3 in let b1 = (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)) addr1 with | ASM.DIRECT b1 -> (fun _ -> b1) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ in (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data, Vector.VEmpty)))))))))) addr2 with | ASM.DIRECT b2 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, (List.Cons (b2, List.Nil)))))) | ASM.INDIRECT i1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, i1, Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER r -> (fun _ -> List.Cons ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))) r), (List.Cons (b1, List.Nil)))) | ASM.ACC_A -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA b2 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, (List.Cons (b2, List.Nil)))))) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __) | Types.Inr addrs2 -> let { Types.fst = addr1; Types.snd = addr2 } = addrs2 in (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Data16, Vector.VEmpty)) addr2 with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 w -> (fun _ -> let b1_b2 = 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)))))))) w in let b1 = b1_b2.Types.fst in let b2 = b1_b2.Types.snd in List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, (List.Cons (b2, List.Nil)))))) | 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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __) | Types.Inr addrs1 -> let { Types.fst = addr1; Types.snd = addr2 } = addrs1 in (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty)) addr2 with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __) | Types.Inr addrs0 -> let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty)) addr1 with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __) | ASM.MOVX addrs -> (match addrs with | Types.Inl addrs0 -> let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))) addr2 with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT i1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, i1, Vector.VEmpty)))))))))))))))), List.Nil)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), List.Nil)) | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.CARRY -> (fun _ -> assert false (* absurd case *)) | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ | Types.Inr addrs0 -> let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O, ASM.Ext_indirect_dptr, Vector.VEmpty)))) addr1 with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT i1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, i1, Vector.VEmpty)))))))))))))))), List.Nil)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), List.Nil)) | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.CARRY -> (fun _ -> assert false (* absurd case *)) | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __) | ASM.SETB addr -> (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O), ASM.Carry, (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty)))) addr with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), List.Nil)) | ASM.BIT_ADDR b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ | ASM.PUSH addr -> (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)) addr with | ASM.DIRECT b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ | ASM.POP addr -> (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty)) addr with | ASM.DIRECT b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ | ASM.XCH (addr1, addr2) -> (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Registr, (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty)))))) addr2 with | ASM.DIRECT b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.INDIRECT i1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, i1, Vector.VEmpty)))))))))))))))), List.Nil)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER r -> (fun _ -> List.Cons ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.True, (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)))))))))) r), List.Nil)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ | ASM.XCHD (addr1, addr2) -> (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Indirect, Vector.VEmpty)) addr2 with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT i1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, i1, Vector.VEmpty)))))))))))))))), List.Nil)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ | ASM.RET -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), List.Nil) | ASM.RETI -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), List.Nil) | ASM.NOP -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), List.Nil) | ASM.JMP adptr -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), List.Nil) (** val assembly1 : ASM.instruction -> Bool.bool Vector.vector List.list **) let assembly1 = function | ASM.ACALL addr -> (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Addr11, Vector.VEmpty)) addr with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 w -> (fun _ -> let v1_v2 = Vector.vsplit (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)))))))) w in let v1 = v1_v2.Types.fst in let v2 = v1_v2.Types.snd in List.Cons ((Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) v1 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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))))))))))), (List.Cons (v2, List.Nil)))) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ | ASM.LCALL addr -> (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Addr16, Vector.VEmpty)) addr with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 w -> (fun _ -> let b1_b2 = 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)))))))) w in let b1 = b1_b2.Types.fst in let b2 = b1_b2.Types.snd in List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, (List.Cons (b2, List.Nil))))))) __ | ASM.AJMP addr -> (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Addr11, Vector.VEmpty)) addr with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 w -> (fun _ -> let v1_v2 = Vector.vsplit (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)))))))) w in let v1 = v1_v2.Types.fst in let v2 = v1_v2.Types.snd in List.Cons ((Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) v1 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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))))))))))), (List.Cons (v2, List.Nil)))) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ | ASM.LJMP addr -> (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Addr16, Vector.VEmpty)) addr with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 w -> (fun _ -> let b1_b2 = 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)))))))) w in let b1 = b1_b2.Types.fst in let b2 = b1_b2.Types.snd in List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, (List.Cons (b2, List.Nil))))))) __ | ASM.SJMP addr -> (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Relative, Vector.VEmpty)) addr with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE b1 -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), (List.Cons (b1, List.Nil)))) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ | ASM.MOVC (addr1, addr2) -> (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O), ASM.Acc_dptr, (Vector.VCons (Nat.O, ASM.Acc_pc, Vector.VEmpty)))) addr2 with | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_DPTR -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), List.Nil)) | ASM.ACC_PC -> (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (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)))))))))))))))), List.Nil)) | 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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __ | ASM.RealInstruction instr -> assembly_preinstruction (fun x -> (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Relative, Vector.VEmpty)) x with | ASM.DIRECT x0 -> (fun _ -> assert false (* absurd case *)) | ASM.INDIRECT x0 -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x0 -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER x0 -> (fun _ -> assert false (* absurd case *)) | ASM.ACC_A -> (fun _ -> assert false (* absurd case *)) | 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 r -> (fun _ -> r) | ASM.ADDR11 x0 -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x0 -> (fun _ -> assert false (* absurd case *))) __) instr (** val expand_relative_jump_internal : (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) -> ASM.identifier -> BitVector.word -> (ASM.subaddressing_mode -> ASM.subaddressing_mode ASM.preinstruction) -> ASM.instruction List.list **) let expand_relative_jump_internal lookup_labels sigma policy lbl ppc i = let lookup_address = sigma (lookup_labels lbl) in let pc_plus_jmp_length = sigma (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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 (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)))))))))))))))) (Nat.S Nat.O))) in let { Types.fst = sj_possible; Types.snd = disp } = short_jump_cond pc_plus_jmp_length lookup_address in (match Bool.andb sj_possible (Bool.notb (policy ppc)) with | Bool.True -> let address = ASM.RELATIVE disp in List.Cons ((ASM.RealInstruction (i address)), List.Nil) | Bool.False -> List.Cons ((ASM.RealInstruction (i (ASM.RELATIVE (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.O)))))), (List.Cons ((ASM.SJMP (ASM.RELATIVE (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.O)))))), (List.Cons ((ASM.LJMP (ASM.ADDR16 lookup_address)), List.Nil)))))) (** val expand_relative_jump : (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) -> BitVector.word -> ASM.identifier ASM.preinstruction -> ASM.instruction List.list **) let expand_relative_jump lookup_labels sigma policy ppc = function | ASM.ADD (arg1, arg2) -> List.Cons ((ASM.RealInstruction (ASM.ADD (arg1, arg2))), List.Nil) | ASM.ADDC (arg1, arg2) -> List.Cons ((ASM.RealInstruction (ASM.ADDC (arg1, arg2))), List.Nil) | ASM.SUBB (arg1, arg2) -> List.Cons ((ASM.RealInstruction (ASM.SUBB (arg1, arg2))), List.Nil) | ASM.INC arg -> List.Cons ((ASM.RealInstruction (ASM.INC arg)), List.Nil) | ASM.DEC arg -> List.Cons ((ASM.RealInstruction (ASM.DEC arg)), List.Nil) | ASM.MUL (arg1, arg2) -> List.Cons ((ASM.RealInstruction (ASM.MUL (arg1, arg2))), List.Nil) | ASM.DIV (arg1, arg2) -> List.Cons ((ASM.RealInstruction (ASM.DIV (arg1, arg2))), List.Nil) | ASM.DA arg -> List.Cons ((ASM.RealInstruction (ASM.DA arg)), List.Nil) | ASM.JC jmp -> expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x -> ASM.JC x) | ASM.JNC jmp -> expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x -> ASM.JNC x) | ASM.JB (baddr, jmp) -> expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x -> ASM.JB (baddr, x)) | ASM.JNB (baddr, jmp) -> expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x -> ASM.JNB (baddr, x)) | ASM.JBC (baddr, jmp) -> expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x -> ASM.JBC (baddr, x)) | ASM.JZ jmp -> expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x -> ASM.JZ x) | ASM.JNZ jmp -> expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x -> ASM.JNZ x) | ASM.CJNE (addr, jmp) -> expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x -> ASM.CJNE (addr, x)) | ASM.DJNZ (addr, jmp) -> expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x -> ASM.DJNZ (addr, x)) | ASM.ANL arg -> List.Cons ((ASM.RealInstruction (ASM.ANL arg)), List.Nil) | ASM.ORL arg -> List.Cons ((ASM.RealInstruction (ASM.ORL arg)), List.Nil) | ASM.XRL arg -> List.Cons ((ASM.RealInstruction (ASM.XRL arg)), List.Nil) | ASM.CLR arg -> List.Cons ((ASM.RealInstruction (ASM.CLR arg)), List.Nil) | ASM.CPL arg -> List.Cons ((ASM.RealInstruction (ASM.CPL arg)), List.Nil) | ASM.RL arg -> List.Cons ((ASM.RealInstruction (ASM.RL arg)), List.Nil) | ASM.RLC arg -> List.Cons ((ASM.RealInstruction (ASM.RLC arg)), List.Nil) | ASM.RR arg -> List.Cons ((ASM.RealInstruction (ASM.RR arg)), List.Nil) | ASM.RRC arg -> List.Cons ((ASM.RealInstruction (ASM.RRC arg)), List.Nil) | ASM.SWAP arg -> List.Cons ((ASM.RealInstruction (ASM.SWAP arg)), List.Nil) | ASM.MOV arg -> List.Cons ((ASM.RealInstruction (ASM.MOV arg)), List.Nil) | ASM.MOVX arg -> List.Cons ((ASM.RealInstruction (ASM.MOVX arg)), List.Nil) | ASM.SETB arg -> List.Cons ((ASM.RealInstruction (ASM.SETB arg)), List.Nil) | ASM.PUSH arg -> List.Cons ((ASM.RealInstruction (ASM.PUSH arg)), List.Nil) | ASM.POP arg -> List.Cons ((ASM.RealInstruction (ASM.POP arg)), List.Nil) | ASM.XCH (arg1, arg2) -> List.Cons ((ASM.RealInstruction (ASM.XCH (arg1, arg2))), List.Nil) | ASM.XCHD (arg1, arg2) -> List.Cons ((ASM.RealInstruction (ASM.XCHD (arg1, arg2))), List.Nil) | ASM.RET -> List.Cons ((ASM.RealInstruction ASM.RET), List.Nil) | ASM.RETI -> List.Cons ((ASM.RealInstruction ASM.RETI), List.Nil) | ASM.NOP -> List.Cons ((ASM.RealInstruction ASM.NOP), List.Nil) | ASM.JMP arg -> List.Cons ((ASM.RealInstruction (ASM.JMP arg)), List.Nil) (** val is_code : AST.region -> Bool.bool **) let is_code = function | AST.XData -> Bool.False | AST.Code -> Bool.True (** val expand_pseudo_instruction : (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) -> BitVector.word -> (ASM.identifier -> (AST.region, BitVector.word) Types.prod) -> ASM.pseudo_instruction -> ASM.instruction List.list **) let expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels = function | ASM.Instruction instr -> expand_relative_jump lookup_labels sigma policy ppc instr | ASM.Comment comment -> List.Nil | ASM.Cost cost -> List.Cons ((ASM.RealInstruction ASM.NOP), List.Nil) | ASM.Jmp jmp -> let pc_plus_jmp_length = sigma (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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 (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)))))))))))))))) (Nat.S Nat.O))) in let do_a_long = policy ppc in let lookup_address = sigma (lookup_labels jmp) in let { Types.fst = sj_possible; Types.snd = disp } = short_jump_cond pc_plus_jmp_length lookup_address in (match Bool.andb sj_possible (Bool.notb do_a_long) with | Bool.True -> let address = ASM.RELATIVE disp in List.Cons ((ASM.SJMP address), List.Nil) | Bool.False -> let { Types.fst = mj_possible; Types.snd = disp2 } = absolute_jump_cond pc_plus_jmp_length lookup_address in (match Bool.andb mj_possible (Bool.notb do_a_long) with | Bool.True -> let address = ASM.ADDR11 disp2 in List.Cons ((ASM.AJMP address), List.Nil) | Bool.False -> let address = ASM.ADDR16 lookup_address in List.Cons ((ASM.LJMP address), List.Nil))) | ASM.Jnz (acc, tgt1, tgt2) -> let lookup_address1 = sigma (lookup_labels tgt1) in let lookup_address2 = sigma (lookup_labels tgt2) in List.Cons ((ASM.RealInstruction (ASM.JNZ (ASM.RELATIVE (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.O))))))), (List.Cons ((ASM.LJMP (ASM.ADDR16 lookup_address2)), (List.Cons ((ASM.LJMP (ASM.ADDR16 lookup_address1)), List.Nil))))) | ASM.Call call -> let pc_plus_jmp_length = sigma (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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 (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)))))))))))))))) (Nat.S Nat.O))) in let lookup_address = sigma (lookup_labels call) in let { Types.fst = mj_possible; Types.snd = disp } = absolute_jump_cond pc_plus_jmp_length lookup_address in let do_a_long = policy ppc in (match Bool.andb mj_possible (Bool.notb do_a_long) with | Bool.True -> let address = ASM.ADDR11 disp in List.Cons ((ASM.ACALL address), List.Nil) | Bool.False -> let address = ASM.ADDR16 lookup_address in List.Cons ((ASM.LCALL address), List.Nil)) | ASM.Mov (d, trgt, off) -> let { Types.fst = r; Types.snd = addr } = lookup_datalabels trgt in let addr0 = (Arithmetic.add_16_with_carry addr off Bool.False).Types.fst in let addr1 = match is_code r with | Bool.True -> sigma addr0 | Bool.False -> addr0 in (match d with | Types.Inl x -> let address = ASM.DATA16 addr1 in List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inr { Types.fst = ASM.DPTR; Types.snd = address }))))), List.Nil) | Types.Inr pr -> let v = ASM.DATA (match pr.Types.snd with | ASM.HIGH -> (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)))))))) addr1).Types.fst | ASM.LOW -> (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)))))))) addr1).Types.snd) in (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)))))) pr.Types.fst with | ASM.DIRECT b1 -> (fun _ -> List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst = (ASM.DIRECT b1); Types.snd = v })))))), List.Nil)) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER r0 -> (fun _ -> List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst = (ASM.REGISTER r0); Types.snd = v }))))))), List.Nil)) | ASM.ACC_A -> (fun _ -> List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd = v }))))))), List.Nil)) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __) (** val assembly_1_pseudoinstruction : (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) -> BitVector.word -> (ASM.identifier -> (AST.region, BitVector.word) Types.prod) -> ASM.pseudo_instruction -> (Nat.nat, Bool.bool Vector.vector List.list) Types.prod **) let assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels i = let pseudos = expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels i in let mapped = List.map assembly1 pseudos in let flattened = List.flatten mapped in let pc_len = List.length flattened in { Types.fst = pc_len; Types.snd = flattened } (** val instruction_size : (ASM.identifier -> BitVector.word) -> (ASM.identifier -> (AST.region, BitVector.word) Types.prod) -> (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) -> BitVector.word -> ASM.pseudo_instruction -> Nat.nat **) let instruction_size lookup_labels lookup_datalabels sigma policy ppc i = (assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels i).Types.fst (** val assembly : ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) -> ASM.labelled_object_code Types.sig0 **) let assembly p sigma policy = (let { Types.fst = labels_to_ppc; Types.snd = ppc_to_costs } = Fetch.create_label_cost_map p.ASM.code in (fun _ -> let preamble = p.ASM.preamble in let instr_list = p.ASM.code in let datalabels = Status.construct_datalabels preamble in let lookup_labels = fun x -> 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)))))))))))))))) (Identifiers.lookup_def PreIdentifiers.ASMTag labels_to_ppc x Nat.O) in let lookup_datalabels = fun x -> match Identifiers.lookup PreIdentifiers.ASMTag (Status.construct_datalabels preamble) x with | Types.None -> { Types.fst = AST.Code; Types.snd = (lookup_labels x) } | Types.Some addr -> { Types.fst = AST.XData; Types.snd = addr } in (let { Types.fst = next_pc; Types.snd = revcode } = Types.pi1 (FoldStuff.foldl_strong instr_list (fun prefix hd tl _ ppc_code -> (let { Types.fst = ppc; Types.snd = code } = Types.pi1 ppc_code in (fun _ -> (let { Types.fst = pc_delta; Types.snd = program } = assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels hd.Types.snd in (fun _ -> let new_ppc = Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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 (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)))))))))))))))) (Nat.S Nat.O)) in { Types.fst = new_ppc; Types.snd = (List.append (List.reverse program) code) })) __)) __) { Types.fst = (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))))))))))))))))); Types.snd = List.Nil }) in (fun _ -> let code = List.reverse revcode in { ASM.oc = code; ASM.cm = (ASM.load_code_memory code); ASM.costlabels = (BitVectorTrie.fold (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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)))))))))))))))) (fun ppc cost pc_to_costs -> 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)))))))))))))))) (sigma ppc) cost pc_to_costs) ppc_to_costs (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)))))))))))))))))); ASM.symboltable = (Util.foldl (fun symboltable newident_oldident -> let ppc = lookup_labels newident_oldident.Types.fst in 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)))))))))))))))) (sigma ppc) newident_oldident.Types.snd symboltable) (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))))))))))))))))) p.ASM.renamed_symbols); ASM.final_pc = (sigma (lookup_labels p.ASM.final_label)) })) __)) __ (** val ticks_of_instruction : ASM.instruction -> Nat.nat **) let ticks_of_instruction i = let trivial_code_memory = assembly1 i in let trivial_status = ASM.load_code_memory trivial_code_memory in (Fetch.fetch trivial_status (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)))))))))))))))))).Types.snd (** val ticks_of0 : ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) -> BitVector.word -> ASM.pseudo_instruction -> (Nat.nat, Nat.nat) Types.prod **) let ticks_of0 program lookup_labels sigma policy ppc = function | ASM.Instruction instr -> (match instr with | ASM.ADD (arg1, arg2) -> let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.ADD (arg1, arg2))) in { Types.fst = ticks; Types.snd = ticks } | ASM.ADDC (arg1, arg2) -> let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.ADDC (arg1, arg2))) in { Types.fst = ticks; Types.snd = ticks } | ASM.SUBB (arg1, arg2) -> let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.SUBB (arg1, arg2))) in { Types.fst = ticks; Types.snd = ticks } | ASM.INC arg -> let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.INC arg)) in { Types.fst = ticks; Types.snd = ticks } | ASM.DEC arg -> let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.DEC arg)) in { Types.fst = ticks; Types.snd = ticks } | ASM.MUL (arg1, arg2) -> let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.MUL (arg1, arg2))) in { Types.fst = ticks; Types.snd = ticks } | ASM.DIV (arg1, arg2) -> let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.DIV (arg1, arg2))) in { Types.fst = ticks; Types.snd = ticks } | ASM.DA arg -> let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.DA arg)) in { Types.fst = ticks; Types.snd = ticks } | ASM.JC lbl -> let lookup_address = sigma (lookup_labels lbl) in let pc_plus_jmp_length = sigma (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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 (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)))))))))))))))) (Nat.S Nat.O))) in let { Types.fst = sj_possible; Types.snd = disp } = short_jump_cond pc_plus_jmp_length lookup_address in (match sj_possible with | Bool.True -> { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S Nat.O)) } | Bool.False -> { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) }) | ASM.JNC lbl -> let lookup_address = sigma (lookup_labels lbl) in let pc_plus_jmp_length = sigma (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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 (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)))))))))))))))) (Nat.S Nat.O))) in let { Types.fst = sj_possible; Types.snd = disp } = short_jump_cond pc_plus_jmp_length lookup_address in (match sj_possible with | Bool.True -> { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S Nat.O)) } | Bool.False -> { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) }) | ASM.JB (bit, lbl) -> let lookup_address = sigma (lookup_labels lbl) in let pc_plus_jmp_length = sigma (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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 (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)))))))))))))))) (Nat.S Nat.O))) in let { Types.fst = sj_possible; Types.snd = disp } = short_jump_cond pc_plus_jmp_length lookup_address in (match sj_possible with | Bool.True -> { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S Nat.O)) } | Bool.False -> { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) }) | ASM.JNB (bit, lbl) -> let lookup_address = sigma (lookup_labels lbl) in let pc_plus_jmp_length = sigma (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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 (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)))))))))))))))) (Nat.S Nat.O))) in let { Types.fst = sj_possible; Types.snd = disp } = short_jump_cond pc_plus_jmp_length lookup_address in (match sj_possible with | Bool.True -> { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S Nat.O)) } | Bool.False -> { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) }) | ASM.JBC (bit, lbl) -> let lookup_address = sigma (lookup_labels lbl) in let pc_plus_jmp_length = sigma (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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 (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)))))))))))))))) (Nat.S Nat.O))) in let { Types.fst = sj_possible; Types.snd = disp } = short_jump_cond pc_plus_jmp_length lookup_address in (match sj_possible with | Bool.True -> { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S Nat.O)) } | Bool.False -> { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) }) | ASM.JZ lbl -> let lookup_address = sigma (lookup_labels lbl) in let pc_plus_jmp_length = sigma (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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 (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)))))))))))))))) (Nat.S Nat.O))) in let { Types.fst = sj_possible; Types.snd = disp } = short_jump_cond pc_plus_jmp_length lookup_address in (match sj_possible with | Bool.True -> { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S Nat.O)) } | Bool.False -> { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) }) | ASM.JNZ lbl -> let lookup_address = sigma (lookup_labels lbl) in let pc_plus_jmp_length = sigma (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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 (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)))))))))))))))) (Nat.S Nat.O))) in let { Types.fst = sj_possible; Types.snd = disp } = short_jump_cond pc_plus_jmp_length lookup_address in (match sj_possible with | Bool.True -> { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S Nat.O)) } | Bool.False -> { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) }) | ASM.CJNE (arg, lbl) -> let lookup_address = sigma (lookup_labels lbl) in let pc_plus_jmp_length = sigma (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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 (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)))))))))))))))) (Nat.S Nat.O))) in let { Types.fst = sj_possible; Types.snd = disp } = short_jump_cond pc_plus_jmp_length lookup_address in (match sj_possible with | Bool.True -> { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S Nat.O)) } | Bool.False -> { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) }) | ASM.DJNZ (arg, lbl) -> let lookup_address = sigma (lookup_labels lbl) in let pc_plus_jmp_length = sigma (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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 (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)))))))))))))))) (Nat.S Nat.O))) in let { Types.fst = sj_possible; Types.snd = disp } = short_jump_cond pc_plus_jmp_length lookup_address in (match sj_possible with | Bool.True -> { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S Nat.O)) } | Bool.False -> { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) }) | ASM.ANL arg -> let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.ANL arg)) in { Types.fst = ticks; Types.snd = ticks } | ASM.ORL arg -> let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.ORL arg)) in { Types.fst = ticks; Types.snd = ticks } | ASM.XRL arg -> let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.XRL arg)) in { Types.fst = ticks; Types.snd = ticks } | ASM.CLR arg -> let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.CLR arg)) in { Types.fst = ticks; Types.snd = ticks } | ASM.CPL arg -> let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.CPL arg)) in { Types.fst = ticks; Types.snd = ticks } | ASM.RL arg -> let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.RL arg)) in { Types.fst = ticks; Types.snd = ticks } | ASM.RLC arg -> let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.RLC arg)) in { Types.fst = ticks; Types.snd = ticks } | ASM.RR arg -> let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.RR arg)) in { Types.fst = ticks; Types.snd = ticks } | ASM.RRC arg -> let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.RRC arg)) in { Types.fst = ticks; Types.snd = ticks } | ASM.SWAP arg -> let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.SWAP arg)) in { Types.fst = ticks; Types.snd = ticks } | ASM.MOV arg -> let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.MOV arg)) in { Types.fst = ticks; Types.snd = ticks } | ASM.MOVX arg -> let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.MOVX arg)) in { Types.fst = ticks; Types.snd = ticks } | ASM.SETB arg -> let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.SETB arg)) in { Types.fst = ticks; Types.snd = ticks } | ASM.PUSH arg -> let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.PUSH arg)) in { Types.fst = ticks; Types.snd = ticks } | ASM.POP arg -> let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.POP arg)) in { Types.fst = ticks; Types.snd = ticks } | ASM.XCH (arg1, arg2) -> let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.XCH (arg1, arg2))) in { Types.fst = ticks; Types.snd = ticks } | ASM.XCHD (arg1, arg2) -> let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.XCHD (arg1, arg2))) in { Types.fst = ticks; Types.snd = ticks } | ASM.RET -> let ticks = ticks_of_instruction (ASM.RealInstruction ASM.RET) in { Types.fst = ticks; Types.snd = ticks } | ASM.RETI -> let ticks = ticks_of_instruction (ASM.RealInstruction ASM.RETI) in { Types.fst = ticks; Types.snd = ticks } | ASM.NOP -> let ticks = ticks_of_instruction (ASM.RealInstruction ASM.NOP) in { Types.fst = ticks; Types.snd = ticks } | ASM.JMP x -> { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S Nat.O)) }) | ASM.Comment comment -> { Types.fst = Nat.O; Types.snd = Nat.O } | ASM.Cost cost -> let ticks = ticks_of_instruction (ASM.RealInstruction ASM.NOP) in { Types.fst = ticks; Types.snd = ticks } | ASM.Jmp jmp -> let pc_plus_jmp_length = sigma (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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 (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)))))))))))))))) (Nat.S Nat.O))) in let do_a_long = policy ppc in let lookup_address = sigma (lookup_labels jmp) in let { Types.fst = sj_possible; Types.snd = disp } = short_jump_cond pc_plus_jmp_length lookup_address in (match Bool.andb sj_possible (Bool.notb do_a_long) with | Bool.True -> { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S Nat.O)) } | Bool.False -> let { Types.fst = mj_possible; Types.snd = disp2 } = absolute_jump_cond pc_plus_jmp_length lookup_address in (match Bool.andb mj_possible (Bool.notb do_a_long) with | Bool.True -> { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S Nat.O)) } | Bool.False -> { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S Nat.O)) })) | ASM.Jnz (x, x0, x1) -> { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) } | ASM.Call call -> let pc_plus_jmp_length = sigma (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.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 (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)))))))))))))))) (Nat.S Nat.O))) in let lookup_address = sigma (lookup_labels call) in let { Types.fst = mj_possible; Types.snd = disp } = absolute_jump_cond pc_plus_jmp_length lookup_address in let do_a_long = policy ppc in (match Bool.andb mj_possible (Bool.notb do_a_long) with | Bool.True -> { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S Nat.O)) } | Bool.False -> { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S Nat.O)) }) | ASM.Mov (dst, lbl, off) -> (match dst with | Types.Inl x -> { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S Nat.O)) } | Types.Inr pr -> (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)))))) pr.Types.fst with | ASM.DIRECT d -> (fun _ -> { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S Nat.O)) }) | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *)) | ASM.REGISTER r -> (fun _ -> { Types.fst = (Nat.S Nat.O); Types.snd = (Nat.S Nat.O) }) | ASM.ACC_A -> (fun _ -> { Types.fst = (Nat.S Nat.O); Types.snd = (Nat.S Nat.O) }) | ASM.ACC_B -> (fun _ -> assert false (* absurd case *)) | ASM.DPTR -> (fun _ -> assert false (* absurd case *)) | ASM.DATA x -> (fun _ -> assert false (* absurd case *)) | ASM.DATA16 x -> (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 x -> (fun _ -> assert false (* absurd case *)) | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *)) | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *)) | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __) (** val ticks_of : ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) -> BitVector.word -> (Nat.nat, Nat.nat) Types.prod **) let ticks_of program addr_of sigma policy ppc = let { Types.fst = fetched; Types.snd = new_ppc } = ASM.fetch_pseudo_instruction program.ASM.code ppc in ticks_of0 program addr_of sigma policy ppc fetched