pretty printer refactoring
This commit is contained in:
parent
75ef078b4b
commit
28356200c1
|
|
@ -32,61 +32,66 @@ ofD = hl Syntax "of"
|
|||
returnD = hl Syntax "return"
|
||||
|
||||
|
||||
export covering
|
||||
export
|
||||
prettyBindType : PrettyHL a => PrettyHL b => PrettyHL q =>
|
||||
Pretty.HasEnv m =>
|
||||
List q -> BaseName -> a -> Doc HL -> b -> m (Doc HL)
|
||||
prettyBindType qtys x s arr t =
|
||||
parensIfM Outer $ hang 2 $
|
||||
parens (hang 2 $ !(prettyQtyBinds qtys (TV x)) <++> colonD
|
||||
<//> !(prettyM s)) <++> arr
|
||||
<//> !(under T x $ prettyM t)
|
||||
prettyBindType qtys x s arr t = do
|
||||
var <- prettyQtyBinds qtys $ TV x
|
||||
s <- withPrec Outer $ prettyM s
|
||||
t <- withPrec Outer $ under T x $ prettyM t
|
||||
let bind = parens (var <++> colonD <//> hang 2 s)
|
||||
parensIfM Outer $ hang 2 $ bind <//> t
|
||||
|
||||
export covering
|
||||
export
|
||||
prettyArm : PrettyHL a => Pretty.HasEnv m =>
|
||||
BinderSort -> List BaseName -> Doc HL -> a -> m (Doc HL)
|
||||
prettyArm sort xs pat body = do
|
||||
body <- withPrec Outer $ unders sort xs $ prettyM body
|
||||
pure $ hang 2 $ sep [pat <+> dotD, body]
|
||||
|
||||
export
|
||||
prettyLams : PrettyHL a => Pretty.HasEnv m =>
|
||||
BinderSort -> List BaseName -> a -> m (Doc HL)
|
||||
prettyLams sort names body = do
|
||||
lam <- case sort of T => lamD; D => dlamD
|
||||
header <- sequence $ [hl TVar <$> prettyM x | x <- names]
|
||||
body <- unders sort names $ prettyM body
|
||||
parensIfM Outer $ (sep (lam :: header) <+> dotD) <//> body
|
||||
Maybe (Doc HL) -> BinderSort -> List BaseName -> a -> m (Doc HL)
|
||||
prettyLams lam sort names body = do
|
||||
let var = case sort of T => TVar; D => DVar
|
||||
header <- sequence $ [hlF var $ prettyM x | x <- names]
|
||||
let header = sep $ maybe header (:: header) lam
|
||||
parensIfM Outer =<< prettyArm sort names header body
|
||||
|
||||
export covering
|
||||
export
|
||||
prettyApps : PrettyHL f => PrettyHL a => Pretty.HasEnv m =>
|
||||
Maybe (Doc HL) -> f -> List a -> m (Doc HL)
|
||||
prettyApps pfx fun args =
|
||||
parensIfM App =<< withPrec Arg
|
||||
[|prettyM fun <//> (align . sep <$> traverse prettyArg args)|]
|
||||
prettyApps pfx fun args = do
|
||||
fun <- withPrec Arg $ prettyM fun
|
||||
args <- traverse (withPrec Arg . prettyArg) args
|
||||
parensIfM App $ hang 2 $ sep $ fun :: args
|
||||
where
|
||||
prettyArg : a -> m (Doc HL)
|
||||
prettyArg x = maybe id (\p => map (hl Delim p <+>)) pfx $ prettyM x
|
||||
prettyArg = case pfx of
|
||||
Nothing => prettyM
|
||||
Just pfx => \x => pure $ hl Delim pfx <+> !(prettyM x)
|
||||
|
||||
export covering
|
||||
export
|
||||
prettyTuple : PrettyHL a => Pretty.HasEnv m => List a -> m (Doc HL)
|
||||
prettyTuple = map (parens . align . separate commaD) . traverse prettyM
|
||||
|
||||
export covering
|
||||
prettyArm : PrettyHL a => Pretty.HasEnv m =>
|
||||
(List BaseName, Doc HL, a) -> m (Doc HL)
|
||||
prettyArm (xs, pat, body) =
|
||||
pure $ hang 2 $ sep
|
||||
[pat <+> dotD, !(withPrec Outer $ unders T xs $ prettyM body)]
|
||||
|
||||
export covering
|
||||
export
|
||||
prettyArms : PrettyHL a => Pretty.HasEnv m =>
|
||||
List (List BaseName, Doc HL, a) -> m (Doc HL)
|
||||
prettyArms = map (braces . align . sep) . traverse prettyArm
|
||||
prettyArms =
|
||||
map (braces . asep) . traverse (\(xs, l, r) => prettyArm T xs l r)
|
||||
|
||||
export covering
|
||||
export
|
||||
prettyCase : PrettyHL a => PrettyHL b => PrettyHL c => PrettyHL q =>
|
||||
Pretty.HasEnv m =>
|
||||
q -> a -> BaseName -> b -> List (List BaseName, Doc HL, c) ->
|
||||
m (Doc HL)
|
||||
prettyCase pi elim r ret arms =
|
||||
pure $ align $ sep $
|
||||
[hsep [caseD, !(prettyQtyBinds [pi] elim)],
|
||||
hsep [returnD, !(prettyM r) <+> dotD, !(under T r $ prettyM ret)],
|
||||
hsep [ofD, !(prettyArms arms)]]
|
||||
prettyCase pi elim r ret arms = do
|
||||
elim <- prettyQtyBinds [pi] elim
|
||||
ret <- prettyLams Nothing T [r] ret
|
||||
arms <- prettyArms arms
|
||||
pure $ asep [caseD <++> elim, returnD <++> ret, ofD <++> arms]
|
||||
|
||||
-- [fixme] put delimiters around tags that aren't simple names
|
||||
export
|
||||
|
|
@ -105,7 +110,7 @@ parameters (showSubsts : Bool)
|
|||
prettyBindType [qty] x s !arrowD t.term
|
||||
prettyM (Lam (S x t)) =
|
||||
let GotLams {names, body, _} = getLams' x t.term Refl in
|
||||
prettyLams T (toList names) body
|
||||
prettyLams (Just !lamD) T (toList names) body
|
||||
prettyM (Sig s (S [x] t)) =
|
||||
prettyBindType {q} [] x s !timesD t.term
|
||||
prettyM (Pair s t) =
|
||||
|
|
@ -116,21 +121,19 @@ parameters (showSubsts : Bool)
|
|||
Prelude.toList tags
|
||||
prettyM (Tag t) =
|
||||
pure $ prettyTag t
|
||||
prettyM (Eq (S _ (N ty)) l r) =
|
||||
parensIfM Eq !(withPrec InEq $ pure $
|
||||
sep [!(prettyM l) <++> !eqndD,
|
||||
!(prettyM r) <++> colonD, !(prettyM ty)])
|
||||
prettyM (Eq (S [i] (Y ty)) l r) =
|
||||
parensIfM App $
|
||||
eqD <++>
|
||||
sep [bracks !(withPrec Outer $ pure $ hang 2 $
|
||||
sep [hl DVar !(prettyM i) <+> dotD,
|
||||
!(under D i $ prettyM ty)]),
|
||||
!(withPrec Arg $ prettyM l),
|
||||
!(withPrec Arg $ prettyM r)]
|
||||
prettyM (Eq (S _ (N ty)) l r) = do
|
||||
l <- withPrec InEq $ prettyM l
|
||||
r <- withPrec InEq $ prettyM r
|
||||
ty <- withPrec InEq $ prettyM ty
|
||||
parensIfM Eq $ asep [l <++> !eqndD, r <++> colonD, ty]
|
||||
prettyM (Eq (S [i] (Y ty)) l r) = do
|
||||
ty <- bracks <$> withPrec Outer (prettyLams Nothing D [i] ty)
|
||||
l <- withPrec Arg $ prettyM l
|
||||
r <- withPrec Arg $ prettyM r
|
||||
parensIfM App $ eqD <++> asep [ty, l, r]
|
||||
prettyM (DLam (S i t)) =
|
||||
let GotDLams {names, body, _} = getDLams' i t.term Refl in
|
||||
prettyLams D (toList names) body
|
||||
prettyLams (Just !dlamD) D (toList names) body
|
||||
prettyM (E e) = bracks <$> prettyM e
|
||||
prettyM (CloT s th) =
|
||||
if showSubsts then
|
||||
|
|
@ -156,8 +159,7 @@ parameters (showSubsts : Bool)
|
|||
let GotArgs {fun, args, _} = getArgs' e [s] in
|
||||
prettyApps Nothing fun args
|
||||
prettyM (CasePair pi p (S [r] ret) (S [x, y] body)) = do
|
||||
pat <- (parens . separate commaD . map (hl TVar)) <$>
|
||||
traverse prettyM [x, y]
|
||||
pat <- parens . separate commaD <$> traverse (hlF TVar . prettyM) [x, y]
|
||||
prettyCase pi p r ret.term [([x, y], pat, body.term)]
|
||||
prettyM (CaseEnum pi t (S [r] ret) arms) =
|
||||
prettyCase pi t r ret.term
|
||||
|
|
@ -165,10 +167,10 @@ parameters (showSubsts : Bool)
|
|||
prettyM (e :% d) =
|
||||
let GotDArgs {fun, args, _} = getDArgs' e [d] in
|
||||
prettyApps (Just "@") fun args
|
||||
prettyM (s :# a) =
|
||||
parensIfM Ann $ hang 2 $
|
||||
!(withPrec AnnL $ prettyM s) <++> !annD
|
||||
<//> !(withPrec Ann $ prettyM a)
|
||||
prettyM (s :# a) = do
|
||||
s <- withPrec AnnL $ prettyM s
|
||||
a <- withPrec Ann $ prettyM a
|
||||
parensIfM Ann $ hang 2 $ s <++> !annD <//> a
|
||||
prettyM (CloE e th) =
|
||||
if showSubsts then
|
||||
parensIfM SApp . hang 2 =<<
|
||||
|
|
|
|||
Loading…
Reference in New Issue