source: src/common/Identifiers.ma @ 1631

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

Use fact that type environments in Cminor have distinct variables to
remove last freshness related axiom in front-end.

File size: 13.1 KB
Line 
1include "basics/types.ma".
2include "ASM/String.ma".
3include "utilities/binary/positive.ma".
4include "utilities/lists.ma".
5include "common/Errors.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
23let rec fresh (tag:String) (u:universe tag) on u : identifier tag × (universe tag) ≝
24  let id ≝ next_identifier ? u in
25  〈an_identifier tag id, mk_universe tag (succ id)〉.
26
27
28let rec fresh_for_univ tag (id:identifier tag) (u:universe tag) on id : Prop ≝
29  match id with [ an_identifier p ⇒ p < next_identifier … u ].
30
31
32lemma fresh_is_fresh : ∀tag,id,u,u'.
33  〈id,u〉 = fresh tag u' →
34  fresh_for_univ tag id u.
35#tag * #id * #u * #u' #E whd in E:(???%); destruct //
36qed.
37
38lemma fresh_remains_fresh : ∀tag,id,id',u,u'.
39  fresh_for_univ tag id u →
40  〈id',u'〉 = fresh tag u →
41  fresh_for_univ tag id u'.
42#tag * #id * #id' * #u * #u' normalize #H #E destruct /2/
43qed.
44
45lemma fresh_distinct : ∀tag,id,id',u,u'.
46  fresh_for_univ tag id u →
47  〈id',u'〉 = fresh tag u →
48  id ≠ id'.
49#tag * #id * #id' * #u * #u' normalize #H #E destruct % #E' destruct /2/
50qed.
51
52
53let rec env_fresh_for_univ tag A (env:list (identifier tag × A)) (u:universe tag) on u : Prop ≝
54  All ? (λida. fresh_for_univ tag (\fst ida) u) env.
55
56lemma fresh_env_extend : ∀tag,A,env,u,u',id,a.
57  env_fresh_for_univ tag A env u →
58  〈id,u'〉 = fresh tag u →
59  env_fresh_for_univ tag A (〈id,a〉::env) u'.
60#tag #A #env * #u * #u' #id #a
61#H #E whd % [ @(fresh_is_fresh … E) | @(All_mp … H) * #id #a #H' /2/ ]
62qed.
63
64definition eq_identifier : ∀t. identifier t → identifier t → bool ≝
65  λt,l,r.
66  match l with
67  [ an_identifier l' ⇒
68    match r with
69    [ an_identifier r' ⇒
70      eqb l' r'
71    ]
72  ].
73
74lemma eq_identifier_elim : ∀P:bool → Type[0]. ∀t,x,y.
75  (x = y → P true) → (x ≠ y → P false) →
76  P (eq_identifier t x y).
77#P #t * #x * #y #T #F
78change with (P (eqb ??))
79@(eqb_elim x y P) [ /2/ | * #H @F % #E destruct /2/ ]
80qed.
81   
82definition word_of_identifier ≝
83  λt.
84  λl: identifier t.
85  match l with   
86  [ an_identifier l' ⇒ l'
87  ].
88
89lemma eq_identifier_refl : ∀tag,id. eq_identifier tag id id = true.
90#tag * #id whd in ⊢ (??%?); >eqb_n_n @refl
91qed.
92
93axiom eq_identifier_sym:
94  ∀tag: String.
95  ∀l  : identifier tag.
96  ∀r  : identifier tag.
97    eq_identifier tag l r = eq_identifier tag r l.
98
99lemma eq_identifier_false : ∀tag,x,y. x≠y → eq_identifier tag x y = false.
100#tag * #x * #y #NE normalize @not_eq_to_eqb_false /2/
101qed.
102
103definition identifier_eq : ∀tag:String. ∀x,y:identifier tag. (x=y) + (x≠y).
104#tag * #x * #y lapply (refl ? (eqb x y)) cases (eqb x y) in ⊢ (???% → %);
105#E [ % | %2 ]
106lapply E @eqb_elim
107[ #H #_ >H @refl | 2,3: #_ #H destruct | #H #_ % #H' destruct /2/ ]
108qed.
109
110definition identifier_of_nat : ∀tag:String. nat → identifier tag ≝
111  λtag,n. an_identifier tag (succ_pos_of_nat  n).
112
113
114(* States that all identifiers in an environment are distinct from one another. *)
115let rec distinct_env tag (A:Type[0]) (l:list (identifier tag × A)) on l : Prop ≝
116match l with
117[ nil ⇒ True
118| cons hd tl ⇒ All ? (λia. \fst hd ≠ \fst ia) tl ∧
119               distinct_env tag A tl
120].
121
122lemma distinct_env_append_l : ∀tag,A,l,r. distinct_env tag A (l@r) → distinct_env tag A l.
123#tag #A #l elim l
124[ //
125| * #id #a #tl #IH #r * #H1 #H2 % /2/
126] qed.
127
128lemma distinct_env_append_r : ∀tag,A,l,r. distinct_env tag A (l@r) → distinct_env tag A r.
129#tag #A #l elim l
130[ //
131| * #id #a #tl #IH #r * #H1 #H2 /2/
132] qed.
133
134(* check_distinct_env is quadratic - we could pay more attention when building maps to make sure that
135   the original environment was distinct. *)
136
137axiom DuplicateVariable : String.
138
139let rec check_member_env tag (A:Type[0]) (id:identifier tag) (l:list (identifier tag × A)) on l : res (All ? (λia. id ≠ \fst ia) l) ≝
140match l return λl.res (All ?? l) with
141[ nil ⇒ OK ? I
142| cons hd tl ⇒
143    match identifier_eq tag id (\fst hd) with
144    [ inl _ ⇒ Error ? [MSG DuplicateVariable; CTX ? id]
145    | inr NE ⇒
146        do Htl ← check_member_env tag A id tl;
147        OK ? (conj ?? NE Htl)
148    ]
149].
150
151let rec check_distinct_env tag (A:Type[0]) (l:list (identifier tag × A)) on l : res (distinct_env tag A l) ≝
152match l return λl.res (distinct_env tag A l) with
153[ nil ⇒ OK ? I
154| cons hd tl ⇒
155    do Hhd ← check_member_env tag A (\fst hd) tl;
156    do Htl ← check_distinct_env tag A tl;
157    OK ? (conj ?? Hhd Htl)
158].
159
160
161
162
163(* Maps from identifiers to arbitrary types. *)
164
165include "common/PositiveMap.ma".
166
167inductive identifier_map (tag:String) (A:Type[0]) : Type[0] ≝
168  an_id_map : positive_map A → identifier_map tag A.
169 
170definition empty_map : ∀tag:String. ∀A. identifier_map tag A ≝
171  λtag,A. an_id_map tag A (pm_leaf A).
172
173let rec lookup tag A (m:identifier_map tag A) (l:identifier tag) on m : option A ≝
174  lookup_opt A (match l with [ an_identifier l' ⇒ l' ])
175               (match m with [ an_id_map m' ⇒ m' ]).
176
177definition lookup_def ≝
178λtag,A,m,l,d. match lookup tag A m l with [ None ⇒ d | Some x ⇒ x].
179
180let rec member tag A (m:identifier_map tag A) (l:identifier tag) on m : bool ≝
181  match lookup tag A m l with [ None ⇒ false | _ ⇒ true ].
182
183(* Always adds the identifier to the map. *)
184let rec add tag A (m:identifier_map tag A) (l:identifier tag) (a:A) on m : identifier_map tag A ≝
185  an_id_map tag A (insert A (match l with [ an_identifier l' ⇒ l' ]) a
186                            (match m with [ an_id_map m' ⇒ m' ])).
187
188lemma lookup_add_hit : ∀tag,A,m,i,a.
189  lookup tag A (add tag A m i a) i = Some ? a.
190#tag #A * #m * #i #a
191@lookup_opt_insert_hit
192qed.
193
194lemma lookup_def_add_hit : ∀tag,A,m,i,a,d.
195  lookup_def tag A (add tag A m i a) i d = a.
196#tag #A * #m * #i #a #d
197@lookup_insert_hit
198qed.
199
200lemma lookup_add_miss : ∀tag,A,m,i,j,a.
201  i ≠ j →
202  lookup tag A (add tag A m j a) i = lookup tag A m i.
203#tag #A * #m * #i * #j #a #H
204@lookup_opt_insert_miss /2/
205qed.
206
207axiom lookup_def_add_miss : ∀tag,A,m,i,j,a,d.
208  i ≠ j →
209  lookup_def tag A (add tag A m j a) i d = lookup_def tag A m i d.
210
211lemma lookup_add_oblivious : ∀tag,A,m,i,j,a.
212  (lookup tag A m i ≠ None ?) →
213  lookup tag A (add tag A m j a) i ≠ None ?.
214#tag #A #m #i #j #a #H
215cases (identifier_eq ? i j)
216[ #E >E >lookup_add_hit % #N destruct
217| #NE >lookup_add_miss //
218] qed.
219
220lemma lookup_add_cases : ∀tag,A,m,i,j,a,v.
221  lookup tag A (add tag A m i a) j = Some ? v →
222  (i=j ∧ v = a) ∨ lookup tag A m j = Some ? v.
223#tag #A #m #i #j #a #v
224cases (identifier_eq ? i j)
225[ #E >E >lookup_add_hit #H %1 destruct % //
226| #NE >lookup_add_miss /2/
227] qed.
228
229(* Extract every identifier, value pair from the map. *)
230definition elements : ∀tag,A. identifier_map tag A → list (identifier tag × A) ≝
231λtag,A,m.
232  fold ?? (λl,a,el. 〈an_identifier tag l, a〉::el)
233          (match m with [ an_id_map m' ⇒ m' ]) [ ].
234
235axiom MissingId : String.
236
237(* Only updates an existing entry; fails with an error otherwise. *)
238definition update : ∀tag,A. identifier_map tag A → identifier tag → A → res (identifier_map tag A) ≝
239λtag,A,m,l,a.
240  match update A (match l with [ an_identifier l' ⇒ l' ]) a
241                 (match m with [ an_id_map m' ⇒ m' ]) with
242  [ None ⇒ Error ? ([MSG MissingId; CTX tag l]) (* missing identifier *)
243  | Some m' ⇒ OK ? (an_id_map tag A m')
244  ].
245
246definition foldi:
247  ∀A, B: Type[0].
248  ∀tag: String.
249  (identifier tag -> A -> B -> B) -> identifier_map tag A -> B -> B ≝
250λA,B,tag,f,m,b.
251  match m with
252  [ an_id_map m' ⇒ fold A B (λbv. f (an_identifier ? bv)) m' b ].
253
254(* A predicate that an identifier is in a map, and a failure-avoiding lookup
255   and update using it. *)
256
257definition present : ∀tag,A. identifier_map tag A → identifier tag → Prop ≝
258λtag,A,m,i. lookup … m i ≠ None ?.
259
260lemma member_present : ∀tag,A,m,id.
261  member tag A m id = true → present tag A m id.
262#tag #A * #m #id normalize cases (lookup_opt A ??) normalize
263[ #E destruct
264| #x #E % #E' destruct
265] qed.
266
267include "ASM/Util.ma".
268
269definition lookup_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A ≝
270λtag,A,m,id. match lookup ?? m id return λx. x ≠ None ? → ? with [ Some a ⇒ λ_. a | None ⇒ λH.⊥ ].
271cases H #H'  cases (H' (refl ??)) qed.
272
273lemma lookup_lookup_present : ∀tag,A,m,id,p.
274  lookup tag A m id = Some ? (lookup_present tag A m id p).
275#tag #A #m #id #p
276whd in p ⊢ (???(??%));
277cases (lookup tag A m id) in p ⊢ %;
278[ * #H @⊥ @H @refl
279| #a #H @refl
280] qed.
281
282definition update_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A → identifier_map tag A ≝
283λtag,A,m,l,p,a.
284  let l' ≝ match l with [ an_identifier l' ⇒ l' ] in
285  let m' ≝ match m with [ an_id_map m' ⇒ m' ] in
286  let u' ≝ update A l' a m' in
287  match u' return λx. update ???? = x → ? with
288  [ None ⇒ λE.⊥
289  | Some m' ⇒ λ_. an_id_map tag A m'
290  ] (refl ? u').
291cases l in p E; cases m; -l' -m' #m' #l'
292whd in ⊢ (% → ?);
293 whd in ⊢ (?(??(???%%)?) → ??(??%?%)? → ?);
294#NL #U cases NL #H @H @(update_fail … U)
295qed.
296
297lemma update_still_present : ∀tag,A,m,id,a,id'.
298  ∀H:present tag A m id.
299  ∀H':present tag A m id'.
300  present tag A (update_present tag A m id' H' a) id.
301#tag #A * #m * #id #a * #id' #H #H'
302whd whd in ⊢ (?(??(???(%??????)?)?)); normalize nodelta
303cases (identifier_eq ? (an_identifier tag id) (an_identifier tag id'))
304[ #E >E @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)); >(update_lookup_opt_same ????? U)
305  % #E' destruct
306| #NE @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)); whd in ⊢ (?(??(??%%)?));
307  <(update_lookup_opt_other ????? U id) [ @H | % #E cases NE >E #H @H @refl ]
308] qed.
309
310
311let rec fresh_for_map tag A (id:identifier tag) (m:identifier_map tag A) on id : Prop ≝
312  lookup … m id = None A.
313
314lemma fresh_for_empty_map : ∀tag,A,id.
315  fresh_for_map tag A id (empty_map tag A).
316#tag #A * #id //
317qed.
318
319definition fresh_map_for_univ ≝
320λtag,A. λm:identifier_map tag A. λu:universe tag.
321  ∀id. present tag A m id → fresh_for_univ tag id u.
322
323lemma fresh_fresh_for_map : ∀tag,A,m,id,u,u'.
324  fresh_map_for_univ tag A m u →
325  〈id,u'〉 = fresh tag u →
326  fresh_for_map tag A id m.
327#tag #A * #m * #id * #u * #u' whd in ⊢ (% → ???% → %);
328#FMU #E destruct lapply (FMU (an_identifier tag u)) whd in ⊢ ((% → %) → ?);
329generalize in ⊢ ((?(??%?) → ?) → ??%?); *
330[ // | #a #H @False_ind lapply (H ?) /2/ % #E destruct
331qed.
332
333lemma fresh_map_preserved : ∀tag,A,m,u,u',id.
334  fresh_map_for_univ tag A m u →
335  〈id,u'〉 = fresh tag u →
336  fresh_map_for_univ tag A m u'.
337#tag #A #m #u * #u' #id whd in ⊢ (% → ? → %); #H #E
338#id' #PR @(fresh_remains_fresh … E) @H //
339qed.
340
341lemma fresh_map_add : ∀tag,A,m,u,id,a.
342  fresh_map_for_univ tag A m u →
343  fresh_for_univ tag id u →
344  fresh_map_for_univ tag A (add tag A m id a) u.
345#tag #A * #m #u #id #a #Hm #Hi
346#id' #PR cases (identifier_eq tag id' id)
347[ #E >E @Hi
348| #NE @Hm whd in PR;
349  change with (add tag A (an_id_map tag A m) id a) in PR:(?(??(???%?)?));
350  >lookup_add_miss in PR; //
351] qed.
352
353lemma present_not_fresh : ∀tag,A,m,id,id'.
354  present tag A m id →
355  fresh_for_map tag A id' m →
356  id ≠ id'.
357#tag #A #m #id * #id' whd in ⊢ (% → % → ?);
358* #NE #E % #E' destruct @(NE E)
359qed.
360
361lemma fresh_for_map_add : ∀tag,A,id,m,id',a.
362  id ≠ id' →
363  fresh_for_map tag A id m →
364  fresh_for_map tag A id (add tag A m id' a).
365#tag #A * #id #m #id' #a #NE #F
366whd >lookup_add_miss //
367qed.
368
369
370(* Sets *)
371
372inductive identifier_set (tag:String) : Type[0] ≝
373  an_id_set : positive_map unit → identifier_set tag.
374
375definition empty_set : ∀tag:String. identifier_set tag ≝
376λtag. an_id_set tag (pm_leaf unit).
377
378let rec add_set (tag:String) (s:identifier_set tag) (i:identifier tag) on s : identifier_set tag ≝
379  an_id_set tag (insert unit (match i with [ an_identifier i' ⇒ i' ])
380                          it (match s with [ an_id_set s' ⇒ s' ])).
381
382definition singleton_set : ∀tag:String. identifier tag → identifier_set tag ≝
383λtag,i. add_set tag (empty_set tag) i.
384
385let rec mem_set (tag:String) (s:identifier_set tag) (i:identifier tag) on s : bool ≝
386  match lookup_opt ? (match i with [ an_identifier i' ⇒ i' ])
387                     (match s with [ an_id_set s' ⇒ s' ]) with
388  [ None ⇒ false
389  | Some _ ⇒ true
390  ].
391
392let rec union_set (tag:String) (s:identifier_set tag) (s':identifier_set tag) on s : identifier_set tag ≝
393  an_id_set tag (merge unit (match s with [ an_id_set s0 ⇒ s0 ])
394                            (match s' with [ an_id_set s1 ⇒ s1 ])).
395
396interpretation "identifier set union" 'union a b = (union_set ? a b).
397notation "∅" non associative with precedence 90 for @{ 'empty }.
398interpretation "empty identifier set" 'empty = (empty_set ?).
399interpretation "singleton identifier set" 'singl a = (add_set ? (empty_set ?) a).
400interpretation "identifier set membership" 'mem a b = (mem_set ? b a).
401
402lemma union_empty_l : ∀tag.∀s:identifier_set tag. ∅ ∪ s = s.
403#tag * //
404qed.
405
406lemma union_empty_r : ∀tag.∀s:identifier_set tag. s ∪ ∅ = s.
407#tag * * // qed.
408
Note: See TracBrowser for help on using the repository browser.