From cd2fe7cc9ff6e18f46217a98b1d08ee70264d4eb Mon Sep 17 00:00:00 2001
From: James Eversole <james@eversole.co>
Date: Thu, 7 Aug 2025 15:28:49 -0500
Subject: [PATCH] Update tests

---
 test/Spec.hs | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)

diff --git a/test/Spec.hs b/test/Spec.hs
index c3af997..e75261f 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -35,6 +35,7 @@ tests = testGroup "Tricu Tests"
   , modules
   , demos
   , decoding
+  , elimLambdaSingle
   ]
 
 lexer :: TestTree
@@ -570,3 +571,36 @@ decoding = testGroup "Decoding Tests"
       let input = ofList [ofList [ofString "nested"], ofString "string"]
       decodeResult input @?= "[[\"nested\"], \"string\"]"
   ]
+
+elimLambdaSingle :: TestTree
+elimLambdaSingle = testCase "elimLambda preserves eval, fires eta, and SDef binds" $ do
+  -- 1) eta reduction, purely structural and parsed from source
+  let [etaIn] = parseTricu "x : f x"
+      [fRef ] = parseTricu "f"
+  elimLambda etaIn @?= fRef
+
+  -- 2) SDef binds its own name and parameters
+  let [defFXY] = parseTricu "f x y : f x"
+      fv       = freeVars defFXY
+  assertBool "f should be bound in SDef" ("f" `Set.notMember` fv)
+  assertBool "x should be bound in SDef" ("x" `Set.notMember` fv)
+  assertBool "y should be bound in SDef" ("y" `Set.notMember` fv)
+
+  -- 3) semantics preserved on a small program that exercises compose and triage
+  let src =
+        unlines
+          [ "false = t"
+          , "_     = t"
+          , "true  = t t"
+          , "id    = a : a"
+          , "const = a b : a"
+          , "compose = f g x : f (g x)"
+          , "triage = leaf stem fork : t (t leaf stem) fork"
+          , "test   = triage \"Leaf\" (_ : \"Stem\") (_ _ : \"Fork\")"
+          , "main   = compose id id test"
+          ]
+      prog        = parseTricu src
+      progElim    = map elimLambda prog
+      evalBefore  = result (evalTricu Map.empty prog)
+      evalAfter   = result (evalTricu Map.empty progElim)
+  evalAfter @?= evalBefore