| 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 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 ] |
|---|
| 30 | lapply E @eq_bv_elim |
|---|
| 31 | [ #H #_ >H @refl | 2,3: #_ #H destruct | #H #_ % #H' destruct /2/ ] |
|---|
| 32 | qed. |
|---|
| 33 | |
|---|
| 34 | definition identifier_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 | |
|---|
| 40 | include "ASM/BitVectorTrie.ma". |
|---|
| 41 | |
|---|
| 42 | inductive identifier_map (tag:String) (A:Type[0]) : Type[0] ≝ |
|---|
| 43 | an_id_map : BitVectorTrie A 16 → identifier_map tag A. |
|---|
| 44 | |
|---|
| 45 | |
|---|
| 46 | definition empty_map : ∀tag:String. ∀A. identifier_map tag A ≝ |
|---|
| 47 | λtag,A. an_id_map tag A (Stub A 16). |
|---|
| 48 | |
|---|
| 49 | definition lookup : ∀tag,A. identifier_map tag A → identifier tag → option A ≝ |
|---|
| 50 | λtag,A,m,l. lookup_opt A 16 (match l with [ an_identifier l' ⇒ l' ]) |
|---|
| 51 | (match m with [ an_id_map m' ⇒ m' ]). |
|---|
| 52 | |
|---|
| 53 | definition add : ∀tag,A. identifier_map tag A → identifier tag → A → identifier_map tag A ≝ |
|---|
| 54 | λtag,A,m,l,a. an_id_map tag A (insert A 16 (match l with [ an_identifier l' ⇒ l' ]) a |
|---|
| 55 | (match m with [ an_id_map m' ⇒ m' ])). |
|---|
| 56 | |
|---|
| 57 | |
|---|
