bfe6499 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Give the pretty-printer access to info about infixes

bfe6499David Raymond Christiansen12 years ago

src/Idris/AbsSyntaxTree.hs+5−4

compare with master

unifiedsplit

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

1127 colour UnderlineText = IdrisColour Nothing True True False False

1128 colour ItalicText = IdrisColour Nothing True False False True

1129

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

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

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

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

1133 -> Doc OutputAnnotation

1134−prettyImp impl = pprintPTerm impl [] []

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

1135

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

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

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

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

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

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

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

1141 -> Doc OutputAnnotation

1142 -> Doc OutputAnnotation

1142−pprintPTerm impl bnd docArgs = prettySe 10 bnd

1143+pprintPTerm impl bnd docArgs infixes = prettySe 10 bnd

1143 where

1144 where

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

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

1145 prettySe p bnd (PQuote r) =

1146 prettySe p bnd (PQuote r) =

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+5−3

@@ -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+10−10

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

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

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

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

612 align (tPretty bnd ist g)

613 align (tPretty bnd ist g)

613

614

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

615

616

617

617process h fn (Check t)

618process h fn (Check t)

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

627 (prettyImp imp (delab ist ty))

628 (prettyImp imp (delab ist ty))

628

629

629process h fn (DocStr n)

630process h fn (DocStr n)

630− = do i <- getIState

631+ = do ist <- getIState

631− let imp = opt_showimp (idris_options i)

632− case lookupCtxtName n (idris_docstrings i) of

632+ case lookupCtxtName n (idris_docstrings ist) of

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

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

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

635 ihRenderResult h (vsep toShow)

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

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

637− return $ pprintDocs imp doc

637+ return $ pprintDocs ist doc

638process h fn Universes

639 = do i <- getIState

640 let cs = idris_constraints i