Changeset 1316 for src/common
- Timestamp:
- Oct 7, 2011, 12:26:39 PM (10 years ago)
- Location:
- src
- Files:
-
- 3 edited
Legend:
- Unmodified
- Added
- Removed
-
src
-
Property
svn:mergeinfo
set to
/Deliverables/D3.3/id-lookup-branch merged eligible
-
Property
svn:mergeinfo
set to
-
src/common/Errors.ma
r1214 r1316 18 18 include "basics/list.ma". 19 19 include "common/PreIdentifiers.ma". 20 include "utilities/lists.ma". 21 include "utilities/deppair.ma". 20 22 21 23 (* * Error reporting and the error monad. *) … … 87 89 notation "'ret' e" non associative with precedence 45 for @{'ret ${e}}.*) 88 90 91 (* Dependent pair version. *) 92 notation > "vbox('do' « ident v , ident p » ← e; break e')" with precedence 40 93 for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ dp ${ident v} ${ident p} ⇒ ${e'} ]) }. 94 89 95 (* 90 96 (** The [do] notation, inspired by Haskell's, keeps the code readable. *) … … 127 133 | cons hd tl ⇒ do hd' ← f hd; do tl' ← mmap ?? f tl; OK ? (hd'::tl') 128 134 ]. 135 136 (* And mmap coupled with proofs. *) 137 138 let rec mmap_sigma (A,B:Type[0]) (P:B → Prop) (f:A → res (Σx:B.P x)) (l:list A) on l : res (Σl':list B.All B P l') ≝ 139 match l with 140 [ nil ⇒ OK ? «nil B, ?» 141 | cons h t ⇒ 142 do h' ← f h; 143 do t' ← mmap_sigma A B P f t; 144 OK ? «cons B h' t', ?» 145 ]. 146 whd // % 147 [ @(use_sig B P) 148 | cases t' #l' #p @p 149 ] qed. 129 150 130 151 (* … … 239 260 qed. 240 261 262 (* A variation of bind and its notation that provides an equality proof for 263 later use. *) 264 265 definition bind_eq ≝ λA,B:Type[0]. λf: res A. λg: ∀a:A. f = OK ? a → res B. 266 match f return λx. f = x → ? with 267 [ OK x ⇒ g x 268 | Error msg ⇒ λ_. Error ? msg 269 ] (refl ? f). 270 271 notation > "vbox('do' ident v 'as' ident E ← e; break e')" with precedence 40 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}. 272 241 273 definition res_to_opt : ∀A:Type[0]. res A → option A ≝ 242 274 λA.λv. match v with [ Error _ ⇒ None ? | OK v ⇒ Some … v]. 275 -
src/common/Identifiers.ma
r1092 r1316 3 3 include "ASM/Arithmetic.ma". 4 4 include "common/Errors.ma". 5 include "utilities/option.ma". 5 6 6 7 (* identifiers and their generators are tagged to differentiate them, and to … … 122 123 ] qed. 123 124 125 lemma lookup_add_cases : ∀tag,A,m,i,j,a,v. 126 lookup tag A (add tag A m i a) j = Some ? v → 127 (i=j ∧ v = a) ∨ lookup tag A m j = Some ? v. 128 #tag #A #m #i #j #a #v 129 cases (identifier_eq ? i j) 130 [ #E >E >lookup_add_hit #H %1 destruct % // 131 | #NE >lookup_add_miss /2/ @eq_identifier_elim /2/ 132 ] qed. 133 124 134 (* Extract every identifier, value pair from the map. *) 125 135 definition elements : ∀tag,A. identifier_map tag A → list (identifier tag × A) ≝ … … 147 157 [ an_id_map m' ⇒ fold A B ? (λbv. f (an_identifier ? bv)) m' b ]. 148 158 159 (* A predicate that an identifier is in a map, and a failure-avoiding lookup 160 and update using it. *) 161 162 definition present : ∀tag,A. identifier_map tag A → identifier tag → Prop ≝ 163 λtag,A,m,i. lookup … m i ≠ None ?. 164 165 definition lookup_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A ≝ 166 λtag,A,m,id. match lookup ?? m id return λx. x ≠ None ? → ? with [ Some a ⇒ λ_. a | None ⇒ λH.⊥ ]. 167 cases H #H' cases (H' (refl ??)) qed. 168 169 definition update_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A → identifier_map tag A ≝ 170 λtag,A,m,l,p,a. 171 let l' ≝ match l with [ an_identifier l' ⇒ l' ] in 172 let m' ≝ match m with [ an_id_map m' ⇒ m' ] in 173 let u' ≝ update A 16 l' a m' in 174 match u' return λx. update ????? = x → ? with 175 [ None ⇒ λE.⊥ 176 | Some m' ⇒ λ_. an_id_map tag A m' 177 ] (refl ? u'). 178 whd in p; whd in p:(?(??%?)) E:(??(???%?%)?); 179 cases l in p E; cases m; -l' -m' #m' #l' whd in ⊢ (?(??(???%%)?) → ??(???%?%)? → ?) 180 #NL #U cases NL #H @H @(update_fail … U) 181 qed. 182 183 lemma update_still_present : ∀tag,A,m,id,a,id'. 184 ∀H:present tag A m id. 185 ∀H':present tag A m id'. 186 present tag A (update_present tag A m id' H' a) id. 187 #tag #A * #m * #id #a * #id' #H #H' 188 whd whd in ⊢ (?(??(???(%??????)?)?)) normalize nodelta 189 cases (identifier_eq ? (an_identifier tag id) (an_identifier tag id')) 190 [ #E >E @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) >(update_lookup_opt_same ?????? U) 191 % #E' destruct 192 | #NE @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) whd in ⊢ (?(??(???%%)?)) 193 <(update_lookup_opt_other ?????? U id) [ @H | % #E cases NE >E #H @H @refl ] 194 ] qed. 195 149 196 (* Sets *) 150 197
Note: See TracChangeset
for help on using the changeset viewer.