0663f4d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1183 from pminten/ppopt

Pretty printing option record

commit0663f4d8ecf58622d14e5094cad797797ac34939 authorEdwin Brady <edwin.brady@gmail.com> dateSun 4 May 2014, 14:26 (12 years ago) parentf30bfc0 9491c3c

9 files changed+127−106

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+73−51 src/Idris/Delaborate.hs+2−2 src/Idris/Docs.hs+9−9 src/Idris/ElabDecls.hs+3−3 src/Idris/IdrisDoc.hs+1−1 src/Idris/Output.hs+6−6 src/Idris/Parser.hs+1−1 src/Idris/Prover.hs+9−9 src/Idris/REPL.hs+23−24

src/Idris/AbsSyntaxTree.hs+73−51

@@ -95,6 +95,28 @@ defaultOpts = IOption { opt_logLevel = 0

9595 , opt_autoSolve = True

9696 }

9797

98+data PPOption = PPOption {

99+ ppopt_impl :: Bool -- ^^ whether to show implicits

100+} deriving (Show)

101+

102+-- | Pretty printing options with default verbosity.

103+defaultPPOption :: PPOption

104+defaultPPOption = PPOption { ppopt_impl = False }

105+

106+-- | Pretty printing options with the most verbosity.

107+verbosePPOption :: PPOption

108+verbosePPOption = PPOption { ppopt_impl = True }

109+

110+-- | Get pretty printing options from the big options record.

111+ppOption :: IOption -> PPOption

112+ppOption opt = PPOption {

113+ ppopt_impl = opt_showimp opt

114+}

115+

116+-- | Get pretty printing options from an idris state record.

117+ppOptionIst :: IState -> PPOption

118+ppOptionIst = ppOption . idris_options

119+

98120data LanguageExt = TypeProviders | ErrorReflection deriving (Show, Eq, Read, Ord)

99121

100122-- | The output mode in use

@@ -1089,19 +1111,19 @@ piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)

10891111-- could interfere with interactive editing, which calls "show".

10901112

10911113instance Show PTerm where

1092− showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp False) tm

1114+ showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp defaultPPOption) tm

10931115

10941116instance Show PDecl where

1095− showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp False) d

1117+ showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp defaultPPOption) d

10961118

10971119instance Show PClause where

1098− showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp True) c

1120+ showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp verbosePPOption) c

10991121

11001122instance Show PData where

1101− showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp False) d

1123+ showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp defaultPPOption) d

11021124

11031125instance Pretty PTerm OutputAnnotation where

1104− pretty = prettyImp False

1126+ pretty = prettyImp defaultPPOption

11051127

11061128-- | Colourise annotations according to an Idris state. It ignores the names

11071129-- in the annotation, as there's no good way to show extended information on a

@@ -1129,23 +1151,23 @@ consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)

11291151 colour ItalicText = IdrisColour Nothing True False False True

11301152

11311153-- | Pretty-print a high-level closed Idris term with no information about precedence/associativity

1132−prettyImp :: Bool -- ^^ whether to show implicits

1154+prettyImp :: PPOption -- ^^ pretty printing options

11331155 -> PTerm -- ^^ the term to pretty-print

11341156 -> Doc OutputAnnotation

11351157prettyImp impl = pprintPTerm impl [] [] []

11361158

11371159-- | Do the right thing for rendering a term in an IState

11381160prettyIst :: IState -> PTerm -> Doc OutputAnnotation

1139−prettyIst ist = pprintPTerm (opt_showimp (idris_options ist)) [] [] (idris_infixes ist)

1161+prettyIst ist = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist)

11401162

11411163-- | Pretty-print a high-level Idris term in some bindings context with infix info

1142−pprintPTerm :: Bool -- ^^ whether to show implicits

1164+pprintPTerm :: PPOption -- ^^ pretty printing options

11431165 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit

11441166 -> [Name] -- ^^ names to always show in pi, even if not used

11451167 -> [FixDecl] -- ^^ Fixity declarations

11461168 -> PTerm -- ^^ the term to pretty-print

11471169 -> Doc OutputAnnotation

1148−pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

1170+pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

11491171 where

