Changeset 322


Ignore:
Timestamp:
Nov 26, 2010, 9:35:28 PM (9 years ago)
Author:
sacerdot
Message:

More work on fetch.

Location:
Deliverables/D4.1/Matita
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Fetch.ma

    r319 r322  
    2121     〈〈AJMP … (ADDR11 (v1 @@ b1)), pc〉, two〉
    2222   else
    23    let 〈b,v〉≝ head8 v in if b then
    24     let 〈b,v〉≝ head8 v in if b then
    25      let 〈b,v〉≝ head8 v in if b then
    26       let 〈b,v〉≝ head8 v in if b then
    27        let 〈b,v〉≝ head8 v in if b then
    28         〈〈MOV (U2 (REGISTER v) ACC_A), pc〉, one〉
    29        else
    30         let 〈b,v〉≝ head8 v in if b then
    31          let 〈b,v〉≝ head8 v in if b then
    32           〈〈MOV (U2 (INDIRECT v) ACC_A), pc〉, one〉
    33          else
    34           let 〈b,v〉≝ head8 v in if b then
     23   let 〈b,v〉≝  head … v in if b then
     24    let 〈b,v〉≝  head … v in if b then
     25     let 〈b,v〉≝  head … v in if b then
     26      let 〈b,v〉≝  head … v in if b then
     27       let 〈b,v〉≝  head … v in if b then
     28        〈〈MOV ? ((Left ?? (Left ?? (Left ?? (Left ?? (Right ?? (? 〈REGISTER v,ACC_A〉))))))), pc〉, one〉
     29       else
     30        let 〈b,v〉≝  head … v in if b then
     31         let 〈b,v〉≝  head … v in if b then
     32          〈〈MOV (U2 (INDIRECT (from_singl … v)) ACC_A), pc〉, one〉
     33         else
     34          let 〈b,v〉≝  head … v in if b then
    3535           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U3 (DIRECT b1) ACC_A), pc〉, one〉
    3636          else
    3737           〈〈CPL ACC_A, pc〉, one〉
    3838        else
    39          let 〈b,v〉≝ head8 v in if b then
     39         let 〈b,v〉≝  head … v in if b then
    4040          〈〈MOVX (U2 (EXT_INDIRECT v) ACC_A), pc〉, two〉
    4141         else
    42           let 〈b,v〉≝ head8 v in if b then
    43            assert false
     42          let 〈b,v〉≝  head … v in if b then
     43            ⊥
    4444          else
    4545           〈〈MOVX (U2 (EXT_IND_DPTR) ACC_A), pc〉, two〉
    4646      else
    47        let 〈b,v〉≝ head8 v in if b then
    48         〈〈MOV (U1 A (REGISTER v)), pc〉, one〉
    49        else
    50         let 〈b,v〉≝ head8 v in if b then
    51          let 〈b,v〉≝ head8 v in if b then
     47       let 〈b,v〉≝  head … v in if b then
     48        〈〈MOV (Left … (Left … (Left … (Left … (Left … (Left … 〈ACC_A,REGISTER v〉)))))), pc〉, one〉
     49       else
     50        let 〈b,v〉≝  head … v in if b then
     51         let 〈b,v〉≝  head … v in if b then
    5252          〈〈MOV (U1 A (INDIRECT v)), pc〉, one〉
    5353         else
    54           let 〈b,v〉≝ head8 v in if b then
     54          let 〈b,v〉≝  head … v in if b then
    5555           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U1 A (DIRECT b1)), pc〉, one〉
    5656          else
    5757           〈〈CLR ACC_A, pc〉, one〉
    5858        else
    59          let 〈b,v〉≝ head8 v in if b then
     59         let 〈b,v〉≝  head … v in if b then
    6060          〈〈MOVX (U1 A (EXT_INDIRECT v)), pc〉, two〉
    6161         else
    62           let 〈b,v〉≝ head8 v in if b then
    63            assert false
     62          let 〈b,v〉≝  head … v in if b then
     63            ⊥
    6464          else
    6565           〈〈MOVX (U1 A EXT_IND_DPTR), pc〉, two〉
    6666     else
    67       let 〈b,v〉≝ head8 v in if b then
    68        let 〈b,v〉≝ head8 v in if b then
    69         let 〈pc,b1〉≝ next pmem pc in 〈〈DJNZ (REGISTER v) (REL b1), pc〉, two〉
    70        else
    71         let 〈b,v〉≝ head8 v in if b then
    72          let 〈b,v〉≝ head8 v in if b then
     67      let 〈b,v〉≝  head … v in if b then
     68       let 〈b,v〉≝  head … v in if b then
     69        let 〈pc,b1〉≝ next pmem pc in 〈〈DJNZ (REGISTER v) (RELATIVE b1), pc〉, two〉
     70       else
     71        let 〈b,v〉≝  head … v in if b then
     72         let 〈b,v〉≝  head … v in if b then
    7373          〈〈XCHD A INDIRECT v, pc〉, one〉
    7474         else
    75           let 〈b,v〉≝ head8 v in if b then
     75          let 〈b,v〉≝  head … v in if b then
    7676           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈DJNZ (DIRECT b1) (REL b2), pc〉, two〉
    7777          else
    7878           〈〈DA ACC_A, pc〉, one〉
    7979        else
    80          let 〈b,v〉≝ head8 v in if b then
    81           let 〈b,v〉≝ head8 v in if b then
     80         let 〈b,v〉≝  head … v in if b then
     81          let 〈b,v〉≝  head … v in if b then
    8282           〈〈SETB C, pc〉, one〉
    8383          else
    8484           let 〈pc,b1〉≝ next pmem pc in 〈〈SETB (BIT b1), pc〉, one〉
    8585         else
    86           let 〈b,v〉≝ head8 v in if b then
    87            assert false
     86          let 〈b,v〉≝  head … v in if b then
     87            ⊥
    8888          else
    8989           let 〈pc,b1〉≝ next pmem pc in 〈〈POP (DIRECT b1), pc〉, two〉
    9090      else
    91        let 〈b,v〉≝ head8 v in if b then
     91       let 〈b,v〉≝  head … v in if b then
    9292        〈〈XCH A (REGISTER v), pc〉, one〉
    9393       else
    94         let 〈b,v〉≝ head8 v in if b then
    95          let 〈b,v〉≝ head8 v in if b then
     94        let 〈b,v〉≝  head … v in if b then
     95         let 〈b,v〉≝  head … v in if b then
    9696          〈〈XCH A (INDIRECT v), pc〉, one〉
    9797         else
    98           let 〈b,v〉≝ head8 v in if b then
     98          let 〈b,v〉≝  head … v in if b then
    9999           let 〈pc,b1〉≝ next pmem pc in 〈〈XCH A (DIRECT b1), pc〉, one〉
    100100          else
    101101           〈〈SWAP ACC_A, pc〉, one〉
    102102        else
    103          let 〈b,v〉≝ head8 v in if b then
    104           let 〈b,v〉≝ head8 v in if b then
     103         let 〈b,v〉≝  head … v in if b then
     104          let 〈b,v〉≝  head … v in if b then
    105105           〈〈CLR C, pc〉, one〉
    106106          else
    107107           let 〈pc,b1〉≝ next pmem pc in 〈〈CLR (BIT b1), pc〉, one〉
    108108         else
    109           let 〈b,v〉≝ head8 v in if b then
    110            assert false
     109          let 〈b,v〉≝  head … v in if b then
     110            ⊥
    111111          else
    112112           let 〈pc,b1〉≝ next pmem pc in 〈〈PUSH (DIRECT b1), pc〉, two〉
    113113    else
    114      let 〈b,v〉≝ head8 v in if b then
    115       let 〈b,v〉≝ head8 v in if b then
    116        let 〈b,v〉≝ head8 v in if b then
     114     let 〈b,v〉≝  head … v in if b then
     115      let 〈b,v〉≝  head … v in if b then
     116       let 〈b,v〉≝  head … v in if b then
    117117        let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈CJNE (U2 (REGISTER v) DATA b1) (REL b2), pc〉, two〉
    118118       else
    119         let 〈b,v〉≝ head8 v in if b then
    120          let 〈b,v〉≝ head8 v in if b then
     119        let 〈b,v〉≝  head … v in if b then
     120         let 〈b,v〉≝  head … v in if b then
    121121          let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈CJNE (U2 (INDIRECT v) (DATA b1)) (REL b2), pc〉, two〉
    122122         else
    123           let 〈b,v〉≝ head8 v in if b then
     123          let 〈b,v〉≝  head … v in if b then
    124124           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈CJNE (U1 A (DIRECT b1)) (REL b2), pc〉, two〉
    125125          else
    126126           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈CJNE (U1 A (DATA b1)) (REL b2), pc〉, two〉
    127127        else
    128          let 〈b,v〉≝ head8 v in if b then
    129           let 〈b,v〉≝ head8 v in if b then
     128         let 〈b,v〉≝  head … v in if b then
     129          let 〈b,v〉≝  head … v in if b then
    130130           〈〈CPL C, pc〉, one〉
    131131          else
    132132           let 〈pc,b1〉≝ next pmem pc in 〈〈CPL (BIT b1), pc〉, one〉
    133133         else
    134           let 〈b,v〉≝ head8 v in if b then
    135            assert false
     134          let 〈b,v〉≝  head … v in if b then
     135            ⊥
    136136          else
    137137           let 〈pc,b1〉≝ next pmem pc in 〈〈ANL (U3 C (NBIT b1)), pc〉, two〉
    138138      else
    139        let 〈b,v〉≝ head8 v in if b then
     139       let 〈b,v〉≝  head … v in if b then
    140140        let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U2 (REGISTER v) (DIRECT b1)), pc〉, two〉
    141141       else
    142         let 〈b,v〉≝ head8 v in if b then
    143          let 〈b,v〉≝ head8 v in if b then
     142        let 〈b,v〉≝  head … v in if b then
     143         let 〈b,v〉≝  head … v in if b then
    144144          let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U2 (INDIRECT v) (DIRECT b1)), pc〉, two〉
    145145         else
    146146          〈〈MUL A B, pc〉, four〉
    147147        else
    148          let 〈b,v〉≝ head8 v in if b then
    149           let 〈b,v〉≝ head8 v in if b then
     148         let 〈b,v〉≝  head … v in if b then
     149          let 〈b,v〉≝  head … v in if b then
    150150           〈〈INC DPTR, pc〉, two〉
    151151          else
    152152           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U5 C (BIT b1)), pc〉, one〉
    153153         else
    154           let 〈b,v〉≝ head8 v in if b then
    155            assert false
     154          let 〈b,v〉≝  head … v in if b then
     155            ⊥
    156156          else
    157157           let 〈pc,b1〉≝ next pmem pc in 〈〈ORL (U3 C (NBIT b1)), pc〉, two〉
    158158     else
    159       let 〈b,v〉≝ head8 v in if b then
    160        let 〈b,v〉≝ head8 v in if b then
     159      let 〈b,v〉≝  head … v in if b then
     160       let 〈b,v〉≝  head … v in if b then
    161161        〈〈SUBB A (REGISTER v), pc〉, one〉
    162162       else
    163         let 〈b,v〉≝ head8 v in if b then
    164          let 〈b,v〉≝ head8 v in if b then
     163        let 〈b,v〉≝  head … v in if b then
     164         let 〈b,v〉≝  head … v in if b then
    165165          〈〈SUBB A (INDIRECT v), pc〉, one〉
    166166         else
    167           let 〈b,v〉≝ head8 v in if b then
     167          let 〈b,v〉≝  head … v in if b then
    168168           let 〈pc,b1〉≝ next pmem pc in 〈〈SUBB A (DIRECT b1), pc〉, one〉
    169169          else
    170170           let 〈pc,b1〉≝ next pmem pc in 〈〈SUBB A (DATA b1), pc〉, one〉
    171171        else
    172          let 〈b,v〉≝ head8 v in if b then
    173           let 〈b,v〉≝ head8 v in if b then
     172         let 〈b,v〉≝  head … v in if b then
     173          let 〈b,v〉≝  head … v in if b then
    174174           〈〈MOVC A (ACC_A_DPTR), pc〉, two〉
    175175          else
    176176           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U6 (BIT b1) C), pc〉, two〉
    177177         else
    178           let 〈b,v〉≝ head8 v in if b then
    179            assert false
     178          let 〈b,v〉≝  head … v in if b then
     179            ⊥
    180180          else
    181181           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV (U4 DPTR (DATA16 (mk_word b1 b2))), pc〉, two〉
    182182      else
    183        let 〈b,v〉≝ head8 v in if b then
     183       let 〈b,v〉≝  head … v in if b then
    184184        let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U3 (DIRECT b1) (REGISTER v)), pc〉, two〉
    185185       else
    186         let 〈b,v〉≝ head8 v in if b then
    187          let 〈b,v〉≝ head8 v in if b then
     186        let 〈b,v〉≝  head … v in if b then
     187         let 〈b,v〉≝  head … v in if b then
    188188          let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U3 (DIRECT b1) (INDIRECT v)), pc〉, two〉
    189189         else
    190           let 〈b,v〉≝ head8 v in if b then
     190          let 〈b,v〉≝  head … v in if b then
    191191           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV (U3 (DIRECT b1) (DIRECT b2)), pc〉, two〉
    192192          else
    193193           〈〈DIV A B, pc〉, four〉
    194194        else
    195          let 〈b,v〉≝ head8 v in if b then
    196           let 〈b,v〉≝ head8 v in if b then
     195         let 〈b,v〉≝  head … v in if b then
     196          let 〈b,v〉≝  head … v in if b then
    197197           〈〈MOVC A (ACC_A_PC), pc〉, two〉
    198198          else
    199199           let 〈pc,b1〉≝ next pmem pc in 〈〈ANL (U3 C (BIT b1)), pc〉, two〉
    200200         else
    201           let 〈b,v〉≝ head8 v in if b then
    202            assert false
     201          let 〈b,v〉≝  head … v in if b then
     202            ⊥
    203203          else
    204204           let 〈pc,b1〉≝ next pmem pc in 〈〈SJMP (REL b1), pc〉, two〉
    205205   else
    206     let 〈b,v〉≝ head8 v in if b then
    207      let 〈b,v〉≝ head8 v in if b then
    208       let 〈b,v〉≝ head8 v in if b then
    209        let 〈b,v〉≝ head8 v in if b then
     206    let 〈b,v〉≝  head … v in if b then
     207     let 〈b,v〉≝  head … v in if b then
     208      let 〈b,v〉≝  head … v in if b then
     209       let 〈b,v〉≝  head … v in if b then
    210210        let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U2 (REGISTER v) (DATA b1)), pc〉, one〉
    211211       else
    212         let 〈b,v〉≝ head8 v in if b then
    213          let 〈b,v〉≝ head8 v in if b then
     212        let 〈b,v〉≝  head … v in if b then
     213         let 〈b,v〉≝  head … v in if b then
    214214          let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U2 (INDIRECT v) (DATA b1)), pc〉, one〉
    215215         else
    216           let 〈b,v〉≝ head8 v in if b then
     216          let 〈b,v〉≝  head … v in if b then
    217217           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV (U3 (DIRECT b1) (DATA b2)), pc〉, three〉
    218218          else
    219219           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U1 A (DATA b1)), pc〉, one〉
    220220        else
    221          let 〈b,v〉≝ head8 v in if b then
    222           let 〈b,v〉≝ head8 v in if b then
     221         let 〈b,v〉≝  head … v in if b then
     222          let 〈b,v〉≝  head … v in if b then
    223223           〈〈JMP IND_DPTR, pc〉, two〉
    224224          else
    225225           let 〈pc,b1〉≝ next pmem pc in 〈〈ORL (U3 C (BIT b1)), pc〉, two〉
    226226         else
    227           let 〈b,v〉≝ head8 v in if b then
    228            assert false
     227          let 〈b,v〉≝  head … v in if b then
     228            ⊥
    229229          else
    230230           let 〈pc,b1〉≝ next pmem pc in 〈〈JNZ (REL b1), pc〉, two〉
    231231      else
    232        let 〈b,v〉≝ head8 v in if b then
     232       let 〈b,v〉≝  head … v in if b then
    233233        〈〈XRL(U1 A (REGISTER v)), pc〉, one〉
    234234       else
    235         let 〈b,v〉≝ head8 v in if b then
    236          let 〈b,v〉≝ head8 v in if b then
     235        let 〈b,v〉≝  head … v in if b then
     236         let 〈b,v〉≝  head … v in if b then
    237237          〈〈XRL(U1 A (INDIRECT v)), pc〉, one〉
    238238         else
    239           let 〈b,v〉≝ head8 v in if b then
     239          let 〈b,v〉≝  head … v in if b then
    240240           let 〈pc,b1〉≝ next pmem pc in 〈〈XRL(U1 A (DIRECT b1)), pc〉, one〉
    241241          else
    242242           let 〈pc,b1〉≝ next pmem pc in 〈〈XRL(U1 A (DATA b1)), pc〉, one〉
    243243        else
    244          let 〈b,v〉≝ head8 v in if b then
    245           let 〈b,v〉≝ head8 v in if b then
     244         let 〈b,v〉≝  head … v in if b then
     245          let 〈b,v〉≝  head … v in if b then
    246246           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈XRL(U2 (DIRECT b1) (DATA b2)), pc〉, two〉
    247247          else
    248248           let 〈pc,b1〉≝ next pmem pc in 〈〈XRL(U2 (DIRECT b1) ACC_A), pc〉, one〉
    249249         else
    250           let 〈b,v〉≝ head8 v in if b then
    251            assert false
     250          let 〈b,v〉≝  head … v in if b then
     251            ⊥
    252252          else
    253253           let 〈pc,b1〉≝ next pmem pc in 〈〈JZ (REL b1), pc〉, two〉
    254254     else
    255       let 〈b,v〉≝ head8 v in if b then
    256        let 〈b,v〉≝ head8 v in if b then
     255      let 〈b,v〉≝  head … v in if b then
     256       let 〈b,v〉≝  head … v in if b then
    257257        〈〈ANL (U1 A (REGISTER v)), pc〉, one〉
    258258       else
    259         let 〈b,v〉≝ head8 v in if b then
    260          let 〈b,v〉≝ head8 v in if b then
     259        let 〈b,v〉≝  head … v in if b then
     260         let 〈b,v〉≝  head … v in if b then
    261261          〈〈ANL (U1 A (INDIRECT v)), pc〉, one〉
    262262         else
    263           let 〈b,v〉≝ head8 v in if b then
     263          let 〈b,v〉≝  head … v in if b then
    264264           let 〈pc,b1〉≝ next pmem pc in 〈〈ANL (U1 A (DIRECT b1)), pc〉, one〉
    265265          else
    266266           let 〈pc,b1〉≝ next pmem pc in 〈〈ANL (U1 A (DATA b1)), pc〉, one〉
    267267        else
    268          let 〈b,v〉≝ head8 v in if b then
    269           let 〈b,v〉≝ head8 v in if b then
     268         let 〈b,v〉≝  head … v in if b then
     269          let 〈b,v〉≝  head … v in if b then
    270270           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ANL (U2 (DIRECT b1) (DATA b2)), pc〉, two〉
    271271          else
    272272           let 〈pc,b1〉≝ next pmem pc in 〈〈ANL (U2 (DIRECT b1) A), pc〉, one〉
    273273         else
    274           let 〈b,v〉≝ head8 v in if b then
    275            assert false
     274          let 〈b,v〉≝  head … v in if b then
     275            ⊥
    276276          else
    277277           let 〈pc,b1〉≝ next pmem pc in 〈〈JNC (REL b1), pc〉, two〉
    278278      else
    279        let 〈b,v〉≝ head8 v in if b then
     279       let 〈b,v〉≝  head … v in if b then
    280280        〈〈ORL (U1 A (REGISTER v)), pc〉, one〉
    281281       else
    282         let 〈b,v〉≝ head8 v in if b then
    283          let 〈b,v〉≝ head8 v in if b then
     282        let 〈b,v〉≝  head … v in if b then
     283         let 〈b,v〉≝  head … v in if b then
    284284          〈〈ORL (U1 A (INDIRECT v)), pc〉, one〉
    285285         else
    286           let 〈b,v〉≝ head8 v in if b then
     286          let 〈b,v〉≝  head … v in if b then
    287287           let 〈pc,b1〉≝ next pmem pc in 〈〈ORL (U1 A (DIRECT b1)), pc〉, one〉
    288288          else
    289289           let 〈pc,b1〉≝ next pmem pc in 〈〈ORL (U1 A (DATA b1)), pc〉, one〉
    290290        else
    291          let 〈b,v〉≝ head8 v in if b then
    292           let 〈b,v〉≝ head8 v in if b then
     291         let 〈b,v〉≝  head … v in if b then
     292          let 〈b,v〉≝  head … v in if b then
    293293           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ORL (U2 (DIRECT b1) (DATA b2)), pc〉, two〉
    294294          else
    295295           let 〈pc,b1〉≝ next pmem pc in 〈〈ORL (U2 (DIRECT b1) ACC_A), pc〉, one〉
    296296         else
    297           let 〈b,v〉≝ head8 v in if b then
    298            assert false
     297          let 〈b,v〉≝  head … v in if b then
     298            ⊥
    299299          else
    300300           let 〈pc,b1〉≝ next pmem pc in 〈〈JC (REL b1), pc〉, two〉
    301301    else
    302      let 〈b,v〉≝ head8 v in if b then
    303       let 〈b,v〉≝ head8 v in if b then
    304        let 〈b,v〉≝ head8 v in if b then
     302     let 〈b,v〉≝  head … v in if b then
     303      let 〈b,v〉≝  head … v in if b then
     304       let 〈b,v〉≝  head … v in if b then
    305305        〈〈ADDC A (REGISTER v), pc〉, one〉
    306306       else
    307         let 〈b,v〉≝ head8 v in if b then
    308          let 〈b,v〉≝ head8 v in if b then
     307        let 〈b,v〉≝  head … v in if b then
     308         let 〈b,v〉≝  head … v in if b then
    309309          〈〈ADDC A (INDIRECT v), pc〉, one〉
    310310         else
    311           let 〈b,v〉≝ head8 v in if b then
     311          let 〈b,v〉≝  head … v in if b then
    312312           let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC A (DIRECT b1), pc〉, one〉
    313313          else
    314314           let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC A (DATA b1), pc〉, one〉
    315315        else
    316          let 〈b,v〉≝ head8 v in if b then
    317           let 〈b,v〉≝ head8 v in if b then
     316         let 〈b,v〉≝  head … v in if b then
     317          let 〈b,v〉≝  head … v in if b then
    318318           〈〈RLC ACC_A, pc〉, one〉
    319319          else
    320320           〈〈RETI, pc〉, two〉
    321321         else
    322           let 〈b,v〉≝ head8 v in if b then
    323            assert false
     322          let 〈b,v〉≝  head … v in if b then
     323             ⊥
    324324          else
    325325           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈JNB (BIT b1) (REL b2), pc〉, two〉
    326326      else
    327        let 〈b,v〉≝ head8 v in if b then
     327       let 〈b,v〉≝  head … v in if b then
    328328        〈〈ADD A (REGISTER v), pc〉, one〉
    329329       else
    330         let 〈b,v〉≝ head8 v in if b then
    331          let 〈b,v〉≝ head8 v in if b then
     330        let 〈b,v〉≝  head … v in if b then
     331         let 〈b,v〉≝  head … v in if b then
    332332          〈〈ADD A (INDIRECT v), pc〉, one〉
    333333         else
    334           let 〈b,v〉≝ head8 v in if b then
     334          let 〈b,v〉≝  head … v in if b then
    335335           let 〈pc,b1〉≝ next pmem pc in 〈〈ADD A (DIRECT b1), pc〉, one〉
    336336          else
    337337           let 〈pc,b1〉≝ next pmem pc in 〈〈ADD A (DATA b1), pc〉, one〉
    338338        else
    339          let 〈b,v〉≝ head8 v in if b then
    340           let 〈b,v〉≝ head8 v in if b then
     339         let 〈b,v〉≝  head … v in if b then
     340          let 〈b,v〉≝  head … v in if b then
    341341           〈〈RL ACC_A, pc〉, one〉
    342           let 〈b,v〉≝ head8 v in if b then
    343342          else
    344343           〈〈RET, pc〉, two〉
    345344         else
    346           let 〈b,v〉≝ head8 v in if b then
    347            assert false
     345          let 〈b,v〉≝  head … v in if b then
     346            ⊥
    348347          else
    349348           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈JB (BIT b1) (REL b2), pc〉, two〉
    350349     else
    351       let 〈b,v〉≝ head8 v in if b then
    352        let 〈b,v〉≝ head8 v in if b then
     350      let 〈b,v〉≝  head … v in if b then
     351       let 〈b,v〉≝  head … v in if b then
    353352        〈〈DEC (REGISTER v), pc〉, one〉
    354353       else
    355         let 〈b,v〉≝ head8 v in if b then
    356          let 〈b,v〉≝ head8 v in if b then
     354        let 〈b,v〉≝  head … v in if b then
     355         let 〈b,v〉≝  head … v in if b then
    357356          〈〈DEC (INDIRECT v), pc〉, one〉
    358357         else
    359           let 〈b,v〉≝ head8 v in if b then
     358          let 〈b,v〉≝  head … v in if b then
    360359           let 〈pc,b1〉≝ next pmem pc in 〈〈DEC (DIRECT b1), pc〉, one〉
    361360          else
    362361           〈〈DEC ACC_A, pc〉, one〉
    363362        else
    364          let 〈b,v〉≝ head8 v in if b then
    365           let 〈b,v〉≝ head8 v in if b then
     363         let 〈b,v〉≝  head … v in if b then
     364          let 〈b,v〉≝  head … v in if b then
    366365           〈〈RRC ACC_A, pc〉, one〉
    367366          else
    368367           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LCALL (ADDR16 (mk_word b1 b2)), pc〉, two〉
    369368         else
    370           let 〈b,v〉≝ head8 v in if b then
    371            assert false
     369          let 〈b,v〉≝  head … v in if b then
     370            ⊥
    372371          else
    373372           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈JBC (BIT b1) (REL b2), pc〉, two〉
    374373      else
    375        let 〈b,v〉≝ head8 v in if b then
     374       let 〈b,v〉≝  head … v in if b then
    376375        〈〈INC (REGISTER v), pc〉, one〉
    377376       else
    378         let 〈b,v〉≝ head8 v in if b then
    379          let 〈b,v〉≝ head8 v in if b then
     377        let 〈b,v〉≝  head … v in if b then
     378         let 〈b,v〉≝  head … v in if b then
    380379          〈〈INC (INDIRECT v), pc〉, one〉
    381380         else
    382           let 〈b,v〉≝ head8 v in if b then
     381          let 〈b,v〉≝  head … v in if b then
    383382           let 〈pc,b1〉≝ next pmem pc in 〈〈INC (DIRECT b1), pc〉, one〉
    384383          else
    385384           〈〈INC ACC_A, pc〉, one〉
    386385        else
    387          let 〈b,v〉≝ head8 v in if b then
    388           let 〈b,v〉≝ head8 v in if b then
     386         let 〈b,v〉≝  head … v in if b then
     387          let 〈b,v〉≝  head … v in if b then
    389388           〈〈RR ACC_A, pc〉, one〉
    390389          else
    391390           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LJMP (ADDR16 (mk_word b1 b2)), pc〉, two〉
    392391         else
    393           let 〈b,v〉≝ head8 v in if b then
    394            assert false
     392          let 〈b,v〉≝  head … v in if b then
     393            ⊥
    395394          else
    396395           〈〈NOP, pc〉, one〉.
  • Deliverables/D4.1/Matita/Vector.ma

    r320 r322  
    147147nqed.
    148148
    149 ndefinition head8 ≝ λA. split A (S Z) (S (S (S (S (S (S (S Z))))))).
     149ndefinition head: ∀A:Type[0]. ∀n. Vector A (S n) → A × (Vector A n)
     150≝ λA,n,v.
     151 match v return λl.λ_:Vector A l.l = S n → A × (Vector A n) with
     152  [ Empty ⇒ λK.⊥
     153  | Cons o he tl ⇒ λK. 〈he,(tl⌈Vector A n ↦ Vector A o⌉)〉
     154  ] (? : S ? = S ?).
     155//; ndestruct; //.
     156nqed.
     157
     158ndefinition from_singl: ∀A:Type[0]. Vector A (S Z) → A ≝
     159 λA,v. first … (head … v).
    150160   
    151161(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    159169    | Cons n hd tl ⇒ f hd (fold_right A B n f x tl)
    160170    ].
    161    
     171
     172(*
    162173nlet rec fold_right_i (A: Type[0]) (B: Type[0]) (C: Type[0])
    163174                      (n: Nat) (m: Nat)
     
    177188        ]
    178189    ]) ?.
    179    
     190*)
     191 
    180192nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: Nat)
    181193                    (f: A → B → A) (x: A) (v: Vector B n) on v ≝
Note: See TracChangeset for help on using the changeset viewer.