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

It starts working...

File:
1 edited

Legend:

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

    r323 r324  
    1818      let 〈b,v〉≝  head … v in if b then
    1919       let 〈b,v〉≝  head … v in if b then
    20         〈〈MOV ? ((Left ?? (Left ?? (Left ?? (Left ?? (Right ?? (? 〈REGISTER v,ACC_A〉))))))), pc〉, one〉
     20        〈〈MOV [[relative]] ((Left ?? (Left ?? (Left ?? (Left ?? (Right ?? (? 〈REGISTER v,ACC_A〉))))))), pc〉, one〉
    2121       else
    2222        let 〈b,v〉≝  head … v in if b then
     
    5959      let 〈b,v〉≝  head … v in if b then
    6060       let 〈b,v〉≝  head … v in if b then
    61         let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (DJNZ (REGISTER v) (RELATIVE b1)), pc〉, two〉
     61        let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (DJNZ [[relative]] (REGISTER v) (RELATIVE b1)), pc〉, two〉
    6262       else
    6363        let 〈b,v〉≝  head … v in if b then
     
    6666         else
    6767          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〉
     68           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump … (DJNZ [[relative]] (DIRECT b1) (RELATIVE b2)), pc〉, two〉
    6969          else
    7070           〈〈DA … ACC_A, pc〉, one〉
     
    155155        let 〈b,v〉≝  head … v in if b then
    156156         let 〈b,v〉≝  head … v in if b then
    157           〈〈SUBB … ACC_A (INDIRECT (from_singg … v)), pc〉, one〉
     157          〈〈SUBB … ACC_A (INDIRECT (from_singl … v)), pc〉, one〉
    158158         else
    159159          let 〈b,v〉≝  head … v in if b then
     
    164164         let 〈b,v〉≝  head … v in if b then
    165165          let 〈b,v〉≝  head … v in if b then
    166            〈〈MOVC … ACC_A (ACC_A_DPTR), pc〉, two〉
     166           〈〈MOVC … ACC_A (ACC_DPTR), pc〉, two〉
    167167          else
    168168           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈MOV (U6 (BIT_ADDR b1) C), pc〉, two〉*)
     
    187187         let 〈b,v〉≝  head … v in if b then
    188188          let 〈b,v〉≝  head … v in if b then
    189            〈〈MOVC … ACC_A (ACC_A_PC), pc〉, two〉
     189           〈〈MOVC … ACC_A (ACC_PC), pc〉, two〉
    190190          else
    191191           let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ANL (U3 C (BIT_ADDR b1)), pc〉, two〉*)
     
    213213         let 〈b,v〉≝  head … v in if b then
    214214          let 〈b,v〉≝  head … v in if b then
    215            〈〈JMP … IND_DPTR, pc〉, two〉
     215           〈〈JMP [[relative]] 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 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 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〉*)
     
    267267           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, two〉
    268268          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
     269           let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JNC [[relative]] (RELATIVE b1)), pc〉, two〉
     270      else
     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 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 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〉
     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〉
    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 ACC_A, pc〉, one〉
     310           〈〈RLC [[relative]] ACC_A, pc〉, one〉
    311311          else
    312312           〈〈RETI …, pc〉, two〉
     
    315315           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, two〉
    316316          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〉
     317           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump … (JNB [[relative]] (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉
    318318      else
    319319       let 〈b,v〉≝  head … v in if b then
     
    338338           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, two〉
    339339          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〉
     340           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump … (JB [[relative]] (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉
    341341     else
    342342      let 〈b,v〉≝  head … v in if b then
    343343       let 〈b,v〉≝  head … v in if b then
    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〉
     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〉
    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 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〉
     357           〈〈RRC [[relative]] ACC_A, pc〉, one〉
     358          else
     359           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LCALL … (ADDR16 (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 [[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〉
    365365      else
    366366       let 〈b,v〉≝  head … v in if b then
     
    380380           〈〈RR … ACC_A, pc〉, one〉
    381381          else
    382            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LJMP … (ADDR16 (mk_word b1 b2)), pc〉, two〉
     382           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, two〉
    383383         else
    384384          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 , pc〉, one〉.
     387           〈〈NOP [[relative]], pc〉, one〉.
    388388 @.
    389389nqed.
Note: See TracChangeset for help on using the changeset viewer.