Changeset 302


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

...

File:
1 edited

Legend:

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

    r301 r302  
    266266  | NOP ⇒
    267267     [ ([[false;false;false;false;false;false;false;false]]) ]
    268 (*
    269   | `ORL (`U1(`A, `REG(r1,r2,r3))) ->
    270     [mk_byte_from_bits ((false,true,false,false),(true,r1,r2,r3))]
    271   | `ORL (`U1(`A, `DIRECT b1)) ->
    272     [mk_byte_from_bits ((false,true,false,false),(false,true,false,true)); b1]
    273   | `ORL (`U1(`A, `INDIRECT i1)) ->
    274     [mk_byte_from_bits ((false,true,false,false),(false,true,true,i1))]
    275   | `ORL (`U1(`A, `DATA b1)) ->
    276     [mk_byte_from_bits ((false,true,false,false),(false,true,false,false)); b1]
    277   | `ORL (`U2(`DIRECT b1, `A)) ->
    278     [mk_byte_from_bits ((false,true,false,false),(false,false,true,false)); b1]
    279   | `ORL (`U2 (`DIRECT b1, `DATA b2)) ->
    280     [mk_byte_from_bits ((false,true,false,false),(false,false,true,true)); b1; b2]
    281   | `ORL (`U3 (`C, `BIT b1)) ->
    282     [mk_byte_from_bits ((false,true,true,true),(false,false,true,false)); b1]
    283   | `ORL (`U3 (`C, `NBIT b1)) ->
    284     [mk_byte_from_bits ((true,false,true,false),(false,false,false,false)); b1]
    285 *)
     268  | ORL addrs ⇒
     269     match addrs with
     270      [ Left addrs ⇒
     271         match addrs with
     272          [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     273             match addr2 return λx. bool_to_Prop (is_in ? [[register;data;direct;indirect]] x) → ? with
     274             [ REGISTER r1 r2 r3 ⇒ λ_.[ ([[false;true;false;false;true;r1;r2;r2]]) ]
     275             | DIRECT b1 ⇒ λ_.[ ([[false;true;false;false;false;true;false;true]]); b1 ]
     276             | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;false;false;true;true;i1]]) ]
     277             | DATA b1 ⇒ λ_. [ ([[false;true;false;false;false;true;false;false]]) ; b1 ]
     278             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     279          | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     280            let b1 ≝
     281              match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
     282               [ DIRECT b1 ⇒ λ_. b1
     283               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
     284             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
     285              [ ACC_A ⇒ λ_.
     286                 [ ([[false;true;false;false;false;false;true;false]]); b1 ]
     287              | DATA b2 ⇒ λ_.
     288                 [ ([[false;true;false;false;false;false;true;true]]); b1; b2 ]
     289              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
     290      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in     
     291         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
     292          [ BIT_ADDR b1 ⇒ λ_.
     293             [ ([[false;true;true;true;false;false;true;false]]); b1 ]
     294          | N_BIT_ADDR b1 ⇒ λ_.
     295             [ ([[true;false;true;false;false;false;false;false]]); b1 ]
     296          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
    286297  | POP addr ⇒
    287298     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
Note: See TracChangeset for help on using the changeset viewer.