Add builtin arithmetic operators

* also allow choosing evaluator
* ensures equivalence of evaluators up-to α-renaming
* checks server accepts answers from challenge

3 files changed, 278 insertions, 7 deletions

diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs
index 85c9d6b..eaff77c 100644
--- a/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs
+++ b/lambda-calcul/haskell/test/Minilang/Lambda/DeBruijnSpec.hs
@@ -1,9 +1,9 @@
 {-# LANGUAGE TypeApplications #-}
 module Minilang.Lambda.DeBruijnSpec where
 
-import Minilang.Lambda.DeBruijn (DeBruijn (..), eval, toDeBruijn, eval')
+import Minilang.Lambda.DeBruijn (DeBruijn (..), Env, builtinDeBruijnEnv, eval, toDeBruijn, eval')
 import qualified Minilang.Lambda.Eval as Eval
-import Test.Hspec (Spec, it, shouldBe)
+import Test.Hspec (Spec, describe, it, shouldBe)
 import Data.Text (Text)
 
 spec :: Spec
@@ -21,5 +21,63 @@ spec = do
 
   it "evaluates deBruijn term in env" $ do
     let term = App (FV "z") (FV "t")
-        env = [("z", toDeBruijn $ Eval.Lam "x" (Eval.Var "x"))]
-    eval' @Text env term `shouldBe` FV "t"
+        env  = [("z", toDeBruijn $ Eval.Lam "x" (Eval.Var "x"))]
+    eval' env term `shouldBe` FV "t"
+
+  describe "built-in arithmetic" $ do
+    let benv = builtinDeBruijnEnv :: Env Text
+
+    it "(+ 3 4) reduces to FNum 7" $
+      eval' benv (App (App (FBuiltin "+") (FNum 3)) (FNum 4))
+        `shouldBe` FNum 7
+
+    it "(- 10 3) reduces to FNum 7" $
+      eval' benv (App (App (FBuiltin "-") (FNum 10)) (FNum 3))
+        `shouldBe` FNum 7
+
+    it "(* 2 5) reduces to FNum 10" $
+      eval' benv (App (App (FBuiltin "*") (FNum 2)) (FNum 5))
+        `shouldBe` FNum 10
+
+    it "(div 10 3) reduces to FNum 3" $
+      eval' benv (App (App (FBuiltin "div") (FNum 10)) (FNum 3))
+        `shouldBe` FNum 3
+
+    it "(mod 10 3) reduces to FNum 1" $
+      eval' benv (App (App (FBuiltin "mod") (FNum 10)) (FNum 3))
+        `shouldBe` FNum 1
+
+    it "(= 3 3) reduces to Church True" $
+      eval' benv (App (App (FBuiltin "=") (FNum 3)) (FNum 3))
+        `shouldBe` Lam "f" (Lam "t" (Var "t" 0))
+
+    it "(= 3 4) reduces to Church False" $
+      eval' benv (App (App (FBuiltin "=") (FNum 3)) (FNum 4))
+        `shouldBe` Lam "f" (Lam "t" (Var "f" 1))
+
+    it "(< 2 5) reduces to Church True" $
+      eval' benv (App (App (FBuiltin "<") (FNum 2)) (FNum 5))
+        `shouldBe` Lam "f" (Lam "t" (Var "t" 0))
+
+    it "(< 5 2) reduces to Church False" $
+      eval' benv (App (App (FBuiltin "<") (FNum 5)) (FNum 2))
+        `shouldBe` Lam "f" (Lam "t" (Var "f" 1))
+
+    it "(neg 7) reduces to FNum -7" $
+      eval' benv (App (FBuiltin "neg") (FNum 7))
+        `shouldBe` FNum (-7)
+
+    it "(+ 1) partial: stays as a spine without reducing" $
+      eval' benv (App (FBuiltin "+") (FNum 1))
+        `shouldBe` App (FBuiltin "+") (FNum 1)
+
+    it "(div 1 0) stays stuck" $
+      eval' benv (App (App (FBuiltin "div") (FNum 1)) (FNum 0))
+        `shouldBe` App (App (FBuiltin "div") (FNum 1)) (FNum 0)
+
+    it "(+ x 1) with free x stays stuck" $
+      eval' benv (App (App (FBuiltin "+") (FV "x")) (FNum 1))
+        `shouldBe` App (App (FBuiltin "+") (FV "x")) (FNum 1)
+
+    it "lookup of '+' in builtin env yields FBuiltin" $
+      eval' benv (FV "+") `shouldBe` FBuiltin "+"
diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
index f07b5a2..e5075f0 100644
--- a/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
+++ b/lambda-calcul/haskell/test/Minilang/Lambda/EvalSpec.hs
@@ -1,11 +1,21 @@
+{-# LANGUAGE LambdaCase #-}
 module Minilang.Lambda.EvalSpec (spec) where
 
 import Control.Concurrent (threadDelay)
 import Control.Concurrent.Async (race_)
-import Minilang.Lambda.Eval (Term (..), Value (..), eval, normalise)
-import Test.Hspec (Spec, describe, it, shouldBe)
+import Data.Aeson (eitherDecodeFileStrict)
+import Data.Text (Text, pack)
+import qualified Data.Text as Text
+import Minilang.API (Challenge (..))
+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 Minilang.Lambda.Infer (newContext)
+import Minilang.Lambda.Parser (parseProgram)
+import Minilang.REPL.Types (Evaluator (..), Language (..))
+import Test.Hspec (Spec, describe, it, runIO, shouldBe)
 import Test.Hspec.QuickCheck (prop)
-import Data.Text (pack)
 import Test.QuickCheck (NonEmptyList (..), arbitrary, forAll, (===))
 
 spec :: Spec
@@ -87,6 +97,113 @@ spec = do
           normalise (App (Num n) (Var (pack x)))
             === App (Num (n :: Int)) (Var (pack x))
 
+  describe "built-in arithmetic" $ do
+    -- Basic two-argument reductions
+    it "(+ 3 4) normalises to 7" $
+      normalise (App (App (Var "+") (Num 3)) (Num 4)) `shouldBe` Num 7
+
+    it "(- 10 3) normalises to 7" $
+      normalise (App (App (Var "-") (Num 10)) (Num 3)) `shouldBe` Num 7
+
+    it "(* 2 5) normalises to 10" $
+      normalise (App (App (Var "*") (Num 2)) (Num 5)) `shouldBe` Num 10
+
+    it "(div 10 3) normalises to 3" $
+      normalise (App (App (Var "div") (Num 10)) (Num 3)) `shouldBe` Num 3
+
+    it "(mod 10 3) normalises to 1" $
+      normalise (App (App (Var "mod") (Num 10)) (Num 3)) `shouldBe` Num 1
+
+    it "(= 3 3) normalises to Church True" $
+      normalise (App (App (Var "=") (Num 3)) (Num 3))
+        `shouldBe` Lam "f" (Lam "t" (Var "t"))
+
+    it "(= 3 4) normalises to Church False" $
+      normalise (App (App (Var "=") (Num 3)) (Num 4))
+        `shouldBe` Lam "f" (Lam "t" (Var "f"))
+
+    it "(< 2 5) normalises to Church True" $
+      normalise (App (App (Var "<") (Num 2)) (Num 5))
+        `shouldBe` Lam "f" (Lam "t" (Var "t"))
+
+    it "(< 5 2) normalises to Church False" $
+      normalise (App (App (Var "<") (Num 5)) (Num 2))
+        `shouldBe` Lam "f" (Lam "t" (Var "f"))
+
+    -- Compose with Church ite: (ite (= 3 3) (Num 1) (Num 2)) == 1
+    -- ite c t e = c e t  (True picks second arg, False picks first)
+    it "(= 3 3) composes with Church ite to select then-branch" $
+      let ite = Lam "c" (Lam "t" (Lam "e" (App (App (Var "c") (Var "e")) (Var "t"))))
+      in normalise (App (App (App ite (App (App (Var "=") (Num 3)) (Num 3))) (Num 1)) (Num 2))
+           `shouldBe` Num 1
+
+    it "(< 5 2) composes with Church ite to select else-branch" $
+      let ite = Lam "c" (Lam "t" (Lam "e" (App (App (Var "c") (Var "e")) (Var "t"))))
+      in normalise (App (App (App ite (App (App (Var "<") (Num 5)) (Num 2))) (Num 1)) (Num 2))
+           `shouldBe` Num 2
+
+    it "(neg 7) normalises to -7" $
+      normalise (App (Var "neg") (Num 7)) `shouldBe` Num (-7)
+
+    it "(neg -3) normalises to 3" $
+      normalise (App (Var "neg") (Num (-3))) `shouldBe` Num 3
+
+    -- Nested arithmetic
+    it "(* 2 (+ 1 4)) normalises to 10" $
+      normalise (App (App (Var "*") (Num 2)) (App (App (Var "+") (Num 1)) (Num 4)))
+        `shouldBe` Num 10
+
+    -- Properties
+    prop "addition is commutative" $ \x y ->
+      normalise (App (App (Var "+") (Num x)) (Num y))
+        === normalise (App (App (Var "+") (Num y)) (Num (x :: Int)))
+
+    prop "subtraction is the inverse of addition" $ \x y ->
+      normalise (App (App (Var "-") (App (App (Var "+") (Num x)) (Num y))) (Num y))
+        === Num (x :: Int)
+
+    prop "multiplication by 0 is 0" $ \x ->
+      normalise (App (App (Var "*") (Num x)) (Num 0))
+        === Num (0 :: Int)
+
+    prop "neg is its own inverse" $ \x ->
+      normalise (App (Var "neg") (App (Var "neg") (Num x)))
+        === Num (x :: Int)
+
+    -- Partial application
+    it "(+ 1) evaluates to a Builtin waiting for one more arg" $
+      eval builtinEnvValue (App (Var "+") (Num 1))
+        `shouldBe` Builtin "+" 1 [VNum 1]
+
+    it "partial builtin applied to its last arg reduces" $
+      eval builtinEnvValue (App (App (Var "+") (Num 1)) (Num 2))
+        `shouldBe` VNum 3
+
+    it "partial builtin passed through a lambda reduces when applied" $
+      normalise (App (Lam "f" (App (App (Var "f") (Num 3)) (Num 4))) (Var "+"))
+        `shouldBe` Num 7
+
+    -- Stuck / neutral cases
+    it "(+ x 1) with free x stays stuck" $
+      normalise (App (App (Var "+") (Var "x")) (Num 1))
+        `shouldBe` App (App (Var "+") (Var "x")) (Num 1)
+
+    it "(div 1 0) stays stuck" $
+      normalise (App (App (Var "div") (Num 1)) (Num 0))
+        `shouldBe` App (App (Var "div") (Num 1)) (Num 0)
+
+    it "(mod 5 0) stays stuck" $
+      normalise (App (App (Var "mod") (Num 5)) (Num 0))
+        `shouldBe` App (App (Var "mod") (Num 5)) (Num 0)
+
+  describe "evaluator equivalence on challenges" $ do
+    challenges <- runIO $
+      eitherDecodeFileStrict "challenges.json" >>= \case
+        Left err -> fail $ "Could not load challenges.json: " <> err
+        Right cs -> pure (cs :: [Challenge])
+
+    mapM_ (challengeEquivalenceTest newEnv) challenges
+
   -- describe "call-by-name eval" $ do
   --   it "evaluates 'x' as itself" $ do
   --     normalise' (Var "x") `shouldBe` Var "x"
@@ -96,6 +213,41 @@ spec = do
   --     shouldDiverge $
   --       normalise' omega
 
+-- | For a single challenge expression, parse it and run both evaluators,
+-- asserting they produce alpha-equivalent results.
+-- Alpha-equivalence is checked by converting both results to De Bruijn-indexed
+-- form (which strips variable names) before comparing.
+challengeEquivalenceTest :: Env -> Challenge -> Spec
+challengeEquivalenceTest env Challenge{level, expr} =
+  it ("level " <> show level <> ": " <> Text.unpack (Text.take 60 expr)) $
+    case parseProgram expr of
+      Left err ->
+        fail $ "Parse error for level " <> show level <> ": " <> show err
+      Right asts ->
+        let runWith ev = loadProgram ev Untyped env newContext asts
+            extractTerms (Right (terms, _, _)) = map fst terms
+            extractTerms (Left err)            = error $ "Type error: " <> show err
+            -- Convert to annotation-erased De Bruijn to compare up to
+            -- alpha-equivalence.  Both evaluators may choose different fresh
+            -- names for lambda binders (NbE normalises under binders and must
+            -- avoid capture); erasing names leaves only structure and indices.
+            toAlpha = map (eraseNames . toDeBruijn) . extractTerms
+            debruijnTerms = toAlpha (runWith DeBruijn)
+            nbeTerms      = toAlpha (runWith NbE)
+        in nbeTerms `shouldBe` debruijnTerms
+
+-- | Erase all name annotations from a 'DeBruijn' term, leaving only the
+-- structural skeleton (indices, numeric literals, free-variable names, and
+-- builtin names).  Two terms that are identical up to alpha-renaming of bound
+-- variables will be equal after erasure.
+eraseNames :: DB.DeBruijn Text -> DB.DeBruijn ()
+eraseNames (DB.FV x)       = DB.FV x
+eraseNames (DB.FNum n)     = DB.FNum n
+eraseNames (DB.FBuiltin b) = DB.FBuiltin b
+eraseNames (DB.Var _ i)    = DB.Var () i
+eraseNames (DB.Lam _ body) = DB.Lam () (eraseNames body)
+eraseNames (DB.App f a)    = DB.App (eraseNames f) (eraseNames a)
+
 shouldDiverge :: Term -> IO ()
 shouldDiverge t =
   race_
diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs
index e9cfc6b..08ec661 100644
--- a/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs
+++ b/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs
@@ -11,6 +11,7 @@ import qualified Data.Text as Text
 import Minilang.Lambda.Eval (Term (Lam))
 import qualified Minilang.Lambda.Eval as Eval
 import Minilang.Lambda.Parser (AST (..), desugar, initialChars, parse, parseProgram, pretty, restChars)
+import Minilang.Lambda.Eval (normalise)
 import Test.Hspec (Spec, describe, it, parallel, shouldBe, shouldSatisfy)
 import Test.Hspec.QuickCheck (prop)
 import Test.QuickCheck (
@@ -114,6 +115,66 @@ spec = parallel $ do
         let spaced = "- " <> Text.pack (show n)
          in parse spaced `shouldSatisfy` (/= Right (Lit (negate n)))
 
+  describe "arithmetic operators" $ do
+    -- Operator names are valid identifiers: they parse as Sym and round-trip.
+    it "parses + as a symbol" $
+      parse "+" `shouldBe` Right (Sym "+")
+
+    it "parses - as a symbol" $
+      parse "-" `shouldBe` Right (Sym "-")
+
+    it "parses * as a symbol" $
+      parse "*" `shouldBe` Right (Sym "*")
+
+    it "parses div as a symbol" $
+      parse "div" `shouldBe` Right (Sym "div")
+
+    it "parses mod as a symbol" $
+      parse "mod" `shouldBe` Right (Sym "mod")
+
+    it "parses = as a symbol" $
+      parse "=" `shouldBe` Right (Sym "=")
+
+    it "parses < as a symbol" $
+      parse "<" `shouldBe` Right (Sym "<")
+
+    it "parses neg as a symbol" $
+      parse "neg" `shouldBe` Right (Sym "neg")
+
+    -- Full expression parses and round-trips
+    it "parses (+ 3 4) and pretty-prints back" $
+      let expr = App (Sym "+") (Lit 3) [Lit 4]
+       in parse "(+ 3 4)" `shouldBe` Right expr
+
+    it "pretty (+ 3 4) round-trips through parse" $
+      let expr = App (Sym "+") (Lit 3) [Lit 4]
+       in parse (pretty expr) `shouldBe` Right expr
+
+    -- desugar of an arithmetic expression produces a normalised integer
+    it "desugar and normalise (+ 3 4) == Num 7" $
+      normalise (desugar (App (Sym "+") (Lit 3) [Lit 4])) `shouldBe` Eval.Num 7
+
+    it "desugar and normalise (* 2 (+ 1 4)) == Num 10" $
+      normalise (desugar (App (Sym "*") (Lit 2) [App (Sym "+") (Lit 1) [Lit 4]]))
+        `shouldBe` Eval.Num 10
+
+    -- Comparison operators produce Church booleans
+    it "desugar and normalise (= 3 3) == Church True" $
+      normalise (desugar (App (Sym "=") (Lit 3) [Lit 3]))
+        `shouldBe` Eval.Lam "f" (Eval.Lam "t" (Eval.Var "t"))
+
+    it "desugar and normalise (= 3 4) == Church False" $
+      normalise (desugar (App (Sym "=") (Lit 3) [Lit 4]))
+        `shouldBe` Eval.Lam "f" (Eval.Lam "t" (Eval.Var "f"))
+
+    it "desugar and normalise (< 2 5) == Church True" $
+      normalise (desugar (App (Sym "<") (Lit 2) [Lit 5]))
+        `shouldBe` Eval.Lam "f" (Eval.Lam "t" (Eval.Var "t"))
+
+    -- A partial application (missing second arg) pretty-prints as an App
+    it "pretty (+ 1) is \"(+ 1)\"" $
+      pretty (App (Sym "+") (Lit 1) []) `shouldBe` "(+ 1)"
+
   it "parses multiline program with blank lines" $ do
     let program =
           "(def id (lam (x) x))\n\