1 | |
---|
2 | include "basics/types.ma". |
---|
3 | include "ASM/String.ma". |
---|
4 | include "ASM/Arithmetic.ma". |
---|
5 | include "common/Errors.ma". |
---|
6 | |
---|
7 | (* identifiers and their generators are tagged to differentiate them, and to |
---|
8 | provide extra type checking. *) |
---|
9 | |
---|
10 | inductive identifier (tag:String) : Type[0] ≝ |
---|
11 | an_identifier : Word → identifier tag. |
---|
12 | |
---|
13 | record universe (tag:String) : Type[0] ≝ |
---|
14 | { next_identifier : Word }. |
---|
15 | |
---|
16 | |
---|
17 | definition new_universe : ∀tag:String. universe tag ≝ |
---|
18 | λtag. mk_universe tag (zero ?). |
---|
19 | |
---|
20 | definition 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 | |
---|
27 | definition 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 | |
---|
39 | definition word_of_identifier ≝ |
---|
40 | λt. |
---|
41 | λl: identifier t. |
---|
42 | match l with |
---|
43 | [ an_identifier l' ⇒ l' |
---|
44 | ]. |
---|
45 | |
---|
46 | definition 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 ] |
---|
49 | lapply E @eq_bv_elim |
---|
50 | [ #H #_ >H @refl | 2,3: #_ #H destruct | #H #_ % #H' destruct /2/ ] |
---|
51 | qed. |
---|
52 | |
---|
53 | definition 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 | |
---|
59 | include "ASM/BitVectorTrie.ma". |
---|
60 | |
---|
61 | inductive identifier_map (tag:String) (A:Type[0]) : Type[0] ≝ |
---|
62 | an_id_map : BitVectorTrie A 16 → identifier_map tag A. |
---|
63 | |
---|
64 | |
---|
65 | definition empty_map : ∀tag:String. ∀A. identifier_map tag A ≝ |
---|
66 | λtag,A. an_id_map tag A (Stub A 16). |
---|
67 | |
---|
68 | definition 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. *) |
---|
73 | definition 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. *) |
---|
78 | definition 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 | |
---|
88 | inductive identifier_set (tag:String) : Type[0] ≝ |
---|
89 | an_id_set : BitVectorTrie unit 16 → identifier_set tag. |
---|
90 | |
---|
91 | definition empty_set : ∀tag:String. identifier_set tag ≝ |
---|
92 | λtag. an_id_set tag (Stub unit 16). |
---|
93 | |
---|
94 | definition 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 | |
---|
98 | definition singleton_set : ∀tag:String. identifier tag → identifier_set tag ≝ |
---|
99 | λtag,i. add_set tag (empty_set tag) i. |
---|
100 | |
---|
101 | definition 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 | |
---|
108 | definition 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 ])). |
---|