source: src/common/Identifiers.ma @ 1515

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

Add type of maps on positive binary numbers, and use them for identifers.

Also:

  • fix interpretation for - on positives
  • move eq_nat_dec to a more appropriate place
  • split out costs from other identifiers in ASM
  • use identifier abstractions in back-end
File size: 8.3 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
61lemma eq_identifier_false : ∀tag,x,y. x≠y → eq_identifier tag x y = false.
62#tag * #x * #y #NE normalize @not_eq_to_eqb_false /2/
63qed.
64
65definition identifier_eq : ∀tag:String. ∀x,y:identifier tag. (x=y) + (x≠y).
66#tag * #x * #y lapply (refl ? (eqb x y)) cases (eqb x y) in ⊢ (???% → %)
67#E [ % | %2 ]
68lapply E @eqb_elim
69[ #H #_ >H @refl | 2,3: #_ #H destruct | #H #_ % #H' destruct /2/ ]
70qed.
71
72definition identifier_of_nat : ∀tag:String. nat → identifier tag ≝
73  λtag,n. an_identifier tag (succ_pos_of_nat  n).
74
75
76(* Maps from identifiers to arbitrary types. *)
77
78include "common/PositiveMap.ma".
79
80inductive identifier_map (tag:String) (A:Type[0]) : Type[0] ≝
81  an_id_map : positive_map A → identifier_map tag A.
82 
83definition empty_map : ∀tag:String. ∀A. identifier_map tag A ≝
84  λtag,A. an_id_map tag A (pm_leaf A).
85
86let rec lookup tag A (m:identifier_map tag A) (l:identifier tag) on m : option A ≝
87  lookup_opt A (match l with [ an_identifier l' ⇒ l' ])
88               (match m with [ an_id_map m' ⇒ m' ]).
89
90definition lookup_def ≝
91λtag,A,m,l,d. match lookup tag A m l with [ None ⇒ d | Some x ⇒ x].
92
93let rec member tag A (m:identifier_map tag A) (l:identifier tag) on m : bool ≝
94  match lookup tag A m l with [ None ⇒ false | _ ⇒ true ].
95
96(* Always adds the identifier to the map. *)
97let rec add tag A (m:identifier_map tag A) (l:identifier tag) (a:A) on m : identifier_map tag A ≝
98  an_id_map tag A (insert A (match l with [ an_identifier l' ⇒ l' ]) a
99                            (match m with [ an_id_map m' ⇒ m' ])).
100
101lemma lookup_add_hit : ∀tag,A,m,i,a.
102  lookup tag A (add tag A m i a) i = Some ? a.
103#tag #A * #m * #i #a
104@lookup_opt_insert_hit
105qed.
106
107lemma lookup_add_miss : ∀tag,A,m,i,j,a.
108  i ≠ j →
109  lookup tag A (add tag A m j a) i = lookup tag A m i.
110#tag #A * #m * #i * #j #a #H
111@lookup_opt_insert_miss /2/
112qed.
113
114lemma lookup_add_oblivious : ∀tag,A,m,i,j,a.
115  (lookup tag A m i ≠ None ?) →
116  lookup tag A (add tag A m j a) i ≠ None ?.
117#tag #A #m #i #j #a #H
118cases (identifier_eq ? i j)
119[ #E >E >lookup_add_hit % #N destruct
120| #NE >lookup_add_miss //
121] qed.
122
123lemma lookup_add_cases : ∀tag,A,m,i,j,a,v.
124  lookup tag A (add tag A m i a) j = Some ? v →
125  (i=j ∧ v = a) ∨ lookup tag A m j = Some ? v.
126#tag #A #m #i #j #a #v
127cases (identifier_eq ? i j)
128[ #E >E >lookup_add_hit #H %1 destruct % //
129| #NE >lookup_add_miss /2/
130] qed.
131
132(* Extract every identifier, value pair from the map. *)
133definition elements : ∀tag,A. identifier_map tag A → list (identifier tag × A) ≝
134λtag,A,m.
135  fold ?? (λl,a,el. 〈an_identifier tag l, a〉::el)
136          (match m with [ an_id_map m' ⇒ m' ]) [ ].
137
138axiom MissingId : String.
139
140(* Only updates an existing entry; fails with an error otherwise. *)
141definition update : ∀tag,A. identifier_map tag A → identifier tag → A → res (identifier_map tag A) ≝
142λtag,A,m,l,a.
143  match update A (match l with [ an_identifier l' ⇒ l' ]) a
144                 (match m with [ an_id_map m' ⇒ m' ]) with
145  [ None ⇒ Error ? ([MSG MissingId; CTX tag l]) (* missing identifier *)
146  | Some m' ⇒ OK ? (an_id_map tag A m')
147  ].
148
149definition foldi:
150  ∀A, B: Type[0].
151  ∀tag: String.
152  (identifier tag -> A -> B -> B) -> identifier_map tag A -> B -> B ≝
153λA,B,tag,f,m,b.
154  match m with
155  [ an_id_map m' ⇒ fold A B (λbv. f (an_identifier ? bv)) m' b ].
156
157(* A predicate that an identifier is in a map, and a failure-avoiding lookup
158   and update using it. *)
159
160definition present : ∀tag,A. identifier_map tag A → identifier tag → Prop ≝
161λtag,A,m,i. lookup … m i ≠ None ?.
162
163lemma member_present : ∀tag,A,m,id.
164  member tag A m id = true → present tag A m id.
165#tag #A * #m #id normalize cases (lookup_opt A ??) normalize
166[ #E destruct
167| #x #E % #E' destruct
168] qed.
169
170include "ASM/Util.ma".
171
172definition lookup_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A ≝
173λtag,A,m,id. match lookup ?? m id return λx. x ≠ None ? → ? with [ Some a ⇒ λ_. a | None ⇒ λH.⊥ ].
174cases H #H'  cases (H' (refl ??)) qed.
175
176definition update_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A → identifier_map tag A ≝
177λtag,A,m,l,p,a.
178  let l' ≝ match l with [ an_identifier l' ⇒ l' ] in
179  let m' ≝ match m with [ an_id_map m' ⇒ m' ] in
180  let u' ≝ update A l' a m' in
181  match u' return λx. update ???? = x → ? with
182  [ None ⇒ λE.⊥
183  | Some m' ⇒ λ_. an_id_map tag A m'
184  ] (refl ? u').
185cases l in p E; cases m; -l' -m' #m' #l'
186whd in ⊢ (% → ?)
187 whd in ⊢ (?(??(???%%)?) → ??(??%?%)? → ?)
188#NL #U cases NL #H @H @(update_fail … U)
189qed.
190
191lemma update_still_present : ∀tag,A,m,id,a,id'.
192  ∀H:present tag A m id.
193  ∀H':present tag A m id'.
194  present tag A (update_present tag A m id' H' a) id.
195#tag #A * #m * #id #a * #id' #H #H'
196whd whd in ⊢ (?(??(???(%??????)?)?)) normalize nodelta
197cases (identifier_eq ? (an_identifier tag id) (an_identifier tag id'))
198[ #E >E @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) >(update_lookup_opt_same ????? U)
199  % #E' destruct
200| #NE @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) whd in ⊢ (?(??(??%%)?))
201  <(update_lookup_opt_other ????? U id) [ @H | % #E cases NE >E #H @H @refl ]
202] qed.
203
204(* Sets *)
205
206inductive identifier_set (tag:String) : Type[0] ≝
207  an_id_set : positive_map unit → identifier_set tag.
208
209definition empty_set : ∀tag:String. identifier_set tag ≝
210λtag. an_id_set tag (pm_leaf unit).
211
212let rec add_set (tag:String) (s:identifier_set tag) (i:identifier tag) on s : identifier_set tag ≝
213  an_id_set tag (insert unit (match i with [ an_identifier i' ⇒ i' ])
214                          it (match s with [ an_id_set s' ⇒ s' ])).
215
216definition singleton_set : ∀tag:String. identifier tag → identifier_set tag ≝
217λtag,i. add_set tag (empty_set tag) i.
218
219let rec mem_set (tag:String) (s:identifier_set tag) (i:identifier tag) on s : bool ≝
220  match lookup_opt ? (match i with [ an_identifier i' ⇒ i' ])
221                     (match s with [ an_id_set s' ⇒ s' ]) with
222  [ None ⇒ false
223  | Some _ ⇒ true
224  ].
225
226let rec union_set (tag:String) (s:identifier_set tag) (s':identifier_set tag) on s : identifier_set tag ≝
227  an_id_set tag (merge unit (match s with [ an_id_set s0 ⇒ s0 ])
228                            (match s' with [ an_id_set s1 ⇒ s1 ])).
229
230interpretation "identifier set union" 'union a b = (union_set ? a b).
231notation "∅" non associative with precedence 90 for @{ 'empty }.
232interpretation "empty identifier set" 'empty = (empty_set ?).
233interpretation "singleton identifier set" 'singl a = (add_set ? (empty_set ?) a).
234interpretation "identifier set membership" 'mem a b = (mem_set ? b a).
235
236lemma union_empty_l : ∀tag.∀s:identifier_set tag. ∅ ∪ s = s.
237#tag * //
238qed.
239
240lemma union_empty_r : ∀tag.∀s:identifier_set tag. s ∪ ∅ = s.
241#tag * * // qed.
Note: See TracBrowser for help on using the repository browser.