From 4fed459d89b6b3abcce8028b19af806b48a38bd7 Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Sun, 22 Mar 2026 13:16:21 +0100 Subject: Add builtin arithmetic operators MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * also allow choosing evaluator * ensures equivalence of evaluators up-to α-renaming * checks server accepts answers from challenge --- lambda-calcul/haskell/src/Minilang/App.hs | 15 ++- lambda-calcul/haskell/src/Minilang/Lambda.hs | 35 +++-- .../haskell/src/Minilang/Lambda/DeBruijn.hs | 143 +++++++++++++++++---- lambda-calcul/haskell/src/Minilang/Lambda/Eval.hs | 88 +++++++++++-- lambda-calcul/haskell/src/Minilang/REPL.hs | 35 ++++- lambda-calcul/haskell/src/Minilang/REPL/Run.hs | 16 ++- lambda-calcul/haskell/src/Minilang/REPL/Types.hs | 22 +++- lambda-calcul/haskell/src/Minilang/Server.hs | 9 +- 8 files changed, 293 insertions(+), 70 deletions(-) (limited to 'lambda-calcul/haskell/src/Minilang') diff --git a/lambda-calcul/haskell/src/Minilang/App.hs b/lambda-calcul/haskell/src/Minilang/App.hs index 3373b75..0174547 100644 --- a/lambda-calcul/haskell/src/Minilang/App.hs +++ b/lambda-calcul/haskell/src/Minilang/App.hs @@ -20,9 +20,9 @@ import Data.Text.Encoding (decodeUtf8, encodeUtf8) import Data.Time (getCurrentTime) import Minilang.API (Challenge (..), LambdaAPI, Score (..), Token (..), User (..), newToken) import Minilang.Lambda.Parser (pretty) -import Minilang.REPL (withInputs) +import Minilang.REPL (withInputs, replEnvWith) import Minilang.REPL.Purer (PurerEnv (..)) -import Minilang.REPL.Types (Command (..), Content (..), In (..), Out (..), initialREPL) +import Minilang.REPL.Types (Command (..), Content (..), Evaluator (..), In (..), Out (..), initialREPL) import Network.Wai.Application.Static (defaultFileServerSettings, staticApp) import Servant (ServerT, err400, err500, errBody, (:<|>) (..), err404) import Servant.Server (Application, Handler (..), Tagged (..)) @@ -31,15 +31,17 @@ import System.Random (StdGen) data Env = Env { gen :: TVar StdGen, users :: TVar (Map Token Score), - challenges :: [Challenge] + challenges :: [Challenge], + evaluator :: Evaluator } -makeEnv :: StdGen -> [Challenge] -> IO Env -makeEnv gen challenges = +makeEnv :: StdGen -> [Challenge] -> Evaluator -> IO Env +makeEnv gen challenges ev = Env <$> newTVarIO gen <*> newTVarIO mempty <*> pure challenges + <*> pure ev newtype AppM a = AppM {runAppM :: ReaderT Env IO a} deriving newtype (Functor, Applicative, Monad, MonadIO, MonadReader Env) @@ -147,7 +149,8 @@ postAnswer Nothing _ = liftIO $ throwM $ err400 {errBody = "Missing token"} postAnswer (Just token) expected = do checkUserToken token Challenge {expr} <- getCurrentChallenge token - let PurerEnv {outputs} = withInputs initialREPL [Com (Load (Data expr))] + ev <- asks evaluator + let PurerEnv {outputs} = withInputs (replEnvWith ev) [Com (Load (Data expr))] result = evaluateOutputs outputs expected updateUserLastTest token result case result of diff --git a/lambda-calcul/haskell/src/Minilang/Lambda.hs b/lambda-calcul/haskell/src/Minilang/Lambda.hs index ff636ce..fbaf35d 100644 --- a/lambda-calcul/haskell/src/Minilang/Lambda.hs +++ b/lambda-calcul/haskell/src/Minilang/Lambda.hs @@ -1,24 +1,26 @@ module Minilang.Lambda where import Data.Bifunctor (second) -import Minilang.Lambda.DeBruijn (eval, eval', fromDeBruijn, toDeBruijn) -import Minilang.Lambda.Eval (Env, Term) +import Minilang.Lambda.DeBruijn (builtinDeBruijnEnv, eval', fromDeBruijn, toDeBruijn) +import Minilang.Lambda.Eval (Env, Term, builtinEnvValue) +import qualified Minilang.Lambda.Eval as Eval import Minilang.Lambda.Infer (Context, TypeError, extendContext, infer) import Minilang.Lambda.Parser (AST (..), desugar) import Minilang.Lambda.Unify (Type (..)) -import Minilang.REPL.Types (Language (..)) +import Minilang.REPL.Types (Evaluator (..), Language (..)) -- | Top-level evaluator -- Load a list of expressions into given `Env` and `Context`, returning an extended -- `Env` and `Context` with declarations bound and the list of evaluated top-level -- terms along with their types. loadProgram :: + Evaluator -> Language -> Env -> Context -> [AST] -> Either TypeError ([(Term, Type)], Env, Context) -loadProgram language env context exprs = +loadProgram evaluator language env context exprs = fmap (\(res, e, c) -> (reverse res, e, c)) result where result = @@ -38,7 +40,7 @@ loadProgram language env context exprs = exprs runExpr language (Def ident body) env context = - let term = evalInEnv env body + let term = evalInEnvWith evaluator env body in case language of Typed -> case infer term of @@ -48,7 +50,7 @@ loadProgram language env context exprs = Untyped -> Right (Nothing, (ident, term) : env, context) runExpr language expr env context = - let v = evalInEnv env expr + let v = evalInEnvWith evaluator env expr in case language of Typed -> case infer v of @@ -58,8 +60,25 @@ loadProgram language env context exprs = Untyped -> Right (Just (v, TyVar ""), env, context) +-- | Evaluate an 'AST' in the given 'Env' using the De Bruijn CBV evaluator. +-- This is the default evaluator used by the server and REPL. evalInEnv :: Env -> AST -> Term -evalInEnv env expr = +evalInEnv = evalInEnvWith DeBruijn + +-- | Evaluate an 'AST' using the selected 'Evaluator'. +evalInEnvWith :: Evaluator -> Env -> AST -> Term +evalInEnvWith DeBruijn env expr = let term = desugar expr - env' = second toDeBruijn <$> env + -- User-defined bindings take precedence over builtins (rightmost wins + -- in a left-to-right lookup, so put user env first). + env' = (second toDeBruijn <$> env) ++ builtinDeBruijnEnv in fromDeBruijn $ eval' env' (toDeBruijn term) +evalInEnvWith NbE env expr = + let term = desugar expr + -- Build an EnvValue from the user Env by evaluating each binding's + -- Term in the accumulated value env (builtins always available at the + -- bottom). foldl builds left-to-right so earlier bindings are visible + -- when evaluating later ones. + envV = foldl addBinding builtinEnvValue env + addBinding acc (name, t) = (name, Eval.eval acc t) : acc + in Eval.readBack (Eval.eval envV term) 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 diff --git a/lambda-calcul/haskell/src/Minilang/REPL.hs b/lambda-calcul/haskell/src/Minilang/REPL.hs index a8d3c77..7da2042 100644 --- a/lambda-calcul/haskell/src/Minilang/REPL.hs +++ b/lambda-calcul/haskell/src/Minilang/REPL.hs @@ -23,6 +23,8 @@ import Minilang.REPL.Pure import Minilang.REPL.Purer import Minilang.REPL.Run import Minilang.REPL.Types +import System.Environment (lookupEnv) +import Text.Read (readMaybe) import System.Console.Haskeline ( defaultBehavior, defaultSettings, @@ -30,13 +32,32 @@ import System.Console.Haskeline runInputTBehavior, setComplete, ) -import System.IO (Handle) +import System.IO (Handle, stderr) + +-- | Read the evaluator selection from the @MINILANG_EVAL@ environment variable. +-- Returns 'DeBruijn' when the variable is absent or unrecognised. +evaluatorFromEnv :: IO Evaluator +evaluatorFromEnv = + lookupEnv "MINILANG_EVAL" >>= \case + Nothing -> pure DeBruijn + Just raw -> case readMaybe raw of + Just ev -> pure ev + Nothing -> do + Text.hPutStrLn stderr $ + "Warning: unknown MINILANG_EVAL value " <> Text.pack (show raw) + <> ", falling back to DeBruijn" + pure DeBruijn + +-- | Build the initial 'REPLEnv' using the given 'Evaluator'. +replEnvWith :: Evaluator -> REPLEnv +replEnvWith ev = initialREPL { evaluator = ev } -- * Haskeline REPL -withTerminal :: IO () -withTerminal = - runInputTBehavior defaultBehavior settings $ evalStateT (runHaskeline runREPL) initialREPL +withTerminal :: Evaluator -> IO () +withTerminal ev = + runInputTBehavior defaultBehavior settings $ + evalStateT (runHaskeline runREPL) (replEnvWith ev) where settings = setComplete completion $ defaultSettings {historyFile = Just "~/.minilang.history"} @@ -50,12 +71,12 @@ withHandles hin hout = evalStateT (runConsole runREPL) (IOEnv hin hout initialREPL) -- | Simple IO REPL, used to evaluate programs from stdin or file loading -withIO :: Handle -> Handle -> IO () -withIO hin hout = do +withIO :: Evaluator -> Handle -> Handle -> IO () +withIO ev hin hout = do programText <- parseProgram <$> Text.hGetContents hin case programText of Left err -> Text.hPutStrLn hout (Text.pack (show err)) - Right prog -> case loadProgram Untyped newEnv newContext prog of + Right prog -> case loadProgram ev Untyped newEnv newContext prog of Right (results, _, _) -> mapM_ (Text.hPutStrLn hout . render) results Left err -> Text.hPutStrLn hout (Text.pack $ show err) where diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Run.hs b/lambda-calcul/haskell/src/Minilang/REPL/Run.hs index 8b9b844..26f3cad 100644 --- a/lambda-calcul/haskell/src/Minilang/REPL/Run.hs +++ b/lambda-calcul/haskell/src/Minilang/REPL/Run.hs @@ -8,7 +8,7 @@ module Minilang.REPL.Run where import Control.Monad.Catch import Data.Text hiding (replicate) -import Minilang.Lambda (loadProgram, evalInEnv) +import Minilang.Lambda (loadProgram, evalInEnvWith) import Minilang.Lambda.Eval (newEnv) import Minilang.Lambda.Infer (extendContext, infer, newContext) import qualified Minilang.Lambda.Infer as Infer @@ -34,11 +34,11 @@ handleUserInput :: Text -> m () handleUserInput txt = do - repl@REPLEnv {language, env, context} <- getEnv + repl@REPLEnv {language, evaluator, env, context} <- getEnv case parse txt of Left err -> output (Msg $ pack $ show err) Right (Def ident body) -> do - let v = evalInEnv env body + let v = evalInEnvWith evaluator env body case language of Typed -> case infer v of @@ -54,7 +54,7 @@ handleUserInput txt = do setEnv $ repl {env = (ident, v) : env} output (Defined ident (TyVar "")) Right expr -> do - let v = evalInEnv env expr + let v = evalInEnvWith evaluator env expr ast = resugar v case language of Typed -> @@ -86,6 +86,10 @@ handleCommand (Set (SelectLanguage lang)) = getEnv >>= \e -> setEnv (e {language = lang}) >> output (Msg $ "Language set to " <> pack (show lang)) +handleCommand (Set (SelectEvaluator ev)) = + getEnv >>= \e -> + setEnv (e {evaluator = ev}) + >> output (Msg $ "Evaluator set to " <> pack (show ev)) handleCommand Help = output (Msg helpText) @@ -94,11 +98,11 @@ loadProgramInEnv :: Text -> m () loadProgramInEnv prog = do - repl@REPLEnv {env, context, language} <- getEnv + repl@REPLEnv {env, context, language, evaluator} <- getEnv case parseProgram prog of Left err -> output (Msg $ pack $ show err) Right exprs -> do - case loadProgram language env context exprs of + case loadProgram evaluator language env context exprs of Left typeError -> output (Msg $ pack $ show typeError) Right (results, env', context') -> do setEnv (repl {env = env', context = context'}) diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Types.hs b/lambda-calcul/haskell/src/Minilang/REPL/Types.hs index baa59ff..0b0472e 100644 --- a/lambda-calcul/haskell/src/Minilang/REPL/Types.hs +++ b/lambda-calcul/haskell/src/Minilang/REPL/Types.hs @@ -49,11 +49,12 @@ data REPLEnv = REPLEnv curIndent :: Int, stepTypeCheck :: Bool, debugParser :: Bool, - language :: Language + language :: Language, + evaluator :: Evaluator } initialREPL :: REPLEnv -initialREPL = REPLEnv newEnv newContext 0 False False Untyped +initialREPL = REPLEnv newEnv newContext 0 False False Untyped DeBruijn -- | Input data In @@ -87,11 +88,22 @@ data Flag = StepTypeChecker Bool | DebugParser Bool | SelectLanguage Language + | SelectEvaluator Evaluator deriving (Eq, Show, Generic, ToJSON, FromJSON) data Language = Untyped | Typed deriving (Eq, Show, Read, Generic, ToJSON, FromJSON) +-- | Which reduction strategy to use. +-- +-- * 'DeBruijn' — call-by-value head reduction on De Bruijn-indexed terms +-- (the original evaluator). +-- * 'NbE' — Normalisation by Evaluation: eval to a 'Value' semantic domain, +-- then read back to a 'Term'. Reduces under lambda binders and therefore +-- produces fully-normalised terms. +data Evaluator = DeBruijn | NbE + deriving (Eq, Show, Read, Generic, ToJSON, FromJSON) + -- | "Parse" given `Text` into some input for the REPL interpret :: Text -> In @@ -113,6 +125,10 @@ interpret (unpack -> (':' : 'l' : 'a' : 'n' : 'g' : ' ' : lang)) = case readMaybe lang of Nothing -> Com Help Just l -> Com $ Set $ SelectLanguage l +interpret (unpack -> (':' : 'e' : 'v' : 'a' : 'l' : ' ' : ev)) = + case readMaybe ev of + Nothing -> Com Help + Just e -> Com $ Set $ SelectEvaluator e interpret t = In t helpText :: Text @@ -128,6 +144,8 @@ helpText = " :set