source: src/common/Identifiers.ma @ 738

Last change on this file since 738 was 738, checked in by campbell, 10 years ago

Use lower case names for identifiers for consistency with CompCert? derived code
and to prevent confusion with the back-end equivalents until they're all merged.

File size: 2.0 KB
RevLine 
[736]1
2include "basics/types.ma".
3include "ASM/String.ma".
4include "ASM/Arithmetic.ma".
5include "common/Errors.ma".
6
[738]7(* identifiers and their generators are tagged to differentiate them, and to
[736]8   provide extra type checking. *)
9
[738]10inductive identifier (tag:String) : Type[0] ≝
11  an_identifier : Word → identifier tag.
[736]12 
[738]13record universe (tag:String) : Type[0] ≝
[736]14  { next_identifier : Word }.
15
16
[738]17definition new_universe : ∀tag:String. universe tag ≝
18  λtag. mk_universe tag (zero ?).
[736]19 
[738]20definition fresh : ∀tag. universe tag → res (identifier tag × (universe tag)) ≝
[736]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
[738]24      OK ? 〈an_identifier tag (next_identifier ? g), mk_universe tag gen〉.
[736]25// qed.
26
[738]27definition identifier_eq : ∀tag:String. ∀x,y:identifier tag. (x=y) + (x≠y).
[736]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
[738]34definition identifier_of_nat : ∀tag:String. nat → identifier tag ≝
[736]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
[738]42inductive identifier_map (tag:String) (A:Type[0]) : Type[0] ≝ an_id_map : BitVectorTrie A 16 → identifier_map tag A.
43definition empty_map : ∀tag:String. ∀A. identifier_map tag A ≝
[736]44  λtag,A. an_id_map tag A (Stub A 16).
45
[738]46definition lookup : ∀tag,A. identifier_map tag A → identifier tag → option A ≝
[736]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
[738]50definition add : ∀tag,A. identifier_map tag A → identifier tag → A → identifier_map tag A ≝
[736]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.