Initialize repository

1 files changed, 33 insertions, 0 deletions

diff --git a/theories/evallang/tests.v b/theories/evallang/tests.v
new file mode 100644
index 0000000..eaba8a0
--- /dev/null
+++ b/theories/evallang/tests.v
@@ -0,0 +1,33 @@
+From mininix Require Export evallang.interp.
+From stdpp Require Import options.
+
+Import evallang.
+
+Definition interp' (n : nat) (s : string) : res val :=
+  interp n ∅ (EEval ∅ (EString s)).
+
+Lemma test_1_a : interp' 1000 ("(x: x) ""s""") = mret (VString "s").
+Proof. by vm_compute. Qed.
+Lemma test_1_b : interp' 1000 ("(""x"": x) ""s""") = mret (VString "s").
+Proof. by vm_compute. Qed.
+Lemma test_1_c : interp' 1000 ("((y:y) ""x"": x) ""s""") = mret (VString "s").
+Proof. by vm_compute. Qed.
+Lemma test_1_d : interp' 1000 ("(((y:y) ""x""): x) ""s""") = mret (VString "s").
+Proof. by vm_compute. Qed.
+
+Lemma test_2 : interp' 1000 ("(x: y: eval! y) ""s"" ""x""") = mret (VString "s").
+Proof. by vm_compute. Qed.
+
+Lemma test_3 : interp' 1000 ("eval! ""x: x"" ""s""") = mret (VString "s").
+Proof. by vm_compute. Qed.
+
+Lemma test_4_a :
+  interp' 1000 ("(x: y: eval! y) ""s"" ""x""") = mret (VString "s").
+Proof. by vm_compute. Qed.
+Lemma test_4_b :
+  interp' 1000 ("eval! ""(x: y: eval! y) \""s\"" \""x\""""") = mret (VString "s").
+Proof. by vm_compute. Qed.
+
+Lemma test_5 :
+  interp' 1000 ("(x: y: eval! ""x: x"" (eval! y)) ""s"" ""x""") = mret (VString "s").
+Proof. by vm_compute. Qed.