From 5234f43194e32fd08757a0f260f9f85b1f11b230 Mon Sep 17 00:00:00 2001 From: William Ball Date: Fri, 22 Nov 2024 19:44:31 -0800 Subject: [PATCH] port to relude + a lot of cleanup --- app/Main.hs | 5 +- app/Repl.hs | 23 +++---- lib/Check.hs | 36 +++++----- lib/Errors.hs | 21 +++--- lib/Eval.hs | 45 ++++++++----- lib/Expr.hs | 28 ++++---- lib/Parser.hs | 158 +++++++++++++++++++++----------------------- lib/Preprocessor.hs | 22 +++--- perga.cabal | 16 +++-- 9 files changed, 176 insertions(+), 178 deletions(-) diff --git a/app/Main.hs b/app/Main.hs index f8396c9..be29682 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -1,11 +1,8 @@ module Main where -import Control.Monad (void) -import Control.Monad.Except import Eval (Env, emptyEnv) import Parser (handleFile) import Repl -import System.Environment main :: IO () main = do @@ -15,5 +12,5 @@ main = do files -> handleFiles emptyEnv files handleFiles :: Env -> [String] -> IO () -handleFiles _ [] = putStrLn "success!" +handleFiles _ [] = putTextLn "success!" handleFiles env (file : rest) = runExceptT (handleFile env file) >>= either putStrLn (`handleFiles` rest) diff --git a/app/Repl.hs b/app/Repl.hs index a529ecd..9d781bb 100644 --- a/app/Repl.hs +++ b/app/Repl.hs @@ -1,10 +1,9 @@ module Repl (repl, showEnvEntry) where -import Control.Monad.Except -import Control.Monad.Reader -import Data.List (isPrefixOf, stripPrefix) -import qualified Data.Map as M -import qualified Data.Text as T +import Check (findType) +import Data.List (stripPrefix) +import qualified Data.Map.Strict as M +import Data.Text (pack) import Errors (Result) import Eval import Expr @@ -38,24 +37,24 @@ parseCommand (Just input) handleInput :: Env -> String -> InputT IO Env handleInput env input = - let (res, env') = parseDefEmpty env (T.pack input) + let (res, env') = parseDefEmpty env (pack input) in case res of Left err -> outputStrLn err >> pure env' Right () -> pure env' actOnParse :: Env -> String -> (Expr -> InputT IO ()) -> InputT IO () -actOnParse env input action = case parseExpr env (T.pack input) of +actOnParse env input action = case parseExpr env (pack input) of Left err -> outputStrLn err Right expr -> action expr printErrorOrResult :: Env -> (Expr -> ReaderT Env Result Expr) -> Expr -> InputT IO () -printErrorOrResult env action expr = outputStrLn $ either show prettyS $ runReaderT (action expr) env +printErrorOrResult env action expr = putTextLn $ either toText pretty $ runReaderT (action expr) env parseActPrint :: Env -> String -> (Expr -> ReaderT Env Result Expr) -> InputT IO () parseActPrint env input action = actOnParse env input (printErrorOrResult env action) -lookupAct :: Env -> String -> (EnvLine -> InputT IO ()) -> InputT IO () -lookupAct env input action = maybe (outputStrLn $ "'" ++ input ++ "' unbound") action $ M.lookup (T.pack input) env +lookupAct :: Env -> String -> (Definition -> InputT IO ()) -> InputT IO () +lookupAct env input action = maybe (outputStrLn $ "'" ++ input ++ "' unbound") action $ M.lookup (pack input) env repl :: IO Env repl = do @@ -72,8 +71,8 @@ repl = do Nothing -> pure env Just Quit -> pure env Just DumpEnv -> lift (dumpEnv env) >> loop env - Just (TypeQuery input) -> lookupAct env input (outputStrLn . prettyS . _ty) >> loop env - Just (ValueQuery input) -> lookupAct env input (outputStrLn . prettyS . _val) >> loop env + Just (TypeQuery input) -> parseActPrint env input (findType []) >> loop env + Just (ValueQuery input) -> lookupAct env input (putTextLn . pretty . _val) >> loop env Just (Normalize input) -> parseActPrint env input normalize >> loop env Just (WeakNormalize input) -> parseActPrint env input whnf >> loop env Just (LoadFile filename) -> lift (runExceptT $ handleFile env filename) >>= either ((>> loop env) . outputStrLn) loop diff --git a/lib/Check.hs b/lib/Check.hs index 4b2b3a2..f451af8 100644 --- a/lib/Check.hs +++ b/lib/Check.hs @@ -1,10 +1,8 @@ {-# LANGUAGE LambdaCase #-} -module Check (checkType) where +module Check (checkType, findType) where -import Control.Monad (unless) import Control.Monad.Except (MonadError (throwError)) -import Control.Monad.Reader import Data.List ((!?)) import Errors import Eval (Env, betaEquiv, envLookupTy, isSort, subst, whnf) @@ -18,15 +16,24 @@ matchPi x mt = (Pi _ a b) -> pure (a, b) t -> throwError $ ExpectedPiType x t +validateType :: Context -> Expr -> ReaderT Env Result Expr +validateType g a = do + s <- findType g a + isSort s >>= flip unless (throwError $ NotASort a s) + pure s + +validateType_ :: Context -> Expr -> ReaderT Env Result () +validateType_ g a = void $ validateType g a + findType :: Context -> Expr -> ReaderT Env Result Expr findType _ Star = pure Square findType _ Square = throwError SquareUntyped -findType g (Var n x) = do - t <- maybe (throwError $ UnboundVariable x) pure $ g !? fromInteger n - (sSort, s) <- findType g t >>= isSort - unless sSort $ throwError $ NotASort t s +findType g (Var x n) = do + t <- g !? fromInteger n `whenNothing` throwError (UnboundVariable x) + validateType_ g t pure t -findType _ (Free n) = envLookupTy n +findType _ (Free n) = do + envLookupTy n findType _ (Axiom n) = envLookupTy n findType g e@(App m n) = do (a, b) <- findType g m >>= matchPi m @@ -35,18 +42,13 @@ findType g e@(App m n) = do unless equiv $ throwError $ NotEquivalent a a' e pure $ subst 0 n b findType g (Abs x a m) = do - (s1Sort, s1) <- findType g a >>= isSort - unless s1Sort $ throwError $ NotASort a s1 + validateType_ g a b <- findType (incIndices a : map incIndices g) m - (s2Sort, s2) <- findType g (Pi x a b) >>= isSort - unless s2Sort $ throwError $ NotASort (Pi x a b) s2 + validateType_ g (Pi x a b) pure $ if occursFree 0 b then Pi x a b else Pi "" a b findType g (Pi _ a b) = do - (s1Sort, s1) <- findType g a >>= isSort - unless s1Sort $ throwError $ NotASort a s1 - (s2Sort, s2) <- findType (incIndices a : map incIndices g) b >>= isSort - unless s2Sort $ throwError $ NotASort b s2 - pure s2 + validateType_ g a + validateType (incIndices a : map incIndices g) b checkType :: Env -> Expr -> Result Expr checkType env t = runReaderT (findType [] t) env diff --git a/lib/Errors.hs b/lib/Errors.hs index fc216d7..3df35d3 100644 --- a/lib/Errors.hs +++ b/lib/Errors.hs @@ -1,7 +1,5 @@ module Errors where -import Data.Text (Text) -import qualified Data.Text as T import Expr data Error @@ -14,13 +12,16 @@ data Error | DuplicateDefinition Text deriving (Eq, Ord) -instance Show Error where - show SquareUntyped = "□ does not have a type" - show (UnboundVariable x) = "Unbound variable: '" ++ T.unpack x ++ "'" - show (NotASort x t) = "Expected '" ++ prettyS x ++ "' to have type * or □, instead found '" ++ prettyS t ++ "'" - show (ExpectedPiType x t) = "'" ++ prettyS x ++ "' : '" ++ prettyS t ++ "' is not a function" - show (NotEquivalent a a' e) = "Cannot unify '" ++ prettyS a ++ "' with '" ++ prettyS a' ++ "' when evaluating '" ++ prettyS e ++ "'" - show (PNMissingType x) = "Axiom '" ++ T.unpack x ++ "' missing type ascription" - show (DuplicateDefinition n) = "'" ++ T.unpack n ++ "' already defined" +instance ToText Error where + toText SquareUntyped = "□ does not have a type" + toText (UnboundVariable x) = "Unbound variable: '" <> x <> "'" + toText (NotASort x t) = "Expected '" <> pretty x <> "' to have type * or □, instead found '" <> pretty t <> "'" + toText (ExpectedPiType x t) = "'" <> pretty x <> "' : '" <> pretty t <> "' is not a function" + toText (NotEquivalent a a' e) = "Cannot unify '" <> pretty a <> "' with '" <> pretty a' <> "' when evaluating '" <> pretty e <> "'" + toText (PNMissingType x) = "Axiom '" <> x <> "' missing type ascription" + toText (DuplicateDefinition n) = "'" <> n <> "' already defined" + +instance ToString Error where + toString = toString . toText type Result = Either Error diff --git a/lib/Eval.hs b/lib/Eval.hs index f8d6062..de6935e 100644 --- a/lib/Eval.hs +++ b/lib/Eval.hs @@ -1,34 +1,45 @@ -{-# LANGUAGE TupleSections #-} +{-# LANGUAGE NamedFieldPuns #-} module Eval where -import Control.Monad (void) -import Control.Monad.Except (MonadError (..)) -import Control.Monad.Reader -import qualified Data.Map as M -import Data.Text (Text) -import qualified Data.Text as T +import Control.Monad.Error.Class +import qualified Data.Map.Strict as M import Errors import Expr +import Relude.Extra.Lens -data EnvLine = EL {_ty :: Expr, _val :: Expr} -type Env = M.Map Text EnvLine +data Definition = Def {_ty :: Expr, _val :: Expr} + +makeDef :: Expr -> Expr -> Definition +makeDef typ value = Def{_ty = typ, _val = value} + +tyL :: Lens' Definition Expr +tyL = lens _ty setter + where + setter (Def{_val}) new = Def{_val, _ty = new} + +valL :: Lens' Definition Expr +valL = lens _val setter + where + setter (Def{_ty}) new = Def{_val = new, _ty} + +type Env = Map Text Definition emptyEnv :: Env emptyEnv = M.empty -showEnvEntry :: Text -> EnvLine -> String -showEnvEntry k EL{_ty = t} = T.unpack k ++ " : " ++ prettyS t +showEnvEntry :: Text -> Definition -> Text +showEnvEntry k Def{_ty = t} = k <> " : " <> pretty t dumpEnv :: Env -> IO () -dumpEnv = void . M.traverseWithKey ((putStrLn .) . showEnvEntry) +dumpEnv = void . M.traverseWithKey ((putTextLn .) . showEnvEntry) -- substitute s for k *AND* decrement indices; only use after reducing a redex. subst :: Integer -> Expr -> Expr -> Expr -subst k s (Var n x) +subst k s (Var x n) | k == n = s - | n > k = Var (n - 1) x - | otherwise = Var n x + | n > k = Var x (n - 1) + | otherwise = Var x n subst _ _ (Free s) = Free s subst _ _ (Axiom s) = Axiom s subst _ _ Star = Star @@ -95,5 +106,5 @@ isSortPure Star = True isSortPure Square = True isSortPure _ = False -isSort :: Expr -> ReaderT Env Result (Bool, Expr) -isSort s = (,s) . isSortPure <$> whnf s +isSort :: Expr -> ReaderT Env Result Bool +isSort = fmap isSortPure . whnf diff --git a/lib/Expr.hs b/lib/Expr.hs index 79ca2dc..c006b27 100644 --- a/lib/Expr.hs +++ b/lib/Expr.hs @@ -1,11 +1,7 @@ module Expr where -import Data.Function (on) -import Data.Text (Text) -import qualified Data.Text as T - data Expr where - Var :: Integer -> Text -> Expr + Var :: Text -> Integer -> Expr Free :: Text -> Expr Axiom :: Text -> Expr Star :: Expr @@ -16,7 +12,7 @@ data Expr where deriving (Show, Ord) instance Eq Expr where - (Var n _) == (Var m _) = n == m + (Var _ n) == (Var _ m) = n == m (Free s) == (Free t) = s == t (Axiom a) == (Axiom b) = a == b Star == Star = True @@ -27,7 +23,7 @@ instance Eq Expr where _ == _ = False occursFree :: Integer -> Expr -> Bool -occursFree n (Var k _) = n == k +occursFree n (Var _ k) = n == k occursFree _ (Free _) = False occursFree _ (Axiom _) = False occursFree _ Star = False @@ -37,9 +33,9 @@ occursFree n (Abs _ a b) = occursFree n a || occursFree (n + 1) b occursFree n (Pi _ a b) = occursFree n a || occursFree (n + 1) b shiftIndices :: Integer -> Integer -> Expr -> Expr -shiftIndices d c (Var k x) - | k >= c = Var (k + d) x - | otherwise = Var k x +shiftIndices d c (Var x k) + | k >= c = Var x (k + d) + | otherwise = Var x k shiftIndices _ _ (Free s) = Free s shiftIndices _ _ (Axiom s) = Axiom s shiftIndices _ _ Star = Star @@ -54,7 +50,7 @@ incIndices = shiftIndices 1 0 {- --------------------- PRETTY PRINTING ----------------------------- -} parenthesize :: Text -> Text -parenthesize s = T.concat ["(", s, ")"] +parenthesize s = "(" <> s <> ")" collectLambdas :: Expr -> ([(Text, Expr)], Expr) collectLambdas (Abs x ty body) = ((x, ty) : params, final) @@ -87,10 +83,10 @@ groupParams = foldr addParam [] | otherwise = ([x], t) : l showParamGroup :: ([Text], Expr) -> Text -showParamGroup (ids, ty) = parenthesize $ T.unwords ids <> " : " <> pretty ty +showParamGroup (ids, ty) = parenthesize $ unwords ids <> " : " <> pretty ty helper :: Integer -> Expr -> Text -helper _ (Var _ s) = s +helper _ (Var s _) = s helper _ (Free s) = s helper _ (Axiom s) = s helper _ Star = "*" @@ -105,15 +101,15 @@ helper k e@(Pi{}) = if k > 2 then parenthesize res else res where (params, body) = collectPis e grouped = showParamGroup <$> groupParams params - res = "∏ " <> T.unwords grouped <> " . " <> pretty body + res = "∏ " <> unwords grouped <> " . " <> pretty body helper k e@(Abs{}) = if k >= 1 then parenthesize res else res where (params, body) = collectLambdas e grouped = showParamGroup <$> groupParams params - res = "λ " <> T.unwords grouped <> " . " <> pretty body + res = "λ " <> unwords grouped <> " . " <> pretty body pretty :: Expr -> Text pretty = helper 0 . cleanNames prettyS :: Expr -> String -prettyS = T.unpack . pretty +prettyS = toString . pretty diff --git a/lib/Parser.hs b/lib/Parser.hs index 7f97907..04709bf 100644 --- a/lib/Parser.hs +++ b/lib/Parser.hs @@ -3,42 +3,38 @@ module Parser (parseDef, parseDefEmpty, parseExpr, parseProgram, handleFile) where import Check -import Control.Monad import Control.Monad.Except -import Control.Monad.State.Strict -import Data.Bifunctor (first) -import Data.List (elemIndex) -import Data.List.NonEmpty (NonEmpty ((:|))) -import qualified Data.List.NonEmpty as NE -import qualified Data.Map as M -import Data.Text (Text) +import Data.List (elemIndex, foldl, foldl1) +import qualified Data.Map.Strict as M import qualified Data.Text as T import Errors (Error (..)) import Eval import Expr (Expr (..), incIndices) import Preprocessor -import Text.Megaparsec hiding (State) +import Relude.Extra.Lens +import Text.Megaparsec (ParsecT, ShowErrorComponent (..), between, choice, chunk, customFailure, errorBundlePretty, label, runParserT, try) import Text.Megaparsec.Char import qualified Text.Megaparsec.Char.Lexer as L -data TypeDef = TD {_ident :: Text, _type :: Expr} -data DefinitionLine = DL {_td :: TypeDef, _body :: Expr} | PN TypeDef +data InnerState = IS {_binders :: [Text], _env :: Env} -data InnerState = IS {_binds :: [TypeDef], _env :: Env} +bindsL :: Lens' InnerState [Text] +bindsL = lens _binders setter + where + setter (IS{_env}) new = IS{_env, _binders = new} + +envL :: Lens' InnerState Env +envL = lens _env setter + where + setter (IS{_binders}) new = IS{_env = new, _binders} newtype TypeError = TE Error - deriving (Eq, Ord, Show) + deriving (Eq, Ord) type Parser = ParsecT TypeError Text (State InnerState) instance ShowErrorComponent TypeError where - showErrorComponent (TE e) = show e - -bindsToIS :: ([TypeDef] -> [TypeDef]) -> InnerState -> InnerState -bindsToIS f x@(IS{_binds}) = x{_binds = f _binds} - -modifyEnv :: (Env -> Env) -> InnerState -> InnerState -modifyEnv f x@(IS{_env}) = x{_env = f _env} + showErrorComponent (TE e) = toString e skipSpace :: Parser () skipSpace = @@ -50,6 +46,9 @@ skipSpace = lexeme :: Parser a -> Parser a lexeme = L.lexeme skipSpace +eat :: Text -> Parser () +eat = void . lexeme . chunk + pIdentifier :: Parser Text pIdentifier = label "identifier" $ lexeme $ do firstChar <- letterChar <|> char '_' @@ -58,24 +57,19 @@ pIdentifier = label "identifier" $ lexeme $ do pVar :: Parser Expr pVar = label "variable" $ lexeme $ do - var <- pIdentifier - binders <- map _ident . _binds <$> get - pure $ case elemIndex var binders of - Just i -> Var (fromIntegral i) var - Nothing -> Free var + name <- pIdentifier + binders <- view bindsL <$> get + pure (Var name . fromIntegral <$> elemIndex name binders ?: Free name) -pPN :: Parser () -pPN = label "primitive notion" $ lexeme $ defChoice $ pure "axiom" - -defChoice :: NE.NonEmpty Text -> Parser () -defChoice options = lexeme $ label (T.unpack $ NE.head options) $ void $ choice $ NE.map chunk options +defChoice :: NonEmpty Text -> Parser () +defChoice options = lexeme $ label (T.unpack $ head options) $ void $ choice $ fmap chunk options pParamGroup :: Parser [(Text, Expr)] pParamGroup = lexeme $ label "parameter group" $ between (char '(') (char ')') $ do idents <- some pIdentifier - _ <- defChoice $ pure ":" + eat ":" ty <- pExpr - modify $ bindsToIS $ flip (foldl $ flip (:)) (map (\idt -> TD{_ident = idt, _type = ty}) idents) + modify $ over bindsL $ flip (foldl $ flip (:)) idents pure $ zip idents (iterate incIndices ty) pSomeParams :: Parser [(Text, Expr)] @@ -84,22 +78,27 @@ pSomeParams = lexeme $ concat <$> some pParamGroup pManyParams :: Parser [(Text, Expr)] pManyParams = lexeme $ concat <$> many pParamGroup +withBinders :: Parser a -> Parser a +withBinders parser = do + oldBinders <- view bindsL <$> get + result <- parser + modify $ set bindsL oldBinders + pure result + pLAbs :: Parser Expr -pLAbs = lexeme $ label "λ-abstraction" $ do +pLAbs = lexeme $ label "λ-abstraction" $ withBinders $ do _ <- defChoice $ "λ" :| ["fun"] params <- pSomeParams _ <- defChoice $ "=>" :| ["⇒"] body <- pExpr - modify $ bindsToIS $ drop $ length params pure $ foldr (uncurry Abs) body params pPAbs :: Parser Expr -pPAbs = lexeme $ label "Π-abstraction" $ do +pPAbs = lexeme $ label "Π-abstraction" $ withBinders $ do _ <- defChoice $ "∏" :| ["forall", "∀"] params <- pSomeParams _ <- defChoice $ pure "," body <- pExpr - modify $ bindsToIS $ drop $ length params pure $ foldr (uncurry Pi) body params pArrow :: Parser Expr @@ -112,61 +111,49 @@ pApp :: Parser Expr pApp = lexeme $ foldl1 App <$> some pTerm pStar :: Parser Expr -pStar = lexeme $ Star <$ defChoice (pure "*") +pStar = lexeme $ Star <$ eat "*" pSquare :: Parser Expr pSquare = lexeme $ Square <$ defChoice ("□" :| ["[]"]) -checkAscription :: Text -> Expr -> Maybe Expr -> Parser DefinitionLine +checkAscription :: Text -> Expr -> Maybe Expr -> Parser () checkAscription ident value massert = do - IS{_env} <- get - case (checkType _env value, massert) of - (Left err, _) -> customFailure $ TE err - (Right ty, Nothing) -> pure DL{_td = TD{_ident = ident, _type = ty}, _body = value} - (Right ty, Just assert) -> case checkBeta _env ty assert of - Left err -> customFailure $ TE err - Right equiv -> do - unless equiv $ customFailure $ TE $ NotEquivalent ty assert value - pure DL{_td = TD{_ident = ident, _type = assert}, _body = value} - -updateStateDefinition :: DefinitionLine -> Parser () -updateStateDefinition DL{_td, _body} = do env <- get - let ident = _ident _td - when (M.member ident (_env env)) (customFailure $ TE $ DuplicateDefinition ident) - modify $ - modifyEnv - (M.insert ident EL{_ty = _type _td, _val = _body}) -updateStateDefinition (PN TD{_type, _ident}) = do - env <- get - when (M.member _ident (_env env)) (customFailure $ TE $ DuplicateDefinition _ident) - modify $ - modifyEnv - (M.insert _ident EL{_ty = _type, _val = Axiom _ident}) + ty <- either (customFailure . TE) pure (checkType (env ^. envL) value) + case massert of + Nothing -> updateStateDefinition ident ty value + Just assert -> do + equiv <- either (customFailure . TE) pure (checkBeta (env ^. envL) ty assert) + unless equiv $ customFailure $ TE $ NotEquivalent ty assert value + updateStateDefinition ident assert value -pDef :: Parser DefinitionLine +updateStateDefinition :: Text -> Expr -> Expr -> Parser () +updateStateDefinition ident ty value = do + env <- get + when (M.member ident (env ^. envL)) (customFailure $ TE $ DuplicateDefinition ident) + modify $ over envL $ M.insert ident $ makeDef ty value + +pAxiom :: Text -> Maybe Expr -> Parser () +pAxiom ident Nothing = customFailure $ TE $ PNMissingType ident +pAxiom ident (Just ascription) = do + eat "axiom" + eat ";" + updateStateDefinition ident ascription (Axiom ident) + +pBody :: [(Text, Expr)] -> Text -> Maybe Expr -> Parser () +pBody params ident ascription = do + value <- flip (foldr (uncurry Abs)) params <$> pExpr + checkAscription ident value ascription + eat ";" + +pDef :: Parser () pDef = lexeme $ label "definition" $ do skipSpace ident <- pIdentifier params <- pManyParams ascription <- fmap (flip (foldr (uncurry Pi)) params) <$> pAscription - _ <- defChoice $ pure ":=" - choice - [ do - _ <- pPN - _ <- defChoice $ pure ";" - case ascription of - Just ty -> pure $ PN TD{_ident = ident, _type = ty} - Nothing -> customFailure $ TE $ PNMissingType ident - , do - value <- flip (foldr (uncurry Abs)) params <$> pExpr - res <- checkAscription ident value ascription - _ <- defChoice $ pure ";" - pure res - ] - -pDefUpdate :: Parser () -pDefUpdate = pDef >>= updateStateDefinition + eat ":=" + choice [pAxiom ident ascription, pBody params ident ascription] pTerm :: Parser Expr pTerm = @@ -189,25 +176,28 @@ pAscription :: Parser (Maybe Expr) pAscription = lexeme $ optional $ try $ defChoice (pure ":") >> label "type" pExpr pProgram :: Parser Env -pProgram = lexeme $ skipSpace >> many pDefUpdate >> _env <$> get +pProgram = lexeme $ skipSpace >> many pDef >> _env <$> get + +emptyBinders :: Env -> InnerState +emptyBinders env = IS{_binders = [], _env = env} parseDef :: Text -> State Env (Either String ()) parseDef input = do env <- get - let (output, IS{_env}) = runState (runParserT pDefUpdate "" input) (IS{_binds = [], _env = env}) + let (output, IS{_env}) = runState (runParserT pDef "" input) (emptyBinders env) put _env pure $ first errorBundlePretty output parseExpr :: Env -> Text -> Either String Expr -parseExpr env input = first errorBundlePretty $ evalState (runParserT pExpr "" input) IS{_binds = [], _env = env} +parseExpr env input = first errorBundlePretty $ evalState (runParserT pExpr "" input) $ emptyBinders env parseDefEmpty :: Env -> Text -> (Either String (), Env) parseDefEmpty env input = runState (parseDef input) env parseProgram :: Env -> Text -> Either String Env -parseProgram initial input = first errorBundlePretty $ evalState (runParserT pProgram "" input) IS{_binds = [], _env = initial} +parseProgram initial input = first errorBundlePretty $ evalState (runParserT pProgram "" input) $ emptyBinders initial handleFile :: Env -> String -> ExceptT String IO Env handleFile initial filename = do - text <- show `withExceptT` preprocess filename + text <- toString `withExceptT` preprocess filename liftEither $ parseProgram initial text diff --git a/lib/Preprocessor.hs b/lib/Preprocessor.hs index 826f863..4b1db6e 100644 --- a/lib/Preprocessor.hs +++ b/lib/Preprocessor.hs @@ -1,17 +1,16 @@ module Preprocessor where import Control.Monad.Except -import Control.Monad.IO.Class -import Data.Text (Text) import qualified Data.Text as T -import qualified Data.Text.IO as TIO import System.FilePath -import System.IO newtype PreprocessorError = ParseError Text -instance Show PreprocessorError where - show (ParseError t) = "Preprocessor error on line '" ++ show t ++ "'" +instance ToText PreprocessorError where + toText (ParseError t) = "Preprocessor error on line '" <> t <> "'" + +instance ToString PreprocessorError where + toString = toString . toText type Result = Either PreprocessorError type ResultIO = ExceptT PreprocessorError IO @@ -22,16 +21,15 @@ concatMapM f (x : xs) = ((<>) . (<> "\n") <$> f x) <*> concatMapM f xs preprocess :: String -> ResultIO Text preprocess filename = do - handle <- liftIO $ openFile filename ReadMode - text <- liftIO $ T.lines <$> TIO.hGetContents handle - result <- concatMapM (preprocessLine $ takeDirectory filename) text - liftIO $ putStrLn $ "loading: " ++ filename + text <- decodeUtf8With lenientDecode <$> readFileBS filename + result <- concatMapM (preprocessLine $ takeDirectory filename) (lines text) + putStrLn $ "loading: " ++ filename pure result parseInclude :: Text -> Result Text -parseInclude line = maybe (Left $ ParseError line) pure $ T.stripPrefix "@include " line +parseInclude line = maybeToRight (ParseError line) $ T.stripPrefix "@include " line preprocessLine :: FilePath -> Text -> ResultIO Text preprocessLine base line - | "@include " `T.isPrefixOf` line = liftEither (parseInclude line) >>= preprocess . normalise . (base ) . T.unpack + | "@include " `T.isPrefixOf` line = liftEither (parseInclude line) >>= preprocess . normalise . (base ) . toString | otherwise = pure line diff --git a/perga.cabal b/perga.cabal index 12515f1..e8e41a4 100644 --- a/perga.cabal +++ b/perga.cabal @@ -34,12 +34,14 @@ library perga-lib hs-source-dirs: lib build-depends: base ^>=4.19.1.0 + , relude + , mtl , megaparsec - , text , parser-combinators , filepath - , mtl - , containers + mixins: base hiding (Prelude) + , relude (Relude as Prelude) + , relude default-language: Haskell2010 default-extensions: OverloadedStrings , GADTs @@ -50,13 +52,15 @@ executable perga other-modules: Repl build-depends: base ^>=4.19.1.0 + , relude , perga-lib - , text - , containers , haskeline + , mtl , directory , filepath - , mtl + mixins: base hiding (Prelude) + , relude (Relude as Prelude) + , relude hs-source-dirs: app default-language: Haskell2010 default-extensions: OverloadedStrings