Changeset 282


Ignore:
Timestamp:
Nov 24, 2010, 7:11:36 PM (9 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

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

    r281 r282  
    1616      | DATA b1 ⇒ λ_. [ ([[false;false;true;false;false;true;false;false]]) ; b1 ]
    1717      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     18  | ADDC addr1 addr2 ⇒
     19     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]]) ]
     21      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;true;false;true;false;true]]); b1 ]
     22      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;true;false;true;true;i1]]) ]
     23      | DATA b1 ⇒ λ_. [ ([[false;false;true;true;false;true;false;false]]) ; b1 ]
     24      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     25  | AJMP addr ⇒
     26     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
     27      [ ADDR11 w ⇒ λ_.
     28         let 〈v1,v2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S Z))) w in
     29          [ (v1 @@ [[false; false; false; false; true]]) ; v2 ]
     30      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     31  | ANL addrs ⇒
     32     match addrs with
     33      [ Left addrs ⇒ match addrs with
     34         [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     35           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]]) ]
     37            | DIRECT b1 ⇒ λ_.[ ([[false;true;false;true;false;true;false;true]]); b1 ]
     38            | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;true;false;true;true;i1]]) ]
     39            | DATA b1 ⇒ λ_. [ ([[false;true;false;true;false;true;false;false]]) ; b1 ]
     40            | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     41         | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     42            let b1 ≝
     43             match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
     44              [ DIRECT b1 ⇒ λ_.b1
     45              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
     46            match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
     47             [ ACC_A ⇒ λ_.[ ([[false;true;false;true;false;false;true;false]]) ; b1 ]
     48             | DATA b2 ⇒ λ_. [ ([[false;true;false;true;false;false;true;true]]) ; b1 ; b2 ]
     49             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     50         ]
     51      | Right addrs ⇒ (*let 〈addr1,addr2〉 ≝ addrs in
     52         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
     53          [ BIT_ADDR b1 ⇒ λ_.[ ([[true;false;false;false;false;false;true;false]]) ; b1 ]
     54          | N_BIT_ADDR b1 ⇒ λ_. [ ([[true;false;true;true;false;false;false;false]]) ; b1 ]
     55          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]*) ?]
     56 
    1857  | _ ⇒ [ ([[false;false;false;false;false;false;false;false]]) ]].
    1958
    20 (*
    21   | `ADDC (`A, `REG(r1,r2,r3)) ->
    22      [mk_byte_from_bits ((false,false,true,true),(true,r1,r2,r3))]
    23   | `ADDC (`A, `DIRECT b1) ->
    24      [mk_byte_from_bits ((false,false,true,true),(false,true,false,true)); b1]
    25   | `ADDC (`A,`INDIRECT i1) ->
    26      [mk_byte_from_bits ((false,false,true,true),(false,true,true,i1))]
    27   | `ADDC (`A,`DATA b1) ->
    28      [mk_byte_from_bits ((false,false,true,true),(false,true,false,false)); b1]
    29   | `AJMP (`ADDR11 w) ->
    30      let (a10,a9,a8,b1) = from_word11 w in
    31        [mk_byte_from_bits ((a10,a9,a8,false),(false,false,false,true))]
    32   | `ANL (`U1 (`A, `REG (r1,r2,r3))) ->
    33      [mk_byte_from_bits ((false,true,false,true),(true,r1,r2,r3))]
    34   | `ANL (`U1 (`A, `DIRECT b1)) ->
    35      [mk_byte_from_bits ((false,true,false,true),(false,true,false,true)); b1]
    36   | `ANL (`U1 (`A, `INDIRECT i1)) ->
    37      [mk_byte_from_bits ((false,true,false,true),(false,true,true,i1))]
    38   | `ANL (`U1 (`A, `DATA b1)) ->
    39      [mk_byte_from_bits ((false,true,false,true),(false,true,false,false)); b1]
    40   | `ANL (`U2 (`DIRECT b1,`A)) ->
    41      [mk_byte_from_bits ((false,true,false,true),(false,false,true,false)); b1]
    42   | `ANL (`U2 (`DIRECT b1,`DATA b2)) ->
    43      [mk_byte_from_bits ((false,true,false,true),(false,false,true,true)); b1; b2]
    44   | `ANL (`U3 (`C,`BIT b1)) ->
    45      [mk_byte_from_bits ((true,false,false,false),(false,false,true,false)); b1]
    46   | `ANL (`U3 (`C,`NBIT b1)) ->
    47     [mk_byte_from_bits ((true,false,true,true),(false,false,false,false)); b1]
     59
    4860  | `CJNE (`U1 (`A, `DIRECT b1), `REL b2) ->
    4961    [mk_byte_from_bits ((true,false,true,true),(false,true,false,true)); b1; b2]
     
    349361 
    350362 ].
    351 *)
     363
Note: See TracChangeset for help on using the changeset viewer.