source: src/common/Identifiers.ma @ 736

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

Extra type safety for identifiers.

File size: 2.0 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 identifier_eq : ∀tag:String. ∀x,y:Identifier tag. (x=y) + (x≠y).
28#tag * #x * #y lapply (refl ? (eq_bv ? x y)) cases (eq_bv ? x y) in ⊢ (???% → %)
29#E [ % | %2 ]
30lapply E @eq_bv_elim
31[ #H #_ >H @refl | 2,3: #_ #H destruct | #H #_ % #H' destruct /2/ ]
32qed.
33
34definition identifer_of_nat : ∀tag:String. nat → Identifier tag ≝
35  λtag,n. an_identifier tag (bitvector_of_nat ? n).
36
37
38(* Maps from identifiers to arbitrary types. *)
39
40include "ASM/BitVectorTrie.ma".
41
42inductive IdentifierMap (tag:String) (A:Type[0]) : Type[0] ≝ an_id_map : BitVectorTrie A 16 → IdentifierMap tag A.
43definition empty_map : ∀tag:String. ∀A. IdentifierMap tag A ≝
44  λtag,A. an_id_map tag A (Stub A 16).
45
46definition lookup : ∀tag,A. IdentifierMap tag A → Identifier tag → option A ≝
47  λtag,A,m,l. lookup_opt A 16 (match l with [ an_identifier l' ⇒ l' ])
48                              (match m with [ an_id_map m' ⇒ m' ]).
49
50definition add : ∀tag,A. IdentifierMap tag A → Identifier tag → A → IdentifierMap tag A ≝
51λtag,A,m,l,a. an_id_map tag A (insert A 16 (match l with [ an_identifier l' ⇒ l' ]) a
52                                           (match m with [ an_id_map m' ⇒ m' ])).
53
54
Note: See TracBrowser for help on using the repository browser.