From ba61dfd69504ec6263a9dee9931d93adeb6f3142 Mon Sep 17 00:00:00 2001
From: Rutger Broekhoff
Date: Mon, 7 Jul 2025 21:52:08 +0200
Subject: Initialize repository

---
 theories/evallang/tests.v | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)
 create mode 100644 theories/evallang/tests.v

(limited to 'theories/evallang/tests.v')

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.
-- 
cgit v1.2.3