Changeset 303


Ignore:
Timestamp:
Nov 25, 2010, 11:41:15 PM (9 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

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

    r302 r303  
    200200          [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ]         
    201201      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    202 (*
     202  | MOV addrs ⇒
     203     match addrs with
     204      [ Left addrs ⇒
     205         match addrs with
     206          [ Left addrs ⇒
     207             match addrs with
     208              [ Left addrs ⇒
     209                 match addrs with
     210                  [ Left addrs ⇒
     211                     match addrs with
     212                      [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     213[] (*
    203214  | `MOV (`U1 (`A, `REG(r1,r2,r3))) ->
    204215    [mk_byte_from_bits ((true,true,true,false),(true,r1,r2,r3))]
     
    209220  | `MOV (`U1 (`A, `DATA b1)) ->
    210221    [mk_byte_from_bits ((false,true,true,true),(false,true,false,false)); b1]
     222*)
     223                      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     224[] (*
    211225  | `MOV (`U2 (`REG(r1,r2,r3), `A)) ->
    212226    [mk_byte_from_bits ((true,true,true,true),(true,r1,r2,r3))]
     
    215229  | `MOV (`U2 (`REG(r1,r2,r3), (`DATA b1))) ->
    216230    [mk_byte_from_bits ((false,true,true,true),(true,r1,r2,r3)); b1]
     231  | `MOV (`U2 (`INDIRECT i1, `A)) ->
     232    [mk_byte_from_bits ((true,true,true,true),(false,true,true,i1))]
     233  | `MOV (`U2 (`INDIRECT i1, `DIRECT b1)) ->
     234    [mk_byte_from_bits ((true,false,true,false),(false,true,true,i1)); b1]
     235  | `MOV (`U2 (`INDIRECT i1, `DATA b1)) ->
     236    [mk_byte_from_bits ((false,true,true,true),(false,true,true,i1)); b1]
     237
     238*)
     239                      ]
     240                  | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     241[] (*
    217242  | `MOV (`U3 (`DIRECT b1, `A)) ->
    218243    [mk_byte_from_bits ((true,true,true,true),(false,true,false,true)); b1]
     
    225250  | `MOV (`U3 (`DIRECT b1, `DATA b2)) ->
    226251    [mk_byte_from_bits ((false,true,true,true),(false,true,false,true)); b1; b2]
    227   | `MOV (`U2 (`INDIRECT i1, `A)) ->
    228     [mk_byte_from_bits ((true,true,true,true),(false,true,true,i1))]
    229   | `MOV (`U2 (`INDIRECT i1, `DIRECT b1)) ->
    230     [mk_byte_from_bits ((true,false,true,false),(false,true,true,i1)); b1]
    231   | `MOV (`U2 (`INDIRECT i1, `DATA b1)) ->
    232     [mk_byte_from_bits ((false,true,true,true),(false,true,true,i1)); b1]
    233   | `MOV (`U5 (`C, `BIT b1)) ->
    234     [mk_byte_from_bits ((true,false,true,false),(false,false,true,false)); b1]
    235   | `MOV (`U6 (`BIT b1, `C)) ->
    236     [mk_byte_from_bits ((true,false,false,true),(false,false,true,false)); b1]
     252*)
     253                  ]
     254              | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     255[] (*
    237256  | `MOV (`U4 (`DPTR, `DATA16 w)) ->
    238257    let (b1,b2) = from_word w in
    239258      [mk_byte_from_bits ((true,false,false,true),(false,false,false,false)); b1; b2]
     259*)           
     260              ]
     261          | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     262[] (*
     263  | `MOV (`U5 (`C, `BIT b1)) ->
     264    [mk_byte_from_bits ((true,false,true,false),(false,false,true,false)); b1]
    240265*)
     266          ]
     267      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     268[] (*
     269  | `MOV (`U6 (`BIT b1, `C)) ->
     270    [mk_byte_from_bits ((true,false,false,true),(false,false,true,false)); b1]   
     271*)
     272      ]
    241273  | MOVC addr1 addr2 ⇒
    242274     match addr2 return λx. bool_to_Prop (is_in ? [[acc_dptr;acc_pc]] x) → ? with
Note: See TracChangeset for help on using the changeset viewer.