source: src/common/Identifiers.ma @ 1139

Last change on this file since 1139 was 1092, checked in by campbell, 9 years ago

Some minor definitions for identifiers and lists.

File size: 6.4 KB
RevLine 
[736]1include "basics/types.ma".
2include "ASM/String.ma".
3include "ASM/Arithmetic.ma".
4include "common/Errors.ma".
5
[738]6(* identifiers and their generators are tagged to differentiate them, and to
[736]7   provide extra type checking. *)
8
[797]9(* in common/PreIdentifiers.ma, via Errors.ma.
[738]10inductive identifier (tag:String) : Type[0] ≝
11  an_identifier : Word → identifier tag.
[797]12*)
13
[738]14record universe (tag:String) : Type[0] ≝
[1055]15{
16  next_identifier : Word;
17  counter_overflow: bool
18}.
[736]19
[738]20definition new_universe : ∀tag:String. universe tag ≝
[1055]21  λtag. mk_universe tag (zero ?) false.
[797]22
[1056]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) ≝
[1055]27  λtag.
28  λuniv: universe tag.
29  let 〈gen, carries〉 ≝ add_with_carries ? (next_identifier ? univ) (zero ?) true in
30    if get_index_v … carries 0 ? then
31      〈an_identifier tag (next_identifier ? univ), mk_universe tag gen true〉
32    else
33      〈an_identifier tag (next_identifier ? univ), mk_universe tag gen false〉.
34  //
35qed.
[797]36
[1056]37axiom TooManyIdentifiers : String.
38
39definition check_universe_ok : ∀tag:String. universe tag → res unit ≝
40  λtag, univ.
41  if counter_overflow ? univ
42  then Error ? (msg TooManyIdentifiers)
43  else OK ? it.
44
[1070]45definition eq_identifier : ∀t. identifier t → identifier t → bool ≝
46  λt,l,r.
[757]47  match l with
48  [ an_identifier l' ⇒
49    match r with
50    [ an_identifier r' ⇒
51      eq_bv ? l' r'
52    ]
53  ].
[1070]54
55lemma eq_identifier_elim : ∀P:bool → Type[0]. ∀t,x,y.
56  (x = y → P true) → (x ≠ y → P false) →
57  P (eq_identifier t x y).
58#P #t * #x * #y #T #F
59change with (P (eq_bv ???))
60@eq_bv_elim [ /2/ | * #H @F % #E destruct /2/ ]
61qed.
[757]62   
63definition word_of_identifier ≝
64  λt.
65  λl: identifier t.
66  match l with   
67  [ an_identifier l' ⇒ l'
68  ].
69
[738]70definition identifier_eq : ∀tag:String. ∀x,y:identifier tag. (x=y) + (x≠y).
[736]71#tag * #x * #y lapply (refl ? (eq_bv ? x y)) cases (eq_bv ? x y) in ⊢ (???% → %)
72#E [ % | %2 ]
73lapply E @eq_bv_elim
74[ #H #_ >H @refl | 2,3: #_ #H destruct | #H #_ % #H' destruct /2/ ]
75qed.
76
[738]77definition identifier_of_nat : ∀tag:String. nat → identifier tag ≝
[736]78  λtag,n. an_identifier tag (bitvector_of_nat ? n).
79
80
81(* Maps from identifiers to arbitrary types. *)
82
83include "ASM/BitVectorTrie.ma".
84
[753]85inductive identifier_map (tag:String) (A:Type[0]) : Type[0] ≝
86  an_id_map : BitVectorTrie A 16 → identifier_map tag A.
87 
[738]88definition empty_map : ∀tag:String. ∀A. identifier_map tag A ≝
[736]89  λtag,A. an_id_map tag A (Stub A 16).
90
[738]91definition lookup : ∀tag,A. identifier_map tag A → identifier tag → option A ≝
[736]92  λtag,A,m,l. lookup_opt A 16 (match l with [ an_identifier l' ⇒ l' ])
93                              (match m with [ an_id_map m' ⇒ m' ]).
94
[761]95(* Always adds the identifier to the map. *)
[738]96definition add : ∀tag,A. identifier_map tag A → identifier tag → A → identifier_map tag A ≝
[736]97λtag,A,m,l,a. an_id_map tag A (insert A 16 (match l with [ an_identifier l' ⇒ l' ]) a
98                                           (match m with [ an_id_map m' ⇒ m' ])).
99
[1070]100lemma lookup_add_hit : ∀tag,A,m,i,a.
101  lookup tag A (add tag A m i a) i = Some ? a.
102#tag #A * #m * #i #a
103@lookup_opt_insert_hit
104qed.
105
106lemma lookup_add_miss : ∀tag,A,m,i,j,a.
107  (notb (eq_identifier tag i j)) →
108  lookup tag A (add tag A m j a) i = lookup tag A m i.
109#tag #A * #m * #i * #j #a
110change with (notb (eq_bv ???) → ?)
111@lookup_opt_insert_miss
112qed.
113
114lemma lookup_add_oblivious : ∀tag,A,m,i,j,a.
[1072]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
[1070]118lapply (lookup_add_miss … m i j a)
119@eq_identifier_elim
[1072]120[ #E #_ >E >lookup_add_hit % #N destruct
121| #_ #H' >H' //
[1070]122] qed.
123
[1058]124(* Extract every identifier, value pair from the map. *)
125definition elements : ∀tag,A. identifier_map tag A → list (identifier tag × A) ≝
126λtag,A,m.
127  fold ??? (λl,a,el. 〈an_identifier tag l, a〉::el)
128           (match m with [ an_id_map m' ⇒ m' ]) [ ].
129
[797]130axiom MissingId : String.
131
[761]132(* Only updates an existing entry; fails with an error otherwise. *)
133definition update : ∀tag,A. identifier_map tag A → identifier tag → A → res (identifier_map tag A) ≝
134λtag,A,m,l,a.
135  match update A 16 (match l with [ an_identifier l' ⇒ l' ]) a
136                    (match m with [ an_id_map m' ⇒ m' ]) with
[797]137  [ None ⇒ Error ? ([MSG MissingId; CTX tag l]) (* missing identifier *)
[761]138  | Some m' ⇒ OK ? (an_id_map tag A m')
139  ].
[736]140
[1092]141definition foldi:
[1068]142  ∀A, B: Type[0].
143  ∀tag: String.
[1092]144  (identifier tag -> A -> B -> B) -> identifier_map tag A -> B -> B ≝
145λA,B,tag,f,m,b.
146  match m with
147  [ an_id_map m' ⇒ fold A B ? (λbv. f (an_identifier ? bv)) m' b ].
[1068]148
[779]149(* Sets *)
150
151inductive identifier_set (tag:String) : Type[0] ≝
152  an_id_set : BitVectorTrie unit 16 → identifier_set tag.
153
154definition empty_set : ∀tag:String. identifier_set tag ≝
155λtag. an_id_set tag (Stub unit 16).
156
[1092]157let rec add_set (tag:String) (s:identifier_set tag) (i:identifier tag) on s : identifier_set tag ≝
158  an_id_set tag (insert unit 16 (match i with [ an_identifier i' ⇒ i' ])
159                             it (match s with [ an_id_set s' ⇒ s' ])).
[779]160
161definition singleton_set : ∀tag:String. identifier tag → identifier_set tag ≝
162λtag,i. add_set tag (empty_set tag) i.
163
[1092]164let rec mem_set (tag:String) (s:identifier_set tag) (i:identifier tag) on s : bool ≝
165  match lookup_opt ? 16 (match i with [ an_identifier i' ⇒ i' ])
166                        (match s with [ an_id_set s' ⇒ s' ]) with
167  [ None ⇒ false
168  | Some _ ⇒ true
169  ].
[779]170
[1092]171let rec union_set (tag:String) (s:identifier_set tag) (s':identifier_set tag) on s : identifier_set tag ≝
172  an_id_set tag (merge unit 16 (match s with [ an_id_set s0 ⇒ s0 ])
173                               (match s' with [ an_id_set s1 ⇒ s1 ])).
[816]174
175interpretation "identifier set union" 'union a b = (union_set ? a b).
176notation "∅" non associative with precedence 90 for @{ 'empty }.
177interpretation "empty identifier set" 'empty = (empty_set ?).
178interpretation "singleton identifier set" 'singl a = (add_set ? (empty_set ?) a).
[1092]179interpretation "identifier set membership" 'mem a b = (mem_set ? b a).
180
181lemma union_empty_l : ∀tag.∀s:identifier_set tag. ∅ ∪ s = s.
182#tag * //
183qed.
184
185lemma union_empty_r : ∀tag.∀s:identifier_set tag. s ∪ ∅ = s.
186#tag * #s cases (BitVectorTrie_Sn … s)
187[ * #x * #y #E >E //
188| #E >E //
189] qed.
Note: See TracBrowser for help on using the repository browser.