source: src/common/Identifiers.ma @ 1562

Last change on this file since 1562 was 1562, checked in by mulligan, 10 years ago

new version of assembly, fixed conflict in positivemap.ma, changed erroneous axiom in identifiers.ma

File size: 9.0 KB
Line 
1include "basics/types.ma".
2include "ASM/String.ma".
3include "utilities/binary/positive.ma".
4include "common/Errors.ma".
5include "utilities/option.ma".
6
7(* identifiers and their generators are tagged to differentiate them, and to
8   provide extra type checking. *)
9
10(* in common/PreIdentifiers.ma, via Errors.ma.
11inductive identifier (tag:String) : Type[0] ≝
12  an_identifier : Pos → identifier tag.
13*)
14
15record universe (tag:String) : Type[0] ≝
16{
17  next_identifier : Pos
18}.
19
20definition new_universe : ∀tag:String. universe tag ≝
21  λtag. mk_universe tag one.
22
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) ≝
27  λtag.
28  λuniv: universe tag.
29  let id ≝ next_identifier ? univ in
30  〈an_identifier tag id, mk_universe tag (succ id)〉.
31
32definition eq_identifier : ∀t. identifier t → identifier t → bool ≝
33  λt,l,r.
34  match l with
35  [ an_identifier l' ⇒
36    match r with
37    [ an_identifier r' ⇒
38      eqb l' r'
39    ]
40  ].
41
42lemma eq_identifier_elim : ∀P:bool → Type[0]. ∀t,x,y.
43  (x = y → P true) → (x ≠ y → P false) →
44  P (eq_identifier t x y).
45#P #t * #x * #y #T #F
46change with (P (eqb ??))
47@(eqb_elim x y P) [ /2/ | * #H @F % #E destruct /2/ ]
48qed.
49   
50definition word_of_identifier ≝
51  λt.
52  λl: identifier t.
53  match l with   
54  [ an_identifier l' ⇒ l'
55  ].
56
57lemma eq_identifier_refl : ∀tag,id. eq_identifier tag id id = true.
58#tag * #id whd in ⊢ (??%?); >eqb_n_n @refl
59qed.
60
61axiom eq_identifier_sym:
62  ∀tag: String.
63  ∀l  : identifier tag.
64  ∀r  : identifier tag.
65    eq_identifier tag l r = eq_identifier tag r l.
66
67lemma eq_identifier_false : ∀tag,x,y. x≠y → eq_identifier tag x y = false.
68#tag * #x * #y #NE normalize @not_eq_to_eqb_false /2/
69qed.
70
71definition identifier_eq : ∀tag:String. ∀x,y:identifier tag. (x=y) + (x≠y).
72#tag * #x * #y lapply (refl ? (eqb x y)) cases (eqb x y) in ⊢ (???% → %);
73#E [ % | %2 ]
74lapply E @eqb_elim
75[ #H #_ >H @refl | 2,3: #_ #H destruct | #H #_ % #H' destruct /2/ ]
76qed.
77
78definition identifier_of_nat : ∀tag:String. nat → identifier tag ≝
79  λtag,n. an_identifier tag (succ_pos_of_nat  n).
80
81
82(* Maps from identifiers to arbitrary types. *)
83
84include "common/PositiveMap.ma".
85
86inductive identifier_map (tag:String) (A:Type[0]) : Type[0] ≝
87  an_id_map : positive_map A → identifier_map tag A.
88 
89definition empty_map : ∀tag:String. ∀A. identifier_map tag A ≝
90  λtag,A. an_id_map tag A (pm_leaf A).
91
92let rec lookup tag A (m:identifier_map tag A) (l:identifier tag) on m : option A ≝
93  lookup_opt A (match l with [ an_identifier l' ⇒ l' ])
94               (match m with [ an_id_map m' ⇒ m' ]).
95
96definition lookup_def ≝
97λtag,A,m,l,d. match lookup tag A m l with [ None ⇒ d | Some x ⇒ x].
98
99let rec member tag A (m:identifier_map tag A) (l:identifier tag) on m : bool ≝
100  match lookup tag A m l with [ None ⇒ false | _ ⇒ true ].
101
102(* Always adds the identifier to the map. *)
103let rec add tag A (m:identifier_map tag A) (l:identifier tag) (a:A) on m : identifier_map tag A ≝
104  an_id_map tag A (insert A (match l with [ an_identifier l' ⇒ l' ]) a
105                            (match m with [ an_id_map m' ⇒ m' ])).
106
107lemma lookup_add_hit : ∀tag,A,m,i,a.
108  lookup tag A (add tag A m i a) i = Some ? a.
109#tag #A * #m * #i #a
110@lookup_opt_insert_hit
111qed.
112
113lemma lookup_def_add_hit : ∀tag,A,m,i,a,d.
114  lookup_def tag A (add tag A m i a) i d = a.
115#tag #A * #m * #i #a #d
116@lookup_insert_hit
117qed.
118
119lemma lookup_add_miss : ∀tag,A,m,i,j,a.
120  i ≠ j →
121  lookup tag A (add tag A m j a) i = lookup tag A m i.
122#tag #A * #m * #i * #j #a #H
123@lookup_opt_insert_miss /2/
124qed.
125
126axiom lookup_def_add_miss : ∀tag,A,m,i,j,a,d.
127  i ≠ j →
128  lookup_def tag A (add tag A m j a) i d = lookup_def tag A m i d.
129
130lemma lookup_add_oblivious : ∀tag,A,m,i,j,a.
131  (lookup tag A m i ≠ None ?) →
132  lookup tag A (add tag A m j a) i ≠ None ?.
133#tag #A #m #i #j #a #H
134cases (identifier_eq ? i j)
135[ #E >E >lookup_add_hit % #N destruct
136| #NE >lookup_add_miss //
137] qed.
138
139lemma lookup_add_cases : ∀tag,A,m,i,j,a,v.
140  lookup tag A (add tag A m i a) j = Some ? v →
141  (i=j ∧ v = a) ∨ lookup tag A m j = Some ? v.
142#tag #A #m #i #j #a #v
143cases (identifier_eq ? i j)
144[ #E >E >lookup_add_hit #H %1 destruct % //
145| #NE >lookup_add_miss /2/
146] qed.
147
148(* Extract every identifier, value pair from the map. *)
149definition elements : ∀tag,A. identifier_map tag A → list (identifier tag × A) ≝
150λtag,A,m.
151  fold ?? (λl,a,el. 〈an_identifier tag l, a〉::el)
152          (match m with [ an_id_map m' ⇒ m' ]) [ ].
153
154axiom MissingId : String.
155
156(* Only updates an existing entry; fails with an error otherwise. *)
157definition update : ∀tag,A. identifier_map tag A → identifier tag → A → res (identifier_map tag A) ≝
158λtag,A,m,l,a.
159  match update A (match l with [ an_identifier l' ⇒ l' ]) a
160                 (match m with [ an_id_map m' ⇒ m' ]) with
161  [ None ⇒ Error ? ([MSG MissingId; CTX tag l]) (* missing identifier *)
162  | Some m' ⇒ OK ? (an_id_map tag A m')
163  ].
164
165definition foldi:
166  ∀A, B: Type[0].
167  ∀tag: String.
168  (identifier tag -> A -> B -> B) -> identifier_map tag A -> B -> B ≝
169λA,B,tag,f,m,b.
170  match m with
171  [ an_id_map m' ⇒ fold A B (λbv. f (an_identifier ? bv)) m' b ].
172
173(* A predicate that an identifier is in a map, and a failure-avoiding lookup
174   and update using it. *)
175
176definition present : ∀tag,A. identifier_map tag A → identifier tag → Prop ≝
177λtag,A,m,i. lookup … m i ≠ None ?.
178
179lemma member_present : ∀tag,A,m,id.
180  member tag A m id = true → present tag A m id.
181#tag #A * #m #id normalize cases (lookup_opt A ??) normalize
182[ #E destruct
183| #x #E % #E' destruct
184] qed.
185
186include "ASM/Util.ma".
187
188definition lookup_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A ≝
189λtag,A,m,id. match lookup ?? m id return λx. x ≠ None ? → ? with [ Some a ⇒ λ_. a | None ⇒ λH.⊥ ].
190cases H #H'  cases (H' (refl ??)) qed.
191
192lemma lookup_lookup_present : ∀tag,A,m,id,p.
193  lookup tag A m id = Some ? (lookup_present tag A m id p).
194#tag #A #m #id #p
195whd in p ⊢ (???(??%));
196cases (lookup tag A m id) in p ⊢ %;
197[ * #H @⊥ @H @refl
198| #a #H @refl
199] qed.
200
201definition update_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A → identifier_map tag A ≝
202λtag,A,m,l,p,a.
203  let l' ≝ match l with [ an_identifier l' ⇒ l' ] in
204  let m' ≝ match m with [ an_id_map m' ⇒ m' ] in
205  let u' ≝ update A l' a m' in
206  match u' return λx. update ???? = x → ? with
207  [ None ⇒ λE.⊥
208  | Some m' ⇒ λ_. an_id_map tag A m'
209  ] (refl ? u').
210cases l in p E; cases m; -l' -m' #m' #l'
211whd in ⊢ (% → ?);
212 whd in ⊢ (?(??(???%%)?) → ??(??%?%)? → ?);
213#NL #U cases NL #H @H @(update_fail … U)
214qed.
215
216lemma update_still_present : ∀tag,A,m,id,a,id'.
217  ∀H:present tag A m id.
218  ∀H':present tag A m id'.
219  present tag A (update_present tag A m id' H' a) id.
220#tag #A * #m * #id #a * #id' #H #H'
221whd whd in ⊢ (?(??(???(%??????)?)?)); normalize nodelta
222cases (identifier_eq ? (an_identifier tag id) (an_identifier tag id'))
223[ #E >E @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)); >(update_lookup_opt_same ????? U)
224  % #E' destruct
225| #NE @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)); whd in ⊢ (?(??(??%%)?));
226  <(update_lookup_opt_other ????? U id) [ @H | % #E cases NE >E #H @H @refl ]
227] qed.
228
229(* Sets *)
230
231inductive identifier_set (tag:String) : Type[0] ≝
232  an_id_set : positive_map unit → identifier_set tag.
233
234definition empty_set : ∀tag:String. identifier_set tag ≝
235λtag. an_id_set tag (pm_leaf unit).
236
237let rec add_set (tag:String) (s:identifier_set tag) (i:identifier tag) on s : identifier_set tag ≝
238  an_id_set tag (insert unit (match i with [ an_identifier i' ⇒ i' ])
239                          it (match s with [ an_id_set s' ⇒ s' ])).
240
241definition singleton_set : ∀tag:String. identifier tag → identifier_set tag ≝
242λtag,i. add_set tag (empty_set tag) i.
243
244let rec mem_set (tag:String) (s:identifier_set tag) (i:identifier tag) on s : bool ≝
245  match lookup_opt ? (match i with [ an_identifier i' ⇒ i' ])
246                     (match s with [ an_id_set s' ⇒ s' ]) with
247  [ None ⇒ false
248  | Some _ ⇒ true
249  ].
250
251let rec union_set (tag:String) (s:identifier_set tag) (s':identifier_set tag) on s : identifier_set tag ≝
252  an_id_set tag (merge unit (match s with [ an_id_set s0 ⇒ s0 ])
253                            (match s' with [ an_id_set s1 ⇒ s1 ])).
254
255interpretation "identifier set union" 'union a b = (union_set ? a b).
256notation "∅" non associative with precedence 90 for @{ 'empty }.
257interpretation "empty identifier set" 'empty = (empty_set ?).
258interpretation "singleton identifier set" 'singl a = (add_set ? (empty_set ?) a).
259interpretation "identifier set membership" 'mem a b = (mem_set ? b a).
260
261lemma union_empty_l : ∀tag.∀s:identifier_set tag. ∅ ∪ s = s.
262#tag * //
263qed.
264
265lemma union_empty_r : ∀tag.∀s:identifier_set tag. s ∪ ∅ = s.
266#tag * * // qed.
Note: See TracBrowser for help on using the repository browser.