bfe6499 · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs+5−4

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

11271127 colour UnderlineText = IdrisColour Nothing True True False False

11281128 colour ItalicText = IdrisColour Nothing True False False True

11291129

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

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

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

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

11331133 -> Doc OutputAnnotation

1134−prettyImp impl = pprintPTerm impl [] []

1134+prettyImp impl = pprintPTerm impl [] [] []

11351135

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

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

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

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

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

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

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

11411142 -> Doc OutputAnnotation

1142−pprintPTerm impl bnd docArgs = prettySe 10 bnd

1143+pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

11431144 where

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

11451146 prettySe p bnd (PQuote r) =

src/Idris/Delaborate.hs+1−1

@@ -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 tm = pprintPTerm (opt_showimp (idris_options ist)) bnd [] tm

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

142142

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

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

src/Idris/Docs.hs+22−17

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

11{-# LANGUAGE PatternGuards #-}

2−module Idris.Docs where

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

33

44import Idris.AbsSyntax

55import Idris.AbsSyntaxTree

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

3434showDoc d | nullDocstring d = empty

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

3636

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

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

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

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

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

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

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

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

4242 renderDocstring doc <$>

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

4444 let argshow = showArgs args [] in

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

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

4747 else empty)

4848

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

49+ where imp = opt_showimp (idris_options ist)

50+ infixes = idris_infixes ist

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

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

51− pprintPTerm imp bnd [] ty <>

53+ pprintPTerm imp bnd [] infixes ty <>

5254 showDoc d <> line

5355 :

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

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

5658 = text "Class constraint" <+>

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

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

5860 :

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

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

6163 = text "(implicit)" <+>

6264 bindingOf n True <+> colon <+>

63− pprintPTerm imp bnd [] ty <>

65+ pprintPTerm imp bnd [] infixes ty <>

6466 showDoc d <> line

6567 :

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

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

6870 showArgs [] _ = []

6971

7072

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

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

73−pprintDocs imp (DataDoc t args)

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

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

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

75+pprintDocs ist (DataDoc t args)

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

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

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

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

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

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

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

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

8082 <> line <$>

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

8284 <> line <$>

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

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

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

8587 <$>

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

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

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

9496 params' = zip pNames (repeat False)

9597

9698 pNames = map fst params

97−

99+

100+ imp = opt_showimp (idris_options ist)

101+ infixes = idris_infixes ist

102+

98103 dumpInstance :: PTerm -> Doc OutputAnnotation

99− dumpInstance = pprintPTerm imp params' []

104+ dumpInstance = pprintPTerm imp params' [] infixes

100105

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

102107 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

457457

458458 where

459459 htmlSignature = displayDecorated decorator $ renderCompact signature

460− signature = pprintPTerm False [] names ftype

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

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

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

463463

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

656656 -> IO ()

657657copyDependencies dir =

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

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

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

src/Idris/Output.hs+5−3

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

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

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

9090 ist <- getIState

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

91+ let infixes = idris_infixes ist

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

9293 case idris_outputmode ist of

9394 RawOutput -> consoleDisplayAnnotated h output

9495 IdeSlave n -> ideSlaveReturnAnnotated n h output

9596 where fullName n = prettyName True bnd n

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

97+ ppOverload imp infixes n tm =

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

9799

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

99101ihRenderResult h d = do ist <- getIState

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

119121 out = displayS . renderPretty 1.0 50 $ renderDocstring o

120122 return (out "")

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

123125 delabTy ist n

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

125127fancifyAnnots _ annot = annot

src/Idris/Prover.hs+13−11

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

112112 where

113113 showImplicits = opt_showimp (idris_options ist)

114114

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

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

116116

117117 assumptionNames :: Env -> [Name]

118118 assumptionNames = map fst

@@ -237,15 +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)

241− ty' = normaliseC ctxt [] ty

242− h = idris_outh ist

240+ let imp = opt_showimp (idris_options ist)

241+ ty' = normaliseC ctxt [] ty

242+ h = idris_outh ist

243+ infixes = idris_infixes ist

243244 case tm of

244245 TType _ ->

245246 ihPrintTermWithType h (prettyImp imp PType) type1Doc

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

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

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

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

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

249250 putIState ist

250251 return (False, e, False, prf))

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

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

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

260261 putIState ist'

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

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

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

264− imp = opt_showimp (idris_options ist')

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

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

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

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

265+ imp = opt_showimp (idris_options ist')

266+ infixes = idris_infixes ist

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

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

267269 ihPrintTermWithType (idris_outh ist') tmDoc tyDoc

268270 putIState ist

269271 return (False, e, False, prf))

src/Idris/REPL.hs+10−10

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

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

328328 (String, SpanList OutputAnnotation))

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

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

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

330+ let infixes = idris_infixes ist

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

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

332333 in ([], concl')

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

334335 let n' = case n of

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

337338 | otherwise -> str nm

338339 _ -> "_"

339340 (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

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

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

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

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

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

612613 align (tPretty bnd ist g)

613614

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

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

615616

616617

617618process h fn (Check t)

@@ -627,14 +628,13 @@ process h fn (Check t)

627628 (prettyImp imp (delab ist ty))

628629

629630process h fn (DocStr n)

630− = do i <- getIState

631− let imp = opt_showimp (idris_options i)

632− case lookupCtxtName n (idris_docstrings i) of

631+ = do ist <- getIState

632+ case lookupCtxtName n (idris_docstrings ist) of

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

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

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

635635 ihRenderResult h (vsep toShow)

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

637− return $ pprintDocs imp doc

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

637+ return $ pprintDocs ist doc

638638process h fn Universes

639639 = do i <- getIState

640640 let cs = idris_constraints i