Changeset 938 for src/ASM/Assembly.ma


Ignore:
Timestamp:
Jun 10, 2011, 6:36:55 PM (9 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r922 r938  
    202202                 match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with
    203203                  [ DATA16 w ⇒ λ_.
    204                      let 〈b1,b2〉 ≝ split ? 8 8 w in
     204                     let b1_b2 ≝ split ? 8 8 w in
     205                     let b1 ≝ \fst b1_b2 in
     206                     let b2 ≝ \fst b1_b2 in
    205207                      [ ([[true;false;false;true;false;false;false;false]]); b1; b2]
    206208                  | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
     
    352354     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
    353355      [ ADDR11 w ⇒ λ_.
    354          let 〈v1,v2〉 ≝ split ? 3 8 w in
     356         let v1_v2 ≝ split ? 3 8 w in
     357         let v1 ≝ \fst v1_v2 in
     358         let v2 ≝ \snd v1_v2 in
    355359          [ (v1 @@ [[true; false; false; false; true]]) ; v2 ]
    356360      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     
    358362     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
    359363      [ ADDR11 w ⇒ λ_.
    360          let 〈v1,v2〉 ≝ split ?  3 8 w in
     364         let v1_v2 ≝ split ? 3 8 w in
     365         let v1 ≝ \fst v1_v2 in
     366         let v2 ≝ \snd v1_v2 in
    361367          [ (v1 @@ [[false; false; false; false; true]]) ; v2 ]
    362368      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     
    366372     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
    367373      [ ADDR16 w ⇒ λ_.
    368          let 〈b1,b2〉 ≝ split ? 8 8 w in
     374         let b1_b2 ≝ split ? 8 8 w in
     375         let b1 ≝ \fst b1_b2 in
     376         let b2 ≝ \snd b1_b2 in
    369377          [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ]         
    370378      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     
    372380     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
    373381      [ ADDR16 w ⇒ λ_.
    374          let 〈b1,b2〉 ≝ split ? 8 8 w in
     382         let b1_b2 ≝ split ? 8 8 w in
     383         let b1 ≝ \fst b1_b2 in
     384         let b2 ≝ \snd b1_b2 in
    375385          [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ]         
    376386      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
Note: See TracChangeset for help on using the changeset viewer.