Add builtin arithmetic operators

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

1 files changed, 116 insertions, 27 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