stringmap.v 2.69 KB
 Robbert Krebbers committed Mar 15, 2017 1 ``````(* Copyright (c) 2012-2017, Coq-std++ developers. *) `````` Robbert Krebbers committed Dec 22, 2015 2 3 4 5 6 ``````(* This file is distributed under the terms of the BSD license. *) (** This files implements an efficient implementation of finite maps whose keys 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. *) `````` Robbert Krebbers committed Feb 13, 2016 7 8 ``````From stdpp Require Export fin_maps pretty. From stdpp Require Import gmap. `````` Ralf Jung committed Jan 31, 2017 9 ``````Set Default Proof Using "Type". `````` Robbert Krebbers committed Dec 22, 2015 10 11 12 13 14 `````` Notation stringmap := (gmap string). Notation stringset := (gset string). (** * Generating fresh strings *) `````` Ralf Jung committed Nov 17, 2016 15 ``````Section stringmap. `````` Robbert Krebbers committed Dec 22, 2015 16 17 18 19 20 21 22 23 24 25 26 27 28 ``````Local Open Scope N_scope. Let R {A} (s : string) (m : stringmap A) (n1 n2 : N) := n2 < n1 ∧ is_Some (m !! (s +:+ pretty (n1 - 1))). Lemma fresh_string_step {A} s (m : stringmap A) n x : m !! (s +:+ pretty n) = Some x → R s m (1 + n) n. Proof. split; [lia|]. replace (1 + n - 1) with n by lia; eauto. Qed. Lemma fresh_string_R_wf {A} s (m : stringmap A) : wf (R s m). Proof. induction (map_wf m) as [m _ IH]. intros n1; constructor; intros n2 [Hn Hs]. specialize (IH _ (delete_subset m (s +:+ pretty (n2 - 1)) Hs) n2). cut (n2 - 1 < n2); [|lia]. clear n1 Hn Hs; revert IH; generalize (n2 - 1). intros n1. induction 1 as [n2 _ IH]; constructor; intros n3 [??]. apply IH; [|lia]; split; [lia|]. `````` Robbert Krebbers committed Feb 17, 2016 29 `````` by rewrite lookup_delete_ne by (intros ?; simplify_eq/=; lia). `````` Robbert Krebbers committed Dec 22, 2015 30 31 32 33 34 35 36 37 ``````Qed. Definition fresh_string_go {A} (s : string) (m : stringmap A) (n : N) (go : ∀ n', R s m n' n → string) : string := let s' := s +:+ pretty n in match Some_dec (m !! s') with | inleft (_↾Hs') => go (1 + n)%N (fresh_string_step s m n _ Hs') | inright _ => s' end. `````` Robbert Krebbers committed Jan 12, 2016 38 ``````Definition fresh_string {A} (s : string) (m : stringmap A) : string := `````` Robbert Krebbers committed Dec 22, 2015 39 40 41 42 43 `````` match m !! s with | None => s | Some _ => Fix_F _ (fresh_string_go s m) (wf_guard 32 (fresh_string_R_wf s m) 0) end. `````` Robbert Krebbers committed Jan 12, 2016 44 ``````Lemma fresh_string_fresh {A} (m : stringmap A) s : m !! fresh_string s m = None. `````` Robbert Krebbers committed Dec 22, 2015 45 46 47 48 49 50 ``````Proof. unfold fresh_string. destruct (m !! s) as [a|] eqn:Hs; [clear a Hs|done]. generalize 0 (wf_guard 32 (fresh_string_R_wf s m) 0); revert m. fix 3; intros m n [?]; simpl; unfold fresh_string_go at 1; simpl. destruct (Some_dec (m !! _)) as [[??]|?]; auto. Qed. `````` Robbert Krebbers committed Jan 12, 2016 51 52 53 54 55 56 57 58 59 60 61 62 ``````Definition fresh_string_of_set (s : string) (X : stringset) : string := fresh_string s (mapset.mapset_car X). Lemma fresh_string_of_set_fresh (X : stringset) s : fresh_string_of_set s X ∉ X. Proof. apply eq_None_ne_Some, fresh_string_fresh. Qed. Fixpoint fresh_strings_of_set (s : string) (n : nat) (X : stringset) : list string := match n with | 0 => [] | S n => let x := fresh_string_of_set s X in x :: fresh_strings_of_set s n ({[ x ]} ∪ X) `````` Robbert Krebbers committed Feb 13, 2016 63 `````` end%nat. `````` Ralf Jung committed Nov 17, 2016 64 ``End stringmap.``