Define E and V scopes in program_logic

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

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 "#?".

heap_lang/notation.v

 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.

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 {_} _ _ _ _ _.

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.
 

[Robbert Krebbers]

Great idea. Merged!

[Ralf Jung]

You didn't even wait for @janno to create a merge request? ;)

[Ralf Jung]

(Needless to say, I fully approve.)

[Janno]

It was Ralf's idea to define the scopes earlier. I don't want to take credit for that. I was simply working on notation stuff already. (And the next pull request will rely on these scopes).