source: src/common/Identifiers.ma @ 779

Last change on this file since 779 was 779, checked in by campbell, 9 years ago

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 size: 3.9 KB
Line 
1
2include "basics/types.ma".
3include "ASM/String.ma".
4include "ASM/Arithmetic.ma".
5include "common/Errors.ma".
6
7(* identifiers and their generators are tagged to differentiate them, and to
8   provide extra type checking. *)
9
10inductive identifier (tag:String) : Type[0] ≝
11  an_identifier : Word → identifier tag.
12 
13record universe (tag:String) : Type[0] ≝
14  { next_identifier : Word }.
15
16
17definition new_universe : ∀tag:String. universe tag ≝
18  λtag. mk_universe tag (zero ?).
19 
20definition fresh : ∀tag. universe tag → res (identifier tag × (universe tag)) ≝
21λtag,g.
22  let 〈gen, carries〉 ≝ add_with_carries ? (next_identifier ? g) (zero ?) true in
23    if get_index_v ?? carries 0 ? then Error ? else
24      OK ? 〈an_identifier tag (next_identifier ? g), mk_universe tag gen〉.
25// qed.
26
27definition eq_identifier ≝
28  λt.
29  λl, r: identifier t.
30  match l with
31  [ an_identifier l' ⇒
32    match r with
33    [ an_identifier r' ⇒
34      eq_bv ? l' r'
35    ]
36  ].
37   
38   
39definition word_of_identifier ≝
40  λt.
41  λl: identifier t.
42  match l with   
43  [ an_identifier l' ⇒ l'
44  ].
45
46definition identifier_eq : ∀tag:String. ∀x,y:identifier tag. (x=y) + (x≠y).
47#tag * #x * #y lapply (refl ? (eq_bv ? x y)) cases (eq_bv ? x y) in ⊢ (???% → %)
48#E [ % | %2 ]
49lapply E @eq_bv_elim
50[ #H #_ >H @refl | 2,3: #_ #H destruct | #H #_ % #H' destruct /2/ ]
51qed.
52
53definition identifier_of_nat : ∀tag:String. nat → identifier tag ≝
54  λtag,n. an_identifier tag (bitvector_of_nat ? n).
55
56
57(* Maps from identifiers to arbitrary types. *)
58
59include "ASM/BitVectorTrie.ma".
60
61inductive identifier_map (tag:String) (A:Type[0]) : Type[0] ≝
62  an_id_map : BitVectorTrie A 16 → identifier_map tag A.
63 
64 
65definition empty_map : ∀tag:String. ∀A. identifier_map tag A ≝
66  λtag,A. an_id_map tag A (Stub A 16).
67
68definition lookup : ∀tag,A. identifier_map tag A → identifier tag → option A ≝
69  λtag,A,m,l. lookup_opt A 16 (match l with [ an_identifier l' ⇒ l' ])
70                              (match m with [ an_id_map m' ⇒ m' ]).
71
72(* Always adds the identifier to the map. *)
73definition add : ∀tag,A. identifier_map tag A → identifier tag → A → identifier_map tag A ≝
74λtag,A,m,l,a. an_id_map tag A (insert A 16 (match l with [ an_identifier l' ⇒ l' ]) a
75                                           (match m with [ an_id_map m' ⇒ m' ])).
76
77(* Only updates an existing entry; fails with an error otherwise. *)
78definition update : ∀tag,A. identifier_map tag A → identifier tag → A → res (identifier_map tag A) ≝
79λtag,A,m,l,a.
80  match update A 16 (match l with [ an_identifier l' ⇒ l' ]) a
81                    (match m with [ an_id_map m' ⇒ m' ]) with
82  [ None ⇒ Error ? (* missing identifier *)
83  | Some m' ⇒ OK ? (an_id_map tag A m')
84  ].
85
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 TracBrowser for help on using the repository browser.