From 99e2ce71faa82e7b99574895e0fe24183ba9f6c3 Mon Sep 17 00:00:00 2001 From: Arnaud Bailly Date: Wed, 5 Nov 2025 12:02:23 +0100 Subject: can parse whole programs and load them --- lambda-calcul/haskell/src/Minilang/Lambda.hs | 69 +++++++++++++++------- .../haskell/src/Minilang/Lambda/DeBruijn.hs | 22 +++---- .../haskell/src/Minilang/Lambda/Parser.hs | 5 ++ lambda-calcul/haskell/src/Minilang/REPL.hs | 58 ++++++++++++------ lambda-calcul/haskell/src/Minilang/REPL/Run.hs | 12 ++-- 5 files changed, 113 insertions(+), 53 deletions(-) (limited to 'lambda-calcul/haskell/src/Minilang') diff --git a/lambda-calcul/haskell/src/Minilang/Lambda.hs b/lambda-calcul/haskell/src/Minilang/Lambda.hs index d2df56f..2372578 100644 --- a/lambda-calcul/haskell/src/Minilang/Lambda.hs +++ b/lambda-calcul/haskell/src/Minilang/Lambda.hs @@ -1,32 +1,61 @@ module Minilang.Lambda where -import Minilang.Lambda.DeBruijn (eval, fromDeBruijn, toDeBruijn) +import Data.Bifunctor (second) +import Minilang.Lambda.DeBruijn (eval, eval', fromDeBruijn, toDeBruijn) import Minilang.Lambda.Eval (Env, Term) import Minilang.Lambda.Infer (Context, TypeError, infer) -import Minilang.Lambda.Parser (AST, desugar) +import Minilang.Lambda.Parser (AST (..), desugar) import Minilang.Lambda.Unify (Type (..)) import Minilang.REPL.Types (Language (..)) -- | Top-level evaluator --- Load an AST into given `Env` and `Context`, returning an extended --- `Env` and `Context` with declarations bound +-- 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 :: Language -> - AST -> Env -> Context -> - Either TypeError (Term, Type, Env, Context) --- loadProgram (Let d r) ρ γ = do --- (ρ', γ') <- checkD 0 d ρ γ --- loadProgram r ρ' γ' -loadProgram language expr env context = - let term = desugar expr - v = fromDeBruijn $ eval (toDeBruijn term) - in case language of - Typed -> - case infer term of - Left typeError -> Left typeError - Right typ -> - Right (v, typ, env, context) - Untyped -> - Right (v, TyVar "", env, context) + [AST] -> + Either TypeError ([(Term, Type)], Env, Context) +loadProgram language env context exprs = + fmap (\(res, e, c) -> (reverse res, e, c)) result + where + result = + foldr + ( \expr acc -> + case acc of + Left typeError -> Left typeError + Right (results, env', context') -> + case runExpr language expr env' context' of + Left typeError -> Left typeError + Right (Nothing, env'', context'') -> + Right (results, env'', context'') + Right (Just res, env'', context'') -> + Right (res : results, env'', context'') + ) + (Right ([], env, context)) + exprs + + runExpr language (Def ident body) env context = + let term = desugar body + in case language of + Typed -> + case infer term of + Left typeError -> Left typeError + Right typ -> + Right (Nothing, (ident, term) : env, context) + Untyped -> + Right (Nothing, (ident, term) : env, context) + runExpr language expr env context = + let term = desugar expr + env' = second toDeBruijn <$> env + v = fromDeBruijn $ eval' env' (toDeBruijn term) + in case language of + Typed -> + case infer term of + Left typeError -> Left typeError + Right typ -> + Right (Just (v, typ), env, context) + Untyped -> + Right (Just (v, TyVar ""), env, context) diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs b/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs index 8b24f8b..de179ad 100644 --- a/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs +++ b/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs @@ -6,6 +6,7 @@ import Data.List (elemIndex) import Data.Text (Text) import Minilang.Lambda.Eval (Term) import qualified Minilang.Lambda.Eval as Eval +import Debug.Trace (trace) data DeBruijn ann = FV Text @@ -19,7 +20,6 @@ type Env ann = [(Text, DeBruijn ann)] newEnv :: Env ann newEnv = [] - fromDeBruijn :: DeBruijn Text -> Term fromDeBruijn = \case FV x -> Eval.Var x @@ -43,28 +43,30 @@ toDeBruijn term = go term [] eval :: DeBruijn ann -> DeBruijn ann eval (App f a) = case eval f of - Lam _ body -> eval (substitute 0 a body) + Lam _ body -> eval (substitute [] 0 a body) f' -> App f' a eval term = term -eval' :: Env ann -> DeBruijn ann -> DeBruijn ann +eval' :: Show 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 0 a body) - f' -> App f' a + Lam _ body -> eval' env (substitute env 0 a body) + f' -> eval' env $ App f' a eval' _ term = term -substitute :: Int -> DeBruijn ann -> DeBruijn ann -> DeBruijn ann -substitute n arg term = case term of - FV x -> FV x +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 + Nothing -> FV x Var t x | x == n -> arg | otherwise -> Var t x - Lam x body -> Lam x (substitute (n + 1) arg body) - App f a -> App (substitute n arg f) (substitute 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 diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Parser.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Parser.hs index b0f4b8f..a0cc577 100644 --- a/lambda-calcul/haskell/src/Minilang/Lambda/Parser.hs +++ b/lambda-calcul/haskell/src/Minilang/Lambda/Parser.hs @@ -67,6 +67,11 @@ pretty = \case App x y rest -> "(" <> mconcat (List.intersperse " " (pretty <$> (x : y : rest))) <> ")" Def name body -> "(def " <> name <> " " <> pretty body <> ")" +parseProgram :: Text -> Either ParseError [AST] +parseProgram input = + first (ParseError . pack . errorBundlePretty) $ + Text.Megaparsec.parse (many ast) "" input + parse :: Text -> Either ParseError AST parse = first (ParseError . pack . errorBundlePretty) . Text.Megaparsec.parse ast "" diff --git a/lambda-calcul/haskell/src/Minilang/REPL.hs b/lambda-calcul/haskell/src/Minilang/REPL.hs index a5ffce1..ae25822 100644 --- a/lambda-calcul/haskell/src/Minilang/REPL.hs +++ b/lambda-calcul/haskell/src/Minilang/REPL.hs @@ -1,59 +1,83 @@ {-# LANGUAGE DuplicateRecordFields #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeSynonymInstances #-} {-# OPTIONS_GHC "-fno-warn-orphans" #-} module Minilang.REPL where -import Control.Monad.Catch.Pure (CatchT (..)) +import Control.Monad.Catch.Pure (CatchT (..), SomeException) import Control.Monad.State import Data.Text hiding (replicate) +import qualified Data.Text as Text +import qualified Data.Text.IO as Text +import Minilang.Lambda (loadProgram) +import Minilang.Lambda.Eval (Term, newEnv) +import Minilang.Lambda.Infer (newContext) +import Minilang.Lambda.Parser (parseProgram, pretty, resugar) +import Minilang.Lambda.Unify (Type) +import qualified Minilang.Lambda.Unify as Unify import Minilang.REPL.Haskeline import Minilang.REPL.IO import Minilang.REPL.Pure import Minilang.REPL.Purer import Minilang.REPL.Run import Minilang.REPL.Types -import System.Console.Haskeline ( - defaultBehavior, +import System.Console.Haskeline + ( defaultBehavior, defaultSettings, historyFile, runInputTBehavior, setComplete, - ) + ) import System.IO (Handle) -- * Haskeline REPL withTerminal :: IO () withTerminal = - runInputTBehavior defaultBehavior settings $ evalStateT (runHaskeline runREPL) initialREPL + runInputTBehavior defaultBehavior settings $ evalStateT (runHaskeline runREPL) initialREPL where - settings = setComplete completion $ defaultSettings{historyFile = Just "~/.minilang.history"} + settings = setComplete completion $ defaultSettings {historyFile = Just "~/.minilang.history"} -- * Other REPLs -{- | Pure IO REPL - Used for testing purposes --} - --- | +-- | Pure IO REPL +-- Used for testing purposes withHandles :: - Handle -> Handle -> IO () + Handle -> Handle -> IO () withHandles hin hout = - evalStateT (runConsole runREPL) (IOEnv hin hout initialREPL) + 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 + input <- parseProgram <$> Text.hGetContents hin + case input of + Left err -> Text.hPutStrLn hout (Text.pack (show err)) + Right inputs -> case loadProgram Untyped newEnv newContext inputs of + Right (results, _, _) -> mapM_ (Text.hPutStrLn hout . render) results + Left err -> Text.hPutStrLn hout (Text.pack $ show err) + where + render :: (Term, Type) -> Text + render (term, typ) = pretty (resugar term) <> " : " <> Unify.pretty typ -- * Pure REPL withInput :: - [Text] -> [Text] + [Text] -> [Text] withInput stream = - outputText $ execState (runCatchT (runPure runREPL)) (PureEnv stream [] initialREPL) + outputText $ execState (runCatchT (runPure runREPL)) (PureEnv stream [] initialREPL) + -- * Purer REPL -- This useful for rehydrating and environment from a sequence of inputs withInputs :: - REPLEnv -> [In] -> PurerEnv + REPLEnv -> [In] -> PurerEnv withInputs initEnv stream = - execState (runCatchT (runPurer runREPL)) (PurerEnv stream [] initEnv) + execState (runCatchT (runPurer runREPL)) (PurerEnv stream [] initEnv) + +runProgram :: PurerREPL a -> PurerEnv +runProgram prog = + execState (runCatchT (runPurer prog)) (PurerEnv [] [] initialREPL) diff --git a/lambda-calcul/haskell/src/Minilang/REPL/Run.hs b/lambda-calcul/haskell/src/Minilang/REPL/Run.hs index a98ff41..bf28b23 100644 --- a/lambda-calcul/haskell/src/Minilang/REPL/Run.hs +++ b/lambda-calcul/haskell/src/Minilang/REPL/Run.hs @@ -14,7 +14,7 @@ import Minilang.Lambda.DeBruijn (eval, eval', fromDeBruijn, toDeBruijn) import Minilang.Lambda.Eval (newEnv) import Minilang.Lambda.Infer (infer, newContext) import qualified Minilang.Lambda.Infer as Infer -import Minilang.Lambda.Parser (AST (..), desugar, parse, resugar) +import Minilang.Lambda.Parser (AST (..), desugar, parse, parseProgram, resugar) import Minilang.Lambda.Unify (Type (TyVar)) import Minilang.REPL.Types @@ -95,11 +95,11 @@ loadProgramInEnv :: m () loadProgramInEnv prog = do repl@REPLEnv {env, context, language} <- getEnv - case parse prog of + case parseProgram prog of Left err -> output (Msg $ pack $ show err) - Right e -> do - case loadProgram language e env context of + Right exprs -> do + case loadProgram language env context exprs of Left typeError -> output (Msg $ pack $ show typeError) - Right (term, typ, env', context') -> do + Right (results, env', context') -> do setEnv (repl {env = env', context = context'}) - output (Evaluated (resugar term) term typ) + mapM_ (\(term, typ) -> output (Evaluated (resugar term) term typ)) results -- cgit v1.3.1