Changeset 2773 for extracted/fetch.ml


Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (8 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/fetch.ml

    r2743 r2773  
    11open Preamble
    22
     3open Exp
     4
     5open Setoids
     6
     7open Monad
     8
     9open Option
     10
    311open Extranat
    412
     
    1119open Russell
    1220
     21open Types
     22
    1323open List
    1424
     
    1929open Bool
    2030
     31open Hints_declaration
     32
     33open Core_notation
     34
     35open Pts
     36
     37open Logic
     38
    2139open Relations
    2240
     
    2543open BitVector
    2644
    27 open Hints_declaration
    28 
    29 open Core_notation
    30 
    31 open Pts
    32 
    33 open Logic
    34 
    35 open Types
     45open Arithmetic
    3646
    3747open BitVectorTrie
    3848
    39 open Exp
    40 
    41 open Arithmetic
    42 
    4349open String
    4450
     51open Integers
     52
     53open AST
     54
    4555open LabelledObjects
    4656
    47 open Integers
    48 
    49 open AST
     57open Proper
     58
     59open PositiveMap
     60
     61open Deqsets
     62
     63open ErrorMessages
     64
     65open PreIdentifiers
     66
     67open Errors
     68
     69open Extralib
     70
     71open Lists
     72
     73open Positive
     74
     75open Identifiers
    5076
    5177open CostLabel
    5278
    53 open Proper
    54 
    55 open PositiveMap
    56 
    57 open Deqsets
    58 
    59 open ErrorMessages
    60 
    61 open PreIdentifiers
    62 
    63 open Errors
    64 
    65 open Extralib
    66 
    67 open Setoids
    68 
    69 open Monad
    70 
    71 open Option
    72 
    73 open Lists
    74 
    75 open Positive
    76 
    77 open Identifiers
    78 
    7979open ASM
    8080
    8181(** val inefficient_address_of_word_labels_code_mem :
    82     ASM.labelled_instruction List.list -> ASM.identifier0 ->
     82    ASM.labelled_instruction List.list -> ASM.identifier ->
    8383    BitVector.bitVector **)
    8484let inefficient_address_of_word_labels_code_mem code_mem id =
     
    8686    (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    8787    Nat.O))))))))))))))))
    88     (LabelledObjects.index_of0
     88    (LabelledObjects.index_of
    8989      (LabelledObjects.instruction_matches_identifier PreIdentifiers.ASMTag
    9090        id) code_mem)
     
    9595    ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
    9696    BitVectorTrie.bitVectorTrie) Types.prod Types.sig0 **)
    97 let create_label_cost_map0 program0 =
     97let create_label_cost_map0 program =
    9898  (Types.pi1
    99     (FoldStuff.foldl_strong program0 (fun prefix0 x tl _ labels_costs_ppc ->
    100       (let { Types.fst = eta29042; Types.snd = ppc } =
     99    (FoldStuff.foldl_strong program (fun prefix x tl _ labels_costs_ppc ->
     100      (let { Types.fst = eta27870; Types.snd = ppc } =
    101101         Types.pi1 labels_costs_ppc
    102102       in
    103103      (fun _ ->
    104       (let { Types.fst = labels; Types.snd = costs } = eta29042 in
     104      (let { Types.fst = labels; Types.snd = costs } = eta27870 in
    105105      (fun _ ->
    106106      (let { Types.fst = label; Types.snd = instr } = x in
     
    138138    ASM.labelled_instruction List.list -> (label_map, CostLabel.costlabel
    139139    BitVectorTrie.bitVectorTrie) Types.prod **)
    140 let create_label_cost_map program0 =
    141   Types.pi1 (create_label_cost_map0 program0)
     140let create_label_cost_map program =
     141  Types.pi1 (create_label_cost_map0 program)
    142142
    143143(** val address_of_word_labels :
    144     ASM.labelled_instruction List.list -> ASM.identifier0 -> BitVector.word **)
     144    ASM.labelled_instruction List.list -> ASM.identifier -> BitVector.word **)
    145145let address_of_word_labels code_mem id =
    146146  let labels = (create_label_cost_map code_mem).Types.fst in
     
    151151
    152152(** val bitvector_max_nat : Nat.nat -> Nat.nat **)
    153 let bitvector_max_nat length0 =
    154   Exp.exp (Nat.S (Nat.S Nat.O)) length0
     153let bitvector_max_nat length =
     154  Exp.exp (Nat.S (Nat.S Nat.O)) length
    155155
    156156(** val code_memory_size : Nat.nat **)
     
    178178
    179179(** val load_code_memory0 :
    180     BitVector.byte List.list -> BitVector.byte BitVectorTrie.bitVectorTrie
    181     Types.sig0 **)
    182 let load_code_memory0 program0 =
     180    ASM.object_code -> BitVector.byte BitVectorTrie.bitVectorTrie Types.sig0 **)
     181let load_code_memory0 program =
    183182  (Types.pi1
    184     (FoldStuff.foldl_strong program0 (fun prefix0 v tl _ i_mem ->
    185       (let { Types.fst = i; Types.snd = mem1 } = Types.pi1 i_mem in
     183    (FoldStuff.foldl_strong program (fun prefix v tl _ i_mem ->
     184      (let { Types.fst = i; Types.snd = mem } = Types.pi1 i_mem in
    186185      (fun _ -> { Types.fst = (Nat.S i); Types.snd =
    187186      (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    190189        (Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    191190          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    192           (Nat.S (Nat.S Nat.O)))))))))))))))) i) v mem1) })) __)
    193       { Types.fst = Nat.O; Types.snd = (BitVectorTrie.Stub (Nat.S (Nat.S
     191          (Nat.S (Nat.S Nat.O)))))))))))))))) i) v mem) })) __) { Types.fst =
     192      Nat.O; Types.snd = (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S
    194193      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    195       (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))))))))) })).Types.snd
     194      (Nat.S (Nat.S Nat.O))))))))))))))))) })).Types.snd
    196195
    197196(** val load_code_memory :
    198     BitVector.byte List.list -> BitVector.byte BitVectorTrie.bitVectorTrie **)
    199 let load_code_memory program0 =
    200   Types.pi1 (load_code_memory0 program0)
    201 
    202 (** val prod_inv_rect_Type5 :
     197    ASM.object_code -> BitVector.byte BitVectorTrie.bitVectorTrie **)
     198let load_code_memory program =
     199  Types.pi1 (load_code_memory0 program)
     200
     201(** val prod_inv_rect_Type0 :
    203202    ('a1, 'a2) Types.prod -> ('a1 -> 'a2 -> __ -> 'a3) -> 'a3 **)
    204 let prod_inv_rect_Type5 clearme =
    205   let { Types.fst = fst0; Types.snd = snd0 } = clearme in
    206   (fun auto -> auto fst0 snd0 __)
     203let prod_inv_rect_Type0 clearme =
     204  let { Types.fst = fst; Types.snd = snd } = clearme in
     205  (fun auto -> auto fst snd __)
    207206
    208207(** val fetch0 :
     
    265264                       (match b6 with
    266265                        | Bool.True ->
    267                           prod_inv_rect_Type5 (next pmem pc)
     266                          prod_inv_rect_Type0 (next pmem pc)
    268267                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    269268                            (ASM.RealInstruction (ASM.MOV (Types.Inl
     
    292291                       (match b6 with
    293292                        | Bool.True ->
    294                           prod_inv_rect_Type5 (next pmem pc)
     293                          prod_inv_rect_Type0 (next pmem pc)
    295294                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    296295                            (ASM.ACALL (ASM.ADDR11
    297                             (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
     296                            (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
    298297                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    299298                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
     
    342341                       (match b6 with
    343342                        | Bool.True ->
    344                           prod_inv_rect_Type5 (next pmem pc)
     343                          prod_inv_rect_Type0 (next pmem pc)
    345344                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    346345                            (ASM.RealInstruction (ASM.MOV (Types.Inl
     
    370369                       (match b6 with
    371370                        | Bool.True ->
    372                           prod_inv_rect_Type5 (next pmem pc)
     371                          prod_inv_rect_Type0 (next pmem pc)
    373372                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    374373                            (ASM.AJMP (ASM.ADDR11
    375                             (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
     374                            (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
    376375                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    377376                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
     
    398397              (match b3 with
    399398               | Bool.True ->
    400                  prod_inv_rect_Type5 (next pmem pc) (fun pc0 b10 _ ->
     399                 prod_inv_rect_Type0 (next pmem pc) (fun pc0 b10 _ ->
    401400                   { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.DJNZ
    402401                   ((ASM.REGISTER v4), (ASM.RELATIVE b10)))); Types.snd =
     
    423422                       (match b6 with
    424423                        | Bool.True ->
    425                           prod_inv_rect_Type5 (next pmem pc)
     424                          prod_inv_rect_Type0 (next pmem pc)
    426425                            (fun pc0 b10 _ ->
    427                             prod_inv_rect_Type5 (next pmem pc0)
     426                            prod_inv_rect_Type0 (next pmem pc0)
    428427                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
    429428                              (ASM.RealInstruction (ASM.DJNZ ((ASM.DIRECT
     
    449448                            Types.snd = (Nat.S Nat.O) }
    450449                        | Bool.False ->
    451                           prod_inv_rect_Type5 (next pmem pc)
     450                          prod_inv_rect_Type0 (next pmem pc)
    452451                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    453452                            (ASM.RealInstruction (ASM.SETB (ASM.BIT_ADDR
     
    460459                       (match b6 with
    461460                        | Bool.True ->
    462                           prod_inv_rect_Type5 (next pmem pc)
     461                          prod_inv_rect_Type0 (next pmem pc)
    463462                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    464463                            (ASM.ACALL (ASM.ADDR11
    465                             (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
     464                            (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
    466465                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    467466                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
     
    472471                            Types.snd = (Nat.S (Nat.S Nat.O)) })
    473472                        | Bool.False ->
    474                           prod_inv_rect_Type5 (next pmem pc)
     473                          prod_inv_rect_Type0 (next pmem pc)
    475474                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    476475                            (ASM.RealInstruction (ASM.POP (ASM.DIRECT b10)));
     
    507506                       (match b6 with
    508507                        | Bool.True ->
    509                           prod_inv_rect_Type5 (next pmem pc)
     508                          prod_inv_rect_Type0 (next pmem pc)
    510509                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    511510                            (ASM.RealInstruction (ASM.XCH (ASM.ACC_A,
     
    531530                            Types.snd = (Nat.S Nat.O) }
    532531                        | Bool.False ->
    533                           prod_inv_rect_Type5 (next pmem pc)
     532                          prod_inv_rect_Type0 (next pmem pc)
    534533                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    535534                            (ASM.RealInstruction (ASM.CLR (ASM.BIT_ADDR
     
    542541                       (match b6 with
    543542                        | Bool.True ->
    544                           prod_inv_rect_Type5 (next pmem pc)
     543                          prod_inv_rect_Type0 (next pmem pc)
    545544                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    546545                            (ASM.AJMP (ASM.ADDR11
    547                             (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
     546                            (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
    548547                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    549548                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
     
    554553                            Types.snd = (Nat.S (Nat.S Nat.O)) })
    555554                        | Bool.False ->
    556                           prod_inv_rect_Type5 (next pmem pc)
     555                          prod_inv_rect_Type0 (next pmem pc)
    557556                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    558557                            (ASM.RealInstruction (ASM.PUSH (ASM.DIRECT
     
    575574              (match b3 with
    576575               | Bool.True ->
    577                  prod_inv_rect_Type5 (next pmem pc) (fun pc0 b10 _ ->
    578                    prod_inv_rect_Type5 (next pmem pc0) (fun pc1 b20 _ ->
     576                 prod_inv_rect_Type0 (next pmem pc) (fun pc0 b10 _ ->
     577                   prod_inv_rect_Type0 (next pmem pc0) (fun pc1 b20 _ ->
    579578                     { Types.fst = { Types.fst = (ASM.RealInstruction
    580579                     (ASM.CJNE ((Types.Inr { Types.fst = (ASM.REGISTER v4);
     
    592591                    (match b5 with
    593592                     | Bool.True ->
    594                        prod_inv_rect_Type5 (next pmem pc) (fun pc0 b10 _ ->
    595                          prod_inv_rect_Type5 (next pmem pc0)
     593                       prod_inv_rect_Type0 (next pmem pc) (fun pc0 b10 _ ->
     594                         prod_inv_rect_Type0 (next pmem pc0)
    596595                           (fun pc1 b20 _ -> { Types.fst = { Types.fst =
    597596                           (ASM.RealInstruction (ASM.CJNE ((Types.Inr
     
    606605                       (match b6 with
    607606                        | Bool.True ->
    608                           prod_inv_rect_Type5 (next pmem pc)
     607                          prod_inv_rect_Type0 (next pmem pc)
    609608                            (fun pc0 b10 _ ->
    610                             prod_inv_rect_Type5 (next pmem pc0)
     609                            prod_inv_rect_Type0 (next pmem pc0)
    611610                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
    612611                              (ASM.RealInstruction (ASM.CJNE ((Types.Inl
     
    616615                              Nat.O)) }))
    617616                        | Bool.False ->
    618                           prod_inv_rect_Type5 (next pmem pc)
     617                          prod_inv_rect_Type0 (next pmem pc)
    619618                            (fun pc0 b10 _ ->
    620                             prod_inv_rect_Type5 (next pmem pc0)
     619                            prod_inv_rect_Type0 (next pmem pc0)
    621620                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
    622621                              (ASM.RealInstruction (ASM.CJNE ((Types.Inl
     
    639638                            Types.snd = (Nat.S Nat.O) }
    640639                        | Bool.False ->
    641                           prod_inv_rect_Type5 (next pmem pc)
     640                          prod_inv_rect_Type0 (next pmem pc)
    642641                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    643642                            (ASM.RealInstruction (ASM.CPL (ASM.BIT_ADDR
     
    650649                       (match b6 with
    651650                        | Bool.True ->
    652                           prod_inv_rect_Type5 (next pmem pc)
     651                          prod_inv_rect_Type0 (next pmem pc)
    653652                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    654653                            (ASM.ACALL (ASM.ADDR11
    655                             (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
     654                            (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
    656655                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    657656                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
     
    662661                            Types.snd = (Nat.S (Nat.S Nat.O)) })
    663662                        | Bool.False ->
    664                           prod_inv_rect_Type5 (next pmem pc)
     663                          prod_inv_rect_Type0 (next pmem pc)
    665664                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    666665                            (ASM.RealInstruction (ASM.ANL (Types.Inr
     
    674673              (match b3 with
    675674               | Bool.True ->
    676                  prod_inv_rect_Type5 (next pmem pc) (fun pc0 b10 _ ->
     675                 prod_inv_rect_Type0 (next pmem pc) (fun pc0 b10 _ ->
    677676                   { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV
    678677                   (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr
     
    691690                    (match b5 with
    692691                     | Bool.True ->
    693                        prod_inv_rect_Type5 (next pmem pc) (fun pc0 b10 _ ->
     692                       prod_inv_rect_Type0 (next pmem pc) (fun pc0 b10 _ ->
    694693                         { Types.fst = { Types.fst = (ASM.RealInstruction
    695694                         (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl
     
    717716                            Types.snd = (Nat.S (Nat.S Nat.O)) }
    718717                        | Bool.False ->
    719                           prod_inv_rect_Type5 (next pmem pc)
     718                          prod_inv_rect_Type0 (next pmem pc)
    720719                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    721720                            (ASM.RealInstruction (ASM.MOV (Types.Inl
     
    729728                       (match b6 with
    730729                        | Bool.True ->
    731                           prod_inv_rect_Type5 (next pmem pc)
     730                          prod_inv_rect_Type0 (next pmem pc)
    732731                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    733732                            (ASM.AJMP (ASM.ADDR11
    734                             (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
     733                            (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
    735734                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    736735                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
     
    741740                            Types.snd = (Nat.S (Nat.S Nat.O)) })
    742741                        | Bool.False ->
    743                           prod_inv_rect_Type5 (next pmem pc)
     742                          prod_inv_rect_Type0 (next pmem pc)
    744743                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    745744                            (ASM.RealInstruction (ASM.ORL (Types.Inr
     
    782781                       (match b6 with
    783782                        | Bool.True ->
    784                           prod_inv_rect_Type5 (next pmem pc)
     783                          prod_inv_rect_Type0 (next pmem pc)
    785784                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    786785                            (ASM.RealInstruction (ASM.SUBB (ASM.ACC_A,
     
    788787                            Types.snd = (Nat.S Nat.O) })
    789788                        | Bool.False ->
    790                           prod_inv_rect_Type5 (next pmem pc)
     789                          prod_inv_rect_Type0 (next pmem pc)
    791790                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    792791                            (ASM.RealInstruction (ASM.SUBB (ASM.ACC_A,
     
    808807                            (Nat.S (Nat.S Nat.O)) }
    809808                        | Bool.False ->
    810                           prod_inv_rect_Type5 (next pmem pc)
     809                          prod_inv_rect_Type0 (next pmem pc)
    811810                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    812811                            (ASM.RealInstruction (ASM.MOV (Types.Inr
     
    820819                       (match b6 with
    821820                        | Bool.True ->
    822                           prod_inv_rect_Type5 (next pmem pc)
     821                          prod_inv_rect_Type0 (next pmem pc)
    823822                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    824823                            (ASM.ACALL (ASM.ADDR11
    825                             (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
     824                            (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
    826825                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    827826                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
     
    832831                            Types.snd = (Nat.S (Nat.S Nat.O)) })
    833832                        | Bool.False ->
    834                           prod_inv_rect_Type5 (next pmem pc)
     833                          prod_inv_rect_Type0 (next pmem pc)
    835834                            (fun pc0 b10 _ ->
    836                             prod_inv_rect_Type5 (next pmem pc0)
     835                            prod_inv_rect_Type0 (next pmem pc0)
    837836                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
    838837                              (ASM.RealInstruction (ASM.MOV (Types.Inl
    839838                              (Types.Inl (Types.Inr { Types.fst = ASM.DPTR;
    840839                              Types.snd = (ASM.DATA16
    841                               (Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S
     840                              (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S
    842841                                (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
    843842                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    851850              (match b3 with
    852851               | Bool.True ->
    853                  prod_inv_rect_Type5 (next pmem pc) (fun pc0 b10 _ ->
     852                 prod_inv_rect_Type0 (next pmem pc) (fun pc0 b10 _ ->
    854853                   { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV
    855854                   (Types.Inl (Types.Inl (Types.Inl (Types.Inr { Types.fst =
     
    867866                    (match b5 with
    868867                     | Bool.True ->
    869                        prod_inv_rect_Type5 (next pmem pc) (fun pc0 b10 _ ->
     868                       prod_inv_rect_Type0 (next pmem pc) (fun pc0 b10 _ ->
    870869                         { Types.fst = { Types.fst = (ASM.RealInstruction
    871870                         (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inr
     
    880879                       (match b6 with
    881880                        | Bool.True ->
    882                           prod_inv_rect_Type5 (next pmem pc)
     881                          prod_inv_rect_Type0 (next pmem pc)
    883882                            (fun pc0 b10 _ ->
    884                             prod_inv_rect_Type5 (next pmem pc0)
     883                            prod_inv_rect_Type0 (next pmem pc0)
    885884                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
    886885                              (ASM.RealInstruction (ASM.MOV (Types.Inl
     
    909908                            (Nat.S (Nat.S Nat.O)) }
    910909                        | Bool.False ->
    911                           prod_inv_rect_Type5 (next pmem pc)
     910                          prod_inv_rect_Type0 (next pmem pc)
    912911                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    913912                            (ASM.RealInstruction (ASM.ANL (Types.Inr
     
    921920                       (match b6 with
    922921                        | Bool.True ->
    923                           prod_inv_rect_Type5 (next pmem pc)
     922                          prod_inv_rect_Type0 (next pmem pc)
    924923                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    925924                            (ASM.AJMP (ASM.ADDR11
    926                             (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
     925                            (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
    927926                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    928927                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
     
    933932                            Types.snd = (Nat.S (Nat.S Nat.O)) })
    934933                        | Bool.False ->
    935                           prod_inv_rect_Type5 (next pmem pc)
     934                          prod_inv_rect_Type0 (next pmem pc)
    936935                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    937936                            (ASM.SJMP (ASM.RELATIVE b10)); Types.snd = pc0 };
     
    958957              (match b3 with
    959958               | Bool.True ->
    960                  prod_inv_rect_Type5 (next pmem pc) (fun pc0 b10 _ ->
     959                 prod_inv_rect_Type0 (next pmem pc) (fun pc0 b10 _ ->
    961960                   { Types.fst = { Types.fst = (ASM.RealInstruction (ASM.MOV
    962961                   (Types.Inl (Types.Inl (Types.Inl (Types.Inl (Types.Inr
     
    975974                    (match b5 with
    976975                     | Bool.True ->
    977                        prod_inv_rect_Type5 (next pmem pc) (fun pc0 b10 _ ->
     976                       prod_inv_rect_Type0 (next pmem pc) (fun pc0 b10 _ ->
    978977                         { Types.fst = { Types.fst = (ASM.RealInstruction
    979978                         (ASM.MOV (Types.Inl (Types.Inl (Types.Inl (Types.Inl
     
    988987                       (match b6 with
    989988                        | Bool.True ->
    990                           prod_inv_rect_Type5 (next pmem pc)
     989                          prod_inv_rect_Type0 (next pmem pc)
    991990                            (fun pc0 b10 _ ->
    992                             prod_inv_rect_Type5 (next pmem pc0)
     991                            prod_inv_rect_Type0 (next pmem pc0)
    993992                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
    994993                              (ASM.RealInstruction (ASM.MOV (Types.Inl
     
    998997                              (Nat.S (Nat.S (Nat.S Nat.O))) }))
    999998                        | Bool.False ->
    1000                           prod_inv_rect_Type5 (next pmem pc)
     999                          prod_inv_rect_Type0 (next pmem pc)
    10011000                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    10021001                            (ASM.RealInstruction (ASM.MOV (Types.Inl
     
    10201019                            Types.snd = (Nat.S (Nat.S Nat.O)) }
    10211020                        | Bool.False ->
    1022                           prod_inv_rect_Type5 (next pmem pc)
     1021                          prod_inv_rect_Type0 (next pmem pc)
    10231022                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    10241023                            (ASM.RealInstruction (ASM.ORL (Types.Inr
     
    10321031                       (match b6 with
    10331032                        | Bool.True ->
    1034                           prod_inv_rect_Type5 (next pmem pc)
     1033                          prod_inv_rect_Type0 (next pmem pc)
    10351034                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    10361035                            (ASM.ACALL (ASM.ADDR11
    1037                             (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
     1036                            (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
    10381037                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    10391038                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
     
    10441043                            Types.snd = (Nat.S (Nat.S Nat.O)) })
    10451044                        | Bool.False ->
    1046                           prod_inv_rect_Type5 (next pmem pc)
     1045                          prod_inv_rect_Type0 (next pmem pc)
    10471046                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    10481047                            (ASM.RealInstruction (ASM.JNZ (ASM.RELATIVE
     
    10811080                       (match b6 with
    10821081                        | Bool.True ->
    1083                           prod_inv_rect_Type5 (next pmem pc)
     1082                          prod_inv_rect_Type0 (next pmem pc)
    10841083                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    10851084                            (ASM.RealInstruction (ASM.XRL (Types.Inl
     
    10881087                            Nat.O) })
    10891088                        | Bool.False ->
    1090                           prod_inv_rect_Type5 (next pmem pc)
     1089                          prod_inv_rect_Type0 (next pmem pc)
    10911090                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    10921091                            (ASM.RealInstruction (ASM.XRL (Types.Inl
     
    11051104                       (match b6 with
    11061105                        | Bool.True ->
    1107                           prod_inv_rect_Type5 (next pmem pc)
     1106                          prod_inv_rect_Type0 (next pmem pc)
    11081107                            (fun pc0 b10 _ ->
    1109                             prod_inv_rect_Type5 (next pmem pc0)
     1108                            prod_inv_rect_Type0 (next pmem pc0)
    11101109                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
    11111110                              (ASM.RealInstruction (ASM.XRL (Types.Inr
     
    11141113                              Types.snd = (Nat.S (Nat.S Nat.O)) }))
    11151114                        | Bool.False ->
    1116                           prod_inv_rect_Type5 (next pmem pc)
     1115                          prod_inv_rect_Type0 (next pmem pc)
    11171116                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    11181117                            (ASM.RealInstruction (ASM.XRL (Types.Inr
     
    11261125                       (match b6 with
    11271126                        | Bool.True ->
    1128                           prod_inv_rect_Type5 (next pmem pc)
     1127                          prod_inv_rect_Type0 (next pmem pc)
    11291128                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    11301129                            (ASM.AJMP (ASM.ADDR11
    1131                             (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
     1130                            (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
    11321131                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    11331132                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
     
    11381137                            Types.snd = (Nat.S (Nat.S Nat.O)) })
    11391138                        | Bool.False ->
    1140                           prod_inv_rect_Type5 (next pmem pc)
     1139                          prod_inv_rect_Type0 (next pmem pc)
    11411140                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    11421141                            (ASM.RealInstruction (ASM.JZ (ASM.RELATIVE
     
    11801179                       (match b6 with
    11811180                        | Bool.True ->
    1182                           prod_inv_rect_Type5 (next pmem pc)
     1181                          prod_inv_rect_Type0 (next pmem pc)
    11831182                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    11841183                            (ASM.RealInstruction (ASM.ANL (Types.Inl
     
    11871186                            Types.snd = (Nat.S Nat.O) })
    11881187                        | Bool.False ->
    1189                           prod_inv_rect_Type5 (next pmem pc)
     1188                          prod_inv_rect_Type0 (next pmem pc)
    11901189                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    11911190                            (ASM.RealInstruction (ASM.ANL (Types.Inl
     
    12041203                       (match b6 with
    12051204                        | Bool.True ->
    1206                           prod_inv_rect_Type5 (next pmem pc)
     1205                          prod_inv_rect_Type0 (next pmem pc)
    12071206                            (fun pc0 b10 _ ->
    1208                             prod_inv_rect_Type5 (next pmem pc0)
     1207                            prod_inv_rect_Type0 (next pmem pc0)
    12091208                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
    12101209                              (ASM.RealInstruction (ASM.ANL (Types.Inl
     
    12131212                              pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) }))
    12141213                        | Bool.False ->
    1215                           prod_inv_rect_Type5 (next pmem pc)
     1214                          prod_inv_rect_Type0 (next pmem pc)
    12161215                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    12171216                            (ASM.RealInstruction (ASM.ANL (Types.Inl
     
    12251224                       (match b6 with
    12261225                        | Bool.True ->
    1227                           prod_inv_rect_Type5 (next pmem pc)
     1226                          prod_inv_rect_Type0 (next pmem pc)
    12281227                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    12291228                            (ASM.ACALL (ASM.ADDR11
    1230                             (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
     1229                            (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
    12311230                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    12321231                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
     
    12371236                            Types.snd = (Nat.S (Nat.S Nat.O)) })
    12381237                        | Bool.False ->
    1239                           prod_inv_rect_Type5 (next pmem pc)
     1238                          prod_inv_rect_Type0 (next pmem pc)
    12401239                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    12411240                            (ASM.RealInstruction (ASM.JNC (ASM.RELATIVE
     
    12741273                       (match b6 with
    12751274                        | Bool.True ->
    1276                           prod_inv_rect_Type5 (next pmem pc)
     1275                          prod_inv_rect_Type0 (next pmem pc)
    12771276                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    12781277                            (ASM.RealInstruction (ASM.ORL (Types.Inl
     
    12811280                            Types.snd = (Nat.S Nat.O) })
    12821281                        | Bool.False ->
    1283                           prod_inv_rect_Type5 (next pmem pc)
     1282                          prod_inv_rect_Type0 (next pmem pc)
    12841283                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    12851284                            (ASM.RealInstruction (ASM.ORL (Types.Inl
     
    12981297                       (match b6 with
    12991298                        | Bool.True ->
    1300                           prod_inv_rect_Type5 (next pmem pc)
     1299                          prod_inv_rect_Type0 (next pmem pc)
    13011300                            (fun pc0 b10 _ ->
    1302                             prod_inv_rect_Type5 (next pmem pc0)
     1301                            prod_inv_rect_Type0 (next pmem pc0)
    13031302                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
    13041303                              (ASM.RealInstruction (ASM.ORL (Types.Inl
     
    13071306                              pc1 }; Types.snd = (Nat.S (Nat.S Nat.O)) }))
    13081307                        | Bool.False ->
    1309                           prod_inv_rect_Type5 (next pmem pc)
     1308                          prod_inv_rect_Type0 (next pmem pc)
    13101309                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    13111310                            (ASM.RealInstruction (ASM.ORL (Types.Inl
     
    13191318                       (match b6 with
    13201319                        | Bool.True ->
    1321                           prod_inv_rect_Type5 (next pmem pc)
     1320                          prod_inv_rect_Type0 (next pmem pc)
    13221321                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    13231322                            (ASM.AJMP (ASM.ADDR11
    1324                             (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
     1323                            (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
    13251324                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    13261325                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
     
    13311330                            Types.snd = (Nat.S (Nat.S Nat.O)) })
    13321331                        | Bool.False ->
    1333                           prod_inv_rect_Type5 (next pmem pc)
     1332                          prod_inv_rect_Type0 (next pmem pc)
    13341333                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    13351334                            (ASM.RealInstruction (ASM.JC (ASM.RELATIVE
     
    13761375                       (match b6 with
    13771376                        | Bool.True ->
    1378                           prod_inv_rect_Type5 (next pmem pc)
     1377                          prod_inv_rect_Type0 (next pmem pc)
    13791378                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    13801379                            (ASM.RealInstruction (ASM.ADDC (ASM.ACC_A,
     
    13821381                            Types.snd = (Nat.S Nat.O) })
    13831382                        | Bool.False ->
    1384                           prod_inv_rect_Type5 (next pmem pc)
     1383                          prod_inv_rect_Type0 (next pmem pc)
    13851384                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    13861385                            (ASM.RealInstruction (ASM.ADDC (ASM.ACC_A,
     
    14111410                       (match b6 with
    14121411                        | Bool.True ->
    1413                           prod_inv_rect_Type5 (next pmem pc)
     1412                          prod_inv_rect_Type0 (next pmem pc)
    14141413                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    14151414                            (ASM.ACALL (ASM.ADDR11
    1416                             (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
     1415                            (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
    14171416                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    14181417                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
     
    14231422                            Types.snd = (Nat.S (Nat.S Nat.O)) })
    14241423                        | Bool.False ->
    1425                           prod_inv_rect_Type5 (next pmem pc)
     1424                          prod_inv_rect_Type0 (next pmem pc)
    14261425                            (fun pc0 b10 _ ->
    1427                             prod_inv_rect_Type5 (next pmem pc0)
     1426                            prod_inv_rect_Type0 (next pmem pc0)
    14281427                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
    14291428                              (ASM.RealInstruction (ASM.JNB ((ASM.BIT_ADDR
     
    14601459                       (match b6 with
    14611460                        | Bool.True ->
    1462                           prod_inv_rect_Type5 (next pmem pc)
     1461                          prod_inv_rect_Type0 (next pmem pc)
    14631462                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    14641463                            (ASM.RealInstruction (ASM.ADD (ASM.ACC_A,
     
    14661465                            Types.snd = (Nat.S Nat.O) })
    14671466                        | Bool.False ->
    1468                           prod_inv_rect_Type5 (next pmem pc)
     1467                          prod_inv_rect_Type0 (next pmem pc)
    14691468                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    14701469                            (ASM.RealInstruction (ASM.ADD (ASM.ACC_A,
     
    14951494                       (match b6 with
    14961495                        | Bool.True ->
    1497                           prod_inv_rect_Type5 (next pmem pc)
     1496                          prod_inv_rect_Type0 (next pmem pc)
    14981497                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    14991498                            (ASM.AJMP (ASM.ADDR11
    1500                             (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
     1499                            (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
    15011500                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    15021501                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
     
    15071506                            Types.snd = (Nat.S (Nat.S Nat.O)) })
    15081507                        | Bool.False ->
    1509                           prod_inv_rect_Type5 (next pmem pc)
     1508                          prod_inv_rect_Type0 (next pmem pc)
    15101509                            (fun pc0 b10 _ ->
    1511                             prod_inv_rect_Type5 (next pmem pc0)
     1510                            prod_inv_rect_Type0 (next pmem pc0)
    15121511                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
    15131512                              (ASM.RealInstruction (ASM.JB ((ASM.BIT_ADDR
     
    15481547                       (match b6 with
    15491548                        | Bool.True ->
    1550                           prod_inv_rect_Type5 (next pmem pc)
     1549                          prod_inv_rect_Type0 (next pmem pc)
    15511550                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    15521551                            (ASM.RealInstruction (ASM.DEC (ASM.DIRECT b10)));
     
    15711570                            Types.snd = (Nat.S Nat.O) }
    15721571                        | Bool.False ->
    1573                           prod_inv_rect_Type5 (next pmem pc)
     1572                          prod_inv_rect_Type0 (next pmem pc)
    15741573                            (fun pc0 b10 _ ->
    1575                             prod_inv_rect_Type5 (next pmem pc0)
     1574                            prod_inv_rect_Type0 (next pmem pc0)
    15761575                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
    15771576                              (ASM.LCALL (ASM.ADDR16
    1578                               (Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S
     1577                              (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S
    15791578                                (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
    15801579                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    15881587                       (match b6 with
    15891588                        | Bool.True ->
    1590                           prod_inv_rect_Type5 (next pmem pc)
     1589                          prod_inv_rect_Type0 (next pmem pc)
    15911590                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    15921591                            (ASM.ACALL (ASM.ADDR11
    1593                             (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
     1592                            (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
    15941593                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    15951594                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
     
    16001599                            Types.snd = (Nat.S (Nat.S Nat.O)) })
    16011600                        | Bool.False ->
    1602                           prod_inv_rect_Type5 (next pmem pc)
     1601                          prod_inv_rect_Type0 (next pmem pc)
    16031602                            (fun pc0 b10 _ ->
    1604                             prod_inv_rect_Type5 (next pmem pc0)
     1603                            prod_inv_rect_Type0 (next pmem pc0)
    16051604                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
    16061605                              (ASM.RealInstruction (ASM.JBC ((ASM.BIT_ADDR
     
    16361635                       (match b6 with
    16371636                        | Bool.True ->
    1638                           prod_inv_rect_Type5 (next pmem pc)
     1637                          prod_inv_rect_Type0 (next pmem pc)
    16391638                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    16401639                            (ASM.RealInstruction (ASM.INC (ASM.DIRECT b10)));
     
    16591658                            Types.snd = (Nat.S Nat.O) }
    16601659                        | Bool.False ->
    1661                           prod_inv_rect_Type5 (next pmem pc)
     1660                          prod_inv_rect_Type0 (next pmem pc)
    16621661                            (fun pc0 b10 _ ->
    1663                             prod_inv_rect_Type5 (next pmem pc0)
     1662                            prod_inv_rect_Type0 (next pmem pc0)
    16641663                              (fun pc1 b20 _ -> { Types.fst = { Types.fst =
    16651664                              (ASM.LJMP (ASM.ADDR16
    1666                               (Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S
     1665                              (Vector.append (Nat.S (Nat.S (Nat.S (Nat.S
    16671666                                (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))
    16681667                                (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     
    16761675                       (match b6 with
    16771676                        | Bool.True ->
    1678                           prod_inv_rect_Type5 (next pmem pc)
     1677                          prod_inv_rect_Type0 (next pmem pc)
    16791678                            (fun pc0 b10 _ -> { Types.fst = { Types.fst =
    16801679                            (ASM.AJMP (ASM.ADDR11
    1681                             (Vector.append0 (Nat.S (Nat.S (Nat.S Nat.O)))
     1680                            (Vector.append (Nat.S (Nat.S (Nat.S Nat.O)))
    16821681                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    16831682                              (Nat.S (Nat.S Nat.O)))))))) (Vector.VCons
     
    16961695    ((ASM.instruction, BitVector.word) Types.prod, Nat.nat) Types.prod **)
    16971696let fetch pmem pc =
    1698   let { Types.fst = word0; Types.snd = byte0 } = next pmem pc in
    1699   fetch0 pmem word0 byte0
    1700 
     1697  let { Types.fst = word; Types.snd = byte } = next pmem pc in
     1698  fetch0 pmem word byte
     1699
Note: See TracChangeset for help on using the changeset viewer.