11501172 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

11511173 prettySe p bnd (PQuote r) =

@@ -1154,7 +1176,7 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

11541176 prettySe p bnd e

11551177 | Just str <- slist p bnd e = str

11561178 | Just n <- snat p e = annotate AnnConstData (text (show n))

1157− prettySe p bnd (PRef fc n) = prettyName impl bnd n

1179+ prettySe p bnd (PRef fc n) = prettyName (ppopt_impl ppo) bnd n

11581180 prettySe p bnd (PLam n ty sc) =

11591181 bracket p 2 . group . align . hang 2 $

11601182 text "\\" <> bindingOf n False <+> text "=>" <$>

@@ -1165,7 +1187,7 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

11651187 prettySe 10 bnd v <+> kwd "in" </>

11661188 prettySe 10 ((n, False):bnd) sc

11671189 prettySe p bnd (PPi (Exp l s _) n ty sc)

1168− | n `elem` allNamesIn sc || impl || n `elem` docArgs =

1190+ | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =

11691191 bracket p 2 . group $

11701192 enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>

11711193 st <> text "->" <$> prettySe 10 ((n, False):bnd) sc

@@ -1178,7 +1200,7 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

11781200 Static -> text "[static]" <> space

11791201 _ -> empty

11801202 prettySe p bnd (PPi (Imp l s _) n ty sc)

1181− | impl =

1203+ | ppopt_impl ppo =

11821204 bracket p 2 $

11831205 lbrace <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>

11841206 st <> text "->" </> prettySe 10 ((n, True):bnd) sc

@@ -1197,16 +1219,16 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

11971219 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc

11981220 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args

11991221 | UN nm <- basename f

1200− , not impl && null (getExps args) = if isAlpha (thead nm)

1201− then prettyName impl bnd f

1202− else enclose lparen rparen $

1203− prettyName impl bnd f

1222+ , not (ppopt_impl ppo) && null (getExps args) =

1223+ if isAlpha (thead nm)

1224+ then prettyName (ppopt_impl ppo) bnd f

1225+ else enclose lparen rparen $ prettyName (ppopt_impl ppo) bnd f

12041226 prettySe p bnd (PAppBind _ (PRef _ f) [])

1205− | not impl = text "!" <> prettyName impl bnd f

1227+ | not (ppopt_impl ppo) = text "!" <> prettyName (ppopt_impl ppo) bnd f

12061228 prettySe p bnd (PApp _ (PRef _ op) args)

12071229 | UN nm <- basename op

12081230 , not (tnull nm) &&

1209− (not impl) && (not $ isAlpha (thead nm)) =

