Add builtin arithmetic operators

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

2 files changed, 194 insertions, 37 deletions

diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs b/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs
index 1e85ca6..1d2f9e8 100644
--- a/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs
+++ b/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs
@@ -3,6 +3,7 @@
 module Minilang.Lambda.DeBruijn where
 
 import Data.List (elemIndex)
+import qualified Data.Map.Strict as Map
 import Data.Text (Text)
 import qualified Data.Text
 import Minilang.Lambda.Eval (Term)
@@ -11,6 +12,7 @@ import qualified Minilang.Lambda.Eval as Eval
 data DeBruijn ann
   = FV Text
   | FNum Int
+  | FBuiltin Text          -- ^ a fully-applied or partial built-in operator
   | Var ann Int
   | Lam ann (DeBruijn ann)
   | App (DeBruijn ann) (DeBruijn ann)
@@ -21,13 +23,21 @@ type Env ann = [(Text, DeBruijn ann)]
 newEnv :: Env ann
 newEnv = []
 
+-- | An environment pre-seeded with every built-in operator name.
+-- Each entry maps the name to an 'FBuiltin' node so that 'eval\'' can
+-- recognise and reduce applications of those names.
+builtinDeBruijnEnv :: Env ann
+builtinDeBruijnEnv =
+  map (\name -> (name, FBuiltin name)) (Map.keys Eval.builtinArity)
+
 fromDeBruijn :: DeBruijn Text -> Term
 fromDeBruijn = \case
-  FV x -> Eval.Var x
-  FNum n -> Eval.Num n
-  Var s _ -> Eval.Var s
-  Lam s body -> Eval.Lam s (fromDeBruijn body)
-  App f a -> Eval.App (fromDeBruijn f) (fromDeBruijn a)
+  FV x        -> Eval.Var x
+  FNum n      -> Eval.Num n
+  FBuiltin b  -> Eval.Var b        -- reads back as a Var; eval recognises it
+  Var s _     -> Eval.Var s
+  Lam s body  -> Eval.Lam s (fromDeBruijn body)
+  App f a     -> Eval.App (fromDeBruijn f) (fromDeBruijn a)
 
 -- Convert a term with named variables to De Bruijn indices
 toDeBruijn :: Term -> DeBruijn Text
@@ -36,7 +46,7 @@ toDeBruijn term = go term []
     go (Eval.Var x) env =
       case elemIndex x env of
         Just idx -> Var x idx
-        Nothing -> FV x
+        Nothing  -> FV x
     go (Eval.Lam x body) env =
       Lam x (go body (x : env))
     go (Eval.App f a) env =
@@ -48,40 +58,119 @@ eval :: DeBruijn ann -> DeBruijn ann
 eval (App f a) =
   case eval f of
     Lam _ body -> eval (substitute [] 0 a body)
-    f' -> App f' a
+    f'         -> App f' a
 eval term = term
 
