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.