source: src/common/Identifiers.ma @ 1064

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

Evict CompCert? Maps interface in favour of BitVectorTries?.

File size: 5.1 KB
RevLine 
[736]1include "basics/types.ma".
2include "ASM/String.ma".
3include "ASM/Arithmetic.ma".
4include "common/Errors.ma".
5
[738]6(* identifiers and their generators are tagged to differentiate them, and to
[736]7   provide extra type checking. *)
8
[797]9(* in common/PreIdentifiers.ma, via Errors.ma.
[738]10inductive identifier (tag:String) : Type[0] ≝
11  an_identifier : Word → identifier tag.
[797]12*)
13
[738]14record universe (tag:String) : Type[0] ≝
[1055]15{
16  next_identifier : Word;
17  counter_overflow: bool
18}.
[736]19
[738]20definition new_universe : ∀tag:String. universe tag ≝
[1055]21  λtag. mk_universe tag (zero ?) false.
[797]22
[1056]23(* Fresh identifier generation uses delayed overflow checking.  To make sure
24   that the identifiers really were fresh, use the check_universe_ok function
25   below afterwards. *)
26definition fresh : ∀tag:String. universe tag → identifier tag × (universe tag) ≝
[1055]27  λtag.
28  λuniv: universe tag.
29  let 〈gen, carries〉 ≝ add_with_carries ? (next_identifier ? univ) (zero ?) true in
30    if get_index_v … carries 0 ? then
31      〈an_identifier tag (next_identifier ? univ), mk_universe tag gen true〉
32    else
33      〈an_identifier tag (next_identifier ? univ), mk_universe tag gen false〉.
34  //
35qed.
[797]36
[1056]37axiom TooManyIdentifiers : String.
38
39definition check_universe_ok : ∀tag:String. universe tag → res unit ≝
40  λtag, univ.
41  if counter_overflow ? univ
42  then Error ? (msg TooManyIdentifiers)
43  else OK ? it.
44
[757]45definition eq_identifier ≝
46  λt.
47  λl, r: identifier t.
48  match l with
49  [ an_identifier l' ⇒
50    match r with
51    [ an_identifier r' ⇒
52      eq_bv ? l' r'
53    ]
54  ].
55   
56definition word_of_identifier ≝
57  λt.
58  λl: identifier t.
59  match l with   
60  [ an_identifier l' ⇒ l'
61  ].
62
[738]63definition identifier_eq : ∀tag:String. ∀x,y:identifier tag. (x=y) + (x≠y).
[736]64#tag * #x * #y lapply (refl ? (eq_bv ? x y)) cases (eq_bv ? x y) in ⊢ (???% → %)
65#E [ % | %2 ]
66lapply E @eq_bv_elim
67[ #H #_ >H @refl | 2,3: #_ #H destruct | #H #_ % #H' destruct /2/ ]
68qed.
69
[738]70definition identifier_of_nat : ∀tag:String. nat → identifier tag ≝
[736]71  λtag,n. an_identifier tag (bitvector_of_nat ? n).
72
73
74(* Maps from identifiers to arbitrary types. *)
75
76include "ASM/BitVectorTrie.ma".
77
[753]78inductive identifier_map (tag:String) (A:Type[0]) : Type[0] ≝
79  an_id_map : BitVectorTrie A 16 → identifier_map tag A.
80 
[738]81definition empty_map : ∀tag:String. ∀A. identifier_map tag A ≝
[736]82  λtag,A. an_id_map tag A (Stub A 16).
83
[738]84definition lookup : ∀tag,A. identifier_map tag A → identifier tag → option A ≝
[736]85  λtag,A,m,l. lookup_opt A 16 (match l with [ an_identifier l' ⇒ l' ])
86                              (match m with [ an_id_map m' ⇒ m' ]).
87
[761]88(* Always adds the identifier to the map. *)
[738]89definition add : ∀tag,A. identifier_map tag A → identifier tag → A → identifier_map tag A ≝
[736]90λtag,A,m,l,a. an_id_map tag A (insert A 16 (match l with [ an_identifier l' ⇒ l' ]) a
91                                           (match m with [ an_id_map m' ⇒ m' ])).
92
[1058]93(* Extract every identifier, value pair from the map. *)
94definition elements : ∀tag,A. identifier_map tag A → list (identifier tag × A) ≝
95λtag,A,m.
96  fold ??? (λl,a,el. 〈an_identifier tag l, a〉::el)
97           (match m with [ an_id_map m' ⇒ m' ]) [ ].
98
[797]99axiom MissingId : String.
100
[761]101(* Only updates an existing entry; fails with an error otherwise. *)
102definition update : ∀tag,A. identifier_map tag A → identifier tag → A → res (identifier_map tag A) ≝
103λtag,A,m,l,a.
104  match update A 16 (match l with [ an_identifier l' ⇒ l' ]) a
105                    (match m with [ an_id_map m' ⇒ m' ]) with
[797]106  [ None ⇒ Error ? ([MSG MissingId; CTX tag l]) (* missing identifier *)
[761]107  | Some m' ⇒ OK ? (an_id_map tag A m')
108  ].
[736]109
[779]110(* Sets *)
111
112inductive identifier_set (tag:String) : Type[0] ≝
113  an_id_set : BitVectorTrie unit 16 → identifier_set tag.
114
115definition empty_set : ∀tag:String. identifier_set tag ≝
116λtag. an_id_set tag (Stub unit 16).
117
118definition add_set : ∀tag:String. identifier_set tag → identifier tag → identifier_set tag ≝
119λtag,s,i. an_id_set tag (insert unit 16 (match i with [ an_identifier i' ⇒ i' ])
120                                     it (match s with [ an_id_set s' ⇒ s' ])).
121
122definition singleton_set : ∀tag:String. identifier tag → identifier_set tag ≝
123λtag,i. add_set tag (empty_set tag) i.
124
125definition mem_set : ∀tag:String. identifier_set tag → identifier tag → bool ≝
126λtag,s,i. match lookup_opt ? 16 (match i with [ an_identifier i' ⇒ i' ])
127                                (match s with [ an_id_set s' ⇒ s' ]) with
128          [ None ⇒ false
129          | Some _ ⇒ true
130          ].
131
132definition union_set : ∀tag:String. identifier_set tag → identifier_set tag → identifier_set tag ≝
133λtag,s,s'. an_id_set tag (merge unit 16 (match s with [ an_id_set s0 ⇒ s0 ])
134                                        (match s' with [ an_id_set s1 ⇒ s1 ])).
[816]135
136interpretation "identifier set union" 'union a b = (union_set ? a b).
137notation "∅" non associative with precedence 90 for @{ 'empty }.
138interpretation "empty identifier set" 'empty = (empty_set ?).
139interpretation "singleton identifier set" 'singl a = (add_set ? (empty_set ?) a).
Note: See TracBrowser for help on using the repository browser.