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

...

File:
1 edited

Legend:

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

    r299 r300  
    339339         [ ([[true;true;false;true;false;true;true;i1]]) ]
    340340      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    341  
     341  | XRL addrs ⇒
     342     match addrs with
     343      [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     344         match addr2 return λx. bool_to_Prop (is_in ? [[data;register;direct;indirect]] x) → ? with
     345          [ REGISTER r1 r2 r3 ⇒ λ_.
     346             [ ([[false;true;true;false;true;r1;r2;r3]]) ]
     347          | DIRECT b1 ⇒ λ_.
     348             [ ([[false;true;true;false;false;true;false;true]]); b1]
     349          | INDIRECT i1 ⇒ λ_.
     350             [ ([[false;true;true;false;false;true;true;i1]]) ]
     351          | DATA b1 ⇒ λ_.
     352             [ ([[false;true;true;false;false;true;false;false]]); b1]
     353          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     354      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
     355         let b1 ≝
     356          match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
     357           [ DIRECT b1 ⇒ λ_. b1
     358           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
     359         match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
     360          [ ACC_A ⇒ λ_.
     361             [ ([[false;true;true;false;false;false;true;false]]); b1 ]         
     362          | DATA b2 ⇒ λ_.
     363             [ ([[false;true;true;false;false;false;true;true]]); b1; b2 ]
     364          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)] 
    342365
    343366  | _ ⇒ [ ]].
     367
     368
    344369(*
    345   | `XRL(`U1(`A, `REG(r1,r2,r3))) ->
    346     [mk_byte_from_bits ((false,true,true,false),(true,r1,r2,r3))]
    347   | `XRL(`U1(`A, `DIRECT b1)) ->
    348     [mk_byte_from_bits ((false,true,true,false),(false,true,false,true)); b1]
    349   | `XRL(`U1(`A, `INDIRECT i1)) ->
    350     [mk_byte_from_bits ((false,true,true,false),(false,true,true,i1))]
    351   | `XRL(`U1(`A, `DATA b1)) ->
    352     [mk_byte_from_bits ((false,true,true,false),(false,true,false,false)); b1]
    353   | `XRL(`U2(`DIRECT b1, `A)) ->
    354     [mk_byte_from_bits ((false,true,true,false),(false,false,true,false)); b1]
    355   | `XRL(`U2(`DIRECT b1, `DATA b2)) ->
    356     [mk_byte_from_bits ((false,true,true,false),(false,false,true,true)); b1; b2]
    357 ;;
    358 
    359 
    360 
    361370nrecord Sigma (A: Type[0]) (T: A → Type[0]) : Type[0] ≝ {
    362371   elem:> A;
Note: See TracChangeset for help on using the changeset viewer.