Changeset 779 for src/common


Ignore:
Timestamp:
Apr 28, 2011, 10:55:47 AM (9 years ago)
Author:
campbell
Message:

Add merging of tries and identifier sets (based on Dominic's earlier code).
Not used at present (I decided to implement the part that would have used it
differently).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Identifiers.ma

    r761 r779  
    8484  ].
    8585
     86(* Sets *)
     87
     88inductive identifier_set (tag:String) : Type[0] ≝
     89  an_id_set : BitVectorTrie unit 16 → identifier_set tag.
     90
     91definition empty_set : ∀tag:String. identifier_set tag ≝
     92λtag. an_id_set tag (Stub unit 16).
     93
     94definition add_set : ∀tag:String. identifier_set tag → identifier tag → identifier_set tag ≝
     95λtag,s,i. an_id_set tag (insert unit 16 (match i with [ an_identifier i' ⇒ i' ])
     96                                     it (match s with [ an_id_set s' ⇒ s' ])).
     97
     98definition singleton_set : ∀tag:String. identifier tag → identifier_set tag ≝
     99λtag,i. add_set tag (empty_set tag) i.
     100
     101definition mem_set : ∀tag:String. identifier_set tag → identifier tag → bool ≝
     102λtag,s,i. match lookup_opt ? 16 (match i with [ an_identifier i' ⇒ i' ])
     103                                (match s with [ an_id_set s' ⇒ s' ]) with
     104          [ None ⇒ false
     105          | Some _ ⇒ true
     106          ].
     107
     108definition union_set : ∀tag:String. identifier_set tag → identifier_set tag → identifier_set tag ≝
     109λtag,s,s'. an_id_set tag (merge unit 16 (match s with [ an_id_set s0 ⇒ s0 ])
     110                                        (match s' with [ an_id_set s1 ⇒ s1 ])).
Note: See TracChangeset for help on using the changeset viewer.