Ignore:
Timestamp:
Jul 13, 2012, 11:20:36 AM (8 years ago)
Author:
tranquil
Message:

updated linearisation pass

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r2155 r2182  
    216216λtag,A,m,l,d. match lookup tag A m l with [ None ⇒ d | Some x ⇒ x].
    217217
    218 let rec member tag A (m:identifier_map tag A) (l:identifier tag) on m : bool ≝
     218definition member ≝
     219  λtag,A.λm:identifier_map tag A.λl:identifier tag.
    219220  match lookup tag A m l with [ None ⇒ false | _ ⇒ true ].
     221
     222interpretation "identifier map membership" 'mem a b = (member ?? b a).
     223
     224definition lookup_safe : ∀tag,A.∀m : identifier_map tag A.∀i.i∈m → A ≝
     225λtag,A,m,i.
     226match lookup … m i return λx.match x in option return λ_.bool with [ _ ⇒ ?] → ? with
     227[ Some x ⇒ λ_.x
     228| None ⇒ λprf.⊥
     229]. @prf qed.
     230
     231lemma lookup_eq_safe : ∀tag,A,m,i,prf.lookup tag A m i = Some ? (lookup_safe tag A m i prf).
     232#tag #A #m #i whd in match (i∈m);
     233whd in match lookup_safe; normalize nodelta
     234cases (lookup ????) normalize nodelta [*] // qed.
    220235
    221236(* Always adds the identifier to the map. *)
     
    472487λtag,i. add_set tag (empty_set tag) i.
    473488
    474 (* mem set is generalised to all maps *)
    475 let rec mem_set (tag:String) A (s:identifier_map tag A) (i:identifier tag) on s : bool ≝
    476   match lookup … s i with
    477   [ None ⇒ false
    478   | Some _ ⇒ true
    479   ].
    480  
    481489let rec union_set (tag:String) A B (s:identifier_map tag A) (s':identifier_map tag B) on s : identifier_set tag ≝
    482490  an_id_map tag unit (merge … (λo,o'.match o with [Some _ ⇒ Some ? it | None ⇒ !_ o'; return it])
     
    497505interpretation "empty identifier set" 'empty = (empty_set ?).
    498506interpretation "singleton identifier set" 'singl a = (add_set ? (empty_set ?) a).
    499 interpretation "identifier set membership" 'mem a b = (mem_set ?? b a).
    500507interpretation "identifier map difference" 'setminus a b = (minus_set ??? a b).
    501508
     
    720727qed.
    721728
    722 lemma mem_set_empty : ∀tag.∀i: identifier tag. i∈∅ = false.
    723 #tag * #i normalize %
     729lemma mem_set_empty : ∀tag,A.∀i: identifier tag. i∈empty_map tag A = false.
     730#tag #A * #i normalize %
    724731qed.
    725732
Note: See TracChangeset for help on using the changeset viewer.