source: src/common/Identifiers.ma @ 1601

Last change on this file since 1601 was 1601, checked in by sacerdot, 8 years ago

Files ported to new version of the standard library.

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