Changeset 2745 for src/compiler.ma
 Timestamp:
 Feb 27, 2013, 10:46:05 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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.