7922bb6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #1175 from david-christiansen/pprint-assoc

7922bb6David Christiansen12 years ago

src/Idris/AbsSyntaxTree.hs+32−6

compare with master

unifiedsplit

@@ -31,6 +31,7 @@ import qualified Data.Map as M

31import Data.Either

32import qualified Data.Set as S

33import Data.Word (Word)

34+import Data.Maybe (fromMaybe)

35import Debug.Trace

36import Debug.Trace

@@ -1127,19 +1128,24 @@ consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)

1127 colour UnderlineText = IdrisColour Nothing True True False False

1128 colour UnderlineText = IdrisColour Nothing True True False False

1128 colour ItalicText = IdrisColour Nothing True False False True

1129 colour ItalicText = IdrisColour Nothing True False False True

1129

1130

1130−-- | Pretty-print a high-level closed Idris term

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

1131prettyImp :: Bool -- ^^ whether to show implicits

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

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

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

1133 -> Doc OutputAnnotation

1134 -> Doc OutputAnnotation

1134−prettyImp impl = pprintPTerm impl [] []

1135+prettyImp impl = pprintPTerm impl [] [] []

1135

1136

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

1138+prettyIst :: IState -> PTerm -> Doc OutputAnnotation

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

1140+

1136−-- | Pretty-print a high-level Idris term in some bindings context

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

1137pprintPTerm :: Bool -- ^^ whether to show implicits

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

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

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

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

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

1145+ -> [FixDecl] -- ^^ Fixity declarations

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

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

1141 -> Doc OutputAnnotation

1147 -> Doc OutputAnnotation

1142−pprintPTerm impl bnd docArgs = prettySe 10 bnd

1148+pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

1143 where

1149 where

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

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

1145 prettySe p bnd (PQuote r) =

1151 prettySe p bnd (PQuote r) =

@@ -1204,13 +1210,23 @@ pprintPTerm impl bnd docArgs = prettySe 10 bnd

1204 case getExps args of

1210 case getExps args of

1205 [] -> enclose lparen rparen opName

1211 [] -> enclose lparen rparen opName

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

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

1213+ [l,r] -> let precedence = fromMaybe 20 (fmap prec f)

1207− [l,r] -> bracket p 1 $ inFix l r

1214+ in bracket p precedence $ inFix l r

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

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

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

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

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

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

1211 where opName = prettyName impl bnd op

1218 where opName = prettyName impl bnd op

1219+ f = getFixity (opStr op)

1220+ left l = case f of

1221+ Nothing -> prettySe (-1) bnd l

1222+ Just (Infixl p') -> prettySe p' bnd l

1223+ Just f' -> prettySe (prec f'-1) bnd l

1224+ right r = case f of

1225+ Nothing -> prettySe (-1) bnd r

1226+ Just (Infixr p') -> prettySe p' bnd r

1227+ Just f' -> prettySe (prec f'-1) bnd r

1212 inFix l r = align . group $

1228 inFix l r = align . group $

1213− (prettySe 1 bnd l <+> opName) <$> group (prettySe 0 bnd r)

1229+ (left l <+> opName) <$> group (right r)

1214 prettySe p bnd (PApp _ hd@(PRef fc f) [tm])

1230 prettySe p bnd (PApp _ hd@(PRef fc f) [tm])

1215 | PConstant (Idris.Core.TT.Str str) <- getTm tm,

1231 | PConstant (Idris.Core.TT.Str str) <- getTm tm,

1216 f == sUN "Symbol_" = char '\'' <> prettySe 10 bnd (PRef fc (sUN str))

1232 f == sUN "Symbol_" = char '\'' <> prettySe 10 bnd (PRef fc (sUN str))

@@ -1315,6 +1331,10 @@ pprintPTerm impl bnd docArgs = prettySe 10 bnd

1315 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation

1331 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation

1316 annName n = annotate (AnnName n Nothing Nothing Nothing)

1332 annName n = annotate (AnnName n Nothing Nothing Nothing)

1317

1333

1334+ opStr :: Name -> String

1335+ opStr (NS n _) = opStr n

1336+ opStr (UN n) = T.unpack n

1337+

1318 basename :: Name -> Name

1338 basename :: Name -> Name

1319 basename (NS n _) = basename n

1339 basename (NS n _) = basename n

1320 basename n = n

1340 basename n = n

@@ -1368,6 +1388,12 @@ pprintPTerm impl bnd docArgs = prettySe 10 bnd

