Changeset 299


Ignore:
Timestamp:
Nov 25, 2010, 10:55:45 PM (9 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

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

    r298 r299  
    307307         [ ([[true;true;false;true;false;false;true;false]]); b1 ]
    308308      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     309  | SJMP addr ⇒
     310     match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
     311      [ RELATIVE b1 ⇒ λ_.
     312         [ ([[true;false;false;false;false;false;false;false]]); b1 ]
     313      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     314  | SUBB addr1 addr2 ⇒
     315     match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
     316      [ REGISTER r1 r2 r3 ⇒ λ_.
     317         [ ([[true;false;false;true;true;r1;r2;r3]]) ]
     318      | DIRECT b1 ⇒ λ_.
     319         [ ([[true;false;false;true;false;true;false;true]]); b1]
     320      | INDIRECT i1 ⇒ λ_.
     321         [ ([[true;false;false;true;false;true;true;i1]]) ]
     322      | DATA b1 ⇒ λ_.
     323         [ ([[true;false;false;true;false;true;false;false]]); b1]
     324      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     325  | SWAP addr ⇒
     326     [ ([[true;true;false;false;false;true;false;false]]) ]
     327  | XCH addr1 addr2 ⇒
     328     match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect]] x) → ? with
     329      [ REGISTER r1 r2 r3 ⇒ λ_.
     330         [ ([[true;true;false;false;true;r1;r2;r3]]) ]
     331      | DIRECT b1 ⇒ λ_.
     332         [ ([[true;true;false;false;false;true;false;true]]); b1]
     333      | INDIRECT i1 ⇒ λ_.
     334         [ ([[true;true;false;false;false;true;true;i1]]) ]
     335      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     336  | XCHD addr1 addr2 ⇒
     337     match addr2 return λx. bool_to_Prop (is_in ? [[indirect]] x) → ? with
     338      [ INDIRECT i1 ⇒ λ_.
     339         [ ([[true;true;false;true;false;true;true;i1]]) ]
     340      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     341 
    309342
    310343  | _ ⇒ [ ]].
    311344(*
    312   | `SJMP (`REL b1) ->
    313     [mk_byte_from_bits ((true,false,false,false),(false,false,false,false)); b1]
    314 
    315   | `SUBB (`A, `REG(r1,r2,r3)) ->
    316     [mk_byte_from_bits ((true,false,false,true),(true,r1,r2,r3))]
    317   | `SUBB (`A, `DIRECT b1) ->
    318     [mk_byte_from_bits ((true,false,false,true),(false,true,false,true)); b1]
    319   | `SUBB (`A, `INDIRECT i1) ->
    320     [mk_byte_from_bits ((true,false,false,true),(false,true,true,i1))]
    321   | `SUBB (`A, `DATA b1) ->
    322     [mk_byte_from_bits ((true,false,false,true),(false,true,false,false)); b1]
    323 
    324   | `SWAP `A ->
    325     [mk_byte_from_bits ((true,true,false,false),(false,true,false,false))]
    326 
    327   | `XCH (`A, `REG(r1,r2,r3)) ->
    328     [mk_byte_from_bits ((true,true,false,false),(true,r1,r2,r3))]
    329   | `XCH (`A, `DIRECT b1) ->
    330     [mk_byte_from_bits ((true,true,false,false),(false,true,false,true)); b1]
    331   | `XCH (`A, `INDIRECT i1) ->
    332     [mk_byte_from_bits ((true,true,false,false),(false,true,true,i1))]
    333 
    334   | `XCHD(`A, `INDIRECT i1) ->
    335     [mk_byte_from_bits ((true,true,false,true),(false,true,true,i1))]
    336 
    337345  | `XRL(`U1(`A, `REG(r1,r2,r3))) ->
    338346    [mk_byte_from_bits ((false,true,true,false),(true,r1,r2,r3))]
Note: See TracChangeset for help on using the changeset viewer.