wball/perga
1
0
Fork 0
Code Issues 15 Pull requests Projects Releases Packages Wiki Activity Actions

converted to Text

Browse source
This commit is contained in:
William Ball 2024-11-14 22:02:04 -08:00
parent c73566d67f
commit 9ef9a8b6ba
6 changed files with 85 additions and 69 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
app/Main.hs
View file

@ -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

60
dependent-lambda.cabal
View file

@ -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

14
lib/Check.hs
View file

@ -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

41
lib/Expr.hs
View file

@ -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

28
lib/Parser.hs
View file

@ -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) []

2
tests/ParserTests.hs
View file

@ -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