From 6ac4c4ebb0a0d0bb24abc12e088ebe5ffb4ffd76 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 28 Jun 2018 22:56:43 +0200
Subject: [PATCH] move option notation to lang.v so we can use it to define CAS
 compare safety

---
 theories/heap_lang/lang.v     | 18 ++++++++++++------
 theories/heap_lang/notation.v |  6 ------
 2 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 4c0027c96..55444e52f 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -66,6 +66,9 @@ Inductive expr :=
   | CAS (e0 : expr) (e1 : expr) (e2 : expr)
   | FAA (e1 : expr) (e2 : expr).
 
+Notation NONE := (InjL (Lit LitUnit)) (only parsing).
+Notation SOME x := (InjR x) (only parsing).
+
 Bind Scope expr_scope with expr.
 
 Fixpoint is_closed (X : list string) (e : expr) : bool :=
@@ -94,6 +97,9 @@ Inductive val :=
   | InjLV (v : val)
   | InjRV (v : val).
 
+Notation NONEV := (InjLV (LitV LitUnit)) (only parsing).
+Notation SOMEV x := (InjRV x) (only parsing).
+
 Bind Scope val_scope with val.
 
 Fixpoint of_val (v : val) : expr :=
@@ -365,12 +371,12 @@ Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
 Definition vals_cas_compare_safe (vl v1 : val) : Prop :=
   match vl, v1 with
   | LitV _, LitV _ => True
-  (* We want to support CAS'ing [NONEV := InjLV LitUnit] to [SOMEV #l := InjRV
-  (LitV l)].  An implementation of this is possible if literals have an invalid
-  bit pattern that can be used to represent NONE. *)
-  | InjLV (LitV LitUnit), InjLV (LitV LitUnit) => True
-  | InjLV (LitV LitUnit), InjRV (LitV _) => True
-  | InjRV (LitV _), InjLV (LitV LitUnit) => True
+  (* We want to support CAS'ing [NONEV] to [SOMEV #l].  An implementation of
+  this is possible if literals have an invalid bit pattern that can be used to
+  represent NONE. *)
+  | NONEV, NONEV => True
+  | NONEV, SOMEV (LitV _) => True
+  | SOMEV (LitV _), NONEV => True
   | _, _ => False
   end.
 (** Just a sanity check. *)
diff --git a/theories/heap_lang/notation.v b/theories/heap_lang/notation.v
index b3f40e897..d991e108d 100644
--- a/theories/heap_lang/notation.v
+++ b/theories/heap_lang/notation.v
@@ -144,12 +144,6 @@ Notation "e1 || e2" :=
   (If e1%E (Lit (LitBool true)) e2%E) (only parsing) : expr_scope.
 
 (** Notations for option *)
-Notation NONE := (InjL #()) (only parsing).
-Notation SOME x := (InjR x) (only parsing).
-
-Notation NONEV := (InjLV #()) (only parsing).
-Notation SOMEV x := (InjRV x) (only parsing).
-
 Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" :=
   (Match e0 BAnon e1 x%bind e2)
   (e0, e1, x, e2 at level 200, only parsing) : expr_scope.
-- 
GitLab