Changeset 316


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

REGISTER now takes a BitVector? 3

Location:
Deliverables/D4.1/Matita
Files:
1 added
5 edited

Legend:

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

    r297 r316  
    77| INDIRECT: Bit → addressing_mode
    88| EXT_INDIRECT: Bit → addressing_mode
    9 | REGISTER: Bit → Bit → Bit → addressing_mode
     9| REGISTER: BitVector (S (S (S Z))) → addressing_mode
    1010| ACC_A: addressing_mode
    1111| ACC_B: addressing_mode
     
    5151   | indirect ⇒ match A with [ INDIRECT _ ⇒ true | _ ⇒ false ]
    5252   | ext_indirect ⇒ match A with [ EXT_INDIRECT _ ⇒ true | _ ⇒ false ]
    53    | register ⇒ match A with [ REGISTER _ _ _ ⇒ true | _ ⇒ false ]
     53   | register ⇒ match A with [ REGISTER _ ⇒ true | _ ⇒ false ]
    5454   | acc_a ⇒ match A with [ ACC_A ⇒ true | _ ⇒ false ]
    5555   | acc_b ⇒ match A with [ ACC_B ⇒ true | _ ⇒ false ]
  • 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]
  • Deliverables/D4.1/Matita/Status.ma

    r314 r316  
    728728      | ACC_B ⇒ λacc_b: True. get_8051_sfr s SFR_ACC_B
    729729      | DATA d ⇒ λdata: True. d
    730       | REGISTER r1 r2 r3 ⇒ λregister: True. get_register s r1 r2 r3
     730      | REGISTER r ⇒ λregister: True. get_register s r
    731731      | EXT_INDIRECT_DPTR ⇒
    732732        λext_indirect_dptr: True.
  • Deliverables/D4.1/Matita/Vector.ma

    r315 r316  
    146146//; ndestruct; //.
    147147nqed.
     148
     149ndefinition head8 ≝ λA. split A (S Z) (S (S (S (S (S (S (S Z))))))).
    148150   
    149151(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    445447  @.
    446448nqed.
     449
     450naxiom eqv: ∀A,n. Vector A n → Vector A n → Bool.
  • Deliverables/D4.1/Matita/depends

    r281 r316  
    1 Status.ma Arithmetic.ma BitVectorTrie.ma
     1Arithmetic.ma BitVector.ma Bool.ma Connectives.ma Exponential.ma List.ma Nat.ma Plogic/equality.ma Universes.ma
     2Status.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
    23Exponential.ma Connectives.ma Nat.ma Plogic/equality.ma
    3 Arithmetic.ma BitVector.ma Bool.ma Connectives.ma Exponential.ma List.ma Nat.ma Plogic/equality.ma Universes.ma
    44BitVectorTrie.ma BitVector.ma Bool.ma Maybe.ma
    55Cartesian.ma Universes.ma
    6 Universes.ma
    76Maybe.ma Bool.ma Plogic/equality.ma Universes.ma
    87Either.ma Bool.ma Maybe.ma Universes.ma
     8Universes.ma
    99ASM.ma BitVectorTrie.ma Either.ma String.ma
     10Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Util.ma
     11Fetch.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
    1012Char.ma Universes.ma
    11 Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Util.ma
    1213Connectives.ma Plogic/equality.ma
    1314Bool.ma Universes.ma
     
    1516List.ma Bool.ma Nat.ma Plogic/equality.ma Universes.ma Util.ma
    1617Util.ma Nat.ma
    17 String.ma Char.ma List.ma
    1818BitVector.ma Bool.ma List.ma Nat.ma Universes.ma Vector.ma
    1919Compare.ma Universes.ma
     20String.ma Char.ma List.ma
    2021Plogic/equality.ma Universes.ma
    2122Nat.ma Bool.ma Cartesian.ma Connectives.ma
Note: See TracChangeset for help on using the changeset viewer.