From f71e526a249c7096308de27fba6629ec8b6a7de3 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Wed, 27 Jan 2016 09:11:06 +0100
Subject: [PATCH] move tests to their own files

---
 _CoqProject         |  2 ++
 barrier/heap_lang.v | 24 ------------------------
 barrier/lifting.v   |  2 +-
 barrier/parameter.v |  1 -
 barrier/tests.v     | 30 ++++++++++++++++++++++++++++++
 iris/model.v        |  4 ----
 iris/tests.v        |  6 ++++++
 7 files changed, 39 insertions(+), 30 deletions(-)
 create mode 100644 barrier/tests.v
 create mode 100644 iris/tests.v

diff --git a/_CoqProject b/_CoqProject
index 22bf662a3..4abb13ff2 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -61,6 +61,8 @@ iris/pviewshifts.v
 iris/resources.v
 iris/hoare.v
 iris/parameter.v
+iris/tests.v
 barrier/heap_lang.v
 barrier/parameter.v
 barrier/lifting.v
+barrier/tests.v
diff --git a/barrier/heap_lang.v b/barrier/heap_lang.v
index 8ee263c47..9ac5c9094 100644
--- a/barrier/heap_lang.v
+++ b/barrier/heap_lang.v
@@ -405,30 +405,6 @@ Proof.
     try (destruct_conjs; eapply fill_not_value2; eassumption).
 Qed.
 
-(** Tests, making sure that stuff works. *)
-Module Tests.
-  Definition add := Op2 plus (Lit 21) (Lit 21).
-
-  Goal forall σ, prim_step add σ (Lit 42) σ None.
-  Proof.
-    apply Op2S.
-  Qed.
-
-  Definition rec := Rec (App (Var 1) (Var 0)). (* fix f x => f x *)
-  Definition rec_app := App rec (Lit 0).
-  Goal forall σ, prim_step rec_app σ rec_app σ None.
-  Proof.
-    move=>?. eapply BetaS. (* Honestly, I have no idea why this works. *)
-    reflexivity.
-  Qed.
-
-  Definition lam := Lam (Op2 plus (Var 0) (Lit 21)).
-  Goal forall σ, prim_step (App lam (Lit 21)) σ add σ None.
-  Proof.
-    move=>?. eapply BetaS. reflexivity.
-  Qed.
-End Tests.
-
 (** Instantiate the Iris language interface. This closes reduction under
     evaluation contexts.
     We could potentially make this a generic construction. *)
diff --git a/barrier/lifting.v b/barrier/lifting.v
index 3aa6c5440..7aa8401cb 100644
--- a/barrier/lifting.v
+++ b/barrier/lifting.v
@@ -1,5 +1,5 @@
+Require Import prelude.gmap iris.lifting.
 Require Export barrier.parameter.
-Require Import prelude.gmap iris.lifting barrier.heap_lang.
 Import uPred.
 
 (* TODO RJ: Figure out a way to to always use our Σ. *)
diff --git a/barrier/parameter.v b/barrier/parameter.v
index 0267acc2c..c3d21e552 100644
--- a/barrier/parameter.v
+++ b/barrier/parameter.v
@@ -2,4 +2,3 @@ Require Export barrier.heap_lang.
 Require Import iris.parameter.
 
 Definition Σ := IParamConst heap_lang unitRA.
-Print Assumptions Σ.
diff --git a/barrier/tests.v b/barrier/tests.v
new file mode 100644
index 000000000..630690101
--- /dev/null
+++ b/barrier/tests.v
@@ -0,0 +1,30 @@
+(** This file is essentially a bunch of testcases. *)
+Require Import modures.base.
+Require Import barrier.lifting.
+
+Module LangTests.
+  Definition add := Op2 plus (Lit 21) (Lit 21).
+
+  Goal ∀ σ, prim_step add σ (Lit 42) σ None.
+  Proof.
+    apply Op2S.
+  Qed.
+
+  Definition rec := Rec (App (Var 1) (Var 0)). (* fix f x => f x *)
+  Definition rec_app := App rec (Lit 0).
+  Goal ∀ σ, prim_step rec_app σ rec_app σ None.
+  Proof.
+    move=>?. eapply BetaS. (* Honestly, I have no idea why this works. *)
+    reflexivity.
+  Qed.
+
+  Definition lam := Lam (Op2 plus (Var 0) (Lit 21)).
+  Goal ∀ σ, prim_step (App lam (Lit 21)) σ add σ None.
+  Proof.
+    move=>?. eapply BetaS. reflexivity.
+  Qed.
+End LangTests.
+
+Module ParamTests.
+  Print Assumptions Σ.
+End ParamTests.
diff --git a/iris/model.v b/iris/model.v
index 61b2f1566..f6d146a2b 100644
--- a/iris/model.v
+++ b/iris/model.v
@@ -40,7 +40,3 @@ Instance iProp_fold_inj n Σ : Injective (dist n) (dist n) (@iProp_fold Σ).
 Proof. by intros X Y H; rewrite -(iProp_unfold_fold X) H iProp_unfold_fold. Qed.
 Instance iProp_unfold_inj n Σ : Injective (dist n) (dist n) (@iProp_unfold Σ).
 Proof. by intros X Y H; rewrite -(iProp_fold_unfold X) H iProp_fold_unfold. Qed.
-
-Module Test. (* Make sure we got the notations right. *)
-  Definition iResTest (Σ : iParam) (w : iWld Σ) (p : iPst Σ) (g : iGst Σ) : iRes Σ := Res w p g.
-End Test.
diff --git a/iris/tests.v b/iris/tests.v
new file mode 100644
index 000000000..77b46203c
--- /dev/null
+++ b/iris/tests.v
@@ -0,0 +1,6 @@
+(** This file tests a bunch of things. *)
+Require Import iris.model.
+
+Module ModelTest. (* Make sure we got the notations right. *)
+  Definition iResTest (Σ : iParam) (w : iWld Σ) (p : iPst Σ) (g : iGst Σ) : iRes Σ := Res w p g.
+End ModelTest.
-- 
GitLab