1368

1388

1369 kwd = annotate AnnKeyword . text

1389 kwd = annotate AnnKeyword . text

1370

1390

1391+ fixities :: M.Map String Fixity

1392+ fixities = M.fromList [(s, f) | (Fix f s) <- infixes]

1393+

1394+ getFixity :: String -> Maybe Fixity

1395+ getFixity = flip M.lookup fixities

1396+

1371-- | Pretty-printer helper for the binding site of a name

1397-- | Pretty-printer helper for the binding site of a name

1372bindingOf :: Name -- ^^ the bound name

1398bindingOf :: Name -- ^^ the bound name

1373 -> Bool -- ^^ whether the name is implicit

1399 -> Bool -- ^^ whether the name is implicit

src/Idris/CaseSplit.hs+4−1

@@ -22,6 +22,7 @@ import Idris.Core.Evaluate

23import Data.Maybe

24import Data.Char

25+import Data.List (isPrefixOf, isSuffixOf)

25import Control.Monad

26import Control.Monad

26import Control.Monad.State.Strict

27import Control.Monad.State.Strict

@@ -299,7 +300,9 @@ replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)

299 else c : updatePat (not (isAlphaNum c)) n tm rest

300 else c : updatePat (not (isAlphaNum c)) n tm rest

300 updatePat start n tm (c:rest) = c : updatePat (not (isAlpha c)) n tm rest

301 updatePat start n tm (c:rest) = c : updatePat (not (isAlpha c)) n tm rest

301

302

302− addBrackets tm | ' ' `elem` tm = "(" ++ tm ++ ")"

303+ addBrackets tm | ' ' `elem` tm

304+ , not (isPrefixOf "(" tm)

305+ , not (isSuffixOf ")" tm) = "(" ++ tm ++ ")"

303 | otherwise = tm

306 | otherwise = tm

304

307

305getUniq nm i

308getUniq nm i

src/Idris/Delaborate.hs+1−1

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

138pprintTerm ist = pprintTerm' ist []

139

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

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

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

142

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

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

src/Idris/Docs.hs+22−17

@@ -1,5 +1,5 @@

1{-# LANGUAGE PatternGuards #-}

2−module Idris.Docs where

2+module Idris.Docs (pprintDocs, getDocs, FunDoc(..), Docs (..)) where

4import Idris.AbsSyntax

5import Idris.AbsSyntaxTree

@@ -34,11 +34,11 @@ data Docs = FunDoc FunDoc

34showDoc d | nullDocstring d = empty

35 | otherwise = text " -- " <> renderDocstring d

37−pprintFD :: Bool -> FunDoc -> Doc OutputAnnotation

37+pprintFD :: IState -> FunDoc -> Doc OutputAnnotation

38−pprintFD imp (FD n doc args ty f)

38+pprintFD ist (FD n doc args ty f)

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

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

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

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

42 renderDocstring doc <$>

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

44 let argshow = showArgs args [] in

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

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

47 else empty)

49+ where imp = opt_showimp (idris_options ist)

50+ infixes = idris_infixes ist

49− where showArgs ((n, ty, Exp {}, Just d):args) bnd

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

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

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

51− pprintPTerm imp bnd [] ty <>

53+ pprintPTerm imp bnd [] infixes ty <>

52 showDoc d <> line

54 showDoc d <> line

53 :

55 :

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

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

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

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

56 = text "Class constraint" <+>

58 = text "Class constraint" <+>

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

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

58 :

60 :

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

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

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

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

61 = text "(implicit)" <+>

63 = text "(implicit)" <+>

62 bindingOf n True <+> colon <+>

64 bindingOf n True <+> colon <+>

63− pprintPTerm imp bnd [] ty <>

65+ pprintPTerm imp bnd [] infixes ty <>

64 showDoc d <> line

66 showDoc d <> line

65 :

67 :

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

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

@@ -68,20 +70,20 @@ pprintFD imp (FD n doc args ty f)

68 showArgs [] _ = []

70 showArgs [] _ = []

71−pprintDocs :: Bool -> Docs -> Doc OutputAnnotation

73+pprintDocs :: IState -> Docs -> Doc OutputAnnotation

72−pprintDocs imp (FunDoc d) = pprintFD imp d

74+pprintDocs ist (FunDoc d) = pprintFD ist d

73−pprintDocs imp (DataDoc t args)

75+pprintDocs ist (DataDoc t args)

