extracted/fetch.ml

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