Changeset 304


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

...

File:
1 edited

Legend:

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

    r303 r304  
    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;r2]]) ]
     13      [ REGISTER r1 r2 r3 ⇒ λ_.[ ([[false;false;true;false;true;r1;r2;r3]]) ]
    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;r2]]) ]
     20      [ REGISTER r1 r2 r3 ⇒ λ_.[ ([[false;false;true;true;true;r1;r2;r3]]) ]
    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;r2]]) ]
     36            [ REGISTER r1 r2 r3 ⇒ λ_.[ ([[false;true;false;true;true;r1;r2;r3]]) ]
    3737            | DIRECT b1 ⇒ λ_.[ ([[false;true;false;true;false;true;false;true]]); b1 ]
    3838            | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;true;false;true;true;i1]]) ]
     
    211211                     match addrs with
    212212                      [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    213 [] (*
    214   | `MOV (`U1 (`A, `REG(r1,r2,r3))) ->
    215     [mk_byte_from_bits ((true,true,true,false),(true,r1,r2,r3))]
    216   | `MOV (`U1 (`A, `DIRECT b1)) ->
    217     [mk_byte_from_bits ((true,true,true,false),(false,true,false,true)); b1]
    218   | `MOV (`U1 (`A, `INDIRECT i1)) ->
    219     [mk_byte_from_bits ((true,true,true,false),(false,true,true,i1))]
    220   | `MOV (`U1 (`A, `DATA b1)) ->
    221     [mk_byte_from_bits ((false,true,true,true),(false,true,false,false)); b1]
    222 *)
     213                         match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
     214                          [ REGISTER r1 r2 r3 ⇒ λ_.[ ([[true;true;true;false;true;r1;r2;r3]]) ]
     215                          | DIRECT b1 ⇒ λ_.[ ([[true;true;true;false;false;true;false;true]]); b1 ]
     216                          | INDIRECT i1 ⇒ λ_. [ ([[true;true;true;false;false;true;true;i1]]) ]
     217                          | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;false;false]]) ; b1 ]
     218                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    223219                      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    224220[] (*
     
    229225  | `MOV (`U2 (`REG(r1,r2,r3), (`DATA b1))) ->
    230226    [mk_byte_from_bits ((false,true,true,true),(true,r1,r2,r3)); b1]
     227
    231228  | `MOV (`U2 (`INDIRECT i1, `A)) ->
    232229    [mk_byte_from_bits ((true,true,true,true),(false,true,true,i1))]
     
    238235*)
    239236                      ]
    240                   | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    241 [] (*
    242   | `MOV (`U3 (`DIRECT b1, `A)) ->
    243     [mk_byte_from_bits ((true,true,true,true),(false,true,false,true)); b1]
    244   | `MOV (`U3 (`DIRECT b1, `REG(r1,r2,r3))) ->
    245     [mk_byte_from_bits ((true,false,false,false),(true,r1,r2,r3)); b1]
    246   | `MOV (`U3 (`DIRECT b1, `DIRECT b2)) ->
    247     [mk_byte_from_bits ((true,false,false,false),(false,true,false,true)); b1; b2]
    248   | `MOV (`U3 (`DIRECT b1, `INDIRECT i1)) ->
    249     [mk_byte_from_bits ((true,false,false,false),(false,true,true,i1)); b1]
    250   | `MOV (`U3 (`DIRECT b1, `DATA b2)) ->
    251     [mk_byte_from_bits ((false,true,true,true),(false,true,false,true)); b1; b2]
    252 *)
    253                   ]
     237                  | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in [] (*
     238                     let b1 ≝
     239                      match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
     240                       [ DIRECT b1 ⇒ λ_. b1
     241                       | _ ⇒ λ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)*)]
    254249              | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    255 [] (*
    256   | `MOV (`U4 (`DPTR, `DATA16 w)) ->
    257     let (b1,b2) = from_word w in
    258       [mk_byte_from_bits ((true,false,false,true),(false,false,false,false)); b1; b2]
    259 *)           
    260               ]
     250                 match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with
     251                  [ DATA16 w ⇒ λ_.
     252                     let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in
     253                      [ ([[true;false;false;true;false;false;false;false]]); b1; b2]
     254                  | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
    261255          | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    262256[] (*
     
    304298          [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    305299             match addr2 return λx. bool_to_Prop (is_in ? [[register;data;direct;indirect]] x) → ? with
    306              [ REGISTER r1 r2 r3 ⇒ λ_.[ ([[false;true;false;false;true;r1;r2;r2]]) ]
     300             [ REGISTER r1 r2 r3 ⇒ λ_.[ ([[false;true;false;false;true;r1;r2;r3]]) ]
    307301             | DIRECT b1 ⇒ λ_.[ ([[false;true;false;false;false;true;false;true]]); b1 ]
    308302             | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;false;false;true;true;i1]]) ]
Note: See TracChangeset for help on using the changeset viewer.