From e5cf4babbd62c1a8968d788cc3c511a93e6ff26e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 20 May 2015 21:26:36 +0200
Subject: [PATCH] Less inefficient fresh function for pset/nset.

It would still be far more efficient to have a counter for the next memory
index in the executable semantics/frontend.
---
 theories/fresh_numbers.v | 34 ----------------------
 theories/nmap.v          | 17 +++++++++++
 theories/pmap.v          | 63 ++++++++++++++++++++++++++++++++++++++++
 theories/prelude.v       |  1 -
 4 files changed, 80 insertions(+), 35 deletions(-)
 delete mode 100644 theories/fresh_numbers.v

diff --git a/theories/fresh_numbers.v b/theories/fresh_numbers.v
deleted file mode 100644
index 27f34b25..00000000
--- a/theories/fresh_numbers.v
+++ /dev/null
@@ -1,34 +0,0 @@
-(* Copyright (c) 2012-2015, Robbert Krebbers. *)
-(* This file is distributed under the terms of the BSD license. *)
-(** Given a finite set of binary naturals [N], we generate a fresh element by
-taking the maximum, and adding one to it. We declare this operation as an
-instance of the type class [Fresh]. *)
-Require Export numbers fin_collections.
-
-Definition Nmax `{Elements N C} : C → N := collection_fold Nmax 0%N.
-
-Instance Nmax_proper `{FinCollection N C} : Proper ((≡) ==> (=)) Nmax.
-Proof.
-  apply (collection_fold_proper (=)).
-  * solve_proper.
-  * intros. rewrite !N.max_assoc. f_equal. apply N.max_comm.
-Qed.
-
-Lemma Nmax_max `{FinCollection N C} X x : x ∈ X → (x ≤ Nmax X)%N.
-Proof.
-  apply (collection_fold_ind (λ b X, x ∈ X → (x ≤ b)%N)).
-  * solve_proper.
-  * solve_elem_of.
-  * solve_elem_of (eauto using N.le_max_l, N.le_max_r, N.le_trans).
-Qed.
-
-Instance Nfresh `{FinCollection N C} : Fresh N C := λ l, (1 + Nmax l)%N.
-Instance Nfresh_spec `{FinCollection N C} : FreshSpec N C.
-Proof.
-  split.
-  * apply _.
-  * intros. unfold fresh, Nfresh.
-    setoid_replace X with Y; [done |]. by apply elem_of_equiv.
-  * intros X E. assert (1 ≤ 0)%N as []; [| done].
-    apply N.add_le_mono_r with (Nmax X). by apply Nmax_max.
-Qed.
diff --git a/theories/nmap.v b/theories/nmap.v
index b6fcf98c..d534989e 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -84,3 +84,20 @@ Qed.
 Notation Nset := (mapset (Nmap unit)).
 Instance Nmap_dom {A} : Dom (Nmap A) Nset := mapset_dom.
 Instance: FinMapDom N Nmap Nset := mapset_dom_spec.
+
+(** * Fresh numbers *)
+Definition Nfresh {A} (m : Nmap A) : N :=
+  match m with NMap None _ => 0 | NMap _ m => Npos (Pfresh m) end.
+Lemma Nfresh_fresh {A} (m : Nmap A) : m !! Nfresh m = None.
+Proof. destruct m as [[]]. apply Pfresh_fresh. done. Qed. 
+
+Instance Nset_fresh : Fresh N Nset := λ X,
+  let (m) := X in Nfresh m.
+Instance Nset_fresh_spec : FreshSpec N Nset.
+Proof.
+  split.
+  * apply _.
+  * intros X Y; rewrite <-elem_of_equiv_L. by intros ->.
+  * unfold elem_of, mapset_elem_of, fresh; intros [m]; simpl.
+    by rewrite Nfresh_fresh.
+Qed.
diff --git a/theories/pmap.v b/theories/pmap.v
index 7bccbf96..c8c35fd6 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -390,3 +390,66 @@ Qed.
 Notation Pset := (mapset (Pmap unit)).
 Instance Pmap_dom {A} : Dom (Pmap A) Pset := mapset_dom.
 Instance: FinMapDom positive Pmap Pset := mapset_dom_spec.
+
+(** * Fresh numbers *)
+Fixpoint Pdepth {A} (m : Pmap_raw A) : nat :=
+  match m with
+  | PLeaf | PNode _ None _ => O | PNode l _ _ => S (Pdepth l)
+  end.
+Fixpoint Pfresh_at_depth {A} (m : Pmap_raw A) (d : nat) : option positive :=
+  match d, m with
+  | O, (PLeaf | PNode _ None _) => Some 1
+  | S d, PNode l _ r =>
+     match Pfresh_at_depth l d with
+     | Some i => Some (i~0) | None => (~1) <$> Pfresh_at_depth r d
+     end
+  | _, _ => None
+  end.
+Fixpoint Pfresh_go {A} (m : Pmap_raw A) (d : nat) : option positive :=
+  match d with
+  | O => None
+  | S d =>
+     match Pfresh_go m d with
+     | Some i => Some i | None => Pfresh_at_depth m d
+     end
+  end.
+Definition Pfresh {A} (m : Pmap A) : positive :=
+  let d := Pdepth (pmap_car m) in
+  match Pfresh_go (pmap_car m) d with
+  | Some i => i | None => Pos.shiftl_nat 1 d
+  end.
+
+Lemma Pfresh_at_depth_fresh {A} (m : Pmap_raw A) d i :
+  Pfresh_at_depth m d = Some i → m !! i = None.
+Proof.
+  revert i m; induction d as [|d IH].
+  { intros i [|l [] r] ?; naive_solver. }
+  intros i [|l o r] ?; simplify_equality'.
+  destruct (Pfresh_at_depth l d) as [i'|] eqn:?,
+    (Pfresh_at_depth r d) as [i''|] eqn:?; simplify_equality'; auto.
+Qed.
+Lemma Pfresh_go_fresh {A} (m : Pmap_raw A) d i :
+  Pfresh_go m d = Some i → m !! i = None.
+Proof.
+  induction d as [|d IH]; intros; simplify_equality'.
+  destruct (Pfresh_go m d); eauto using Pfresh_at_depth_fresh.
+Qed.
+Lemma Pfresh_depth {A} (m : Pmap_raw A) :
+  m !! Pos.shiftl_nat 1 (Pdepth m) = None.
+Proof. induction m as [|l IHl [x|] r IHr]; auto. Qed.
+Lemma Pfresh_fresh {A} (m : Pmap A) : m !! Pfresh m = None.
+Proof.
+  destruct m as [m ?]; unfold lookup, Plookup, Pfresh; simpl.
+  destruct (Pfresh_go m _) eqn:?; eauto using Pfresh_go_fresh, Pfresh_depth.
+Qed.
+
+Instance Pset_fresh : Fresh positive Pset := λ X,
+  let (m) := X in Pfresh m.
+Instance Pset_fresh_spec : FreshSpec positive Pset.
+Proof.
+  split.
+  * apply _.
+  * intros X Y; rewrite <-elem_of_equiv_L. by intros ->.
+  * unfold elem_of, mapset_elem_of, fresh; intros [m]; simpl.
+    by rewrite Pfresh_fresh.
+Qed.
diff --git a/theories/prelude.v b/theories/prelude.v
index 219e3c9a..75e7d672 100644
--- a/theories/prelude.v
+++ b/theories/prelude.v
@@ -12,6 +12,5 @@ Require Export
   collections
   fin_collections
   listset
-  fresh_numbers
   list
   lexico.
-- 
GitLab