Consolidate =* and =*> to bedrock2.Map.Separation

mit-plv · Jun 20, 2023 · 4929e1b · 4929e1b
1 parent 8d146d9
commit 4929e1b
Show file tree

Hide file tree

Showing 10 changed files with 3 additions and 10 deletions.
diff --git a/bedrock2/src/bedrock2/Map/Separation.v b/bedrock2/src/bedrock2/Map/Separation.v
@@ -20,3 +20,5 @@ Declare Scope sep_scope.
 Delimit Scope sep_scope with sep.
 Infix "*" := sep (at level 40, left associativity) : sep_scope.
 Infix "⋆" := sep (at level 40, left associativity) : sep_scope.
+Notation "m =* P" := ((P%sep) m) (at level 70, only parsing).
+Notation "m =*> P" := (exists R, (sep P R) m) (at level 70, only parsing).
diff --git a/bedrock2/src/bedrock2Examples/indirect_add.v b/bedrock2/src/bedrock2Examples/indirect_add.v
@@ -26,7 +26,6 @@ Section WithParameters.
 
   Definition f (a b : word) := word.add (word.add a b) b.
 
-  Local Notation "m =* P" := (P%sep m) (at level 70, only parsing). (* experiment *)
   Instance spec_of_indirect_add : spec_of "indirect_add" :=
     fnspec! "indirect_add" a b c / va Ra vb Rb vc Rc,
     { requires t m := m =* scalar a va * Ra /\ m =* scalar b vb * Rb /\ m =* scalar c vc * Rc;

diff --git a/bedrock2/src/bedrock2Examples/indirect_add_heapletwise.v b/bedrock2/src/bedrock2Examples/indirect_add_heapletwise.v
@@ -30,7 +30,6 @@ Section WithParameters.
 
   Definition f (a b : word) := word.add (word.add a b) b.
 
-  Local Notation "m =* P" := (P%sep m) (at level 70, only parsing). (* experiment *)
   Instance spec_of_indirect_add : spec_of "indirect_add" :=
     fnspec! "indirect_add" a b c / va Ra vb Rb vc Rc,
     { requires t m :=

diff --git a/bedrock2/src/bedrock2Examples/memconst.v b/bedrock2/src/bedrock2Examples/memconst.v
@@ -20,7 +20,6 @@ Local Notation string := String.string.
 
 (*Require Import bedrock2.ptsto_bytes.*)
 Local Notation "xs $@ a" := (Array.array ptsto (word.of_Z 1) a xs) (at level 10, format "xs $@ a").
-Local Notation "m =* P" := ((P%sep) m) (at level 70, only parsing) (* experiment*).
 
 Section WithParameters.
   Context {width} {BW: Bitwidth width}.

diff --git a/bedrock2/src/bedrock2Examples/memequal.v b/bedrock2/src/bedrock2Examples/memequal.v
@@ -23,7 +23,6 @@ Local Notation string := String.string.
 
 (*Require Import bedrock2.ptsto_bytes.*)
 Local Notation "xs $@ a" := (Array.array ptsto (word.of_Z 1) a xs) (at level 10, format "xs $@ a").
-Local Notation "m =* P" := ((P%sep) m) (at level 70, only parsing) (* experiment*).
 
 Section WithParameters.
   Context {width} {BW: Bitwidth width}.

diff --git a/bedrock2/src/bedrock2Examples/memmove.v b/bedrock2/src/bedrock2Examples/memmove.v
@@ -14,7 +14,6 @@ Local Notation string := String.string.
 (*Require Import bedrock2.ptsto_bytes.*)
 Require Import coqutil.Map.OfListWord.
 Local Notation "xs $@ a" := (map.of_list_word_at a xs) (at level 10, format "xs $@ a").
-Local Notation "m =* P" := ((P%sep) m) (at level 70, only parsing) (* experiment*).
 
 Section WithParameters.
   Context {width} {BW: Bitwidth width}.

diff --git a/bedrock2/src/bedrock2Examples/memswap.v b/bedrock2/src/bedrock2Examples/memswap.v
@@ -27,7 +27,6 @@ Local Notation string := String.string.
 
 (*Require Import bedrock2.ptsto_bytes.*)
 Local Notation "xs $@ a" := (Array.array ptsto (word.of_Z 1) a xs) (at level 10, format "xs $@ a").
-Local Notation "m =* P" := ((P%sep) m) (at level 70, only parsing) (* experiment*).
 
 Section WithParameters.
   Context {width} {BW: Bitwidth width}.

diff --git a/bedrock2/src/bedrock2Examples/swap.v b/bedrock2/src/bedrock2Examples/swap.v
@@ -32,7 +32,6 @@ Require Import coqutil.Tactics.rdelta.
 Section WithParameters.
   Context {word: word.word 32} {mem: map.map word Byte.byte}.
   Context {word_ok: word.ok word} {mem_ok: map.ok mem}.
-  Local Notation "m =* P" := ((P%sep) m) (at level 70, only parsing) (* experiment*).
 
   Instance spec_of_swap : spec_of "swap" :=
     fnspec! "swap" a_addr b_addr / a b R,

diff --git a/bedrock2/src/bedrock2Examples/swap_by_add.v b/bedrock2/src/bedrock2Examples/swap_by_add.v
@@ -26,7 +26,7 @@ Require Import coqutil.Tactics.eplace Coq.setoid_ring.Ring_tac.
 
 Section WithParameters.
   Context {mem: map.map word32 Byte.byte} {mem_ok: map.ok mem}.
-  Local Notation "m =* P" := ((P%sep) (m : mem)) (at level 70, only parsing) (* experiment*).
+  Implicit Types (R : mem -> Prop).
 
   Instance spec_of_swap : spec_of "swap" :=
     fnspec! "swap" a_addr b_addr / a b R,

diff --git a/bedrock2/src/bedrock2Examples/uint128_32.v b/bedrock2/src/bedrock2Examples/uint128_32.v
@@ -48,8 +48,6 @@ Local Ltac invert H := inversion H; clear H.
 Section WithParameters.
   Context {word: word.word 32} {mem: map.map word Byte.byte}.
   Context {word_ok: word.ok word} {mem_ok: map.ok mem}.
-  Local Notation "m =* P" := ((P%sep) m) (at level 70, only parsing) (* experiment*).
-  Local Notation "m =*> P" := (exists R, (sep P R) m) (at level 70, only parsing) (* experiment*).
   Import ProgramLogic.Coercions.
   Local Number Notation nat Nat.of_num_uint Nat.to_num_hex_uint (abstract after 5001) : core_scope.
   Local Number Notation nat Nat.of_num_uint Nat.to_num_uint (abstract after 5001) : core_scope.