Changeset 820 for src/ASM/Fetch.ma


Ignore:
Timestamp:
May 20, 2011, 6:09:00 PM (9 years ago)
Author:
mulligan
Message:

changes to get the semantics of pseudoassembly working

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Fetch.ma

    r712 r820  
    2020      let 〈b,v〉 ≝ head … v in if b then
    2121       let 〈b,v〉 ≝ head … v in if b then
    22         〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,ACC_A〉))))), pc〉, 1〉
    23        else
    24         let 〈b,v〉≝  head … v in if b then
    25          let 〈b,v〉≝  head … v in if b then
    26           〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),ACC_A〉))))), pc〉, 1〉
    27          else
    28           let 〈b,v〉≝  head … v in if b then
    29            let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉)))), pc〉, 1〉
     22        〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,ACC_A〉)))))), pc〉, 1〉
     23       else
     24        let 〈b,v〉≝  head … v in if b then
     25         let 〈b,v〉≝  head … v in if b then
     26          〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),ACC_A〉)))))), pc〉, 1〉
     27         else
     28          let 〈b,v〉≝  head … v in if b then
     29           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉))))), pc〉, 1〉
    3030          else
    3131           〈〈CPL … ACC_A, pc〉, 1〉
    3232        else
    3333         let 〈b,v〉≝  head … v in if b then
    34           〈〈MOVX … (inr … 〈EXT_INDIRECT (from_singl … v),ACC_A〉), pc〉, 2〉
     34          〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT (from_singl … v),ACC_A〉)), pc〉, 2〉
    3535         else
    3636          let 〈b,v〉≝  head … v in if b then
    3737           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
    3838          else
    39            〈〈MOVX … (inr … 〈EXT_INDIRECT_DPTR,ACC_A〉), pc〉, 2〉
    40       else
    41        let 〈b,v〉≝  head … v in if b then
    42         〈〈MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,REGISTER v〉))))), pc〉, 1〉
    43        else
    44         let 〈b,v〉≝  head … v in if b then
    45          let 〈b,v〉≝  head … v in if b then
    46           〈〈MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))))), pc〉, 1〉
    47          else
    48           let 〈b,v〉≝  head … v in if b then
    49            let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DIRECT b1〉))))), pc〉, 1〉
    50           else
    51            〈〈CLR … ACC_A, pc〉, 1〉
    52         else
    53          let 〈b,v〉≝  head … v in if b then
    54           〈〈MOVX … (inl … 〈ACC_A,EXT_INDIRECT (from_singl … v)〉), pc〉, 2〉
     39           〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT_DPTR,ACC_A〉)), pc〉, 2〉
     40      else
     41       let 〈b,v〉≝  head … v in if b then
     42        〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,REGISTER v〉)))))), pc〉, 1〉
     43       else
     44        let 〈b,v〉≝  head … v in if b then
     45         let 〈b,v〉≝  head … v in if b then
     46          〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)))))), pc〉, 1〉
     47         else
     48          let 〈b,v〉≝  head … v in if b then
     49           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DIRECT b1〉)))))), pc〉, 1〉
     50          else
     51           〈〈RealInstruction (CLR … ACC_A), pc〉, 1〉
     52        else
     53         let 〈b,v〉≝  head … v in if b then
     54          〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT (from_singl … v)〉)), pc〉, 2〉
    5555         else
    5656          let 〈b,v〉≝  head … v in if b then
    5757           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
    5858          else
    59            〈〈MOVX … (inl … 〈ACC_A,EXT_INDIRECT_DPTR〉), pc〉, 2〉
     59           〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT_DPTR〉)), pc〉, 2〉
    6060     else
    6161      let 〈b,v〉≝  head … v in if b then
    6262       let 〈b,v〉≝  head … v in if b then
    63         let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉
    64        else
    65         let 〈b,v〉≝  head … v in if b then
    66          let 〈b,v〉≝  head … v in if b then
    67           〈〈XCHD … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉
    68          else
    69           let 〈b,v〉≝  head … v in if b then
    70            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉
    71           else
    72            〈〈DA … ACC_A, pc〉, 1〉
    73         else
    74          let 〈b,v〉≝  head … v in if b then
    75           let 〈b,v〉≝  head … v in if b then
    76            〈〈SETB … CARRY, pc〉, 1〉
    77           else
    78            let 〈pc,b1〉≝ next pmem pc in 〈〈SETB … (BIT_ADDR b1), pc〉, 1〉
     63        let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉
     64       else
     65        let 〈b,v〉≝  head … v in if b then
     66         let 〈b,v〉≝  head … v in if b then
     67          〈〈RealInstruction (XCHD … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
     68         else
     69          let 〈b,v〉≝  head … v in if b then
     70           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉
     71          else
     72           〈〈RealInstruction (DA … ACC_A), pc〉, 1〉
     73        else
     74         let 〈b,v〉≝  head … v in if b then
     75          let 〈b,v〉≝  head … v in if b then
     76           〈〈RealInstruction (SETB … CARRY), pc〉, 1〉
     77          else
     78           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (SETB … (BIT_ADDR b1)), pc〉, 1〉
    7979         else
    8080          let 〈b,v〉≝  head … v in if b then
    8181           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
    8282          else
    83            let 〈pc,b1〉≝ next pmem pc in 〈〈POP … (DIRECT b1), pc〉, 2〉
    84       else
    85        let 〈b,v〉≝  head … v in if b then
    86         〈〈XCH … ACC_A (REGISTER v), pc〉, 1〉
    87        else
    88         let 〈b,v〉≝  head … v in if b then
    89          let 〈b,v〉≝  head … v in if b then
    90           〈〈XCH … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉
    91          else
    92           let 〈b,v〉≝  head … v in if b then
    93            let 〈pc,b1〉≝ next pmem pc in 〈〈XCH … ACC_A (DIRECT b1), pc〉, 1〉
    94           else
    95            〈〈SWAP … ACC_A, pc〉, 1〉
    96         else
    97          let 〈b,v〉≝  head … v in if b then
    98           let 〈b,v〉≝  head … v in if b then
    99            〈〈CLR … CARRY, pc〉, 1〉
    100           else
    101            let 〈pc,b1〉≝ next pmem pc in 〈〈CLR … (BIT_ADDR b1), pc〉, 1〉
     83           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (POP … (DIRECT b1)), pc〉, 2〉
     84      else
     85       let 〈b,v〉≝  head … v in if b then
     86        〈〈RealInstruction (XCH … ACC_A (REGISTER v)), pc〉, 1〉
     87       else
     88        let 〈b,v〉≝  head … v in if b then
     89         let 〈b,v〉≝  head … v in if b then
     90          〈〈RealInstruction (XCH … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
     91         else
     92          let 〈b,v〉≝  head … v in if b then
     93           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (XCH … ACC_A (DIRECT b1)), pc〉, 1〉
     94          else
     95           〈〈RealInstruction (SWAP … ACC_A), pc〉, 1〉
     96        else
     97         let 〈b,v〉≝  head … v in if b then
     98          let 〈b,v〉≝  head … v in if b then
     99           〈〈RealInstruction (CLR … CARRY), pc〉, 1〉
     100          else
     101           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (CLR … (BIT_ADDR b1)), pc〉, 1〉
    102102         else
    103103          let 〈b,v〉≝  head … v in if b then
    104104           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
    105105          else
    106            let 〈pc,b1〉≝ next pmem pc in 〈〈PUSH … (DIRECT b1), pc〉, 2〉
     106           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (PUSH … (DIRECT b1)), pc〉, 2〉
    107107    else
    108108     let 〈b,v〉≝  head … v in if b then
    109109      let 〈b,v〉≝  head … v in if b then
    110110       let 〈b,v〉≝  head … v in if b then
    111         let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE …  (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
    112        else
    113         let 〈b,v〉≝  head … v in if b then
    114          let 〈b,v〉≝  head … v in if b then
    115           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉
    116          else
    117           let 〈b,v〉≝  head … v in if b then
    118            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE …  (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉
    119           else
    120            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
    121         else
    122          let 〈b,v〉≝  head … v in if b then
    123           let 〈b,v〉≝  head … v in if b then
    124            〈〈CPL … CARRY, pc〉, 1〉
    125           else
    126            let 〈pc,b1〉≝ next pmem pc in 〈〈CPL … (BIT_ADDR b1), pc〉, 1〉
     111        let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (CJNE …  (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
     112       else
     113        let 〈b,v〉≝  head … v in if b then
     114         let 〈b,v〉≝  head … v in if b then
     115          let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉
     116         else
     117          let 〈b,v〉≝  head … v in if b then
     118           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (CJNE …  (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉
     119          else
     120           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
     121        else
     122         let 〈b,v〉≝  head … v in if b then
     123          let 〈b,v〉≝  head … v in if b then
     124           〈〈RealInstruction (CPL … CARRY), pc〉, 1〉
     125          else
     126           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (CPL … (BIT_ADDR b1)), pc〉, 1〉
    127127         else
    128128          let 〈b,v〉≝  head … v in if b then
    129129           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
    130130          else
    131            let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉), pc〉, 2〉
    132       else
    133        let 〈b,v〉≝  head … v in if b then
    134         let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉))))), pc〉, 2〉
    135        else
    136         let 〈b,v〉≝  head … v in if b then
    137          let 〈b,v〉≝  head … v in if b then
    138           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉))))), pc〉, 2〉
    139          else
    140           〈〈MUL … ACC_A ACC_B, pc〉, 4〉
    141         else
    142          let 〈b,v〉≝  head … v in if b then
    143           let 〈b,v〉≝  head … v in if b then
    144            〈〈INC … DPTR, pc〉, 2〉
    145           else
    146            let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 1〉
     131           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
     132      else
     133       let 〈b,v〉≝  head … v in if b then
     134        let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉)))))), pc〉, 2〉
     135       else
     136        let 〈b,v〉≝  head … v in if b then
     137         let 〈b,v〉≝  head … v in if b then
     138          let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉)))))), pc〉, 2〉
     139         else
     140          〈〈RealInstruction (MUL … ACC_A ACC_B), pc〉, 4〉
     141        else
     142         let 〈b,v〉≝  head … v in if b then
     143          let 〈b,v〉≝  head … v in if b then
     144           〈〈RealInstruction (INC … DPTR), pc〉, 2〉
     145          else
     146           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉))), pc〉, 1〉
    147147         else
    148148          let 〈b,v〉≝  head … v in if b then
    149149           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
    150150          else
    151            let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉), pc〉, 2〉
     151           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
    152152     else
    153153      let 〈b,v〉≝  head … v in if b then
    154154       let 〈b,v〉≝  head … v in if b then
    155         〈〈SUBB … ACC_A (REGISTER v), pc〉, 1〉
    156        else
    157         let 〈b,v〉≝  head … v in if b then
    158          let 〈b,v〉≝  head … v in if b then
    159           〈〈SUBB … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉
    160          else
    161           let 〈b,v〉≝  head … v in if b then
    162            let 〈pc,b1〉≝ next pmem pc in 〈〈SUBB … ACC_A (DIRECT b1), pc〉, 1〉
    163           else
    164            let 〈pc,b1〉≝ next pmem pc in 〈〈SUBB … ACC_A (DATA b1), pc〉, 1〉
     155        〈〈RealInstruction (SUBB … ACC_A (REGISTER v)), pc〉, 1〉
     156       else
     157        let 〈b,v〉≝  head … v in if b then
     158         let 〈b,v〉≝  head … v in if b then
     159          〈〈RealInstruction (SUBB … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
     160         else
     161          let 〈b,v〉≝  head … v in if b then
     162           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (SUBB … ACC_A (DIRECT b1)), pc〉, 1〉
     163          else
     164           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (SUBB … ACC_A (DATA b1)), pc〉, 1〉
    165165        else
    166166         let 〈b,v〉≝  head … v in if b then
     
    168168           〈〈MOVC … ACC_A (ACC_DPTR), pc〉, 2〉
    169169          else
    170            let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inr … 〈BIT_ADDR b1,CARRY〉), pc〉, 2〉
     170           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inr … 〈BIT_ADDR b1,CARRY〉)), pc〉, 2〉
    171171         else
    172172          let 〈b,v〉≝  head … v in if b then
    173173           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
    174174          else
    175            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉))), pc〉, 2〉
    176       else
    177        let 〈b,v〉≝  head … v in if b then
    178         let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉)))), pc〉, 2〉
    179        else
    180         let 〈b,v〉≝  head … v in if b then
    181          let 〈b,v〉≝  head … v in if b then
    182           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉)))), pc〉, 2〉
    183          else
    184           let 〈b,v〉≝  head … v in if b then
    185            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉)))), pc〉, 2〉
    186           else
    187            〈〈DIV … ACC_A ACC_B, pc〉, 4〉
     175           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉)))), pc〉, 2〉
     176      else
     177       let 〈b,v〉≝  head … v in if b then
     178        let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉))))), pc〉, 2〉
     179       else
     180        let 〈b,v〉≝  head … v in if b then
     181         let 〈b,v〉≝  head … v in if b then
     182          let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉))))), pc〉, 2〉
     183         else
     184          let 〈b,v〉≝  head … v in if b then
     185           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉))))), pc〉, 2〉
     186          else
     187           〈〈RealInstruction (DIV … ACC_A ACC_B), pc〉, 4〉
    188188        else
    189189         let 〈b,v〉≝  head … v in if b then
     
    191191           〈〈MOVC … ACC_A (ACC_PC), pc〉, 2〉
    192192          else
    193            let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (inr … 〈CARRY,BIT_ADDR b1〉), pc〉, 2〉
     193           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
    194194         else
    195195          let 〈b,v〉≝  head … v in if b then
     
    202202      let 〈b,v〉≝  head … v in if b then
    203203       let 〈b,v〉≝  head … v in if b then
    204         let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DATA b1〉))))), pc〉, 1〉
    205        else
    206         let 〈b,v〉≝  head … v in if b then
    207          let 〈b,v〉≝  head … v in if b then
    208           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉))))), pc〉, 1〉
    209          else
    210           let 〈b,v〉≝  head … v in if b then
    211            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉)))), pc〉, 3〉
    212           else
    213            let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉))))), pc〉, 1〉
     204        let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DATA b1〉)))))), pc〉, 1〉
     205       else
     206        let 〈b,v〉≝  head … v in if b then
     207         let 〈b,v〉≝  head … v in if b then
     208          let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉)))))), pc〉, 1〉
     209         else
     210          let 〈b,v〉≝  head … v in if b then
     211           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉))))), pc〉, 3〉
     212          else
     213           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉)))))), pc〉, 1〉
    214214        else
    215215         let 〈b,v〉≝  head … v in if b then
     
    217217           〈〈JMP … INDIRECT_DPTR, pc〉, 2〉
    218218          else
    219            let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (inr … 〈CARRY,BIT_ADDR b1〉), pc〉, 2〉
     219           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
    220220         else
    221221          let 〈b,v〉≝  head … v in if b then
    222222           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
    223223          else
    224            let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JNZ … (RELATIVE b1)), pc〉, 2〉
    225       else
    226        let 〈b,v〉≝  head … v in if b then
    227         〈〈XRL … (inl … 〈ACC_A,REGISTER v〉), pc〉, 1〉
    228        else
    229         let 〈b,v〉≝  head … v in if b then
    230          let 〈b,v〉≝  head … v in if b then
    231           〈〈XRL … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉), pc〉, 1〉
    232          else
    233           let 〈b,v〉≝  head … v in if b then
    234            let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … (inl … 〈ACC_A,DIRECT b1〉), pc〉, 1〉
    235           else
    236            let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … (inl … 〈ACC_A,DATA b1〉), pc〉, 1〉
    237         else
    238          let 〈b,v〉≝  head … v in if b then
    239           let 〈b,v〉≝  head … v in if b then
    240            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈XRL … (inr … 〈DIRECT b1,DATA b2〉), pc〉, 2〉
    241           else
    242            let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … (inr … 〈DIRECT b1,ACC_A〉), pc〉, 1〉
     224           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (JNZ … (RELATIVE b1)), pc〉, 2〉
     225      else
     226       let 〈b,v〉≝  head … v in if b then
     227        〈〈RealInstruction (XRL … (inl … 〈ACC_A,REGISTER v〉)), pc〉, 1〉
     228       else
     229        let 〈b,v〉≝  head … v in if b then
     230         let 〈b,v〉≝  head … v in if b then
     231          〈〈RealInstruction (XRL … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, 1〉
     232         else
     233          let 〈b,v〉≝  head … v in if b then
     234           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉
     235          else
     236           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉
     237        else
     238         let 〈b,v〉≝  head … v in if b then
     239          let 〈b,v〉≝  head … v in if b then
     240           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉
     241          else
     242           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉
    243243         else
    244244          let 〈b,v〉≝  head … v in if b then
    245245           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
    246246          else
    247            let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JZ … (RELATIVE b1)), pc〉, 2〉
     247           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (JZ … (RELATIVE b1)), pc〉, 2〉
    248248     else
    249249      let 〈b,v〉≝  head … v in if b then
    250250       let 〈b,v〉≝  head … v in if b then
    251         〈〈ANL … (inl … (inl … 〈ACC_A,REGISTER v〉)), pc〉, 1〉
    252        else
    253         let 〈b,v〉≝  head … v in if b then
    254          let 〈b,v〉≝  head … v in if b then
    255           〈〈ANL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, 1〉
    256          else
    257           let 〈b,v〉≝  head … v in if b then
    258            let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉
    259           else
    260            let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (inl … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉
    261         else
    262          let 〈b,v〉≝  head … v in if b then
    263           let 〈b,v〉≝  head … v in if b then
    264            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉
    265           else
    266            let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉
     251        〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,REGISTER v〉))), pc〉, 1〉
     252       else
     253        let 〈b,v〉≝  head … v in if b then
     254         let 〈b,v〉≝  head … v in if b then
     255          〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))), pc〉, 1〉
     256         else
     257          let 〈b,v〉≝  head … v in if b then
     258           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
     259          else
     260           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
     261        else
     262         let 〈b,v〉≝  head … v in if b then
     263          let 〈b,v〉≝  head … v in if b then
     264           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
     265          else
     266           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
    267267         else
    268268          let 〈b,v〉≝  head … v in if b then
    269269           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
    270270          else
    271            let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JNC … (RELATIVE b1)), pc〉, 2〉
    272       else
    273        let 〈b,v〉≝  head … v in if b then
    274         〈〈ORL … (inl … (inl … 〈ACC_A,REGISTER v〉)), pc〉, 1〉
    275        else
    276         let 〈b,v〉≝  head … v in if b then
    277          let 〈b,v〉≝  head … v in if b then
    278           〈〈ORL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, 1〉
    279          else
    280           let 〈b,v〉≝  head … v in if b then
    281            let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉
    282           else
    283            let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (inl … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉
    284         else
    285          let 〈b,v〉≝  head … v in if b then
    286           let 〈b,v〉≝  head … v in if b then
    287            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉
    288           else
    289            let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉
     271           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (JNC … (RELATIVE b1)), pc〉, 2〉
     272      else
     273       let 〈b,v〉≝  head … v in if b then
     274        〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,REGISTER v〉))), pc〉, 1〉
     275       else
     276        let 〈b,v〉≝  head … v in if b then
     277         let 〈b,v〉≝  head … v in if b then
     278          〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))), pc〉, 1〉
     279         else
     280          let 〈b,v〉≝  head … v in if b then
     281           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
     282          else
     283           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
     284        else
     285         let 〈b,v〉≝  head … v in if b then
     286          let 〈b,v〉≝  head … v in if b then
     287           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
     288          else
     289           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
    290290         else
    291291          let 〈b,v〉≝  head … v in if b then
    292292           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
    293293          else
    294            let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JC … (RELATIVE b1)), pc〉, 2〉
     294           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (JC … (RELATIVE b1)), pc〉, 2〉
    295295    else
    296296     let 〈b,v〉≝  head … v in if b then
    297297      let 〈b,v〉≝  head … v in if b then
    298298       let 〈b,v〉≝  head … v in if b then
    299         〈〈ADDC … ACC_A (REGISTER v), pc〉, 1〉
    300        else
    301         let 〈b,v〉≝  head … v in if b then
    302          let 〈b,v〉≝  head … v in if b then
    303           〈〈ADDC … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉
    304          else
    305           let 〈b,v〉≝  head … v in if b then
    306            let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC … ACC_A (DIRECT b1), pc〉, 1〉
    307           else
    308            let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC … ACC_A (DATA b1), pc〉, 1〉
    309         else
    310          let 〈b,v〉≝  head … v in if b then
    311           let 〈b,v〉≝  head … v in if b then
    312            〈〈RLC … ACC_A, pc〉, 1〉
    313           else
    314            〈〈RETI …, pc〉, 2〉
     299        〈〈RealInstruction (ADDC … ACC_A (REGISTER v)), pc〉, 1〉
     300       else
     301        let 〈b,v〉≝  head … v in if b then
     302         let 〈b,v〉≝  head … v in if b then
     303          〈〈RealInstruction (ADDC … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
     304         else
     305          let 〈b,v〉≝  head … v in if b then
     306           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DIRECT b1)), pc〉, 1〉
     307          else
     308           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ADDC … ACC_A (DATA b1)), pc〉, 1〉
     309        else
     310         let 〈b,v〉≝  head … v in if b then
     311          let 〈b,v〉≝  head … v in if b then
     312           〈〈RealInstruction (RLC … ACC_A), pc〉, 1〉
     313          else
     314           〈〈RealInstruction (RETI …), pc〉, 2〉
    315315         else
    316316          let 〈b,v〉≝  head … v in if b then
    317317           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
    318318          else
    319            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
    320       else
    321        let 〈b,v〉≝  head … v in if b then
    322         〈〈ADD … ACC_A (REGISTER v), pc〉, 1〉
    323        else
    324         let 〈b,v〉≝  head … v in if b then
    325          let 〈b,v〉≝  head … v in if b then
    326           〈〈ADD … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉
    327          else
    328           let 〈b,v〉≝  head … v in if b then
    329            let 〈pc,b1〉≝ next pmem pc in 〈〈ADD … ACC_A (DIRECT b1), pc〉, 1〉
    330           else
    331            let 〈pc,b1〉≝ next pmem pc in 〈〈ADD … ACC_A (DATA b1), pc〉, 1〉
    332         else
    333          let 〈b,v〉≝  head … v in if b then
    334           let 〈b,v〉≝  head … v in if b then
    335            〈〈RL … ACC_A, pc〉, 1〉
    336           else
    337            〈〈RET …, pc〉, 2〉
     319           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
     320      else
     321       let 〈b,v〉≝  head … v in if b then
     322        〈〈RealInstruction (ADD … ACC_A (REGISTER v)), pc〉, 1〉
     323       else
     324        let 〈b,v〉≝  head … v in if b then
     325         let 〈b,v〉≝  head … v in if b then
     326          〈〈RealInstruction (ADD … ACC_A (INDIRECT (from_singl … v))), pc〉, 1〉
     327         else
     328          let 〈b,v〉≝  head … v in if b then
     329           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DIRECT b1)), pc〉, 1〉
     330          else
     331           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (ADD … ACC_A (DATA b1)), pc〉, 1〉
     332        else
     333         let 〈b,v〉≝  head … v in if b then
     334          let 〈b,v〉≝  head … v in if b then
     335           〈〈RealInstruction (RL … ACC_A), pc〉, 1〉
     336          else
     337           〈〈RealInstruction (RET …), pc〉, 2〉
    338338         else
    339339          let 〈b,v〉≝  head … v in if b then
    340340           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
    341341          else
    342            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
     342           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
    343343     else
    344344      let 〈b,v〉≝  head … v in if b then
    345345       let 〈b,v〉≝  head … v in if b then
    346         〈〈DEC … (REGISTER v), pc〉, 1〉
    347        else
    348         let 〈b,v〉≝  head … v in if b then
    349          let 〈b,v〉≝  head … v in if b then
    350           〈〈DEC … (INDIRECT (from_singl … v)), pc〉, 1〉
    351          else
    352           let 〈b,v〉≝  head … v in if b then
    353            let 〈pc,b1〉≝ next pmem pc in 〈〈DEC … (DIRECT b1), pc〉, 1〉
    354           else
    355            〈〈DEC … ACC_A, pc〉, 1〉
    356         else
    357          let 〈b,v〉≝  head … v in if b then
    358           let 〈b,v〉≝  head … v in if b then
    359            〈〈RRC … ACC_A, pc〉, 1〉
     346        〈〈RealInstruction (DEC … (REGISTER v)), pc〉, 1〉
     347       else
     348        let 〈b,v〉≝  head … v in if b then
     349         let 〈b,v〉≝  head … v in if b then
     350          〈〈RealInstruction (DEC … (INDIRECT (from_singl … v))), pc〉, 1〉
     351         else
     352          let 〈b,v〉≝  head … v in if b then
     353           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (DEC … (DIRECT b1)), pc〉, 1〉
     354          else
     355           〈〈RealInstruction (DEC … ACC_A), pc〉, 1〉
     356        else
     357         let 〈b,v〉≝  head … v in if b then
     358          let 〈b,v〉≝  head … v in if b then
     359           〈〈RealInstruction (RRC … ACC_A), pc〉, 1〉
    360360          else
    361361           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉
     
    364364           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
    365365          else
    366            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
    367       else
    368        let 〈b,v〉≝  head … v in if b then
    369         〈〈INC … (REGISTER v), pc〉, 1〉
    370        else
    371         let 〈b,v〉≝  head … v in if b then
    372          let 〈b,v〉≝  head … v in if b then
    373           〈〈INC … (INDIRECT (from_singl … v)), pc〉, 1〉
    374          else
    375           let 〈b,v〉≝  head … v in if b then
    376            let 〈pc,b1〉≝ next pmem pc in 〈〈INC … (DIRECT b1), pc〉, 1〉
    377           else
    378            〈〈INC … ACC_A, pc〉, 1〉
    379         else
    380          let 〈b,v〉≝  head … v in if b then
    381           let 〈b,v〉≝  head … v in if b then
    382            〈〈RR … ACC_A, pc〉, 1〉
     366           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈RealInstruction (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
     367      else
     368       let 〈b,v〉≝  head … v in if b then
     369        〈〈RealInstruction (INC … (REGISTER v)), pc〉, 1〉
     370       else
     371        let 〈b,v〉≝  head … v in if b then
     372         let 〈b,v〉≝  head … v in if b then
     373          〈〈RealInstruction (INC … (INDIRECT (from_singl … v))), pc〉, 1〉
     374         else
     375          let 〈b,v〉≝  head … v in if b then
     376           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (INC … (DIRECT b1)), pc〉, 1〉
     377          else
     378           〈〈RealInstruction (INC … ACC_A), pc〉, 1〉
     379        else
     380         let 〈b,v〉≝  head … v in if b then
     381          let 〈b,v〉≝  head … v in if b then
     382           〈〈RealInstruction (RR … ACC_A), pc〉, 1〉
    383383          else
    384384           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉
     
    387387           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
    388388          else
    389            〈〈NOP …, pc〉, 1〉.
     389           〈〈RealInstruction (NOP …), pc〉, 1〉.
    390390  %.
    391391qed.
Note: See TracChangeset for help on using the changeset viewer.