74− = text "Data type" <+> pprintFD imp t <$>

76+ = text "Data type" <+> pprintFD ist t <$>

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

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

76− vsep (map (pprintFD imp) args))

78+ vsep (map (pprintFD ist) args))

77−pprintDocs imp (ClassDoc n doc meths params instances)

79+pprintDocs ist (ClassDoc n doc meths params instances)

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

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

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

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

80 <> line <$>

82 <> line <$>

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

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

82 <> line <$>

84 <> line <$>

83 nest 4 (text "Methods:" <$>

85 nest 4 (text "Methods:" <$>

84− vsep (map (pprintFD imp) meths))

86+ vsep (map (pprintFD ist) meths))

85 <$>

87 <$>

86 nest 4 (text "Instances:" <$>

88 nest 4 (text "Instances:" <$>

87 vsep (if null instances' then [text "<no instances>"]

89 vsep (if null instances' then [text "<no instances>"]

@@ -94,9 +96,12 @@ pprintDocs imp (ClassDoc n doc meths params instances)

94 params' = zip pNames (repeat False)

96 params' = zip pNames (repeat False)

96 pNames = map fst params

98 pNames = map fst params

97−

99+

100+ imp = opt_showimp (idris_options ist)

101+ infixes = idris_infixes ist

102+

98 dumpInstance :: PTerm -> Doc OutputAnnotation

103 dumpInstance :: PTerm -> Doc OutputAnnotation

99− dumpInstance = pprintPTerm imp params' []

104+ dumpInstance = pprintPTerm imp params' [] infixes

100

105

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

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

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

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

src/Idris/IdrisDoc.hs+2−2

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

457

458 where

459 htmlSignature = displayDecorated decorator $ renderCompact signature

460− signature = pprintPTerm False [] names ftype

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

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

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

463

@@ -656,4 +656,4 @@ copyDependencies :: FilePath -- ^ The base directory to which

656 -> IO ()

657copyDependencies dir =

658 do styles <- getDataFileName $ "idrisdoc" </> "styles.css"

659− copyFile styles (dir </> "styles.css")

659+ copyFile styles (dir </> "styles.css")

src/Idris/Output.hs+6−4

@@ -78,7 +78,7 @@ ideSlaveReturnAnnotated n h out = do ist <- getIState

79ihPrintTermWithType :: Handle -> Doc OutputAnnotation -> Doc OutputAnnotation -> Idris ()

80ihPrintTermWithType h tm ty = do ist <- getIState

81− let output = tm <+> colon <+> ty

81+ let output = tm <+> colon <+> align ty

82 case idris_outputmode ist of

83 RawOutput -> consoleDisplayAnnotated h output

84 IdeSlave n -> ideSlaveReturnAnnotated n h output

@@ -88,12 +88,14 @@ ihPrintFunTypes :: Handle -> [(Name, Bool)] -> Name -> [(Name, PTerm)] -> Idris

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

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

90 ist <- getIState

91+ let infixes = idris_infixes ist

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

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

92 case idris_outputmode ist of

93 case idris_outputmode ist of

93 RawOutput -> consoleDisplayAnnotated h output

94 RawOutput -> consoleDisplayAnnotated h output

94 IdeSlave n -> ideSlaveReturnAnnotated n h output

95 IdeSlave n -> ideSlaveReturnAnnotated n h output

95 where fullName n = prettyName True bnd n

96 where fullName n = prettyName True bnd n

97+ ppOverload imp infixes n tm =

96− ppOverload imp n tm = fullName n <+> colon <+> align (pprintPTerm imp bnd [] tm)

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

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

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

99ihRenderResult h d = do ist <- getIState

101ihRenderResult h d = do ist <- getIState

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

119 out = displayS . renderPretty 1.0 50 $ renderDocstring o

121 out = displayS . renderPretty 1.0 50 $ renderDocstring o

120 return (out "")

122 return (out "")

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

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

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

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

123 delabTy ist n

125 delabTy ist n

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

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

125fancifyAnnots _ annot = annot

127fancifyAnnots _ annot = annot

src/Idris/Prover.hs+13−11

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

112 where

113 showImplicits = opt_showimp (idris_options ist)

114

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

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

116

117 assumptionNames :: Env -> [Name]

118 assumptionNames = map fst

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

237 ctxt' = envCtxt env ctxt

238 putIState ist { tt_ctxt = ctxt' }

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

240− let imp = opt_showimp (idris_options ist)

240+ let imp = opt_showimp (idris_options ist)

241− ty' = normaliseC ctxt [] ty

241+ ty' = normaliseC ctxt [] ty

242− h = idris_outh ist

242+ h = idris_outh ist

243+ infixes = idris_infixes ist

243 case tm of

244 case tm of

244 TType _ ->

245 TType _ ->

245 ihPrintTermWithType h (prettyImp imp PType) type1Doc

246 ihPrintTermWithType h (prettyImp imp PType) type1Doc

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

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

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

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

248− (pprintPTerm imp bnd [] (delab ist ty))

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

249 putIState ist

250 putIState ist

250 return (False, e, False, prf))

251 return (False, e, False, prf))

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

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

@@ -259,11 +260,12 @@ ploop fn d prompt prf e h

259 bnd = map (\x -> (fst x, False)) env

260 bnd = map (\x -> (fst x, False)) env

260 putIState ist'

261 putIState ist'

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

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

262− let tm' = force (normaliseAll ctxt' env tm)

263+ let tm' = force (normaliseAll ctxt' env tm)

263− ty' = force (normaliseAll ctxt' env ty)

