1 files changed, 97 insertions, 0 deletions
diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
index e5075f0..96fff08 100644
--- a/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
+++ b/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
@@ -11,6 +11,7 @@ import Minilang.Lambda (loadProgram)
 import qualified Minilang.Lambda.DeBruijn as DB
 import Minilang.Lambda.DeBruijn (toDeBruijn)
 import Minilang.Lambda.Eval (Env, Term (..), Value (..), eval, normalise, builtinEnvValue, newEnv)
+import qualified Data.Text as Text
 import Minilang.Lambda.Infer (newContext)
 import Minilang.Lambda.Parser (parseProgram)
 import Minilang.REPL.Types (Evaluator (..), Language (..))
@@ -196,6 +197,101 @@ spec = do
       normalise (App (App (Var "mod") (Num 5)) (Num 0))
         `shouldBe` App (App (Var "mod") (Num 5)) (Num 0)
 
+  describe "string literals and builtins" $ do
+    -- Self-evaluation
+    it "string literal evaluates to itself" $
+      normalise (Str "hello") `shouldBe` Str "hello"
+
+    it "empty string evaluates to itself" $
+      normalise (Str "") `shouldBe` Str ""
+
+    prop "any string literal normalises to itself" $ \s ->
+      normalise (Str (Text.pack s)) === Str (Text.pack s)
+
+    -- eval produces VStr
+    prop "eval of a string literal produces VStr" $ \s ->
+      eval [] (Str (Text.pack s)) === VStr (Text.pack s)
+
+    -- String in function position is stuck
+    it "string in function position produces a stuck application" $
+      normalise (App (Str "oops") (Var "x"))
+        `shouldBe` App (Str "oops") (Var "x")
+
+    -- str-concat
+    it "(str-concat \"foo\" \"bar\") == \"foobar\"" $
+      normalise (App (App (Var "str-concat") (Str "foo")) (Str "bar"))
+        `shouldBe` Str "foobar"
+
+    it "(str-concat \"\" \"abc\") == \"abc\"" $
+      normalise (App (App (Var "str-concat") (Str "")) (Str "abc"))
+        `shouldBe` Str "abc"
+
+    prop "str-concat is associative" $ \a b c ->
+      let s x = Str (Text.pack x)
+          cat x y = App (App (Var "str-concat") x) y
+      in normalise (cat (cat (s a) (s b)) (s c))
+           === normalise (cat (s a) (cat (s b) (s c)))
+
+    -- str-length
+    it "(str-length \"hello\") == 5" $
+      normalise (App (Var "str-length") (Str "hello")) `shouldBe` Num 5
+
+    it "(str-length \"\") == 0" $
+      normalise (App (Var "str-length") (Str "")) `shouldBe` Num 0
+
+    prop "str-length of concat equals sum of lengths" $ \a b ->
+      let sa = Text.pack a; sb = Text.pack b
+      in normalise (App (Var "str-length") (App (App (Var "str-concat") (Str sa)) (Str sb)))
+           === normalise (App (App (Var "+") (App (Var "str-length") (Str sa)))
+                                             (App (Var "str-length") (Str sb)))
+
+    -- str-slice
+    it "(str-slice 1 3 \"abcde\") == \"bc\"" $
+      normalise (App (App (App (Var "str-slice") (Num 1)) (Num 3)) (Str "abcde"))
+        `shouldBe` Str "bc"
+
+    it "(str-slice 0 0 \"abc\") == \"\"" $
+      normalise (App (App (App (Var "str-slice") (Num 0)) (Num 0)) (Str "abc"))
+        `shouldBe` Str ""
+
+    -- str= (Church booleans)
+    it "(str= \"abc\" \"abc\") == Church True" $
+      normalise (App (App (Var "str=") (Str "abc")) (Str "abc"))
+        `shouldBe` Lam "f" (Lam "t" (Var "t"))
+
+    it "(str= \"abc\" \"xyz\") == Church False" $
+      normalise (App (App (Var "str=") (Str "abc")) (Str "xyz"))
+        `shouldBe` Lam "f" (Lam "t" (Var "f"))
+
+    prop "str= is reflexive" $ \s ->
+      normalise (App (App (Var "str=") (Str (Text.pack s))) (Str (Text.pack s)))
+        === Lam "f" (Lam "t" (Var "t"))
+
+    -- str<
+    it "(str< \"abc\" \"abd\") == Church True" $
+      normalise (App (App (Var "str<") (Str "abc")) (Str "abd"))
+        `shouldBe` Lam "f" (Lam "t" (Var "t"))
+
+    it "(str< \"b\" \"a\") == Church False" $
+      normalise (App (App (Var "str<") (Str "b")) (Str "a"))
+        `shouldBe` Lam "f" (Lam "t" (Var "f"))
+
+    -- Partial application
+    it "(str-concat \"hello\") is partial" $
+      eval builtinEnvValue (App (Var "str-concat") (Str "hello"))
+        `shouldBe` Builtin "str-concat" 1 [VStr "hello"]
+
+    -- Stuck: free variable argument
+    it "(str-concat x \"bar\") with free x stays stuck" $
+      normalise (App (App (Var "str-concat") (Var "x")) (Str "bar"))
+        `shouldBe` App (App (Var "str-concat") (Var "x")) (Str "bar")
+
+    -- Higher-order: pass builtin as function
+    it "str-concat passed as higher-order argument works" $
+      normalise (App (Lam "f" (App (App (Var "f") (Str "hello")) (Str " world")))
+                     (Var "str-concat"))
+        `shouldBe` Str "hello world"
+
   describe "evaluator equivalence on challenges" $ do
     challenges <- runIO $
       eitherDecodeFileStrict "challenges.json" >>= \case
@@ -243,6 +339,7 @@ challengeEquivalenceTest env Challenge{level, expr} =
 eraseNames :: DB.DeBruijn Text -> DB.DeBruijn ()
 eraseNames (DB.FV x)       = DB.FV x
 eraseNames (DB.FNum n)     = DB.FNum n
+eraseNames (DB.FStr s)     = DB.FStr s
 eraseNames (DB.FBuiltin b) = DB.FBuiltin b
 eraseNames (DB.Var _ i)    = DB.Var () i
 eraseNames (DB.Lam _ body) = DB.Lam () (eraseNames body)