 Timestamp:
 Feb 27, 2013, 10:46:05 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Policy.ma
r2700 r2745 22 22 match n return λx.n = x → Σa:bool × (option ppc_pc_map).? with 23 23 [ O ⇒ λp.〈false,pi1 ?? (jump_expansion_start program labels)〉 24  S m ⇒ λp.let 〈no_ch,z〉 as p1 ≝ (pi1 ?? (jump_expansion_internal program m)) in 24  S m ⇒ λp. 25 let res ≝ pi1 ?? (jump_expansion_internal program m) in 26 let 〈no_ch,z〉 as p1 ≝ res in 25 27 match z return λx. z=x → Σa:bool × (option ppc_pc_map).? with 26 28 [ None ⇒ λp2.〈false,None ?〉 27 29  Some op ⇒ λp2.if no_ch 28 then pi1 ?? (jump_expansion_internal program m)30 then res 29 31 else pi1 ?? (jump_expansion_step program (pi1 ?? labels) «op,?») 30 32 ] (refl … z) … … 55 57 ] 56 58 ] 57  cases (jump_expansion_internal program m) in p1; 59  whd in match res in p1; 60 cases (jump_expansion_internal program m) in p1; 58 61 #p cases p p #p #r cases r normalize nodelta 59 62 [ #_ >p2 #ABS destruct (ABS)
Note: See TracChangeset
for help on using the changeset viewer.