1231+ (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =

12101232 case getExps args of

12111233 [] -> enclose lparen rparen opName

12121234 [x] -> group (enclose lparen rparen opName <$> group (prettySe 0 bnd x))

@@ -1215,7 +1237,7 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

12151237 (l:r:rest) -> bracket p 1 $

12161238 enclose lparen rparen (inFix l r) <+>

12171239 align (group (vsep (map (prettyArgSe bnd) rest)))

1218− where opName = prettyName impl bnd op

1240+ where opName = prettyName (ppopt_impl ppo) bnd op

12191241 f = getFixity (opStr op)

12201242 left l = case f of

12211243 Nothing -> prettySe (-1) bnd l

@@ -1235,7 +1257,7 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

12351257 fp = prettySe 1 bnd f

12361258 in

12371259 bracket p 1 . group $

1238− if impl

1260+ if ppopt_impl ppo

12391261 then if null as

12401262 then fp

12411263 else fp <+> align (vsep (map (prettyArgS bnd) as))

@@ -1340,9 +1362,9 @@ pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

13401362 basename n = n

13411363

13421364 slist' p bnd (PApp _ (PRef _ nil) _)

1343− | not impl && nsroot nil == sUN "Nil" = Just []

1365+ | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []

13441366 slist' p bnd (PRef _ nil)

1345− | not impl && nsroot nil == sUN "Nil" = Just []

1367+ | not (ppopt_impl ppo) && nsroot nil == sUN "Nil" = Just []

13461368 slist' p bnd (PApp _ (PRef _ cons) args)

13471369 | nsroot cons == sUN "::",

13481370 (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,

@@ -1415,43 +1437,43 @@ prettyName showNS bnd n | Just imp <- lookup n bnd = annotate (AnnBoundName n im

14151437 strName other = show other

14161438

14171439

1418−showCImp :: Bool -> PClause -> Doc OutputAnnotation

1419−showCImp impl (PClause _ n l ws r w)

1420− = prettyImp impl l <+> showWs ws <+> text "=" <+> prettyImp impl r

1440+showCImp :: PPOption -> PClause -> Doc OutputAnnotation

1441+showCImp ppo (PClause _ n l ws r w)

1442+ = prettyImp ppo l <+> showWs ws <+> text "=" <+> prettyImp ppo r

14211443 <+> text "where" <+> text (show w)

14221444 where

14231445 showWs [] = empty

1424− showWs (x : xs) = text "|" <+> prettyImp impl x <+> showWs xs

1425−showCImp impl (PWith _ n l ws r w)

1426− = prettyImp impl l <+> showWs ws <+> text "with" <+> prettyImp impl r

1446+ showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs

1447+showCImp ppo (PWith _ n l ws r w)

1448+ = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r

14271449 <+> braces (text (show w))

14281450 where

14291451 showWs [] = empty

1430− showWs (x : xs) = text "|" <+> prettyImp impl x <+> showWs xs

1452+ showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs

14311453

14321454

1433−showDImp :: Bool -> PData -> Doc OutputAnnotation

1434−showDImp impl (PDatadecl n ty cons)

1435− = text "data" <+> text (show n) <+> colon <+> prettyImp impl ty <+> text "where" <$>

1436− (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName False [] n <+> colon <+> prettyImp impl t) cons))

1455+showDImp :: PPOption -> PData -> Doc OutputAnnotation

1456+showDImp ppo (PDatadecl n ty cons)

1457+ = text "data" <+> text (show n) <+> colon <+> prettyImp ppo ty <+> text "where" <$>

1458+ (indent 2 $ vsep (map (\ (_, _, n, t, _, _) -> pipe <+> prettyName False [] n <+> colon <+> prettyImp ppo t) cons))

14371459

1438−showDecls :: Bool -> [PDecl] -> Doc OutputAnnotation

1439−showDecls i ds = vsep (map (showDeclImp i) ds)

1460+showDecls :: PPOption -> [PDecl] -> Doc OutputAnnotation

1461+showDecls o ds = vsep (map (showDeclImp o) ds)

14401462

14411463showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))

