Changeset 301


Ignore:
Timestamp:
Nov 25, 2010, 11:19:22 PM (9 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

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

    r300 r301  
    246246         [ ([[true;false;false;false;false;false;true;true]]) ]
    247247      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    248 (*
    249   | `MOVX (`U1 (`A, `EXT_INDIRECT i1)) ->
    250     [mk_byte_from_bits ((true,true,true,false),(false,false,true,i1))]
    251   | `MOVX (`U1 (`A, `EXT_IND_DPTR)) ->
    252     [mk_byte_from_bits ((true,true,true,false),(false,false,false,false))]
    253   | `MOVX (`U2 (`EXT_INDIRECT i1, `A)) ->
    254     [mk_byte_from_bits ((true,true,true,true),(false,false,true,i1))]
    255   | `MOVX (`U2 (`EXT_IND_DPTR, `A)) ->
    256     [mk_byte_from_bits ((true,true,true,true),(false,false,false,false))]
    257 *)
     248  | MOVX addrs ⇒
     249     match addrs with
     250      [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     251         match addr2 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
     252          [ EXT_INDIRECT i1 ⇒ λ_.
     253             [ ([[true;true;true;false;false;false;true;i1]]) ]
     254          | EXT_INDIRECT_DPTR ⇒ λ_.
     255             [ ([[true;true;true;false;false;false;false;false]]) ]
     256          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     257      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     258         match addr1 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
     259          [ EXT_INDIRECT i1 ⇒ λ_.
     260             [ ([[true;true;true;true;false;false;true;i1]]) ]
     261          | EXT_INDIRECT_DPTR ⇒ λ_.
     262             [ ([[true;true;true;true;false;false;false;false]]) ]
     263          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
    258264  | MUL addr1 addr2 ⇒
    259265     [ ([[true;false;true;false;false;true;false;false]]) ]
Note: See TracChangeset for help on using the changeset viewer.