From 9ef9a8b6baaf5071bdb9bc2d52db79d859cb4461 Mon Sep 17 00:00:00 2001 From: William Ball Date: Thu, 14 Nov 2024 22:02:04 -0800 Subject: [PATCH] converted to `Text` --- app/Main.hs | 9 ++++--- dependent-lambda.cabal | 60 ++++++++++++++++++++++++------------------ lib/Check.hs | 14 +++++----- lib/Expr.hs | 41 ++++++++++++++++------------- lib/Parser.hs | 28 ++++++++++---------- tests/ParserTests.hs | 2 ++ 6 files changed, 85 insertions(+), 69 deletions(-) diff --git a/app/Main.hs b/app/Main.hs index cea0ec7..c1f0c34 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -3,16 +3,17 @@ module Main where import Check import Expr import Parser +import qualified Data.Text.IO as T import System.IO main :: IO () main = do - _ <- putStr "> " + _ <- T.putStr "> " _ <- hFlush stdout - input <- getLine + input <- T.getLine case pAll input of - Left err -> putStrLn err + Left err -> T.putStrLn err Right expr -> case findType [] expr of - Right ty -> putStrLn $ pretty expr ++ " : " ++ pretty ty + Right ty -> T.putStrLn $ pretty expr <> " : " <> pretty ty Left err -> print err main diff --git a/dependent-lambda.cabal b/dependent-lambda.cabal index 9e8c94c..fdf69fc 100644 --- a/dependent-lambda.cabal +++ b/dependent-lambda.cabal @@ -28,38 +28,46 @@ extra-doc-files: CHANGELOG.md -- extra-source-files: library dependent-lambda-lib - exposed-modules: Check - Parser - Expr + exposed-modules: Check + Parser + Expr - hs-source-dirs: lib - build-depends: base ^>=4.19.1.0 - , megaparsec - , text - , parser-combinators - , mtl - default-language: Haskell2010 + hs-source-dirs: lib + build-depends: base ^>=4.19.1.0 + , megaparsec + , text + , parser-combinators + , mtl + default-language: Haskell2010 + default-extensions: OverloadedStrings + , GADTs common warnings ghc-options: -Wall executable dependent-lambda - import: warnings - main-is: Main.hs + import: warnings + main-is: Main.hs - build-depends: base ^>=4.19.1.0 - , dependent-lambda-lib - hs-source-dirs: app - default-language: Haskell2010 + build-depends: base ^>=4.19.1.0 + , dependent-lambda-lib + , text + hs-source-dirs: app + default-language: Haskell2010 + default-extensions: OverloadedStrings + , GADTs test-suite tests - type: exitcode-stdio-1.0 - main-is: Tests.hs - other-modules: ExprTests - , ParserTests - , CheckTests - build-depends: base ^>=4.19.1.0 - , HUnit - , dependent-lambda-lib - hs-source-dirs: tests - default-language: Haskell2010 + type: exitcode-stdio-1.0 + main-is: Tests.hs + other-modules: ExprTests + , ParserTests + , CheckTests + build-depends: base ^>=4.19.1.0 + , HUnit + , text + , dependent-lambda-lib + hs-source-dirs: tests + default-language: Haskell2010 + default-extensions: OverloadedStrings + , GADTs diff --git a/lib/Check.hs b/lib/Check.hs index 10e1160..aca307c 100644 --- a/lib/Check.hs +++ b/lib/Check.hs @@ -1,21 +1,23 @@ module Check (TypeCheckError (..), CheckResult (..), findType) where -import Control.Monad.Except ( MonadError(throwError) ) +import Control.Monad.Except (MonadError (throwError)) import Data.List (intercalate, (!?)) +import Data.Text (Text) +import qualified Data.Text as T import Control.Monad (unless) import Expr type Context = [Expr] -data TypeCheckError = SquareUntyped | UnboundVariable String | NotASort Expr Expr | ExpectedPiType Expr Expr | NotEquivalent Expr Expr Expr +data TypeCheckError = SquareUntyped | UnboundVariable Text | NotASort Expr Expr | ExpectedPiType Expr Expr | NotEquivalent Expr Expr Expr deriving (Eq) instance Show TypeCheckError where show SquareUntyped = "□ does not have a type" - show (UnboundVariable x) = "Unbound variable: " ++ x - show (NotASort x t) = "Expected " ++ pretty x ++ " to have type * or □, instead found " ++ pretty t - show (ExpectedPiType m a) = pretty m ++ " : " ++ pretty a ++ " is not a function" - show (NotEquivalent a a' e) = "Cannot unify " ++ pretty a ++ " with " ++ pretty a' ++ " when evaluating " ++ pretty e + 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 m a) = prettyS m ++ " : " ++ prettyS a ++ " is not a function" + show (NotEquivalent a a' e) = "Cannot unify " ++ prettyS a ++ " with " ++ prettyS a' ++ " when evaluating " ++ prettyS e type CheckResult = Either TypeCheckError diff --git a/lib/Expr.hs b/lib/Expr.hs index d444a24..d199974 100644 --- a/lib/Expr.hs +++ b/lib/Expr.hs @@ -1,16 +1,16 @@ -{-# LANGUAGE GADTs #-} - module Expr where import Data.Function (on) +import Data.Text (Text) +import qualified Data.Text as T data Expr where - Var :: Integer -> String -> Expr + Var :: Integer -> Text -> Expr Star :: Expr Square :: Expr App :: Expr -> Expr -> Expr - Abs :: String -> Expr -> Expr -> Expr - Pi :: String -> Expr -> Expr -> Expr + Abs :: Text -> Expr -> Expr -> Expr + Pi :: Text -> Expr -> Expr -> Expr deriving (Show) instance Eq Expr where @@ -32,58 +32,61 @@ occursFree n (Pi _ a b) = occursFree n a || occursFree (n + 1) b {- --------------------- PRETTY PRINTING ----------------------------- -} -parenthesize :: String -> String -parenthesize s = "(" ++ s ++ ")" +parenthesize :: Text -> Text +parenthesize s = T.concat ["(", s, ")"] -collectLambdas :: Expr -> ([(String, Expr)], Expr) +collectLambdas :: Expr -> ([(Text, Expr)], Expr) collectLambdas (Abs x ty body) = ((x, ty) : params, final) where (params, final) = collectLambdas body collectLambdas e = ([], e) -collectPis :: Expr -> ([(String, Expr)], Expr) +collectPis :: Expr -> ([(Text, Expr)], Expr) collectPis p@(Pi "" _ _) = ([], p) collectPis (Pi x ty body) = ((x, ty) : params, final) where (params, final) = collectPis body collectPis e = ([], e) -groupParams :: [(String, Expr)] -> [([String], Expr)] +groupParams :: [(Text, Expr)] -> [([Text], Expr)] groupParams = foldr addParam [] where - addParam :: (String, Expr) -> [([String], Expr)] -> [([String], Expr)] + addParam :: (Text, Expr) -> [([Text], Expr)] -> [([Text], Expr)] addParam (x, t) [] = [([x], t)] addParam (x, t) l@((xs, s) : rest) | incIndices t == s = (x : xs, t) : rest | otherwise = ([x], t) : l -showParamGroup :: ([String], Expr) -> String -showParamGroup (ids, ty) = parenthesize $ unwords ids ++ " : " ++ pretty ty +showParamGroup :: ([Text], Expr) -> Text +showParamGroup (ids, ty) = parenthesize $ T.unwords ids <> " : " <> pretty ty -helper :: Integer -> Expr -> String +helper :: Integer -> Expr -> Text helper _ (Var _ s) = s helper _ Star = "*" helper _ Square = "□" helper k (App e1 e2) = if k > 3 then parenthesize res else res where - res = helper 3 e1 ++ " " ++ helper 4 e2 + res = helper 3 e1 <> " " <> helper 4 e2 helper k (Pi "" t1 t2) = if k > 2 then parenthesize res else res where - res = helper 3 t1 ++ " -> " ++ helper 2 t2 + res = helper 3 t1 <> " -> " <> helper 2 t2 helper k e@(Pi{}) = if k > 2 then parenthesize res else res where (params, body) = collectPis e grouped = showParamGroup <$> groupParams params - res = "∏ " ++ unwords grouped ++ " . " ++ pretty body + res = "∏ " <> T.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 = "λ " ++ unwords grouped ++ " . " ++ pretty body + res = "λ " <> T.unwords grouped <> " . " <> pretty body -pretty :: Expr -> String +pretty :: Expr -> Text pretty = helper 0 +prettyS :: Expr -> String +prettyS = T.unpack . pretty + {- --------------- ACTUAL MATH STUFF ---------------- -} isSort :: Expr -> Bool diff --git a/lib/Parser.hs b/lib/Parser.hs index cddd6f3..5a6859f 100644 --- a/lib/Parser.hs +++ b/lib/Parser.hs @@ -7,20 +7,22 @@ import Data.Functor.Identity import Data.List (elemIndex) import Data.List.NonEmpty (NonEmpty ((:|))) import qualified Data.List.NonEmpty as NE +import Data.Text (Text) +import qualified Data.Text as T import Expr (Expr (..), incIndices) import Text.Megaparsec hiding (State) import Text.Megaparsec.Char import qualified Text.Megaparsec.Char.Lexer as L -type InnerState = [String] +type InnerState = [Text] -data CustomErrors = UnboundVariable String [String] deriving (Eq, Ord, Show) +data CustomErrors = UnboundVariable Text [Text] deriving (Eq, Ord, Show) instance ShowErrorComponent CustomErrors where showErrorComponent (UnboundVariable var bound) = - "Unbound variable: " ++ var ++ ". Did you mean one of: " ++ unwords bound ++ "?" + "Unbound variable: " ++ T.unpack var ++ ". Did you mean one of: " ++ T.unpack (T.unwords bound) ++ "?" -type Parser = ParsecT CustomErrors String (State InnerState) +type Parser = ParsecT CustomErrors Text (State InnerState) skipSpace :: Parser () skipSpace = @@ -32,11 +34,11 @@ skipSpace = lexeme :: Parser a -> Parser a lexeme = L.lexeme skipSpace -pIdentifier :: Parser String +pIdentifier :: Parser Text pIdentifier = label "identifier" $ lexeme $ do firstChar <- letterChar <|> char '_' rest <- many $ alphaNumChar <|> char '_' - return $ firstChar : rest + return $ T.pack (firstChar : rest) -- Still need T.pack here as we're building from chars pVar :: Parser Expr pVar = label "variable" $ lexeme $ do @@ -46,12 +48,10 @@ pVar = label "variable" $ lexeme $ do Just i -> return $ Var (fromIntegral i) var Nothing -> customFailure $ UnboundVariable var binders -defChoice :: NE.NonEmpty String -> Parser () -defChoice options = lexeme $ label labelText $ void $ choice $ NE.map string options - where - labelText = NE.head options +defChoice :: NE.NonEmpty Text -> Parser () +defChoice options = lexeme $ label (T.unpack $ NE.head options) $ void $ choice $ NE.map chunk options -pParamGroup :: Parser [(String, Expr)] +pParamGroup :: Parser [(Text, Expr)] pParamGroup = lexeme $ label "parameter group" $ between (char '(') (char ')') $ do idents <- some pIdentifier _ <- defChoice $ ":" :| [] @@ -59,7 +59,7 @@ pParamGroup = lexeme $ label "parameter group" $ between (char '(') (char ')') $ modify (flip (foldl $ flip (:)) idents) pure $ zip idents (iterate incIndices ty) -pParams :: Parser [(String, Expr)] +pParams :: Parser [(Text, Expr)] pParams = concat <$> some pParamGroup pLAbs :: Parser Expr @@ -112,5 +112,5 @@ pAppTerm = lexeme $ pLAbs <|> pPAbs <|> pApp pExpr :: Parser Expr pExpr = lexeme $ try pArrow <|> pAppTerm -pAll :: String -> Either String Expr -pAll input = first errorBundlePretty $ fst $ runIdentity $ runStateT (runParserT pExpr "" input) [] +pAll :: Text -> Either Text Expr +pAll input = first (T.pack . errorBundlePretty) $ fst $ runIdentity $ runStateT (runParserT pExpr "" input) [] diff --git a/tests/ParserTests.hs b/tests/ParserTests.hs index 8e8d916..bb620ca 100644 --- a/tests/ParserTests.hs +++ b/tests/ParserTests.hs @@ -1,5 +1,7 @@ module ParserTests (tests) where +import Data.Text (Text) +import qualified Data.Text as T import Expr (Expr (..)) import Parser (pAll) import Test.HUnit