Changeset 323


Ignore:
Timestamp:
Nov 26, 2010, 10:14:45 PM (9 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

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

    r322 r323  
    1313 λpmem,pc.
    1414  let 〈pc,v〉 ≝ next pmem pc in
    15   let 〈v1,v2〉 ≝ split … three five v in
    16    if eqv … v2 [[true;false;false;false;true]] then
    17     let 〈pc,b1〉 ≝ next pmem pc in
    18      〈〈ACALL … (ADDR11 (v1 @@ b1)), pc〉, two〉
    19    else if eqv … v2 [[false;false;false;false;true]] then
    20     let 〈pc,b1〉 ≝ next pmem pc in
    21      〈〈AJMP … (ADDR11 (v1 @@ b1)), pc〉, two〉
    22    else
    2315   let 〈b,v〉≝  head … v in if b then
    2416    let 〈b,v〉≝  head … v in if b then
     
    3022        let 〈b,v〉≝  head … v in if b then
    3123         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
    35            let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U3 (DIRECT b1) ACC_A), pc〉, one〉
    36           else
    37            〈〈CPL ACC_A, pc〉, one〉
    38         else
    39          let 〈b,v〉≝  head … v in if b then
    40           〈〈MOVX (U2 (EXT_INDIRECT v) ACC_A), pc〉, two〉
    41          else
    42           let 〈b,v〉≝  head … v in if b then
    43             ⊥
    44           else
    45            〈〈MOVX (U2 (EXT_IND_DPTR) ACC_A), pc〉, two〉
    46       else
    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
    52           〈〈MOV (U1 A (INDIRECT v)), pc〉, one〉
    53          else
    54           let 〈b,v〉≝  head … v in if b then
    55            let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U1 A (DIRECT b1)), pc〉, one〉
    56           else
    57            〈〈CLR ACC_A, pc〉, one〉
    58         else
    59          let 〈b,v〉≝  head … v in if b then
    60           〈〈MOVX (U1 A (EXT_INDIRECT v)), pc〉, two〉
    61          else
    62           let 〈b,v〉≝  head … v in if b then
    63             ⊥
    64           else
    65            〈〈MOVX (U1 A EXT_IND_DPTR), pc〉, two〉
     24          ?(*〈〈MOV (U2 (INDIRECT (from_singl … v)) ACC_A), pc〉, one〉*)
     25         else
     26          let 〈b,v〉≝  head … v in if b then
     27           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈MOV (U3 (DIRECT b1) ACC_A), pc〉, one〉*)
     28          else
     29           〈〈CPL ACC_A, pc〉, one〉
     30        else
     31         let 〈b,v〉≝  head … v in if b then
     32          ?(*〈〈MOVX (U2 (EXT_INDIRECT (from_singl … v)) ACC_A), pc〉, two〉*)
     33         else
     34          let 〈b,v〉≝  head … v in if b then
     35           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, two〉
     36          else
     37           ?(*〈〈MOVX (U2 (EXT_IND_DPTR) ACC_A), pc〉, two〉*)
     38      else
     39       let 〈b,v〉≝  head … v in if b then
     40        〈〈MOV ? (Left ?? (Left ?? (Left ?? (Left ?? (Left ?? (? 〈ACC_A,REGISTER v〉)))))), pc〉, one〉
     41       else
     42        let 〈b,v〉≝  head … v in if b then
     43         let 〈b,v〉≝  head … v in if b then
     44          ?(*〈〈MOV (U1 ACC_A (INDIRECT (from_singl … v))), pc〉, one〉*)
     45         else
     46          let 〈b,v〉≝  head … v in if b then
     47           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈MOV (U1 ACC_A (DIRECT b1)), pc〉, one〉*)
     48          else
     49           〈〈CLR ACC_A, pc〉, one〉
     50        else
     51         let 〈b,v〉≝  head … v in if b then
     52          ?(*〈〈MOVX (U1 ACC_A (EXT_INDIRECT (from_singl … v))), pc〉, two〉*)
     53         else
     54          let 〈b,v〉≝  head … v in if b then
     55           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, two〉
     56          else
     57           ?(*〈〈MOVX (U1 ACC_A EXT_IND_DPTR), pc〉, two〉*)
    6658     else
    6759      let 〈b,v〉≝  head … v in if b then
    6860       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
    73           〈〈XCHD A INDIRECT v, pc〉, one〉
    74          else
    75           let 〈b,v〉≝  head … v in if b then
    76            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈DJNZ (DIRECT b1) (REL b2), pc〉, two〉
    77           else
    78            〈〈DA ACC_A, pc〉, one〉
    79         else
    80          let 〈b,v〉≝  head … v in if b then
    81           let 〈b,v〉≝  head … v in if b then
    82            〈〈SETB C, pc〉, one〉
    83           else
    84            let 〈pc,b1〉≝ next pmem pc in 〈〈SETB (BIT b1), pc〉, one〉
    85          else
    86           let 〈b,v〉≝  head … v in if b then
    87             ⊥
    88           else
    89            let 〈pc,b1〉≝ next pmem pc in 〈〈POP (DIRECT b1), pc〉, two〉
    90       else
    91        let 〈b,v〉≝  head … v in if b then
    92         〈〈XCH A (REGISTER v), pc〉, one〉
    93        else
    94         let 〈b,v〉≝  head … v in if b then
    95          let 〈b,v〉≝  head … v in if b then
    96           〈〈XCH A (INDIRECT v), pc〉, one〉
    97          else
    98           let 〈b,v〉≝  head … v in if b then
    99            let 〈pc,b1〉≝ next pmem pc in 〈〈XCH A (DIRECT b1), pc〉, one〉
    100           else
    101            〈〈SWAP ACC_A, pc〉, one〉
    102         else
    103          let 〈b,v〉≝  head … v in if b then
    104           let 〈b,v〉≝  head … v in if b then
    105            〈〈CLR C, pc〉, one〉
    106           else
    107            let 〈pc,b1〉≝ next pmem pc in 〈〈CLR (BIT b1), pc〉, one〉
    108          else
    109           let 〈b,v〉≝  head … v in if b then
    110             ⊥
    111           else
    112            let 〈pc,b1〉≝ next pmem pc in 〈〈PUSH (DIRECT b1), pc〉, two〉
     61        let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, two〉
     62       else
     63        let 〈b,v〉≝  head … v in if b then
     64         let 〈b,v〉≝  head … v in if b then
     65          〈〈XCHD … ACC_A (INDIRECT (from_singl … v)), pc〉, one〉
     66         else
     67          let 〈b,v〉≝  head … v in if b then
     68           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump … (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, two〉
     69          else
     70           〈〈DA ACC_A, pc〉, one〉
     71        else
     72         let 〈b,v〉≝  head … v in if b then
     73          let 〈b,v〉≝  head … v in if b then
     74           〈〈SETB … CARRY, pc〉, one〉
     75          else
     76           let 〈pc,b1〉≝ next pmem pc in 〈〈SETB … (BIT_ADDR (from_singl … b1)), pc〉, one〉
     77         else
     78          let 〈b,v〉≝  head … v in if b then
     79           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, two〉
     80          else
     81           let 〈pc,b1〉≝ next pmem pc in 〈〈POP (DIRECT b1), pc〉, two〉
     82      else
     83       let 〈b,v〉≝  head … v in if b then
     84        〈〈XCH … ACC_A (REGISTER v), pc〉, one〉
     85       else
     86        let 〈b,v〉≝  head … v in if b then
     87         let 〈b,v〉≝  head … v in if b then
     88          〈〈XCH … ACC_A (INDIRECT (from_singl … v)), pc〉, one〉
     89         else
     90          let 〈b,v〉≝  head … v in if b then
     91           let 〈pc,b1〉≝ next pmem pc in 〈〈XCH … ACC_A (DIRECT b1), pc〉, one〉
     92          else
     93           〈〈SWAP ACC_A, pc〉, one〉
     94        else
     95         let 〈b,v〉≝  head … v in if b then
     96          let 〈b,v〉≝  head … v in if b then
     97           〈〈CLR … CARRY, pc〉, one〉
     98          else
     99           let 〈pc,b1〉≝ next pmem pc in 〈〈CLR … (BIT_ADDR b1), pc〉, one〉
     100         else
     101          let 〈b,v〉≝  head … v in if b then
     102           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, two〉
     103          else
     104           let 〈pc,b1〉≝ next pmem pc in 〈〈PUSH (DIRECT b1), pc〉, two〉
    113105    else
    114106     let 〈b,v〉≝  head … v in if b then
    115107      let 〈b,v〉≝  head … v in if b then
    116108       let 〈b,v〉≝  head … v in if b then
    117         let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈CJNE (U2 (REGISTER v) DATA b1) (REL b2), pc〉, two〉
    118        else
    119         let 〈b,v〉≝  head … v in if b then
    120          let 〈b,v〉≝  head … v in if b then
    121           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈CJNE (U2 (INDIRECT v) (DATA b1)) (REL b2), pc〉, two〉
    122          else
    123           let 〈b,v〉≝  head … v in if b then
    124            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈CJNE (U1 A (DIRECT b1)) (REL b2), pc〉, two〉
    125           else
    126            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈CJNE (U1 A (DATA b1)) (REL b2), pc〉, two〉
    127         else
    128          let 〈b,v〉≝  head … v in if b then
    129           let 〈b,v〉≝  head … v in if b then
    130            〈〈CPL C, pc〉, one〉
    131           else
    132            let 〈pc,b1〉≝ next pmem pc in 〈〈CPL (BIT b1), pc〉, one〉
    133          else
    134           let 〈b,v〉≝  head … v in if b then
    135             ⊥
    136           else
    137            let 〈pc,b1〉≝ next pmem pc in 〈〈ANL (U3 C (NBIT b1)), pc〉, two〉
    138       else
    139        let 〈b,v〉≝  head … v in if b then
    140         let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U2 (REGISTER v) (DIRECT b1)), pc〉, two〉
    141        else
    142         let 〈b,v〉≝  head … v in if b then
    143          let 〈b,v〉≝  head … v in if b then
    144           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U2 (INDIRECT v) (DIRECT b1)), pc〉, two〉
    145          else
    146           〈〈MUL A B, pc〉, four〉
    147         else
    148          let 〈b,v〉≝  head … v in if b then
    149           let 〈b,v〉≝  head … v in if b then
    150            〈〈INC DPTR, pc〉, two〉
    151           else
    152            let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U5 C (BIT b1)), pc〉, one〉
    153          else
    154           let 〈b,v〉≝  head … v in if b then
    155             ⊥
    156           else
    157            let 〈pc,b1〉≝ next pmem pc in 〈〈ORL (U3 C (NBIT b1)), pc〉, two〉
     109        let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in ?(*〈〈Jump … (CJNE …  (U2 (REGISTER v) DATA b1) (RELATIVE b2)), pc〉, two〉*)
     110       else
     111        let 〈b,v〉≝  head … v in if b then
     112         let 〈b,v〉≝  head … v in if b then
     113          let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in ?(*〈〈Jump … (CJNE … (U2 (INDIRECT (from_singl … v)) (DATA b1)) (RELATIVE b2)), pc〉, two〉*)
     114         else
     115          let 〈b,v〉≝  head … v in if b then
     116           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in ?(*〈〈Jump … (CJNE …  (U1 ACC_A (DIRECT b1)) (RELATIVE b2)), pc〉, two〉*)
     117          else
     118           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in ?(*〈〈Jump … (CJNE … (U1 ACC_A (DATA b1)) (RELATIVE b2)), pc〉, two〉*)
     119        else
     120         let 〈b,v〉≝  head … v in if b then
     121          let 〈b,v〉≝  head … v in if b then
     122           〈〈CPL … CARRY, pc〉, one〉
     123          else
     124           let 〈pc,b1〉≝ next pmem pc in 〈〈CPL … (BIT_ADDR b1), pc〉, one〉
     125         else
     126          let 〈b,v〉≝  head … v in if b then
     127           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, two〉
     128          else
     129           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ANL (U3 C (N_BIT_ADDR b1)), pc〉, two〉*)
     130      else
     131       let 〈b,v〉≝  head … v in if b then
     132        let 〈pc,b1〉≝ next pmem pc in ?(*〈〈MOV (U2 (REGISTER v) (DIRECT b1)), pc〉, two〉*)
     133       else
     134        let 〈b,v〉≝  head … v in if b then
     135         let 〈b,v〉≝  head … v in if b then
     136          let 〈pc,b1〉≝ next pmem pc in ?(*〈〈MOV (U2 (INDIRECT (from_singl … v)) (DIRECT b1)), pc〉, two〉*)
     137         else
     138          〈〈MUL … ACC_A ACC_B, pc〉, four〉
     139        else
     140         let 〈b,v〉≝  head … v in if b then
     141          let 〈b,v〉≝  head … v in if b then
     142           〈〈INC DPTR, pc〉, two〉
     143          else
     144           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈MOV (U5 C (BIT_ADDR b1)), pc〉, one〉*)
     145         else
     146          let 〈b,v〉≝  head … v in if b then
     147           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, two〉
     148          else
     149           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ORL (U3 C (N_BIT_ADDR b1)), pc〉, two〉*)
    158150     else
    159151      let 〈b,v〉≝  head … v in if b then
    160152       let 〈b,v〉≝  head … v in if b then
    161         〈〈SUBB A (REGISTER v), pc〉, one〉
    162        else
    163         let 〈b,v〉≝  head … v in if b then
    164          let 〈b,v〉≝  head … v in if b then
    165           〈〈SUBB A (INDIRECT v), pc〉, one〉
    166          else
    167           let 〈b,v〉≝  head … v in if b then
    168            let 〈pc,b1〉≝ next pmem pc in 〈〈SUBB A (DIRECT b1), pc〉, one〉
    169           else
    170            let 〈pc,b1〉≝ next pmem pc in 〈〈SUBB A (DATA b1), pc〉, one〉
    171         else
    172          let 〈b,v〉≝  head … v in if b then
    173           let 〈b,v〉≝  head … v in if b then
    174            〈〈MOVC A (ACC_A_DPTR), pc〉, two〉
    175           else
    176            let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U6 (BIT b1) C), pc〉, two〉
    177          else
    178           let 〈b,v〉≝  head … v in if b then
    179             ⊥
    180           else
    181            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV (U4 DPTR (DATA16 (mk_word b1 b2))), pc〉, two〉
    182       else
    183        let 〈b,v〉≝  head … v in if b then
    184         let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U3 (DIRECT b1) (REGISTER v)), pc〉, two〉
    185        else
    186         let 〈b,v〉≝  head … v in if b then
    187          let 〈b,v〉≝  head … v in if b then
    188           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U3 (DIRECT b1) (INDIRECT v)), pc〉, two〉
    189          else
    190           let 〈b,v〉≝  head … v in if b then
    191            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV (U3 (DIRECT b1) (DIRECT b2)), pc〉, two〉
    192           else
    193            〈〈DIV A B, pc〉, four〉
    194         else
    195          let 〈b,v〉≝  head … v in if b then
    196           let 〈b,v〉≝  head … v in if b then
    197            〈〈MOVC A (ACC_A_PC), pc〉, two〉
    198           else
    199            let 〈pc,b1〉≝ next pmem pc in 〈〈ANL (U3 C (BIT b1)), pc〉, two〉
    200          else
    201           let 〈b,v〉≝  head … v in if b then
    202             ⊥
    203           else
    204            let 〈pc,b1〉≝ next pmem pc in 〈〈SJMP (REL b1), pc〉, two〉
     153        〈〈SUBB … ACC_A (REGISTER v), pc〉, one〉
     154       else
     155        let 〈b,v〉≝  head … v in if b then
     156         let 〈b,v〉≝  head … v in if b then
     157          〈〈SUBB … ACC_A (INDIRECT (from_singg … v)), pc〉, one〉
     158         else
     159          let 〈b,v〉≝  head … v in if b then
     160           let 〈pc,b1〉≝ next pmem pc in 〈〈SUBB … ACC_A (DIRECT b1), pc〉, one〉
     161          else
     162           let 〈pc,b1〉≝ next pmem pc in 〈〈SUBB … ACC_A (DATA b1), pc〉, one〉
     163        else
     164         let 〈b,v〉≝  head … v in if b then
     165          let 〈b,v〉≝  head … v in if b then
     166           〈〈MOVC … ACC_A (ACC_A_DPTR), pc〉, two〉
     167          else
     168           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈MOV (U6 (BIT_ADDR b1) C), pc〉, two〉*)
     169         else
     170          let 〈b,v〉≝  head … v in if b then
     171           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, two〉
     172          else
     173           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in ?(*〈〈MOV (U4 DPTR (DATA16 (mk_word b1 b2))), pc〉, two〉*)
     174      else
     175       let 〈b,v〉≝  head … v in if b then
     176        let 〈pc,b1〉≝ next pmem pc in ?(*〈〈MOV (U3 (DIRECT b1) (REGISTER v)), pc〉, two〉*)
     177       else
     178        let 〈b,v〉≝  head … v in if b then
     179         let 〈b,v〉≝  head … v in if b then
     180          let 〈pc,b1〉≝ next pmem pc in ?(*〈〈MOV (U3 (DIRECT b1) (INDIRECT (from_singl … v))), pc〉, two〉*)
     181         else
     182          let 〈b,v〉≝  head … v in if b then
     183           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in ?(*〈〈MOV (U3 (DIRECT b1) (DIRECT b2)), pc〉, two〉*)
     184          else
     185           〈〈DIV … ACC_A ACC_B, pc〉, four〉
     186        else
     187         let 〈b,v〉≝  head … v in if b then
     188          let 〈b,v〉≝  head … v in if b then
     189           〈〈MOVC … ACC_A (ACC_A_PC), pc〉, two〉
     190          else
     191           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ANL (U3 C (BIT_ADDR b1)), pc〉, two〉*)
     192         else
     193          let 〈b,v〉≝  head … v in if b then
     194           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, two〉
     195          else
     196           let 〈pc,b1〉≝ next pmem pc in 〈〈SJMP … (RELATIVE b1), pc〉, two〉
    205197   else
    206198    let 〈b,v〉≝  head … v in if b then
     
    208200      let 〈b,v〉≝  head … v in if b then
    209201       let 〈b,v〉≝  head … v in if b then
    210         let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U2 (REGISTER v) (DATA b1)), pc〉, one〉
    211        else
    212         let 〈b,v〉≝  head … v in if b then
    213          let 〈b,v〉≝  head … v in if b then
    214           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U2 (INDIRECT v) (DATA b1)), pc〉, one〉
    215          else
    216           let 〈b,v〉≝  head … v in if b then
    217            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV (U3 (DIRECT b1) (DATA b2)), pc〉, three〉
    218           else
    219            let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U1 A (DATA b1)), pc〉, one〉
    220         else
    221          let 〈b,v〉≝  head … v in if b then
    222           let 〈b,v〉≝  head … v in if b then
    223            〈〈JMP IND_DPTR, pc〉, two〉
    224           else
    225            let 〈pc,b1〉≝ next pmem pc in 〈〈ORL (U3 C (BIT b1)), pc〉, two〉
    226          else
    227           let 〈b,v〉≝  head … v in if b then
    228             ⊥
    229           else
    230            let 〈pc,b1〉≝ next pmem pc in 〈〈JNZ (REL b1), pc〉, two〉
    231       else
    232        let 〈b,v〉≝  head … v in if b then
    233         〈〈XRL(U1 A (REGISTER v)), pc〉, one〉
    234        else
    235         let 〈b,v〉≝  head … v in if b then
    236          let 〈b,v〉≝  head … v in if b then
    237           〈〈XRL(U1 A (INDIRECT v)), pc〉, one〉
    238          else
    239           let 〈b,v〉≝  head … v in if b then
    240            let 〈pc,b1〉≝ next pmem pc in 〈〈XRL(U1 A (DIRECT b1)), pc〉, one〉
    241           else
    242            let 〈pc,b1〉≝ next pmem pc in 〈〈XRL(U1 A (DATA b1)), pc〉, one〉
    243         else
    244          let 〈b,v〉≝  head … v in if b then
    245           let 〈b,v〉≝  head … v in if b then
    246            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈XRL(U2 (DIRECT b1) (DATA b2)), pc〉, two〉
    247           else
    248            let 〈pc,b1〉≝ next pmem pc in 〈〈XRL(U2 (DIRECT b1) ACC_A), pc〉, one〉
    249          else
    250           let 〈b,v〉≝  head … v in if b then
    251             ⊥
    252           else
    253            let 〈pc,b1〉≝ next pmem pc in 〈〈JZ (REL b1), pc〉, two〉
     202        let 〈pc,b1〉≝ next pmem pc in ?(*〈〈MOV (U2 (REGISTER v) (DATA b1)), pc〉, one〉*)
     203       else
     204        let 〈b,v〉≝  head … v in if b then
     205         let 〈b,v〉≝  head … v in if b then
     206          let 〈pc,b1〉≝ next pmem pc in ?(*〈〈MOV (U2 (INDIRECT (from_singl … v)) (DATA b1)), pc〉, one〉*)
     207         else
     208          let 〈b,v〉≝  head … v in if b then
     209           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in ?(*〈〈MOV (U3 (DIRECT b1) (DATA b2)), pc〉, three〉*)
     210          else
     211           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈MOV (U1 ACC_A (DATA b1)), pc〉, one〉*)
     212        else
     213         let 〈b,v〉≝  head … v in if b then
     214          let 〈b,v〉≝  head … v in if b then
     215           〈〈JMP IND_DPTR, pc〉, two〉
     216          else
     217           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ORL (U3 C (BIT_ADDR b1)), pc〉, two〉*)
     218         else
     219          let 〈b,v〉≝  head … v in if b then
     220           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, two〉
     221          else
     222           let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JNZ … (RELATIVE b1)), pc〉, two〉
     223      else
     224       let 〈b,v〉≝  head … v in if b then
     225        ?(*〈〈XRL(U1 ACC_A (REGISTER v)), pc〉, one〉*)
     226       else
     227        let 〈b,v〉≝  head … v in if b then
     228         let 〈b,v〉≝  head … v in if b then
     229          ?(*〈〈XRL(U1 ACC_A (INDIRECT (from_singl … v))), pc〉, one〉*)
     230         else
     231          let 〈b,v〉≝  head … v in if b then
     232           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈XRL(U1 ACC_A (DIRECT b1)), pc〉, one〉*)
     233          else
     234           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈XRL(U1 ACC_A (DATA b1)), pc〉, one〉*)
     235        else
     236         let 〈b,v〉≝  head … v in if b then
     237          let 〈b,v〉≝  head … v in if b then
     238           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in ?(*〈〈XRL(U2 (DIRECT b1) (DATA b2)), pc〉, two〉*)
     239          else
     240           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈XRL(U2 (DIRECT b1) ACC_A), pc〉, one〉*)
     241         else
     242          let 〈b,v〉≝  head … v in if b then
     243           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, two〉
     244          else
     245           let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JZ … (RELATIVE b1)), pc〉, two〉
    254246     else
    255247      let 〈b,v〉≝  head … v in if b then
    256248       let 〈b,v〉≝  head … v in if b then
    257         〈〈ANL (U1 A (REGISTER v)), pc〉, one〉
    258        else
    259         let 〈b,v〉≝  head … v in if b then
    260          let 〈b,v〉≝  head … v in if b then
    261           〈〈ANL (U1 A (INDIRECT v)), pc〉, one〉
    262          else
    263           let 〈b,v〉≝  head … v in if b then
    264            let 〈pc,b1〉≝ next pmem pc in 〈〈ANL (U1 A (DIRECT b1)), pc〉, one〉
    265           else
    266            let 〈pc,b1〉≝ next pmem pc in 〈〈ANL (U1 A (DATA b1)), pc〉, one〉
    267         else
    268          let 〈b,v〉≝  head … v in if b then
    269           let 〈b,v〉≝  head … v in if b then
    270            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ANL (U2 (DIRECT b1) (DATA b2)), pc〉, two〉
    271           else
    272            let 〈pc,b1〉≝ next pmem pc in 〈〈ANL (U2 (DIRECT b1) A), pc〉, one〉
    273          else
    274           let 〈b,v〉≝  head … v in if b then
    275             ⊥
    276           else
    277            let 〈pc,b1〉≝ next pmem pc in 〈〈JNC (REL b1), pc〉, two〉
    278       else
    279        let 〈b,v〉≝  head … v in if b then
    280         〈〈ORL (U1 A (REGISTER v)), pc〉, one〉
    281        else
    282         let 〈b,v〉≝  head … v in if b then
    283          let 〈b,v〉≝  head … v in if b then
    284           〈〈ORL (U1 A (INDIRECT v)), pc〉, one〉
    285          else
    286           let 〈b,v〉≝  head … v in if b then
    287            let 〈pc,b1〉≝ next pmem pc in 〈〈ORL (U1 A (DIRECT b1)), pc〉, one〉
    288           else
    289            let 〈pc,b1〉≝ next pmem pc in 〈〈ORL (U1 A (DATA b1)), pc〉, one〉
    290         else
    291          let 〈b,v〉≝  head … v in if b then
    292           let 〈b,v〉≝  head … v in if b then
    293            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ORL (U2 (DIRECT b1) (DATA b2)), pc〉, two〉
    294           else
    295            let 〈pc,b1〉≝ next pmem pc in 〈〈ORL (U2 (DIRECT b1) ACC_A), pc〉, one〉
    296          else
    297           let 〈b,v〉≝  head … v in if b then
    298             ⊥
    299           else
    300            let 〈pc,b1〉≝ next pmem pc in 〈〈JC (REL b1), pc〉, two〉
     249        ?(*〈〈ANL (U1 ACC_A (REGISTER v)), pc〉, one〉*)
     250       else
     251        let 〈b,v〉≝  head … v in if b then
     252         let 〈b,v〉≝  head … v in if b then
     253          ?(*〈〈ANL (U1 ACC_A (INDIRECT (from_singl … v))), pc〉, one〉*)
     254         else
     255          let 〈b,v〉≝  head … v in if b then
     256           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ANL (U1 ACC_A (DIRECT b1)), pc〉, one〉*)
     257          else
     258           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ANL (U1 ACC_A (DATA b1)), pc〉, one〉*)
     259        else
     260         let 〈b,v〉≝  head … v in if b then
     261          let 〈b,v〉≝  head … v in if b then
     262           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in ?(*〈〈ANL (U2 (DIRECT b1) (DATA b2)), pc〉, two〉*)
     263          else
     264           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ANL (U2 (DIRECT b1) A), pc〉, one〉*)
     265         else
     266          let 〈b,v〉≝  head … v in if b then
     267           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, two〉
     268          else
     269           let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JNC … (RELATIVE b1)), pc〉, two〉
     270      else
     271       let 〈b,v〉≝  head … v in if b then
     272        ?(*〈〈ORL (U1 ACC_A (REGISTER v)), pc〉, one〉*)
     273       else
     274        let 〈b,v〉≝  head … v in if b then
     275         let 〈b,v〉≝  head … v in if b then
     276          ?(*〈〈ORL (U1 ACC_A (INDIRECT (from_singl … v))), pc〉, one〉*)
     277         else
     278          let 〈b,v〉≝  head … v in if b then
     279           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ORL (U1 ACC_A (DIRECT b1)), pc〉, one〉*)
     280          else
     281           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ORL (U1 ACC_A (DATA b1)), pc〉, one〉*)
     282        else
     283         let 〈b,v〉≝  head … v in if b then
     284          let 〈b,v〉≝  head … v in if b then
     285           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in ?(*〈〈ORL (U2 (DIRECT b1) (DATA b2)), pc〉, two〉*)
     286          else
     287           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ORL (U2 (DIRECT b1) ACC_A), pc〉, one〉*)
     288         else
     289          let 〈b,v〉≝  head … v in if b then
     290           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, two〉
     291          else
     292           let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JC … (RELATIVE b1)), pc〉, two〉
    301293    else
    302294     let 〈b,v〉≝  head … v in if b then
    303295      let 〈b,v〉≝  head … v in if b then
    304296       let 〈b,v〉≝  head … v in if b then
    305         〈〈ADDC A (REGISTER v), pc〉, one〉
    306        else
    307         let 〈b,v〉≝  head … v in if b then
    308          let 〈b,v〉≝  head … v in if b then
    309           〈〈ADDC A (INDIRECT v), pc〉, one〉
    310          else
    311           let 〈b,v〉≝  head … v in if b then
    312            let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC A (DIRECT b1), pc〉, one〉
    313           else
    314            let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC A (DATA b1), pc〉, one〉
    315         else
    316          let 〈b,v〉≝  head … v in if b then
    317           let 〈b,v〉≝  head … v in if b then
    318            〈〈RLC ACC_A, pc〉, one〉
    319           else
    320            〈〈RETI, pc〉, two〉
    321          else
    322           let 〈b,v〉≝  head … v in if b then
    323              ⊥
    324           else
    325            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈JNB (BIT b1) (REL b2), pc〉, two〉
    326       else
    327        let 〈b,v〉≝  head … v in if b then
    328         〈〈ADD A (REGISTER v), pc〉, one〉
    329        else
    330         let 〈b,v〉≝  head … v in if b then
    331          let 〈b,v〉≝  head … v in if b then
    332           〈〈ADD A (INDIRECT v), pc〉, one〉
    333          else
    334           let 〈b,v〉≝  head … v in if b then
    335            let 〈pc,b1〉≝ next pmem pc in 〈〈ADD A (DIRECT b1), pc〉, one〉
    336           else
    337            let 〈pc,b1〉≝ next pmem pc in 〈〈ADD A (DATA b1), pc〉, one〉
    338         else
    339          let 〈b,v〉≝  head … v in if b then
    340           let 〈b,v〉≝  head … v in if b then
    341            〈〈RL ACC_A, pc〉, one〉
    342           else
    343            〈〈RET, pc〉, two〉
    344          else
    345           let 〈b,v〉≝  head … v in if b then
    346             ⊥
    347           else
    348            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈JB (BIT b1) (REL b2), pc〉, two〉
     297        〈〈ADDC … ACC_A (REGISTER v), pc〉, one〉
     298       else
     299        let 〈b,v〉≝  head … v in if b then
     300         let 〈b,v〉≝  head … v in if b then
     301          〈〈ADDC … ACC_A (INDIRECT (from_singl … v)), pc〉, one〉
     302         else
     303          let 〈b,v〉≝  head … v in if b then
     304           let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC … ACC_A (DIRECT b1), pc〉, one〉
     305          else
     306           let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC … ACC_A (DATA b1), pc〉, one〉
     307        else
     308         let 〈b,v〉≝  head … v in if b then
     309          let 〈b,v〉≝  head … v in if b then
     310           〈〈RLC ACC_A, pc〉, one〉
     311          else
     312           〈〈RETI …, pc〉, two〉
     313         else
     314          let 〈b,v〉≝  head … v in if b then
     315           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, two〉
     316          else
     317           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump … (JNB (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉
     318      else
     319       let 〈b,v〉≝  head … v in if b then
     320        〈〈ADD … ACC_A (REGISTER v), pc〉, one〉
     321       else
     322        let 〈b,v〉≝  head … v in if b then
     323         let 〈b,v〉≝  head … v in if b then
     324          〈〈ADD … ACC_A (INDIRECT (from_singl … v)), pc〉, one〉
     325         else
     326          let 〈b,v〉≝  head … v in if b then
     327           let 〈pc,b1〉≝ next pmem pc in 〈〈ADD … ACC_A (DIRECT b1), pc〉, one〉
     328          else
     329           let 〈pc,b1〉≝ next pmem pc in 〈〈ADD … ACC_A (DATA b1), pc〉, one〉
     330        else
     331         let 〈b,v〉≝  head … v in if b then
     332          let 〈b,v〉≝  head … v in if b then
     333           〈〈RL ACC_A, pc〉, one〉
     334          else
     335           〈〈RET …, pc〉, two〉
     336         else
     337          let 〈b,v〉≝  head … v in if b then
     338           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, two〉
     339          else
     340           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump … (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉
    349341     else
    350342      let 〈b,v〉≝  head … v in if b then
    351343       let 〈b,v〉≝  head … v in if b then
    352         〈〈DEC (REGISTER v), pc〉, one〉
    353        else
    354         let 〈b,v〉≝  head … v in if b then
    355          let 〈b,v〉≝  head … v in if b then
    356           〈〈DEC (INDIRECT v), pc〉, one〉
    357          else
    358           let 〈b,v〉≝  head … v in if b then
    359            let 〈pc,b1〉≝ next pmem pc in 〈〈DEC (DIRECT b1), pc〉, one〉
    360           else
    361            〈〈DEC ACC_A, pc〉, one〉
    362         else
    363          let 〈b,v〉≝  head … v in if b then
    364           let 〈b,v〉≝  head … v in if b then
    365            〈〈RRC ACC_A, pc〉, one〉
    366           else
    367            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LCALL (ADDR16 (mk_word b1 b2)), pc〉, two〉
    368          else
    369           let 〈b,v〉≝  head … v in if b then
    370             ⊥
    371           else
    372            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈JBC (BIT b1) (REL b2), pc〉, two〉
    373       else
    374        let 〈b,v〉≝  head … v in if b then
    375         〈〈INC (REGISTER v), pc〉, one〉
    376        else
    377         let 〈b,v〉≝  head … v in if b then
    378          let 〈b,v〉≝  head … v in if b then
    379           〈〈INC (INDIRECT v), pc〉, one〉
    380          else
    381           let 〈b,v〉≝  head … v in if b then
    382            let 〈pc,b1〉≝ next pmem pc in 〈〈INC (DIRECT b1), pc〉, one〉
    383           else
    384            〈〈INC ACC_A, pc〉, one〉
    385         else
    386          let 〈b,v〉≝  head … v in if b then
    387           let 〈b,v〉≝  head … v in if b then
    388            〈〈RR ACC_A, pc〉, one〉
    389           else
    390            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LJMP (ADDR16 (mk_word b1 b2)), pc〉, two〉
    391          else
    392           let 〈b,v〉≝  head … v in if b then
    393             ⊥
    394           else
    395            〈〈NOP, pc〉, one〉.
     344        〈〈DEC (REGISTER v), pc〉, one〉
     345       else
     346        let 〈b,v〉≝  head … v in if b then
     347         let 〈b,v〉≝  head … v in if b then
     348          〈〈DEC … (INDIRECT (from_singl … v)), pc〉, one〉
     349         else
     350          let 〈b,v〉≝  head … v in if b then
     351           let 〈pc,b1〉≝ next pmem pc in 〈〈DEC (DIRECT b1), pc〉, one〉
     352          else
     353           〈〈DEC ACC_A, pc〉, one〉
     354        else
     355         let 〈b,v〉≝  head … v in if b then
     356          let 〈b,v〉≝  head … v in if b then
     357           〈〈RRC ACC_A, pc〉, one〉
     358          else
     359           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LCALL (ADDR16 (mk_word b1 b2)), pc〉, two〉
     360         else
     361          let 〈b,v〉≝  head … v in if b then
     362           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, two〉
     363          else
     364           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump … (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉
     365      else
     366       let 〈b,v〉≝  head … v in if b then
     367        〈〈INC (REGISTER v), pc〉, one〉
     368       else
     369        let 〈b,v〉≝  head … v in if b then
     370         let 〈b,v〉≝  head … v in if b then
     371          〈〈INC … (INDIRECT (from_singl … v)), pc〉, one〉
     372         else
     373          let 〈b,v〉≝  head … v in if b then
     374           let 〈pc,b1〉≝ next pmem pc in 〈〈INC (DIRECT b1), pc〉, one〉
     375          else
     376           〈〈INC ACC_A, pc〉, one〉
     377        else
     378         let 〈b,v〉≝  head … v in if b then
     379          let 〈b,v〉≝  head … v in if b then
     380           〈〈RR ACC_A, pc〉, one〉
     381          else
     382           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LJMP (ADDR16 (mk_word b1 b2)), pc〉, two〉
     383         else
     384          let 〈b,v〉≝  head … v in if b then
     385           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, two〉
     386          else
     387           〈〈NOP …, pc〉, one〉.
    396388 @.
    397389nqed.
Note: See TracChangeset for help on using the changeset viewer.