5e3c248 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Change impl argument to a pretty printing opt record

commit5e3c248b0c28fec999debc8313d5694bff37f5a0 authorPeter Minten <peter.minten@online.nl> dateMon 28 Apr 2014, 19:12 (12 years ago) parent89c3853

9 files changed+123−106

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+69−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+69−51

@@ -95,6 +95,24 @@ 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+

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

99117

100118-- | The output mode in use

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

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

10901108

10911109instance Show PTerm where

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

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

10931111

10941112instance Show PDecl where

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

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

10961114

10971115instance Show PClause where

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

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

10991117

11001118instance Show PData where

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

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

11021120

11031121instance Pretty PTerm OutputAnnotation where

1104− pretty = prettyImp False

1122+ pretty = prettyImp defaultPPOption

11051123

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

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

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

11291147 colour ItalicText = IdrisColour Nothing True False False True

11301148

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

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

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

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

11341152 -> Doc OutputAnnotation

11351153prettyImp impl = pprintPTerm impl [] [] []

11361154

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

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

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

1157+prettyIst ist = pprintPTerm (ppOption (idris_options ist)) [] [] (idris_infixes ist)

11401158

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

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

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

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

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

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

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

11471165 -> Doc OutputAnnotation

1148−pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

1166+pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

11491167 where

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

11511169 prettySe p bnd (PQuote r) =

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

11541172 prettySe p bnd e

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

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

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

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

11581176 prettySe p bnd (PLam n ty sc) =

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

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

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

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

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

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

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

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

11691187 bracket p 2 . group $

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

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

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

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

11791197 _ -> empty

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

1181− | impl =

1199+ | ppopt_impl ppo =

11821200 bracket p 2 $

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

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

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

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

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

11991217 | 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

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

1219+ if isAlpha (thead nm)

1220+ then prettyName (ppopt_impl ppo) bnd f

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

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

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

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

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

12071225 | UN nm <- basename op

12081226 , not (tnull nm) &&

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

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

12101228 case getExps args of

12111229 [] -> enclose lparen rparen opName

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

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

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

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

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

1218− where opName = prettyName impl bnd op

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

12191237 f = getFixity (opStr op)

12201238 left l = case f of

12211239 Nothing -> prettySe (-1) bnd l

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

12351253 fp = prettySe 1 bnd f

12361254 in

12371255 bracket p 1 . group $

1238− if impl

1256+ if ppopt_impl ppo

12391257 then if null as

12401258 then fp

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

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

13401358 basename n = n

13411359

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

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

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

13441362 slist' p bnd (PRef _ nil)

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

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

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

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

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

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

14151433 strName other = show other

14161434

14171435

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

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

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

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

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

14221440 where

14231441 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

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

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

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

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

14281446 where

14291447 showWs [] = empty

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

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

14311449

14321450

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))

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

1452+showDImp ppo (PDatadecl n ty cons)

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

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

14371455

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

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

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

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

14401458

14411459showDeclImp _ (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)

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

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

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

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

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

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

14481466showDeclImp _ (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

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

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

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

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

14531471showDeclImp _ _ = text "..."

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

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

14551473

14561474instance Show (Doc OutputAnnotation) where

14571475 show = flip (displayS . renderCompact) ""

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

14781496-- | Show Idris name

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

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

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

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

14821500 -> Bool -- ^^ whether to colourise

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

14841502 -> String

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

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

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

14871505 Nothing -> showbasic n

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

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

14891507 showbasic n@(UN _) = showCG n

14901508 showbasic (MN _ s) = str s

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

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

15091527 -> String

15101528showTm ist = displayDecorated (consoleDecorate ist) .

15111529 renderPretty 0.8 100000 .

1512− prettyImp (opt_showimp (idris_options ist))

1530+ prettyImp (ppOption (idris_options ist))

15131531

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

15151533showTmImpls :: PTerm -> String

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

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

15171535

15181536

15191537instance 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 (ppOption (idris_options 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) [] (ppOption (idris_options 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 = ppOption (idris_options 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 = ppOption (idris_options 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

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

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

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

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

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

90− ist <- getIState

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

90+ let ppo = ppOption (idris_options ist)

9191 let infixes = idris_infixes ist

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

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

9393 case idris_outputmode ist of

9494 RawOutput -> consoleDisplayAnnotated h output

9595 IdeSlave n -> ideSlaveReturnAnnotated n h output

9696 where fullName n = prettyName True bnd n

97− ppOverload imp infixes n tm =

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

97+ ppOverload ppo infixes n tm =

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

9999

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

101101ihRenderResult h d = do ist <- getIState

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

121121 out = displayS . renderPretty 1.0 50 $ renderDocstring o

122122 return (out "")

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

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

124+ getTy ist n = let theTy = pprintPTerm (ppOption (idris_options ist)) [] [] (idris_infixes ist) $

125125 delabTy ist n

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

127127fancifyAnnots _ annot = annot

src/Idris/Parser.hs+1−1

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

12471247 -- Parsing done, now process declarations

12481248

12491249 let ds = namespaces mname ds'

1250− logLvl 3 (show $ showDecls True ds)

1250+ logLvl 3 (show $ showDecls verbosePPOption ds)

12511251 i <- getIState

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

12531253 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 = ppOption (idris_options 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 = ppOption (idris_options 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 = ppOption (idris_options 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 = ppOption (idris_options 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 (ppOption (idris_options 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 = ppOption (idris_options 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 = ppOption (idris_options 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