source: src/common/Identifiers.ma @ 1635

Last change on this file since 1635 was 1635, checked in by tranquil, 8 years ago
  • lists with binders and monads
  • Joint.ma and other temprarily forked, awaiting feedback from Claudio
  • translation of RTLabs → RTL refactored with new tools
File size: 13.3 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 by le_S/
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 by absurd/
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 by fresh_remains_fresh/ ]
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 by / | * #H @F % #E destruct /2 by / ]
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 by not_to_not/
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 by absurd/ ]
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 by All_append_l/
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 by /
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 by not_to_not/
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 by or_intror, sym_not_eq/
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 by absurd/ % #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.