rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

don't print substitutions by default

Browse source
This commit is contained in:
rhiannon morris 2023-02-26 11:25:11 +01:00
parent 8447098f28
commit 75ef078b4b
2 changed files with 42 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
exe/Main.idr
View file

@ -63,5 +63,6 @@ tm =
main : IO Unit main : IO Unit
main = do main = do
putStrLn $ banner defPrettyOpts putStrLn $ banner defPrettyOpts
prettyTermDef @{TermSubst True} tm
prettyTermDef @{TermSubst True} $ fst $ pushSubsts tm
prettyTermDef tm prettyTermDef tm
prettyTermDef $ pushSubsts tm

60
lib/Quox/Syntax/Term/Pretty.idr
View file

@ -94,18 +94,20 @@ prettyTag : TagVal -> Doc HL
prettyTag t = hl Tag $ "`" <+> fromString t prettyTag t = hl Tag $ "`" <+> fromString t
mutual parameters (showSubsts : Bool)
mutual
export covering export covering
PrettyHL q => PrettyHL (Term q d n) where [TermSubst] PrettyHL q => PrettyHL (Term q d n) using TermSubst ElimSubst
where
prettyM (TYPE l) = prettyM (TYPE l) =
parensIfM App $ !typeD <+> hl Syntax !(prettyUnivSuffix l) parensIfM App $ !typeD <+> hl Syntax !(prettyUnivSuffix l)
prettyM (Pi qty s (S [x] t)) = prettyM (Pi qty s (S [x] t)) =
prettyBindType [qty] x s !arrowD t prettyBindType [qty] x s !arrowD t.term
prettyM (Lam (S x t)) = prettyM (Lam (S x t)) =
let GotLams {names, body, _} = getLams' x t.term Refl in let GotLams {names, body, _} = getLams' x t.term Refl in
prettyLams T (toList names) body prettyLams T (toList names) body
prettyM (Sig s (S [x] t)) = prettyM (Sig s (S [x] t)) =
prettyBindType {q} [] x s !timesD t prettyBindType {q} [] x s !timesD t.term
prettyM (Pair s t) = prettyM (Pair s t) =
let GotPairs {init, last, _} = getPairs' [< s] t in let GotPairs {init, last, _} = getPairs' [< s] t in
prettyTuple $ toList $ init :< last prettyTuple $ toList $ init :< last
@ -131,14 +133,21 @@ mutual
prettyLams D (toList names) body prettyLams D (toList names) body
prettyM (E e) = bracks <$> prettyM e prettyM (E e) = bracks <$> prettyM e
prettyM (CloT s th) = prettyM (CloT s th) =
parensIfM SApp . hang 2 =<< if showSubsts then
[|withPrec SApp (prettyM s) </> prettyTSubst th|] parensIfM SApp . hang 2 =<<
[|withPrec SApp (prettyM s) </> prettyTSubst th|]
else
prettyM $ pushSubstsWith' id th s
prettyM (DCloT s th) = prettyM (DCloT s th) =
parensIfM SApp . hang 2 =<< if showSubsts then
[|withPrec SApp (prettyM s) </> prettyDSubst th|] parensIfM SApp . hang 2 =<<
[|withPrec SApp (prettyM s) </> prettyDSubst th|]
else
prettyM $ pushSubstsWith' th id s
export covering export covering
PrettyHL q => PrettyHL (Elim q d n) where [ElimSubst] PrettyHL q => PrettyHL (Elim q d n) using TermSubst ElimSubst
where
prettyM (F x) = prettyM (F x) =
hl' Free <$> prettyM x hl' Free <$> prettyM x
prettyM (B i) = prettyM (B i) =
@ -149,9 +158,9 @@ mutual
prettyM (CasePair pi p (S [r] ret) (S [x, y] body)) = do prettyM (CasePair pi p (S [r] ret) (S [x, y] body)) = do
pat <- (parens . separate commaD . map (hl TVar)) <$> pat <- (parens . separate commaD . map (hl TVar)) <$>
traverse prettyM [x, y] traverse prettyM [x, y]
prettyCase pi p r ret [([x, y], pat, body)] prettyCase pi p r ret.term [([x, y], pat, body.term)]
prettyM (CaseEnum pi t (S [r] ret) arms) = prettyM (CaseEnum pi t (S [r] ret) arms) =
prettyCase pi t r ret prettyCase pi t r ret.term
[([], prettyTag t, b) | (t, b) <- SortedMap.toList arms] [([], prettyTag t, b) | (t, b) <- SortedMap.toList arms]
prettyM (e :% d) = prettyM (e :% d) =
let GotDArgs {fun, args, _} = getDArgs' e [d] in let GotDArgs {fun, args, _} = getDArgs' e [d] in
@ -161,17 +170,28 @@ mutual
!(withPrec AnnL $ prettyM s) <++> !annD !(withPrec AnnL $ prettyM s) <++> !annD
<//> !(withPrec Ann $ prettyM a) <//> !(withPrec Ann $ prettyM a)
prettyM (CloE e th) = prettyM (CloE e th) =
parensIfM SApp . hang 2 =<< if showSubsts then
[|withPrec SApp (prettyM e) </> prettyTSubst th|] parensIfM SApp . hang 2 =<<
[|withPrec SApp (prettyM e) </> prettyTSubst th|]
else
prettyM $ pushSubstsWith' id th e
prettyM (DCloE e th) = prettyM (DCloE e th) =
parensIfM SApp . hang 2 =<< if showSubsts then
[|withPrec SApp (prettyM e) </> prettyDSubst th|] parensIfM SApp . hang 2 =<<
[|withPrec SApp (prettyM e) </> prettyDSubst th|]
export covering else
{s : Nat} -> PrettyHL q => PrettyHL (ScopedBody s (Term q d) n) where prettyM $ pushSubstsWith' th id e
prettyM body = prettyM body.term
export covering export covering
prettyTSubst : Pretty.HasEnv m => PrettyHL q => prettyTSubst : Pretty.HasEnv m => PrettyHL q =>
TSubst q d from to -> m (Doc HL) TSubst q d from to -> m (Doc HL)
prettyTSubst s = prettySubstM prettyM (!ask).tnames TVar "[" "]" s prettyTSubst s =
prettySubstM (prettyM @{ElimSubst}) (!ask).tnames TVar "[" "]" s
export covering %inline
PrettyHL q => PrettyHL (Term q d n) where
prettyM = prettyM @{TermSubst False}
export covering %inline
PrettyHL q => PrettyHL (Elim q d n) where
prettyM = prettyM @{ElimSubst False}