From 3f1a95d129ddbb5e9f735d5b845dc5c1bac58c09 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 17 Mar 2021 11:56:34 +0100
Subject: [PATCH] move scope tests to new file

---
 tests/iris_notation.ref |  0
 tests/iris_notation.v   | 45 +++++++++++++++++++++++++++++++++++++++++
 tests/proofmode_iris.v  | 22 --------------------
 3 files changed, 45 insertions(+), 22 deletions(-)
 create mode 100644 tests/iris_notation.ref
 create mode 100644 tests/iris_notation.v

diff --git a/tests/iris_notation.ref b/tests/iris_notation.ref
new file mode 100644
index 000000000..e69de29bb
diff --git a/tests/iris_notation.v b/tests/iris_notation.v
new file mode 100644
index 000000000..3e6fb5536
--- /dev/null
+++ b/tests/iris_notation.v
@@ -0,0 +1,45 @@
+From iris.algebra Require Import frac.
+From iris.proofmode Require Import tactics monpred.
+From iris.base_logic Require Import base_logic lib.fancy_updates.
+
+Section base_logic_tests.
+  Context {M : ucmra}.
+  Implicit Types P Q R : uPred M.
+
+  (* Test scopes for bupd *)
+  Definition use_bupd_uPred (n : nat) : uPred M :=
+    □ |==> ∃ m : nat , ⌜ n = 2 ⌝.
+  Definition use_plainly_uPred (n : nat) : uPred M :=
+    ■ |==> ∃ m : nat , ⌜ n = 2 ⌝.
+
+  (* Test scopes inside big-ops *)
+  Definition big_op_scope_uPred_1 (xs : list nat) : uPred M :=
+    [∗ list] _ ↦ x ∈ xs, True.
+  Definition big_op_scope_uPred_2 (xs : list nat) : uPred M :=
+    [∗ list] x; y ∈ xs; xs, True.
+  Definition big_op_scope_uPred_3 (m : gmap nat nat) : uPred M :=
+    [∗ map] _ ↦ x ∈ m, True.
+  Definition big_op_scope_uPred_4 (m : gmap nat nat) : uPred M :=
+    [∗ map] x; y ∈ m; m, True.
+End base_logic_tests.
+
+Section iris_tests.
+  Context `{!invG Σ}.
+  Implicit Types P Q R : iProp Σ.
+
+  (* Test scopes for bupd and fupd *)
+  Definition use_bupd_iProp (n : nat) : iProp Σ :=
+    □ |==> ∃ m : nat , ⌜ n = 2 ⌝.
+  Definition use_fupd_iProp (n : nat) : iProp Σ :=
+    □ |={⊤}=> ∃ m : nat , ⌜ n = 2 ⌝.
+
+  (* Test scopes inside big-ops *)
+  Definition big_op_scope_iProp_1 (xs : list nat) : iProp Σ :=
+    [∗ list] _ ↦ x ∈ xs, True.
+  Definition big_op_scope_iProp_2 (xs : list nat) : iProp Σ :=
+    [∗ list] x; y ∈ xs; xs, True.
+  Definition big_op_scope_iProp_3 (m : gmap nat nat) : iProp Σ :=
+    [∗ map] _ ↦ x ∈ m, True.
+  Definition big_op_scope_iProp_4 (m : gmap nat nat) : iProp Σ :=
+    [∗ map] x; y ∈ m; m, True.
+End iris_tests.
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index 0d1c96a3a..f8601d2b0 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -9,22 +9,6 @@ Section base_logic_tests.
   Context {M : ucmra}.
   Implicit Types P Q R : uPred M.
 
-  (* Test scopes for bupd *)
-  Definition use_bupd_uPred (n : nat) : uPred M :=
-    □ |==> ∃ m : nat , ⌜ n = 2 ⌝.
-  Definition use_plainly_uPred (n : nat) : uPred M :=
-    ■ |==> ∃ m : nat , ⌜ n = 2 ⌝.
-
-  (* Test scopes inside big-ops *)
-  Definition big_op_scope_1 (xs : list nat) : uPred M :=
-    [∗ list] _ ↦ x ∈ xs, True.
-  Definition big_op_scope_2 (xs : list nat) : uPred M :=
-    [∗ list] x; y ∈ xs; xs, True.
-  Definition big_op_scope_3 (m : gmap nat nat) : uPred M :=
-    [∗ map] _ ↦ x ∈ m, True.
-  Definition big_op_scope_4 (m : gmap nat nat) : uPred M :=
-    [∗ map] x; y ∈ m; m, True.
-
   Lemma test_random_stuff (P1 P2 P3 : nat → uPred M) :
     ⊢ ∀ (x y : nat) a b,
       x ≡ y →
@@ -71,12 +55,6 @@ Section iris_tests.
   Context `{!invG Σ, !cinvG Σ, !na_invG Σ}.
   Implicit Types P Q R : iProp Σ.
 
-  (* Test scopes for bupd and fupd *)
-  Definition use_bupd_iProp (n : nat) : iProp Σ :=
-    □ |==> ∃ m : nat , ⌜ n = 2 ⌝.
-  Definition use_fupd_iProp (n : nat) : iProp Σ :=
-    □ |={⊤}=> ∃ m : nat , ⌜ n = 2 ⌝.
-
   Lemma test_masks  N E P Q R :
     ↑N ⊆ E →
     (True -∗ P -∗ inv N Q -∗ True -∗ R) -∗ P -∗ ▷ Q ={E}=∗ R.
-- 
GitLab