From ecbac61a665c27d44c9ab2e7d2a27c55a7d3d4be Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Wed, 2 Mar 2016 18:24:00 +0100
Subject: [PATCH] rename BAnom -> BAnon; avoid overloading notation in the same
 scope

---
 barrier/client.v         |  2 +-
 heap_lang/derived.v      |  8 ++++----
 heap_lang/lang.v         | 20 +++++++++++++-------
 heap_lang/lifting.v      |  2 --
 heap_lang/notation.v     | 36 +++++++++++++++++++-----------------
 heap_lang/substitution.v |  2 +-
 heap_lang/tests.v        |  2 --
 heap_lang/wp_tactics.v   |  2 +-
 8 files changed, 39 insertions(+), 35 deletions(-)

diff --git a/barrier/client.v b/barrier/client.v
index 0ed241d8b..ffb962c27 100644
--- a/barrier/client.v
+++ b/barrier/client.v
@@ -56,7 +56,7 @@ Section client.
       wp_seq. (ewp eapply wp_store); eauto with I. strip_later.
       rewrite assoc [(_ ★ y ↦ _)%I]comm. apply sep_mono_r, wand_intro_l.
       wp_seq. rewrite -signal_spec right_id assoc sep_elim_l comm.
-      apply sep_mono_r. rewrite /y_inv -(exist_intro (λ: "z", "z" + #42)%L).
+      apply sep_mono_r. rewrite /y_inv -(exist_intro (λ: "z", "z" + #42)%V).
       apply sep_intro_True_r; first done. apply: always_intro.
       apply forall_intro=>n. wp_let. wp_op. by apply const_intro. }
     (* The two spawned threads, the waiters. *)
diff --git a/heap_lang/derived.v b/heap_lang/derived.v
index 196ddf4f7..d8957ece3 100644
--- a/heap_lang/derived.v
+++ b/heap_lang/derived.v
@@ -2,12 +2,12 @@ From heap_lang Require Export lifting.
 Import uPred.
 
 (** Define some derived forms, and derived lemmas about them. *)
-Notation Lam x e := (Rec BAnom x e).
+Notation Lam x e := (Rec BAnon x e).
 Notation Let x e1 e2 := (App (Lam x e2) e1).
-Notation Seq e1 e2 := (Let BAnom e1 e2).
-Notation LamV x e := (RecV BAnom x e).
+Notation Seq e1 e2 := (Let BAnon e1 e2).
+Notation LamV x e := (RecV BAnon x e).
 Notation LetCtx x e2 := (AppRCtx (LamV x e2)).
-Notation SeqCtx e2 := (LetCtx BAnom e2).
+Notation SeqCtx e2 := (LetCtx BAnon e2).
 Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
 Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)).
 
diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index db52de949..b5ee9c9c3 100644
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
@@ -15,9 +15,14 @@ Inductive un_op : Set :=
 Inductive bin_op : Set :=
   | PlusOp | MinusOp | LeOp | LtOp | EqOp.
 
-Inductive binder := BAnom | BNamed : string → binder.
+Inductive binder := BAnon | BNamed : string → binder.
+
 Delimit Scope binder_scope with binder.
-Bind Scope binder_scope with expr binder.
+Bind Scope binder_scope with binder.
+Delimit Scope lang_scope with L.
+Bind Scope lang_scope with base_lit.
+Delimit Scope val_scope with V.
+Bind Scope val_scope with base_lit.
 
 Inductive expr :=
   (* Base lambda calculus *)
@@ -54,6 +59,10 @@ Inductive val :=
   | InjRV (v : val)
   | LocV (l : loc).
 
+Bind Scope binder_scope with expr.
+Bind Scope lang_scope with expr base_lit.
+Bind Scope val_scope with val base_lit.
+
 Global Instance base_lit_dec_eq (l1 l2 : base_lit) : Decision (l1 = l2).
 Proof. solve_decision. Defined.
 Global Instance un_op_dec_eq (op1 op2 : un_op) : Decision (op1 = op2).
@@ -67,9 +76,6 @@ Proof. solve_decision. Defined.
 Global Instance val_dec_eq (v1 v2 : val) : Decision (v1 = v2).
 Proof. solve_decision. Defined.
 
-Delimit Scope lang_scope with L.
-Bind Scope lang_scope with expr val base_lit.
-
 Fixpoint of_val (v : val) : expr :=
   match v with
   | RecV f x e => Rec f x e
@@ -144,7 +150,7 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
 Definition fill (K : ectx) (e : expr) : expr := fold_right fill_item e K.
 
 (** Substitution *)
-(** We have [subst e None v = e] to deal with anonymous binders *)
+(** We have [subst' e BAnon v = e] to deal with anonymous binders *)
 Fixpoint subst (e : expr) (x : string) (v : val) : expr :=
   match e with
   | Var y => if decide (x = y) then of_val v else Var y
@@ -170,7 +176,7 @@ Fixpoint subst (e : expr) (x : string) (v : val) : expr :=
   | Cas e0 e1 e2 => Cas (subst e0 x v) (subst e1 x v) (subst e2 x v)
   end.
 Definition subst' (e : expr) (mx : binder) (v : val) : expr :=
-  match mx with BNamed x => subst e x v | BAnom => e end.
+  match mx with BNamed x => subst e x v | BAnon => e end.
 
 (** The stepping relation *)
 Definition un_op_eval (op : un_op) (l : base_lit) : option base_lit :=
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index da7962dee..70200c1b3 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -82,8 +82,6 @@ Proof.
   rewrite later_sep -(wp_value _ _ (Lit _)) //.
 Qed.
 
-(* For the lemmas involving substitution, we only derive a preliminary version.
-   The final version is defined in substitution.v. *)
 Lemma wp_rec E f x e1 e2 v Φ :
   to_val e2 = Some v →
   ▷ || subst' (subst' e1 f (RecV f x e1)) x v @ E {{ Φ }}
diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index 0b4ea4752..e0bdc4ac7 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -17,7 +17,7 @@ Coercion App : expr >-> Funclass.
 Coercion of_val : val >-> expr.
 
 Coercion BNamed : string >-> binder.
-Notation "<>" := BAnom : binder_scope.
+Notation "<>" := BAnon : binder_scope.
 
 (** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
     first. *)
@@ -30,9 +30,9 @@ Notation "( e1 , e2 , .. , en )" := (Pair .. (Pair e1 e2) .. en) : lang_scope.
 Notation "'match:' e0 'with' 'InjL' x1 => e1 | 'InjR' x2 => e2 'end'" :=
   (Match e0 x1 e1 x2 e2)
   (e0, x1, e1, x2, e2 at level 200) : lang_scope.
-Notation "()" := LitUnit : lang_scope.
-Notation "# l" := (Lit l%Z%L) (at level 8, format "# l").
-Notation "# l" := (LitV l%Z%L) (at level 8, format "# l").
+Notation "()" := LitUnit : val_scope.
+(* No scope, does not conflict and scope is often not inferred properly. *)
+Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
 Notation "! e" := (Load e%L) (at level 9, right associativity) : lang_scope.
 Notation "'ref' e" := (Alloc e%L)
   (at level 30, right associativity) : lang_scope.
@@ -51,7 +51,7 @@ Notation "e1 <- e2" := (Store e1%L e2%L) (at level 80) : lang_scope.
 Notation "'rec:' f x := e" := (Rec f x e%L)
   (at level 102, f at level 1, x at level 1, e at level 200) : lang_scope.
 Notation "'rec:' f x := e" := (RecV f x e%L)
-  (at level 102, f at level 1, x at level 1, e at level 200) : lang_scope.
+  (at level 102, f at level 1, x at level 1, e at level 200) : val_scope.
 Notation "'if:' e1 'then' e2 'else' e3" := (If e1%L e2%L e3%L)
   (at level 200, e1, e2, e3 at level 200) : lang_scope.
 
@@ -62,29 +62,31 @@ notations are otherwise not pretty printed back accordingly. *)
 Notation "λ: x , e" := (Lam x e%L)
   (at level 102, x at level 1, e at level 200) : lang_scope.
 Notation "λ: x , e" := (LamV x e%L)
-  (at level 102, x at level 1, e at level 200) : lang_scope.
+  (at level 102, x at level 1, e at level 200) : val_scope.
+
 Notation "'let:' x := e1 'in' e2" := (Lam x e2%L e1%L)
   (at level 102, x at level 1, e1, e2 at level 200) : lang_scope.
-Notation "'let:' x := e1 'in' e2" := (LamV x e2%L e1%L)
-  (at level 102, x at level 1, e1, e2 at level 200) : lang_scope.
-Notation "e1 ;; e2" := (Lam BAnom e2%L e1%L)
-  (at level 100, e2 at level 200, format "e1  ;;  e2") : lang_scope.
-Notation "e1 ;; e2" := (LamV BAnom e2%L e1%L)
+Notation "e1 ;; e2" := (Lam BAnon e2%L e1%L)
   (at level 100, e2 at level 200, format "e1  ;;  e2") : lang_scope.
+(* These are not actually values, but we want them to be pretty-printed. *)
+Notation "'let:' x := e1 'in' e2" := (LamV x e2%L e1%L)
+  (at level 102, x at level 1, e1, e2 at level 200) : val_scope.
+Notation "e1 ;; e2" := (LamV BAnon e2%L e1%L)
+  (at level 100, e2 at level 200, format "e1  ;;  e2") : val_scope.
 
 Notation "'rec:' f x y := e" := (Rec f x (Lam y e%L))
   (at level 102, f, x, y at level 1, e at level 200) : lang_scope.
 Notation "'rec:' f x y := e" := (RecV f x (Lam y e%L))
-  (at level 102, f, x, y at level 1, e at level 200) : lang_scope.
+  (at level 102, f, x, y at level 1, e at level 200) : val_scope.
 Notation "'rec:' f x y z := e" := (Rec f x (Lam y (Lam z e%L)))
   (at level 102, f, x, y, z at level 1, e at level 200) : lang_scope.
 Notation "'rec:' f x y z := e" := (RecV f x (Lam y (Lam z e%L)))
-  (at level 102, f, x, y, z at level 1, e at level 200) : lang_scope.
+  (at level 102, f, x, y, z at level 1, e at level 200) : val_scope.
 Notation "λ: x y , e" := (Lam x (Lam y e%L))
   (at level 102, x, y at level 1, e at level 200) : lang_scope.
 Notation "λ: x y , e" := (LamV x (Lam y e%L))
-  (at level 102, x, y at level 1, e at level 200) : lang_scope.
-Notation "λ: x y z , e" := (Lam x (LamV y (LamV z e%L)))
-  (at level 102, x, y, z at level 1, e at level 200) : lang_scope.
-Notation "λ: x y z , e" := (LamV x (LamV y (LamV z e%L)))
+  (at level 102, x, y at level 1, e at level 200) : val_scope.
+Notation "λ: x y z , e" := (Lam x (Lam y (Lam z e%L)))
   (at level 102, x, y, z at level 1, e at level 200) : lang_scope.
+Notation "λ: x y z , e" := (LamV x (Lam y (Lam z e%L)))
+  (at level 102, x, y, z at level 1, e at level 200) : val_scope.
diff --git a/heap_lang/substitution.v b/heap_lang/substitution.v
index 6c98a0ab1..97836ee6d 100644
--- a/heap_lang/substitution.v
+++ b/heap_lang/substitution.v
@@ -111,7 +111,7 @@ Instance subst_cas e0 e1 e2 x v e0r e1r e2r :
 Proof. by intros; red; f_equal/=. Qed.
 
 Definition of_binder (mx : binder) : stringset :=
-  match mx with BAnom => ∅ | BNamed x => {[ x ]} end.
+  match mx with BAnon => ∅ | BNamed x => {[ x ]} end.
 Lemma elem_of_of_binder x mx: x ∈ of_binder mx ↔ mx = BNamed x.
 Proof. destruct mx; set_solver. Qed.
 Global Instance set_unfold_of_binder (mx : binder) x :
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 6c694ac23..54baf3fe7 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -90,6 +90,4 @@ Section ClosedProofs.
     apply wp_strip_pvs, exist_elim=> ?. rewrite and_elim_l.
     rewrite -heap_e_spec; first by eauto with I. by rewrite nclose_nroot.
   Qed.
-
-  Print Assumptions heap_e_closed.
 End ClosedProofs.
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 4ad185a0a..c9b6bd404 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -41,7 +41,7 @@ Tactic Notation "wp_lam" ">" :=
   match goal with
   | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval cbv in e' with
-    | App (Rec BAnom _ _) _ =>
+    | App (Rec BAnon _ _) _ =>
        wp_bind K; etrans;
          [|eapply wp_lam; repeat (reflexivity || rewrite /= to_of_val)];
          simpl_subst; wp_finish
-- 
GitLab