Commit f71e526a authored by Ralf Jung's avatar Ralf Jung

move tests to their own files

parent eec1486d
......@@ -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
......@@ -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. *)
......
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 Σ. *)
......
......@@ -2,4 +2,3 @@ Require Export barrier.heap_lang.
Require Import iris.parameter.
Definition Σ := IParamConst heap_lang unitRA.
Print Assumptions Σ.
(** 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.
......@@ -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.
(** 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.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment