extracted/assembly.ml

   1 open Preamble
   2
   3 open Div_and_mod
   4
   5 open Jmeq
   6
   7 open Russell
   8
   9 open Util
  10
  11 open Bool
  12
  13 open Relations
  14
  15 open Nat
  16
  17 open List
  18
  19 open Hints_declaration
  20
  21 open Core_notation
  22
  23 open Pts
  24
  25 open Logic
  26
  27 open Types
  28
  29 open Extralib
  30
  31 open BitVectorTrie
  32
  33 open String
  34
  35 open Integers
  36
  37 open AST
  38
  39 open LabelledObjects
  40
  41 open Proper
  42
  43 open PositiveMap
  44
  45 open Deqsets
  46
  47 open ErrorMessages
  48
  49 open PreIdentifiers
  50
  51 open Errors
  52
  53 open Lists
  54
  55 open Positive
  56
  57 open Identifiers
  58
  59 open CostLabel
  60
  61 open ASM
  62
  63 open Exp
  64
  65 open Setoids
  66
  67 open Monad
  68
  69 open Option
  70
  71 open Extranat
  72
  73 open Vector
  74
  75 open FoldStuff
  76
  77 open BitVector
  78
  79 open Arithmetic
  80
  81 open Fetch
  82
  83 open Status
  84
  85 type jump_length =
  86 | Short_jump
  87 | Absolute_jump
  88 | Long_jump
  89
  90 (** val jump_length_rect_Type4 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1 **)
  91 let rec jump_length_rect_Type4 h_short_jump h_absolute_jump h_long_jump = function
  92 | Short_jump -> h_short_jump
  93 | Absolute_jump -> h_absolute_jump
  94 | Long_jump -> h_long_jump
  95
  96 (** val jump_length_rect_Type5 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1 **)
  97 let rec jump_length_rect_Type5 h_short_jump h_absolute_jump h_long_jump = function
  98 | Short_jump -> h_short_jump
  99 | Absolute_jump -> h_absolute_jump
 100 | Long_jump -> h_long_jump
 101
 102 (** val jump_length_rect_Type3 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1 **)
 103 let rec jump_length_rect_Type3 h_short_jump h_absolute_jump h_long_jump = function
 104 | Short_jump -> h_short_jump
 105 | Absolute_jump -> h_absolute_jump
 106 | Long_jump -> h_long_jump
 107
 108 (** val jump_length_rect_Type2 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1 **)
 109 let rec jump_length_rect_Type2 h_short_jump h_absolute_jump h_long_jump = function
 110 | Short_jump -> h_short_jump
 111 | Absolute_jump -> h_absolute_jump
 112 | Long_jump -> h_long_jump
 113
 114 (** val jump_length_rect_Type1 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1 **)
 115 let rec jump_length_rect_Type1 h_short_jump h_absolute_jump h_long_jump = function
 116 | Short_jump -> h_short_jump
 117 | Absolute_jump -> h_absolute_jump
 118 | Long_jump -> h_long_jump
 119
 120 (** val jump_length_rect_Type0 : 'a1 -> 'a1 -> 'a1 -> jump_length -> 'a1 **)
 121 let rec jump_length_rect_Type0 h_short_jump h_absolute_jump h_long_jump = function
 122 | Short_jump -> h_short_jump
 123 | Absolute_jump -> h_absolute_jump
 124 | Long_jump -> h_long_jump
 125
 126 (** val jump_length_inv_rect_Type4 :
 127     jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 128 let jump_length_inv_rect_Type4 hterm h1 h2 h3 =
 129   let hcut = jump_length_rect_Type4 h1 h2 h3 hterm in hcut __
 130
 131 (** val jump_length_inv_rect_Type3 :
 132     jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 133 let jump_length_inv_rect_Type3 hterm h1 h2 h3 =
 134   let hcut = jump_length_rect_Type3 h1 h2 h3 hterm in hcut __
 135
 136 (** val jump_length_inv_rect_Type2 :
 137     jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 138 let jump_length_inv_rect_Type2 hterm h1 h2 h3 =
 139   let hcut = jump_length_rect_Type2 h1 h2 h3 hterm in hcut __
 140
 141 (** val jump_length_inv_rect_Type1 :
 142     jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 143 let jump_length_inv_rect_Type1 hterm h1 h2 h3 =
 144   let hcut = jump_length_rect_Type1 h1 h2 h3 hterm in hcut __
 145
 146 (** val jump_length_inv_rect_Type0 :
 147     jump_length -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
 148 let jump_length_inv_rect_Type0 hterm h1 h2 h3 =
 149   let hcut = jump_length_rect_Type0 h1 h2 h3 hterm in hcut __
 150
 151 (** val jump_length_discr : jump_length -> jump_length -> __ **)
 152 let jump_length_discr x y =
 153   Logic.eq_rect_Type2 x
 154     (match x with
 155      | Short_jump -> Obj.magic (fun _ dH -> dH)
 156      | Absolute_jump -> Obj.magic (fun _ dH -> dH)
 157      | Long_jump -> Obj.magic (fun _ dH -> dH)) y
 158
 159 (** val jump_length_jmdiscr : jump_length -> jump_length -> __ **)
 160 let jump_length_jmdiscr x y =
 161   Logic.eq_rect_Type2 x
 162     (match x with
 163      | Short_jump -> Obj.magic (fun _ dH -> dH)
 164      | Absolute_jump -> Obj.magic (fun _ dH -> dH)
 165      | Long_jump -> Obj.magic (fun _ dH -> dH)) y
 166
 167 (** val short_jump_cond :
 168     BitVector.word -> BitVector.word -> (Bool.bool, BitVector.bitVector)
 169     Types.prod **)
 170 let short_jump_cond pc_plus_jmp_length addr =
 171   let { Types.fst = result; Types.snd = flags } =
 172     Arithmetic.sub_16_with_carry addr pc_plus_jmp_length Bool.False
 173   in
 174   let { Types.fst = upper; Types.snd = lower } =
 175     Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 176       (Nat.S Nat.O))))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 177       Nat.O))))))) result
 178   in
 179   (match Vector.get_index' (Nat.S (Nat.S Nat.O)) Nat.O flags with
 180    | Bool.True ->
 181      { Types.fst =
 182        (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 183          (Nat.S (Nat.S Nat.O))))))))) upper (Vector.VCons ((Nat.S (Nat.S
 184          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))), Bool.True,
 185          (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 186          Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
 187          (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
 188          (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S
 189          (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S
 190          (Nat.S (Nat.S Nat.O))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
 191          Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True,
 192          (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty)))))))))))))))))));
 193        Types.snd = (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 194        (Nat.S Nat.O))))))), Bool.True, lower)) }
 195    | Bool.False ->
 196      { Types.fst =
 197        (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 198          (Nat.S (Nat.S Nat.O))))))))) upper
 199          (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 200            (Nat.S (Nat.S Nat.O))))))))))); Types.snd = (Vector.VCons ((Nat.S
 201        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False,
 202        lower)) })
 203
 204 (** val absolute_jump_cond :
 205     BitVector.word -> BitVector.word -> (Bool.bool, BitVector.bitVector)
 206     Types.prod **)
 207 let absolute_jump_cond pc_plus_jmp_length addr =
 208   let { Types.fst = fst_5_addr; Types.snd = rest_addr } =
 209     Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S (Nat.S
 210       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 211       Nat.O))))))))))) addr
 212   in
 213   let { Types.fst = fst_5_pc; Types.snd = rest_pc } =
 214     Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S (Nat.S
 215       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 216       Nat.O))))))))))) pc_plus_jmp_length
 217   in
 218   { Types.fst =
 219   (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) fst_5_addr
 220     fst_5_pc); Types.snd = rest_addr }
 221
 222 (** val assembly_preinstruction :
 223     ('a1 -> BitVector.byte) -> 'a1 ASM.preinstruction -> Bool.bool
 224     Vector.vector List.list **)
 225 let assembly_preinstruction addr_of = function
 226 | ASM.ADD (addr1, addr2) ->
 227   (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
 228            ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S
 229            (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O),
 230            ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data,
 231            Vector.VEmpty)))))))) addr2 with
 232    | ASM.DIRECT b1 ->
 233      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 234        (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
 235        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
 236        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
 237        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
 238        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
 239        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
 240        Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.True,
 241        Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
 242    | ASM.INDIRECT i1 ->
 243      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 244        (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
 245        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
 246        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
 247        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
 248        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
 249        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
 250        Nat.O), Bool.True, (Vector.VCons (Nat.O, i1,
 251        Vector.VEmpty)))))))))))))))), List.Nil))
 252    | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
 253    | ASM.REGISTER r ->
 254      (fun _ -> List.Cons
 255        ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
 256           (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
 257           Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
 258           Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
 259           Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons
 260           (Nat.O, Bool.True, Vector.VEmpty)))))))))) r), List.Nil))
 261    | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
 262    | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
 263    | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
 264    | ASM.DATA b1 ->
 265      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 266        (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
 267        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
 268        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
 269        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
 270        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
 271        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
 272        Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
 273        Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
 274    | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
 275    | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
 276    | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
 277    | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 278    | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 279    | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
 280    | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
 281    | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
 282    | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
 283    | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
 284    | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
 285 | ASM.ADDC (addr1, addr2) ->
 286   (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
 287            ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S
 288            (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O),
 289            ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data,
 290            Vector.VEmpty)))))))) addr2 with
 291    | ASM.DIRECT b1 ->
 292      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 293        (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
 294        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
 295        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
 296        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
 297        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
 298        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
 299        Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.True,
 300        Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
 301    | ASM.INDIRECT i1 ->
 302      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 303        (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
 304        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
 305        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
 306        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
 307        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
 308        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
 309        Nat.O), Bool.True, (Vector.VCons (Nat.O, i1,
 310        Vector.VEmpty)))))))))))))))), List.Nil))
 311    | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
 312    | ASM.REGISTER r ->
 313      (fun _ -> List.Cons
 314        ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
 315           (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
 316           Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
 317           Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
 318           Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons
 319           (Nat.O, Bool.True, Vector.VEmpty)))))))))) r), List.Nil))
 320    | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
 321    | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
 322    | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
 323    | ASM.DATA b1 ->
 324      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 325        (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
 326        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
 327        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
 328        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
 329        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
 330        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
 331        Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
 332        Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
 333    | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
 334    | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
 335    | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
 336    | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 337    | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 338    | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
 339    | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
 340    | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
 341    | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
 342    | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
 343    | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
 344 | ASM.SUBB (addr1, addr2) ->
 345   (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
 346            ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S
 347            (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O),
 348            ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data,
 349            Vector.VEmpty)))))))) addr2 with
 350    | ASM.DIRECT b1 ->
 351      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 352        (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
 353        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
 354        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
 355        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
 356        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
 357        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
 358        Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.True,
 359        Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
 360    | ASM.INDIRECT i1 ->
 361      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 362        (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
 363        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
 364        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
 365        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
 366        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
 367        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
 368        Nat.O), Bool.True, (Vector.VCons (Nat.O, i1,
 369        Vector.VEmpty)))))))))))))))), List.Nil))
 370    | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
 371    | ASM.REGISTER r ->
 372      (fun _ -> List.Cons
 373        ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
 374           (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
 375           Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
 376           Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
 377           (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
 378           Bool.True, Vector.VEmpty)))))))))) r), List.Nil))
 379    | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
 380    | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
 381    | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
 382    | ASM.DATA b1 ->
 383      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 384        (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
 385        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
 386        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
 387        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
 388        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
 389        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
 390        Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
 391        Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
 392    | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
 393    | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
 394    | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
 395    | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 396    | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 397    | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
 398    | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
 399    | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
 400    | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
 401    | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
 402    | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
 403 | ASM.INC addr ->
 404   (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))
 405            (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), ASM.Acc_a,
 406            (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr,
 407            (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct, (Vector.VCons
 408            ((Nat.S Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Dptr,
 409            Vector.VEmpty)))))))))) addr with
 410    | ASM.DIRECT b1 ->
 411      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 412        (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
 413        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
 414        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
 415        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
 416        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
 417        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
 418        Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.True,
 419        Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
 420    | ASM.INDIRECT i1 ->
 421      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 422        (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
 423        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
 424        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
 425        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
 426        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
 427        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
 428        Nat.O), Bool.True, (Vector.VCons (Nat.O, i1,
 429        Vector.VEmpty)))))))))))))))), List.Nil))
 430    | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
 431    | ASM.REGISTER r ->
 432      (fun _ -> List.Cons
 433        ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
 434           (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
 435           Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
 436           Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
 437           Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons
 438           (Nat.O, Bool.True, Vector.VEmpty)))))))))) r), List.Nil))
 439    | ASM.ACC_A ->
 440      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 441        (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
 442        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
 443        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
 444        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
 445        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
 446        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
 447        Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
 448        Vector.VEmpty)))))))))))))))), List.Nil))
 449    | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
 450    | ASM.DPTR ->
 451      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 452        (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
 453        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
 454        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
 455        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
 456        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
 457        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
 458        ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True,
 459        Vector.VEmpty)))))))))))))))), List.Nil))
 460    | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
 461    | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
 462    | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
 463    | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
 464    | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 465    | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 466    | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
 467    | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
 468    | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
 469    | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
 470    | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
 471    | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
 472 | ASM.DEC addr ->
 473   (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
 474            ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Acc_a, (Vector.VCons ((Nat.S
 475            (Nat.S Nat.O)), ASM.Registr, (Vector.VCons ((Nat.S Nat.O),
 476            ASM.Direct, (Vector.VCons (Nat.O, ASM.Indirect,
 477            Vector.VEmpty)))))))) addr with
 478    | ASM.DIRECT b1 ->
 479      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 480        (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
 481        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
 482        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
 483        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
 484        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
 485        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
 486        Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.True,
 487        Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
 488    | ASM.INDIRECT i1 ->
 489      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 490        (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
 491        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
 492        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
 493        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
 494        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
 495        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
 496        Nat.O), Bool.True, (Vector.VCons (Nat.O, i1,
 497        Vector.VEmpty)))))))))))))))), List.Nil))
 498    | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
 499    | ASM.REGISTER r ->
 500      (fun _ -> List.Cons
 501        ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
 502           (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
 503           Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
 504           Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
 505           Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons
 506           (Nat.O, Bool.True, Vector.VEmpty)))))))))) r), List.Nil))
 507    | ASM.ACC_A ->
 508      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 509        (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
 510        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
 511        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
 512        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
 513        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
 514        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
 515        Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
 516        Vector.VEmpty)))))))))))))))), List.Nil))
 517    | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
 518    | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
 519    | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
 520    | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
 521    | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
 522    | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
 523    | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 524    | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 525    | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
 526    | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
 527    | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
 528    | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
 529    | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
 530    | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
 531 | ASM.MUL (addr1, addr2) ->
 532   List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 533     Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
 534     (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
 535     (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
 536     (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
 537     Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
 538     (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
 539     Bool.False, Vector.VEmpty)))))))))))))))), List.Nil)
 540 | ASM.DIV (addr1, addr2) ->
 541   List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 542     Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
 543     (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
 544     (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
 545     (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
 546     Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
 547     (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
 548     Bool.False, Vector.VEmpty)))))))))))))))), List.Nil)
 549 | ASM.DA addr ->
 550   List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 551     Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
 552     (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
 553     (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
 554     (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
 555     Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
 556     (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
 557     Bool.False, Vector.VEmpty)))))))))))))))), List.Nil)
 558 | ASM.JC addr ->
 559   let b1 = addr_of addr in
 560   List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 561   Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 562   (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
 563   (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
 564   Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
 565   Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
 566   ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
 567   Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil)))
 568 | ASM.JNC addr ->
 569   let b1 = addr_of addr in
 570   List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 571   Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 572   (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
 573   (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
 574   Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
 575   Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
 576   ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
 577   Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil)))
 578 | ASM.JB (addr1, addr2) ->
 579   let b2 = addr_of addr2 in
 580   (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Bit_addr,
 581            Vector.VEmpty)) addr1 with
 582    | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
 583    | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
 584    | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
 585    | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
 586    | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
 587    | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
 588    | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
 589    | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
 590    | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
 591    | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
 592    | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
 593    | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 594    | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 595    | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
 596    | ASM.BIT_ADDR b1 ->
 597      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 598        (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
 599        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
 600        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
 601        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
 602        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
 603        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
 604        ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
 605        Vector.VEmpty)))))))))))))))), (List.Cons (b1, (List.Cons (b2,
 606        List.Nil))))))
 607    | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
 608    | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
 609    | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
 610    | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
 611 | ASM.JNB (addr1, addr2) ->
 612   let b2 = addr_of addr2 in
 613   (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Bit_addr,
 614            Vector.VEmpty)) addr1 with
 615    | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
 616    | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
 617    | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
 618    | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
 619    | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
 620    | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
 621    | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
 622    | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
 623    | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
 624    | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
 625    | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
 626    | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 627    | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 628    | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
 629    | ASM.BIT_ADDR b1 ->
 630      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 631        (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
 632        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
 633        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
 634        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
 635        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
 636        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
 637        ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
 638        Vector.VEmpty)))))))))))))))), (List.Cons (b1, (List.Cons (b2,
 639        List.Nil))))))
 640    | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
 641    | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
 642    | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
 643    | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
 644 | ASM.JBC (addr1, addr2) ->
 645   let b2 = addr_of addr2 in
 646   (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Bit_addr,
 647            Vector.VEmpty)) addr1 with
 648    | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
 649    | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
 650    | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
 651    | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
 652    | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
 653    | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
 654    | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
 655    | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
 656    | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
 657    | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
 658    | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
 659    | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 660    | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 661    | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
 662    | ASM.BIT_ADDR b1 ->
 663      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 664        (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
 665        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
 666        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
 667        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
 668        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
 669        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
 670        ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
 671        Vector.VEmpty)))))))))))))))), (List.Cons (b1, (List.Cons (b2,
 672        List.Nil))))))
 673    | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
 674    | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
 675    | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
 676    | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
 677 | ASM.JZ addr ->
 678   let b1 = addr_of addr in
 679   List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 680   Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 681   (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
 682   (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
 683   Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
 684   Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
 685   ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
 686   Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil)))
 687 | ASM.JNZ addr ->
 688   let b1 = addr_of addr in
 689   List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 690   Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 691   (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
 692   (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
 693   Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
 694   Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
 695   ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
 696   Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil)))
 697 | ASM.CJNE (addrs, addr3) ->
 698   let b3 = addr_of addr3 in
 699   (match addrs with
 700    | Types.Inl addrs0 ->
 701      let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in
 702      (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
 703               Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Data,
 704               Vector.VEmpty)))) addr2 with
 705       | ASM.DIRECT b1 ->
 706         (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
 707           (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
 708           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False,
 709           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
 710           Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
 711           Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
 712           Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
 713           (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
 714           Bool.True, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
 715           (List.Cons (b3, List.Nil))))))
 716       | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
 717       | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
 718       | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
 719       | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
 720       | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
 721       | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
 722       | ASM.DATA b1 ->
 723         (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
 724           (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
 725           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False,
 726           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
 727           Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
 728           Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
 729           Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
 730           (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
 731           Bool.False, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
 732           (List.Cons (b3, List.Nil))))))
 733       | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
 734       | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
 735       | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
 736       | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 737       | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 738       | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
 739       | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
 740       | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
 741       | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
 742       | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
 743       | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
 744    | Types.Inr addrs0 ->
 745      let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in
 746      let b2 =
 747        (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Data,
 748                 Vector.VEmpty)) addr2 with
 749         | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
 750         | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
 751         | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
 752         | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
 753         | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
 754         | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
 755         | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
 756         | ASM.DATA b2 -> (fun _ -> b2)
 757         | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
 758         | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
 759         | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
 760         | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 761         | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 762         | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
 763         | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
 764         | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
 765         | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
 766         | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
 767         | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
 768      in
 769      (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
 770               Nat.O), ASM.Registr, (Vector.VCons (Nat.O, ASM.Indirect,
 771               Vector.VEmpty)))) addr1 with
 772       | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
 773       | ASM.INDIRECT i1 ->
 774         (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
 775           (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
 776           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False,
 777           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
 778           Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
 779           Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
 780           Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
 781           (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, i1,
 782           Vector.VEmpty)))))))))))))))), (List.Cons (b2, (List.Cons (b3,
 783           List.Nil))))))
 784       | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
 785       | ASM.REGISTER r ->
 786         (fun _ -> List.Cons
 787           ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
 788              (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S
 789              (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
 790              (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
 791              Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True,
 792              (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty)))))))))) r),
 793           (List.Cons (b2, (List.Cons (b3, List.Nil))))))
 794       | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
 795       | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
 796       | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
 797       | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
 798       | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
 799       | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
 800       | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
 801       | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 802       | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 803       | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
 804       | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
 805       | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
 806       | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
 807       | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
 808       | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
 809 | ASM.DJNZ (addr1, addr2) ->
 810   let b2 = addr_of addr2 in
 811   (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O),
 812            ASM.Registr, (Vector.VCons (Nat.O, ASM.Direct, Vector.VEmpty))))
 813            addr1 with
 814    | ASM.DIRECT b1 ->
 815      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 816        (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
 817        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons
 818        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
 819        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
 820        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
 821        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
 822        Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.True,
 823        Vector.VEmpty)))))))))))))))), (List.Cons (b1, (List.Cons (b2,
 824        List.Nil))))))
 825    | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
 826    | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
 827    | ASM.REGISTER r ->
 828      (fun _ -> List.Cons
 829        ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
 830           (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
 831           Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
 832           Bool.True, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
 833           (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
 834           Bool.True, Vector.VEmpty)))))))))) r), (List.Cons (b2, List.Nil))))
 835    | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
 836    | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
 837    | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
 838    | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
 839    | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
 840    | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
 841    | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
 842    | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 843    | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 844    | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
 845    | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
 846    | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
 847    | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
 848    | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
 849    | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
 850 | ASM.ANL addrs ->
 851   (match addrs with
 852    | Types.Inl addrs0 ->
 853      (match addrs0 with
 854       | Types.Inl addrs1 ->
 855         let { Types.fst = addr1; Types.snd = addr2 } = addrs1 in
 856         (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O)))
 857                  (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr,
 858                  (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Direct,
 859                  (Vector.VCons ((Nat.S Nat.O), ASM.Indirect, (Vector.VCons
 860                  (Nat.O, ASM.Data, Vector.VEmpty)))))))) addr2 with
 861          | ASM.DIRECT b1 ->
 862            (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
 863              (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
 864              ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
 865              Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 866              Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
 867              (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
 868              Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
 869              Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False,
 870              (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty)))))))))))))))),
 871              (List.Cons (b1, List.Nil))))
 872          | ASM.INDIRECT i1 ->
 873            (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
 874              (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
 875              ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
 876              Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 877              Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
 878              (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
 879              Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
 880              Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True,
 881              (Vector.VCons (Nat.O, i1, Vector.VEmpty)))))))))))))))),
 882              List.Nil))
 883          | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
 884          | ASM.REGISTER r ->
 885            (fun _ -> List.Cons
 886              ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
 887                 (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S
 888                 (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S
 889                 (Nat.S (Nat.S Nat.O))), Bool.True, (Vector.VCons ((Nat.S
 890                 (Nat.S Nat.O)), Bool.False, (Vector.VCons ((Nat.S Nat.O),
 891                 Bool.True, (Vector.VCons (Nat.O, Bool.True,
 892                 Vector.VEmpty)))))))))) r), List.Nil))
 893          | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
 894          | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
 895          | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
 896          | ASM.DATA b1 ->
 897            (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
 898              (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
 899              ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
 900              Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 901              Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
 902              (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
 903              Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
 904              Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False,
 905              (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty)))))))))))))))),
 906              (List.Cons (b1, List.Nil))))
 907          | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
 908          | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
 909          | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
 910          | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 911          | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 912          | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
 913          | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
 914          | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
 915          | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
 916          | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
 917          | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
 918       | Types.Inr addrs1 ->
 919         let { Types.fst = addr1; Types.snd = addr2 } = addrs1 in
 920         let b1 =
 921           (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O,
 922                    ASM.Direct, Vector.VEmpty)) addr1 with
 923            | ASM.DIRECT b1 -> (fun _ -> b1)
 924            | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
 925            | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
 926            | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
 927            | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
 928            | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
 929            | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
 930            | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
 931            | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
 932            | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
 933            | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
 934            | ASM.EXT_INDIRECT_DPTR ->
 935              (fun _ -> assert false (* absurd case *))
 936            | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 937            | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
 938            | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
 939            | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
 940            | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
 941            | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
 942            | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
 943         in
 944         (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
 945                  Nat.O), ASM.Acc_a, (Vector.VCons (Nat.O, ASM.Data,
 946                  Vector.VEmpty)))) addr2 with
 947          | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
 948          | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
 949          | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
 950          | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
 951          | ASM.ACC_A ->
 952            (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
 953              (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
 954              ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
 955              Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 956              Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
 957              (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
 958              Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
 959              Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.True,
 960              (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty)))))))))))))))),
 961              (List.Cons (b1, List.Nil))))
 962          | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
 963          | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
 964          | ASM.DATA b2 ->
 965            (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
 966              (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
 967              ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
 968              Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 969              Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
 970              (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
 971              Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
 972              Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.True,
 973              (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty)))))))))))))))),
 974              (List.Cons (b1, (List.Cons (b2, List.Nil))))))
 975          | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
 976          | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
 977          | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
 978          | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 979          | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
 980          | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
 981          | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
 982          | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
 983          | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
 984          | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
 985          | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
 986    | Types.Inr addrs0 ->
 987      let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in
 988      (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
 989               Nat.O), ASM.Bit_addr, (Vector.VCons (Nat.O, ASM.N_bit_addr,
 990               Vector.VEmpty)))) addr2 with
 991       | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
 992       | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
 993       | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
 994       | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
 995       | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
 996       | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
 997       | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
 998       | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
 999       | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1000       | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1001       | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1002       | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1003       | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1004       | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1005       | ASM.BIT_ADDR b1 ->
