Changeset 938 for src/ASM/Assembly.ma
 Timestamp:
 Jun 10, 2011, 6:36:55 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r922 r938 202 202 match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with 203 203 [ 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 205 207 [ ([[true;false;false;true;false;false;false;false]]); b1; b2] 206 208  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)] … … 352 354 match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with 353 355 [ 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 355 359 [ (v1 @@ [[true; false; false; false; true]]) ; v2 ] 356 360  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) … … 358 362 match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with 359 363 [ 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 361 367 [ (v1 @@ [[false; false; false; false; true]]) ; v2 ] 362 368  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) … … 366 372 match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with 367 373 [ 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 369 377 [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ] 370 378  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) … … 372 380 match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with 373 381 [ 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 375 385 [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ] 376 386  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
Note: See TracChangeset
for help on using the changeset viewer.