-eval' :: (Show ann, Eq ann) => Env ann -> DeBruijn ann -> DeBruijn ann
-eval' env (FV v) = case lookup v env of
-  Just term -> term
-  Nothing -> FV v
-eval' env (App f a) =
-  case eval' env f of
-    Lam _ body -> eval' env (substitute env 0 a body)
-    f' -> if f' /= f
-          then eval' env $ App f' a
-          else App f' a
-eval' _ term = term
+eval' :: Env Text -> DeBruijn Text -> DeBruijn Text
+eval' env = \case
+  FV v -> case lookup v env of
+    Just term -> term
+    Nothing   -> FV v
+  FBuiltin b -> FBuiltin b
+  App f a ->
+    let f' = eval' env f
+        a' = eval' env a
+    in case f' of
+      -- Beta-reduction
+      Lam _ body -> eval' env (substitute env 0 a' body)
+      -- Built-in: collect arguments and reduce when saturated
+      FBuiltin b -> evalBuiltin env b [a']
+      -- Left-spine is itself a partial builtin application
+      App g arg ->
+        case collectBuiltin (App g arg) of
+          Just (b, accumulated) -> evalBuiltin env b (accumulated ++ [a'])
+          Nothing ->
+            let applied = App f' a'
+            in if applied /= App f a
+               then eval' env applied
+               else applied
+      f'' ->
+        let applied = App f'' a'
+        in if applied /= App f a
+           then eval' env applied
+           else applied
+  term -> term
+
+-- | Walk a left-spine of 'App' nodes and check whether the root is an
+-- 'FBuiltin'.  If so, return the builtin name and the already-accumulated
+-- arguments (left-to-right order).
+collectBuiltin :: DeBruijn Text -> Maybe (Text, [DeBruijn Text])
+collectBuiltin = go []
+  where
+    go acc (App f arg) = go (arg : acc) f
+    go acc (FBuiltin b) = Just (b, acc)
+    go _ _ = Nothing
+
+-- | Attempt to reduce a built-in application once all required arguments
+-- are present.  Falls back to a neutral 'App' spine when the arity has not
+-- been reached yet or when the arguments are not integer literals.
+evalBuiltin :: Env Text -> Text -> [DeBruijn Text] -> DeBruijn Text
+evalBuiltin env b args =
+  case Map.lookup b Eval.builtinArity of
+    Nothing -> rebuild (FBuiltin b) args   -- unknown builtin; leave as-is
+    Just ar
+      | length args < ar ->
+          -- Still partial: return the spine as-is for now
+          rebuild (FBuiltin b) args
+      | length args == ar ->
+          case tryReduce b args of
+            Just result -> result
+            Nothing     -> rebuild (FBuiltin b) args
+      | otherwise ->
+          -- Over-applied: reduce with exactly `ar` args then apply the rest
+          let (sat, extra) = splitAt ar args
+          in case tryReduce b sat of
+               Just reduced -> foldl (\acc x -> eval' env (App acc x)) reduced extra
+               Nothing      -> rebuild (FBuiltin b) args
+
+-- | Church-encoded True as a DeBruijn term: lam f -> lam t -> t
+churchTrue :: DeBruijn Text
+churchTrue  = Lam "f" (Lam "t" (Var "t" 0))
+
+-- | Church-encoded False as a DeBruijn term: lam f -> lam t -> f
+churchFalse :: DeBruijn Text
+churchFalse = Lam "f" (Lam "t" (Var "f" 1))
+
+-- | Attempt a numeric reduction.  Returns 'Nothing' when either argument is
+-- not an 'FNum' (e.g. it is still a free variable).
+-- Comparison operators return Church booleans rather than integer flags.
+tryReduce :: Text -> [DeBruijn Text] -> Maybe (DeBruijn Text)
+tryReduce name args = case (name, args) of
+  ("+",   [FNum x, FNum y]) -> Just $ FNum (x + y)
+  ("-",   [FNum x, FNum y]) -> Just $ FNum (x - y)
+  ("*",   [FNum x, FNum y]) -> Just $ FNum (x * y)
+  ("div", [FNum x, FNum y]) | y /= 0 -> Just $ FNum (x `div` y)
+  ("mod", [FNum x, FNum y]) | y /= 0 -> Just $ FNum (x `mod` y)
+  ("=",   [FNum x, FNum y]) -> Just $ if x == y then churchTrue else churchFalse
+  ("<",   [FNum x, FNum y]) -> Just $ if x <  y then churchTrue else churchFalse
+  ("neg", [FNum x])         -> Just $ FNum (negate x)
+  _                         -> Nothing
+
+-- | Rebuild a left-spine application from a head and a list of arguments.
+rebuild :: DeBruijn Text -> [DeBruijn Text] -> DeBruijn Text
+rebuild = foldl App
 
 substitute :: Env ann -> Int -> DeBruijn ann -> DeBruijn ann -> DeBruijn ann
 substitute env n arg term = case term of
   FV x -> case lookup x env of
-    Just term -> term
+    Just t  -> t
     Nothing -> FV x
-  FNum _ -> term
+  FNum _     -> term
+  FBuiltin _ -> term
   Var t x
-    | x == n -> arg
+    | x == n    -> arg
     | otherwise -> Var t x
-  Lam x body -> Lam x (substitute env (n + 1) arg body)
-  App f a -> App (substitute env n arg f) (substitute env n arg a)
+  Lam x body  -> Lam x (substitute env (n + 1) arg body)
+  App f a     -> App (substitute env n arg f) (substitute env n arg a)
 
 pretty :: DeBruijn Text -> Text
 pretty = \case
-  FV x -> x
-  FNum n -> showNum n
-  Var s _ -> s
+  FV x       -> x
+  FNum n     -> showNum n
+  FBuiltin b -> b
+  Var s _    -> s
   Lam s body -> "(lam (" <> s <> ") " <> pretty body <> ")"
-  App f a -> "(" <> pretty f <> " " <> pretty a <> ")"
+  App f a    -> "(" <> pretty f <> " " <> pretty a <> ")"
 
 -- | Render an integer, using no space between '-' and digits for negative numbers.
 showNum :: Int -> Text
diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs
index 650c4bd..324c881 100644
--- a/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs
+++ b/lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs
@@ -4,6 +4,8 @@
 module Minilang.Lambda.Eval where
 
 import Data.Aeson (FromJSON, ToJSON)
+import Data.Map.Strict (Map)
+import qualified Data.Map.Strict as Map
 import Data.String (IsString (..))
 import Data.Text (Text, pack)
 import GHC.Generics (Generic)
@@ -18,7 +20,14 @@ data Term
 instance IsString Term where
   fromString = Var . pack
 
-data Value = Clos EnvValue Text Term | VNeut Neutral | VNum Int
+-- | A built-in arithmetic operator value.
+-- Carries its name, the number of arguments still needed, and the
+-- already-accumulated argument values (in order of application).
+data Value
+  = Clos EnvValue Text Term
+  | VNeut Neutral
+  | VNum Int
+  | Builtin Text Int [Value]
   deriving (Show, Read, Eq)
 
 data Neutral = NVar Text | NNum Int | NApp Neutral Value
@@ -31,15 +40,36 @@ type EnvValue = [(Text, Value)]
 newEnv :: Env
 newEnv = []
 
+-- | Arity table for every built-in operator.
+builtinArity :: Map Text Int
+builtinArity = Map.fromList
+  [ ("+",   2)
+  , ("-",   2)
+  , ("*",   2)
+  , ("div", 2)
+  , ("mod", 2)
+  , ("=",   2)
+  , ("<",   2)
+  , ("neg", 1)
+  ]
+
+-- | The set of built-in names, for fast membership testing.
+builtinNames :: Map Text Value
+builtinNames = Map.mapWithKey (\name ar -> Builtin name ar []) builtinArity
+
 normalise :: Term -> Term
-normalise term = readBack (eval [] term)
+normalise term = readBack (eval builtinEnvValue term)
+
+-- | An 'EnvValue' pre-seeded with all built-in operators.
+builtinEnvValue :: EnvValue
+builtinEnvValue = Map.toList builtinNames
 
 -- call-by-value evaluator
 -- from https://davidchristiansen.dk/tutorials/nbe/#%28part._untyped-eval%29
 eval :: EnvValue -> Term -> Value
 eval env = \case
   Var x -> case lookup x env of
-    Just term -> term
+    Just v  -> v
     Nothing -> VNeut (NVar x)
   Lam x body -> Clos env x body
   App f a ->
@@ -55,21 +85,59 @@ apply f a =
       let env' = (x, a) : closureEnv
        in eval env' body
     VNeut f' -> VNeut (NApp f' a)
-    VNum n -> VNeut (NApp (NNum n) a)
+    VNum n   -> VNeut (NApp (NNum n) a)
+    -- Last argument arrives: dispatch and reduce.
+    Builtin name 1 args -> dispatchBuiltin name (args ++ [a])
+    -- Still waiting for more arguments: accumulate.
+    Builtin name ar args -> Builtin name (ar - 1) (args ++ [a])
+
+-- | Church-encoded True: lam f t -> t
+churchTrue :: Value
+churchTrue = Clos builtinEnvValue "f" (Lam "t" (Var "t"))
+
+-- | Church-encoded False: lam f t -> f
+churchFalse :: Value
+churchFalse = Clos builtinEnvValue "f" (Lam "t" (Var "f"))
+
+-- | Reduce a fully-saturated built-in application.
+-- If the arguments are not both integers (free variables in function
+-- position), fall back to a stuck neutral term.
+-- Comparison operators (= and <) return Church booleans rather than integers.
+dispatchBuiltin :: Text -> [Value] -> Value
+dispatchBuiltin name args = case (name, args) of
+  ("+",   [VNum x, VNum y]) -> VNum (x + y)
+  ("-",   [VNum x, VNum y]) -> VNum (x - y)
+  ("*",   [VNum x, VNum y]) -> VNum (x * y)
+  ("div", [VNum x, VNum y])
+    | y /= 0   -> VNum (x `div` y)
+  ("mod", [VNum x, VNum y])
+    | y /= 0   -> VNum (x `mod` y)
+  ("=",   [VNum x, VNum y]) -> if x == y then churchTrue else churchFalse
+  ("<",   [VNum x, VNum y]) -> if x <  y then churchTrue else churchFalse
+  ("neg", [VNum x])         -> VNum (negate x)
+  -- Stuck: reconstruct a neutral application chain rooted at the builtin name.
+  _ -> foldl (\acc v -> VNeut (NApp (neutralOf acc) v)) (VNeut (NVar name)) args
+  where
+    neutralOf (VNeut n) = n
+    neutralOf v         = NApp (NVar name) v   -- shouldn't happen in practice
 
 readBack :: Value -> Term
 readBack = go []
   where
     go names = \case
       Clos env x body ->
-        let name = freshName x names
+        let name  = freshName x names
             names' = name : names
-            val' = eval ((x, VNeut (NVar name)) : env) body
+            val'  = eval ((x, VNeut (NVar name)) : env) body
          in Lam name (go names' val')
-      VNeut (NVar n) -> Var n
-      VNeut (NNum n) -> Num n
-      VNeut (NApp f a) -> App (go names (VNeut f)) (go names a)
-      VNum n -> Num n
+      VNeut (NVar n)    -> Var n
+      VNeut (NNum n)    -> Num n
+      VNeut (NApp f a)  -> App (go names (VNeut f)) (go names a)
+      VNum n            -> Num n
+      -- A partial builtin reads back as a chain of applications rooted at
+      -- the builtin name, e.g. Builtin "+" 1 [VNum 3]  →  App (Var "+") (Num 3)
+      Builtin bname _ accumulated ->
+        foldl (\acc v -> App acc (go names v)) (Var bname) accumulated
 
 freshName :: Text -> [Text] -> Text
 freshName x names