extracted/fetch.ml

   1 open Preamble
   2
   3 open Exp
   4
   5 open Setoids
   6
   7 open Monad
   8
   9 open Option
  10
  11 open Extranat
  12
  13 open Vector
  14
  15 open Div_and_mod
  16
  17 open Jmeq
  18
  19 open Russell
  20
  21 open Types
  22
  23 open List
  24
  25 open Util
  26
  27 open FoldStuff
  28
  29 open Bool
  30
  31 open Hints_declaration
  32
  33 open Core_notation
  34
  35 open Pts
  36
  37 open Logic
  38
  39 open Relations
  40
  41 open Nat
  42
  43 open BitVector
  44
  45 open Arithmetic
  46
  47 open BitVectorTrie
  48
  49 open String
  50
  51 open Integers
  52
  53 open AST
  54
  55 open LabelledObjects
  56
  57 open Proper
  58
  59 open PositiveMap
  60
  61 open Deqsets
  62
  63 open ErrorMessages
  64
  65 open PreIdentifiers
  66
  67 open Errors
  68
  69 open Extralib
  70
  71 open Lists
  72
  73 open Positive
  74
  75 open Identifiers
  76
  77 open CostLabel
  78
  79 open ASM
  80
  81 (** val inefficient_address_of_word_labels_code_mem :
  82     ASM.labelled_instruction List.list -> ASM.identifier ->
  83     BitVector.bitVector **)
  84 let inefficient_address_of_word_labels_code_mem code_mem id =
  85   Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
  86     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
  87     Nat.O))))))))))))))))
  88     (LabelledObjects.index_of
  89       (LabelledObjects.instruction_matches_identifier PreIdentifiers.ASMTag
  90         id) code_mem)
  91
  92 type label_map = Nat.nat Identifiers.identifier_map
  93
  94 (** val create_label_cost_map0 :
  95     ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
  96     BitVectorTrie.bitVectorTrie) Types.prod Types.sig0 **)
  97 let create_label_cost_map0 program =
  98   (Types.pi1
  99     (FoldStuff.foldl_strong program (fun prefix x tl _ labels_costs_ppc ->
 100       (let { Types.fst = eta28695; Types.snd = ppc } =
 101          Types.pi1 labels_costs_ppc
 102        in
 103       (fun _ ->
 104       (let { Types.fst = labels; Types.snd = costs } = eta28695 in
 105       (fun _ ->
 106       (let { Types.fst = label; Types.snd = instr } = x in
 107       (fun _ ->
 108       let labels1 =
 109         match label with
 110         | Types.None -> labels
 111         | Types.Some l -> Identifiers.add PreIdentifiers.ASMTag labels l ppc
 112       in
 113       let costs1 =
 114         match instr with
 115         | ASM.Instruction x0 -> costs
 116         | ASM.Comment x0 -> costs
 117         | ASM.Cost cost ->
 118           BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 119             (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 120             (Nat.S Nat.O))))))))))))))))
 121             (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 122               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 123               (Nat.S (Nat.S Nat.O)))))))))))))))) ppc) cost costs
 124         | ASM.Jmp x0 -> costs
 125         | ASM.Jnz (x0, x1, x2) -> costs
 126         | ASM.Call x0 -> costs
 127         | ASM.Mov (x0, x1, x2) -> costs
 128       in
 129       { Types.fst = { Types.fst = labels1; Types.snd = costs1 }; Types.snd =
 130       (Nat.S ppc) })) __)) __)) __) { Types.fst = { Types.fst =
 131       (Identifiers.empty_map PreIdentifiers.ASMTag); Types.snd =
 132       (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 133       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 134       Nat.O))))))))))))))))) }; Types.snd = Nat.O })).Types.fst
 135
 136 (** val create_label_cost_map :
 137     ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
 138     BitVectorTrie.bitVectorTrie) Types.prod **)
 139 let create_label_cost_map program =
 140   Types.pi1 (create_label_cost_map0 program)
 141
 142 (** val address_of_word_labels :
 143     ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.word **)
 144 let address_of_word_labels code_mem id =
 145   let labels = (create_label_cost_map code_mem).Types.fst in
 146   Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 147     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 148     Nat.O))))))))))))))))
 149     (Identifiers.lookup_def PreIdentifiers.ASMTag labels id Nat.O)
 150
 151 (** val bitvector_max_nat : Nat.nat -> Nat.nat **)
 152 let bitvector_max_nat length =
 153   Exp.exp (Nat.S (Nat.S Nat.O)) length
 154
 155 (** val code_memory_size : Nat.nat **)
 156 let code_memory_size =
 157   bitvector_max_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 158     (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 159     Nat.O))))))))))))))))
 160
 161 (** val prod_inv_rect_Type0 :
 162     ('a1, 'a2) Types.prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
 163 let prod_inv_rect_Type0 clearme =
 164   let { Types.fst = fst; Types.snd = snd } = clearme in
 165   (fun auto -> auto fst snd __)
 166
 167 (** val fetch0 :
 168     BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
 169     BitVector.byte -> ((ASM.instruction, BitVector.word) Types.prod, Nat.nat)
 170     Types.prod **)
 171 let fetch0 pmem pc v =
 172   let { Types.fst = b; Types.snd = v0 } =
 173     Vector.head (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))
 174       v
 175   in
 176   (match b with
 177    | Bool.True ->
 178      let { Types.fst = b0; Types.snd = v1 } =
 179        Vector.head (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) v0
 180      in
 181      (match b0 with
 182       | Bool.True ->
 183         let { Types.fst = b1; Types.snd = v2 } =
 184           Vector.head (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) v1
 185         in
 186         (match b1 with
 187          | Bool.True ->
 188            let { Types.fst = b2; Types.snd = v3 } =
 189              Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2
 190            in
 191            (match b2 with
 192             | Bool.True ->
 193               let { Types.fst = b3; Types.snd = v4 } =
 194                 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
 195               in
 196               (match b3 with
 197                | Bool.True ->
 198                  { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV
 199                    (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr
 200                    { Types.fst = (ASM.REGISTER v4); Types.snd =
 201                    ASM.ACC_A }))))))); Types.snd = pc }; Types.snd = (Nat.S
 202                    Nat.O) }
 203                | Bool.False ->
 204                  let { Types.fst = b4; Types.snd = v5 } =
 205                    Vector.head (Nat.S (Nat.S Nat.O)) v4
 206                  in
 207                  (match b4 with
 208                   | Bool.True ->
 209                     let { Types.fst = b5; Types.snd = v6 } =
 210                       Vector.head (Nat.S Nat.O) v5
 211                     in
 212                     (match b5 with
 213                      | Bool.True ->
 214                        { Types.fst = { Types.fst = (ASM.RealInstruction
 215                          (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl
 216                          (Types.Inr { Types.fst = (ASM.INDIRECT
 217                          (Vector.from_singl v6)); Types.snd =
 218                          ASM.ACC_A }))))))); Types.snd = pc }; Types.snd =
 219                          (Nat.S Nat.O) }
 220                      | Bool.False ->
 221                        let { Types.fst = b6; Types.snd = v7 } =
 222                          Vector.head Nat.O v6
 223                        in
 224                        (match b6 with
 225                         | Bool.True ->
 226                           prod_inv_rect_Type0 (ASM.next pmem pc)
 227                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
 228                             (ASM.RealInstruction (ASM.MOV (Types.Inl
 229                             (Types.Inl (Types.Inl (Types.Inr { Types.fst =
 230                             (ASM.DIRECT b10); Types.snd = ASM.ACC_A }))))));
 231                             Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) })
 232                         | Bool.False ->
 233                           { Types.fst = { Types.fst = (ASM.RealInstruction
 234                             (ASM.CPL ASM.ACC_A)); Types.snd = pc };
 235                             Types.snd = (Nat.S Nat.O) }))
 236                   | Bool.False ->
 237                     let { Types.fst = b5; Types.snd = v6 } =
 238                       Vector.head (Nat.S Nat.O) v5
 239                     in
 240                     (match b5 with
 241                      | Bool.True ->
 242                        { Types.fst = { Types.fst = (ASM.RealInstruction
 243                          (ASM.MOVX (Types.Inr { Types.fst = (ASM.EXT_INDIRECT
 244                          (Vector.from_singl v6)); Types.snd = ASM.ACC_A })));
 245                          Types.snd = pc }; Types.snd = (Nat.S (Nat.S
 246                          Nat.O)) }
 247                      | Bool.False ->
 248                        let { Types.fst = b6; Types.snd = v7 } =
 249                          Vector.head Nat.O v6
 250                        in
 251                        (match b6 with
 252                         | Bool.True ->
 253                           prod_inv_rect_Type0 (ASM.next pmem pc)
 254                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
 255                             (ASM.ACALL (ASM.ADDR11
 256                             (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
 257                               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 258                               (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
 259                               ((Nat.S (Nat.S Nat.O)), Bool.True,
 260                               (Vector.VCons ((Nat.S Nat.O), Bool.True,
 261                               (Vector.VCons (Nat.O, Bool.True,
 262                               Vector.VEmpty)))))) b10))); Types.snd = pc0 };
 263                             Types.snd = (Nat.S (Nat.S Nat.O)) })
 264                         | Bool.False ->
 265                           { Types.fst = { Types.fst = (ASM.RealInstruction
 266                             (ASM.MOVX (Types.Inr { Types.fst =
 267                             ASM.EXT_INDIRECT_DPTR; Types.snd =
 268                             ASM.ACC_A }))); Types.snd = pc }; Types.snd =
 269                             (Nat.S (Nat.S Nat.O)) }))))
 270             | Bool.False ->
 271               let { Types.fst = b3; Types.snd = v4 } =
 272                 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
 273               in
 274               (match b3 with
 275                | Bool.True ->
 276                  { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV
 277                    (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inl
 278                    { Types.fst = ASM.ACC_A; Types.snd = (ASM.REGISTER
 279                    v4) }))))))); Types.snd = pc }; Types.snd = (Nat.S
 280                    Nat.O) }
 281                | Bool.False ->
 282                  let { Types.fst = b4; Types.snd = v5 } =
 283                    Vector.head (Nat.S (Nat.S Nat.O)) v4
 284                  in
 285                  (match b4 with
 286                   | Bool.True ->
 287                     let { Types.fst = b5; Types.snd = v6 } =
 288                       Vector.head (Nat.S Nat.O) v5
 289                     in
 290                     (match b5 with
 291                      | Bool.True ->
 292                        { Types.fst = { Types.fst = (ASM.RealInstruction
 293                          (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl
 294                          (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
 295                          (ASM.INDIRECT (Vector.from_singl v6)) })))))));
 296                          Types.snd = pc }; Types.snd = (Nat.S Nat.O) }
 297                      | Bool.False ->
 298                        let { Types.fst = b6; Types.snd = v7 } =
 299                          Vector.head Nat.O v6
 300                        in
 301                        (match b6 with
 302                         | Bool.True ->
 303                           prod_inv_rect_Type0 (ASM.next pmem pc)
 304                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
 305                             (ASM.RealInstruction (ASM.MOV (Types.Inl
 306                             (Types.Inl (Types.Inl (Types.Inl (Types.Inl
 307                             { Types.fst = ASM.ACC_A; Types.snd = (ASM.DIRECT
 308                             b10) }))))))); Types.snd = pc0 }; Types.snd =
 309                             (Nat.S Nat.O) })
 310                         | Bool.False ->
 311                           { Types.fst = { Types.fst = (ASM.RealInstruction
 312                             (ASM.CLR ASM.ACC_A)); Types.snd = pc };
 313                             Types.snd = (Nat.S Nat.O) }))
 314                   | Bool.False ->
 315                     let { Types.fst = b5; Types.snd = v6 } =
 316                       Vector.head (Nat.S Nat.O) v5
 317                     in
 318                     (match b5 with
 319                      | Bool.True ->
 320                        { Types.fst = { Types.fst = (ASM.RealInstruction
 321                          (ASM.MOVX (Types.Inl { Types.fst = ASM.ACC_A;
 322                          Types.snd = (ASM.EXT_INDIRECT
 323                          (Vector.from_singl v6)) }))); Types.snd = pc };
 324                          Types.snd = (Nat.S (Nat.S Nat.O)) }
 325                      | Bool.False ->
 326                        let { Types.fst = b6; Types.snd = v7 } =
 327                          Vector.head Nat.O v6
 328                        in
 329                        (match b6 with
 330                         | Bool.True ->
 331                           prod_inv_rect_Type0 (ASM.next pmem pc)
 332                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
 333                             (ASM.AJMP (ASM.ADDR11
 334                             (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
 335                               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 336                               (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
 337                               ((Nat.S (Nat.S Nat.O)), Bool.True,
 338                               (Vector.VCons ((Nat.S Nat.O), Bool.True,
 339                               (Vector.VCons (Nat.O, Bool.True,
 340                               Vector.VEmpty)))))) b10))); Types.snd = pc0 };
 341                             Types.snd = (Nat.S (Nat.S Nat.O)) })
 342                         | Bool.False ->
 343                           { Types.fst = { Types.fst = (ASM.RealInstruction
 344                             (ASM.MOVX (Types.Inl { Types.fst = ASM.ACC_A;
 345                             Types.snd = ASM.EXT_INDIRECT_DPTR })));
 346                             Types.snd = pc }; Types.snd = (Nat.S (Nat.S
 347                             Nat.O)) })))))
 348          | Bool.False ->
 349            let { Types.fst = b2; Types.snd = v3 } =
 350              Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2
 351            in
 352            (match b2 with
 353             | Bool.True ->
 354               let { Types.fst = b3; Types.snd = v4 } =
 355                 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
 356               in
 357               (match b3 with
 358                | Bool.True ->
 359                  prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ ->
 360                    { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.DJNZ
 361                    ((ASM.REGISTER v4), (ASM.RELATIVE b10)))); Types.snd =
 362                    pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) })
 363                | Bool.False ->
 364                  let { Types.fst = b4; Types.snd = v5 } =
 365                    Vector.head (Nat.S (Nat.S Nat.O)) v4
 366                  in
 367                  (match b4 with
 368                   | Bool.True ->
 369                     let { Types.fst = b5; Types.snd = v6 } =
 370                       Vector.head (Nat.S Nat.O) v5
 371                     in
 372                     (match b5 with
 373                      | Bool.True ->
 374                        { Types.fst = { Types.fst = (ASM.RealInstruction
 375                          (ASM.XCHD (ASM.ACC_A, (ASM.INDIRECT
 376                          (Vector.from_singl v6))))); Types.snd = pc };
 377                          Types.snd = (Nat.S Nat.O) }
 378                      | Bool.False ->
 379                        let { Types.fst = b6; Types.snd = v7 } =
 380                          Vector.head Nat.O v6
 381                        in
 382                        (match b6 with
 383                         | Bool.True ->
 384                           prod_inv_rect_Type0 (ASM.next pmem pc)
 385                             (fun pc0 b10 _ ->
 386                             prod_inv_rect_Type0 (ASM.next pmem pc0)
 387                               (fun pc1 b20 _ -> { Types.fst = { Types.fst =
 388                               (ASM.RealInstruction (ASM.DJNZ ((ASM.DIRECT
 389                               b10), (ASM.RELATIVE b20)))); Types.snd = pc1 };
 390                               Types.snd = (Nat.S (Nat.S Nat.O)) }))
 391                         | Bool.False ->
 392                           { Types.fst = { Types.fst = (ASM.RealInstruction
 393                             (ASM.DA ASM.ACC_A)); Types.snd = pc };
 394                             Types.snd = (Nat.S Nat.O) }))
 395                   | Bool.False ->
 396                     let { Types.fst = b5; Types.snd = v6 } =
 397                       Vector.head (Nat.S Nat.O) v5
 398                     in
 399                     (match b5 with
 400                      | Bool.True ->
 401                        let { Types.fst = b6; Types.snd = v7 } =
 402                          Vector.head Nat.O v6
 403                        in
 404                        (match b6 with
 405                         | Bool.True ->
 406                           { Types.fst = { Types.fst = (ASM.RealInstruction
 407                             (ASM.SETB ASM.CARRY)); Types.snd = pc };
 408                             Types.snd = (Nat.S Nat.O) }
 409                         | Bool.False ->
 410                           prod_inv_rect_Type0 (ASM.next pmem pc)
 411                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
 412                             (ASM.RealInstruction (ASM.SETB (ASM.BIT_ADDR
 413                             b10))); Types.snd = pc0 }; Types.snd = (Nat.S
 414                             Nat.O) }))
 415                      | Bool.False ->
 416                        let { Types.fst = b6; Types.snd = v7 } =
 417                          Vector.head Nat.O v6
 418                        in
 419                        (match b6 with
 420                         | Bool.True ->
 421                           prod_inv_rect_Type0 (ASM.next pmem pc)
 422                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
 423                             (ASM.ACALL (ASM.ADDR11
 424                             (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
 425                               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 426                               (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
 427                               ((Nat.S (Nat.S Nat.O)), Bool.True,
 428                               (Vector.VCons ((Nat.S Nat.O), Bool.True,
 429                               (Vector.VCons (Nat.O, Bool.False,
 430                               Vector.VEmpty)))))) b10))); Types.snd = pc0 };
 431                             Types.snd = (Nat.S (Nat.S Nat.O)) })
 432                         | Bool.False ->
 433                           prod_inv_rect_Type0 (ASM.next pmem pc)
 434                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
 435                             (ASM.RealInstruction (ASM.POP (ASM.DIRECT b10)));
 436                             Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S
 437                             Nat.O)) })))))
 438             | Bool.False ->
 439               let { Types.fst = b3; Types.snd = v4 } =
 440                 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
 441               in
 442               (match b3 with
 443                | Bool.True ->
 444                  { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.XCH
 445                    (ASM.ACC_A, (ASM.REGISTER v4)))); Types.snd = pc };
 446                    Types.snd = (Nat.S Nat.O) }
 447                | Bool.False ->
 448                  let { Types.fst = b4; Types.snd = v5 } =
 449                    Vector.head (Nat.S (Nat.S Nat.O)) v4
 450                  in
 451                  (match b4 with
 452                   | Bool.True ->
 453                     let { Types.fst = b5; Types.snd = v6 } =
 454                       Vector.head (Nat.S Nat.O) v5
 455                     in
 456                     (match b5 with
 457                      | Bool.True ->
 458                        { Types.fst = { Types.fst = (ASM.RealInstruction
 459                          (ASM.XCH (ASM.ACC_A, (ASM.INDIRECT
 460                          (Vector.from_singl v6))))); Types.snd = pc };
 461                          Types.snd = (Nat.S Nat.O) }
 462                      | Bool.False ->
 463                        let { Types.fst = b6; Types.snd = v7 } =
 464                          Vector.head Nat.O v6
 465                        in
 466                        (match b6 with
 467                         | Bool.True ->
 468                           prod_inv_rect_Type0 (ASM.next pmem pc)
 469                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
 470                             (ASM.RealInstruction (ASM.XCH (ASM.ACC_A,
 471                             (ASM.DIRECT b10)))); Types.snd = pc0 };
 472                             Types.snd = (Nat.S Nat.O) })
 473                         | Bool.False ->
 474                           { Types.fst = { Types.fst = (ASM.RealInstruction
 475                             (ASM.SWAP ASM.ACC_A)); Types.snd = pc };
 476                             Types.snd = (Nat.S Nat.O) }))
 477                   | Bool.False ->
 478                     let { Types.fst = b5; Types.snd = v6 } =
 479                       Vector.head (Nat.S Nat.O) v5
 480                     in
 481                     (match b5 with
 482                      | Bool.True ->
 483                        let { Types.fst = b6; Types.snd = v7 } =
 484                          Vector.head Nat.O v6
 485                        in
 486                        (match b6 with
 487                         | Bool.True ->
 488                           { Types.fst = { Types.fst = (ASM.RealInstruction
 489                             (ASM.CLR ASM.CARRY)); Types.snd = pc };
 490                             Types.snd = (Nat.S Nat.O) }
 491                         | Bool.False ->
 492                           prod_inv_rect_Type0 (ASM.next pmem pc)
 493                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
 494                             (ASM.RealInstruction (ASM.CLR (ASM.BIT_ADDR
 495                             b10))); Types.snd = pc0 }; Types.snd = (Nat.S
 496                             Nat.O) }))
 497                      | Bool.False ->
 498                        let { Types.fst = b6; Types.snd = v7 } =
 499                          Vector.head Nat.O v6
 500                        in
 501                        (match b6 with
 502                         | Bool.True ->
 503                           prod_inv_rect_Type0 (ASM.next pmem pc)
 504                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
 505                             (ASM.AJMP (ASM.ADDR11
 506                             (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
 507                               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 508                               (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
 509                               ((Nat.S (Nat.S Nat.O)), Bool.True,
 510                               (Vector.VCons ((Nat.S Nat.O), Bool.True,
 511                               (Vector.VCons (Nat.O, Bool.False,
 512                               Vector.VEmpty)))))) b10))); Types.snd = pc0 };
 513                             Types.snd = (Nat.S (Nat.S Nat.O)) })
 514                         | Bool.False ->
 515                           prod_inv_rect_Type0 (ASM.next pmem pc)
 516                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
 517                             (ASM.RealInstruction (ASM.PUSH (ASM.DIRECT
 518                             b10))); Types.snd = pc0 }; Types.snd = (Nat.S
 519                             (Nat.S Nat.O)) })))))))
 520       | Bool.False ->
 521         let { Types.fst = b1; Types.snd = v2 } =
 522           Vector.head (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) v1
 523         in
 524         (match b1 with
 525          | Bool.True ->
 526            let { Types.fst = b2; Types.snd = v3 } =
 527              Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2
 528            in
 529            (match b2 with
 530             | Bool.True ->
 531               let { Types.fst = b3; Types.snd = v4 } =
 532                 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
 533               in
 534               (match b3 with
 535                | Bool.True ->
 536                  prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ ->
 537                    prod_inv_rect_Type0 (ASM.next pmem pc0) (fun pc1 b20 _ ->
 538                      { Types.fst = { Types.fst = (ASM.RealInstruction
 539                      (ASM.CJNE ((Types.Inr { Types.fst = (ASM.REGISTER v4);
 540                      Types.snd = (ASM.DATA b10) }), (ASM.RELATIVE b20))));
 541                      Types.snd = pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) }))
 542                | Bool.False ->
 543                  let { Types.fst = b4; Types.snd = v5 } =
 544                    Vector.head (Nat.S (Nat.S Nat.O)) v4
 545                  in
 546                  (match b4 with
 547                   | Bool.True ->
 548                     let { Types.fst = b5; Types.snd = v6 } =
 549                       Vector.head (Nat.S Nat.O) v5
 550                     in
 551                     (match b5 with
 552                      | Bool.True ->
 553                        prod_inv_rect_Type0 (ASM.next pmem pc)
 554                          (fun pc0 b10 _ ->
 555                          prod_inv_rect_Type0 (ASM.next pmem pc0)
 556                            (fun pc1 b20 _ -> { Types.fst = { Types.fst =
 557                            (ASM.RealInstruction (ASM.CJNE ((Types.Inr
 558                            { Types.fst = (ASM.INDIRECT
 559                            (Vector.from_singl v6)); Types.snd = (ASM.DATA
 560                            b10) }), (ASM.RELATIVE b20)))); Types.snd = pc1 };
 561                            Types.snd = (Nat.S (Nat.S Nat.O)) }))
 562                      | Bool.False ->
 563                        let { Types.fst = b6; Types.snd = v7 } =
 564                          Vector.head Nat.O v6
 565                        in
 566                        (match b6 with
 567                         | Bool.True ->
 568                           prod_inv_rect_Type0 (ASM.next pmem pc)
 569                             (fun pc0 b10 _ ->
 570                             prod_inv_rect_Type0 (ASM.next pmem pc0)
 571                               (fun pc1 b20 _ -> { Types.fst = { Types.fst =
 572                               (ASM.RealInstruction (ASM.CJNE ((Types.Inl
 573                               { Types.fst = ASM.ACC_A; Types.snd =
 574                               (ASM.DIRECT b10) }), (ASM.RELATIVE b20))));
 575                               Types.snd = pc1 }; Types.snd = (Nat.S (Nat.S
 576                               Nat.O)) }))
 577                         | Bool.False ->
 578                           prod_inv_rect_Type0 (ASM.next pmem pc)
 579                             (fun pc0 b10 _ ->
 580                             prod_inv_rect_Type0 (ASM.next pmem pc0)
 581                               (fun pc1 b20 _ -> { Types.fst = { Types.fst =
 582                               (ASM.RealInstruction (ASM.CJNE ((Types.Inl
 583                               { Types.fst = ASM.ACC_A; Types.snd = (ASM.DATA
 584                               b10) }), (ASM.RELATIVE b20)))); Types.snd =
 585                               pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) }))))
 586                   | Bool.False ->
 587                     let { Types.fst = b5; Types.snd = v6 } =
 588                       Vector.head (Nat.S Nat.O) v5
 589                     in
 590                     (match b5 with
 591                      | Bool.True ->
 592                        let { Types.fst = b6; Types.snd = v7 } =
 593                          Vector.head Nat.O v6
 594                        in
 595                        (match b6 with
 596                         | Bool.True ->
 597                           { Types.fst = { Types.fst = (ASM.RealInstruction
 598                             (ASM.CPL ASM.CARRY)); Types.snd = pc };
 599                             Types.snd = (Nat.S Nat.O) }
 600                         | Bool.False ->
 601                           prod_inv_rect_Type0 (ASM.next pmem pc)
 602                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
 603                             (ASM.RealInstruction (ASM.CPL (ASM.BIT_ADDR
 604                             b10))); Types.snd = pc0 }; Types.snd = (Nat.S
 605                             Nat.O) }))
 606                      | Bool.False ->
 607                        let { Types.fst = b6; Types.snd = v7 } =
 608                          Vector.head Nat.O v6
 609                        in
 610                        (match b6 with
 611                         | Bool.True ->
 612                           prod_inv_rect_Type0 (ASM.next pmem pc)
 613                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
 614                             (ASM.ACALL (ASM.ADDR11
 615                             (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
 616                               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 617                               (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
 618                               ((Nat.S (Nat.S Nat.O)), Bool.True,
 619                               (Vector.VCons ((Nat.S Nat.O), Bool.False,
 620                               (Vector.VCons (Nat.O, Bool.True,
 621                               Vector.VEmpty)))))) b10))); Types.snd = pc0 };
 622                             Types.snd = (Nat.S (Nat.S Nat.O)) })
 623                         | Bool.False ->
 624                           prod_inv_rect_Type0 (ASM.next pmem pc)
 625                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
 626                             (ASM.RealInstruction (ASM.ANL (Types.Inr
 627                             { Types.fst = ASM.CARRY; Types.snd =
 628                             (ASM.N_BIT_ADDR b10) }))); Types.snd = pc0 };
 629                             Types.snd = (Nat.S (Nat.S Nat.O)) })))))
 630             | Bool.False ->
 631               let { Types.fst = b3; Types.snd = v4 } =
 632                 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
 633               in
 634               (match b3 with
 635                | Bool.True ->
 636                  prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ ->
 637                    { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV
 638                    (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr
 639                    { Types.fst = (ASM.REGISTER v4); Types.snd = (ASM.DIRECT
 640                    b10) }))))))); Types.snd = pc0 }; Types.snd = (Nat.S
 641                    (Nat.S Nat.O)) })
 642                | Bool.False ->
 643                  let { Types.fst = b4; Types.snd = v5 } =
 644                    Vector.head (Nat.S (Nat.S Nat.O)) v4
 645                  in
 646                  (match b4 with
 647                   | Bool.True ->
 648                     let { Types.fst = b5; Types.snd = v6 } =
 649                       Vector.head (Nat.S Nat.O) v5
 650                     in
 651                     (match b5 with
 652                      | Bool.True ->
 653                        prod_inv_rect_Type0 (ASM.next pmem pc)
 654                          (fun pc0 b10 _ -> { Types.fst = { Types.fst =
 655                          (ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl
 656                          (Types.Inl (Types.Inl (Types.Inr { Types.fst =
 657                          (ASM.INDIRECT (Vector.from_singl v6)); Types.snd =
 658                          (ASM.DIRECT b10) }))))))); Types.snd = pc0 };
 659                          Types.snd = (Nat.S (Nat.S Nat.O)) })
 660                      | Bool.False ->
 661                        { Types.fst = { Types.fst = (ASM.RealInstruction
 662                          (ASM.MUL (ASM.ACC_A, ASM.ACC_B))); Types.snd = pc };
 663                          Types.snd = (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) })
 664                   | Bool.False ->
 665                     let { Types.fst = b5; Types.snd = v6 } =
 666                       Vector.head (Nat.S Nat.O) v5
 667                     in
 668                     (match b5 with
 669                      | Bool.True ->
 670                        let { Types.fst = b6; Types.snd = v7 } =
 671                          Vector.head Nat.O v6
 672                        in
 673                        (match b6 with
 674                         | Bool.True ->
 675                           { Types.fst = { Types.fst = (ASM.RealInstruction
 676                             (ASM.INC ASM.DPTR)); Types.snd = pc };
 677                             Types.snd = (Nat.S (Nat.S Nat.O)) }
 678                         | Bool.False ->
 679                           prod_inv_rect_Type0 (ASM.next pmem pc)
 680                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
 681                             (ASM.RealInstruction (ASM.MOV (Types.Inl
 682                             (Types.Inr { Types.fst = ASM.CARRY; Types.snd =
 683                             (ASM.BIT_ADDR b10) })))); Types.snd = pc0 };
 684                             Types.snd = (Nat.S Nat.O) }))
 685                      | Bool.False ->
 686                        let { Types.fst = b6; Types.snd = v7 } =
 687                          Vector.head Nat.O v6
 688                        in
 689                        (match b6 with
 690                         | Bool.True ->
 691                           prod_inv_rect_Type0 (ASM.next pmem pc)
 692                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
 693                             (ASM.AJMP (ASM.ADDR11
 694                             (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
 695                               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 696                               (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
 697                               ((Nat.S (Nat.S Nat.O)), Bool.True,
 698                               (Vector.VCons ((Nat.S Nat.O), Bool.False,
 699                               (Vector.VCons (Nat.O, Bool.True,
 700                               Vector.VEmpty)))))) b10))); Types.snd = pc0 };
 701                             Types.snd = (Nat.S (Nat.S Nat.O)) })
 702                         | Bool.False ->
 703                           prod_inv_rect_Type0 (ASM.next pmem pc)
 704                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
 705                             (ASM.RealInstruction (ASM.ORL (Types.Inr
 706                             { Types.fst = ASM.CARRY; Types.snd =
 707                             (ASM.N_BIT_ADDR b10) }))); Types.snd = pc0 };
 708                             Types.snd = (Nat.S (Nat.S Nat.O)) }))))))
 709          | Bool.False ->
 710            let { Types.fst = b2; Types.snd = v3 } =
 711              Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2
 712            in
 713            (match b2 with
 714             | Bool.True ->
 715               let { Types.fst = b3; Types.snd = v4 } =
 716                 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
 717               in
 718               (match b3 with
 719                | Bool.True ->
 720                  { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.SUBB
 721                    (ASM.ACC_A, (ASM.REGISTER v4)))); Types.snd = pc };
 722                    Types.snd = (Nat.S Nat.O) }
 723                | Bool.False ->
 724                  let { Types.fst = b4; Types.snd = v5 } =
 725                    Vector.head (Nat.S (Nat.S Nat.O)) v4
 726                  in
 727                  (match b4 with
 728                   | Bool.True ->
 729                     let { Types.fst = b5; Types.snd = v6 } =
 730                       Vector.head (Nat.S Nat.O) v5
 731                     in
 732                     (match b5 with
 733                      | Bool.True ->
 734                        { Types.fst = { Types.fst = (ASM.RealInstruction
 735                          (ASM.SUBB (ASM.ACC_A, (ASM.INDIRECT
 736                          (Vector.from_singl v6))))); Types.snd = pc };
 737                          Types.snd = (Nat.S Nat.O) }
 738                      | Bool.False ->
 739                        let { Types.fst = b6; Types.snd = v7 } =
 740                          Vector.head Nat.O v6
 741                        in
 742                        (match b6 with
 743                         | Bool.True ->
 744                           prod_inv_rect_Type0 (ASM.next pmem pc)
 745                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
 746                             (ASM.RealInstruction (ASM.SUBB (ASM.ACC_A,
 747                             (ASM.DIRECT b10)))); Types.snd = pc0 };
 748                             Types.snd = (Nat.S Nat.O) })
 749                         | Bool.False ->
 750                           prod_inv_rect_Type0 (ASM.next pmem pc)
 751                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
 752                             (ASM.RealInstruction (ASM.SUBB (ASM.ACC_A,
 753                             (ASM.DATA b10)))); Types.snd = pc0 }; Types.snd =
 754                             (Nat.S Nat.O) })))
 755                   | Bool.False ->
 756                     let { Types.fst = b5; Types.snd = v6 } =
 757                       Vector.head (Nat.S Nat.O) v5
 758                     in
 759                     (match b5 with
 760                      | Bool.True ->
 761                        let { Types.fst = b6; Types.snd = v7 } =
 762                          Vector.head Nat.O v6
 763                        in
 764                        (match b6 with
 765                         | Bool.True ->
 766                           { Types.fst = { Types.fst = (ASM.MOVC (ASM.ACC_A,
 767                             ASM.ACC_DPTR)); Types.snd = pc }; Types.snd =
 768                             (Nat.S (Nat.S Nat.O)) }
 769                         | Bool.False ->
 770                           prod_inv_rect_Type0 (ASM.next pmem pc)
 771                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
 772                             (ASM.RealInstruction (ASM.MOV (Types.Inr
 773                             { Types.fst = (ASM.BIT_ADDR b10); Types.snd =
 774                             ASM.CARRY }))); Types.snd = pc0 }; Types.snd =
 775                             (Nat.S (Nat.S Nat.O)) }))
 776                      | Bool.False ->
 777                        let { Types.fst = b6; Types.snd = v7 } =
 778                          Vector.head Nat.O v6
 779                        in
 780                        (match b6 with
 781                         | Bool.True ->
 782                           prod_inv_rect_Type0 (ASM.next pmem pc)
 783                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
 784                             (ASM.ACALL (ASM.ADDR11
 785                             (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
 786                               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 787                               (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
 788                               ((Nat.S (Nat.S Nat.O)), Bool.True,
 789                               (Vector.VCons ((Nat.S Nat.O), Bool.False,
 790                               (Vector.VCons (Nat.O, Bool.False,
 791                               Vector.VEmpty)))))) b10))); Types.snd = pc0 };
 792                             Types.snd = (Nat.S (Nat.S Nat.O)) })
 793                         | Bool.False ->
 794                           prod_inv_rect_Type0 (ASM.next pmem pc)
 795                             (fun pc0 b10 _ ->
 796                             prod_inv_rect_Type0 (ASM.next pmem pc0)
 797                               (fun pc1 b20 _ -> { Types.fst = { Types.fst =
 798                               (ASM.RealInstruction (ASM.MOV (Types.Inl
 799                               (Types.Inl (Types.Inr { Types.fst = ASM.DPTR;
 800                               Types.snd = (ASM.DATA16
 801                               (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S
 802                                 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
 803                                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 804                                 (Nat.S (Nat.S Nat.O)))))))) b10 b20)) })))));
 805                               Types.snd = pc1 }; Types.snd = (Nat.S (Nat.S
 806                               Nat.O)) }))))))
 807             | Bool.False ->
 808               let { Types.fst = b3; Types.snd = v4 } =
 809                 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
 810               in
 811               (match b3 with
 812                | Bool.True ->
 813                  prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ ->
 814                    { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV
 815                    (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst =
 816                    (ASM.DIRECT b10); Types.snd = (ASM.REGISTER v4) }))))));
 817                    Types.snd = pc0 }; Types.snd = (Nat.S (Nat.S Nat.O)) })
 818                | Bool.False ->
 819                  let { Types.fst = b4; Types.snd = v5 } =
 820                    Vector.head (Nat.S (Nat.S Nat.O)) v4
 821                  in
 822                  (match b4 with
 823                   | Bool.True ->
 824                     let { Types.fst = b5; Types.snd = v6 } =
 825                       Vector.head (Nat.S Nat.O) v5
 826                     in
 827                     (match b5 with
 828                      | Bool.True ->
 829                        prod_inv_rect_Type0 (ASM.next pmem pc)
 830                          (fun pc0 b10 _ -> { Types.fst = { Types.fst =
 831                          (ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl
 832                          (Types.Inl (Types.Inr { Types.fst = (ASM.DIRECT
 833                          b10); Types.snd = (ASM.INDIRECT
 834                          (Vector.from_singl v6)) })))))); Types.snd = pc0 };
 835                          Types.snd = (Nat.S (Nat.S Nat.O)) })
 836                      | Bool.False ->
 837                        let { Types.fst = b6; Types.snd = v7 } =
 838                          Vector.head Nat.O v6
 839                        in
 840                        (match b6 with
 841                         | Bool.True ->
 842                           prod_inv_rect_Type0 (ASM.next pmem pc)
 843                             (fun pc0 b10 _ ->
 844                             prod_inv_rect_Type0 (ASM.next pmem pc0)
 845                               (fun pc1 b20 _ -> { Types.fst = { Types.fst =
 846                               (ASM.RealInstruction (ASM.MOV (Types.Inl
 847                               (Types.Inl (Types.Inl (Types.Inr { Types.fst =
 848                               (ASM.DIRECT b10); Types.snd = (ASM.DIRECT
 849                               b20) })))))); Types.snd = pc1 }; Types.snd =
 850                               (Nat.S (Nat.S Nat.O)) }))
 851                         | Bool.False ->
 852                           { Types.fst = { Types.fst = (ASM.RealInstruction
 853                             (ASM.DIV (ASM.ACC_A, ASM.ACC_B))); Types.snd =
 854                             pc }; Types.snd = (Nat.S (Nat.S (Nat.S (Nat.S
 855                             Nat.O)))) }))
 856                   | Bool.False ->
 857                     let { Types.fst = b5; Types.snd = v6 } =
 858                       Vector.head (Nat.S Nat.O) v5
 859                     in
 860                     (match b5 with
 861                      | Bool.True ->
 862                        let { Types.fst = b6; Types.snd = v7 } =
 863                          Vector.head Nat.O v6
 864                        in
 865                        (match b6 with
 866                         | Bool.True ->
 867                           { Types.fst = { Types.fst = (ASM.MOVC (ASM.ACC_A,
 868                             ASM.ACC_PC)); Types.snd = pc }; Types.snd =
 869                             (Nat.S (Nat.S Nat.O)) }
 870                         | Bool.False ->
 871                           prod_inv_rect_Type0 (ASM.next pmem pc)
 872                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
 873                             (ASM.RealInstruction (ASM.ANL (Types.Inr
 874                             { Types.fst = ASM.CARRY; Types.snd =
 875                             (ASM.BIT_ADDR b10) }))); Types.snd = pc0 };
 876                             Types.snd = (Nat.S (Nat.S Nat.O)) }))
 877                      | Bool.False ->
 878                        let { Types.fst = b6; Types.snd = v7 } =
 879                          Vector.head Nat.O v6
 880                        in
 881                        (match b6 with
 882                         | Bool.True ->
 883                           prod_inv_rect_Type0 (ASM.next pmem pc)
 884                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
 885                             (ASM.AJMP (ASM.ADDR11
 886                             (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
 887                               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 888                               (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
 889                               ((Nat.S (Nat.S Nat.O)), Bool.True,
 890                               (Vector.VCons ((Nat.S Nat.O), Bool.False,
 891                               (Vector.VCons (Nat.O, Bool.False,
 892                               Vector.VEmpty)))))) b10))); Types.snd = pc0 };
 893                             Types.snd = (Nat.S (Nat.S Nat.O)) })
 894                         | Bool.False ->
 895                           prod_inv_rect_Type0 (ASM.next pmem pc)
 896                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
 897                             (ASM.SJMP (ASM.RELATIVE b10)); Types.snd = pc0 };
 898                             Types.snd = (Nat.S (Nat.S Nat.O)) }))))))))
 899    | Bool.False ->
 900      let { Types.fst = b0; Types.snd = v1 } =
 901        Vector.head (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))) v0
 902      in
 903      (match b0 with
 904       | Bool.True ->
 905         let { Types.fst = b1; Types.snd = v2 } =
 906           Vector.head (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) v1
 907         in
 908         (match b1 with
 909          | Bool.True ->
 910            let { Types.fst = b2; Types.snd = v3 } =
 911              Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2
 912            in
 913            (match b2 with
 914             | Bool.True ->
 915               let { Types.fst = b3; Types.snd = v4 } =
 916                 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
 917               in
 918               (match b3 with
 919                | Bool.True ->
 920                  prod_inv_rect_Type0 (ASM.next pmem pc) (fun pc0 b10 _ ->
 921                    { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV
 922                    (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr
 923                    { Types.fst = (ASM.REGISTER v4); Types.snd = (ASM.DATA
 924                    b10) }))))))); Types.snd = pc0 }; Types.snd = (Nat.S
 925                    Nat.O) })
 926                | Bool.False ->
 927                  let { Types.fst = b4; Types.snd = v5 } =
 928                    Vector.head (Nat.S (Nat.S Nat.O)) v4
 929                  in
 930                  (match b4 with
 931                   | Bool.True ->
 932                     let { Types.fst = b5; Types.snd = v6 } =
 933                       Vector.head (Nat.S Nat.O) v5
 934                     in
 935                     (match b5 with
 936                      | Bool.True ->
 937                        prod_inv_rect_Type0 (ASM.next pmem pc)
 938                          (fun pc0 b10 _ -> { Types.fst = { Types.fst =
 939                          (ASM.RealInstruction (ASM.MOV (Types.Inl (Types.Inl
 940                          (Types.Inl (Types.Inl (Types.Inr { Types.fst =
 941                          (ASM.INDIRECT (Vector.from_singl v6)); Types.snd =
 942                          (ASM.DATA b10) }))))))); Types.snd = pc0 };
 943                          Types.snd = (Nat.S Nat.O) })
 944                      | Bool.False ->
 945                        let { Types.fst = b6; Types.snd = v7 } =
 946                          Vector.head Nat.O v6
 947                        in
 948                        (match b6 with
 949                         | Bool.True ->
 950                           prod_inv_rect_Type0 (ASM.next pmem pc)
 951                             (fun pc0 b10 _ ->
 952                             prod_inv_rect_Type0 (ASM.next pmem pc0)
 953                               (fun pc1 b20 _ -> { Types.fst = { Types.fst =
 954                               (ASM.RealInstruction (ASM.MOV (Types.Inl
 955                               (Types.Inl (Types.Inl (Types.Inr { Types.fst =
 956                               (ASM.DIRECT b10); Types.snd = (ASM.DATA
 957                               b20) })))))); Types.snd = pc1 }; Types.snd =
 958                               (Nat.S (Nat.S (Nat.S Nat.O))) }))
 959                         | Bool.False ->
 960                           prod_inv_rect_Type0 (ASM.next pmem pc)
 961                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
 962                             (ASM.RealInstruction (ASM.MOV (Types.Inl
 963                             (Types.Inl (Types.Inl (Types.Inl (Types.Inl
 964                             { Types.fst = ASM.ACC_A; Types.snd = (ASM.DATA
 965                             b10) }))))))); Types.snd = pc0 }; Types.snd =
 966                             (Nat.S Nat.O) })))
 967                   | Bool.False ->
 968                     let { Types.fst = b5; Types.snd = v6 } =
 969                       Vector.head (Nat.S Nat.O) v5
 970                     in
 971                     (match b5 with
 972                      | Bool.True ->
 973                        let { Types.fst = b6; Types.snd = v7 } =
 974                          Vector.head Nat.O v6
 975                        in
 976                        (match b6 with
 977                         | Bool.True ->
 978                           { Types.fst = { Types.fst = (ASM.RealInstruction
 979                             (ASM.JMP ASM.ACC_DPTR)); Types.snd = pc };
 980                             Types.snd = (Nat.S (Nat.S Nat.O)) }
 981                         | Bool.False ->
 982                           prod_inv_rect_Type0 (ASM.next pmem pc)
 983                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
 984                             (ASM.RealInstruction (ASM.ORL (Types.Inr
 985                             { Types.fst = ASM.CARRY; Types.snd =
 986                             (ASM.BIT_ADDR b10) }))); Types.snd = pc0 };
 987                             Types.snd = (Nat.S (Nat.S Nat.O)) }))
 988                      | Bool.False ->
 989                        let { Types.fst = b6; Types.snd = v7 } =
 990                          Vector.head Nat.O v6
 991                        in
 992                        (match b6 with
 993                         | Bool.True ->
 994                           prod_inv_rect_Type0 (ASM.next pmem pc)
 995                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
 996                             (ASM.ACALL (ASM.ADDR11
 997                             (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
 998                               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 999                               (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
1000                               ((Nat.S (Nat.S Nat.O)), Bool.False,
1001                               (Vector.VCons ((Nat.S Nat.O), Bool.True,
1002                               (Vector.VCons (Nat.O, Bool.True,
1003                               Vector.VEmpty)))))) b10))); Types.snd = pc0 };
1004                             Types.snd = (Nat.S (Nat.S Nat.O)) })
1005                         | Bool.False ->
1006                           prod_inv_rect_Type0 (ASM.next pmem pc)
1007                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1008                             (ASM.RealInstruction (ASM.JNZ (ASM.RELATIVE
1009                             b10))); Types.snd = pc0 }; Types.snd = (Nat.S
1010                             (Nat.S Nat.O)) })))))
1011             | Bool.False ->
1012               let { Types.fst = b3; Types.snd = v4 } =
1013                 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
1014               in
1015               (match b3 with
1016                | Bool.True ->
1017                  { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.XRL
1018                    (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
1019                    (ASM.REGISTER v4) }))); Types.snd = pc }; Types.snd =
1020                    (Nat.S Nat.O) }
1021                | Bool.False ->
1022                  let { Types.fst = b4; Types.snd = v5 } =
1023                    Vector.head (Nat.S (Nat.S Nat.O)) v4
1024                  in
1025                  (match b4 with
1026                   | Bool.True ->
1027                     let { Types.fst = b5; Types.snd = v6 } =
1028                       Vector.head (Nat.S Nat.O) v5
1029                     in
1030                     (match b5 with
1031                      | Bool.True ->
1032                        { Types.fst = { Types.fst = (ASM.RealInstruction
1033                          (ASM.XRL (Types.Inl { Types.fst = ASM.ACC_A;
1034                          Types.snd = (ASM.INDIRECT
1035                          (Vector.from_singl v6)) }))); Types.snd = pc };
1036                          Types.snd = (Nat.S Nat.O) }
1037                      | Bool.False ->
1038                        let { Types.fst = b6; Types.snd = v7 } =
1039                          Vector.head Nat.O v6
1040                        in
1041                        (match b6 with
1042                         | Bool.True ->
1043                           prod_inv_rect_Type0 (ASM.next pmem pc)
1044                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1045                             (ASM.RealInstruction (ASM.XRL (Types.Inl
1046                             { Types.fst = ASM.ACC_A; Types.snd = (ASM.DIRECT
1047                             b10) }))); Types.snd = pc0 }; Types.snd = (Nat.S
1048                             Nat.O) })
1049                         | Bool.False ->
1050                           prod_inv_rect_Type0 (ASM.next pmem pc)
1051                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1052                             (ASM.RealInstruction (ASM.XRL (Types.Inl
1053                             { Types.fst = ASM.ACC_A; Types.snd = (ASM.DATA
1054                             b10) }))); Types.snd = pc0 }; Types.snd = (Nat.S
1055                             Nat.O) })))
1056                   | Bool.False ->
1057                     let { Types.fst = b5; Types.snd = v6 } =
1058                       Vector.head (Nat.S Nat.O) v5
1059                     in
1060                     (match b5 with
1061                      | Bool.True ->
1062                        let { Types.fst = b6; Types.snd = v7 } =
1063                          Vector.head Nat.O v6
1064                        in
1065                        (match b6 with
1066                         | Bool.True ->
1067                           prod_inv_rect_Type0 (ASM.next pmem pc)
1068                             (fun pc0 b10 _ ->
1069                             prod_inv_rect_Type0 (ASM.next pmem pc0)
1070                               (fun pc1 b20 _ -> { Types.fst = { Types.fst =
1071                               (ASM.RealInstruction (ASM.XRL (Types.Inr
1072                               { Types.fst = (ASM.DIRECT b10); Types.snd =
1073                               (ASM.DATA b20) }))); Types.snd = pc1 };
1074                               Types.snd = (Nat.S (Nat.S Nat.O)) }))
1075                         | Bool.False ->
1076                           prod_inv_rect_Type0 (ASM.next pmem pc)
1077                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1078                             (ASM.RealInstruction (ASM.XRL (Types.Inr
1079                             { Types.fst = (ASM.DIRECT b10); Types.snd =
1080                             ASM.ACC_A }))); Types.snd = pc0 }; Types.snd =
1081                             (Nat.S Nat.O) }))
1082                      | Bool.False ->
1083                        let { Types.fst = b6; Types.snd = v7 } =
1084                          Vector.head Nat.O v6
1085                        in
1086                        (match b6 with
1087                         | Bool.True ->
1088                           prod_inv_rect_Type0 (ASM.next pmem pc)
1089                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1090                             (ASM.AJMP (ASM.ADDR11
1091                             (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
1092                               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1093                               (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
1094                               ((Nat.S (Nat.S Nat.O)), Bool.False,
1095                               (Vector.VCons ((Nat.S Nat.O), Bool.True,
1096                               (Vector.VCons (Nat.O, Bool.True,
1097                               Vector.VEmpty)))))) b10))); Types.snd = pc0 };
1098                             Types.snd = (Nat.S (Nat.S Nat.O)) })
1099                         | Bool.False ->
1100                           prod_inv_rect_Type0 (ASM.next pmem pc)
1101                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1102                             (ASM.RealInstruction (ASM.JZ (ASM.RELATIVE
1103                             b10))); Types.snd = pc0 }; Types.snd = (Nat.S
1104                             (Nat.S Nat.O)) }))))))
1105          | Bool.False ->
1106            let { Types.fst = b2; Types.snd = v3 } =
1107              Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2
1108            in
1109            (match b2 with
1110             | Bool.True ->
1111               let { Types.fst = b3; Types.snd = v4 } =
1112                 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
1113               in
1114               (match b3 with
1115                | Bool.True ->
1116                  { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ANL
1117                    (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
1118                    (ASM.REGISTER v4) })))); Types.snd = pc }; Types.snd =
1119                    (Nat.S Nat.O) }
1120                | Bool.False ->
1121                  let { Types.fst = b4; Types.snd = v5 } =
1122                    Vector.head (Nat.S (Nat.S Nat.O)) v4
1123                  in
1124                  (match b4 with
1125                   | Bool.True ->
1126                     let { Types.fst = b5; Types.snd = v6 } =
1127                       Vector.head (Nat.S Nat.O) v5
1128                     in
1129                     (match b5 with
1130                      | Bool.True ->
1131                        { Types.fst = { Types.fst = (ASM.RealInstruction
1132                          (ASM.ANL (Types.Inl (Types.Inl { Types.fst =
1133                          ASM.ACC_A; Types.snd = (ASM.INDIRECT
1134                          (Vector.from_singl v6)) })))); Types.snd = pc };
1135                          Types.snd = (Nat.S Nat.O) }
1136                      | Bool.False ->
1137                        let { Types.fst = b6; Types.snd = v7 } =
1138                          Vector.head Nat.O v6
1139                        in
1140                        (match b6 with
1141                         | Bool.True ->
1142                           prod_inv_rect_Type0 (ASM.next pmem pc)
1143                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1144                             (ASM.RealInstruction (ASM.ANL (Types.Inl
1145                             (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
1146                             (ASM.DIRECT b10) })))); Types.snd = pc0 };
1147                             Types.snd = (Nat.S Nat.O) })
1148                         | Bool.False ->
1149                           prod_inv_rect_Type0 (ASM.next pmem pc)
1150                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1151                             (ASM.RealInstruction (ASM.ANL (Types.Inl
1152                             (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
1153                             (ASM.DATA b10) })))); Types.snd = pc0 };
1154                             Types.snd = (Nat.S Nat.O) })))
1155                   | Bool.False ->
1156                     let { Types.fst = b5; Types.snd = v6 } =
1157                       Vector.head (Nat.S Nat.O) v5
1158                     in
1159                     (match b5 with
1160                      | Bool.True ->
1161                        let { Types.fst = b6; Types.snd = v7 } =
1162                          Vector.head Nat.O v6
1163                        in
1164                        (match b6 with
1165                         | Bool.True ->
1166                           prod_inv_rect_Type0 (ASM.next pmem pc)
1167                             (fun pc0 b10 _ ->
1168                             prod_inv_rect_Type0 (ASM.next pmem pc0)
1169                               (fun pc1 b20 _ -> { Types.fst = { Types.fst =
1170                               (ASM.RealInstruction (ASM.ANL (Types.Inl
1171                               (Types.Inr { Types.fst = (ASM.DIRECT b10);
1172                               Types.snd = (ASM.DATA b20) })))); Types.snd =
1173                               pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) }))
1174                         | Bool.False ->
1175                           prod_inv_rect_Type0 (ASM.next pmem pc)
1176                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1177                             (ASM.RealInstruction (ASM.ANL (Types.Inl
1178                             (Types.Inr { Types.fst = (ASM.DIRECT b10);
1179                             Types.snd = ASM.ACC_A })))); Types.snd = pc0 };
1180                             Types.snd = (Nat.S Nat.O) }))
1181                      | Bool.False ->
1182                        let { Types.fst = b6; Types.snd = v7 } =
1183                          Vector.head Nat.O v6
1184                        in
1185                        (match b6 with
1186                         | Bool.True ->
1187                           prod_inv_rect_Type0 (ASM.next pmem pc)
1188                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1189                             (ASM.ACALL (ASM.ADDR11
1190                             (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
1191                               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1192                               (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
1193                               ((Nat.S (Nat.S Nat.O)), Bool.False,
1194                               (Vector.VCons ((Nat.S Nat.O), Bool.True,
1195                               (Vector.VCons (Nat.O, Bool.False,
1196                               Vector.VEmpty)))))) b10))); Types.snd = pc0 };
1197                             Types.snd = (Nat.S (Nat.S Nat.O)) })
1198                         | Bool.False ->
1199                           prod_inv_rect_Type0 (ASM.next pmem pc)
1200                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1201                             (ASM.RealInstruction (ASM.JNC (ASM.RELATIVE
1202                             b10))); Types.snd = pc0 }; Types.snd = (Nat.S
1203                             (Nat.S Nat.O)) })))))
1204             | Bool.False ->
1205               let { Types.fst = b3; Types.snd = v4 } =
1206                 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
1207               in
1208               (match b3 with
1209                | Bool.True ->
1210                  { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ORL
1211                    (Types.Inl (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
1212                    (ASM.REGISTER v4) })))); Types.snd = pc }; Types.snd =
1213                    (Nat.S Nat.O) }
1214                | Bool.False ->
1215                  let { Types.fst = b4; Types.snd = v5 } =
1216                    Vector.head (Nat.S (Nat.S Nat.O)) v4
1217                  in
1218                  (match b4 with
1219                   | Bool.True ->
1220                     let { Types.fst = b5; Types.snd = v6 } =
1221                       Vector.head (Nat.S Nat.O) v5
1222                     in
1223                     (match b5 with
1224                      | Bool.True ->
1225                        { Types.fst = { Types.fst = (ASM.RealInstruction
1226                          (ASM.ORL (Types.Inl (Types.Inl { Types.fst =
1227                          ASM.ACC_A; Types.snd = (ASM.INDIRECT
1228                          (Vector.from_singl v6)) })))); Types.snd = pc };
1229                          Types.snd = (Nat.S Nat.O) }
1230                      | Bool.False ->
1231                        let { Types.fst = b6; Types.snd = v7 } =
1232                          Vector.head Nat.O v6
1233                        in
1234                        (match b6 with
1235                         | Bool.True ->
1236                           prod_inv_rect_Type0 (ASM.next pmem pc)
1237                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1238                             (ASM.RealInstruction (ASM.ORL (Types.Inl
1239                             (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
1240                             (ASM.DIRECT b10) })))); Types.snd = pc0 };
1241                             Types.snd = (Nat.S Nat.O) })
1242                         | Bool.False ->
1243                           prod_inv_rect_Type0 (ASM.next pmem pc)
1244                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1245                             (ASM.RealInstruction (ASM.ORL (Types.Inl
1246                             (Types.Inl { Types.fst = ASM.ACC_A; Types.snd =
1247                             (ASM.DATA b10) })))); Types.snd = pc0 };
1248                             Types.snd = (Nat.S Nat.O) })))
1249                   | Bool.False ->
1250                     let { Types.fst = b5; Types.snd = v6 } =
1251                       Vector.head (Nat.S Nat.O) v5
1252                     in
1253                     (match b5 with
1254                      | Bool.True ->
1255                        let { Types.fst = b6; Types.snd = v7 } =
1256                          Vector.head Nat.O v6
1257                        in
1258                        (match b6 with
1259                         | Bool.True ->
1260                           prod_inv_rect_Type0 (ASM.next pmem pc)
1261                             (fun pc0 b10 _ ->
1262                             prod_inv_rect_Type0 (ASM.next pmem pc0)
1263                               (fun pc1 b20 _ -> { Types.fst = { Types.fst =
1264                               (ASM.RealInstruction (ASM.ORL (Types.Inl
1265                               (Types.Inr { Types.fst = (ASM.DIRECT b10);
1266                               Types.snd = (ASM.DATA b20) })))); Types.snd =
1267                               pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) }))
1268                         | Bool.False ->
1269                           prod_inv_rect_Type0 (ASM.next pmem pc)
1270                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1271                             (ASM.RealInstruction (ASM.ORL (Types.Inl
1272                             (Types.Inr { Types.fst = (ASM.DIRECT b10);
1273                             Types.snd = ASM.ACC_A })))); Types.snd = pc0 };
1274                             Types.snd = (Nat.S Nat.O) }))
1275                      | Bool.False ->
1276                        let { Types.fst = b6; Types.snd = v7 } =
1277                          Vector.head Nat.O v6
1278                        in
1279                        (match b6 with
1280                         | Bool.True ->
1281                           prod_inv_rect_Type0 (ASM.next pmem pc)
1282                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1283                             (ASM.AJMP (ASM.ADDR11
1284                             (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
1285                               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1286                               (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
1287                               ((Nat.S (Nat.S Nat.O)), Bool.False,
1288                               (Vector.VCons ((Nat.S Nat.O), Bool.True,
1289                               (Vector.VCons (Nat.O, Bool.False,
1290                               Vector.VEmpty)))))) b10))); Types.snd = pc0 };
1291                             Types.snd = (Nat.S (Nat.S Nat.O)) })
1292                         | Bool.False ->
1293                           prod_inv_rect_Type0 (ASM.next pmem pc)
1294                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1295                             (ASM.RealInstruction (ASM.JC (ASM.RELATIVE
1296                             b10))); Types.snd = pc0 }; Types.snd = (Nat.S
1297                             (Nat.S Nat.O)) })))))))
1298       | Bool.False ->
1299         let { Types.fst = b1; Types.snd = v2 } =
1300           Vector.head (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))) v1
1301         in
1302         (match b1 with
1303          | Bool.True ->
1304            let { Types.fst = b2; Types.snd = v3 } =
1305              Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2
1306            in
1307            (match b2 with
1308             | Bool.True ->
1309               let { Types.fst = b3; Types.snd = v4 } =
1310                 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
1311               in
1312               (match b3 with
1313                | Bool.True ->
1314                  { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ADDC
1315                    (ASM.ACC_A, (ASM.REGISTER v4)))); Types.snd = pc };
1316                    Types.snd = (Nat.S Nat.O) }
1317                | Bool.False ->
1318                  let { Types.fst = b4; Types.snd = v5 } =
1319                    Vector.head (Nat.S (Nat.S Nat.O)) v4
1320                  in
1321                  (match b4 with
1322                   | Bool.True ->
1323                     let { Types.fst = b5; Types.snd = v6 } =
1324                       Vector.head (Nat.S Nat.O) v5
1325                     in
1326                     (match b5 with
1327                      | Bool.True ->
1328                        { Types.fst = { Types.fst = (ASM.RealInstruction
1329                          (ASM.ADDC (ASM.ACC_A, (ASM.INDIRECT
1330                          (Vector.from_singl v6))))); Types.snd = pc };
1331                          Types.snd = (Nat.S Nat.O) }
1332                      | Bool.False ->
1333                        let { Types.fst = b6; Types.snd = v7 } =
1334                          Vector.head Nat.O v6
1335                        in
1336                        (match b6 with
1337                         | Bool.True ->
1338                           prod_inv_rect_Type0 (ASM.next pmem pc)
1339                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1340                             (ASM.RealInstruction (ASM.ADDC (ASM.ACC_A,
1341                             (ASM.DIRECT b10)))); Types.snd = pc0 };
1342                             Types.snd = (Nat.S Nat.O) })
1343                         | Bool.False ->
1344                           prod_inv_rect_Type0 (ASM.next pmem pc)
1345                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1346                             (ASM.RealInstruction (ASM.ADDC (ASM.ACC_A,
1347                             (ASM.DATA b10)))); Types.snd = pc0 }; Types.snd =
1348                             (Nat.S Nat.O) })))
1349                   | Bool.False ->
1350                     let { Types.fst = b5; Types.snd = v6 } =
1351                       Vector.head (Nat.S Nat.O) v5
1352                     in
1353                     (match b5 with
1354                      | Bool.True ->
1355                        let { Types.fst = b6; Types.snd = v7 } =
1356                          Vector.head Nat.O v6
1357                        in
1358                        (match b6 with
1359                         | Bool.True ->
1360                           { Types.fst = { Types.fst = (ASM.RealInstruction
1361                             (ASM.RLC ASM.ACC_A)); Types.snd = pc };
1362                             Types.snd = (Nat.S Nat.O) }
1363                         | Bool.False ->
1364                           { Types.fst = { Types.fst = (ASM.RealInstruction
1365                             ASM.RETI); Types.snd = pc }; Types.snd = (Nat.S
1366                             (Nat.S Nat.O)) })
1367                      | Bool.False ->
1368                        let { Types.fst = b6; Types.snd = v7 } =
1369                          Vector.head Nat.O v6
1370                        in
1371                        (match b6 with
1372                         | Bool.True ->
1373                           prod_inv_rect_Type0 (ASM.next pmem pc)
1374                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1375                             (ASM.ACALL (ASM.ADDR11
1376                             (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
1377                               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1378                               (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
1379                               ((Nat.S (Nat.S Nat.O)), Bool.False,
1380                               (Vector.VCons ((Nat.S Nat.O), Bool.False,
1381                               (Vector.VCons (Nat.O, Bool.True,
1382                               Vector.VEmpty)))))) b10))); Types.snd = pc0 };
1383                             Types.snd = (Nat.S (Nat.S Nat.O)) })
1384                         | Bool.False ->
1385                           prod_inv_rect_Type0 (ASM.next pmem pc)
1386                             (fun pc0 b10 _ ->
1387                             prod_inv_rect_Type0 (ASM.next pmem pc0)
1388                               (fun pc1 b20 _ -> { Types.fst = { Types.fst =
1389                               (ASM.RealInstruction (ASM.JNB ((ASM.BIT_ADDR
1390                               b10), (ASM.RELATIVE b20)))); Types.snd = pc1 };
1391                               Types.snd = (Nat.S (Nat.S Nat.O)) }))))))
1392             | Bool.False ->
1393               let { Types.fst = b3; Types.snd = v4 } =
1394                 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
1395               in
1396               (match b3 with
1397                | Bool.True ->
1398                  { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.ADD
1399                    (ASM.ACC_A, (ASM.REGISTER v4)))); Types.snd = pc };
1400                    Types.snd = (Nat.S Nat.O) }
1401                | Bool.False ->
1402                  let { Types.fst = b4; Types.snd = v5 } =
1403                    Vector.head (Nat.S (Nat.S Nat.O)) v4
1404                  in
1405                  (match b4 with
1406                   | Bool.True ->
1407                     let { Types.fst = b5; Types.snd = v6 } =
1408                       Vector.head (Nat.S Nat.O) v5
1409                     in
1410                     (match b5 with
1411                      | Bool.True ->
1412                        { Types.fst = { Types.fst = (ASM.RealInstruction
1413                          (ASM.ADD (ASM.ACC_A, (ASM.INDIRECT
1414                          (Vector.from_singl v6))))); Types.snd = pc };
1415                          Types.snd = (Nat.S Nat.O) }
1416                      | Bool.False ->
1417                        let { Types.fst = b6; Types.snd = v7 } =
1418                          Vector.head Nat.O v6
1419                        in
1420                        (match b6 with
1421                         | Bool.True ->
1422                           prod_inv_rect_Type0 (ASM.next pmem pc)
1423                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1424                             (ASM.RealInstruction (ASM.ADD (ASM.ACC_A,
1425                             (ASM.DIRECT b10)))); Types.snd = pc0 };
1426                             Types.snd = (Nat.S Nat.O) })
1427                         | Bool.False ->
1428                           prod_inv_rect_Type0 (ASM.next pmem pc)
1429                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1430                             (ASM.RealInstruction (ASM.ADD (ASM.ACC_A,
1431                             (ASM.DATA b10)))); Types.snd = pc0 }; Types.snd =
1432                             (Nat.S Nat.O) })))
1433                   | Bool.False ->
1434                     let { Types.fst = b5; Types.snd = v6 } =
1435                       Vector.head (Nat.S Nat.O) v5
1436                     in
1437                     (match b5 with
1438                      | Bool.True ->
1439                        let { Types.fst = b6; Types.snd = v7 } =
1440                          Vector.head Nat.O v6
1441                        in
1442                        (match b6 with
1443                         | Bool.True ->
1444                           { Types.fst = { Types.fst = (ASM.RealInstruction
1445                             (ASM.RL ASM.ACC_A)); Types.snd = pc };
1446                             Types.snd = (Nat.S Nat.O) }
1447                         | Bool.False ->
1448                           { Types.fst = { Types.fst = (ASM.RealInstruction
1449                             ASM.RET); Types.snd = pc }; Types.snd = (Nat.S
1450                             (Nat.S Nat.O)) })
1451                      | Bool.False ->
1452                        let { Types.fst = b6; Types.snd = v7 } =
1453                          Vector.head Nat.O v6
1454                        in
1455                        (match b6 with
1456                         | Bool.True ->
1457                           prod_inv_rect_Type0 (ASM.next pmem pc)
1458                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1459                             (ASM.AJMP (ASM.ADDR11
1460                             (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
1461                               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1462                               (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
1463                               ((Nat.S (Nat.S Nat.O)), Bool.False,
1464                               (Vector.VCons ((Nat.S Nat.O), Bool.False,
1465                               (Vector.VCons (Nat.O, Bool.True,
1466                               Vector.VEmpty)))))) b10))); Types.snd = pc0 };
1467                             Types.snd = (Nat.S (Nat.S Nat.O)) })
1468                         | Bool.False ->
1469                           prod_inv_rect_Type0 (ASM.next pmem pc)
1470                             (fun pc0 b10 _ ->
1471                             prod_inv_rect_Type0 (ASM.next pmem pc0)
1472                               (fun pc1 b20 _ -> { Types.fst = { Types.fst =
1473                               (ASM.RealInstruction (ASM.JB ((ASM.BIT_ADDR
1474                               b10), (ASM.RELATIVE b20)))); Types.snd = pc1 };
1475                               Types.snd = (Nat.S (Nat.S Nat.O)) })))))))
1476          | Bool.False ->
1477            let { Types.fst = b2; Types.snd = v3 } =
1478              Vector.head (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) v2
1479            in
1480            (match b2 with
1481             | Bool.True ->
1482               let { Types.fst = b3; Types.snd = v4 } =
1483                 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
1484               in
1485               (match b3 with
1486                | Bool.True ->
1487                  { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.DEC
1488                    (ASM.REGISTER v4))); Types.snd = pc }; Types.snd = (Nat.S
1489                    Nat.O) }
1490                | Bool.False ->
1491                  let { Types.fst = b4; Types.snd = v5 } =
1492                    Vector.head (Nat.S (Nat.S Nat.O)) v4
1493                  in
1494                  (match b4 with
1495                   | Bool.True ->
1496                     let { Types.fst = b5; Types.snd = v6 } =
1497                       Vector.head (Nat.S Nat.O) v5
1498                     in
1499                     (match b5 with
1500                      | Bool.True ->
1501                        { Types.fst = { Types.fst = (ASM.RealInstruction
1502                          (ASM.DEC (ASM.INDIRECT (Vector.from_singl v6))));
1503                          Types.snd = pc }; Types.snd = (Nat.S Nat.O) }
1504                      | Bool.False ->
1505                        let { Types.fst = b6; Types.snd = v7 } =
1506                          Vector.head Nat.O v6
1507                        in
1508                        (match b6 with
1509                         | Bool.True ->
1510                           prod_inv_rect_Type0 (ASM.next pmem pc)
1511                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1512                             (ASM.RealInstruction (ASM.DEC (ASM.DIRECT b10)));
1513                             Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) })
1514                         | Bool.False ->
1515                           { Types.fst = { Types.fst = (ASM.RealInstruction
1516                             (ASM.DEC ASM.ACC_A)); Types.snd = pc };
1517                             Types.snd = (Nat.S Nat.O) }))
1518                   | Bool.False ->
1519                     let { Types.fst = b5; Types.snd = v6 } =
1520                       Vector.head (Nat.S Nat.O) v5
1521                     in
1522                     (match b5 with
1523                      | Bool.True ->
1524                        let { Types.fst = b6; Types.snd = v7 } =
1525                          Vector.head Nat.O v6
1526                        in
1527                        (match b6 with
1528                         | Bool.True ->
1529                           { Types.fst = { Types.fst = (ASM.RealInstruction
1530                             (ASM.RRC ASM.ACC_A)); Types.snd = pc };
1531                             Types.snd = (Nat.S Nat.O) }
1532                         | Bool.False ->
1533                           prod_inv_rect_Type0 (ASM.next pmem pc)
1534                             (fun pc0 b10 _ ->
1535                             prod_inv_rect_Type0 (ASM.next pmem pc0)
1536                               (fun pc1 b20 _ -> { Types.fst = { Types.fst =
1537                               (ASM.LCALL (ASM.ADDR16
1538                               (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S
1539                                 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
1540                                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1541                                 (Nat.S (Nat.S Nat.O)))))))) b10 b20)));
1542                               Types.snd = pc1 }; Types.snd = (Nat.S (Nat.S
1543                               Nat.O)) })))
1544                      | Bool.False ->
1545                        let { Types.fst = b6; Types.snd = v7 } =
1546                          Vector.head Nat.O v6
1547                        in
1548                        (match b6 with
1549                         | Bool.True ->
1550                           prod_inv_rect_Type0 (ASM.next pmem pc)
1551                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1552                             (ASM.ACALL (ASM.ADDR11
1553                             (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
1554                               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1555                               (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
1556                               ((Nat.S (Nat.S Nat.O)), Bool.False,
1557                               (Vector.VCons ((Nat.S Nat.O), Bool.False,
1558                               (Vector.VCons (Nat.O, Bool.False,
1559                               Vector.VEmpty)))))) b10))); Types.snd = pc0 };
1560                             Types.snd = (Nat.S (Nat.S Nat.O)) })
1561                         | Bool.False ->
1562                           prod_inv_rect_Type0 (ASM.next pmem pc)
1563                             (fun pc0 b10 _ ->
1564                             prod_inv_rect_Type0 (ASM.next pmem pc0)
1565                               (fun pc1 b20 _ -> { Types.fst = { Types.fst =
1566                               (ASM.RealInstruction (ASM.JBC ((ASM.BIT_ADDR
1567                               b10), (ASM.RELATIVE b20)))); Types.snd = pc1 };
1568                               Types.snd = (Nat.S (Nat.S Nat.O)) }))))))
1569             | Bool.False ->
1570               let { Types.fst = b3; Types.snd = v4 } =
1571                 Vector.head (Nat.S (Nat.S (Nat.S Nat.O))) v3
1572               in
1573               (match b3 with
1574                | Bool.True ->
1575                  { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.INC
1576                    (ASM.REGISTER v4))); Types.snd = pc }; Types.snd = (Nat.S
1577                    Nat.O) }
1578                | Bool.False ->
1579                  let { Types.fst = b4; Types.snd = v5 } =
1580                    Vector.head (Nat.S (Nat.S Nat.O)) v4
1581                  in
1582                  (match b4 with
1583                   | Bool.True ->
1584                     let { Types.fst = b5; Types.snd = v6 } =
1585                       Vector.head (Nat.S Nat.O) v5
1586                     in
1587                     (match b5 with
1588                      | Bool.True ->
1589                        { Types.fst = { Types.fst = (ASM.RealInstruction
1590                          (ASM.INC (ASM.INDIRECT (Vector.from_singl v6))));
1591                          Types.snd = pc }; Types.snd = (Nat.S Nat.O) }
1592                      | Bool.False ->
1593                        let { Types.fst = b6; Types.snd = v7 } =
1594                          Vector.head Nat.O v6
1595                        in
1596                        (match b6 with
1597                         | Bool.True ->
1598                           prod_inv_rect_Type0 (ASM.next pmem pc)
1599                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1600                             (ASM.RealInstruction (ASM.INC (ASM.DIRECT b10)));
1601                             Types.snd = pc0 }; Types.snd = (Nat.S Nat.O) })
1602                         | Bool.False ->
1603                           { Types.fst = { Types.fst = (ASM.RealInstruction
1604                             (ASM.INC ASM.ACC_A)); Types.snd = pc };
1605                             Types.snd = (Nat.S Nat.O) }))
1606                   | Bool.False ->
1607                     let { Types.fst = b5; Types.snd = v6 } =
1608                       Vector.head (Nat.S Nat.O) v5
1609                     in
1610                     (match b5 with
1611                      | Bool.True ->
1612                        let { Types.fst = b6; Types.snd = v7 } =
1613                          Vector.head Nat.O v6
1614                        in
1615                        (match b6 with
1616                         | Bool.True ->
1617                           { Types.fst = { Types.fst = (ASM.RealInstruction
1618                             (ASM.RR ASM.ACC_A)); Types.snd = pc };
1619                             Types.snd = (Nat.S Nat.O) }
1620                         | Bool.False ->
1621                           prod_inv_rect_Type0 (ASM.next pmem pc)
1622                             (fun pc0 b10 _ ->
1623                             prod_inv_rect_Type0 (ASM.next pmem pc0)
1624                               (fun pc1 b20 _ -> { Types.fst = { Types.fst =
1625                               (ASM.LJMP (ASM.ADDR16
1626                               (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S
1627                                 (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
1628                                 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1629                                 (Nat.S (Nat.S Nat.O)))))))) b10 b20)));
1630                               Types.snd = pc1 }; Types.snd = (Nat.S (Nat.S
1631                               Nat.O)) })))
1632                      | Bool.False ->
1633                        let { Types.fst = b6; Types.snd = v7 } =
1634                          Vector.head Nat.O v6
1635                        in
1636                        (match b6 with
1637                         | Bool.True ->
1638                           prod_inv_rect_Type0 (ASM.next pmem pc)
1639                             (fun pc0 b10 _ -> { Types.fst = { Types.fst =
1640                             (ASM.AJMP (ASM.ADDR11
1641                             (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
1642                               (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
1643                               (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
1644                               ((Nat.S (Nat.S Nat.O)), Bool.False,
1645                               (Vector.VCons ((Nat.S Nat.O), Bool.False,
1646                               (Vector.VCons (Nat.O, Bool.False,
1647                               Vector.VEmpty)))))) b10))); Types.snd = pc0 };
1648                             Types.snd = (Nat.S (Nat.S Nat.O)) })
1649                         | Bool.False ->
1650                           { Types.fst = { Types.fst = (ASM.RealInstruction
1651                             ASM.NOP); Types.snd = pc }; Types.snd = (Nat.S
1652                             Nat.O) }))))))))
1653
1654 (** val fetch :
1655     BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
1656     ((ASM.instruction, BitVector.word) Types.prod, Nat.nat) Types.prod **)
1657 let fetch pmem pc =
1658   let { Types.fst = word; Types.snd = byte } = ASM.next pmem pc in
1659   fetch0 pmem word byte
1660