source: src/common/Identifiers.ma @ 789

Last change on this file since 789 was 782, checked in by mulligan, 9 years ago

More work on rtl-ertl pass from today, plus resolved conflict.

File size: 3.9 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
[757]27definition 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   
39definition word_of_identifier ≝
40  λt.
41  λl: identifier t.
42  match l with   
43  [ an_identifier l' ⇒ l'
44  ].
45
[738]46definition identifier_eq : ∀tag:String. ∀x,y:identifier tag. (x=y) + (x≠y).
[736]47#tag * #x * #y lapply (refl ? (eq_bv ? x y)) cases (eq_bv ? x y) in ⊢ (???% → %)
48#E [ % | %2 ]
49lapply E @eq_bv_elim
50[ #H #_ >H @refl | 2,3: #_ #H destruct | #H #_ % #H' destruct /2/ ]
51qed.
52
[738]53definition identifier_of_nat : ∀tag:String. nat → identifier tag ≝
[736]54  λtag,n. an_identifier tag (bitvector_of_nat ? n).
55
56
57(* Maps from identifiers to arbitrary types. *)
58
59include "ASM/BitVectorTrie.ma".
60
[753]61inductive identifier_map (tag:String) (A:Type[0]) : Type[0] ≝
62  an_id_map : BitVectorTrie A 16 → identifier_map tag A.
63 
[738]64definition empty_map : ∀tag:String. ∀A. identifier_map tag A ≝
[736]65  λtag,A. an_id_map tag A (Stub A 16).
66
[738]67definition lookup : ∀tag,A. identifier_map tag A → identifier tag → option A ≝
[736]68  λtag,A,m,l. lookup_opt A 16 (match l with [ an_identifier l' ⇒ l' ])
69                              (match m with [ an_id_map m' ⇒ m' ]).
70
[761]71(* Always adds the identifier to the map. *)
[738]72definition add : ∀tag,A. identifier_map tag A → identifier tag → A → identifier_map tag A ≝
[736]73λtag,A,m,l,a. an_id_map tag A (insert A 16 (match l with [ an_identifier l' ⇒ l' ]) a
74                                           (match m with [ an_id_map m' ⇒ m' ])).
75
[761]76(* Only updates an existing entry; fails with an error otherwise. *)
77definition update : ∀tag,A. identifier_map tag A → identifier tag → A → res (identifier_map tag A) ≝
78λtag,A,m,l,a.
79  match update A 16 (match l with [ an_identifier l' ⇒ l' ]) a
80                    (match m with [ an_id_map m' ⇒ m' ]) with
81  [ None ⇒ Error ? (* missing identifier *)
82  | Some m' ⇒ OK ? (an_id_map tag A m')
83  ].
[736]84
[779]85(* Sets *)
86
87inductive identifier_set (tag:String) : Type[0] ≝
88  an_id_set : BitVectorTrie unit 16 → identifier_set tag.
89
90definition empty_set : ∀tag:String. identifier_set tag ≝
91λtag. an_id_set tag (Stub unit 16).
92
93definition add_set : ∀tag:String. identifier_set tag → identifier tag → identifier_set tag ≝
94λtag,s,i. an_id_set tag (insert unit 16 (match i with [ an_identifier i' ⇒ i' ])
95                                     it (match s with [ an_id_set s' ⇒ s' ])).
96
97definition singleton_set : ∀tag:String. identifier tag → identifier_set tag ≝
98λtag,i. add_set tag (empty_set tag) i.
99
100definition mem_set : ∀tag:String. identifier_set tag → identifier tag → bool ≝
101λtag,s,i. match lookup_opt ? 16 (match i with [ an_identifier i' ⇒ i' ])
102                                (match s with [ an_id_set s' ⇒ s' ]) with
103          [ None ⇒ false
104          | Some _ ⇒ true
105          ].
106
107definition union_set : ∀tag:String. identifier_set tag → identifier_set tag → identifier_set tag ≝
108λtag,s,s'. an_id_set tag (merge unit 16 (match s with [ an_id_set s0 ⇒ s0 ])
109                                        (match s' with [ an_id_set s1 ⇒ s1 ])).
Note: See TracBrowser for help on using the repository browser.