Changeset 325


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

Almost finished.

File:
1 edited

Legend:

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

    r324 r325  
    1818      let 〈b,v〉≝  head … v in if b then
    1919       let 〈b,v〉≝  head … v in if b then
    20         〈〈MOV [[relative]] ((Left ?? (Left ?? (Left ?? (Left ?? (Right ?? (? 〈REGISTER v,ACC_A〉))))))), pc〉, one〉
     20        〈〈MOV ((Left ?? (Left ?? (Left ?? (Left ?? (Right ?? (? 〈REGISTER v,ACC_A〉))))))), pc〉, one〉
    2121       else
    2222        let 〈b,v〉≝  head … v in if b then
     
    213213         let 〈b,v〉≝  head … v in if b then
    214214          let 〈b,v〉≝  head … v in if b then
    215            〈〈JMP [[relative]] INDIRECT_DPTR, pc〉, two〉
     215           〈〈JMP INDIRECT_DPTR, pc〉, two〉
    216216          else
    217217           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ORL (U3 C (BIT_ADDR b1)), pc〉, two〉*)
    218218         else
    219           ? (*let 〈b,v〉≝  head … v in if b then
     219          let 〈b,v〉≝  head … v in if b then
    220220           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, two〉
    221221          else
    222            let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JNZ [[relative]] (RELATIVE b1)), pc〉, two〉 *)
    223       else
    224        ?(*let 〈b,v〉≝  head … v in if b then
     222           let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JNZ [[relative]] (RELATIVE b1)), pc〉, two〉
     223      else
     224       let 〈b,v〉≝  head … v in if b then
    225225        ?(*〈〈XRL(U1 ACC_A (REGISTER v)), pc〉, one〉*)
    226226       else
     
    243243           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, two〉
    244244          else
    245            let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JZ [[relative]] (RELATIVE b1)), pc〉, two〉*)
     245           let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JZ [[relative]] (RELATIVE b1)), pc〉, two〉
    246246     else
    247       ?(*let 〈b,v〉≝  head … v in if b then
     247      let 〈b,v〉≝  head … v in if b then
    248248       let 〈b,v〉≝  head … v in if b then
    249249        ?(*〈〈ANL (U1 ACC_A (REGISTER v)), pc〉, one〉*)
     
    269269           let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JNC [[relative]] (RELATIVE b1)), pc〉, two〉
    270270      else
    271        ?(*let 〈b,v〉≝  head … v in if b then
     271       let 〈b,v〉≝  head … v in if b then
    272272        ?(*〈〈ORL (U1 ACC_A (REGISTER v)), pc〉, one〉*)
    273273       else
     
    290290           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, two〉
    291291          else
    292            let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JC [[relative]] (RELATIVE b1)), pc〉, two〉*)*)
     292           let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JC [[relative]] (RELATIVE b1)), pc〉, two〉
    293293    else
    294294     let 〈b,v〉≝  head … v in if b then
    295295      let 〈b,v〉≝  head … v in if b then
    296296       let 〈b,v〉≝  head … v in if b then
    297         〈〈ADDC [[relative]] 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 [[relative]] ACC_A (INDIRECT (from_singl … v)), pc〉, one〉
     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〉
    302302         else
    303303          let 〈b,v〉≝  head … v in if b then
     
    308308         let 〈b,v〉≝  head … v in if b then
    309309          let 〈b,v〉≝  head … v in if b then
    310            〈〈RLC [[relative]] ACC_A, pc〉, one〉
     310           〈〈RLC ACC_A, pc〉, one〉
    311311          else
    312312           〈〈RETI …, pc〉, two〉
     
    342342      let 〈b,v〉≝  head … v in if b then
    343343       let 〈b,v〉≝  head … v in if b then
    344         〈〈DEC [[relative]] (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 [[relative]] (INDIRECT (from_singl … v)), 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〉
    349349         else
    350350          let 〈b,v〉≝  head … v in if b then
     
    355355         let 〈b,v〉≝  head … v in if b then
    356356          let 〈b,v〉≝  head … v in if b then
    357            〈〈RRC [[relative]] ACC_A, pc〉, one〉
     357           〈〈RRC ACC_A, pc〉, one〉
    358358          else
    359359           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, two〉
    360360         else
    361361          let 〈b,v〉≝  head … v in if b then
    362            let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP [[relative]] (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 [[relative]] (JBC [[relative]] (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉
     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 [[relative]] (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉
    365365      else
    366366       let 〈b,v〉≝  head … v in if b then
     
    385385           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, two〉
    386386          else
    387            〈〈NOP [[relative]], pc〉, one〉.
     387           〈〈NOP , pc〉, one〉.
    388388 @.
    389389nqed.
Note: See TracChangeset for help on using the changeset viewer.