264+ ty' = force (normaliseAll ctxt' env ty)

264− imp = opt_showimp (idris_options ist')

265+ imp = opt_showimp (idris_options ist')

266+ infixes = idris_infixes ist

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

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

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

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

267 ihPrintTermWithType (idris_outh ist') tmDoc tyDoc

269 ihPrintTermWithType (idris_outh ist') tmDoc tyDoc

268 putIState ist

270 putIState ist

269 return (False, e, False, prf))

271 return (False, e, False, prf))

src/Idris/REPL.hs+25−26

@@ -327,8 +327,9 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =

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

328 (String, SpanList OutputAnnotation))

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

330+ let infixes = idris_infixes ist

330− let concl' = displaySpans . renderPretty 0.9 cols . fmap (fancifyAnnots ist) $

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

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

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

332 in ([], concl')

333 in ([], concl')

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

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

334 let n' = case n of

335 let n' = case n of

@@ -337,7 +338,7 @@ runIdeSlaveCommand id orig fn mods (IdeSlave.Metavariables cols) =

337 | otherwise -> str nm

338 | otherwise -> str nm

338 _ -> "_"

339 _ -> "_"

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

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

340− pprintPTerm imp (zip ns (repeat False)) [] t

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

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

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

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

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

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

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

@@ -562,21 +563,19 @@ process h fn (Eval t)

562 ist <- getIState

563 ist <- getIState

563 logLvl 3 $ "Raw: " ++ show (tm', ty')

564 logLvl 3 $ "Raw: " ++ show (tm', ty')

564 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'

565 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'

565− let imp = opt_showimp (idris_options ist)

566− tmDoc = prettyImp imp (delab ist tm')

566+ let tmDoc = prettyIst ist (delab ist tm')

567− tyDoc = prettyImp imp (delab ist ty')

567+ tyDoc = prettyIst ist (delab ist ty')

568 ihPrintTermWithType h tmDoc tyDoc

569

570process h fn (ExecVal t)

571 = do ctxt <- getContext

572 ist <- getIState

573− let imp = opt_showimp (idris_options ist)

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

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

575-- let tm' = normaliseAll ctxt [] tm

574-- let tm' = normaliseAll ctxt [] tm

576 let ty' = normaliseAll ctxt [] ty

575 let ty' = normaliseAll ctxt [] ty

577 res <- execute tm

576 res <- execute tm

578− let (resOut, tyOut) = (prettyImp imp (delab ist res),

577+ let (resOut, tyOut) = (prettyIst ist (delab ist res),

579− prettyImp imp (delab ist ty'))

578+ prettyIst ist (delab ist ty'))

580 ihPrintTermWithType h resOut tyOut

579 ihPrintTermWithType h resOut tyOut

581

580

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

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

@@ -611,7 +610,7 @@ process h fn (Check (PRef _ n))

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

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

612 align (tPretty bnd ist g)

611 align (tPretty bnd ist g)

613

612

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

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

615

614

616

615

617process h fn (Check t)

616process h fn (Check t)

@@ -622,19 +621,18 @@ process h fn (Check t)

622 ty' = normaliseC ctxt [] ty

621 ty' = normaliseC ctxt [] ty

623 case tm of

622 case tm of

624 TType _ ->

623 TType _ ->

625− ihPrintTermWithType h (prettyImp imp PType) type1Doc

624+ ihPrintTermWithType h (prettyIst ist PType) type1Doc

626− _ -> ihPrintTermWithType h (prettyImp imp (delab ist tm))

625+ _ -> ihPrintTermWithType h (prettyIst ist (delab ist tm))

627− (prettyImp imp (delab ist ty))

626+ (prettyIst ist (delab ist ty))

628

627

629process h fn (DocStr n)

628process h fn (DocStr n)

630− = do i <- getIState

629+ = do ist <- getIState

631− let imp = opt_showimp (idris_options i)

632− case lookupCtxtName n (idris_docstrings i) of

630+ case lookupCtxtName n (idris_docstrings ist) of

633 [] -> iPrintError $ "No documentation for " ++ show n

631 [] -> iPrintError $ "No documentation for " ++ show n

634− ns -> do toShow <- mapM (showDoc imp) ns

632+ ns -> do toShow <- mapM (showDoc ist) ns

635 ihRenderResult h (vsep toShow)

633 ihRenderResult h (vsep toShow)

636− where showDoc imp (n, d) = do doc <- getDocs n

634+ where showDoc ist (n, d) = do doc <- getDocs n

637− return $ pprintDocs imp doc

635+ return $ pprintDocs ist doc

638process h fn Universes

636process h fn Universes

639 = do i <- getIState

637 = do i <- getIState

640 let cs = idris_constraints i

638 let cs = idris_constraints i

@@ -826,9 +824,11 @@ process h fn (DoProofSearch updatefile rec l n hints)

826 (tm, ty) <- elabVal toplevel False (PRef fc mn)

824 (tm, ty) <- elabVal toplevel False (PRef fc mn)

827 ctxt <- getContext

825 ctxt <- getContext

828 i <- getIState

826 i <- getIState

827+ return . flip displayS "" . renderPretty 1.0 80 $

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

829− return $ show (stripNS

829+ (stripNS

830− (dropCtxt envlen

830+ (dropCtxt envlen

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

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

832 (\e -> return ("?" ++ show n))

833 if updatefile then

834 do let fb = fn ++ "~"

@@ -1051,15 +1051,14 @@ process h fn (SetConsoleWidth w) = setWidth w

1051

1052process h fn (Apropos a) =

1053 do ist <- getIState

1054− let impl = opt_showimp (idris_options ist)

1055 let names = apropos ist (T.pack a)

1054 let names = apropos ist (T.pack a)

1056 let aproposInfo = [ (n,

1055 let aproposInfo = [ (n,

1057 delabTy ist n,

1056 delabTy ist n,

1058 fmap (overview . fst) (lookupCtxtExact n (idris_docstrings ist)))

1057 fmap (overview . fst) (lookupCtxtExact n (idris_docstrings ist)))

1059 | n <- sort names, isUN n ]

1058 | n <- sort names, isUN n ]

1060− ihRenderResult h $ vsep (map (renderApropos impl) aproposInfo)

1059+ ihRenderResult h $ vsep (map (renderApropos ist) aproposInfo)

1061− where renderApropos impl (name, ty, docs) =

1060+ where renderApropos ist (name, ty, docs) =

1062− prettyName True [] name <+> colon <+> align (prettyImp impl ty) <$>

1061+ prettyName True [] name <+> colon <+> align (prettyIst ist ty) <$>

1063 fromMaybe empty (fmap (\d -> renderDocstring d <> line) docs)

1062 fromMaybe empty (fmap (\d -> renderDocstring d <> line) docs)

1064 isUN (UN _) = True

1063 isUN (UN _) = True

1065 isUN (NS n _) = isUN n

1064 isUN (NS n _) = isUN n

test/interactive001/expected+1−1

@@ -4,7 +4,7 @@ isElem x (y :: xs) = ?isElem_rhs_3

5 localZipWith f (_ :: _) (x :: ys) = ?localZipWith_rhs_1

7−f x :: (map f xs)

7+f x :: map f xs

8isElem2 x (y :: ys) with (_)

9 isElem2 x (y :: ys) | with_pat = ?isElem2_rhs

10 isElem3 x (x :: ys) | (Yes refl) = ?isElem3_rhs_3

test/interactive003/expected+2−2

@@ -1,5 +1,5 @@

1Type checking ./interactive003.idr

2ys

3−x :: (app xs ys)

3+x :: app xs ys

4[]

5−f x y :: (vzipWith f xs ys)

5+f x y :: vzipWith f xs ys