git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1001 from david-christiansen/doc-arg-names

Show argument names in :doc, and don't show undocumented args

commita72453179cc32436de58548cf3b92c9fd3d70e60 authorEdwin Brady <edwin.brady@gmail.com> dateTue 25 Mar 2014, 13:13 (13 years ago) parent5a4daf5d1e12d5
6 files changed+25−21
compare with master
unifiedsplit
src/Idris/AbsSyntax.hs+1−1 src/Idris/AbsSyntaxTree.hs+4−3 src/Idris/Delaborate.hs+1−1 src/Idris/Docs.hs+13−10 src/Idris/Prover.hs+5−5 src/Idris/REPL.hs+1−1
src/Idris/AbsSyntax.hs+1−1
@@ -567,7 +567,7 @@ ihPrintFunTypes h bnd n overloads = do imp <- impShow
567567 RawOutput -> consoleDisplayAnnotated h output
568568 IdeSlave n -> ideSlaveReturnAnnotated n h output
569569 where fullName n = prettyName True bnd n
570− ppOverload imp n tm = fullName n <+> colon <+> align (pprintPTerm imp bnd tm)
570+ ppOverload imp n tm = fullName n <+> colon <+> align (pprintPTerm imp bnd [] tm)
571571
572572ihRenderResult :: Handle -> Doc OutputAnnotation -> Idris ()
573573ihRenderResult h d = do ist <- getIState
src/Idris/AbsSyntaxTree.hs+4−3
@@ -1085,14 +1085,15 @@ consoleDecorate ist (AnnTextFmt fmt) = Idris.Colours.colourise (colour fmt)
10851085prettyImp :: Bool -- ^^ whether to show implicits
10861086 -> PTerm -- ^^ the term to pretty-print
10871087 -> Doc OutputAnnotation
1088−prettyImp impl = pprintPTerm impl []
1088+prettyImp impl = pprintPTerm impl [] []
10891089
10901090-- | Pretty-print a high-level Idris term in some bindings context
10911091pprintPTerm :: Bool -- ^^ whether to show implicits
10921092 -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
1093+ -> [Name] -- ^^ names to always show in pi, even if not used
10931094 -> PTerm -- ^^ the term to pretty-print
10941095 -> Doc OutputAnnotation
1095−pprintPTerm impl bnd = prettySe 10 bnd
1096+pprintPTerm impl bnd docArgs = prettySe 10 bnd
10961097 where
10971098 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
10981099 prettySe p bnd (PQuote r) =
@@ -1112,7 +1113,7 @@ pprintPTerm impl bnd = prettySe 10 bnd
11121113 prettySe 10 bnd v <+> kwd "in" </>
11131114 prettySe 10 ((n, False):bnd) sc
11141115 prettySe p bnd (PPi (Exp l s _) n ty sc)
1115− | n `elem` allNamesIn sc || impl =
1116+ | n `elem` allNamesIn sc || impl || n `elem` docArgs =
11161117 let open = if Lazy `elem` l then text "|" <> lparen else lparen in
11171118 bracket p 2 . group $
11181119 enclose open rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>
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 = pprintPTerm (opt_showimp (idris_options ist))
141+pprintTerm' ist bnd tm = pprintPTerm (opt_showimp (idris_options ist)) bnd [] tm
142142
143143pshow :: IState -> Err -> String
144144pshow ist err = displayDecorated (consoleDecorate ist) .
src/Idris/Docs.hs+13−10
@@ -12,6 +12,7 @@ import Util.Pretty
1212
1313import Data.Maybe
1414import Data.List
15+import qualified Data.Text as T
1516
1617-- TODO: Only include names with public/abstract accessibility
1718
@@ -33,30 +34,32 @@ showDoc d | nullDocstring d = empty
3334
3435pprintFD :: Bool -> FunDoc -> Doc OutputAnnotation
3536pprintFD imp (FD n doc args ty f)
36− = nest 4 (prettyName imp [] n <+> colon <+> prettyImp imp ty <$> renderDocstring doc <$>
37+ = nest 4 (prettyName imp [] n <+> colon <+>
38+ pprintPTerm imp [] [ n | (n@(UN n'),_,_,_) <- args
39+ , not (T.isPrefixOf (T.pack "__") n') ] ty <$>
40+ renderDocstring doc <$>
3741 maybe empty (\f -> text (show f) <> line) f <>
3842 let argshow = showArgs args [] in
3943 if not (null argshow)
4044 then nest 4 $ text "Arguments:" <$> vsep argshow
4145 else empty)
4246
43− where showArgs ((n, ty, Exp {}, d):args) bnd
47+ where showArgs ((n, ty, Exp {}, Just d):args) bnd
4448 = bindingOf n False <+> colon <+>
45− pprintPTerm imp bnd ty <>
46− showDoc (maybe emptyDocstring id d) <> line
49+ pprintPTerm imp bnd [] ty <>
50+ showDoc d <> line
4751 :
4852 showArgs args ((n, False):bnd)
49− showArgs ((n, ty, Constraint {}, d):args) bnd
53+ showArgs ((n, ty, Constraint {}, Just d):args) bnd
5054 = text "Class constraint" <+>
51− pprintPTerm imp bnd ty <> showDoc (maybe emptyDocstring id d) <> line
55+ pprintPTerm imp bnd [] ty <> showDoc d <> line
5256 :
5357 showArgs args ((n, True):bnd)
54− showArgs ((n, ty, Imp {}, d):args) bnd
55− | Just d' <- d
58+ showArgs ((n, ty, Imp {}, Just d):args) bnd
5659 = text "(implicit)" <+>
5760 bindingOf n True <+> colon <+>
58− pprintPTerm imp bnd ty <>
59− showDoc d' <> line
61+ pprintPTerm imp bnd [] ty <>
62+ showDoc d <> line
6063 :
6164 showArgs args ((n, True):bnd)
6265 showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)
src/Idris/Prover.hs+5−5
@@ -104,7 +104,7 @@ dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _ _) =
104104 where
105105 showImplicits = opt_showimp (idris_options ist)
106106
107− tPretty bnd t = pprintPTerm showImplicits bnd $ delab ist t
107+ tPretty bnd t = pprintPTerm showImplicits bnd [] $ delab ist t
108108
109109 assumptionNames :: Env -> [Name]
110110 assumptionNames = map fst
@@ -236,8 +236,8 @@ ploop fn d prompt prf e h
236236 TType _ ->
237237 ihPrintTermWithType h (prettyImp imp PType) type1Doc
238238 _ -> let bnd = map (\x -> (fst x, False)) env in
239− ihPrintTermWithType h (pprintPTerm imp bnd (delab ist tm))
240− (pprintPTerm imp bnd (delab ist ty))
239+ ihPrintTermWithType h (pprintPTerm imp bnd [] (delab ist tm))
240+ (pprintPTerm imp bnd [] (delab ist ty))
241241 putIState ist
242242 return (False, e, False, prf))
243243 (\err -> do putIState ist { tt_ctxt = ctxt } ; ierror err)
@@ -254,8 +254,8 @@ ploop fn d prompt prf e h
254254 let tm' = force (normaliseAll ctxt' env tm)
255255 ty' = force (normaliseAll ctxt' env ty)
256256 imp = opt_showimp (idris_options ist')
257− tmDoc = pprintPTerm imp bnd (delab ist' tm')
258− tyDoc = pprintPTerm imp bnd (delab ist' ty')
257+ tmDoc = pprintPTerm imp bnd [] (delab ist' tm')
258+ tyDoc = pprintPTerm imp bnd [] (delab ist' ty')
259259 ihPrintTermWithType (idris_outh ist') tmDoc tyDoc
260260 putIState ist
261261 return (False, e, False, prf))
src/Idris/REPL.hs+1−1
@@ -518,7 +518,7 @@ process h fn (Check (PRef _ n))
518518 annotate (AnnName n Nothing Nothing) (text $ show n) <+> colon <+>
519519 align (tPretty bnd ist g)
520520
521− tPretty bnd ist t = pprintPTerm (opt_showimp (idris_options ist)) bnd t
521+ tPretty bnd ist t = pprintPTerm (opt_showimp (idris_options ist)) bnd [] t
522522
523523
524524process h fn (Check t)