 Timestamp:
 Feb 27, 2013, 10:46:05 PM (7 years ago)
 Location:
 src
 Files:

 2 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) 
src/compiler.ma
r2724 r2745 82 82 include "ASM/ASMCostsSplit.ma". 83 83 84 (*CSC: move the next definitions, e.g. in BitVectorTrie *) 85 definition in_codomain: ∀A:Type[0].∀n:nat. BitVectorTrie A n → A → Prop ≝ 86 λA,n,m,a. ∃k:BitVector n. lookup_opt … k m = Some … a. 87 88 definition strong_decidable: Prop → Type[0] ≝ 89 λP:Prop. P + ¬ P. 90 91 lemma strong_decidable_in_codomain: 92 ∀A:DeqSet.∀n:nat.∀m: BitVectorTrie A n.∀a:A. 93 strong_decidable (in_codomain A n m a). 94 #A #n #m elim m 95 [ normalize #a' #a inversion (a' == a) #H 96 [ %1 %{(VEmpty …)} >(\P H) % 97  %2 % * #_ #EQ destruct lapply (\Pf H) /2/ ] 98  n #n #L #R #Hl #Hr #a 99 cases (Hl a) Hl [#K %1 cases K #k #H %{(false:::k)} <H % ] #Hl 100 cases (Hr a) Hr [#K %1 cases K #k #H %{(true:::k)} <H % ] #Hr 101 %2 % * #k cases (BitVector_Sn … k) ** #tl #EQ >EQ whd in ⊢ (??%? → ?); 102 normalize nodelta whd in match (tail ???); #abs [ cases Hr  cases Hl ] /3/ 103  #n #A %2 % * #x normalize #abs destruct ] 104 qed. 105 84 106 definition compile : clight_program → 85 107 res (object_code × costlabel_map × (𝚺labelled:clight_program. clight_cost_map labelled)) ≝ … … 96 118 in 97 119 return 〈p, ❬p', k'❭〉. 98 cases daemon 120 [ @strong_decidable_in_codomain 121  cases daemon ] 99 122 qed.
Note: See TracChangeset
for help on using the changeset viewer.