Changeset 1631 for src/common
- Timestamp:
- Dec 19, 2011, 2:48:37 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/Identifiers.ma
r1627 r1631 2 2 include "ASM/String.ma". 3 3 include "utilities/binary/positive.ma". 4 include "utilities/lists.ma". 4 5 include "common/Errors.ma". 5 6 … … 60 61 #H #E whd % [ @(fresh_is_fresh … E) | @(All_mp … H) * #id #a #H' /2/ ] 61 62 qed. 62 63 63 64 64 definition eq_identifier : ∀t. identifier t → identifier t → bool ≝ … … 110 110 definition identifier_of_nat : ∀tag:String. nat → identifier tag ≝ 111 111 λtag,n. an_identifier tag (succ_pos_of_nat n). 112 113 114 (* States that all identifiers in an environment are distinct from one another. *) 115 let rec distinct_env tag (A:Type[0]) (l:list (identifier tag × A)) on l : Prop ≝ 116 match l with 117 [ nil ⇒ True 118 | cons hd tl ⇒ All ? (λia. \fst hd ≠ \fst ia) tl ∧ 119 distinct_env tag A tl 120 ]. 121 122 lemma distinct_env_append_l : ∀tag,A,l,r. distinct_env tag A (l@r) → distinct_env tag A l. 123 #tag #A #l elim l 124 [ // 125 | * #id #a #tl #IH #r * #H1 #H2 % /2/ 126 ] qed. 127 128 lemma distinct_env_append_r : ∀tag,A,l,r. distinct_env tag A (l@r) → distinct_env tag A r. 129 #tag #A #l elim l 130 [ // 131 | * #id #a #tl #IH #r * #H1 #H2 /2/ 132 ] qed. 133 134 (* check_distinct_env is quadratic - we could pay more attention when building maps to make sure that 135 the original environment was distinct. *) 136 137 axiom DuplicateVariable : String. 138 139 let rec check_member_env tag (A:Type[0]) (id:identifier tag) (l:list (identifier tag × A)) on l : res (All ? (λia. id ≠ \fst ia) l) ≝ 140 match l return λl.res (All ?? l) with 141 [ nil ⇒ OK ? I 142 | cons hd tl ⇒ 143 match identifier_eq tag id (\fst hd) with 144 [ inl _ ⇒ Error ? [MSG DuplicateVariable; CTX ? id] 145 | inr NE ⇒ 146 do Htl ← check_member_env tag A id tl; 147 OK ? (conj ?? NE Htl) 148 ] 149 ]. 150 151 let rec check_distinct_env tag (A:Type[0]) (l:list (identifier tag × A)) on l : res (distinct_env tag A l) ≝ 152 match l return λl.res (distinct_env tag A l) with 153 [ nil ⇒ OK ? I 154 | cons hd tl ⇒ 155 do Hhd ← check_member_env tag A (\fst hd) tl; 156 do Htl ← check_distinct_env tag A tl; 157 OK ? (conj ?? Hhd Htl) 158 ]. 159 160 112 161 113 162 … … 263 312 lookup … m id = None A. 264 313 314 lemma fresh_for_empty_map : ∀tag,A,id. 315 fresh_for_map tag A id (empty_map tag A). 316 #tag #A * #id // 317 qed. 318 265 319 definition fresh_map_for_univ ≝ 266 320 λtag,A. λm:identifier_map tag A. λu:universe tag. … … 305 359 qed. 306 360 361 lemma fresh_for_map_add : ∀tag,A,id,m,id',a. 362 id ≠ id' → 363 fresh_for_map tag A id m → 364 fresh_for_map tag A id (add tag A m id' a). 365 #tag #A * #id #m #id' #a #NE #F 366 whd >lookup_add_miss // 367 qed. 368 369 307 370 (* Sets *) 308 371 … … 343 406 lemma union_empty_r : ∀tag.∀s:identifier_set tag. s ∪ ∅ = s. 344 407 #tag * * // qed. 408
Note: See TracChangeset
for help on using the changeset viewer.