@@ -121,6 +121,7 @@ defaultOpts = IOption { opt_logLevel = 0
121121
122122data PPOption = PPOption {
123123 ppopt_impl :: Bool -- ^^ whether to show implicits
124+ , ppopt_pinames :: Bool -- ^^ whether to show names in pi bindings
124125 , ppopt_depth :: Maybe Int
125126} deriving (Show)
126127
@@ -131,16 +132,21 @@ defaultOptimise = [PETransform]
131132
132133-- | Pretty printing options with default verbosity.
133134defaultPPOption :: PPOption
134−defaultPPOption = PPOption { ppopt_impl = False , ppopt_depth = Just 200 }
135+defaultPPOption = PPOption { ppopt_impl = False,
136+ ppopt_pinames = False,
137+ ppopt_depth = Just 200 }
135138
136139-- | Pretty printing options with the most verbosity.
137140verbosePPOption :: PPOption
138−verbosePPOption = PPOption { ppopt_impl = True, ppopt_depth = Just 200 }
141+verbosePPOption = PPOption { ppopt_impl = True,
142+ ppopt_pinames = True,
143+ ppopt_depth = Just 200 }
139144
140145-- | Get pretty printing options from the big options record.
141146ppOption :: IOption -> PPOption
142147ppOption opt = PPOption {
143148 ppopt_impl = opt_showimp opt,
149+ ppopt_pinames = False,
144150 ppopt_depth = opt_printdepth opt
145151}
146152
@@ -1558,7 +1564,8 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
15581564 kwd "let" <+> (group . align . hang 2 $ prettyBindingOf n False <+> text "=" <$> prettySe (decD d) startPrec bnd v) </>
15591565 kwd "in" <+> (group . align . hang 2 $ prettySe (decD d) startPrec ((n, False):bnd) sc)
15601566 prettySe d p bnd (PPi (Exp l s _) n _ ty sc)
1561− | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1567+ | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs
1568+ || ppopt_pinames ppo && uname n =
15621569 depth d . bracket p startPrec . group $
15631570 enclose lparen rparen (group . align $ prettyBindingOf n False <+> colon <+> prettySe (decD d) startPrec bnd ty) <+>
15641571 st <> text "->" <$> prettySe (decD d) startPrec ((n, False):bnd) sc
@@ -1567,6 +1574,9 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
15671574 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
15681575 group (prettySe (decD d) startPrec ((n, False):bnd) sc)
15691576 where
1577+ uname (UN _) = True
1578+ uname _ = False
1579+
15701580 st =
15711581 case s of
15721582 Static -> text "[static]" <> space
@@ -2005,6 +2015,9 @@ showTm ist = displayDecorated (consoleDecorate ist) .
20052015showTmImpls :: PTerm -> String
20062016showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""
20072017
2018+-- | Show a term with specific options
2019+showTmOpts :: PPOption -> PTerm -> String
2020+showTmOpts opt = flip (displayS . renderPretty 1.0 10000000 . prettyImp opt) ""
20082021
20092022
20102023instance Sized PTerm where