Ignore:
Timestamp:
Nov 26, 2010, 5:38:04 PM (9 years ago)
Author:
sacerdot
Message:

REGISTER now takes a BitVector? 3

File:
1 edited

Legend:

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

    r312 r316  
    1111  | ADD addr1 addr2 ⇒
    1212     match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
    13       [ REGISTER r1 r2 r3 ⇒ λ_.[ ([[false;false;true;false;true;r1;r2;r3]]) ]
     13      [ REGISTER r ⇒ λ_.[ ([[false;false;true;false;true]]) @@ r ]
    1414      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;false;false;true;false;true]]); b1 ]
    1515      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;false;false;true;true;i1]]) ]
     
    1818  | ADDC addr1 addr2 ⇒
    1919     match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
    20       [ REGISTER r1 r2 r3 ⇒ λ_.[ ([[false;false;true;true;true;r1;r2;r3]]) ]
     20      [ REGISTER r ⇒ λ_.[ ([[false;false;true;true;true]]) @@ r ]
    2121      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;true;false;true;false;true]]); b1 ]
    2222      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;true;false;true;true;i1]]) ]
     
    3434         [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    3535           match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
    36             [ REGISTER r1 r2 r3 ⇒ λ_.[ ([[false;true;false;true;true;r1;r2;r3]]) ]
     36            [ REGISTER r ⇒ λ_.[ ([[false;true;false;true;true]]) @@ r ]
    3737            | DIRECT b1 ⇒ λ_.[ ([[false;true;false;true;false;true;false;true]]); b1 ]
    3838            | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;true;false;true;true;i1]]) ]
     
    7878      [ ACC_A ⇒ λ_.
    7979         [ ([[false; false; false; true; false; true; false; false]]) ]
    80       | REGISTER r1 r2 r3 ⇒ λ_.
    81          [ ([[false; false; false; true; true; r1; r2; r3]]) ]
     80      | REGISTER r ⇒ λ_.
     81         [ ([[false; false; false; true; true]]) @@ r ]
    8282      | DIRECT b1 ⇒ λ_.
    8383         [ ([[false; false; false; true; false; true; false; true]]); b1 ]
     
    9595           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
    9696         match addr1 return λx. bool_to_Prop (is_in ? [[register;direct]] x) → ? with
    97           [ REGISTER r1 r2 r3 ⇒ λ_.
    98              [ ([[true; true; false; true; true; r1; r2; r3]]) ; b2 ]
     97          [ REGISTER r ⇒ λ_.
     98             [ ([[true; true; false; true; true]]) @@ r ; b2 ]
    9999          | DIRECT b1 ⇒ λ_.
    100100             [ ([[true; true; false; true; false; true; false; true]]); b1; b2 ]
     
    166166               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
    167167             match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → List Byte with
    168               [ REGISTER r1 r2 r3 ⇒ λ_.
    169                  [ ([[true; false; true; true; true; r1; r2; r3]]); b2; b3 ]
     168              [ REGISTER r⇒ λ_.
     169                 [ ([[true; false; true; true; true]]) @@ r; b2; b3 ]
    170170              | INDIRECT i1 ⇒ λ_.
    171171                 [ ([[true; false; true; true; false; true; true; i1]]); b2; b3 ]
     
    175175      [ ACC_A ⇒ λ_.
    176176         [ ([[false;false;false;false;false;true;false;false]]) ]         
    177       | REGISTER r1 r2 r3 ⇒ λ_.
    178          [ ([[false;false;false;false;true;r1;r2;r3]]) ]
     177      | REGISTER r ⇒ λ_.
     178         [ ([[false;false;false;false;true]]) @@ r ]
    179179      | DIRECT b1 ⇒ λ_.
    180180         [ ([[false; false; false; false; false; true; false; true]]); b1 ]
     
    210210                      [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    211211                         match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
    212                           [ REGISTER r1 r2 r3 ⇒ λ_.[ ([[true;true;true;false;true;r1;r2;r3]]) ]
     212                          [ REGISTER r ⇒ λ_.[ ([[true;true;true;false;true]]) @@ r ]
    213213                          | DIRECT b1 ⇒ λ_.[ ([[true;true;true;false;false;true;false;true]]); b1 ]
    214214                          | INDIRECT i1 ⇒ λ_. [ ([[true;true;true;false;false;true;true;i1]]) ]
     
    217217                      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    218218                         match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → ? with
    219                           [ REGISTER r1 r2 r3 ⇒ λ_.
     219                          [ REGISTER r ⇒ λ_.
    220220                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
    221                               [ ACC_A ⇒ λ_.[ ([[true;true;true;true;true;r1;r2;r3]]) ]
    222                               | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;true;r1;r2;r3]]); b1 ]
    223                               | DATA b1 ⇒ λ_. [ ([[false;true;true;true;true;r1;r2;r3]]) ; b1 ]
     221                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;true]]) @@ r ]
     222                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;true]]) @@ r; b1 ]
     223                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;true]]) @@ r; b1 ]
    224224                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    225225                          | INDIRECT i1 ⇒ λ_.
     
    237237                     match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect;data]] x) → ? with
    238238                      [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;false;true]]); b1]
    239                       | REGISTER r1 r2 r3 ⇒ λ_.[ ([[true;false;false;false;true;r1;r2;r3]]); b1 ]
     239                      | REGISTER r ⇒ λ_.[ ([[true;false;false;false;true]]) @@ r; b1 ]
    240240                      | DIRECT b2 ⇒ λ_.[ ([[true;false;false;false;false;true;false;true]]); b1; b2 ]
    241241                      | INDIRECT i1 ⇒ λ_. [ ([[true;false;false;false;false;true;true;i1]]); b1 ]
     
    291291          [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    292292             match addr2 return λx. bool_to_Prop (is_in ? [[register;data;direct;indirect]] x) → ? with
    293              [ REGISTER r1 r2 r3 ⇒ λ_.[ ([[false;true;false;false;true;r1;r2;r3]]) ]
     293             [ REGISTER r ⇒ λ_.[ ([[false;true;false;false;true]]) @@ r ]
    294294             | DIRECT b1 ⇒ λ_.[ ([[false;true;false;false;false;true;false;true]]); b1 ]
    295295             | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;false;false;true;true;i1]]) ]
     
    350350  | SUBB addr1 addr2 ⇒
    351351     match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
    352       [ REGISTER r1 r2 r3 ⇒ λ_.
    353          [ ([[true;false;false;true;true;r1;r2;r3]]) ]
     352      [ REGISTER r ⇒ λ_.
     353         [ ([[true;false;false;true;true]]) @@ r ]
    354354      | DIRECT b1 ⇒ λ_.
    355355         [ ([[true;false;false;true;false;true;false;true]]); b1]
     
    363363  | XCH addr1 addr2 ⇒
    364364     match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect]] x) → ? with
    365       [ REGISTER r1 r2 r3 ⇒ λ_.
    366          [ ([[true;true;false;false;true;r1;r2;r3]]) ]
     365      [ REGISTER r ⇒ λ_.
     366         [ ([[true;true;false;false;true]]) @@ r ]
    367367      | DIRECT b1 ⇒ λ_.
    368368         [ ([[true;true;false;false;false;true;false;true]]); b1]
     
    379379      [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    380380         match addr2 return λx. bool_to_Prop (is_in ? [[data;register;direct;indirect]] x) → ? with
    381           [ REGISTER r1 r2 r3 ⇒ λ_.
    382              [ ([[false;true;true;false;true;r1;r2;r3]]) ]
     381          [ REGISTER r ⇒ λ_.
     382             [ ([[false;true;true;false;true]]) @@ r ]
    383383          | DIRECT b1 ⇒ λ_.
    384384             [ ([[false;true;true;false;false;true;false;true]]); b1]
Note: See TracChangeset for help on using the changeset viewer.