From 2b7a62bf66e79e4a0b8f39fc95a505fab01ea433 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Wed, 2 Mar 2016 18:40:07 +0100
Subject: [PATCH] notation for locations

---
 barrier/client.v     |  2 +-
 barrier/proof.v      |  6 +++---
 heap_lang/notation.v | 12 +++++-------
 3 files changed, 9 insertions(+), 11 deletions(-)

diff --git a/barrier/client.v b/barrier/client.v
index ffb962c27..3a97f9598 100644
--- a/barrier/client.v
+++ b/barrier/client.v
@@ -27,7 +27,7 @@ Section client.
 
   Lemma worker_safe q (n : Z) (b y : loc) :
     (heap_ctx heapN ★ recv heapN N b (y_inv q y))
-      ⊑ || worker n (Loc b) (Loc y) {{ λ _, True }}.
+      ⊑ || worker n (%b) (%y) {{ λ _, True }}.
   Proof.
     rewrite /worker. wp_lam. wp_let. ewp apply wait_spec.
     rewrite comm. apply sep_mono_r. apply wand_intro_l.
diff --git a/barrier/proof.v b/barrier/proof.v
index bc5e1c04a..b849ce969 100644
--- a/barrier/proof.v
+++ b/barrier/proof.v
@@ -125,7 +125,7 @@ Qed.
 (** Actual proofs *)
 Lemma newbarrier_spec (P : iProp) (Φ : val → iProp) :
   heapN ⊥ N →
-  (heap_ctx heapN ★ ∀ l, recv l P ★ send l P -★ Φ (LocV l))
+  (heap_ctx heapN ★ ∀ l, recv l P ★ send l P -★ Φ (%l))
   ⊑ || newbarrier #() {{ Φ }}.
 Proof.
   intros HN. rewrite /newbarrier. wp_seq.
@@ -172,7 +172,7 @@ Proof.
 Qed.
 
 Lemma signal_spec l P (Φ : val → iProp) :
-  (send l P ★ P ★ Φ #()) ⊑ || signal (LocV l) {{ Φ }}.
+  (send l P ★ P ★ Φ #()) ⊑ || signal (%l) {{ Φ }}.
 Proof.
   rewrite /signal /send /barrier_ctx. rewrite sep_exist_r.
   apply exist_elim=>γ. rewrite -!assoc. apply const_elim_sep_l=>?. wp_let.
@@ -199,7 +199,7 @@ Proof.
 Qed.
 
 Lemma wait_spec l P (Φ : val → iProp) :
-  (recv l P ★ (P -★ Φ #())) ⊑ || wait (LocV l) {{ Φ }}.
+  (recv l P ★ (P -★ Φ #())) ⊑ || wait (%l) {{ Φ }}.
 Proof.
   rename P into R. wp_rec.
   rewrite {1}/recv /barrier_ctx. rewrite !sep_exist_r.
diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index e0bdc4ac7..1ea9ae21e 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -21,18 +21,16 @@ Notation "<>" := BAnon : binder_scope.
 
 (** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
     first. *)
-(* We have overlapping notation for values and expressions, with the expressions
-   coming first. This way, parsing as a value will be preferred. If an expression
-   was needed, the coercion of_val will be called. The notations for literals
-   are not put in any scope so as to avoid lots of annoying %L scopes while
-   pretty printing. *)
+
+(* No scope, does not conflict and scope is often not inferred properly. *)
+Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
+Notation "% l" := (LocV l) (at level 8, format "% l").
+
 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 : 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.
-- 
GitLab