1442−showDeclImp i (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp i t

1443−showDeclImp i (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>

1444− indent 2 (vsep (map (showCImp i) cs))

1445−showDeclImp _ (PData _ _ _ _ _ d) = showDImp True d

1446−showDeclImp i (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls i ps <> line)

1447−showDeclImp i (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls i ps <> line)

1464+showDeclImp o (PTy _ _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp o t

1465+showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>

1466+ indent 2 (vsep (map (showCImp o) cs))

1467+showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d

1468+showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)

1469+showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)

14481470showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

1449−showDeclImp i (PClass _ _ _ cs n ps _ ds)

1450− = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls i ds

1451−showDeclImp i (PInstance _ _ cs n _ t _ ds)

1452− = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp i t <> line <> showDecls i ds

1471+showDeclImp o (PClass _ _ _ cs n ps _ ds)

1472+ = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds

1473+showDeclImp o (PInstance _ _ cs n _ t _ ds)

1474+ = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds

14531475showDeclImp _ _ = text "..."

1454−-- showDeclImp (PImport i) = "import " ++ i

1476+-- showDeclImp (PImport o) = "import " ++ o

14551477

14561478instance Show (Doc OutputAnnotation) where

14571479 show = flip (displayS . renderCompact) ""

@@ -1478,14 +1500,14 @@ getAll = map getTm

14781500-- | Show Idris name

14791501showName :: Maybe IState -- ^^ the Idris state, for information about names and colours

14801502 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit

1481− -> Bool -- ^^ whether to show implicits

1503+ -> PPOption -- ^^ pretty printing options

14821504 -> Bool -- ^^ whether to colourise

14831505 -> Name -- ^^ the term to show

14841506 -> String

1485−showName ist bnd impl colour n = case ist of

1507+showName ist bnd ppo colour n = case ist of

14861508 Just i -> if colour then colourise n (idris_colourTheme i) else showbasic n

14871509 Nothing -> showbasic n

1488− where name = if impl then show n else showbasic n

1510+ where name = if ppopt_impl ppo then show n else showbasic n

14891511 showbasic n@(UN _) = showCG n

14901512 showbasic (MN _ s) = str s

14911513 showbasic (NS n s) = showSep "." (map str (reverse s)) ++ "." ++ showbasic n

@@ -1509,11 +1531,11 @@ showTm :: IState -- ^^ the Idris state, for information about identifiers and co

15091531 -> String

15101532showTm ist = displayDecorated (consoleDecorate ist) .

15111533 renderPretty 0.8 100000 .

1512− prettyImp (opt_showimp (idris_options ist))

1534+ prettyImp (ppOptionIst ist)

15131535

15141536-- | Show a term with implicits, no colours

15151537showTmImpls :: PTerm -> String

1516−showTmImpls = flip (displayS . renderCompact . prettyImp True) ""

1538+showTmImpls = flip (displayS . renderCompact . prettyImp verbosePPOption) ""

15171539

15181540

15191541instance Sized PTerm where

src/Idris/Delaborate.hs+2−2

@@ -138,7 +138,7 @@ pprintTerm :: IState -> PTerm -> Doc OutputAnnotation

138138pprintTerm ist = pprintTerm' ist []

139139

140140pprintTerm' :: IState -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

141−pprintTerm' ist bnd = pprintPTerm (opt_showimp (idris_options ist)) bnd [] (idris_infixes ist)

141+pprintTerm' ist bnd tm = pprintPTerm (ppOptionIst ist) bnd [] (idris_infixes ist) tm

142142

143143pprintErr :: IState -> Err -> Doc OutputAnnotation

144144pprintErr i err = pprintErr' i (fmap (errReverse i) err)

@@ -269,7 +269,7 @@ showSc i xs = line <> line <> text "In context:" <>

269269

270270

271271showqual :: IState -> Name -> String

272−showqual i n = showName (Just i) [] False False (dens n)

272+showqual i n = showName (Just i) [] (ppOptionIst i) { ppopt_impl = False } False (dens n)

273273 where

274274 dens ns@(NS n _) = case lookupCtxt n (idris_implicits i) of

275275 [_] -> n -- just one thing

src/Idris/Docs.hs+9−9

@@ -36,8 +36,8 @@ showDoc d | nullDocstring d = empty

3636

3737pprintFD :: IState -> FunDoc -> Doc OutputAnnotation

3838pprintFD ist (FD n doc args ty f)

39− = nest 4 (prettyName imp [] n <+> colon <+>

40− pprintPTerm imp [] [ n | (n@(UN n'),_,_,_) <- args

39+ = nest 4 (prettyName (ppopt_impl ppo) [] n <+> colon <+>

40+ pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args

4141 , not (T.isPrefixOf (T.pack "__") n') ] infixes ty <$>

4242 renderDocstring doc <$>

4343 maybe empty (\f -> text (show f) <> line) f <>

@@ -46,23 +46,23 @@ pprintFD ist (FD n doc args ty f)

4646 then nest 4 $ text "Arguments:" <$> vsep argshow

4747 else empty)

4848

49− where imp = opt_showimp (idris_options ist)

49+ where ppo = ppOptionIst ist

5050 infixes = idris_infixes ist

5151 showArgs ((n, ty, Exp {}, Just d):args) bnd

5252 = bindingOf n False <+> colon <+>

53− pprintPTerm imp bnd [] infixes ty <>

53+ pprintPTerm ppo bnd [] infixes ty <>

5454 showDoc d <> line

5555 :

5656 showArgs args ((n, False):bnd)

5757 showArgs ((n, ty, Constraint {}, Just d):args) bnd

5858 = text "Class constraint" <+>

59− pprintPTerm imp bnd [] infixes ty <> showDoc d <> line

59+ pprintPTerm ppo bnd [] infixes ty <> showDoc d <> line

6060 :

6161 showArgs args ((n, True):bnd)

6262 showArgs ((n, ty, Imp {}, Just d):args) bnd

6363 = text "(implicit)" <+>

6464 bindingOf n True <+> colon <+>

65− pprintPTerm imp bnd [] infixes ty <>

65+ pprintPTerm ppo bnd [] infixes ty <>

6666 showDoc d <> line

6767 :

6868 showArgs args ((n, True):bnd)

@@ -77,7 +77,7 @@ pprintDocs ist (DataDoc t args)

7777 nest 4 (text "Constructors:" <> line <>

7878 vsep (map (pprintFD ist) args))

7979pprintDocs ist (ClassDoc n doc meths params instances)

80− = nest 4 (text "Type class" <+> prettyName imp [] n <>

80+ = nest 4 (text "Type class" <+> prettyName (ppopt_impl ppo) [] n <>

8181 if nullDocstring doc then empty else line <> renderDocstring doc)

8282 <> line <$>

8383 nest 4 (text "Parameters:" <$> prettyParameters)

@@ -97,11 +97,11 @@ pprintDocs ist (ClassDoc n doc meths params instances)

9797

9898 pNames = map fst params

9999

100− imp = opt_showimp (idris_options ist)

100+ ppo = ppOptionIst ist

101101 infixes = idris_infixes ist

102102

103103 dumpInstance :: PTerm -> Doc OutputAnnotation

104− dumpInstance = pprintPTerm imp params' [] infixes

104+ dumpInstance = pprintPTerm ppo params' [] infixes

105105

106106 prettifySubclasses (PPi (Constraint _ _) _ tm _) = prettifySubclasses tm

107107 prettifySubclasses (PPi plcity nm t1 t2) = PPi plcity (safeHead nm pNames) (prettifySubclasses t1) (prettifySubclasses t2)

src/Idris/ElabDecls.hs+3−3

@@ -393,7 +393,7 @@ elabEliminator paramPos n ty cons info = do

393393 elimLog elimSig

394394 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)

395395 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses

396− elimLog $ "-- eliminator definition: " ++ (show . showDeclImp True) eliminatorDef

396+ elimLog $ "-- eliminator definition: " ++ (show . showDeclImp verbosePPOption) eliminatorDef

397397 State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())

398398 -- Do not elaborate clauses if there aren't any

399399 case eliminatorClauses of

@@ -1863,7 +1863,7 @@ elabClass info syn doc fc constraints tn ps pDocs ds

18631863 constraint

18641864 let cons = [(emptyDocstring, [], cn, cty, fc, [])]

18651865 let ddecl = PDatadecl tn tty cons

1866− logLvl 5 $ "Class data " ++ show (showDImp True ddecl)

1866+ logLvl 5 $ "Class data " ++ show (showDImp verbosePPOption ddecl)

18671867 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc pDocs fc [] ddecl

18681868 -- for each constraint, build a top level function to chase it

18691869 logLvl 5 $ "Building functions"

@@ -2059,7 +2059,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

20592059 let wbTys = map mkTyDecl mtys

20602060 let wbVals = map (decorateid (decorate ns iname)) ds'

20612061 let wb = wbTys ++ wbVals

2062− logLvl 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp True . mkTyDecl) mtys)

2062+ logLvl 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp verbosePPOption . mkTyDecl) mtys)

20632063 logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++

20642064 show (concat (nub wparams))

20652065

src/Idris/IdrisDoc.hs+1−1

@@ -457,7 +457,7 @@ genTypeHeader ist (FD n _ args ftype _) = do

457457

458458 where

459459 htmlSignature = displayDecorated decorator $ renderCompact signature

460− signature = pprintPTerm False [] names (idris_infixes ist) ftype

460+ signature = pprintPTerm defaultPPOption [] names (idris_infixes ist) ftype

461461 names = [ n | (n@(UN n'), _, _, _) <- args,

462462 not (T.isPrefixOf (txt "__") n') ]

463463

src/Idris/Output.hs+6−6

@@ -88,16 +88,16 @@ ihPrintTermWithType h tm ty = do ist <- getIState

8888-- | Pretty-print a collection of overloadings to REPL or IDESlave - corresponds to :t name

8989ihPrintFunTypes :: Handle -> [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris ()

9090ihPrintFunTypes h bnd n [] = ihPrintError h $ "No such variable " ++ show n

91−ihPrintFunTypes h bnd n overloads = do imp <- impShow

92− ist <- getIState

91+ihPrintFunTypes h bnd n overloads = do ist <- getIState

92+ let ppo = ppOptionIst ist

9393 let infixes = idris_infixes ist

94− let output = vsep (map (uncurry (ppOverload imp infixes)) overloads)

94+ let output = vsep (map (uncurry (ppOverload ppo infixes)) overloads)

9595 case idris_outputmode ist of

9696 RawOutput -> consoleDisplayAnnotated h output

9797 IdeSlave n -> ideSlaveReturnAnnotated n h output

9898 where fullName n = prettyName True bnd n

99− ppOverload imp infixes n tm =

100− fullName n <+> colon <+> align (pprintPTerm imp bnd [] infixes tm)

99+ ppOverload ppo infixes n tm =

100+ fullName n <+> colon <+> align (pprintPTerm ppo bnd [] infixes tm)

101101

102102ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()

103103ihRenderResult h d = do ist <- getIState

@@ -123,7 +123,7 @@ fancifyAnnots ist annot@(AnnName n _ _ _) =

123123 out = displayS . renderPretty 1.0 50 $ renderDocstring o

124124 return (out "")

125125 getTy :: IState -> Name -> String -- fails if name not already extant!

126− getTy ist n = let theTy = pprintPTerm (opt_showimp (idris_options ist)) [] [] (idris_infixes ist) $

126+ getTy ist n = let theTy = pprintPTerm (ppOptionIst ist) [] [] (idris_infixes ist) $

127127 delabTy ist n

128128 in (displayS . renderPretty 1.0 50 $ theTy) ""

129129fancifyAnnots _ annot = annot

src/Idris/Parser.hs+1−1

@@ -1248,7 +1248,7 @@ loadSource h lidr f

12481248 -- Parsing done, now process declarations

12491249

12501250 let ds = namespaces mname ds'

1251− logLvl 3 (show $ showDecls True ds)

1251+ logLvl 3 (show $ showDecls verbosePPOption ds)

12521252 i <- getIState

12531253 logLvl 10 (show (toAlist (idris_implicits i)))

12541254 logLvl 3 (show (idris_infixes i))

src/Idris/Prover.hs+9−9

@@ -110,9 +110,9 @@ dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _ _) =

110110 iputGoal rendered

111111

112112 where

113− showImplicits = opt_showimp (idris_options ist)

113+ ppo = ppOptionIst ist

114114

115− tPretty bnd t = pprintPTerm showImplicits bnd [] (idris_infixes ist) $ delab ist t

115+ tPretty bnd t = pprintPTerm ppo bnd [] (idris_infixes ist) $ delab ist t

116116

117117 assumptionNames :: Env -> [Name]

118118 assumptionNames = map fst

@@ -237,16 +237,16 @@ ploop fn d prompt prf e h

237237 ctxt' = envCtxt env ctxt

238238 putIState ist { tt_ctxt = ctxt' }

239239 (tm, ty) <- elabVal toplevel False t

240− let imp = opt_showimp (idris_options ist)

240+ let ppo = ppOptionIst ist

241241 ty' = normaliseC ctxt [] ty

242242 h = idris_outh ist

243243 infixes = idris_infixes ist

244244 case tm of

245245 TType _ ->

246− ihPrintTermWithType h (prettyImp imp PType) type1Doc

246+ ihPrintTermWithType h (prettyImp ppo PType) type1Doc

247247 _ -> let bnd = map (\x -> (fst x, False)) env in

248− ihPrintTermWithType h (pprintPTerm imp bnd [] infixes (delab ist tm))

249− (pprintPTerm imp bnd [] infixes (delab ist ty))

248+ ihPrintTermWithType h (pprintPTerm ppo bnd [] infixes (delab ist tm))

249+ (pprintPTerm ppo bnd [] infixes (delab ist ty))

250250 putIState ist

251251 return (False, e, False, prf))

252252 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)

@@ -262,10 +262,10 @@ ploop fn d prompt prf e h

262262 (tm, ty) <- elabVal toplevel False t

263263 let tm' = force (normaliseAll ctxt' env tm)

264264 ty' = force (normaliseAll ctxt' env ty)

265− imp = opt_showimp (idris_options ist')

265+ ppo = ppOption (idris_options ist')

266266 infixes = idris_infixes ist

267− tmDoc = pprintPTerm imp bnd [] infixes (delab ist' tm')

268− tyDoc = pprintPTerm imp bnd [] infixes (delab ist' ty')

267+ tmDoc = pprintPTerm ppo bnd [] infixes (delab ist' tm')

268+ tyDoc = pprintPTerm ppo bnd [] infixes (delab ist' ty')

269269 ihPrintTermWithType (idris_outh ist') tmDoc tyDoc

270270 putIState ist

271271 return (False, e, False, prf))

src/Idris/REPL.hs+23−24

@@ -312,34 +312,34 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.SetOpt IdeSlave.ErrContext b) =

312312runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =

313313 do ist <- getIState

314314 let mvs = reverse $ map fst (idris_metavars ist) \\ primDefs

315− imp <- impShow

315+ let ppo = ppOptionIst ist

316316 let mvarTys = map (delabTy ist) mvs

317317 let res = (IdeSlave.SymbolAtom "ok",

318318 zipWith (\ n (prems, concl) -> (n, prems, concl))

319319 (map (IdeSlave.StringAtom . show) mvs)

320− (map (sexpGoal ist cols imp [] . getGoal) mvarTys))

320+ (map (sexpGoal ist cols ppo [] . getGoal) mvarTys))

321321 runIO . putStrLn $ IdeSlave.convSExp "return" res id

322322 where getGoal :: PTerm -> ([(Name, PTerm)], PTerm)

323323 getGoal (PPi _ n t sc) = let (prems, conc) = getGoal sc

324324 in ((n, t):prems, conc)

325325 getGoal tm = ([], tm)

326− sexpGoal :: IState -> Int -> Bool -> [Name] -> ([(Name, PTerm)], PTerm)

326+ sexpGoal :: IState -> Int -> PPOption -> [Name] -> ([(Name, PTerm)], PTerm)

327327 -> ([(String, String, SpanList OutputAnnotation)],

328328 (String, SpanList OutputAnnotation))

329− sexpGoal ist cols imp ns ([], concl) =

329+ sexpGoal ist cols ppo ns ([], concl) =

330330 let infixes = idris_infixes ist

331331 concl' = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $

332− pprintPTerm imp (zip ns (repeat False)) [] infixes concl

332+ pprintPTerm ppo (zip ns (repeat False)) [] infixes concl

333333 in ([], concl')

334− sexpGoal ist cols imp ns ((n, t):ps, concl) =

334+ sexpGoal ist cols ppo ns ((n, t):ps, concl) =

335335 let n' = case n of

336336 NS (UN nm) ns -> str nm

337337 UN nm | ('_':'_':_) <- str nm -> "_"

338338 | otherwise -> str nm

339339 _ -> "_"

340340 (t', spans) = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $

341− pprintPTerm imp (zip ns (repeat False)) [] (idris_infixes ist) t

342− rest = sexpGoal ist cols imp (n:ns) (ps, concl)

341+ pprintPTerm ppo (zip ns (repeat False)) [] (idris_infixes ist) t

342+ rest = sexpGoal ist cols ppo (n:ns) (ps, concl)

343343 in ((n', t', spans) : fst rest, snd rest)

344344runIdeSlaveCommand id orig fn mods (IdeSlave.WhoCalls n) =

345345 case splitName n of

@@ -581,21 +581,21 @@ process h fn (ExecVal t)

581581process h fn (Check (PRef _ n))

582582 = do ctxt <- getContext

583583 ist <- getIState

584− imp <- impShow

584+ let ppo = ppOptionIst ist

585585 case lookupNames n ctxt of

586586 ts@(t:_) ->

587587 case lookup t (idris_metavars ist) of

588588 Just (_, i, _) -> ihRenderResult h . fmap (fancifyAnnots ist) $

589− showMetavarInfo imp ist n i

589+ showMetavarInfo ppo ist n i

590590 Nothing -> ihPrintFunTypes h [] n (map (\n -> (n, delabTy ist n)) ts)

591591 [] -> ihPrintError h $ "No such variable " ++ show n

592592 where

593− showMetavarInfo imp ist n i

593+ showMetavarInfo ppo ist n i

594594 = case lookupTy n (tt_ctxt ist) of

595− (ty:_) -> putTy imp ist i [] (delab ist (errReverse ist ty))

596− putTy :: Bool -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

597− putTy imp ist 0 bnd sc = putGoal imp ist bnd sc

598− putTy imp ist i bnd (PPi _ n t sc)

595+ (ty:_) -> putTy ppo ist i [] (delab ist (errReverse ist ty))

596+ putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

597+ putTy ppo ist 0 bnd sc = putGoal ppo ist bnd sc

598+ putTy ppo ist i bnd (PPi _ n t sc)

599599 = let current = text " " <>

600600 (case n of

601601 MN _ _ -> text "_"

@@ -603,21 +603,21 @@ process h fn (Check (PRef _ n))

603603 _ -> bindingOf n False) <+>

604604 colon <+> align (tPretty bnd ist t) <> line

605605 in

606− current <> putTy imp ist (i-1) ((n,False):bnd) sc

607− putTy imp ist _ bnd sc = putGoal imp ist ((n,False):bnd) sc

608− putGoal imp ist bnd g

606+ current <> putTy ppo ist (i-1) ((n,False):bnd) sc

607+ putTy ppo ist _ bnd sc = putGoal ppo ist ((n,False):bnd) sc

608+ putGoal ppo ist bnd g

609609 = text "--------------------------------------" <$>

610610 annotate (AnnName n Nothing Nothing Nothing) (text $ show n) <+> colon <+>

611611 align (tPretty bnd ist g)

612612

613− tPretty bnd ist t = pprintPTerm (opt_showimp (idris_options ist)) bnd [] (idris_infixes ist) t

613+ tPretty bnd ist t = pprintPTerm (ppOptionIst ist) bnd [] (idris_infixes ist) t

614614

615615

616616process h fn (Check t)

617617 = do (tm, ty) <- elabVal toplevel False t

618618 ctxt <- getContext

619619 ist <- getIState

620− let imp = opt_showimp (idris_options ist)

620+ let ppo = ppOptionIst ist

621621 ty' = normaliseC ctxt [] ty

622622 case tm of

623623 TType _ ->

@@ -664,8 +664,8 @@ process h fn (TotCheck n)

664664 [] -> ihPrintError h $ "Unknown operator " ++ show n

665665 ts -> do ist <- getIState

666666 c <- colourise

667− imp <- impShow

668− let showN = showName (Just ist) [] imp c

667+ let ppo = ppOptionIst ist

668+ let showN = showName (Just ist) [] ppo c

669669 ihPrintResult h . concat . intersperse "\n" .

670670 map (\(n, t) -> showN n ++ " is " ++ showTotal t i) $

671671 ts

@@ -825,7 +825,7 @@ process h fn (DoProofSearch updatefile rec l n hints)

825825 ctxt <- getContext

826826 i <- getIState

827827 return . flip displayS "" . renderPretty 1.0 80 $

828− pprintPTerm False [] [] (idris_infixes i)

828+ pprintPTerm defaultPPOption [] [] (idris_infixes i)

829829 (stripNS

830830 (dropCtxt envlen

831831 (delab i (specialise ctxt [] [(mn, 1)] tm)))))

@@ -958,7 +958,6 @@ process h fn (TestInline t)

958958 ctxt <- getContext

959959 ist <- getIState

960960 let tm' = inlineTerm ist tm

961− imp <- impShow

962961 c <- colourise

963962 iPrintResult (showTm ist (delab ist tm'))

964963process h fn Execute