From a543981b67d59f7e34d4f3e4adaf288da40d14b3 Mon Sep 17 00:00:00 2001 From: James Martin Date: Tue, 16 Mar 2021 17:19:50 -0700 Subject: [PATCH] Combine expression representations using the 'trees that grow' design pattern. Trees that grow introduces a lot of boilerplate but is bound to be essentially necessary when I add in the type checker and all sorts of builtin data types. (I know this because I already *implemented* those things; it's mostly a matter of trying to merge it all into this codebase). Accomplishing this also involved restructuring the project and rewriting a few algorithms in the process, but those changes are fundamentally intwined with this one. --- app/Main.hs | 21 ++- package.yaml | 15 +- src/Data/Stream.hs | 12 +- src/LambdaCalculus.hs | 162 ++--------------- src/LambdaCalculus/Evaluator.hs | 171 ++++++++++++++++++ src/LambdaCalculus/Evaluator/Base.hs | 52 ++++++ .../{ => Evaluator}/Continuation.hs | 20 +- src/LambdaCalculus/Expression.hs | 117 +++--------- src/LambdaCalculus/Expression/Base.hs | 166 +++++++++++++++++ src/LambdaCalculus/Parser/AbstractSyntax.hs | 96 ---------- src/LambdaCalculus/Syntax.hs | 7 + src/LambdaCalculus/Syntax/Base.hs | 66 +++++++ src/LambdaCalculus/{ => Syntax}/Parser.hs | 46 ++--- src/LambdaCalculus/Syntax/Printer.hs | 63 +++++++ stack.yaml | 2 +- stack.yaml.lock | 8 +- test/Spec.hs | 81 +++++---- 17 files changed, 675 insertions(+), 430 deletions(-) create mode 100644 src/LambdaCalculus/Evaluator.hs create mode 100644 src/LambdaCalculus/Evaluator/Base.hs rename src/LambdaCalculus/{ => Evaluator}/Continuation.hs (54%) create mode 100644 src/LambdaCalculus/Expression/Base.hs delete mode 100644 src/LambdaCalculus/Parser/AbstractSyntax.hs create mode 100644 src/LambdaCalculus/Syntax.hs create mode 100644 src/LambdaCalculus/Syntax/Base.hs rename src/LambdaCalculus/{ => Syntax}/Parser.hs (59%) create mode 100644 src/LambdaCalculus/Syntax/Printer.hs diff --git a/app/Main.hs b/app/Main.hs index e2ffc04..cd99939 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -1,19 +1,22 @@ module Main (main) where +import LambdaCalculus + import Control.Monad (forever) -import Data.Text -import Data.Text.IO qualified as TIO -import LambdaCalculus (eval) -import LambdaCalculus.Parser (parseExpression) +import Data.Text (pack) +import Data.Text.IO +import Prelude hiding (putStr, putStrLn, getLine) import System.IO (hFlush, stdout) prompt :: Text -> IO Text prompt text = do - TIO.putStr text + putStr text hFlush stdout - TIO.getLine + getLine main :: IO () -main = forever $ parseExpression <$> prompt ">> " >>= \case - Left parseError -> putStrLn $ "Parse error: " ++ show parseError - Right expr -> print $ eval expr +main = forever $ parseEval <$> prompt ">> " >>= \case + Left parseError -> putStrLn $ "Parse error: " <> pack (show parseError) + -- TODO: Support choosing which version to use at runtime. + Right expr -> putStrLn $ unparseEval $ eval expr + --Right expr -> mapM_ (putStrLn . unparseEval) $ snd $ traceEval expr diff --git a/package.yaml b/package.yaml index f83cd1d..60a2efd 100644 --- a/package.yaml +++ b/package.yaml @@ -14,18 +14,25 @@ extra-source-files: default-extensions: - BlockArguments +- DefaultSignatures +- EmptyCase +- EmptyDataDeriving - FlexibleContexts +- FlexibleInstances - ImportQualifiedPost - LambdaCase - OverloadedStrings - PatternSynonyms +- StandaloneDeriving - ViewPatterns -# Required for use of recursion-schemes +# Required for use of the 'trees that grow' pattern +- MultiParamTypeClasses +- TypeFamilies +# Used by recursion-schemes when using template haskell - DeriveFoldable - DeriveFunctor - DeriveTraversable - TemplateHaskell -- TypeFamilies dependencies: - base >= 4.14 && < 5 @@ -33,7 +40,6 @@ dependencies: - parsec >= 3.1 && < 4 - recursion-schemes >= 5.2 && < 6 - text >= 1.2 && < 2 -- text-show >= 3.9 && < 4 - unordered-containers >= 0.2.13 && < 0.3 library: @@ -48,9 +54,10 @@ library: - -Wno-implicit-prelude - -Wno-missing-deriving-strategies # Less stupid warnings, but I still don't care - - -Wno-unused-do-bind - -Wno-all-missed-specialisations - -Wno-missing-local-signatures + # This is a good warning, but often polymorphism isn't actually needed. + - -Wno-monomorphism-restriction # Explicit import lists are generally a good thing, but I don't want them # in certain cases (e.g. importing my own modules, task-specific modules like the parser). - -Wno-missing-import-lists diff --git a/src/Data/Stream.hs b/src/Data/Stream.hs index df585e1..5463a2b 100644 --- a/src/Data/Stream.hs +++ b/src/Data/Stream.hs @@ -1,9 +1,12 @@ -module Data.Stream (Stream (Cons), filter, fromList) where +module Data.Stream + ( Stream (..) + , filter, iterate, fromList + ) where import Data.Functor.Foldable (Base, Corecursive, Recursive, embed, project, ana) -import Prelude hiding (filter, head, tail) +import Prelude hiding (filter, iterate, head, tail) -data Stream a = Cons a (Stream a) +data Stream a = Cons { head :: a, tail :: Stream a } type instance Base (Stream a) = (,) a @@ -19,6 +22,9 @@ filter p = ana \case | p x -> (x, xs) | otherwise -> project xs +iterate :: (a -> a) -> a -> Stream a +iterate f = ana \x -> (x, f x) + fromList :: [a] -> Stream a fromList = ana coalg where diff --git a/src/LambdaCalculus.hs b/src/LambdaCalculus.hs index 1b22300..139e6a0 100644 --- a/src/LambdaCalculus.hs +++ b/src/LambdaCalculus.hs @@ -1,156 +1,16 @@ module LambdaCalculus - ( module LambdaCalculus.Expression - , eval, traceEval + ( module LambdaCalculus.Evaluator + , module LambdaCalculus.Expression + , module LambdaCalculus.Syntax + , parseEval, unparseEval ) where -import Control.Monad.Except (MonadError, ExceptT, throwError, runExceptT) -import Control.Monad.State (MonadState, State, evalState, modify', state, put, gets) -import Control.Monad.Writer (runWriterT, tell) -import Data.Functor.Foldable (cata, para, project, embed) -import Data.HashSet (HashSet) -import Data.HashSet qualified as HS -import Data.Stream (Stream) -import Data.Stream qualified as S -import Data.Text (Text) -import Data.Text qualified as T -import Data.Void (Void, absurd) -import LambdaCalculus.Continuation -import LambdaCalculus.Expression (Expression (..), ExpressionF (..)) +import LambdaCalculus.Evaluator +import LambdaCalculus.Expression +import LambdaCalculus.Syntax --- | Free variables are variables which are present in an expression but not bound by any abstraction. -freeVariables :: Expression -> HashSet Text -freeVariables = cata \case - VariableF name -> HS.singleton name - ApplicationF e1 e2 -> HS.union e1 e2 - AbstractionF n e -> HS.delete n e - ContinuationF e -> HS.delete "!" e +parseEval :: Text -> Either ParseError EvalExpr +parseEval = fmap ast2eval . parseAST --- | Bound variables are variables which are bound by any form of abstraction in an expression. -boundVariables :: Expression -> HashSet Text -boundVariables = cata \case - VariableF _ -> HS.empty - ApplicationF e1 e2 -> HS.union e1 e2 - AbstractionF n e -> HS.insert n e - ContinuationF e -> HS.insert "!" e - --- | Variables that occur anywhere in an experession, bound or free. -usedVariables :: Expression -> HashSet Text -usedVariables x = HS.union (freeVariables x) (boundVariables x) - --- | Generate a stream of new variables which are not in the set of provided variables. -freshVariables :: HashSet Text -> Stream Text -freshVariables ctx = S.filter (not . flip HS.member ctx) $ S.fromList $ fmap T.pack $ (:) <$> ['a'..'z'] <*> map show [0 :: Int ..] - --- | Create a new variable which is not used anywhere else. -fresh :: State (Stream Text) Text -fresh = state project - --- | Substitution is the process of replacing all free occurrences of a variable in one expression with another expression. -substitute :: Text -> Expression -> Expression -> Expression -substitute var val = unsafeSubstitute var val . alphaConvert (usedVariables val) - --- | Rename the bound variables in `e` so they do not overlap any variables used in `ctx`. --- --- This is used as part of substitution when substituting `val` with free variables `ctx` into `e`, --- because it prevents any of the binders in `e` from accidentally capturing a free variable in `ctx`. -alphaConvert :: HashSet Text -> Expression -> Expression -alphaConvert ctx e_ = evalState (rename e_) $ freshVariables $ HS.union (usedVariables e_) ctx - where - rename :: Expression -> State (Stream Text) Expression - rename = cata \case - VariableF var -> pure $ Variable var - ApplicationF ef ex -> Application <$> ef <*> ex - ContinuationF e -> Continuation <$> e - AbstractionF n e - | HS.member n ctx -> do - n' <- fresh - Abstraction n' . unsafeSubstitute n (Variable n') <$> e - | otherwise -> Abstraction n <$> e - --- | Substitution with the assumption that no free variables in the value are bound in the expression. -unsafeSubstitute :: Text -> Expression -> Expression -> Expression -unsafeSubstitute var val = para \case - e' - | VariableF var2 <- e', var == var2 -> val - | ApplicationF (_, ef) (_, ex) <- e' -> Application ef ex - | ContinuationF (_, e) <- e', var /= "!" -> Continuation e - | AbstractionF var2 (_, e) <- e', var /= var2 -> Abstraction var2 e - | otherwise -> embed $ fmap fst e' - -isReducible :: Expression -> Bool -isReducible = snd . cata \case - ApplicationF ctr args -> eliminator ctr [args] - VariableF "callcc" -> constructor - AbstractionF _ _ -> constructor - ContinuationF _ -> constructor - VariableF _ -> constant - where - -- | Constants are irreducible in any context. - constant = (False, False) - -- | Constructors are reducible if an eliminator is applied to them. - constructor = (True, False) - -- | Eliminators are reducible if they are applied to a constructor or their arguments are reducible. - eliminator ctr args = (False, fst ctr || snd ctr || any snd args) - -push :: MonadState Continuation m => ContinuationCrumb -> m () -push c = modify' (c :) - -pop :: MonadState Continuation m => m (Maybe ContinuationCrumb) -pop = state \case - [] -> (Nothing, []) - (crumb:k) -> (Just crumb, k) - -ret :: (MonadError Expression m, MonadState Continuation m) => Expression -> m Expression -ret e = pop >>= maybe (throwError e) (pure . continue1 e) - --- | Iteratively perform an action forever (or at least until it performs a control flow effect). -iterateM_ :: Monad m => (a -> m a) -> a -> m b -iterateM_ m = m' where m' x = m x >>= m' - -fromLeft :: Either a Void -> a -fromLeft (Left x) = x -fromLeft (Right x) = absurd x - --- | Iteratively call an action until it 'throws' a return value. -loop :: Monad m => (a -> ExceptT b m a) -> a -> m b -loop f = fmap fromLeft . runExceptT . iterateM_ f - --- | A call-by-value expression evaluator. -evaluatorStep :: (MonadError Expression m, MonadState Continuation m) => Expression -> m Expression -evaluatorStep = \case - unmodified@(Application ef ex) - -- First reduce the argument... - | isReducible ex -> do - push (AppliedTo ef) - pure ex - -- then reduce the function... - | isReducible ef -> do - push (ApplyTo ex) - pure ef - | otherwise -> case ef of - -- perform beta reduction if possible... - Abstraction name body -> - pure $ substitute name ex body - -- perform continuation calls if possible... - Continuation body -> do - put [] - pure $ substitute "!" ex body - -- capture the current continuation if requested... - Variable "callcc" -> do - -- Don't worry about variable capture here for now. - k <- gets $ continue (Variable "!") - pure $ Application ex (Continuation k) - -- otherwise the value is irreducible and we can continue evaluation. - _ -> ret unmodified - -- Neither abstractions nor variables are reducible. - e -> ret e - -eval :: Expression -> Expression -eval = flip evalState [] . loop evaluatorStep - -traceEval :: Expression -> (Expression, [Expression]) -traceEval = flip evalState [] . runWriterT . loop \e -> do - -- You can also use `gets (continue e)` to print the *entire* expression each step. - -- This is a trade-off because it becomes much harder to pick out what changed from the rest of the expression. - tell [e] - evaluatorStep e +unparseEval :: EvalExpr -> Text +unparseEval = unparseAST . simplify . eval2ast diff --git a/src/LambdaCalculus/Evaluator.hs b/src/LambdaCalculus/Evaluator.hs new file mode 100644 index 0000000..e56edca --- /dev/null +++ b/src/LambdaCalculus/Evaluator.hs @@ -0,0 +1,171 @@ +module LambdaCalculus.Evaluator + ( Expr (..), ExprF (..), VoidF, Text + , Eval, EvalExpr, EvalX, EvalXF (..) + , pattern AppFE, pattern Cont, pattern ContF + , eval, traceEval + ) where + +import LambdaCalculus.Evaluator.Base +import LambdaCalculus.Evaluator.Continuation + +import Control.Monad.Except (MonadError, ExceptT, throwError, runExceptT) +import Control.Monad.State (MonadState, State, evalState, modify', state, put, gets) +import Control.Monad.Writer (runWriterT, tell) +import Data.Functor.Foldable (cata, para, embed) +import Data.HashSet (HashSet) +import Data.HashSet qualified as HS +import Data.Stream qualified as S +import Data.Text qualified as T +import Data.Void (Void, absurd) + +-- | Free variables are variables which are present in an expression but not bound by any abstraction. +freeVars :: EvalExpr -> HashSet Text +freeVars = cata \case + VarF name -> HS.singleton name + AppFE e1 e2 -> HS.union e1 e2 + AbsF n e -> HS.delete n e + ContF e -> HS.delete "!" e + +-- | Bound variables are variables which are bound by any form of abstraction in an expression. +boundVars :: EvalExpr -> HashSet Text +boundVars = cata \case + VarF _ -> HS.empty + AppFE e1 e2 -> HS.union e1 e2 + AbsF n e -> HS.insert n e + ContF e -> HS.insert "!" e + +-- | Vars that occur anywhere in an experession, bound or free. +usedVars :: EvalExpr -> HashSet Text +usedVars x = HS.union (freeVars x) (boundVars x) + +-- | Substitution is the process of replacing all free occurrences of a variable in one expression with another expression. +substitute :: Text -> EvalExpr -> EvalExpr -> EvalExpr +substitute var val = unsafeSubstitute var val . alphaConvert (freeVars val) + +-- | Substitution is only safe if the bound variables in the body +-- are disjoint from the free variables in the argument; +-- this function makes an expression body safe for substitution +-- by replacing the bound variables in the body +-- with completely new variables which do not occur in either expression +-- (without changing any *free* variables in the body, of course). +alphaConvert :: HashSet Text -> EvalExpr -> EvalExpr +alphaConvert ctx e_ = evalState (alphaConverter e_) $ HS.union ctx (usedVars e_) + where + alphaConverter :: EvalExpr -> State (HashSet Text) EvalExpr + alphaConverter = cata \case + e + | AbsF n e' <- e, n `HS.member` ctx -> do + n' <- fresh n + e'' <- e' + pure $ Abs n' $ replace n n' e'' + | otherwise -> embed <$> sequenceA e + + -- | Create a new name which is not used anywhere else. + fresh :: Text -> State (HashSet Text) Text + fresh n = state \ctx' -> + let n' = S.head $ S.filter (not . (`HS.member` ctx')) names + in (n', HS.insert n' ctx') + where names = S.iterate (`T.snoc` '\'') n + +-- | Replace a name with an entirely new name in all contexts. +-- This will only give correct results if +-- the new name does not occur anywhere in the expression. +replace :: Text -> Text -> EvalExpr -> EvalExpr +replace name name' = cata \case + e + | VarF name2 <- e, name == name2 -> Var name' + | AbsF name2 e' <- e, name == name2 -> Abs name' e' + | otherwise -> embed e + +-- | Substitution which does *not* avoid variable capture; +-- it only gives the correct result if the bound variables in the body +-- are disjoint from the free variables in the argument. +unsafeSubstitute :: Text -> EvalExpr -> EvalExpr -> EvalExpr +unsafeSubstitute var val = para \case + e' + | VarF var2 <- e', var == var2 -> val + | AbsF var2 _ <- e', var == var2 -> unmodified e' + | ContF _ <- e', var == "!" -> unmodified e' + | otherwise -> substituted e' + where + substituted = embed . fmap snd + unmodified = embed . fmap fst + +isReducible :: EvalExpr -> Bool +isReducible = snd . cata \case + AppF ctr (Identity args) -> eliminator ctr [args] + VarF "callcc" -> constructor + AbsF _ _ -> constructor + ContF _ -> constructor + VarF _ -> constant + where + -- | Constants are irreducible in any context. + constant = (False, False) + -- | Constructors are reducible if an eliminator is applied to them. + constructor = (True, False) + -- | Eliminators are reducible if they are applied to a constructor or their arguments are reducible. + eliminator ctr args = (False, fst ctr || snd ctr || any snd args) + +push :: MonadState Continuation m => ContinuationCrumb -> m () +push c = modify' (c :) + +pop :: MonadState Continuation m => m (Maybe ContinuationCrumb) +pop = state \case + [] -> (Nothing, []) + (crumb:k) -> (Just crumb, k) + +ret :: (MonadError EvalExpr m, MonadState Continuation m) => EvalExpr -> m EvalExpr +ret e = pop >>= maybe (throwError e) (pure . continue1 e) + +-- | Iteratively perform an action forever (or at least until it performs a control flow effect). +iterateM_ :: Monad m => (a -> m a) -> a -> m b +iterateM_ m = m' where m' x = m x >>= m' + +fromLeft :: Either a Void -> a +fromLeft (Left x) = x +fromLeft (Right x) = absurd x + +-- | Iteratively call an action until it 'throws' a return value. +loop :: Monad m => (a -> ExceptT b m a) -> a -> m b +loop f = fmap fromLeft . runExceptT . iterateM_ f + +-- | A call-by-value expression evaluator. +evaluatorStep :: (MonadError EvalExpr m, MonadState Continuation m) => EvalExpr -> m EvalExpr +evaluatorStep = \case + unmodified@(App ef ex) + -- First reduce the argument... + | isReducible ex -> do + push (AppliedTo ef) + pure ex + -- then reduce the function... + | isReducible ef -> do + push (ApplyTo ex) + pure ef + | otherwise -> case ef of + -- perform beta reduction if possible... + Abs name body -> + pure $ substitute name ex body + -- perform continuation calls if possible... + Cont body -> do + put [] + pure $ substitute "!" ex body + -- capture the current continuation if requested... + Var "callcc" -> do + -- Don't worry about variable capture here for now. + k <- gets $ continue (Var "!") + pure $ App ex (Cont k) + -- otherwise the value is irreducible and we can continue evaluation. + _ -> ret unmodified + -- Neither abstractions nor variables are reducible. + e -> ret e + +eval :: EvalExpr -> EvalExpr +eval = flip evalState [] . loop evaluatorStep + +traceEval :: EvalExpr -> (EvalExpr, [EvalExpr]) +traceEval = flip evalState [] . runWriterT . loop \e -> do + -- You can also use `gets (continue e)` to print the *entire* expression each step. + -- This is a trade-off because it becomes much harder to pick out what changed from the rest of the expression. + e' <- gets (continue e) + tell [e'] + evaluatorStep e diff --git a/src/LambdaCalculus/Evaluator/Base.hs b/src/LambdaCalculus/Evaluator/Base.hs new file mode 100644 index 0000000..c9a22f4 --- /dev/null +++ b/src/LambdaCalculus/Evaluator/Base.hs @@ -0,0 +1,52 @@ +module LambdaCalculus.Evaluator.Base + ( Identity (..) + , Expr (..), ExprF (..), VoidF, Text + , Eval, EvalExpr, EvalExprF, EvalX, EvalXF (..) + , pattern AppFE, pattern Cont, pattern ContF + ) where + +import LambdaCalculus.Expression.Base + +import Data.Functor.Identity (Identity (..)) + +data Eval +type EvalExpr = Expr Eval +type instance AppArgs Eval = EvalExpr +type instance AbsArgs Eval = Text +type instance LetArgs Eval = VoidF EvalExpr +type instance XExpr Eval = EvalX + +type EvalX = EvalXF EvalExpr + +type EvalExprF = ExprF Eval +type instance AppArgsF Eval = Identity +type instance LetArgsF Eval = VoidF +type instance XExprF Eval = EvalXF + +newtype EvalXF r + -- | A continuation. This is identical to a lambda abstraction, + -- with the exception that it performs the side-effect of + -- deleting the current continuation. + -- + -- Continuations do not have any corresponding surface-level syntax, + -- but may be printed like a lambda with the illegal variable `!`. + = Cont_ r + deriving (Eq, Functor, Foldable, Traversable, Show) + +instance RecursivePhase Eval where + projectAppArgs = Identity + embedAppArgs = runIdentity + +pattern Cont :: EvalExpr -> EvalExpr +pattern Cont e = ExprX (Cont_ e) + +pattern ContF :: r -> EvalExprF r +pattern ContF e = ExprXF (Cont_ e) + +pattern AppFE :: r -> r -> EvalExprF r +pattern AppFE ef ex = AppF ef (Identity ex) + +{-# COMPLETE Var, App, Abs, Let, Cont #-} +{-# COMPLETE VarF, AppF, AbsF, LetF, ContF #-} +{-# COMPLETE VarF, AppFE, AbsF, LetF, ExprXF #-} +{-# COMPLETE VarF, AppFE, AbsF, LetF, ContF #-} diff --git a/src/LambdaCalculus/Continuation.hs b/src/LambdaCalculus/Evaluator/Continuation.hs similarity index 54% rename from src/LambdaCalculus/Continuation.hs rename to src/LambdaCalculus/Evaluator/Continuation.hs index 048bc99..009f29f 100644 --- a/src/LambdaCalculus/Continuation.hs +++ b/src/LambdaCalculus/Evaluator/Continuation.hs @@ -1,26 +1,26 @@ -module LambdaCalculus.Continuation +module LambdaCalculus.Evaluator.Continuation ( Continuation, continue, continue1 , ContinuationCrumb (ApplyTo, AppliedTo, AbstractedOver) ) where +import LambdaCalculus.Evaluator.Base + import Data.List (foldl') -import Data.Text (Text) -import LambdaCalculus.Expression data ContinuationCrumb -- | The one-hole context of a function application: `(_ e)` - = ApplyTo Expression + = ApplyTo EvalExpr -- | The one-hole context of the argument to a function application: `(f _)` - | AppliedTo Expression + | AppliedTo EvalExpr -- | The one-hole context of the body of a lambda abstraction: `(λx. _)` | AbstractedOver Text type Continuation = [ContinuationCrumb] -continue1 :: Expression -> ContinuationCrumb -> Expression -continue1 e (ApplyTo x) = Application e x -continue1 e (AppliedTo x) = Application x e -continue1 e (AbstractedOver name) = Abstraction name e +continue1 :: EvalExpr -> ContinuationCrumb -> EvalExpr +continue1 e (ApplyTo x) = App e x +continue1 e (AppliedTo x) = App x e +continue1 e (AbstractedOver name) = Abs name e -continue :: Expression -> Continuation -> Expression +continue :: EvalExpr -> Continuation -> EvalExpr continue = foldl' continue1 diff --git a/src/LambdaCalculus/Expression.hs b/src/LambdaCalculus/Expression.hs index 2b30d64..88629c9 100644 --- a/src/LambdaCalculus/Expression.hs +++ b/src/LambdaCalculus/Expression.hs @@ -1,96 +1,33 @@ module LambdaCalculus.Expression - ( Expression (..), ExpressionF (..) - , ast2expr, expr2ast - , pattern Lets, pattern Abstractions, pattern Applications - , viewLet, viewAbstraction, viewApplication + ( Expr (..), ExprF (..), DefF (..), VoidF, Text + , Eval, EvalExpr, EvalX, EvalXF (..), Identity (..) + , pattern AppFE, pattern Cont, pattern ContF + , Parse, AST, ASTF, NonEmptyDefFs (..), NonEmpty (..), simplify + , pattern LetFP + , ast2eval, eval2ast ) where --- The definition of Expression is in its own file because: --- * Expression and AbstractSyntax should not be in the same file --- * Expression's `show` definition depends on AbstractSyntax's show definition, --- which means that `ast2expr` and `expr2ast` can't be in AbstractSyntax --- because of mutually recursive modules --- * I don't want to clutter the module focusing on the actual evaluation --- with all of these irrelevant conversion operators. +import LambdaCalculus.Evaluator.Base +import LambdaCalculus.Syntax.Base -import Data.Bifunctor (first) -import Data.Functor.Foldable (ana, cata) -import Data.Functor.Foldable.TH (makeBaseFunctor) -import Data.List (foldl1') -import Data.List.NonEmpty (NonEmpty ((:|)), fromList, toList) -import Data.Text (Text) -import Data.Text qualified as T -import LambdaCalculus.Parser.AbstractSyntax (AbstractSyntax) -import LambdaCalculus.Parser.AbstractSyntax qualified as AST -import TextShow (TextShow, showb, showt) +import Data.Functor.Foldable (cata, hoist) +import Data.List (foldl') +import Data.List.NonEmpty (toList) -data Expression - = Variable Text - -- | Function application: `(f x)`. - | Application Expression Expression - -- | Lambda abstraction: `(λx. e)`. - | Abstraction Text Expression - -- | A continuation. This is identical to a lambda abstraction, - -- with the exception that it performs the side-effect of - -- deleting the current continuation. - -- - -- Continuations do not have any corresponding surface-level syntax. - | Continuation Expression - deriving Eq +-- | Convert from an abstract syntax tree to an evaluator expression. +ast2eval :: AST -> EvalExpr +ast2eval = cata \case + VarF name -> Var name + AppF ef exs -> foldl' App ef $ toList exs + AbsF ns e -> foldr Abs e $ toList ns + LetF ds e -> + let letExpr name val body' = App (Abs name body') val + in foldr (uncurry letExpr) e $ getNonEmptyDefFs ds -makeBaseFunctor ''Expression - --- | Convert from an abstract syntax tree to an expression. -ast2expr :: AbstractSyntax -> Expression -ast2expr = cata \case - AST.VariableF name -> Variable name - AST.ApplicationF es -> case es of - x :| [] -> x - xs -> foldl1' Application (toList xs) - AST.AbstractionF names body -> foldr Abstraction body (toList names) - AST.LetF defs body -> - let letExpr name val body' = Application (Abstraction name body') val - in foldr (uncurry letExpr) body defs - --- | View nested applications of abstractions as a list. -pattern Lets :: [(Text, Expression)] -> Expression -> Expression -pattern Lets defs body <- (viewLet -> (defs@(_:_), body)) - -viewLet :: Expression -> ([(Text, Expression)], Expression) -viewLet (Application (Abstraction var body) x) = first ((var, x) :) (viewLet body) -viewLet x = ([], x) - --- | View nested abstractions as a list. -pattern Abstractions :: [Text] -> Expression -> Expression -pattern Abstractions names body <- (viewAbstraction -> (names@(_:_), body)) - -viewAbstraction :: Expression -> ([Text], Expression) -viewAbstraction (Abstraction name body) = first (name :) (viewAbstraction body) -viewAbstraction x = ([], x) - --- | View left-nested applications as a list. -pattern Applications :: [Expression] -> Expression -pattern Applications exprs <- (viewApplication -> exprs@(_:_:_)) - -{-# COMPLETE Abstractions, Applications, Continuation, Variable :: Expression #-} - -viewApplication :: Expression -> [Expression] -viewApplication (Application ef ex) = viewApplication ef ++ [ex] -viewApplication x = [x] - --- | Convert from an expression to an abstract syntax tree. --- --- This function will use let, and applications and abstractions of multiple values when possible. -expr2ast :: Expression -> AbstractSyntax -expr2ast = ana \case - Lets defs body -> AST.LetF (fromList defs) body - Abstractions names body -> AST.AbstractionF (fromList names) body - Applications exprs -> AST.ApplicationF $ fromList exprs - Continuation body -> AST.AbstractionF ("!" :| []) body - Variable name -> AST.VariableF name - -instance TextShow Expression where - showb = showb . expr2ast - -instance Show Expression where - show = T.unpack . showt +-- | Convert from an evaluator expression to an abstract syntax tree. +eval2ast :: EvalExpr -> AST +eval2ast = hoist \case + VarF name -> VarF name + AppFE ef ex -> AppF ef (ex :| []) + AbsF n e -> AbsF (n :| []) e + ContF e -> AbsF ("!" :| []) e diff --git a/src/LambdaCalculus/Expression/Base.hs b/src/LambdaCalculus/Expression/Base.hs new file mode 100644 index 0000000..2253989 --- /dev/null +++ b/src/LambdaCalculus/Expression/Base.hs @@ -0,0 +1,166 @@ +{-# LANGUAGE UndecidableInstances #-} +module LambdaCalculus.Expression.Base + ( Text, VoidF, absurd' + , Expr (..), Def, AppArgs, AbsArgs, LetArgs, XExpr + , ExprF (..), DefF (..), AppArgsF, LetArgsF, XExprF + , RecursivePhase, projectAppArgs, projectLetArgs, projectXExpr, projectDef + , embedAppArgs, embedLetArgs, embedXExpr, embedDef + ) where + +import Data.Functor.Foldable (Base, Recursive, Corecursive, project, embed) +import Data.Kind (Type) +import Data.Text (Text) + +data Expr phase + -- | A variable: `x`. + = Var !Text + -- | Function application: `f x_0 ... x_n`. + | App !(Expr phase) !(AppArgs phase) + -- | Lambda abstraction: `λx_0 ... x_n. e`. + | Abs !(AbsArgs phase) !(Expr phase) + -- | Let expression: `let x_0 = v_0 ... ; x_n = v_n in e`. + | Let !(LetArgs phase) !(Expr phase) + -- | Additional phase-specific constructors. + | ExprX !(XExpr phase) + +deriving instance + ( Eq (AppArgs phase) + , Eq (AbsArgs phase) + , Eq (LetArgs phase) + , Eq (XExpr phase) + ) => Eq (Expr phase) + +deriving instance + ( Show (AppArgs phase) + , Show (AbsArgs phase) + , Show (LetArgs phase) + , Show (XExpr phase) + ) => Show (Expr phase) + +type family AppArgs phase +type family AbsArgs phase +type family LetArgs phase +type family XExpr phase + +-- | A definition, mapping a name to a value. +type Def phase = (Text, Expr phase) + +--- +--- Base functor boilerplate for recursion-schemes +--- + +data ExprF phase r + = VarF !Text + | AppF !r !(AppArgsF phase r) + | AbsF !(AbsArgs phase) r + | LetF !(LetArgsF phase r) r + | ExprXF !(XExprF phase r) + +type instance Base (Expr phase) = ExprF phase + +type family AppArgsF phase :: Type -> Type +type family LetArgsF phase :: Type -> Type +type family XExprF phase :: Type -> Type + +data DefF r = DefF !Text !r + deriving (Eq, Functor, Show) + +-- | An empty type with one extra type parameter. +data VoidF a + deriving (Eq, Functor, Foldable, Traversable, Show) + +absurd' :: VoidF a -> b +absurd' x = case x of {} + +instance + ( Functor (AppArgsF phase) + , Functor (LetArgsF phase) + , Functor (XExprF phase) + ) => Functor (ExprF phase) where + fmap f = \case + VarF n -> VarF n + AppF ef exs -> AppF (f ef) (fmap f exs) + AbsF ns e -> AbsF ns (f e) + LetF ds e -> LetF (fmap f ds) (f e) + ExprXF q -> ExprXF (fmap f q) + +instance + ( Foldable (AppArgsF phase) + , Foldable (LetArgsF phase) + , Foldable (XExprF phase) + ) => Foldable (ExprF phase) where + foldMap f = \case + VarF _ -> mempty + AppF ef exs -> f ef <> foldMap f exs + AbsF _ e -> f e + LetF ds e -> foldMap f ds <> f e + ExprXF q -> foldMap f q + +instance + ( Traversable (AppArgsF phase) + , Traversable (LetArgsF phase) + , Traversable (XExprF phase) + ) => Traversable (ExprF phase) where + traverse f = \case + VarF n -> pure $ VarF n + AppF ef exs -> AppF <$> f ef <*> traverse f exs + AbsF ns e -> AbsF ns <$> f e + LetF ds e -> LetF <$> traverse f ds <*> f e + ExprXF q -> ExprXF <$> traverse f q + +class Functor (ExprF phase) => RecursivePhase phase where + projectAppArgs :: AppArgs phase -> AppArgsF phase (Expr phase) + projectLetArgs :: LetArgs phase -> LetArgsF phase (Expr phase) + projectXExpr :: XExpr phase -> XExprF phase (Expr phase) + + embedAppArgs :: AppArgsF phase (Expr phase) -> AppArgs phase + embedLetArgs :: LetArgsF phase (Expr phase) -> LetArgs phase + embedXExpr :: XExprF phase (Expr phase) -> XExpr phase + + default projectAppArgs :: AppArgs phase ~ AppArgsF phase (Expr phase) + => AppArgs phase -> AppArgsF phase (Expr phase) + default projectLetArgs :: LetArgs phase ~ LetArgsF phase (Expr phase) + => LetArgs phase -> LetArgsF phase (Expr phase) + default projectXExpr :: XExpr phase ~ XExprF phase (Expr phase) + => XExpr phase -> XExprF phase (Expr phase) + + default embedAppArgs :: AppArgsF phase (Expr phase) ~ AppArgs phase + => AppArgsF phase (Expr phase) -> AppArgs phase + default embedLetArgs :: LetArgsF phase (Expr phase) ~ LetArgs phase + => LetArgsF phase (Expr phase) -> LetArgs phase + default embedXExpr :: XExprF phase (Expr phase) ~ XExpr phase + => XExprF phase (Expr phase) -> XExpr phase + + projectAppArgs = id + projectLetArgs = id + projectXExpr = id + + embedAppArgs = id + embedLetArgs = id + embedXExpr = id + +projectDef :: Def phase -> DefF (Expr phase) +projectDef = uncurry DefF + +embedDef :: DefF (Expr phase) -> Def phase +embedDef (DefF n e) = (n, e) + +instance RecursivePhase phase => Recursive (Expr phase) where + project = \case + Var n -> VarF n + App ef exs -> AppF ef (projectAppArgs exs) + Abs ns e -> AbsF ns e + Let ds e -> LetF (projectLetArgs ds) e + ExprX q -> ExprXF (projectXExpr q) + +instance RecursivePhase phase => Corecursive (Expr phase) where + embed = \case + VarF n -> Var n + AppF ef exs -> App ef (embedAppArgs exs) + AbsF ns e -> Abs ns e + LetF ds e -> Let (embedLetArgs ds) e + ExprXF q -> ExprX (embedXExpr q) + +--- +--- End base functor boilerplate. +--- diff --git a/src/LambdaCalculus/Parser/AbstractSyntax.hs b/src/LambdaCalculus/Parser/AbstractSyntax.hs deleted file mode 100644 index 0b6edb3..0000000 --- a/src/LambdaCalculus/Parser/AbstractSyntax.hs +++ /dev/null @@ -1,96 +0,0 @@ -module LambdaCalculus.Parser.AbstractSyntax - ( AbstractSyntax (..), AbstractSyntaxF (..), Definition, Identifier - ) where - -import Data.Functor.Base (NonEmptyF (NonEmptyF)) -import Data.Functor.Foldable (cata) -import Data.Functor.Foldable.TH (makeBaseFunctor) -import Data.List.NonEmpty (NonEmpty, toList) -import Data.Text (Text) -import Data.Text qualified as T -import TextShow (Builder, TextShow, showb, showt, toText, fromText) - --- | The abstract syntax tree reflects the structure of the externally-visible syntax. --- --- This contains a lot of syntactic sugar when compared with 'LambdaCalculus.Expression'. --- If this syntactic sugar were used in Expression, then operations like evaluation --- would become unnecessarily complicated, because the same expression --- can be represented in terms of multiple abstract syntax trees. -data AbstractSyntax - = Variable Identifier - -- There is no technical reason for the AST to forbid nullary applications and so forth. - -- However the parser rejects them to avoid confusing edge cases like `let x=in`, - -- so they're forbidden here too so that the syntax tree can't contain data - -- that the parser would refuse to accept. - -- - -- As a matter of curiosity, here's why `let x=in` was syntactically valid: - -- 1. Parentheses in `let` statements are optional, infer them: `let x=()in()`. - -- 2. Insert optional whitespace: `let x = () in ()`. - -- 3. Nullary application expands to the identity function because - -- the identity function is the left identity of function application: - -- `let x=(\x.x) in \x.x`. - -- - -- | n-ary function application: `(f x_1 x_2 ... x_n)`. - | Application (NonEmpty AbstractSyntax) - -- | Lambda abstraction over n variables: `(λx_1 x_2 ... x_n. e)` - | Abstraction (NonEmpty Identifier) AbstractSyntax - -- | Let expressions (syntactic sugar) binding `n` variables: - -- `let x_1 = e_1; x_2 = e_2; ... x_n = e_n`. - | Let (NonEmpty Definition) AbstractSyntax -type Definition = (Identifier, AbstractSyntax) -type Identifier = Text - -makeBaseFunctor ''AbstractSyntax - --- I'm surprised this isn't in base somewhere. -unsnoc :: NonEmpty a -> ([a], a) -unsnoc = cata \case - NonEmptyF x' Nothing -> ([], x') - NonEmptyF x (Just (xs, x')) -> (x : xs, x') - -data SyntaxType - -- | Ambiguous syntax is not necessarily finite and not guaranteed to consume any input. - = Ambiguous - -- | Block syntax is not necessarily finite but is guaranteed to consume input. - | Block - -- | Unambiguous syntax is finite and guaranteed to consume input. - | Finite -type Tagged a = (SyntaxType, a) - -tag :: SyntaxType -> a -> Tagged a -tag = (,) - -group :: Builder -> Builder -group x = "(" <> x <> ")" - --- | An unambiguous context has a marked beginning and end. -unambiguous :: Tagged Builder -> Builder -unambiguous (_, t) = t - --- | A final context has a marked end but no marked beginning, --- so we provide a grouper when a beginning marker is necessary. -final :: Tagged Builder -> Builder -final (Ambiguous, t) = group t -final (_, t) = t - --- | An ambiguous context has neither a marked end nor marked beginning, --- so we provide a grouper when an ending marker is necessary. -ambiguous :: Tagged Builder -> Builder -ambiguous (Finite, t) = t -ambiguous (_, t) = group t - -instance TextShow AbstractSyntax where - showb = snd . cata \case - VariableF name -> tag Finite $ fromText name - ApplicationF (unsnoc -> (es, efinal)) -> tag Ambiguous $ foldr (\e es' -> ambiguous e <> " " <> es') (final efinal) es - AbstractionF names body -> tag Block $ - let names' = fromText (T.intercalate " " $ toList names) - in "λ" <> names' <> ". " <> unambiguous body - LetF defs body -> tag Block $ - let - showDef (name, val) = fromText name <> " = " <> unambiguous val - defs' = fromText (T.intercalate "; " $ map (toText . showDef) $ toList defs) - in "let " <> defs' <> " in " <> unambiguous body - -instance Show AbstractSyntax where - show = T.unpack . showt diff --git a/src/LambdaCalculus/Syntax.hs b/src/LambdaCalculus/Syntax.hs new file mode 100644 index 0000000..3304d05 --- /dev/null +++ b/src/LambdaCalculus/Syntax.hs @@ -0,0 +1,7 @@ +module LambdaCalculus.Syntax + ( module LambdaCalculus.Syntax.Parser + , module LambdaCalculus.Syntax.Printer + ) where + +import LambdaCalculus.Syntax.Parser +import LambdaCalculus.Syntax.Printer diff --git a/src/LambdaCalculus/Syntax/Base.hs b/src/LambdaCalculus/Syntax/Base.hs new file mode 100644 index 0000000..9dee3ca --- /dev/null +++ b/src/LambdaCalculus/Syntax/Base.hs @@ -0,0 +1,66 @@ +module LambdaCalculus.Syntax.Base + ( Expr (..), ExprF (..), Def, DefF (..), VoidF, Text, NonEmpty (..) + , Parse, AST, ASTF, NonEmptyDefFs (..) + , pattern LetFP + , simplify + ) where + +import LambdaCalculus.Expression.Base + +import Data.Functor.Foldable (embed, project) +import Data.List.NonEmpty (NonEmpty (..)) + +data Parse +-- | The abstract syntax tree reflects the structure of the externally-visible syntax. +-- +-- It includes syntactic sugar, which allows multiple ways to express many constructions, +-- e.g. multiple definitions in a single let expression or multiple names bound by one abstraction. +type AST = Expr Parse +-- There is no technical reason that the AST can't allow nullary applications and so forth, +-- nor is there any technical reason that the parser couldn't parse them, +-- but the parser *does* reject them to avoid confusing edge cases like `let x=in`, +-- so they're forbidden here too so that the syntax tree can't contain data +-- +-- that the parser would refuse to accept. +-- As a matter of curiosity, here's why `let x=in` was syntactically valid: +-- 1. Parentheses in `let` statements are optional, infer them: `let x=()in()`. +-- 2. Insert optional whitespace: `let x = () in ()`. +-- 3. Nullary application expands to the identity function because +-- the identity function is the left identity of function application: +-- `let x=(\x.x) in \x.x`. +type instance AppArgs Parse = NonEmpty AST +type instance AbsArgs Parse = NonEmpty Text +type instance LetArgs Parse = NonEmpty (Def Parse) +type instance XExpr Parse = VoidF AST + +type ASTF = ExprF Parse +type instance AppArgsF Parse = NonEmpty +type instance LetArgsF Parse = NonEmptyDefFs +type instance XExprF Parse = VoidF + +instance RecursivePhase Parse where + projectLetArgs = NonEmptyDefFs + embedLetArgs = getNonEmptyDefFs + +newtype NonEmptyDefFs r = NonEmptyDefFs { getNonEmptyDefFs :: NonEmpty (Text, r) } + deriving (Eq, Functor, Foldable, Traversable, Show) + +pattern LetFP :: NonEmpty (Text, r) -> r -> ASTF r +pattern LetFP ds e = LetF (NonEmptyDefFs ds) e + +{-# COMPLETE VarF, AppF, AbsF, LetFP, ExprXF #-} + +-- | Combine nested expressions into compound expressions when possible. +simplify :: AST -> AST +simplify = simplify' . embed . fmap simplify' . project + where + simplify' (App (App f es1) es2) = simplify' $ App f (es1 <> es2) + simplify' (App (Abs (nx :| ns) eb) (ex :| es)) = simplify' $ app' es $ Let ((nx, ex) :| []) $ abs' ns eb + where app' [] e = e + app' (ex2:es2) e = App e (ex2 :| es2) + + abs' [] e = e + abs' (nx2:ns2) e = Abs (nx2 :| ns2) e + simplify' (Abs ns1 (Abs ns2 e)) = simplify' $ Abs (ns1 <> ns2) e + simplify' (Let ds1 (Let ds2 e)) = simplify' $ Let (ds1 <> ds2) e + simplify' e = e diff --git a/src/LambdaCalculus/Parser.hs b/src/LambdaCalculus/Syntax/Parser.hs similarity index 59% rename from src/LambdaCalculus/Parser.hs rename to src/LambdaCalculus/Syntax/Parser.hs index 7e76aaf..3991202 100644 --- a/src/LambdaCalculus/Parser.hs +++ b/src/LambdaCalculus/Syntax/Parser.hs @@ -1,10 +1,12 @@ -module LambdaCalculus.Parser (parseAST, parseExpression) where +module LambdaCalculus.Syntax.Parser + ( ParseError + , parseAST + ) where + +import LambdaCalculus.Syntax.Base import Data.List.NonEmpty (fromList) -import Data.Text (Text) import Data.Text qualified as T -import LambdaCalculus.Expression (Expression, ast2expr) -import LambdaCalculus.Parser.AbstractSyntax import Text.Parsec hiding (label, token) import Text.Parsec qualified import Text.Parsec.Text (Parser) @@ -22,49 +24,49 @@ keywords = ["let", "in"] keyword :: Text -> Parser () keyword kwd = label (T.unpack kwd) $ do try do - string $ T.unpack kwd + _ <- string $ T.unpack kwd notFollowedBy letter spaces -- | An identifier is a sequence of letters which is not a keyword. -identifier :: Parser Identifier +identifier :: Parser Text identifier = label "identifier" $ do notFollowedBy anyKeyword T.pack <$> (many1 letter <* spaces) where anyKeyword = choice $ map keyword keywords -variable :: Parser AbstractSyntax -variable = label "variable" $ Variable <$> identifier +variable :: Parser AST +variable = label "variable" $ Var <$> identifier -many2 :: Parser a -> Parser [a] -many2 p = (:) <$> p <*> many1 p +many1' :: Parser a -> Parser (NonEmpty a) +many1' p = fromList <$> many1 p -grouping :: Parser AbstractSyntax +many2 :: Parser a -> Parser (a, NonEmpty a) +many2 p = (,) <$> p <*> many1' p + +grouping :: Parser AST grouping = label "grouping" $ between (token '(') (token ')') expression -application :: Parser AbstractSyntax -application = Application . fromList <$> many2 applicationTerm +application :: Parser AST +application = uncurry App <$> many2 applicationTerm where applicationTerm = abstraction <|> let_ <|> grouping <|> variable -abstraction :: Parser AbstractSyntax -abstraction = label "lambda abstraction" $ Abstraction <$> between lambda (token '.') (fromList <$> many1 identifier) <*> expression +abstraction :: Parser AST +abstraction = label "lambda abstraction" $ Abs <$> between lambda (token '.') (many1' identifier) <*> expression where lambda = label "lambda" $ (char '\\' <|> char 'λ') *> spaces -let_ :: Parser AbstractSyntax +let_ :: Parser AST let_ = Let <$> between (keyword "let") (keyword "in") (fromList <$> definitions) <*> expression where - definitions :: Parser [Definition] + definitions :: Parser [Def Parse] definitions = flip sepBy1 (token ';') do name <- identifier token '=' value <- expression pure (name, value) -expression :: Parser AbstractSyntax +expression :: Parser AST expression = label "expression" $ abstraction <|> let_ <|> try application <|> grouping <|> variable -parseAST :: Text -> Either ParseError AbstractSyntax +parseAST :: Text -> Either ParseError AST parseAST = parse (spaces *> expression <* eof) "input" - -parseExpression :: Text -> Either ParseError Expression -parseExpression = fmap ast2expr . parseAST diff --git a/src/LambdaCalculus/Syntax/Printer.hs b/src/LambdaCalculus/Syntax/Printer.hs new file mode 100644 index 0000000..f96f737 --- /dev/null +++ b/src/LambdaCalculus/Syntax/Printer.hs @@ -0,0 +1,63 @@ +module LambdaCalculus.Syntax.Printer (unparseAST) where + +import LambdaCalculus.Syntax.Base + +import Data.Functor.Base (NonEmptyF (NonEmptyF)) +import Data.Functor.Foldable (cata) +import Data.List.NonEmpty (toList) +import Data.Text.Lazy (fromStrict, toStrict, intercalate, unwords) +import Data.Text.Lazy.Builder (Builder, fromText, fromLazyText, toLazyText) +import Prelude hiding (unwords) + +-- I'm surprised this isn't in base somewhere. +unsnoc :: NonEmpty a -> ([a], a) +unsnoc = cata \case + NonEmptyF x' Nothing -> ([], x') + NonEmptyF x (Just (xs, x')) -> (x : xs, x') + +data SyntaxType + -- | Ambiguous syntax is not necessarily finite and not guaranteed to consume any input. + = Ambiguous + -- | Block syntax is not necessarily finite but is guaranteed to consume input. + | Block + -- | Unambiguous syntax is finite and guaranteed to consume input. + | Finite +type Tagged a = (SyntaxType, a) + +tag :: SyntaxType -> a -> Tagged a +tag = (,) + +group :: Builder -> Builder +group x = "(" <> x <> ")" + +-- | An unambiguous context has a marked beginning and end. +unambiguous :: Tagged Builder -> Builder +unambiguous (_, t) = t + +-- | A final context has a marked end but no marked beginning, +-- so we provide a grouper when a beginning marker is necessary. +final :: Tagged Builder -> Builder +final (Ambiguous, t) = group t +final (_, t) = t + +-- | An ambiguous context has neither a marked end nor marked beginning, +-- so we provide a grouper when an ending marker is necessary. +ambiguous :: Tagged Builder -> Builder +ambiguous (Finite, t) = t +ambiguous (_, t) = group t + +-- | Turn an abstract syntax tree into the corresponding concrete syntax. +-- +-- This is *not* a pretty-printer; it uses minimal whitespace. +unparseAST :: AST -> Text +unparseAST = toStrict . toLazyText . snd . cata \case + VarF name -> tag Finite $ fromText name + AppF ef (unsnoc -> (exs, efinal)) -> tag Ambiguous $ foldr (\e es' -> ambiguous e <> " " <> es') (final efinal) (ef : exs) + AbsF names body -> tag Block $ + let names' = fromLazyText (unwords $ map fromStrict $ toList names) + in "λ" <> names' <> ". " <> unambiguous body + LetFP defs body -> tag Block $ + let + unparseDef (name, val) = fromText name <> " = " <> unambiguous val + defs' = fromLazyText (intercalate "; " $ map (toLazyText . unparseDef) $ toList defs) + in "let " <> defs' <> " in " <> unambiguous body diff --git a/stack.yaml b/stack.yaml index 4d3fc11..a135319 100644 --- a/stack.yaml +++ b/stack.yaml @@ -1,3 +1,3 @@ -resolver: lts-17.5 +resolver: lts-17.6 packages: - . diff --git a/stack.yaml.lock b/stack.yaml.lock index fa953b3..a0e9c1f 100644 --- a/stack.yaml.lock +++ b/stack.yaml.lock @@ -6,7 +6,7 @@ packages: [] snapshots: - completed: - size: 565266 - url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/5.yaml - sha256: 78e8ebabf11406261abbc95b44f240acf71802630b368888f6d758de7fc3a2f7 - original: lts-17.5 + size: 565712 + url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/6.yaml + sha256: 4e5e581a709c88e3fe26a9ce8bf331435729bead762fb5c190064c6c5bb1b835 + original: lts-17.6 diff --git a/test/Spec.hs b/test/Spec.hs index ba5638e..59ae7be 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -1,5 +1,5 @@ import LambdaCalculus -import LambdaCalculus.Parser + import Test.Tasty import Test.Tasty.HUnit @@ -9,63 +9,64 @@ import Test.Tasty.HUnit -- so the names for them are somewhat arbitrary. -- This should evaluate to `y y`. -dfi :: Expression -dfi = Application d (Application f i) +dfi :: EvalExpr +dfi = App d (App f i) where - d = Abstraction "x" $ Application (Variable "x") (Variable "x") - f = Abstraction "f" $ Application (Variable "f") (Application (Variable "f") (Variable "y")) - i = Abstraction "x" $ Variable "x" + d = Abs "x" $ App (Var "x") (Var "x") + f = Abs "f" $ App (Var "f") (App (Var "f") (Var "y")) + i = Abs "x" $ Var "x" -- This should evalaute to `y`. -ttttt :: Expression -ttttt = Application (Application (Application f t) (Abstraction "x" (Variable "x"))) (Variable "y") +ttttt :: EvalExpr +ttttt = App (App (App f t) (Abs "x" (Var "x"))) (Var "y") where - t = Abstraction "f" $ Abstraction "x" $ - Application (Variable "f") (Application (Variable "f") (Variable "x")) - f = Abstraction "T" $ Abstraction "f" $ Abstraction "x" $ - Application (Application - (Application (Variable "T") - (Application (Variable "T") - (Application (Variable "T") - (Application (Variable "T") - (Variable "T"))))) - (Variable "f")) - (Variable "x") + t = Abs "f" $ Abs "x" $ + App (Var "f") (App (Var "f") (Var "x")) + f = Abs "T" $ Abs "f" $ Abs "x" $ + App + (App + (App (Var "T") + (App (Var "T") + (App (Var "T") + (App (Var "T") + (Var "T"))))) + (Var "f")) + (Var "x") -- | A simple divergent expression. -omega :: Expression -omega = Application x x - where x = Abstraction "x" (Application (Variable "x") (Variable "x")) +omega :: EvalExpr +omega = App x x + where x = Abs "x" (App (Var "x") (Var "x")) -cc1 :: Expression -cc1 = Application (Variable "callcc") (Abstraction "k" (Application omega (Application (Variable "k") (Variable "z")))) +cc1 :: EvalExpr +cc1 = App (Var "callcc") (Abs "k" (App omega (App (Var "k") (Var "z")))) -cc2 :: Expression -cc2 = Application (Variable "y") (Application (Variable "callcc") (Abstraction "k" (Application (Variable "z") (Application (Variable "k") (Variable "x"))))) +cc2 :: EvalExpr +cc2 = App (Var "y") (App (Var "callcc") (Abs "k" (App (Var "z") (App (Var "k") (Var "x"))))) main :: IO () main = defaultMain $ testGroup "Tests" [ testGroup "Evaluator tests" - [ testCase "capture test 1: DFI" $ eval dfi @?= Application (Variable "y") (Variable "y") - , testCase "capture test 2: ttttt" $ eval ttttt @?= Variable "y" - , testCase "invoking a continuation replaces the current continuation" $ eval cc1 @?= Variable "z" - , testCase "callcc actually captures the current continuation" $ eval cc2 @?= Application (Variable "y") (Variable "x") + [ testCase "capture test 1: DFI" $ eval dfi @?= App (Var "y") (Var "y") + , testCase "capture test 2: ttttt" $ eval ttttt @?= Var "y" + , testCase "invoking a continuation replaces the current continuation" $ eval cc1 @?= Var "z" + , testCase "callcc actually captures the current continuation" $ eval cc2 @?= App (Var "y") (Var "x") ] , testGroup "Parser tests" [ testGroup "Unit tests" - [ testCase "identity" $ parseExpression "\\x.x" @?= Right (Abstraction "x" $ Variable "x") - , testCase "unary application" $ parseExpression "(x)" @?= Right (Variable "x") - , testCase "application shorthand" $ parseExpression "a b c d" @?= Right (Application (Application (Application (Variable "a") (Variable "b")) (Variable "c")) (Variable "d")) - , testCase "let" $ parseExpression "let x = \\y.y in x" @?= Right (Application (Abstraction "x" (Variable "x")) (Abstraction "y" (Variable "y"))) - , testCase "multi-let" $ parseExpression "let x = y; y = z in x y" @?= Right (Application (Abstraction "x" (Application (Abstraction "y" (Application (Variable "x") (Variable "y"))) (Variable "z"))) (Variable "y")) - , testCase "ttttt" $ parseExpression "(\\T f x.(T (T (T (T T)))) f x) (\\f x.f (f x)) (\\x.x) y" + [ testCase "identity" $ parseEval "\\x.x" @?= Right (Abs "x" $ Var "x") + , testCase "unary application" $ parseEval "(x)" @?= Right (Var "x") + , testCase "application shorthand" $ parseEval "a b c d" @?= Right (App (App (App (Var "a") (Var "b")) (Var "c")) (Var "d")) + , testCase "let" $ parseEval "let x = \\y.y in x" @?= Right (App (Abs "x" (Var "x")) (Abs "y" (Var "y"))) + , testCase "multi-let" $ parseEval "let x = y; y = z in x y" @?= Right (App (Abs "x" (App (Abs "y" (App (Var "x") (Var "y"))) (Var "z"))) (Var "y")) + , testCase "ttttt" $ parseEval "(\\T f x.(T (T (T (T T)))) f x) (\\f x.f (f x)) (\\x.x) y" @?= Right ttttt , testGroup "Redundant whitespace" - [ testCase "around variable" $ parseExpression " x " @?= Right (Variable "x") - , testCase "around lambda" $ parseExpression " \\ x y . x " @?= Right (Abstraction "x" $ Abstraction "y" $ Variable "x") - , testCase "around application" $ parseExpression " ( x (y ) ) " @?= Right (Application (Variable "x") (Variable "y")) - , testCase "around let" $ parseExpression " let x=(y)in x " @?= Right (Application (Abstraction "x" (Variable "x")) (Variable "y")) + [ testCase "around variable" $ parseEval " x " @?= Right (Var "x") + , testCase "around lambda" $ parseEval " \\ x y . x " @?= Right (Abs "x" $ Abs "y" $ Var "x") + , testCase "around application" $ parseEval " ( x (y ) ) " @?= Right (App (Var "x") (Var "y")) + , testCase "around let" $ parseEval " let x=(y)in x " @?= Right (App (Abs "x" (Var "x")) (Var "y")) ] ] ]