Add builtin arithmetic operators

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

1 files changed, 62 insertions, 4 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 "+"