From a00676623e63af33280f1694ec8957a21678d6d6 Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@mpi-sws.org>
Date: Thu, 25 Aug 2016 16:33:53 +0200
Subject: [PATCH] Define E and V scopes in program_logic

---
 heap_lang/lang.v           | 22 ----------------------
 heap_lang/lib/spawn.v      |  1 +
 heap_lang/notation.v       | 16 ----------------
 program_logic/language.v   |  4 ++++
 program_logic/weakestpre.v | 10 +++++-----
 5 files changed, 10 insertions(+), 43 deletions(-)

diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index f850174c4..8f6bac10b 100644
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
@@ -59,24 +59,6 @@ Inductive expr :=
   | CAS (e0 : expr) (e1 : expr) (e2 : expr).
 
 Bind Scope expr_scope with expr.
-Delimit Scope expr_scope with E.
-Arguments Rec _ _ _%E.
-Arguments App _%E _%E.
-Arguments Lit _.
-Arguments UnOp _ _%E.
-Arguments BinOp _ _%E _%E.
-Arguments If _%E _%E _%E.
-Arguments Pair _%E _%E.
-Arguments Fst _%E.
-Arguments Snd _%E.
-Arguments InjL _%E.
-Arguments InjR _%E.
-Arguments Case _%E _%E _%E.
-Arguments Fork _%E.
-Arguments Alloc _%E.
-Arguments Load _%E.
-Arguments Store _%E _%E.
-Arguments CAS _%E _%E _%E.
 
 Fixpoint is_closed (X : list string) (e : expr) : bool :=
   match e with
@@ -105,10 +87,6 @@ Inductive val :=
   | InjRV (v : val).
 
 Bind Scope val_scope with val.
-Delimit Scope val_scope with V.
-Arguments PairV _%V _%V.
-Arguments InjLV _%V.
-Arguments InjRV _%V.
 
 Fixpoint of_val (v : val) : expr :=
   match v with
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index 50e2c21f0..81195b9d4 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -53,6 +53,7 @@ Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) (Φ : val → iProp Σ) :
   ⊢ WP spawn e {{ Φ }}.
 Proof.
   iIntros (<-%of_to_val ?) "(#Hh & Hf & HΦ)". rewrite /spawn.
+  (* TODO: Coq is printing %V here.  *)
   wp_let. wp_alloc l as "Hl". wp_let.
   iVs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
   iVs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index 45e6932a4..600cca0a3 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -1,22 +1,6 @@
 From iris.heap_lang Require Export derived.
 Export heap_lang.
 
-Arguments wp {_ _ _} _ _%E _.
-
-Notation "'WP' e @ E {{ Φ } }" := (wp E e%E Φ)
-  (at level 20, e, Φ at level 200,
-   format "'WP'  e  @  E  {{  Φ  } }") : uPred_scope.
-Notation "'WP' e {{ Φ } }" := (wp ⊤ e%E Φ)
-  (at level 20, e, Φ at level 200,
-   format "'WP'  e  {{  Φ  } }") : uPred_scope.
-
-Notation "'WP' e @ E {{ v , Q } }" := (wp E e%E (λ v, Q))
-  (at level 20, e, Q at level 200,
-   format "'WP'  e  @  E  {{  v ,  Q  } }") : uPred_scope.
-Notation "'WP' e {{ v , Q } }" := (wp ⊤ e%E (λ v, Q))
-  (at level 20, e, Q at level 200,
-   format "'WP'  e  {{  v ,  Q  } }") : uPred_scope.
-
 Coercion LitInt : Z >-> base_lit.
 Coercion LitBool : bool >-> base_lit.
 Coercion LitLoc : loc >-> base_lit.
diff --git a/program_logic/language.v b/program_logic/language.v
index 04bba2a4a..cd33108da 100644
--- a/program_logic/language.v
+++ b/program_logic/language.v
@@ -11,6 +11,10 @@ Structure language := Language {
   of_to_val e v : to_val e = Some v → of_val v = e;
   val_stuck e σ e' σ' efs : prim_step e σ e' σ' efs → to_val e = None
 }.
+Delimit Scope expr_scope with E.
+Delimit Scope val_scope with V.
+Bind Scope expr_scope with expr.
+Bind Scope expr_scope with val.
 Arguments of_val {_} _.
 Arguments to_val {_} _.
 Arguments prim_step {_} _ _ _ _ _.
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 3026e7e71..2e94c9ccd 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -33,20 +33,20 @@ Definition wp_aux : { x | x = @wp_def }. by eexists. Qed.
 Definition wp := proj1_sig wp_aux.
 Definition wp_eq : @wp = @wp_def := proj2_sig wp_aux.
 
-Arguments wp {_ _ _} _ _ _.
+Arguments wp {_ _ _} _ _%E _.
 Instance: Params (@wp) 5.
 
-Notation "'WP' e @ E {{ Φ } }" := (wp E e Φ)
+Notation "'WP' e @ E {{ Φ } }" := (wp E e%E Φ)
   (at level 20, e, Φ at level 200,
    format "'WP'  e  @  E  {{  Φ  } }") : uPred_scope.
-Notation "'WP' e {{ Φ } }" := (wp ⊤ e Φ)
+Notation "'WP' e {{ Φ } }" := (wp ⊤ e%E Φ)
   (at level 20, e, Φ at level 200,
    format "'WP'  e  {{  Φ  } }") : uPred_scope.
 
-Notation "'WP' e @ E {{ v , Q } }" := (wp E e (λ v, Q))
+Notation "'WP' e @ E {{ v , Q } }" := (wp E e%E (λ v, Q))
   (at level 20, e, Q at level 200,
    format "'WP'  e  @  E  {{  v ,  Q  } }") : uPred_scope.
-Notation "'WP' e {{ v , Q } }" := (wp ⊤ e (λ v, Q))
+Notation "'WP' e {{ v , Q } }" := (wp ⊤ e%E (λ v, Q))
   (at level 20, e, Q at level 200,
    format "'WP'  e  {{  v ,  Q  } }") : uPred_scope.
 
-- 
GitLab