Changeset 305


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

...

File:
1 edited

Legend:

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

    r304 r305  
    254254                  | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
    255255          | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    256 [] (*
    257   | `MOV (`U5 (`C, `BIT b1)) ->
    258     [mk_byte_from_bits ((true,false,true,false),(false,false,true,false)); b1]
    259 *)
    260           ]
     256             match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
     257              [ BIT_ADDR b1 ⇒ λ_.
     258                 [ ([[true;false;true;false;false;false;true;false]]); b1 ]
     259              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
    261260      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    262 [] (*
    263   | `MOV (`U6 (`BIT b1, `C)) ->
    264     [mk_byte_from_bits ((true,false,false,true),(false,false,true,false)); b1]   
    265 *)
    266       ]
     261         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
     262          [ BIT_ADDR b1 ⇒ λ_.
     263             [ ([[true;false;false;true;false;false;true;false]]); b1 ]
     264          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
    267265  | MOVC addr1 addr2 ⇒
    268266     match addr2 return λx. bool_to_Prop (is_in ? [[acc_dptr;acc_pc]] x) → ? with
Note: See TracChangeset for help on using the changeset viewer.