source: src/common/Identifiers.ma @ 1056

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

Switch to delayed identifier error scheme.

File size: 4.8 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
10(* in common/PreIdentifiers.ma, via Errors.ma.
11inductive identifier (tag:String) : Type[0] ≝
12  an_identifier : Word → identifier tag.
13*)
14
15record universe (tag:String) : Type[0] ≝
16{
17  next_identifier : Word;
18  counter_overflow: bool
19}.
20
21definition new_universe : ∀tag:String. universe tag ≝
22  λtag. mk_universe tag (zero ?) false.
23
24(* Fresh identifier generation uses delayed overflow checking.  To make sure
25   that the identifiers really were fresh, use the check_universe_ok function
26   below afterwards. *)
27definition fresh : ∀tag:String. universe tag → identifier tag × (universe tag) ≝
28  λtag.
29  λuniv: universe tag.
30  let 〈gen, carries〉 ≝ add_with_carries ? (next_identifier ? univ) (zero ?) true in
31    if get_index_v … carries 0 ? then
32      〈an_identifier tag (next_identifier ? univ), mk_universe tag gen true〉
33    else
34      〈an_identifier tag (next_identifier ? univ), mk_universe tag gen false〉.
35  //
36qed.
37
38axiom TooManyIdentifiers : String.
39
40definition check_universe_ok : ∀tag:String. universe tag → res unit ≝
41  λtag, univ.
42  if counter_overflow ? univ
43  then Error ? (msg TooManyIdentifiers)
44  else OK ? it.
45
46definition eq_identifier ≝
47  λt.
48  λl, r: identifier t.
49  match l with
50  [ an_identifier l' ⇒
51    match r with
52    [ an_identifier r' ⇒
53      eq_bv ? l' r'
54    ]
55  ].
56   
57definition word_of_identifier ≝
58  λt.
59  λl: identifier t.
60  match l with   
61  [ an_identifier l' ⇒ l'
62  ].
63
64definition identifier_eq : ∀tag:String. ∀x,y:identifier tag. (x=y) + (x≠y).
65#tag * #x * #y lapply (refl ? (eq_bv ? x y)) cases (eq_bv ? x y) in ⊢ (???% → %)
66#E [ % | %2 ]
67lapply E @eq_bv_elim
68[ #H #_ >H @refl | 2,3: #_ #H destruct | #H #_ % #H' destruct /2/ ]
69qed.
70
71definition identifier_of_nat : ∀tag:String. nat → identifier tag ≝
72  λtag,n. an_identifier tag (bitvector_of_nat ? n).
73
74
75(* Maps from identifiers to arbitrary types. *)
76
77include "ASM/BitVectorTrie.ma".
78
79inductive identifier_map (tag:String) (A:Type[0]) : Type[0] ≝
80  an_id_map : BitVectorTrie A 16 → identifier_map tag A.
81 
82definition empty_map : ∀tag:String. ∀A. identifier_map tag A ≝
83  λtag,A. an_id_map tag A (Stub A 16).
84
85definition lookup : ∀tag,A. identifier_map tag A → identifier tag → option A ≝
86  λtag,A,m,l. lookup_opt A 16 (match l with [ an_identifier l' ⇒ l' ])
87                              (match m with [ an_id_map m' ⇒ m' ]).
88
89(* Always adds the identifier to the map. *)
90definition add : ∀tag,A. identifier_map tag A → identifier tag → A → identifier_map tag A ≝
91λtag,A,m,l,a. an_id_map tag A (insert A 16 (match l with [ an_identifier l' ⇒ l' ]) a
92                                           (match m with [ an_id_map m' ⇒ m' ])).
93
94axiom MissingId : String.
95
96(* Only updates an existing entry; fails with an error otherwise. *)
97definition update : ∀tag,A. identifier_map tag A → identifier tag → A → res (identifier_map tag A) ≝
98λtag,A,m,l,a.
99  match update A 16 (match l with [ an_identifier l' ⇒ l' ]) a
100                    (match m with [ an_id_map m' ⇒ m' ]) with
101  [ None ⇒ Error ? ([MSG MissingId; CTX tag l]) (* missing identifier *)
102  | Some m' ⇒ OK ? (an_id_map tag A m')
103  ].
104
105(* Sets *)
106
107inductive identifier_set (tag:String) : Type[0] ≝
108  an_id_set : BitVectorTrie unit 16 → identifier_set tag.
109
110definition empty_set : ∀tag:String. identifier_set tag ≝
111λtag. an_id_set tag (Stub unit 16).
112
113definition add_set : ∀tag:String. identifier_set tag → identifier tag → identifier_set tag ≝
114λtag,s,i. an_id_set tag (insert unit 16 (match i with [ an_identifier i' ⇒ i' ])
115                                     it (match s with [ an_id_set s' ⇒ s' ])).
116
117definition singleton_set : ∀tag:String. identifier tag → identifier_set tag ≝
118λtag,i. add_set tag (empty_set tag) i.
119
120definition mem_set : ∀tag:String. identifier_set tag → identifier tag → bool ≝
121λtag,s,i. match lookup_opt ? 16 (match i with [ an_identifier i' ⇒ i' ])
122                                (match s with [ an_id_set s' ⇒ s' ]) with
123          [ None ⇒ false
124          | Some _ ⇒ true
125          ].
126
127definition union_set : ∀tag:String. identifier_set tag → identifier_set tag → identifier_set tag ≝
128λtag,s,s'. an_id_set tag (merge unit 16 (match s with [ an_id_set s0 ⇒ s0 ])
129                                        (match s' with [ an_id_set s1 ⇒ s1 ])).
130
131interpretation "identifier set union" 'union a b = (union_set ? a b).
132notation "∅" non associative with precedence 90 for @{ 'empty }.
133interpretation "empty identifier set" 'empty = (empty_set ?).
134interpretation "singleton identifier set" 'singl a = (add_set ? (empty_set ?) a).
Note: See TracBrowser for help on using the repository browser.