Changeset 757 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Apr 18, 2011, 12:30:53 PM (9 years ago)
Author:
mulligan
Message:

Lots more fixing to get both front and backends using same conventions and types.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r719 r757  
    1515      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    1616  | ADD addr1 addr2 ⇒
    17      match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
     17     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
    1818      [ REGISTER r ⇒ λ_.[ ([[false;false;true;false;true]]) @@ r ]
    1919      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;false;false;true;false;true]]); b1 ]
     
    2222      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    2323  | ADDC addr1 addr2 ⇒
    24      match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
     24     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
    2525      [ REGISTER r ⇒ λ_.[ ([[false;false;true;true;true]]) @@ r ]
    2626      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;true;false;true;false;true]]); b1 ]
     
    3838      [ inl addrs ⇒ match addrs with
    3939         [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    40            match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
     40           match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
    4141            [ REGISTER r ⇒ λ_.[ ([[false;true;false;true;true]]) @@ r ]
    4242            | DIRECT b1 ⇒ λ_.[ ([[false;true;false;true;false;true;false;true]]); b1 ]
     
    8080     [ ([[true; true; false; true; false; true; false; false]]) ]
    8181  | DEC addr ⇒
    82      match addr return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect]] x) → ? with
     82     match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect]] x) → ? with
    8383      [ ACC_A ⇒ λ_.
    8484         [ ([[false; false; false; true; false; true; false; false]]) ]
     
    9999           [ RELATIVE b2 ⇒ λ_. b2
    100100           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
    101          match addr1 return λx. bool_to_Prop (is_in ? [[register;direct]] x) → ? with
     101         match addr1 return λx. bool_to_Prop (is_in ? [[registr;direct]] x) → ? with
    102102          [ REGISTER r ⇒ λ_.
    103103             [ ([[true; true; false; true; true]]) @@ r ; b2 ]
     
    170170               [ DATA b2 ⇒ λ_. b2
    171171               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
    172              match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → list Byte with
     172             match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → list Byte with
    173173              [ REGISTER r⇒ λ_.
    174174                 [ ([[true; false; true; true; true]]) @@ r; b2; b3 ]
     
    177177              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) ]]
    178178  | INC addr ⇒
    179      match addr return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect;dptr]] x) → ? with
     179     match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;dptr]] x) → ? with
    180180      [ ACC_A ⇒ λ_.
    181181         [ ([[false;false;false;false;false;true;false;false]]) ]         
     
    214214                     match addrs with
    215215                      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    216                          match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
     216                         match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
    217217                          [ REGISTER r ⇒ λ_.[ ([[true;true;true;false;true]]) @@ r ]
    218218                          | DIRECT b1 ⇒ λ_.[ ([[true;true;true;false;false;true;false;true]]); b1 ]
     
    221221                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    222222                      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    223                          match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → ? with
     223                         match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → ? with
    224224                          [ REGISTER r ⇒ λ_.
    225225                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
     
    240240                       [ DIRECT b1 ⇒ λ_. b1
    241241                       | _ ⇒ λ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
     242                     match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;data]] x) → ? with
    243243                      [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;false;true]]); b1]
    244244                      | REGISTER r ⇒ λ_.[ ([[true;false;false;false;true]]) @@ r; b1 ]
     
    295295         match addrs with
    296296          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    297              match addr2 return λx. bool_to_Prop (is_in ? [[register;data;direct;indirect]] x) → ? with
     297             match addr2 return λx. bool_to_Prop (is_in ? [[registr;data;direct;indirect]] x) → ? with
    298298             [ REGISTER r ⇒ λ_.[ ([[false;true;false;false;true]]) @@ r ]
    299299             | DIRECT b1 ⇒ λ_.[ ([[false;true;false;false;false;true;false;true]]); b1 ]
     
    354354      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
    355355  | SUBB addr1 addr2 ⇒
    356      match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
     356     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
    357357      [ REGISTER r ⇒ λ_.
    358358         [ ([[true;false;false;true;true]]) @@ r ]
     
    367367     [ ([[true;true;false;false;false;true;false;false]]) ]
    368368  | XCH addr1 addr2 ⇒
    369      match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect]] x) → ? with
     369     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect]] x) → ? with
    370370      [ REGISTER r ⇒ λ_.
    371371         [ ([[true;true;false;false;true]]) @@ r ]
     
    383383     match addrs with
    384384      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    385          match addr2 return λx. bool_to_Prop (is_in ? [[data;register;direct;indirect]] x) → ? with
     385         match addr2 return λx. bool_to_Prop (is_in ? [[data;registr;direct;indirect]] x) → ? with
    386386          [ REGISTER r ⇒ λ_.
    387387             [ ([[false;true;true;false;true]]) @@ r ]
Note: See TracChangeset for help on using the changeset viewer.