source: Deliverables/D3.3/id-lookup-branch/common/Identifiers.ma @ 1134

Last change on this file since 1134 was 1134, checked in by campbell, 8 years ago

Extra results for non-failing map updates.

File size: 8.4 KB
Line 
1include "basics/types.ma".
2include "ASM/String.ma".
3include "ASM/Arithmetic.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 : Word → identifier tag.
13*)
14
15record universe (tag:String) : Type[0] ≝
16{
17  next_identifier : Word;
18  counter_overflow: bool
19}.
20
21definition new_universe : ∀tag:String. universe tag ≝
22  λtag. mk_universe tag (zero ?) false.
23
24(* Fresh identifier generation uses delayed overflow checking.  To make sure
25   that the identifiers really were fresh, use the check_universe_ok function
26   below afterwards. *)
27definition fresh : ∀tag:String. universe tag → identifier tag × (universe tag) ≝
28  λtag.
29  λuniv: universe tag.
30  let 〈gen, carries〉 ≝ add_with_carries ? (next_identifier ? univ) (zero ?) true in
31    if get_index_v … carries 0 ? then
32      〈an_identifier tag (next_identifier ? univ), mk_universe tag gen true〉
33    else
34      〈an_identifier tag (next_identifier ? univ), mk_universe tag gen false〉.
35  //
36qed.
37
38axiom TooManyIdentifiers : String.
39
40definition check_universe_ok : ∀tag:String. universe tag → res unit ≝
41  λtag, univ.
42  if counter_overflow ? univ
43  then Error ? (msg TooManyIdentifiers)
44  else OK ? it.
45
46definition eq_identifier : ∀t. identifier t → identifier t → bool ≝
47  λt,l,r.
48  match l with
49  [ an_identifier l' ⇒
50    match r with
51    [ an_identifier r' ⇒
52      eq_bv ? l' r'
53    ]
54  ].
55
56lemma eq_identifier_elim : ∀P:bool → Type[0]. ∀t,x,y.
57  (x = y → P true) → (x ≠ y → P false) →
58  P (eq_identifier t x y).
59#P #t * #x * #y #T #F
60change with (P (eq_bv ???))
61@eq_bv_elim [ /2/ | * #H @F % #E destruct /2/ ]
62qed.
63   
64definition word_of_identifier ≝
65  λt.
66  λl: identifier t.
67  match l with   
68  [ an_identifier l' ⇒ l'
69  ].
70
71definition identifier_eq : ∀tag:String. ∀x,y:identifier tag. (x=y) + (x≠y).
72#tag * #x * #y lapply (refl ? (eq_bv ? x y)) cases (eq_bv ? x y) in ⊢ (???% → %)
73#E [ % | %2 ]
74lapply E @eq_bv_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 (bitvector_of_nat ? n).
80
81
82(* Maps from identifiers to arbitrary types. *)
83
84include "ASM/BitVectorTrie.ma".
85
86inductive identifier_map (tag:String) (A:Type[0]) : Type[0] ≝
87  an_id_map : BitVectorTrie A 16 → identifier_map tag A.
88 
89definition empty_map : ∀tag:String. ∀A. identifier_map tag A ≝
90  λtag,A. an_id_map tag A (Stub A 16).
91
92definition lookup : ∀tag,A. identifier_map tag A → identifier tag → option A ≝
93  λtag,A,m,l. lookup_opt A 16 (match l with [ an_identifier l' ⇒ l' ])
94                              (match m with [ an_id_map m' ⇒ m' ]).
95
96(* Always adds the identifier to the map. *)
97definition add : ∀tag,A. identifier_map tag A → identifier tag → A → identifier_map tag A ≝
98λtag,A,m,l,a. an_id_map tag A (insert A 16 (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  (notb (eq_identifier tag 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
111change with (notb (eq_bv ???) → ?)
112@lookup_opt_insert_miss
113qed.
114
115lemma lookup_add_oblivious : ∀tag,A,m,i,j,a.
116  (lookup tag A m i ≠ None ?) →
117  lookup tag A (add tag A m j a) i ≠ None ?.
118#tag #A #m #i #j #a #H
119lapply (lookup_add_miss … m i j a)
120@eq_identifier_elim
121[ #E #_ >E >lookup_add_hit % #N destruct
122| #_ #H' >H' //
123] qed.
124
125lemma lookup_add_cases : ∀tag,A,m,i,j,a,v.
126  lookup tag A (add tag A m i a) j = Some ? v →
127  (i=j ∧ v = a) ∨ lookup tag A m j = Some ? v.
128#tag #A #m #i #j #a #v
129cases (identifier_eq ? i j)
130[ #E >E >lookup_add_hit #H %1 destruct % //
131| #NE >lookup_add_miss /2/ @eq_identifier_elim /2/
132] qed.
133
134(* Extract every identifier, value pair from the map. *)
135definition elements : ∀tag,A. identifier_map tag A → list (identifier tag × A) ≝
136λtag,A,m.
137  fold ??? (λl,a,el. 〈an_identifier tag l, a〉::el)
138           (match m with [ an_id_map m' ⇒ m' ]) [ ].
139
140axiom MissingId : String.
141
142(* Only updates an existing entry; fails with an error otherwise. *)
143definition update : ∀tag,A. identifier_map tag A → identifier tag → A → res (identifier_map tag A) ≝
144λtag,A,m,l,a.
145  match update A 16 (match l with [ an_identifier l' ⇒ l' ]) a
146                    (match m with [ an_id_map m' ⇒ m' ]) with
147  [ None ⇒ Error ? ([MSG MissingId; CTX tag l]) (* missing identifier *)
148  | Some m' ⇒ OK ? (an_id_map tag A m')
149  ].
150
151definition foldi:
152  ∀A, B: Type[0].
153  ∀tag: String.
154  (identifier tag -> A -> B -> B) -> identifier_map tag A -> B -> B ≝
155λA,B,tag,f,m,b.
156  match m with
157  [ an_id_map m' ⇒ fold A B ? (λbv. f (an_identifier ? bv)) m' b ].
158
159(* A predicate that an identifier is in a map, and a failure-avoiding lookup
160   and update using it. *)
161
162definition present : ∀tag,A. identifier_map tag A → identifier tag → Prop ≝
163λtag,A,m,i. lookup … m i ≠ None ?.
164
165definition lookup_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A ≝
166λtag,A,m,id. match lookup ?? m id return λx. x ≠ None ? → ? with [ Some a ⇒ λ_. a | None ⇒ λH.⊥ ].
167cases H #H'  cases (H' (refl ??)) qed.
168
169definition update_present : ∀tag,A. ∀m:identifier_map tag A. ∀id. present ?? m id → A → identifier_map tag A ≝
170λtag,A,m,l,p,a.
171  let l' ≝ match l with [ an_identifier l' ⇒ l' ] in
172  let m' ≝ match m with [ an_id_map m' ⇒ m' ] in
173  let u' ≝ update A 16 l' a m' in
174  match u' return λx. update ????? = x → ? with
175  [ None ⇒ λE.⊥
176  | Some m' ⇒ λ_. an_id_map tag A m'
177  ] (refl ? u').
178whd in p; whd in p:(?(??%?)) E:(??(???%?%)?);
179cases l in p E; cases m; -l' -m' #m' #l' whd in ⊢ (?(??(???%%)?) → ??(???%?%)? → ?)
180#NL #U cases NL #H @H @(update_fail … U)
181qed.
182
183lemma update_still_present : ∀tag,A,m,id,a,id'.
184  ∀H:present tag A m id.
185  ∀H':present tag A m id'.
186  present tag A (update_present tag A m id' H' a) id.
187#tag #A * #m * #id #a * #id' #H #H'
188whd whd in ⊢ (?(??(???(%??????)?)?)) normalize nodelta
189cases (identifier_eq ? (an_identifier tag id) (an_identifier tag id'))
190[ #E >E @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) >(update_lookup_opt_same ?????? U)
191  % #E' destruct
192| #NE @refute_none_by_refl #m' #U whd in ⊢ (?(??%?)) whd in ⊢ (?(??(???%%)?))
193  <(update_lookup_opt_other ?????? U id) [ @H | % #E cases NE >E #H @H @refl ]
194] qed.
195
196(* Sets *)
197
198inductive identifier_set (tag:String) : Type[0] ≝
199  an_id_set : BitVectorTrie unit 16 → identifier_set tag.
200
201definition empty_set : ∀tag:String. identifier_set tag ≝
202λtag. an_id_set tag (Stub unit 16).
203
204let rec add_set (tag:String) (s:identifier_set tag) (i:identifier tag) on s : identifier_set tag ≝
205  an_id_set tag (insert unit 16 (match i with [ an_identifier i' ⇒ i' ])
206                             it (match s with [ an_id_set s' ⇒ s' ])).
207
208definition singleton_set : ∀tag:String. identifier tag → identifier_set tag ≝
209λtag,i. add_set tag (empty_set tag) i.
210
211let rec mem_set (tag:String) (s:identifier_set tag) (i:identifier tag) on s : bool ≝
212  match lookup_opt ? 16 (match i with [ an_identifier i' ⇒ i' ])
213                        (match s with [ an_id_set s' ⇒ s' ]) with
214  [ None ⇒ false
215  | Some _ ⇒ true
216  ].
217
218let rec union_set (tag:String) (s:identifier_set tag) (s':identifier_set tag) on s : identifier_set tag ≝
219  an_id_set tag (merge unit 16 (match s with [ an_id_set s0 ⇒ s0 ])
220                               (match s' with [ an_id_set s1 ⇒ s1 ])).
221
222interpretation "identifier set union" 'union a b = (union_set ? a b).
223notation "∅" non associative with precedence 90 for @{ 'empty }.
224interpretation "empty identifier set" 'empty = (empty_set ?).
225interpretation "singleton identifier set" 'singl a = (add_set ? (empty_set ?) a).
226interpretation "identifier set membership" 'mem a b = (mem_set ? b a).
227
228lemma union_empty_l : ∀tag.∀s:identifier_set tag. ∅ ∪ s = s.
229#tag * //
230qed.
231
232lemma union_empty_r : ∀tag.∀s:identifier_set tag. s ∪ ∅ = s.
233#tag * #s cases (BitVectorTrie_Sn … s)
234[ * #x * #y #E >E //
235| #E >E //
236] qed.
Note: See TracBrowser for help on using the repository browser.