Changeset 1631 for src/common


Ignore:
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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r1627 r1631  
    22include "ASM/String.ma".
    33include "utilities/binary/positive.ma".
     4include "utilities/lists.ma".
    45include "common/Errors.ma".
    56
     
    6061#H #E whd % [ @(fresh_is_fresh … E) | @(All_mp … H) * #id #a #H' /2/ ]
    6162qed.
    62 
    6363
    6464definition eq_identifier : ∀t. identifier t → identifier t → bool ≝
     
    110110definition identifier_of_nat : ∀tag:String. nat → identifier tag ≝
    111111  λ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. *)
     115let rec distinct_env tag (A:Type[0]) (l:list (identifier tag × A)) on l : Prop ≝
     116match l with
     117[ nil ⇒ True
     118| cons hd tl ⇒ All ? (λia. \fst hd ≠ \fst ia) tl ∧
     119               distinct_env tag A tl
     120].
     121
     122lemma 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
     128lemma 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
     137axiom DuplicateVariable : String.
     138
     139let 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) ≝
     140match 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
     151let rec check_distinct_env tag (A:Type[0]) (l:list (identifier tag × A)) on l : res (distinct_env tag A l) ≝
     152match 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
    112161
    113162
     
    263312  lookup … m id = None A.
    264313
     314lemma fresh_for_empty_map : ∀tag,A,id.
     315  fresh_for_map tag A id (empty_map tag A).
     316#tag #A * #id //
     317qed.
     318
    265319definition fresh_map_for_univ ≝
    266320λtag,A. λm:identifier_map tag A. λu:universe tag.
     
    305359qed.
    306360
     361lemma 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
     366whd >lookup_add_miss //
     367qed.
     368
     369
    307370(* Sets *)
    308371
     
    343406lemma union_empty_r : ∀tag.∀s:identifier_set tag. s ∪ ∅ = s.
    344407#tag * * // qed.
     408
Note: See TracChangeset for help on using the changeset viewer.