1006         (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1007           (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
1008           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False,
1009           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1010           Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1011           Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1012           Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1013           (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
1014           Bool.False, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1015           List.Nil))))
1016       | ASM.N_BIT_ADDR b1 ->
1017         (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1018           (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
1019           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False,
1020           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1021           Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1022           Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1023           Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1024           (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
1025           Bool.False, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1026           List.Nil))))
1027       | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1028       | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1029       | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
1030 | ASM.ORL addrs ->
1031   (match addrs with
1032    | Types.Inl addrs0 ->
1033      (match addrs0 with
1034       | Types.Inl addrs1 ->
1035         let { Types.fst = addr1; Types.snd = addr2 } = addrs1 in
1036         (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O)))
1037                  (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Registr,
1038                  (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Data,
1039                  (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons
1040                  (Nat.O, ASM.Indirect, Vector.VEmpty)))))))) addr2 with
1041          | ASM.DIRECT b1 ->
1042            (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1043              (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1044              ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
1045              Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1046              Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1047              (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1048              (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1049              Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False,
1050              (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty)))))))))))))))),
1051              (List.Cons (b1, List.Nil))))
1052          | ASM.INDIRECT i1 ->
1053            (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1054              (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1055              ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
1056              Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1057              Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1058              (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1059              (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1060              Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.True,
1061              (Vector.VCons (Nat.O, i1, Vector.VEmpty)))))))))))))))),
1062              List.Nil))
1063          | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1064          | ASM.REGISTER r ->
1065            (fun _ -> List.Cons
1066              ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
1067                 (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S
1068                 (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S
1069                 (Nat.S (Nat.S Nat.O))), Bool.True, (Vector.VCons ((Nat.S
1070                 (Nat.S Nat.O)), Bool.False, (Vector.VCons ((Nat.S Nat.O),
1071                 Bool.False, (Vector.VCons (Nat.O, Bool.True,
1072                 Vector.VEmpty)))))))))) r), List.Nil))
1073          | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1074          | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1075          | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1076          | ASM.DATA b1 ->
1077            (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1078              (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1079              ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
1080              Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1081              Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1082              (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1083              (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1084              Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False,
1085              (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty)))))))))))))))),
1086              (List.Cons (b1, List.Nil))))
1087          | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1088          | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1089          | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1090          | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1091          | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1092          | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1093          | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1094          | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1095          | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1096          | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1097          | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
1098       | Types.Inr addrs1 ->
1099         let { Types.fst = addr1; Types.snd = addr2 } = addrs1 in
1100         let b1 =
1101           (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O,
1102                    ASM.Direct, Vector.VEmpty)) addr1 with
1103            | ASM.DIRECT b1 -> (fun _ -> b1)
1104            | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1105            | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1106            | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1107            | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1108            | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1109            | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1110            | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1111            | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1112            | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1113            | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1114            | ASM.EXT_INDIRECT_DPTR ->
1115              (fun _ -> assert false (* absurd case *))
1116            | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1117            | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1118            | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1119            | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1120            | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1121            | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1122            | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
1123         in
1124         (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
1125                  Nat.O), ASM.Acc_a, (Vector.VCons (Nat.O, ASM.Data,
1126                  Vector.VEmpty)))) addr2 with
1127          | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1128          | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1129          | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1130          | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1131          | ASM.ACC_A ->
1132            (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1133              (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1134              ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
1135              Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1136              Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1137              (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1138              (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1139              Nat.O)), Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.True,
1140              (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty)))))))))))))))),
1141              (List.Cons (b1, List.Nil))))
1142          | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1143          | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1144          | ASM.DATA b2 ->
1145            (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1146              (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1147              ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
1148              Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1149              Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1150              (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1151              (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1152              Nat.O)), Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.True,
1153              (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty)))))))))))))))),
1154              (List.Cons (b1, (List.Cons (b2, List.Nil))))))
1155          | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1156          | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1157          | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1158          | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1159          | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1160          | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1161          | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1162          | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1163          | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1164          | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1165          | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
1166    | Types.Inr addrs0 ->
1167      let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in
1168      (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
1169               Nat.O), ASM.Bit_addr, (Vector.VCons (Nat.O, ASM.N_bit_addr,
1170               Vector.VEmpty)))) addr2 with
1171       | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1172       | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1173       | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1174       | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1175       | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1176       | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1177       | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1178       | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1179       | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1180       | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1181       | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1182       | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1183       | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1184       | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1185       | ASM.BIT_ADDR b1 ->
1186         (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1187           (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1188           ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
1189           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1190           Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1191           Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1192           Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1193           (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
1194           Bool.False, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1195           List.Nil))))
1196       | ASM.N_BIT_ADDR b1 ->
1197         (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1198           (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
1199           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False,
1200           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1201           Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1202           Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1203           Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1204           (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
1205           Bool.False, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1206           List.Nil))))
1207       | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1208       | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1209       | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
1210 | ASM.XRL addrs ->
1211   (match addrs with
1212    | Types.Inl addrs0 ->
1213      let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in
1214      (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O)))
1215               (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), ASM.Data,
1216               (Vector.VCons ((Nat.S (Nat.S Nat.O)), ASM.Registr,
1217               (Vector.VCons ((Nat.S Nat.O), ASM.Direct, (Vector.VCons (Nat.O,
1218               ASM.Indirect, Vector.VEmpty)))))))) addr2 with
1219       | ASM.DIRECT b1 ->
1220         (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1221           (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1222           ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
1223           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1224           Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1225           Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1226           Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
1227           (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
1228           Bool.True, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1229           List.Nil))))
1230       | ASM.INDIRECT i1 ->
1231         (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1232           (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1233           ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
1234           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1235           Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1236           Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1237           Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
1238           (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, i1,
1239           Vector.VEmpty)))))))))))))))), List.Nil))
1240       | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1241       | ASM.REGISTER r ->
1242         (fun _ -> List.Cons
1243           ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))
1244              (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S
1245              (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S
1246              (Nat.S (Nat.S Nat.O))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1247              Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O), Bool.False,
1248              (Vector.VCons (Nat.O, Bool.True, Vector.VEmpty)))))))))) r),
1249           List.Nil))
1250       | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1251       | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1252       | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1253       | ASM.DATA b1 ->
1254         (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1255           (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1256           ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
1257           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1258           Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1259           Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1260           Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
1261           (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
1262           Bool.False, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1263           List.Nil))))
1264       | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1265       | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1266       | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1267       | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1268       | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1269       | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1270       | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1271       | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1272       | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1273       | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1274       | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
1275    | Types.Inr addrs0 ->
1276      let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in
1277      let b1 =
1278        (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O,
1279                 ASM.Direct, Vector.VEmpty)) addr1 with
1280         | ASM.DIRECT b1 -> (fun _ -> b1)
1281         | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1282         | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1283         | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1284         | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1285         | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1286         | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1287         | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1288         | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1289         | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1290         | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1291         | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1292         | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1293         | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1294         | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1295         | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1296         | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1297         | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1298         | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
1299      in
1300      (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
1301               Nat.O), ASM.Acc_a, (Vector.VCons (Nat.O, ASM.Data,
1302               Vector.VEmpty)))) addr2 with
1303       | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1304       | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1305       | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1306       | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1307       | ASM.ACC_A ->
1308         (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1309           (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1310           ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
1311           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1312           Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1313           Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1314           Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1315           (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
1316           Bool.False, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1317           List.Nil))))
1318       | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1319       | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1320       | ASM.DATA b2 ->
1321         (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1322           (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False, (Vector.VCons
1323           ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
1324           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1325           Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1326           Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1327           Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1328           (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
1329           Bool.True, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1330           (List.Cons (b2, List.Nil))))))
1331       | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1332       | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1333       | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1334       | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1335       | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1336       | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1337       | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1338       | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1339       | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1340       | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1341       | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
1342 | ASM.CLR addr ->
1343   (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S
1344            (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O),
1345            ASM.Carry, (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty))))))
1346            addr with
1347    | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1348    | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1349    | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1350    | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1351    | ASM.ACC_A ->
1352      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1353        (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1354        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons
1355        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
1356        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
1357        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
1358        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
1359        Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
1360        Vector.VEmpty)))))))))))))))), List.Nil))
1361    | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1362    | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1363    | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1364    | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1365    | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1366    | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1367    | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1368    | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1369    | ASM.CARRY ->
1370      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1371        (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1372        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons
1373        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
1374        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
1375        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
1376        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
1377        ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True,
1378        Vector.VEmpty)))))))))))))))), List.Nil))
1379    | ASM.BIT_ADDR b1 ->
1380      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1381        (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1382        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons
1383        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
1384        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
1385        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
1386        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
1387        ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.False,
1388        Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
1389    | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1390    | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1391    | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1392    | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
1393 | ASM.CPL addr ->
1394   (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S
1395            (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O),
1396            ASM.Carry, (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty))))))
1397            addr with
1398    | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1399    | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1400    | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1401    | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1402    | ASM.ACC_A ->
1403      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1404        (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1405        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons
1406        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
1407        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
1408        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
1409        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
1410        Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
1411        Vector.VEmpty)))))))))))))))), List.Nil))
1412    | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1413    | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1414    | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1415    | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1416    | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1417    | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1418    | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1419    | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1420    | ASM.CARRY ->
1421      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1422        (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1423        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
1424        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
1425        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
1426        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
1427        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
1428        ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True,
1429        Vector.VEmpty)))))))))))))))), List.Nil))
1430    | ASM.BIT_ADDR b1 ->
1431      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1432        (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1433        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
1434        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
1435        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
1436        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
1437        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
1438        ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.False,
1439        Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
1440    | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1441    | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1442    | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1443    | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
1444 | ASM.RL addr ->
1445   List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1446     Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1447     (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1448     (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1449     (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1450     Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1451     (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True,
1452     Vector.VEmpty)))))))))))))))), List.Nil)
1453 | ASM.RLC addr ->
1454   List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1455     Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1456     (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1457     (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1458     (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1459     Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1460     (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True,
1461     Vector.VEmpty)))))))))))))))), List.Nil)
1462 | ASM.RR addr ->
1463   List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1464     Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1465     (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1466     (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1467     (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1468     Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1469     (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True,
1470     Vector.VEmpty)))))))))))))))), List.Nil)
1471 | ASM.RRC addr ->
1472   List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1473     Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1474     (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1475     (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1476     (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1477     Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1478     (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True,
1479     Vector.VEmpty)))))))))))))))), List.Nil)
1480 | ASM.SWAP addr ->
1481   List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1482     Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1483     (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1484     (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1485     (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1486     Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
1487     (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
1488     Bool.False, Vector.VEmpty)))))))))))))))), List.Nil)
1489 | ASM.MOV addrs ->
1490   (match addrs with
1491    | Types.Inl addrs0 ->
1492      (match addrs0 with
1493       | Types.Inl addrs1 ->
1494         (match addrs1 with
1495          | Types.Inl addrs2 ->
1496            (match addrs2 with
1497             | Types.Inl addrs3 ->
1498               (match addrs3 with
1499                | Types.Inl addrs4 ->
1500                  let { Types.fst = addr1; Types.snd = addr2 } = addrs4 in
1501                  (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S
1502                           Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S
1503                           Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S (Nat.S
1504                           Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S Nat.O),
1505                           ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data,
1506                           Vector.VEmpty)))))))) addr2 with
1507                   | ASM.DIRECT b1 ->
1508                     (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S
1509                       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True,
1510                       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1511                       (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S
1512                       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
1513                       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1514                       Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1515                       Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1516                       Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O),
1517                       Bool.False, (Vector.VCons (Nat.O, Bool.True,
1518                       Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1519                       List.Nil))))
1520                   | ASM.INDIRECT i1 ->
1521                     (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S
1522                       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True,
1523                       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1524                       (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S
1525                       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
1526                       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1527                       Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1528                       Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1529                       Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O),
1530                       Bool.True, (Vector.VCons (Nat.O, i1,
1531                       Vector.VEmpty)))))))))))))))), List.Nil))
1532                   | ASM.EXT_INDIRECT x ->
1533                     (fun _ -> assert false (* absurd case *))
1534                   | ASM.REGISTER r ->
1535                     (fun _ -> List.Cons
1536                       ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1537                          Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O)))
1538                          (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1539                          Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1540                          (Nat.S Nat.O))), Bool.True, (Vector.VCons ((Nat.S
1541                          (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
1542                          Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.True,
1543                          Vector.VEmpty)))))))))) r), List.Nil))
1544                   | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1545                   | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1546                   | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1547                   | ASM.DATA b1 ->
1548                     (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S
1549                       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False,
1550                       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1551                       (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S
1552                       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True,
1553                       (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1554                       Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1555                       Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1556                       Nat.O)), Bool.True, (Vector.VCons ((Nat.S Nat.O),
1557                       Bool.False, (Vector.VCons (Nat.O, Bool.False,
1558                       Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1559                       List.Nil))))
1560                   | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1561                   | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1562                   | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1563                   | ASM.EXT_INDIRECT_DPTR ->
1564                     (fun _ -> assert false (* absurd case *))
1565                   | ASM.INDIRECT_DPTR ->
1566                     (fun _ -> assert false (* absurd case *))
1567                   | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1568                   | ASM.BIT_ADDR x ->
1569                     (fun _ -> assert false (* absurd case *))
1570                   | ASM.N_BIT_ADDR x ->
1571                     (fun _ -> assert false (* absurd case *))
1572                   | ASM.RELATIVE x ->
1573                     (fun _ -> assert false (* absurd case *))
1574                   | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1575                   | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *)))
1576                    __
1577                | Types.Inr addrs4 ->
1578                  let { Types.fst = addr1; Types.snd = addr2 } = addrs4 in
1579                  (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons
1580                           ((Nat.S Nat.O), ASM.Registr, (Vector.VCons (Nat.O,
1581                           ASM.Indirect, Vector.VEmpty)))) addr1 with
1582                   | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1583                   | ASM.INDIRECT i1 ->
1584                     (fun _ ->
1585                       (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O))
1586                                (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1587                                ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O),
1588                                ASM.Direct, (Vector.VCons (Nat.O, ASM.Data,
1589                                Vector.VEmpty)))))) addr2 with
1590                        | ASM.DIRECT b1 ->
1591                          (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S
1592                            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))),
1593                            Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1594                            (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False,
1595                            (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1596                            Nat.O))))), Bool.True, (Vector.VCons ((Nat.S
1597                            (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
1598                            (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1599                            Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1600                            Bool.True, (Vector.VCons ((Nat.S Nat.O),
1601                            Bool.True, (Vector.VCons (Nat.O, i1,
1602                            Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1603                            List.Nil))))
1604                        | ASM.INDIRECT x0 ->
1605                          (fun _ -> assert false (* absurd case *))
1606                        | ASM.EXT_INDIRECT x0 ->
1607                          (fun _ -> assert false (* absurd case *))
1608                        | ASM.REGISTER x0 ->
1609                          (fun _ -> assert false (* absurd case *))
1610                        | ASM.ACC_A ->
1611                          (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S
1612                            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))),
1613                            Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1614                            (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
1615                            (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1616                            Nat.O))))), Bool.True, (Vector.VCons ((Nat.S
1617                            (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
1618                            (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1619                            Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1620                            Bool.True, (Vector.VCons ((Nat.S Nat.O),
1621                            Bool.True, (Vector.VCons (Nat.O, i1,
1622                            Vector.VEmpty)))))))))))))))), List.Nil))
1623                        | ASM.ACC_B ->
1624                          (fun _ -> assert false (* absurd case *))
1625                        | ASM.DPTR ->
1626                          (fun _ -> assert false (* absurd case *))
1627                        | ASM.DATA b1 ->
1628                          (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S
1629                            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))),
1630                            Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1631                            (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
1632                            (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1633                            Nat.O))))), Bool.True, (Vector.VCons ((Nat.S
1634                            (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
1635                            (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1636                            Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1637                            Bool.True, (Vector.VCons ((Nat.S Nat.O),
1638                            Bool.True, (Vector.VCons (Nat.O, i1,
1639                            Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1640                            List.Nil))))
1641                        | ASM.DATA16 x0 ->
1642                          (fun _ -> assert false (* absurd case *))
1643                        | ASM.ACC_DPTR ->
1644                          (fun _ -> assert false (* absurd case *))
1645                        | ASM.ACC_PC ->
1646                          (fun _ -> assert false (* absurd case *))
1647                        | ASM.EXT_INDIRECT_DPTR ->
1648                          (fun _ -> assert false (* absurd case *))
1649                        | ASM.INDIRECT_DPTR ->
1650                          (fun _ -> assert false (* absurd case *))
1651                        | ASM.CARRY ->
1652                          (fun _ -> assert false (* absurd case *))
1653                        | ASM.BIT_ADDR x0 ->
1654                          (fun _ -> assert false (* absurd case *))
1655                        | ASM.N_BIT_ADDR x0 ->
1656                          (fun _ -> assert false (* absurd case *))
1657                        | ASM.RELATIVE x0 ->
1658                          (fun _ -> assert false (* absurd case *))
1659                        | ASM.ADDR11 x0 ->
1660                          (fun _ -> assert false (* absurd case *))
1661                        | ASM.ADDR16 x0 ->
1662                          (fun _ -> assert false (* absurd case *))) __)
1663                   | ASM.EXT_INDIRECT x ->
1664                     (fun _ -> assert false (* absurd case *))
1665                   | ASM.REGISTER r ->
1666                     (fun _ ->
1667                       (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O))
1668                                (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1669                                ASM.Acc_a, (Vector.VCons ((Nat.S Nat.O),
1670                                ASM.Direct, (Vector.VCons (Nat.O, ASM.Data,
1671                                Vector.VEmpty)))))) addr2 with
1672                        | ASM.DIRECT b1 ->
1673                          (fun _ -> List.Cons
1674                            ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1675                               Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O)))
1676                               (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1677                               Nat.O)))), Bool.True, (Vector.VCons ((Nat.S
1678                               (Nat.S (Nat.S Nat.O))), Bool.False,
1679                               (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1680                               Bool.True, (Vector.VCons ((Nat.S Nat.O),
1681                               Bool.False, (Vector.VCons (Nat.O, Bool.True,
1682                               Vector.VEmpty)))))))))) r), (List.Cons (b1,
1683                            List.Nil))))
1684                        | ASM.INDIRECT x0 ->
1685                          (fun _ -> assert false (* absurd case *))
1686                        | ASM.EXT_INDIRECT x0 ->
1687                          (fun _ -> assert false (* absurd case *))
1688                        | ASM.REGISTER x0 ->
1689                          (fun _ -> assert false (* absurd case *))
1690                        | ASM.ACC_A ->
1691                          (fun _ -> List.Cons
1692                            ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1693                               Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O)))
1694                               (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1695                               Nat.O)))), Bool.True, (Vector.VCons ((Nat.S
1696                               (Nat.S (Nat.S Nat.O))), Bool.True,
1697                               (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1698                               Bool.True, (Vector.VCons ((Nat.S Nat.O),
1699                               Bool.True, (Vector.VCons (Nat.O, Bool.True,
1700                               Vector.VEmpty)))))))))) r), List.Nil))
1701                        | ASM.ACC_B ->
1702                          (fun _ -> assert false (* absurd case *))
1703                        | ASM.DPTR ->
1704                          (fun _ -> assert false (* absurd case *))
1705                        | ASM.DATA b1 ->
1706                          (fun _ -> List.Cons
1707                            ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1708                               Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O)))
1709                               (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1710                               Nat.O)))), Bool.False, (Vector.VCons ((Nat.S
1711                               (Nat.S (Nat.S Nat.O))), Bool.True,
1712                               (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1713                               Bool.True, (Vector.VCons ((Nat.S Nat.O),
1714                               Bool.True, (Vector.VCons (Nat.O, Bool.True,
1715                               Vector.VEmpty)))))))))) r), (List.Cons (b1,
1716                            List.Nil))))
1717                        | ASM.DATA16 x0 ->
1718                          (fun _ -> assert false (* absurd case *))
1719                        | ASM.ACC_DPTR ->
1720                          (fun _ -> assert false (* absurd case *))
1721                        | ASM.ACC_PC ->
1722                          (fun _ -> assert false (* absurd case *))
1723                        | ASM.EXT_INDIRECT_DPTR ->
1724                          (fun _ -> assert false (* absurd case *))
1725                        | ASM.INDIRECT_DPTR ->
1726                          (fun _ -> assert false (* absurd case *))
1727                        | ASM.CARRY ->
1728                          (fun _ -> assert false (* absurd case *))
1729                        | ASM.BIT_ADDR x0 ->
1730                          (fun _ -> assert false (* absurd case *))
1731                        | ASM.N_BIT_ADDR x0 ->
1732                          (fun _ -> assert false (* absurd case *))
1733                        | ASM.RELATIVE x0 ->
1734                          (fun _ -> assert false (* absurd case *))
1735                        | ASM.ADDR11 x0 ->
1736                          (fun _ -> assert false (* absurd case *))
1737                        | ASM.ADDR16 x0 ->
1738                          (fun _ -> assert false (* absurd case *))) __)
1739                   | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1740                   | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1741                   | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1742                   | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1743                   | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1744                   | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1745                   | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1746                   | ASM.EXT_INDIRECT_DPTR ->
1747                     (fun _ -> assert false (* absurd case *))
1748                   | ASM.INDIRECT_DPTR ->
1749                     (fun _ -> assert false (* absurd case *))
1750                   | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1751                   | ASM.BIT_ADDR x ->
1752                     (fun _ -> assert false (* absurd case *))
1753                   | ASM.N_BIT_ADDR x ->
1754                     (fun _ -> assert false (* absurd case *))
1755                   | ASM.RELATIVE x ->
1756                     (fun _ -> assert false (* absurd case *))
1757                   | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1758                   | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *)))
1759                    __)
1760             | Types.Inr addrs3 ->
1761               let { Types.fst = addr1; Types.snd = addr2 } = addrs3 in
1762               let b1 =
1763                 (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O,
1764                          ASM.Direct, Vector.VEmpty)) addr1 with
1765                  | ASM.DIRECT b1 -> (fun _ -> b1)
1766                  | ASM.INDIRECT x ->
1767                    (fun _ -> assert false (* absurd case *))
1768                  | ASM.EXT_INDIRECT x ->
1769                    (fun _ -> assert false (* absurd case *))
1770                  | ASM.REGISTER x ->
1771                    (fun _ -> assert false (* absurd case *))
1772                  | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1773                  | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1774                  | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1775                  | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1776                  | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1777                  | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1778                  | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1779                  | ASM.EXT_INDIRECT_DPTR ->
1780                    (fun _ -> assert false (* absurd case *))
1781                  | ASM.INDIRECT_DPTR ->
1782                    (fun _ -> assert false (* absurd case *))
1783                  | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1784                  | ASM.BIT_ADDR x ->
1785                    (fun _ -> assert false (* absurd case *))
1786                  | ASM.N_BIT_ADDR x ->
1787                    (fun _ -> assert false (* absurd case *))
1788                  | ASM.RELATIVE x ->
1789                    (fun _ -> assert false (* absurd case *))
1790                  | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1791                  | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *)))
1792                   __
1793               in
1794               (match ASM.subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S
1795                        Nat.O)))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1796                        Nat.O)))), ASM.Acc_a, (Vector.VCons ((Nat.S (Nat.S
1797                        (Nat.S Nat.O))), ASM.Registr, (Vector.VCons ((Nat.S
1798                        (Nat.S Nat.O)), ASM.Direct, (Vector.VCons ((Nat.S
1799                        Nat.O), ASM.Indirect, (Vector.VCons (Nat.O, ASM.Data,
1800                        Vector.VEmpty)))))))))) addr2 with
1801                | ASM.DIRECT b2 ->
1802                  (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S
1803                    (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True,
1804                    (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1805                    Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1806                    (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons
1807                    ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
1808                    (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
1809                    (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
1810                    (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons
1811                    (Nat.O, Bool.True, Vector.VEmpty)))))))))))))))),
1812                    (List.Cons (b1, (List.Cons (b2, List.Nil))))))
1813                | ASM.INDIRECT i1 ->
1814                  (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S
1815                    (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True,
1816                    (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1817                    Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1818                    (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons
1819                    ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
1820                    (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
1821                    (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
1822                    (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons
1823                    (Nat.O, i1, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1824                    List.Nil))))
1825                | ASM.EXT_INDIRECT x ->
1826                  (fun _ -> assert false (* absurd case *))
1827                | ASM.REGISTER r ->
1828                  (fun _ -> List.Cons
1829                    ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1830                       Nat.O))))) (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons
1831                       ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
1832                       (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1833                       Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1834                       Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.False,
1835                       (Vector.VCons (Nat.O, Bool.True,
1836                       Vector.VEmpty)))))))))) r), (List.Cons (b1,
1837                    List.Nil))))
1838                | ASM.ACC_A ->
1839                  (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S
1840                    (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True,
1841                    (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1842                    Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1843                    (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons
1844                    ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
1845                    (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
1846                    (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
1847                    (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons
1848                    (Nat.O, Bool.True, Vector.VEmpty)))))))))))))))),
1849                    (List.Cons (b1, List.Nil))))
1850                | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1851                | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1852                | ASM.DATA b2 ->
1853                  (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S
1854                    (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.False,
1855                    (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1856                    Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
1857                    (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons
1858                    ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
1859                    (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
1860                    (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True,
1861                    (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons
1862                    (Nat.O, Bool.True, Vector.VEmpty)))))))))))))))),
1863                    (List.Cons (b1, (List.Cons (b2, List.Nil))))))
1864                | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1865                | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1866                | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1867                | ASM.EXT_INDIRECT_DPTR ->
1868                  (fun _ -> assert false (* absurd case *))
1869                | ASM.INDIRECT_DPTR ->
1870                  (fun _ -> assert false (* absurd case *))
1871                | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1872                | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1873                | ASM.N_BIT_ADDR x ->
1874                  (fun _ -> assert false (* absurd case *))
1875                | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1876                | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1877                | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *)))
1878                 __)
1879          | Types.Inr addrs2 ->
1880            let { Types.fst = addr1; Types.snd = addr2 } = addrs2 in
1881            (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O,
1882                     ASM.Data16, Vector.VEmpty)) addr2 with
1883             | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1884             | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1885             | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1886             | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1887             | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1888             | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1889             | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1890             | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1891             | ASM.DATA16 w ->
1892               (fun _ ->
1893                 let b1_b2 =
1894                   Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1895                     (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
1896                     (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) w
1897                 in
1898                 let b1 = b1_b2.Types.fst in
1899                 let b2 = b1_b2.Types.snd in
1900                 List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1901                 (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
1902                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False,
1903                 (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1904                 Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1905                 Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1906                 Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
1907                 Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.False,
1908                 (Vector.VCons (Nat.O, Bool.False,
1909                 Vector.VEmpty)))))))))))))))), (List.Cons (b1, (List.Cons
1910                 (b2, List.Nil))))))
1911             | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1912             | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1913             | ASM.EXT_INDIRECT_DPTR ->
1914               (fun _ -> assert false (* absurd case *))
1915             | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1916             | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1917             | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1918             | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1919             | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1920             | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1921             | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
1922       | Types.Inr addrs1 ->
1923         let { Types.fst = addr1; Types.snd = addr2 } = addrs1 in
1924         (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O,
1925                  ASM.Bit_addr, Vector.VEmpty)) addr2 with
1926          | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1927          | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1928          | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1929          | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1930          | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1931          | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1932          | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1933          | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1934          | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1935          | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1936          | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1937          | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1938          | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1939          | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1940          | ASM.BIT_ADDR b1 ->
1941            (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1942              (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons
1943              ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))),
1944              Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1945              Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
1946              (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1947              (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
1948              Nat.O)), Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.True,
1949              (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty)))))))))))))))),
1950              (List.Cons (b1, List.Nil))))
1951          | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1952          | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1953          | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1954          | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
1955    | Types.Inr addrs0 ->
1956      let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in
1957      (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O,
1958               ASM.Bit_addr, Vector.VEmpty)) addr1 with
1959       | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1960       | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1961       | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
1962       | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
1963       | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
1964       | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
1965       | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
1966       | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
1967       | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
1968       | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
1969       | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
1970       | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1971       | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
1972       | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
1973       | ASM.BIT_ADDR b1 ->
1974         (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1975           (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
1976           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False,
1977           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
1978           Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
1979           Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
1980           Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
1981           (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
1982           Bool.False, Vector.VEmpty)))))))))))))))), (List.Cons (b1,
1983           List.Nil))))
1984       | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
1985       | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
1986       | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
1987       | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
1988 | ASM.MOVX addrs ->
1989   (match addrs with
1990    | Types.Inl addrs0 ->
1991      let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in
1992      (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
1993               Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O,
1994               ASM.Ext_indirect_dptr, Vector.VEmpty)))) addr2 with
1995       | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
1996       | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
1997       | ASM.EXT_INDIRECT i1 ->
1998         (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
1999           (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
2000           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
2001           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
2002           Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
2003           Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
2004           Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
2005           (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, i1,
2006           Vector.VEmpty)))))))))))))))), List.Nil))
2007       | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
2008       | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
2009       | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2010       | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2011       | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
2012       | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
2013       | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
2014       | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
2015       | ASM.EXT_INDIRECT_DPTR ->
2016         (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2017           (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
2018           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
2019           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
2020           Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
2021           Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
2022           Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
2023           (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
2024           Bool.False, Vector.VEmpty)))))))))))))))), List.Nil))
2025       | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2026       | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
2027       | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2028       | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2029       | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
2030       | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
2031       | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
2032    | Types.Inr addrs0 ->
2033      let { Types.fst = addr1; Types.snd = addr2 } = addrs0 in
2034      (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S
2035               Nat.O), ASM.Ext_indirect, (Vector.VCons (Nat.O,
2036               ASM.Ext_indirect_dptr, Vector.VEmpty)))) addr1 with
2037       | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
2038       | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
2039       | ASM.EXT_INDIRECT i1 ->
2040         (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2041           (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
2042           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
2043           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
2044           Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
2045           Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
2046           Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
2047           (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, i1,
2048           Vector.VEmpty)))))))))))))))), List.Nil))
2049       | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
2050       | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
2051       | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2052       | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2053       | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
2054       | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
2055       | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
2056       | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
2057       | ASM.EXT_INDIRECT_DPTR ->
2058         (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2059           (Nat.S (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S
2060           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True,
2061           (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))),
2062           Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))),
2063           Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
2064           Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
2065           (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
2066           Bool.False, Vector.VEmpty)))))))))))))))), List.Nil))
2067       | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2068       | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
2069       | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2070       | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2071       | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
2072       | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
2073       | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
2074 | ASM.SETB addr ->
2075   (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O),
2076            ASM.Carry, (Vector.VCons (Nat.O, ASM.Bit_addr, Vector.VEmpty))))
2077            addr with
2078    | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
2079    | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
2080    | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
2081    | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
2082    | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
2083    | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2084    | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2085    | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
2086    | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
2087    | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
2088    | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
2089    | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2090    | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2091    | ASM.CARRY ->
2092      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2093        (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
2094        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons
2095        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
2096        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
2097        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
2098        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
2099        ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True,
2100        Vector.VEmpty)))))))))))))))), List.Nil))
2101    | ASM.BIT_ADDR b1 ->
2102      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2103        (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
2104        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons
2105        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
2106        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
2107        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
2108        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
2109        ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.False,
2110        Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
2111    | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2112    | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
2113    | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
2114    | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
2115 | ASM.PUSH addr ->
2116   (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Direct,
2117            Vector.VEmpty)) addr with
2118    | ASM.DIRECT b1 ->
2119      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2120        (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
2121        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons
2122        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
2123        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
2124        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
2125        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
2126        ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
2127        Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
2128    | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
2129    | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
2130    | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
2131    | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
2132    | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2133    | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2134    | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
2135    | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
2136    | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
2137    | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
2138    | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2139    | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2140    | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
2141    | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2142    | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2143    | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
2144    | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
2145    | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
2146 | ASM.POP addr ->
2147   (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Direct,
2148            Vector.VEmpty)) addr with
2149    | ASM.DIRECT b1 ->
2150      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2151        (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
2152        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons
2153        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
2154        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
2155        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
2156        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
2157        ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
2158        Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
2159    | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
2160    | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
2161    | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
2162    | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
2163    | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2164    | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2165    | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
2166    | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
2167    | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
2168    | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
2169    | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2170    | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2171    | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
2172    | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2173    | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2174    | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
2175    | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
2176    | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
2177 | ASM.XCH (addr1, addr2) ->
2178   (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons ((Nat.S
2179            (Nat.S Nat.O)), ASM.Registr, (Vector.VCons ((Nat.S Nat.O),
2180            ASM.Direct, (Vector.VCons (Nat.O, ASM.Indirect,
2181            Vector.VEmpty)))))) addr2 with
2182    | ASM.DIRECT b1 ->
2183      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2184        (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
2185        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons
2186        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
2187        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
2188        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
2189        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
2190        Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.True,
2191        Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
2192    | ASM.INDIRECT i1 ->
2193      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2194        (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
2195        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons
2196        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
2197        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
2198        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
2199        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
2200        Nat.O), Bool.True, (Vector.VCons (Nat.O, i1,
2201        Vector.VEmpty)))))))))))))))), List.Nil))
2202    | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
2203    | ASM.REGISTER r ->
2204      (fun _ -> List.Cons
2205        ((Vector.append (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) (Nat.S
2206           (Nat.S (Nat.S Nat.O))) (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2207           Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))),
2208           Bool.True, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
2209           (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
2210           Bool.True, Vector.VEmpty)))))))))) r), List.Nil))
2211    | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
2212    | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2213    | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2214    | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
2215    | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
2216    | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
2217    | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
2218    | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2219    | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2220    | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
2221    | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2222    | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2223    | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
2224    | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
2225    | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
2226 | ASM.XCHD (addr1, addr2) ->
2227   (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Indirect,
2228            Vector.VEmpty)) addr2 with
2229    | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
2230    | ASM.INDIRECT i1 ->
2231      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2232        (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
2233        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons
2234        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
2235        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
2236        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
2237        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.True, (Vector.VCons ((Nat.S
2238        Nat.O), Bool.True, (Vector.VCons (Nat.O, i1,
2239        Vector.VEmpty)))))))))))))))), List.Nil))
2240    | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
2241    | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
2242    | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
2243    | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2244    | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2245    | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
2246    | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
2247    | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
2248    | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
2249    | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2250    | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2251    | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
2252    | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2253    | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2254    | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
2255    | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
2256    | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
2257 | ASM.RET ->
2258   List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2259     Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2260     (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
2261     (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
2262     (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2263     Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
2264     (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
2265     Bool.False, Vector.VEmpty)))))))))))))))), List.Nil)
2266 | ASM.RETI ->
2267   List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2268     Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2269     (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
2270     (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
2271     (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2272     Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
2273     (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O,
2274     Bool.False, Vector.VEmpty)))))))))))))))), List.Nil)
2275 | ASM.NOP ->
2276   List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2277     Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2278     (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
2279     (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S
2280     (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2281     Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
2282     (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O,
2283     Bool.False, Vector.VEmpty)))))))))))))))), List.Nil)
2284 | ASM.JMP adptr ->
2285   List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2286     Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S
2287     (Nat.S (Nat.S Nat.O)))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2288     (Nat.S (Nat.S Nat.O))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2289     (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2290     Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False,
2291     (Vector.VCons ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True,
2292     Vector.VEmpty)))))))))))))))), List.Nil)
2293
2294 (** val assembly1 : ASM.instruction -> Bool.bool Vector.vector List.list **)
2295 let assembly1 = function
2296 | ASM.ACALL addr ->
2297   (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Addr11,
2298            Vector.VEmpty)) addr with
2299    | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
2300    | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
2301    | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
2302    | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
2303    | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
2304    | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2305    | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2306    | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
2307    | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
2308    | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
2309    | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
2310    | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2311    | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2312    | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
2313    | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2314    | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2315    | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
2316    | ASM.ADDR11 w ->
2317      (fun _ ->
2318        let v1_v2 =
2319          Vector.vsplit (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
2320            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) w
2321        in
2322        let v1 = v1_v2.Types.fst in
2323        let v2 = v1_v2.Types.snd in
2324        List.Cons
2325        ((Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
2326           (Nat.S (Nat.S Nat.O))))) v1 (Vector.VCons ((Nat.S (Nat.S (Nat.S
2327           (Nat.S Nat.O)))), Bool.True, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2328           Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
2329           Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons
2330           (Nat.O, Bool.True, Vector.VEmpty))))))))))), (List.Cons (v2,
2331        List.Nil))))
2332    | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
2333 | ASM.LCALL addr ->
2334   (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Addr16,
2335            Vector.VEmpty)) addr with
2336    | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
2337    | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
2338    | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
2339    | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
2340    | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
2341    | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2342    | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2343    | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
2344    | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
2345    | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
2346    | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
2347    | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2348    | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2349    | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
2350    | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2351    | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2352    | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
2353    | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
2354    | ASM.ADDR16 w ->
2355      (fun _ ->
2356        let b1_b2 =
2357          Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2358            (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2359            (Nat.S (Nat.S Nat.O)))))))) w
2360        in
2361        let b1 = b1_b2.Types.fst in
2362        let b2 = b1_b2.Types.snd in
2363        List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2364        (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2365        (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S
2366        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons
2367        ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True, (Vector.VCons
2368        ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S
2369        (Nat.S Nat.O)), Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.True,
2370        (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty)))))))))))))))),
2371        (List.Cons (b1, (List.Cons (b2, List.Nil))))))) __
2372 | ASM.AJMP addr ->
2373   (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Addr11,
2374            Vector.VEmpty)) addr with
2375    | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
2376    | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
2377    | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
2378    | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
2379    | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
2380    | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2381    | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2382    | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
2383    | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
2384    | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
2385    | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
2386    | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2387    | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2388    | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
2389    | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2390    | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2391    | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
2392    | ASM.ADDR11 w ->
2393      (fun _ ->
2394        let v1_v2 =
2395          Vector.vsplit (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
2396            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) w
2397        in
2398        let v1 = v1_v2.Types.fst in
2399        let v2 = v1_v2.Types.snd in
2400        List.Cons
2401        ((Vector.append (Nat.S (Nat.S (Nat.S Nat.O))) (Nat.S (Nat.S (Nat.S
2402           (Nat.S (Nat.S Nat.O))))) v1 (Vector.VCons ((Nat.S (Nat.S (Nat.S
2403           (Nat.S Nat.O)))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2404           Nat.O))), Bool.False, (Vector.VCons ((Nat.S (Nat.S Nat.O)),
2405           Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.False, (Vector.VCons
2406           (Nat.O, Bool.True, Vector.VEmpty))))))))))), (List.Cons (v2,
2407        List.Nil))))
2408    | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
2409 | ASM.LJMP addr ->
2410   (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Addr16,
2411            Vector.VEmpty)) addr with
2412    | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
2413    | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
2414    | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
2415    | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
2416    | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
2417    | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2418    | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2419    | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
2420    | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
2421    | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
2422    | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
2423    | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2424    | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2425    | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
2426    | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2427    | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2428    | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
2429    | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
2430    | ASM.ADDR16 w ->
2431      (fun _ ->
2432        let b1_b2 =
2433          Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2434            (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2435            (Nat.S (Nat.S Nat.O)))))))) w
2436        in
2437        let b1 = b1_b2.Types.fst in
2438        let b2 = b1_b2.Types.snd in
2439        List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2440        (Nat.S Nat.O))))))), Bool.False, (Vector.VCons ((Nat.S (Nat.S (Nat.S
2441        (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons ((Nat.S
2442        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False, (Vector.VCons
2443        ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False, (Vector.VCons
2444        ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False, (Vector.VCons ((Nat.S
2445        (Nat.S Nat.O)), Bool.False, (Vector.VCons ((Nat.S Nat.O), Bool.True,
2446        (Vector.VCons (Nat.O, Bool.False, Vector.VEmpty)))))))))))))))),
2447        (List.Cons (b1, (List.Cons (b2, List.Nil))))))) __
2448 | ASM.SJMP addr ->
2449   (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Relative,
2450            Vector.VEmpty)) addr with
2451    | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
2452    | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
2453    | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
2454    | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
2455    | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
2456    | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2457    | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2458    | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
2459    | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
2460    | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
2461    | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
2462    | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2463    | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2464    | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
2465    | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2466    | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2467    | ASM.RELATIVE b1 ->
2468      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2469        (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
2470        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
2471        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
2472        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
2473        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
2474        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
2475        ((Nat.S Nat.O), Bool.False, (Vector.VCons (Nat.O, Bool.False,
2476        Vector.VEmpty)))))))))))))))), (List.Cons (b1, List.Nil))))
2477    | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
2478    | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
2479 | ASM.MOVC (addr1, addr2) ->
2480   (match ASM.subaddressing_modeel (Nat.S Nat.O) (Vector.VCons ((Nat.S Nat.O),
2481            ASM.Acc_dptr, (Vector.VCons (Nat.O, ASM.Acc_pc, Vector.VEmpty))))
2482            addr2 with
2483    | ASM.DIRECT x -> (fun _ -> assert false (* absurd case *))
2484    | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
2485    | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
2486    | ASM.REGISTER x -> (fun _ -> assert false (* absurd case *))
2487    | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
2488    | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2489    | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2490    | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
2491    | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
2492    | ASM.ACC_DPTR ->
2493      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2494        (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
2495        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
2496        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
2497        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.True,
2498        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
2499        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
2500        ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True,
2501        Vector.VEmpty)))))))))))))))), List.Nil))
2502    | ASM.ACC_PC ->
2503      (fun _ -> List.Cons ((Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2504        (Nat.S (Nat.S Nat.O))))))), Bool.True, (Vector.VCons ((Nat.S (Nat.S
2505        (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))), Bool.False, (Vector.VCons
2506        ((Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))), Bool.False,
2507        (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Bool.False,
2508        (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Bool.False,
2509        (Vector.VCons ((Nat.S (Nat.S Nat.O)), Bool.False, (Vector.VCons
2510        ((Nat.S Nat.O), Bool.True, (Vector.VCons (Nat.O, Bool.True,
2511        Vector.VEmpty)))))))))))))))), List.Nil))
2512    | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2513    | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2514    | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
2515    | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2516    | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2517    | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
2518    | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
2519    | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __
2520 | ASM.RealInstruction instr ->
2521   assembly_preinstruction (fun x ->
2522     (match ASM.subaddressing_modeel Nat.O (Vector.VCons (Nat.O, ASM.Relative,
2523              Vector.VEmpty)) x with
2524      | ASM.DIRECT x0 -> (fun _ -> assert false (* absurd case *))
2525      | ASM.INDIRECT x0 -> (fun _ -> assert false (* absurd case *))
2526      | ASM.EXT_INDIRECT x0 -> (fun _ -> assert false (* absurd case *))
2527      | ASM.REGISTER x0 -> (fun _ -> assert false (* absurd case *))
2528      | ASM.ACC_A -> (fun _ -> assert false (* absurd case *))
2529      | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2530      | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2531      | ASM.DATA x0 -> (fun _ -> assert false (* absurd case *))
2532      | ASM.DATA16 x0 -> (fun _ -> assert false (* absurd case *))
2533      | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
2534      | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
2535      | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2536      | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2537      | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
2538      | ASM.BIT_ADDR x0 -> (fun _ -> assert false (* absurd case *))
2539      | ASM.N_BIT_ADDR x0 -> (fun _ -> assert false (* absurd case *))
2540      | ASM.RELATIVE r -> (fun _ -> r)
2541      | ASM.ADDR11 x0 -> (fun _ -> assert false (* absurd case *))
2542      | ASM.ADDR16 x0 -> (fun _ -> assert false (* absurd case *))) __) instr
2543
2544 (** val expand_relative_jump_internal :
2545     (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word)
2546     -> (BitVector.word -> Bool.bool) -> ASM.identifier -> BitVector.word ->
2547     (ASM.subaddressing_mode -> ASM.subaddressing_mode ASM.preinstruction) ->
2548     ASM.instruction List.list **)
2549 let expand_relative_jump_internal lookup_labels sigma policy lbl ppc i =
2550   let lookup_address = sigma (lookup_labels lbl) in
2551   let pc_plus_jmp_length =
2552     sigma
2553       (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2554         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2555         Nat.O)))))))))))))))) ppc
2556         (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2557           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2558           (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
2559   in
2560   let { Types.fst = sj_possible; Types.snd = disp } =
2561     short_jump_cond pc_plus_jmp_length lookup_address
2562   in
2563   (match Bool.andb sj_possible (Bool.notb (policy ppc)) with
2564    | Bool.True ->
2565      let address = ASM.RELATIVE disp in
2566      List.Cons ((ASM.RealInstruction (i address)), List.Nil)
2567    | Bool.False ->
2568      List.Cons ((ASM.RealInstruction
2569        (i (ASM.RELATIVE
2570          (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2571            (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S Nat.O)))))),
2572        (List.Cons ((ASM.SJMP (ASM.RELATIVE
2573        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2574          (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S Nat.O)))))),
2575        (List.Cons ((ASM.LJMP (ASM.ADDR16 lookup_address)), List.Nil))))))
2576
2577 (** val expand_relative_jump :
2578     (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word)
2579     -> (BitVector.word -> Bool.bool) -> BitVector.word -> ASM.identifier
2580     ASM.preinstruction -> ASM.instruction List.list **)
2581 let expand_relative_jump lookup_labels sigma policy ppc = function
2582 | ASM.ADD (arg1, arg2) ->
2583   List.Cons ((ASM.RealInstruction (ASM.ADD (arg1, arg2))), List.Nil)
2584 | ASM.ADDC (arg1, arg2) ->
2585   List.Cons ((ASM.RealInstruction (ASM.ADDC (arg1, arg2))), List.Nil)
2586 | ASM.SUBB (arg1, arg2) ->
2587   List.Cons ((ASM.RealInstruction (ASM.SUBB (arg1, arg2))), List.Nil)
2588 | ASM.INC arg -> List.Cons ((ASM.RealInstruction (ASM.INC arg)), List.Nil)
2589 | ASM.DEC arg -> List.Cons ((ASM.RealInstruction (ASM.DEC arg)), List.Nil)
2590 | ASM.MUL (arg1, arg2) ->
2591   List.Cons ((ASM.RealInstruction (ASM.MUL (arg1, arg2))), List.Nil)
2592 | ASM.DIV (arg1, arg2) ->
2593   List.Cons ((ASM.RealInstruction (ASM.DIV (arg1, arg2))), List.Nil)
2594 | ASM.DA arg -> List.Cons ((ASM.RealInstruction (ASM.DA arg)), List.Nil)
2595 | ASM.JC jmp ->
2596   expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x ->
2597     ASM.JC x)
2598 | ASM.JNC jmp ->
2599   expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x ->
2600     ASM.JNC x)
2601 | ASM.JB (baddr, jmp) ->
2602   expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x ->
2603     ASM.JB (baddr, x))
2604 | ASM.JNB (baddr, jmp) ->
2605   expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x ->
2606     ASM.JNB (baddr, x))
2607 | ASM.JBC (baddr, jmp) ->
2608   expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x ->
2609     ASM.JBC (baddr, x))
2610 | ASM.JZ jmp ->
2611   expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x ->
2612     ASM.JZ x)
2613 | ASM.JNZ jmp ->
2614   expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x ->
2615     ASM.JNZ x)
2616 | ASM.CJNE (addr, jmp) ->
2617   expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x ->
2618     ASM.CJNE (addr, x))
2619 | ASM.DJNZ (addr, jmp) ->
2620   expand_relative_jump_internal lookup_labels sigma policy jmp ppc (fun x ->
2621     ASM.DJNZ (addr, x))
2622 | ASM.ANL arg -> List.Cons ((ASM.RealInstruction (ASM.ANL arg)), List.Nil)
2623 | ASM.ORL arg -> List.Cons ((ASM.RealInstruction (ASM.ORL arg)), List.Nil)
2624 | ASM.XRL arg -> List.Cons ((ASM.RealInstruction (ASM.XRL arg)), List.Nil)
2625 | ASM.CLR arg -> List.Cons ((ASM.RealInstruction (ASM.CLR arg)), List.Nil)
2626 | ASM.CPL arg -> List.Cons ((ASM.RealInstruction (ASM.CPL arg)), List.Nil)
2627 | ASM.RL arg -> List.Cons ((ASM.RealInstruction (ASM.RL arg)), List.Nil)
2628 | ASM.RLC arg -> List.Cons ((ASM.RealInstruction (ASM.RLC arg)), List.Nil)
2629 | ASM.RR arg -> List.Cons ((ASM.RealInstruction (ASM.RR arg)), List.Nil)
2630 | ASM.RRC arg -> List.Cons ((ASM.RealInstruction (ASM.RRC arg)), List.Nil)
2631 | ASM.SWAP arg -> List.Cons ((ASM.RealInstruction (ASM.SWAP arg)), List.Nil)
2632 | ASM.MOV arg -> List.Cons ((ASM.RealInstruction (ASM.MOV arg)), List.Nil)
2633 | ASM.MOVX arg -> List.Cons ((ASM.RealInstruction (ASM.MOVX arg)), List.Nil)
2634 | ASM.SETB arg -> List.Cons ((ASM.RealInstruction (ASM.SETB arg)), List.Nil)
2635 | ASM.PUSH arg -> List.Cons ((ASM.RealInstruction (ASM.PUSH arg)), List.Nil)
2636 | ASM.POP arg -> List.Cons ((ASM.RealInstruction (ASM.POP arg)), List.Nil)
2637 | ASM.XCH (arg1, arg2) ->
2638   List.Cons ((ASM.RealInstruction (ASM.XCH (arg1, arg2))), List.Nil)
2639 | ASM.XCHD (arg1, arg2) ->
2640   List.Cons ((ASM.RealInstruction (ASM.XCHD (arg1, arg2))), List.Nil)
2641 | ASM.RET -> List.Cons ((ASM.RealInstruction ASM.RET), List.Nil)
2642 | ASM.RETI -> List.Cons ((ASM.RealInstruction ASM.RETI), List.Nil)
2643 | ASM.NOP -> List.Cons ((ASM.RealInstruction ASM.NOP), List.Nil)
2644 | ASM.JMP arg -> List.Cons ((ASM.RealInstruction (ASM.JMP arg)), List.Nil)
2645
2646 (** val is_code : AST.region -> Bool.bool **)
2647 let is_code = function
2648 | AST.XData -> Bool.False
2649 | AST.Code -> Bool.True
2650
2651 (** val expand_pseudo_instruction :
2652     (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word)
2653     -> (BitVector.word -> Bool.bool) -> BitVector.word -> (ASM.identifier ->
2654     (AST.region, BitVector.word) Types.prod) -> ASM.pseudo_instruction ->
2655     ASM.instruction List.list **)
2656 let expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels = function
2657 | ASM.Instruction instr ->
2658   expand_relative_jump lookup_labels sigma policy ppc instr
2659 | ASM.Comment comment -> List.Nil
2660 | ASM.Cost cost -> List.Cons ((ASM.RealInstruction ASM.NOP), List.Nil)
2661 | ASM.Jmp jmp ->
2662   let pc_plus_jmp_length =
2663     sigma
2664       (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2665         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2666         Nat.O)))))))))))))))) ppc
2667         (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2668           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2669           (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
2670   in
2671   let do_a_long = policy ppc in
2672   let lookup_address = sigma (lookup_labels jmp) in
2673   let { Types.fst = sj_possible; Types.snd = disp } =
2674     short_jump_cond pc_plus_jmp_length lookup_address
2675   in
2676   (match Bool.andb sj_possible (Bool.notb do_a_long) with
2677    | Bool.True ->
2678      let address = ASM.RELATIVE disp in
2679      List.Cons ((ASM.SJMP address), List.Nil)
2680    | Bool.False ->
2681      let { Types.fst = mj_possible; Types.snd = disp2 } =
2682        absolute_jump_cond pc_plus_jmp_length lookup_address
2683      in
2684      (match Bool.andb mj_possible (Bool.notb do_a_long) with
2685       | Bool.True ->
2686         let address = ASM.ADDR11 disp2 in
2687         List.Cons ((ASM.AJMP address), List.Nil)
2688       | Bool.False ->
2689         let address = ASM.ADDR16 lookup_address in
2690         List.Cons ((ASM.LJMP address), List.Nil)))
2691 | ASM.Jnz (acc, tgt1, tgt2) ->
2692   let lookup_address1 = sigma (lookup_labels tgt1) in
2693   let lookup_address2 = sigma (lookup_labels tgt2) in
2694   List.Cons ((ASM.RealInstruction (ASM.JNZ (ASM.RELATIVE
2695   (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2696     (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S Nat.O))))))), (List.Cons
2697   ((ASM.LJMP (ASM.ADDR16 lookup_address2)), (List.Cons ((ASM.LJMP (ASM.ADDR16
2698   lookup_address1)), List.Nil)))))
2699 | ASM.Call call ->
2700   let pc_plus_jmp_length =
2701     sigma
2702       (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2703         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2704         Nat.O)))))))))))))))) ppc
2705         (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2706           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2707           (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
2708   in
2709   let lookup_address = sigma (lookup_labels call) in
2710   let { Types.fst = mj_possible; Types.snd = disp } =
2711     absolute_jump_cond pc_plus_jmp_length lookup_address
2712   in
2713   let do_a_long = policy ppc in
2714   (match Bool.andb mj_possible (Bool.notb do_a_long) with
2715    | Bool.True ->
2716      let address = ASM.ADDR11 disp in
2717      List.Cons ((ASM.ACALL address), List.Nil)
2718    | Bool.False ->
2719      let address = ASM.ADDR16 lookup_address in
2720      List.Cons ((ASM.LCALL address), List.Nil))
2721 | ASM.Mov (d, trgt, off) ->
2722   let { Types.fst = r; Types.snd = addr } = lookup_datalabels trgt in
2723   let addr0 = (Arithmetic.add_16_with_carry addr off Bool.False).Types.fst in
2724   let addr1 =
2725     match is_code r with
2726     | Bool.True -> sigma addr0
2727     | Bool.False -> addr0
2728   in
2729   (match d with
2730    | Types.Inl x ->
2731      let address = ASM.DATA16 addr1 in
2732      List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl
2733      (Types.Inr { Types.fst = ASM.DPTR; Types.snd = address }))))), List.Nil)
2734    | Types.Inr pr ->
2735      let v = ASM.DATA
2736        (match pr.Types.snd with
2737         | ASM.HIGH ->
2738           (Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2739             (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2740             (Nat.S (Nat.S Nat.O)))))))) addr1).Types.fst
2741         | ASM.LOW ->
2742           (Vector.vsplit (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2743             (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2744             (Nat.S (Nat.S Nat.O)))))))) addr1).Types.snd)
2745      in
2746      (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons
2747               ((Nat.S (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons ((Nat.S
2748               Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Registr,
2749               Vector.VEmpty)))))) pr.Types.fst with
2750       | ASM.DIRECT b1 ->
2751         (fun _ -> List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl
2752           (Types.Inl (Types.Inl (Types.Inr { Types.fst = (ASM.DIRECT b1);
2753           Types.snd = v })))))), List.Nil))
2754       | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
2755       | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
2756       | ASM.REGISTER r0 ->
2757         (fun _ -> List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl
2758           (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst =
2759           (ASM.REGISTER r0); Types.snd = v }))))))), List.Nil))
2760       | ASM.ACC_A ->
2761         (fun _ -> List.Cons ((ASM.RealInstruction (ASM.MOV (Types.Inl
2762           (Types.Inl (Types.Inl (Types.Inl (Types.Inl { Types.fst =
2763           ASM.ACC_A; Types.snd = v }))))))), List.Nil))
2764       | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
2765       | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
2766       | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
2767       | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
2768       | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
2769       | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
2770       | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2771       | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
2772       | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
2773       | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2774       | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
2775       | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
2776       | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
2777       | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
2778
2779 (** val assembly_1_pseudoinstruction :
2780     (ASM.identifier -> BitVector.word) -> (BitVector.word -> BitVector.word)
2781     -> (BitVector.word -> Bool.bool) -> BitVector.word -> (ASM.identifier ->
2782     (AST.region, BitVector.word) Types.prod) -> ASM.pseudo_instruction ->
2783     (Nat.nat, Bool.bool Vector.vector List.list) Types.prod **)
2784 let assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels i =
2785   let pseudos =
2786     expand_pseudo_instruction lookup_labels sigma policy ppc
2787       lookup_datalabels i
2788   in
2789   let mapped = List.map assembly1 pseudos in
2790   let flattened = List.flatten mapped in
2791   let pc_len = List.length flattened in
2792   { Types.fst = pc_len; Types.snd = flattened }
2793
2794 (** val instruction_size :
2795     (ASM.identifier -> BitVector.word) -> (ASM.identifier -> (AST.region,
2796     BitVector.word) Types.prod) -> (BitVector.word -> BitVector.word) ->
2797     (BitVector.word -> Bool.bool) -> BitVector.word -> ASM.pseudo_instruction
2798     -> Nat.nat **)
2799 let instruction_size lookup_labels lookup_datalabels sigma policy ppc i =
2800   (assembly_1_pseudoinstruction lookup_labels sigma policy ppc
2801     lookup_datalabels i).Types.fst
2802
2803 (** val assembly :
2804     ASM.pseudo_assembly_program -> (BitVector.word -> BitVector.word) ->
2805     (BitVector.word -> Bool.bool) -> ASM.labelled_object_code Types.sig0 **)
2806 let assembly p sigma policy =
2807   (let { Types.fst = labels_to_ppc; Types.snd = ppc_to_costs } =
2808      Fetch.create_label_cost_map p.ASM.code
2809    in
2810   (fun _ ->
2811   let preamble = p.ASM.preamble in
2812   let instr_list = p.ASM.code in
2813   let datalabels = Status.construct_datalabels preamble in
2814   let lookup_labels = fun x ->
2815     Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2816       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2817       Nat.O))))))))))))))))
2818       (Identifiers.lookup_def PreIdentifiers.ASMTag labels_to_ppc x Nat.O)
2819   in
2820   let lookup_datalabels = fun x ->
2821     match Identifiers.lookup PreIdentifiers.ASMTag
2822             (Status.construct_datalabels preamble) x with
2823     | Types.None -> { Types.fst = AST.Code; Types.snd = (lookup_labels x) }
2824     | Types.Some addr -> { Types.fst = AST.XData; Types.snd = addr }
2825   in
2826   (let { Types.fst = next_pc; Types.snd = revcode } =
2827      Types.pi1
2828        (FoldStuff.foldl_strong instr_list (fun prefix hd tl _ ppc_code ->
2829          (let { Types.fst = ppc; Types.snd = code } = Types.pi1 ppc_code in
2830          (fun _ ->
2831          (let { Types.fst = pc_delta; Types.snd = program } =
2832             assembly_1_pseudoinstruction lookup_labels sigma policy ppc
2833               lookup_datalabels hd.Types.snd
2834           in
2835          (fun _ ->
2836          let new_ppc =
2837            Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2838              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2839              Nat.O)))))))))))))))) ppc
2840              (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2841                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2842                (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O))
2843          in
2844          { Types.fst = new_ppc; Types.snd =
2845          (List.append (List.reverse program) code) })) __)) __) { Types.fst =
2846          (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2847            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2848            Nat.O))))))))))))))))); Types.snd = List.Nil })
2849    in
2850   (fun _ ->
2851   let code = List.reverse revcode in
2852   { ASM.oc = code; ASM.cm = (ASM.load_code_memory code); ASM.costlabels =
2853   (BitVectorTrie.fold (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2854     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2855     Nat.O)))))))))))))))) (fun ppc cost pc_to_costs ->
2856     BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2857       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2858       Nat.O)))))))))))))))) (sigma ppc) cost pc_to_costs) ppc_to_costs
2859     (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2860     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2861     Nat.O)))))))))))))))))); ASM.symboltable =
2862   (Util.foldl (fun symboltable newident_oldident ->
2863     let ppc = lookup_labels newident_oldident.Types.fst in
2864     BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2865       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2866       Nat.O)))))))))))))))) (sigma ppc) newident_oldident.Types.snd
2867       symboltable) (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2868     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2869     (Nat.S Nat.O))))))))))))))))) p.ASM.renamed_symbols); ASM.final_pc =
2870   (sigma (lookup_labels p.ASM.final_label)) })) __)) __
2871
2872 (** val ticks_of_instruction : ASM.instruction -> Nat.nat **)
2873 let ticks_of_instruction i =
2874   let trivial_code_memory = assembly1 i in
2875   let trivial_status = ASM.load_code_memory trivial_code_memory in
2876   (Fetch.fetch trivial_status
2877     (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2878       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2879       Nat.O)))))))))))))))))).Types.snd
2880
2881 (** val ticks_of0 :
2882     ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
2883     (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) ->
2884     BitVector.word -> ASM.pseudo_instruction -> (Nat.nat, Nat.nat) Types.prod **)
2885 let ticks_of0 program lookup_labels sigma policy ppc = function
2886 | ASM.Instruction instr ->
2887   (match instr with
2888    | ASM.ADD (arg1, arg2) ->
2889      let ticks =
2890        ticks_of_instruction (ASM.RealInstruction (ASM.ADD (arg1, arg2)))
2891      in
2892      { Types.fst = ticks; Types.snd = ticks }
2893    | ASM.ADDC (arg1, arg2) ->
2894      let ticks =
2895        ticks_of_instruction (ASM.RealInstruction (ASM.ADDC (arg1, arg2)))
2896      in
2897      { Types.fst = ticks; Types.snd = ticks }
2898    | ASM.SUBB (arg1, arg2) ->
2899      let ticks =
2900        ticks_of_instruction (ASM.RealInstruction (ASM.SUBB (arg1, arg2)))
2901      in
2902      { Types.fst = ticks; Types.snd = ticks }
2903    | ASM.INC arg ->
2904      let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.INC arg)) in
2905      { Types.fst = ticks; Types.snd = ticks }
2906    | ASM.DEC arg ->
2907      let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.DEC arg)) in
2908      { Types.fst = ticks; Types.snd = ticks }
2909    | ASM.MUL (arg1, arg2) ->
2910      let ticks =
2911        ticks_of_instruction (ASM.RealInstruction (ASM.MUL (arg1, arg2)))
2912      in
2913      { Types.fst = ticks; Types.snd = ticks }
2914    | ASM.DIV (arg1, arg2) ->
2915      let ticks =
2916        ticks_of_instruction (ASM.RealInstruction (ASM.DIV (arg1, arg2)))
2917      in
2918      { Types.fst = ticks; Types.snd = ticks }
2919    | ASM.DA arg ->
2920      let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.DA arg)) in
2921      { Types.fst = ticks; Types.snd = ticks }
2922    | ASM.JC lbl ->
2923      let lookup_address = sigma (lookup_labels lbl) in
2924      let pc_plus_jmp_length =
2925        sigma
2926          (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2927            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2928            Nat.O)))))))))))))))) ppc
2929            (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2930              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2931              (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
2932      in
2933      let { Types.fst = sj_possible; Types.snd = disp } =
2934        short_jump_cond pc_plus_jmp_length lookup_address
2935      in
2936      (match sj_possible with
2937       | Bool.True ->
2938         { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
2939           Nat.O)) }
2940       | Bool.False ->
2941         { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd =
2942           (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) })
2943    | ASM.JNC lbl ->
2944      let lookup_address = sigma (lookup_labels lbl) in
2945      let pc_plus_jmp_length =
2946        sigma
2947          (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2948            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2949            Nat.O)))))))))))))))) ppc
2950            (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2951              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2952              (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
2953      in
2954      let { Types.fst = sj_possible; Types.snd = disp } =
2955        short_jump_cond pc_plus_jmp_length lookup_address
2956      in
2957      (match sj_possible with
2958       | Bool.True ->
2959         { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
2960           Nat.O)) }
2961       | Bool.False ->
2962         { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd =
2963           (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) })
2964    | ASM.JB (bit, lbl) ->
2965      let lookup_address = sigma (lookup_labels lbl) in
2966      let pc_plus_jmp_length =
2967        sigma
2968          (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2969            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2970            Nat.O)))))))))))))))) ppc
2971            (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2972              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2973              (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
2974      in
2975      let { Types.fst = sj_possible; Types.snd = disp } =
2976        short_jump_cond pc_plus_jmp_length lookup_address
2977      in
2978      (match sj_possible with
2979       | Bool.True ->
2980         { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
2981           Nat.O)) }
2982       | Bool.False ->
2983         { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd =
2984           (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) })
2985    | ASM.JNB (bit, lbl) ->
2986      let lookup_address = sigma (lookup_labels lbl) in
2987      let pc_plus_jmp_length =
2988        sigma
2989          (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2990            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2991            Nat.O)))))))))))))))) ppc
2992            (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2993              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
2994              (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
2995      in
2996      let { Types.fst = sj_possible; Types.snd = disp } =
2997        short_jump_cond pc_plus_jmp_length lookup_address
2998      in
2999      (match sj_possible with
3000       | Bool.True ->
3001         { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
3002           Nat.O)) }
3003       | Bool.False ->
3004         { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd =
3005           (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) })
3006    | ASM.JBC (bit, lbl) ->
3007      let lookup_address = sigma (lookup_labels lbl) in
3008      let pc_plus_jmp_length =
3009        sigma
3010          (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3011            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3012            Nat.O)))))))))))))))) ppc
3013            (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3014              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3015              (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
3016      in
3017      let { Types.fst = sj_possible; Types.snd = disp } =
3018        short_jump_cond pc_plus_jmp_length lookup_address
3019      in
3020      (match sj_possible with
3021       | Bool.True ->
3022         { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
3023           Nat.O)) }
3024       | Bool.False ->
3025         { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd =
3026           (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) })
3027    | ASM.JZ lbl ->
3028      let lookup_address = sigma (lookup_labels lbl) in
3029      let pc_plus_jmp_length =
3030        sigma
3031          (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3032            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3033            Nat.O)))))))))))))))) ppc
3034            (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3035              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3036              (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
3037      in
3038      let { Types.fst = sj_possible; Types.snd = disp } =
3039        short_jump_cond pc_plus_jmp_length lookup_address
3040      in
3041      (match sj_possible with
3042       | Bool.True ->
3043         { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
3044           Nat.O)) }
3045       | Bool.False ->
3046         { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd =
3047           (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) })
3048    | ASM.JNZ lbl ->
3049      let lookup_address = sigma (lookup_labels lbl) in
3050      let pc_plus_jmp_length =
3051        sigma
3052          (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3053            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3054            Nat.O)))))))))))))))) ppc
3055            (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3056              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3057              (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
3058      in
3059      let { Types.fst = sj_possible; Types.snd = disp } =
3060        short_jump_cond pc_plus_jmp_length lookup_address
3061      in
3062      (match sj_possible with
3063       | Bool.True ->
3064         { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
3065           Nat.O)) }
3066       | Bool.False ->
3067         { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd =
3068           (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) })
3069    | ASM.CJNE (arg, lbl) ->
3070      let lookup_address = sigma (lookup_labels lbl) in
3071      let pc_plus_jmp_length =
3072        sigma
3073          (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3074            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3075            Nat.O)))))))))))))))) ppc
3076            (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3077              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3078              (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
3079      in
3080      let { Types.fst = sj_possible; Types.snd = disp } =
3081        short_jump_cond pc_plus_jmp_length lookup_address
3082      in
3083      (match sj_possible with
3084       | Bool.True ->
3085         { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
3086           Nat.O)) }
3087       | Bool.False ->
3088         { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd =
3089           (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) })
3090    | ASM.DJNZ (arg, lbl) ->
3091      let lookup_address = sigma (lookup_labels lbl) in
3092      let pc_plus_jmp_length =
3093        sigma
3094          (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3095            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3096            Nat.O)))))))))))))))) ppc
3097            (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3098              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3099              (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
3100      in
3101      let { Types.fst = sj_possible; Types.snd = disp } =
3102        short_jump_cond pc_plus_jmp_length lookup_address
3103      in
3104      (match sj_possible with
3105       | Bool.True ->
3106         { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
3107           Nat.O)) }
3108       | Bool.False ->
3109         { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd =
3110           (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) })
3111    | ASM.ANL arg ->
3112      let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.ANL arg)) in
3113      { Types.fst = ticks; Types.snd = ticks }
3114    | ASM.ORL arg ->
3115      let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.ORL arg)) in
3116      { Types.fst = ticks; Types.snd = ticks }
3117    | ASM.XRL arg ->
3118      let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.XRL arg)) in
3119      { Types.fst = ticks; Types.snd = ticks }
3120    | ASM.CLR arg ->
3121      let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.CLR arg)) in
3122      { Types.fst = ticks; Types.snd = ticks }
3123    | ASM.CPL arg ->
3124      let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.CPL arg)) in
3125      { Types.fst = ticks; Types.snd = ticks }
3126    | ASM.RL arg ->
3127      let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.RL arg)) in
3128      { Types.fst = ticks; Types.snd = ticks }
3129    | ASM.RLC arg ->
3130      let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.RLC arg)) in
3131      { Types.fst = ticks; Types.snd = ticks }
3132    | ASM.RR arg ->
3133      let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.RR arg)) in
3134      { Types.fst = ticks; Types.snd = ticks }
3135    | ASM.RRC arg ->
3136      let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.RRC arg)) in
3137      { Types.fst = ticks; Types.snd = ticks }
3138    | ASM.SWAP arg ->
3139      let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.SWAP arg)) in
3140      { Types.fst = ticks; Types.snd = ticks }
3141    | ASM.MOV arg ->
3142      let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.MOV arg)) in
3143      { Types.fst = ticks; Types.snd = ticks }
3144    | ASM.MOVX arg ->
3145      let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.MOVX arg)) in
3146      { Types.fst = ticks; Types.snd = ticks }
3147    | ASM.SETB arg ->
3148      let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.SETB arg)) in
3149      { Types.fst = ticks; Types.snd = ticks }
3150    | ASM.PUSH arg ->
3151      let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.PUSH arg)) in
3152      { Types.fst = ticks; Types.snd = ticks }
3153    | ASM.POP arg ->
3154      let ticks = ticks_of_instruction (ASM.RealInstruction (ASM.POP arg)) in
3155      { Types.fst = ticks; Types.snd = ticks }
3156    | ASM.XCH (arg1, arg2) ->
3157      let ticks =
3158        ticks_of_instruction (ASM.RealInstruction (ASM.XCH (arg1, arg2)))
3159      in
3160      { Types.fst = ticks; Types.snd = ticks }
3161    | ASM.XCHD (arg1, arg2) ->
3162      let ticks =
3163        ticks_of_instruction (ASM.RealInstruction (ASM.XCHD (arg1, arg2)))
3164      in
3165      { Types.fst = ticks; Types.snd = ticks }
3166    | ASM.RET ->
3167      let ticks = ticks_of_instruction (ASM.RealInstruction ASM.RET) in
3168      { Types.fst = ticks; Types.snd = ticks }
3169    | ASM.RETI ->
3170      let ticks = ticks_of_instruction (ASM.RealInstruction ASM.RETI) in
3171      { Types.fst = ticks; Types.snd = ticks }
3172    | ASM.NOP ->
3173      let ticks = ticks_of_instruction (ASM.RealInstruction ASM.NOP) in
3174      { Types.fst = ticks; Types.snd = ticks }
3175    | ASM.JMP x ->
3176      { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S Nat.O)) })
3177 | ASM.Comment comment -> { Types.fst = Nat.O; Types.snd = Nat.O }
3178 | ASM.Cost cost ->
3179   let ticks = ticks_of_instruction (ASM.RealInstruction ASM.NOP) in
3180   { Types.fst = ticks; Types.snd = ticks }
3181 | ASM.Jmp jmp ->
3182   let pc_plus_jmp_length =
3183     sigma
3184       (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3185         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3186         Nat.O)))))))))))))))) ppc
3187         (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3188           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3189           (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
3190   in
3191   let do_a_long = policy ppc in
3192   let lookup_address = sigma (lookup_labels jmp) in
3193   let { Types.fst = sj_possible; Types.snd = disp } =
3194     short_jump_cond pc_plus_jmp_length lookup_address
3195   in
3196   (match Bool.andb sj_possible (Bool.notb do_a_long) with
3197    | Bool.True ->
3198      { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S Nat.O)) }
3199    | Bool.False ->
3200      let { Types.fst = mj_possible; Types.snd = disp2 } =
3201        absolute_jump_cond pc_plus_jmp_length lookup_address
3202      in
3203      (match Bool.andb mj_possible (Bool.notb do_a_long) with
3204       | Bool.True ->
3205         { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
3206           Nat.O)) }
3207       | Bool.False ->
3208         { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S
3209           Nat.O)) }))
3210 | ASM.Jnz (x, x0, x1) ->
3211   { Types.fst = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))); Types.snd = (Nat.S
3212     (Nat.S (Nat.S (Nat.S Nat.O)))) }
3213 | ASM.Call call ->
3214   let pc_plus_jmp_length =
3215     sigma
3216       (Arithmetic.add (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3217         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3218         Nat.O)))))))))))))))) ppc
3219         (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3220           (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
3221           (Nat.S (Nat.S Nat.O)))))))))))))))) (Nat.S Nat.O)))
3222   in
3223   let lookup_address = sigma (lookup_labels call) in
3224   let { Types.fst = mj_possible; Types.snd = disp } =
3225     absolute_jump_cond pc_plus_jmp_length lookup_address
3226   in
3227   let do_a_long = policy ppc in
3228   (match Bool.andb mj_possible (Bool.notb do_a_long) with
3229    | Bool.True ->
3230      { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S Nat.O)) }
3231    | Bool.False ->
3232      { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S Nat.O)) })
3233 | ASM.Mov (dst, lbl, off) ->
3234   (match dst with
3235    | Types.Inl x ->
3236      { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S (Nat.S Nat.O)) }
3237    | Types.Inr pr ->
3238      (match ASM.subaddressing_modeel (Nat.S (Nat.S Nat.O)) (Vector.VCons
3239               ((Nat.S (Nat.S Nat.O)), ASM.Acc_a, (Vector.VCons ((Nat.S
3240               Nat.O), ASM.Direct, (Vector.VCons (Nat.O, ASM.Registr,
3241               Vector.VEmpty)))))) pr.Types.fst with
3242       | ASM.DIRECT d ->
3243         (fun _ -> { Types.fst = (Nat.S (Nat.S Nat.O)); Types.snd = (Nat.S
3244           (Nat.S Nat.O)) })
3245       | ASM.INDIRECT x -> (fun _ -> assert false (* absurd case *))
3246       | ASM.EXT_INDIRECT x -> (fun _ -> assert false (* absurd case *))
3247       | ASM.REGISTER r ->
3248         (fun _ -> { Types.fst = (Nat.S Nat.O); Types.snd = (Nat.S Nat.O) })
3249       | ASM.ACC_A ->
3250         (fun _ -> { Types.fst = (Nat.S Nat.O); Types.snd = (Nat.S Nat.O) })
3251       | ASM.ACC_B -> (fun _ -> assert false (* absurd case *))
3252       | ASM.DPTR -> (fun _ -> assert false (* absurd case *))
3253       | ASM.DATA x -> (fun _ -> assert false (* absurd case *))
3254       | ASM.DATA16 x -> (fun _ -> assert false (* absurd case *))
3255       | ASM.ACC_DPTR -> (fun _ -> assert false (* absurd case *))
3256       | ASM.ACC_PC -> (fun _ -> assert false (* absurd case *))
3257       | ASM.EXT_INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
3258       | ASM.INDIRECT_DPTR -> (fun _ -> assert false (* absurd case *))
3259       | ASM.CARRY -> (fun _ -> assert false (* absurd case *))
3260       | ASM.BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
3261       | ASM.N_BIT_ADDR x -> (fun _ -> assert false (* absurd case *))
3262       | ASM.RELATIVE x -> (fun _ -> assert false (* absurd case *))
3263       | ASM.ADDR11 x -> (fun _ -> assert false (* absurd case *))
3264       | ASM.ADDR16 x -> (fun _ -> assert false (* absurd case *))) __)
3265
3266 (** val ticks_of :
3267     ASM.pseudo_assembly_program -> (ASM.identifier -> BitVector.word) ->
3268     (BitVector.word -> BitVector.word) -> (BitVector.word -> Bool.bool) ->
3269     BitVector.word -> (Nat.nat, Nat.nat) Types.prod **)
3270 let ticks_of program addr_of sigma policy ppc =
3271   let { Types.fst = fetched; Types.snd = new_ppc } =
3272     ASM.fetch_pseudo_instruction program.ASM.code ppc
3273   in
3274   ticks_of0 program addr_of sigma policy ppc fetched
3275