git.iko.soy/Idris-dev
on master help sign in
Show argument names in :doc

Now, :doc will show the names of any documented arguments, even if they are not used in the body. Fixes #1000.

commit7faf4e8c2e2c7df2e8f99aeea05fd25b6e9ab5f4 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 24 Mar 2014, 21:13 (13 years ago) parent7cea995
6 files changed+17−15
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+5−4 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+5−4
@@ -33,7 +33,8 @@ showDoc d | nullDocstring d = empty
3333
3434pprintFD :: Bool -> FunDoc -> Doc OutputAnnotation
3535pprintFD imp (FD n doc args ty f)
36− = nest 4 (prettyName imp [] n <+> colon <+> prettyImp imp ty <$> renderDocstring doc <$>
36+ = nest 4 (prettyName imp [] n <+> colon <+> pprintPTerm imp [] (map (\(n,_,_,_) -> n) args) ty <$>
37+ renderDocstring doc <$>
3738 maybe empty (\f -> text (show f) <> line) f <>
3839 let argshow = showArgs args [] in
3940 if not (null argshow)
@@ -42,20 +43,20 @@ pprintFD imp (FD n doc args ty f)
4243
4344 where showArgs ((n, ty, Exp {}, d):args) bnd
4445 = bindingOf n False <+> colon <+>
45− pprintPTerm imp bnd ty <>
46+ pprintPTerm imp bnd [] ty <>
4647 showDoc (maybe emptyDocstring id d) <> line
4748 :
4849 showArgs args ((n, False):bnd)
4950 showArgs ((n, ty, Constraint {}, d):args) bnd
5051 = text "Class constraint" <+>
51− pprintPTerm imp bnd ty <> showDoc (maybe emptyDocstring id d) <> line
52+ pprintPTerm imp bnd [] ty <> showDoc (maybe emptyDocstring id d) <> line
5253 :
5354 showArgs args ((n, True):bnd)
5455 showArgs ((n, ty, Imp {}, d):args) bnd
5556 | Just d' <- d
5657 = text "(implicit)" <+>
5758 bindingOf n True <+> colon <+>
58− pprintPTerm imp bnd ty <>
59+ pprintPTerm imp bnd [] ty <>
5960 showDoc d' <> line
6061 :
6162 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)