Changeset 1631 for src/common

Timestamp:

Dec 19, 2011, 2:48:37 PM (8 years ago)

Author:

campbell

Message:

Use fact that type environments in Cminor have distinct variables to
remove last freshness related axiom in front-end.

File:

• src/common/Identifiers.ma (modified) (6 diffs)

src/common/Identifiers.ma

@@ -2 +2 @@
 include "ASM/String.ma".
 include "utilities/binary/positive.ma".
+include "utilities/lists.ma".
 include "common/Errors.ma".
 
@@ -60 +61 @@
 #H #E whd % [ @(fresh_is_fresh … E) | @(All_mp … H) * #id #a #H' /2/ ]
 qed.
-
 
 definition eq_identifier : ∀t. identifier t → identifier t → bool ≝
@@ -110 +110 @@
 definition identifier_of_nat : ∀tag:String. nat → identifier tag ≝
   λtag,n. an_identifier tag (succ_pos_of_nat  n).
+
+
+(* States that all identifiers in an environment are distinct from one another. *)
+let rec distinct_env tag (A:Type[0]) (l:list (identifier tag × A)) on l : Prop ≝
+match l with
+[ nil ⇒ True
+| cons hd tl ⇒ All ? (λia. \fst hd ≠ \fst ia) tl ∧
+               distinct_env tag A tl
+].
+
+lemma distinct_env_append_l : ∀tag,A,l,r. distinct_env tag A (l@r) → distinct_env tag A l.
+#tag #A #l elim l
+[ //
+| * #id #a #tl #IH #r * #H1 #H2 % /2/
+] qed.
+
+lemma distinct_env_append_r : ∀tag,A,l,r. distinct_env tag A (l@r) → distinct_env tag A r.
+#tag #A #l elim l
+[ //
+| * #id #a #tl #IH #r * #H1 #H2 /2/
+] qed.
+
+(* check_distinct_env is quadratic - we could pay more attention when building maps to make sure that
+   the original environment was distinct. *)
+
+axiom DuplicateVariable : String.
+
+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) ≝
+match l return λl.res (All ?? l) with
+[ nil ⇒ OK ? I
+| cons hd tl ⇒
+    match identifier_eq tag id (\fst hd) with
+    [ inl _ ⇒ Error ? [MSG DuplicateVariable; CTX ? id]
+    | inr NE ⇒
+        do Htl ← check_member_env tag A id tl;
+        OK ? (conj ?? NE Htl)
+    ]
+].
+
+let rec check_distinct_env tag (A:Type[0]) (l:list (identifier tag × A)) on l : res (distinct_env tag A l) ≝
+match l return λl.res (distinct_env tag A l) with
+[ nil ⇒ OK ? I
+| cons hd tl ⇒
+    do Hhd ← check_member_env tag A (\fst hd) tl;
+    do Htl ← check_distinct_env tag A tl;
+    OK ? (conj ?? Hhd Htl)
+].
+
+
 
 
@@ -263 +312 @@
   lookup … m id = None A.
 
+lemma fresh_for_empty_map : ∀tag,A,id.
+  fresh_for_map tag A id (empty_map tag A).
+#tag #A * #id //
+qed.
+
 definition fresh_map_for_univ ≝
 λtag,A. λm:identifier_map tag A. λu:universe tag.
@@ -305 +359 @@
 qed.
 
+lemma fresh_for_map_add : ∀tag,A,id,m,id',a.
+  id ≠ id' →
+  fresh_for_map tag A id m →
+  fresh_for_map tag A id (add tag A m id' a).
+#tag #A * #id #m #id' #a #NE #F
+whd >lookup_add_miss //
+qed.
+
+
 (* Sets *)
 
@@ -343 +406 @@
 lemma union_empty_r : ∀tag.∀s:identifier_set tag. s ∪ ∅ = s.
 #tag * * // qed.
+