better prettyprinting
This commit is contained in:
parent
7f9d029ff9
commit
8bc8e5e171
7 changed files with 110 additions and 79 deletions
|
|
@ -51,7 +51,7 @@ actOnParse :: String -> (Expr -> InputT IO ()) -> InputT IO ()
|
|||
actOnParse input action = either outputStrLn (action . elaborate) $ parseExpr "repl" (pack input)
|
||||
|
||||
printErrorOrResult :: Env -> (Expr -> ReaderT Env Result Expr) -> Expr -> InputT IO ()
|
||||
printErrorOrResult env action expr = putTextLn $ either toText pretty $ runReaderT (action expr) env
|
||||
printErrorOrResult env action expr = putTextLn $ either toText prettyT $ runReaderT (action expr) env
|
||||
|
||||
parseActPrint :: Env -> String -> (Expr -> ReaderT Env Result Expr) -> InputT IO ()
|
||||
parseActPrint env input action = actOnParse input (printErrorOrResult env action)
|
||||
|
|
@ -75,7 +75,7 @@ repl = do
|
|||
Just Quit -> pure env
|
||||
Just DumpEnv -> lift (dumpEnv env) >> loop env
|
||||
Just (TypeQuery input) -> parseActPrint env input (findType []) >> loop env
|
||||
Just (ValueQuery input) -> lookupAct env input (putTextLn . pretty . _val) >> loop env
|
||||
Just (ValueQuery input) -> lookupAct env input (putTextLn . prettyT . _val) >> loop env
|
||||
Just (Normalize input) -> parseActPrint env input normalize >> loop env
|
||||
Just (WeakNormalize input) -> parseActPrint env input whnf >> loop env
|
||||
Just (DumpDebug input) -> either outputStrLn (outputStrLn . show) (parseDef "repl" (pack input)) >> loop env
|
||||
|
|
|
|||
|
|
@ -3,10 +3,6 @@
|
|||
-- import basic logic definitions from <logic.pg>
|
||||
|
||||
@include logic.pg
|
||||
@include algebra.pg
|
||||
|
||||
def comp (A B C : *) (g : B -> C) (f : A -> B) (x : A) : C :=
|
||||
g (f x);
|
||||
|
||||
-- }}}
|
||||
|
||||
|
|
@ -473,7 +469,8 @@ def one_plus_one_two : eq nat (plus one one) two :=
|
|||
-- We will now prove a couple standard properties of addition.
|
||||
|
||||
-- First, associativity, namely that n + (m + p) = (n + m) + p.
|
||||
def plus_assoc : assoc nat plus := fun (n m : nat) =>
|
||||
def plus_assoc : forall (n m p : nat), eq nat (plus n (plus m p)) (plus (plus n m) p)
|
||||
:= fun (n m : nat) =>
|
||||
-- We prove this via induction on p for any fixed n and m.
|
||||
nat_ind
|
||||
(fun (p : nat) => eq nat (plus n (plus m p)) (plus (plus n m) p))
|
||||
|
|
|
|||
|
|
@ -22,7 +22,7 @@ findLevel g a = do
|
|||
whnf s >>= \case
|
||||
Level i -> pure i
|
||||
Star -> pure $ -1 -- HACK: but works, so...
|
||||
_ -> throwError $ NotASort a s
|
||||
_ -> throwError $ NotASort a
|
||||
|
||||
validateType :: Context -> Expr -> ReaderT Env Result ()
|
||||
validateType g a = void $ findLevel g a
|
||||
|
|
@ -39,9 +39,9 @@ compSort _ _ (Level i) Star
|
|||
| i == 0 = pure Star
|
||||
| otherwise = pure $ Level i
|
||||
compSort _ _ (Level i) (Level j) = pure $ Level $ max i j
|
||||
compSort a b left right
|
||||
| isSort left = throwError $ NotASort b right
|
||||
| otherwise = throwError $ NotASort a left
|
||||
compSort a b left _
|
||||
| isSort left = throwError $ NotASort b
|
||||
| otherwise = throwError $ NotASort a
|
||||
|
||||
findType :: Context -> Expr -> ReaderT Env Result Expr
|
||||
findType _ Star = pure $ Level 0
|
||||
|
|
|
|||
|
|
@ -1,25 +1,35 @@
|
|||
module Errors where
|
||||
|
||||
import Expr
|
||||
import Prettyprinter
|
||||
import Prettyprinter.Render.Text
|
||||
import Prelude hiding (group)
|
||||
|
||||
data Error
|
||||
= UnboundVariable Text
|
||||
| NotASort Expr Expr
|
||||
| NotASort Expr
|
||||
| ExpectedPiType Expr Expr
|
||||
| NotEquivalent Expr Expr Expr
|
||||
| PNMissingType Text
|
||||
| DuplicateDefinition Text
|
||||
| EmptySection Text
|
||||
deriving (Eq, Ord)
|
||||
|
||||
instance Pretty Error where
|
||||
pretty (UnboundVariable x) = "Unbound variable: '" <> pretty x <> "'"
|
||||
pretty (NotASort x) = group $ hang 4 ("Term:" <> line <> pretty x) <> line <> "is not a type"
|
||||
pretty (ExpectedPiType x t) = group $ hang 4 ("Term:" <> line <> pretty x) <> hang 4 ("is not a function, instead is type" <> line <> pretty t)
|
||||
pretty (NotEquivalent a a' e) =
|
||||
group $
|
||||
hang 4 ("Cannot unify" <> line <> pretty a)
|
||||
<> line
|
||||
<> hang 4 ("with" <> line <> pretty a')
|
||||
<> line
|
||||
<> hang 4 ("when evaluating" <> line <> pretty e)
|
||||
pretty (PNMissingType x) = "Axiom '" <> pretty x <> "' missing type ascription"
|
||||
pretty (DuplicateDefinition n) = "'" <> pretty n <> "' already defined"
|
||||
|
||||
instance ToText Error where
|
||||
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"
|
||||
toText (EmptySection var) = "Tried to declare variable " <> var <> " without a section"
|
||||
toText = renderStrict . layoutSmart (LayoutOptions (AvailablePerLine 100 1.0)) . pretty
|
||||
|
||||
instance ToString Error where
|
||||
toString = toString . toText
|
||||
|
|
|
|||
|
|
@ -26,7 +26,7 @@ emptyEnv :: Env
|
|||
emptyEnv = M.empty
|
||||
|
||||
showEnvEntry :: Text -> Definition -> Text
|
||||
showEnvEntry k Def{_ty = t} = k <> " : " <> pretty t
|
||||
showEnvEntry k Def{_ty = t} = k <> " : " <> prettyT t
|
||||
|
||||
dumpEnv :: Env -> IO ()
|
||||
dumpEnv = void . M.traverseWithKey ((putTextLn .) . showEnvEntry)
|
||||
|
|
|
|||
129
lib/Expr.hs
129
lib/Expr.hs
|
|
@ -1,5 +1,10 @@
|
|||
module Expr where
|
||||
|
||||
import qualified Data.List.NonEmpty as NE
|
||||
import Prettyprinter
|
||||
import Prettyprinter.Render.Text
|
||||
import Prelude hiding (group)
|
||||
|
||||
data Expr where
|
||||
Var :: Text -> Integer -> Expr
|
||||
Free :: Text -> Expr
|
||||
|
|
@ -12,6 +17,9 @@ data Expr where
|
|||
Let :: Text -> Maybe Expr -> Expr -> Expr -> Expr
|
||||
deriving (Show, Ord)
|
||||
|
||||
instance Pretty Expr where
|
||||
pretty = prettyExpr 0 . cleanNames
|
||||
|
||||
instance Eq Expr where
|
||||
(Var _ n) == (Var _ m) = n == m
|
||||
(Free s) == (Free t) = s == t
|
||||
|
|
@ -53,21 +61,28 @@ incIndices = shiftIndices 1 0
|
|||
|
||||
{- --------------------- PRETTY PRINTING ----------------------------- -}
|
||||
|
||||
parenthesize :: Text -> Text
|
||||
parenthesize s = "(" <> s <> ")"
|
||||
data Param = Param Text Expr
|
||||
data ParamGroup = ParamGroup [Text] Expr
|
||||
data Binding = Binding Text [ParamGroup] Expr
|
||||
|
||||
type Param = (Text, Expr)
|
||||
type ParamGroup = ([Text], Expr)
|
||||
type Binding = (Text, [ParamGroup], Expr)
|
||||
instance Pretty Param where
|
||||
pretty (Param x ty) = group $ parens $ pretty x <+> ":" <+> pretty ty
|
||||
|
||||
instance Pretty ParamGroup where
|
||||
pretty (ParamGroup vars ty) = group $ parens $ align (sep (map pretty vars)) <+> ":" <+> pretty ty
|
||||
|
||||
instance Pretty Binding where
|
||||
pretty (Binding var [] body) = group $ parens $ pretty var <+> ":=" <+> pretty body
|
||||
pretty (Binding var params body) = group $ parens $ pretty var <+> align (sep (map pretty params)) <+> ":=" <+> pretty body
|
||||
|
||||
collectLambdas :: Expr -> ([Param], Expr)
|
||||
collectLambdas (Abs x ty _ body) = ((x, ty) : params, final)
|
||||
collectLambdas (Abs x ty _ body) = (Param x ty : params, final)
|
||||
where
|
||||
(params, final) = collectLambdas body
|
||||
collectLambdas e = ([], e)
|
||||
|
||||
collectLets :: Expr -> ([Binding], Expr)
|
||||
collectLets (Let x _ val body) = ((x, params', val') : bindings, final)
|
||||
collectLets (Let x _ val body) = (Binding x params' val' : bindings, final)
|
||||
where
|
||||
(bindings, final) = collectLets body
|
||||
(params, val') = collectLambdas val
|
||||
|
|
@ -76,11 +91,17 @@ collectLets e = ([], e)
|
|||
|
||||
collectPis :: Expr -> ([Param], Expr)
|
||||
collectPis p@(Pi "" _ _ _) = ([], p)
|
||||
collectPis (Pi x ty _ body) = ((x, ty) : params, final)
|
||||
collectPis (Pi x ty _ body) = (Param x ty : params, final)
|
||||
where
|
||||
(params, final) = collectPis body
|
||||
collectPis e = ([], e)
|
||||
|
||||
collectApps :: Expr -> NonEmpty Expr
|
||||
collectApps (App e1 e2) = e2 :| toList rest
|
||||
where
|
||||
rest = collectApps e1
|
||||
collectApps e = pure e
|
||||
|
||||
cleanNames :: Expr -> Expr
|
||||
cleanNames (App m n) = App (cleanNames m) (cleanNames n)
|
||||
cleanNames (Abs x ty a body) = Abs x (cleanNames ty) a (cleanNames body)
|
||||
|
|
@ -92,25 +113,13 @@ cleanNames e = e
|
|||
groupParams :: [Param] -> [ParamGroup]
|
||||
groupParams = foldr addParam []
|
||||
where
|
||||
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
|
||||
addParam :: Param -> [ParamGroup] -> [ParamGroup]
|
||||
addParam (Param x t) [] = [ParamGroup [x] t]
|
||||
addParam (Param x t) l@(ParamGroup xs s : rest)
|
||||
| incIndices t == s = ParamGroup (x : xs) t : rest
|
||||
| otherwise = ParamGroup [x] t : l
|
||||
|
||||
showParamGroup :: ParamGroup -> Text
|
||||
showParamGroup (ids, ty) = parenthesize $ unwords ids <> " : " <> pretty ty
|
||||
|
||||
showBinding :: Binding -> Text
|
||||
showBinding (ident, params, val) =
|
||||
parenthesize $
|
||||
ident
|
||||
<> " "
|
||||
<> unwords (map showParamGroup params)
|
||||
<> " := "
|
||||
<> pretty val
|
||||
|
||||
printLevel :: Integer -> Text
|
||||
printLevel :: Integer -> Doc ann
|
||||
printLevel k
|
||||
| k == 0 = "₀"
|
||||
| k == 1 = "₁"
|
||||
|
|
@ -122,40 +131,54 @@ printLevel k
|
|||
| k == 7 = "₇"
|
||||
| k == 8 = "₈"
|
||||
| k == 9 = "₉"
|
||||
| k < 0 = show k
|
||||
| k < 0 = pretty k
|
||||
| otherwise = printLevel (k `div` 10) <> printLevel (k `mod` 10)
|
||||
|
||||
helper :: Integer -> Expr -> Text
|
||||
helper _ (Var s _) = s
|
||||
helper _ (Free s) = s
|
||||
helper _ (Axiom s) = s
|
||||
helper _ Star = "*"
|
||||
helper _ (Level i)
|
||||
| i == 0 = "□"
|
||||
| otherwise = "□" <> printLevel i
|
||||
helper k (App e1 e2) = if k > 3 then parenthesize res else res
|
||||
prettyExpr :: Integer -> Expr -> Doc ann
|
||||
prettyExpr k expr = case expr of
|
||||
Var s _ -> pretty s
|
||||
Free s -> pretty s
|
||||
Axiom s -> pretty s
|
||||
Star -> "*"
|
||||
Level i
|
||||
| i == 0 -> "□"
|
||||
| otherwise -> "□" <> printLevel i
|
||||
App{}
|
||||
| k > 3 -> parens application
|
||||
| otherwise -> application
|
||||
where
|
||||
res = helper 3 e1 <> " " <> helper 4 e2
|
||||
helper k (Pi "" t1 _ t2) = if k > 2 then parenthesize res else res
|
||||
(top :| rest) = NE.reverse $ collectApps expr
|
||||
application = group $ hang 4 $ prettyExpr 3 top <> line <> align (sep $ map (prettyExpr 4) rest)
|
||||
Pi "" t1 _ t2
|
||||
| k > 2 -> parens piType
|
||||
| otherwise -> piType
|
||||
where
|
||||
res = helper 3 t1 <> " -> " <> helper 2 t2
|
||||
helper k e@(Pi{}) = if k > 2 then parenthesize res else res
|
||||
piType = group $ prettyExpr 3 t1 <+> "->" <+> align (prettyExpr 2 t2)
|
||||
Pi{} -> group $ hang 4 $ "∏" <+> align (sep grouped) <> "," <> line <> align (prettyExpr 0 body)
|
||||
where
|
||||
(params, body) = collectPis e
|
||||
grouped = showParamGroup <$> groupParams params
|
||||
res = "∏ " <> unwords grouped <> " , " <> pretty body
|
||||
helper k e@(Abs{}) = if k >= 1 then parenthesize res else res
|
||||
(params, body) = collectPis expr
|
||||
grouped = pretty <$> groupParams params
|
||||
Abs{} ->
|
||||
if k >= 1
|
||||
then parens lambdaForm
|
||||
else lambdaForm
|
||||
where
|
||||
(params, body) = collectLambdas e
|
||||
grouped = showParamGroup <$> groupParams params
|
||||
res = "λ " <> unwords grouped <> " => " <> pretty body
|
||||
helper _ e@(Let{}) = res
|
||||
(params, body) = collectLambdas expr
|
||||
grouped = pretty <$> groupParams params
|
||||
lambdaForm = group $ hang 4 $ "λ" <+> align (sep grouped) <+> "=>" <> line <> align (prettyExpr 0 body)
|
||||
Let{} ->
|
||||
group $
|
||||
vsep
|
||||
[ "let" <+> align bindings
|
||||
, "in" <+> align (prettyExpr 0 body)
|
||||
, "end"
|
||||
]
|
||||
where
|
||||
(binds, body) = collectLets e
|
||||
res = "let " <> unwords (map showBinding binds) <> " in " <> pretty body <> " end"
|
||||
(binds, body) = collectLets expr
|
||||
bindings = sep $ map pretty binds
|
||||
|
||||
pretty :: Expr -> Text
|
||||
pretty = helper 0 . cleanNames
|
||||
prettyT :: Expr -> Text
|
||||
prettyT = renderStrict . layoutSmart defaultLayoutOptions . pretty
|
||||
|
||||
prettyS :: Expr -> String
|
||||
prettyS = toString . pretty
|
||||
prettyS = toString . prettyT
|
||||
|
|
|
|||
|
|
@ -42,6 +42,7 @@ library perga-lib
|
|||
, megaparsec
|
||||
, mtl
|
||||
, parser-combinators
|
||||
, prettyprinter
|
||||
mixins: base hiding (Prelude)
|
||||
, relude (Relude as Prelude)
|
||||
, relude
|
||||
|
|
|
|||
Loading…
Reference in a new issue