source: src/common/Identifiers.ma @ 1586

Last change on this file since 1586 was 1562, checked in by mulligan, 8 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.