Changeset 306


Ignore:
Timestamp:
Nov 26, 2010, 12:19:42 AM (9 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

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

    r305 r306  
    218218                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    219219                      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    220 [] (*
    221   | `MOV (`U2 (`REG(r1,r2,r3), `A)) ->
    222     [mk_byte_from_bits ((true,true,true,true),(true,r1,r2,r3))]
    223   | `MOV (`U2 (`REG(r1,r2,r3), (`DIRECT b1))) ->
    224     [mk_byte_from_bits ((true,false,true,false),(true,r1,r2,r3)); b1]
    225   | `MOV (`U2 (`REG(r1,r2,r3), (`DATA b1))) ->
    226     [mk_byte_from_bits ((false,true,true,true),(true,r1,r2,r3)); b1]
    227 
    228   | `MOV (`U2 (`INDIRECT i1, `A)) ->
    229     [mk_byte_from_bits ((true,true,true,true),(false,true,true,i1))]
    230   | `MOV (`U2 (`INDIRECT i1, `DIRECT b1)) ->
    231     [mk_byte_from_bits ((true,false,true,false),(false,true,true,i1)); b1]
    232   | `MOV (`U2 (`INDIRECT i1, `DATA b1)) ->
    233     [mk_byte_from_bits ((false,true,true,true),(false,true,true,i1)); b1]
    234 
    235 *)
    236                       ]
     220                         match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → ? with
     221                          [ REGISTER r1 r2 r3 ⇒ λ_.
     222                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
     223                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;true;r1;r2;r3]]) ]
     224                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;true;r1;r2;r3]]); b1 ]
     225                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;true;r1;r2;r3]]) ; b1 ]
     226                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     227                          | INDIRECT i1 ⇒ λ_.
     228                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
     229                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;true;i1]]) ]
     230                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;false;true;true;i1]]); b1 ]
     231                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;true;i1]]) ; b1 ]
     232                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     233                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
    237234                  | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in [] (*
    238235                     let b1 ≝
     
    240237                       [ DIRECT b1 ⇒ λ_. b1
    241238                       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
    242                       match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect;data]] x) → ? with
    243                        [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;false;true]]); b1]
    244                        | REGISTER r1 r2 r3 ⇒ λ_.[ ([[true;false;false;false;true;r1;r2;r3]]); b1 ]
    245                        | DIRECT b2 ⇒ λ_.[ ([[true;false;false;false;false;true;false;true]]); b1; b2 ]
    246                        | INDIRECT i1 ⇒ λ_. [ ([[true;false;false;false;false;true;true;i1]]); b1 ]
    247                        | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;false;true]]); b1; b2 ]
    248                        | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)*)]
     239                     match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect;data]] x) → ? with
     240                      [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;false;true]]); b1]
     241                      | REGISTER r1 r2 r3 ⇒ λ_.[ ([[true;false;false;false;true;r1;r2;r3]]); b1 ]
     242                      | DIRECT b2 ⇒ λ_.[ ([[true;false;false;false;false;true;false;true]]); b1; b2 ]
     243                      | INDIRECT i1 ⇒ λ_. [ ([[true;false;false;false;false;true;true;i1]]); b1 ]
     244                      | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;false;true]]); b1; b2 ]
     245                      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)*)]
    249246              | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    250247                 match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with
Note: See TracChangeset for help on using the changeset viewer.