summaryrefslogtreecommitdiff
path: root/lambda-calcul/haskell
diff options
context:
space:
mode:
Diffstat (limited to 'lambda-calcul/haskell')
-rw-r--r--lambda-calcul/haskell/app/Main.hs5
-rw-r--r--lambda-calcul/haskell/src/Minilang/Lambda.hs69
-rw-r--r--lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs22
-rw-r--r--lambda-calcul/haskell/src/Minilang/Lambda/Parser.hs5
-rw-r--r--lambda-calcul/haskell/src/Minilang/REPL.hs58
-rw-r--r--lambda-calcul/haskell/src/Minilang/REPL/Run.hs12
-rw-r--r--lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs20
-rw-r--r--lambda-calcul/haskell/test/Minilang/REPL/HaskelineSpec.hs2
-rw-r--r--lambda-calcul/haskell/test/Minilang/REPLSpec.hs17
9 files changed, 152 insertions, 58 deletions
diff --git a/lambda-calcul/haskell/app/Main.hs b/lambda-calcul/haskell/app/Main.hs
index 769d2f0..6ba9321 100644
--- a/lambda-calcul/haskell/app/Main.hs
+++ b/lambda-calcul/haskell/app/Main.hs
@@ -1,5 +1,4 @@
-import Minilang.IO (runEval)
-import Minilang.REPL (withTerminal)
+import Minilang.REPL (withIO, withTerminal)
import Minilang.Server (startServer, waitServer)
import Options.Applicative
import System.IO (stdin, stdout)
@@ -58,5 +57,5 @@ main = do
hasTty <- queryTerminal stdInput
if hasTty
then withTerminal
- else runEval stdin stdout
+ else withIO stdin stdout
Server -> startServer serverPort >>= waitServer
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
diff --git a/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs b/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs
index e6f05b9..932eff6 100644
--- a/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs
+++ b/lambda-calcul/haskell/test/Minilang/Lambda/ParserSpec.hs
@@ -10,7 +10,7 @@ import Data.Text (Text, pack)
import qualified Data.Text as Text
import Minilang.Lambda.Eval (Term (Lam))
import qualified Minilang.Lambda.Eval as Eval
-import Minilang.Lambda.Parser (AST (..), desugar, initialChars, parse, pretty, restChars)
+import Minilang.Lambda.Parser (AST (..), desugar, initialChars, parse, parseProgram, pretty, restChars)
import Test.Hspec (Spec, it, parallel, shouldBe, shouldSatisfy)
import Test.Hspec.QuickCheck (prop)
import Test.QuickCheck
@@ -103,6 +103,24 @@ spec = parallel $ do
let text = pretty ast
in parse text `shouldBe` Right ast
+ it "parses multiline program with blank lines" $ do
+ let program =
+ "(def id (lam (x) x))\n\
+ \\n\
+ \(def const (lam (x y) x))\n\
+ \(def apply (lam (f x) (f x)))\n\
+ \(apply id const)"
+ expected =
+ [ Def "id" (Abs ["x"] (Sym "x")),
+ Def "const" (Abs ["x", "y"] (Sym "x")),
+ Def "apply" (Abs ["f", "x"] (App (Sym "f") (Sym "x") [])),
+ App
+ (Sym "apply")
+ (Sym "id")
+ [Sym "const"]
+ ]
+ parseProgram program `shouldBe` Right expected
+
spine :: AST -> Int
spine = \case
App x _ rest -> 1 + spine x + length rest
diff --git a/lambda-calcul/haskell/test/Minilang/REPL/HaskelineSpec.hs b/lambda-calcul/haskell/test/Minilang/REPL/HaskelineSpec.hs
index 1b0f600..1cc1d09 100644
--- a/lambda-calcul/haskell/test/Minilang/REPL/HaskelineSpec.hs
+++ b/lambda-calcul/haskell/test/Minilang/REPL/HaskelineSpec.hs
@@ -26,7 +26,7 @@ spec = parallel $ describe "MiniLang Haskeline REPL" $ describe "Completion" $ d
it "returns list of files when input ':load' " $
sort . fmap replacement . snd <$> completion ("daol:", "")
- `shouldReturn` [":load bool.lisp", ":load fac.lisp"]
+ `shouldReturn` [":load bool-prog.lisp", ":load bool.lisp", ":load fac.lisp"]
it "returns filtered list of files when input ':load xxx' " $
fmap replacement . snd <$> completion ("f daol:", "")
diff --git a/lambda-calcul/haskell/test/Minilang/REPLSpec.hs b/lambda-calcul/haskell/test/Minilang/REPLSpec.hs
index 861c24c..aa73b69 100644
--- a/lambda-calcul/haskell/test/Minilang/REPLSpec.hs
+++ b/lambda-calcul/haskell/test/Minilang/REPLSpec.hs
@@ -1,8 +1,15 @@
module Minilang.REPLSpec where
import Control.Exception (bracket)
+import Data.Either (isRight)
import Data.Text.IO
+import Minilang.Lambda.Eval (Term (Lam, Var))
+import Minilang.Lambda.Parser (AST (..))
+import Minilang.Lambda.Unify (Type (TyVar))
import Minilang.REPL
+import Minilang.REPL.Purer (PurerEnv (..))
+import Minilang.REPL.Run (loadProgramInEnv)
+import Minilang.REPL.Types (Out (Evaluated))
import System.Directory (getTemporaryDirectory, removeFile)
import System.FilePath ((<.>), (</>))
import System.IO (IOMode (..), hClose, withFile)
@@ -83,6 +90,16 @@ spec = parallel $
"REPLError \"cannot load file foo in Pure interpreter\""
]
+ -- it "can load 'bool-prog.lisp'" $ do
+ -- boolProg <- readFile "bool-prog.lisp"
+ -- let PurerEnv{outputs} = runProgram (loadProgramInEnv boolProg)
+ -- outputs `shouldBe` []
+
+ it "can load 'bool.lisp'" $ do
+ boolProg <- readFile "bool.lisp"
+ let PurerEnv {outputs} = runProgram (loadProgramInEnv boolProg)
+ outputs `shouldBe` [Evaluated (Abs ["f", "t"] (Sym "f")) (Lam "f" (Lam "t" (Var "f"))) (TyVar "<?>")]
+
around withTempFile $
it "evaluates single MiniLang term read from IO" $ \fileName -> do
let outputFileName = fileName <> ".out"
generated by cgit v1.3.1 (git 2.54.0) at 2026-10-24 04:21:18 +0000