stringmap.v 2.69 KB
Newer Older
1
(* Copyright (c) 2012-2019, Coq-std++ developers. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
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. *)
7 8
From stdpp Require Export fin_maps pretty.
From stdpp Require Import gmap.
9
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
10 11 12 13 14

Notation stringmap := (gmap string).
Notation stringset := (gset string).

(** * Generating fresh strings *)
Ralf Jung's avatar
Ralf Jung committed
15
Section stringmap.
Robbert Krebbers's avatar
Robbert Krebbers committed
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|].
29
  by rewrite lookup_delete_ne by (intros ?; simplify_eq/=; lia).
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
38
Definition fresh_string {A} (s : string) (m : stringmap A) : string :=
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
44
Lemma fresh_string_fresh {A} (m : stringmap A) s : m !! fresh_string s m = None.
Robbert Krebbers's avatar
Robbert Krebbers committed
45 46 47
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.
48
  fix FIX 3; intros m n [?]; simpl; unfold fresh_string_go at 1; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
49 50
  destruct (Some_dec (m !! _)) as [[??]|?]; auto.
Qed.
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)
63
  end%nat.
Ralf Jung's avatar
Ralf Jung committed
64
End stringmap.