Commit 0a1205dd authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Base stringmap on gmap.

parent 0e2a06fe
......@@ -5,7 +5,7 @@ range over Coq's data type of strings [string]. The implementation uses radix-2
search trees (uncompressed Patricia trees) as implemented in the file [pmap]
and guarantees logarithmic-time operations. *)
Require Export prelude.fin_maps prelude.pretty.
Require Import Ascii String prelude.list prelude.pmap prelude.mapset.
Require Import Ascii String prelude.gmap.
(** * Encoding and decoding *)
(** In order to reuse or existing implementation of radix-2 search trees over
......@@ -47,120 +47,16 @@ Definition string_of_pos (p : positive) : string :=
string_of_digits (digits_of_pos p).
Lemma string_of_to_pos s : string_of_pos (string_to_pos s) = s.
unfold string_of_pos.
by induction s as [|[[] [] [] [] [] [] [] []]]; simpl; f_equal.
Instance: Injective (=) (=) string_to_pos.
intros s1 s2 Hs. by rewrite <-(string_of_to_pos s1), Hs, string_of_to_pos.
(** * The data structure *)
(** We pack a [Pmap] together with a proof that ensures that all keys correspond
to actual strings. *)
Definition stringmap_wf {A} : Pmap A Prop :=
map_Forall (λ p _, string_to_pos (string_of_pos p) = p).
Record stringmap A := StringMap {
stringmap_car : Pmap A;
stringmap_prf : bool_decide (stringmap_wf stringmap_car)
Arguments StringMap {_} _ _.
Arguments stringmap_car {_} _.
Lemma stringmap_eq {A} (m1 m2 : stringmap A) :
m1 = m2 stringmap_car m1 = stringmap_car m2.
split; [by intros ->|intros]. destruct m1, m2; simplify_equality'.
f_equal; apply proof_irrel.
Instance stringmap_eq_eq {A} `{ x y : A, Decision (x = y)}
(m1 m2 : stringmap A) : Decision (m1 = m2).
refine (cast_if (decide (stringmap_car m1 = stringmap_car m2)));
abstract (by rewrite stringmap_eq).
(** * Operations on the data structure *)
Instance stringmap_lookup {A} : Lookup string A (stringmap A) := λ s m,
let (m,_) := m in m !! string_to_pos s.
Instance stringmap_empty {A} : Empty (stringmap A) := StringMap I.
Lemma stringmap_partial_alter_wf {A} (f : option A option A) m s :
stringmap_wf m stringmap_wf (partial_alter f (string_to_pos s) m).
intros Hm p x. destruct (decide (string_to_pos s = p)) as [<-|?].
* by rewrite string_of_to_pos.
* rewrite lookup_partial_alter_ne by done. by apply Hm.
Instance stringmap_partial_alter {A} :
PartialAlter string A (stringmap A) := λ f s m,
let (m,Hm) := m in StringMap (partial_alter f (string_to_pos s) m)
(bool_decide_pack _ (stringmap_partial_alter_wf f m s
(bool_decide_unpack _ Hm))).
Lemma stringmap_fmap_wf {A B} (f : A B) m :
stringmap_wf m stringmap_wf (f <$> m).
Proof. intros ? p x. rewrite lookup_fmap, fmap_Some; intros (?&?&?); eauto. Qed.
Instance stringmap_fmap : FMap stringmap := λ A B f m,
let (m,Hm) := m in StringMap (f <$> m)
(bool_decide_pack _ (stringmap_fmap_wf f m (bool_decide_unpack _ Hm))).
Lemma stringmap_omap_wf {A B} (f : A option B) m :
stringmap_wf m stringmap_wf (omap f m).
Proof. intros ? p x; rewrite lookup_omap, bind_Some; intros (?&?&?); eauto. Qed.
Instance stringmap_omap : OMap stringmap := λ A B f m,
let (m,Hm) := m in StringMap (omap f m)
(bool_decide_pack _ (stringmap_omap_wf f m (bool_decide_unpack _ Hm))).
Lemma stringmap_merge_wf {A B C} (f : option A option B option C) m1 m2 :
let f' o1 o2 := match o1, o2 with None, None => None | _, _ => f o1 o2 end in
stringmap_wf m1 stringmap_wf m2 stringmap_wf (merge f' m1 m2).
intros f' Hm1 Hm2 p z; rewrite lookup_merge by done; intros.
destruct (m1 !! _) eqn:?, (m2 !! _) eqn:?; naive_solver.
Instance stringmap_merge : Merge stringmap := λ A B C f m1 m2,
let (m1,Hm1) := m1 in let (m2,Hm2) := m2 in
let f' o1 o2 := match o1, o2 with None, None => None | _, _ => f o1 o2 end in
StringMap (merge f' m1 m2) (bool_decide_pack _ (stringmap_merge_wf f _ _
(bool_decide_unpack _ Hm1) (bool_decide_unpack _ Hm2))).
Instance stringmap_to_list {A} : FinMapToList string A (stringmap A) := λ m,
let (m,_) := m in prod_map string_of_pos id <$> map_to_list m.
(** * Instantiation of the finite map interface *)
Instance: FinMap string stringmap.
* unfold lookup; intros A [m1 Hm1] [m2 Hm2] H.
apply stringmap_eq, map_eq; intros i; simpl in *.
apply bool_decide_unpack in Hm1; apply bool_decide_unpack in Hm2.
apply option_eq; intros x; split; intros Hi.
+ generalize Hi. rewrite <-(Hm1 i x) by done; eauto using option_eq_1.
+ generalize Hi. rewrite <-(Hm2 i x) by done; eauto using option_eq_1.
* done.
* intros A f [m Hm] s; apply (lookup_partial_alter f m).
* intros A f [m Hm] s s' Hs; apply (lookup_partial_alter_ne f m).
by contradict Hs; apply (injective string_to_pos).
* intros A B f [m Hm] s; apply (lookup_fmap f m).
* intros A [m Hm]; unfold map_to_list; simpl.
apply bool_decide_unpack, map_Forall_to_list in Hm; revert Hm.
induction (NoDup_map_to_list m) as [|[p x] l Hpx];
inversion 1 as [|??? Hm']; simplify_equality'; constructor; eauto.
rewrite elem_of_list_fmap; intros ([p' x']&?&?); simplify_equality'.
cut (string_to_pos (string_of_pos p') = p'); [congruence|].
rewrite Forall_forall in Hm'. eapply (Hm' (_,_)); eauto.
* intros A [m Hm] s x; unfold map_to_list, lookup; simpl.
apply bool_decide_unpack in Hm; rewrite elem_of_list_fmap; split.
+ intros ([p' x']&?&Hp'); simplify_equality'.
apply elem_of_map_to_list in Hp'. by rewrite (Hm p' x').
+ intros. exists (string_to_pos s,x); simpl.
by rewrite elem_of_map_to_list, string_of_to_pos.
* intros A B f [m Hm] s; apply (lookup_omap f m).
* intros A B C f ? [m1 Hm1] [m2 Hm2] s; unfold merge, lookup; simpl.
set (f' o1 o2 := match o1, o2 with None, None => None | _, _ => f o1 o2 end).
rewrite lookup_merge by done. by destruct (m1 !! _), (m2 !! _).
unfold string_of_pos. by induction s as [|[[][][][][][][][]]]; f_equal'.
Program Instance string_countable : Countable string := {|
encode := string_to_pos; decode p := Some (string_of_pos p)
Solve Obligations with naive_solver eauto using string_of_to_pos with f_equal.
(** * Finite sets *)
(** We construct sets of [strings]s satisfying extensional equality. *)
Notation stringset := (mapset stringmap).
Instance stringmap_dom {A} : Dom (stringmap A) stringset := mapset_dom.
Instance: FinMapDom positive Pmap Pset := mapset_dom_spec.
(** * Maps and sets *)
Notation stringmap := (gmap string).
Notation stringset := (gset string).
(** * Generating fresh strings *)
Local Open Scope N_scope.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment