git.iko.soy/Idris-dev
on master help sign in
Fixes #3264 Show auto implicit documentaton in Idris Doc.
088846bJan de Muijnck-Hughes
CHANGELOG.md+5
compare with master
unifiedsplit
@@ -26,6 +26,11 @@
26* The File Effect has been updated to take into account changes in
26* The File Effect has been updated to take into account changes in
27 `Prelude.File` and to provide a 'better' API.
27 `Prelude.File` and to provide a 'better' API.
28
28
29+## Tool updates
30+
31+* Idris' documentation system now displays the documentation for auto
32+ implicits in the output of `:doc`. This is tested for in `docs005`.
33+
29# New in 0.12:
34# New in 0.12:
30
35
31## Language updates
36## Language updates
idris.cabal+9
@@ -858,6 +858,15 @@ Extra-source-files:
858 test/docs003/input
858 test/docs003/input
859 test/docs003/*.idr
859 test/docs003/*.idr
860 test/docs003/expected
860 test/docs003/expected
861+ test/docs004/run
862+ test/docs004/input
863+ test/docs004/*.idr
864+ test/docs004/expected
865+ test/docs005/run
866+ test/docs005/input
867+ test/docs005/*.idr
868+ test/docs005/expected
869+
861
870
862 benchmarks/ALL
871 benchmarks/ALL
863 benchmarks/*.pl
872 benchmarks/*.pl
src/Idris/Docs.hs+56−43
@@ -69,49 +69,62 @@ showDoc ist d
69 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) d
69 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) d
70
70
71pprintFD :: IState -> Bool -> Bool -> FunDoc -> Doc OutputAnnotation
71pprintFD :: IState -> Bool -> Bool -> FunDoc -> Doc OutputAnnotation
72−pprintFD ist totalityFlag nsFlag (FD n doc args ty f)
72+pprintFD ist totalityFlag nsFlag (FD n doc args ty f) =
73− = nest 4 (prettyName True nsFlag [] n <+> colon <+>
73+ nest 4 (prettyName True nsFlag [] n
74+ <+> colon
74− pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args
75+ <+> pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args
75− , not (T.isPrefixOf (T.pack "__") n') ] infixes ty <$>
76+ , not (T.isPrefixOf (T.pack "__") n') ] infixes ty
76− -- show doc
77+ -- show doc
77− renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc <$>
78+ <$> renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc
78− -- show fixity
79+ -- show fixity
79− maybe empty (\f -> text (show f) <> line) f <>
80+ <$> maybe empty (\f -> text (show f) <> line) f
80− -- show arguments doc
81+ -- show arguments doc
81− let argshow = showArgs args [] in
82+ <> let argshow = showArgs args [] in
82− (if not (null argshow)
83+ (if not (null argshow)
83− then nest 4 $ text "Arguments:" <$> vsep argshow
84+ then nest 4 $ text "Arguments:" <$> vsep argshow
84− else empty) <>
85+ else empty)
85− -- show totality status
86+ -- show totality status
86− let totality = getTotality in
87+ <> let totality = getTotality in
87− (if totalityFlag && not (null totality) then
88+ (if totalityFlag && not (null totality)
88− line <> (vsep . map (\t -> text "The function is" <+> t) $ totality)
89+ then line <> (vsep . map (\t -> text "The function is" <+> t) $ totality)
89− else
90− empty))
90+ else empty))
91−
91+
92+ where
92− where ppo = ppOptionIst ist
93+ ppo = ppOptionIst ist
94+
93− infixes = idris_infixes ist
95+ infixes = idris_infixes ist
96+
97+ -- Recurse over and show the Function's Documented arguments
94− showArgs ((n, ty, Exp {}, Just d):args) bnd
98+ showArgs ((n, ty, Exp {}, Just d):args) bnd = -- Explicitly bound.
95− = bindingOf n False <+> colon <+>
99+ bindingOf n False
100+ <+> colon
96− pprintPTerm ppo bnd [] infixes ty <>
101+ <+> pprintPTerm ppo bnd [] infixes ty
97− showDoc ist d <> line
102+ <> showDoc ist d
98− :
99− showArgs args ((n, False):bnd)
103+ <> line : showArgs args ((n, False):bnd)
100− showArgs ((n, ty, Constraint {}, Just d):args) bnd
104+ showArgs ((n, ty, Constraint {}, Just d):args) bnd = -- Class constraints.
101− = text "Class constraint" <+>
105+ text "Class constraint"
102− pprintPTerm ppo bnd [] infixes ty <> showDoc ist d <> line
106+ <+> pprintPTerm ppo bnd [] infixes ty
103− :
107+ <> showDoc ist d
104− showArgs args ((n, True):bnd)
108+ <> line : showArgs args ((n, True):bnd)
105− showArgs ((n, ty, Imp {}, Just d):args) bnd
109+ showArgs ((n, ty, Imp {}, Just d):args) bnd = -- Implicit arguments.
106− = text "(implicit)" <+>
110+ text "(implicit)"
107− bindingOf n True <+> colon <+>
111+ <+> bindingOf n True
112+ <+> colon
113+ <+> pprintPTerm ppo bnd [] infixes ty
114+ <> showDoc ist d
115+ <> line : showArgs args ((n, True):bnd)
116+ showArgs ((n, ty, TacImp{}, Just d):args) bnd = -- Tacit implicits
117+ text "(auto implicit)"
118+ <+> bindingOf n True
119+ <+> colon
108− pprintPTerm ppo bnd [] infixes ty <>
120+ <+> pprintPTerm ppo bnd [] infixes ty
109− showDoc ist d <> line
121+ <> showDoc ist d
110− :
111− showArgs args ((n, True):bnd)
122+ <> line : showArgs args ((n, True):bnd)
123+ showArgs ((n, _, _, _):args) bnd = -- Anything else
112− showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)
124+ showArgs args ((n, True):bnd)
113− showArgs [] _ = []
125+ showArgs [] _ = [] -- end of arguments
126+
114− getTotality = map (text . show) $ lookupTotal n (tt_ctxt ist)
127+ getTotality = map (text . show) $ lookupTotal n (tt_ctxt ist)
115
128
116pprintFDWithTotality :: IState -> Bool -> FunDoc -> Doc OutputAnnotation
129pprintFDWithTotality :: IState -> Bool -> FunDoc -> Doc OutputAnnotation
117pprintFDWithTotality ist = pprintFD ist True
130pprintFDWithTotality ist = pprintFD ist True
test/docs005/docs005.idrnew file+19
@@ -0,0 +1,19 @@
1+module docs005
2+
3+import Data.List
4+
5+%default total
6+
7+||| A foobar with an auto implicit
8+data Foobar : Type where
9+ ||| New Foo
10+ |||
11+ ||| @xs Some `xs`
12+ ||| @ys Some `ys`
13+ ||| @prf The prf
14+ ||| @prf1 A prf
15+ NewFoo : (xs : List String)
16+ -> (ys : List Nat)
17+ -> {prf1 : NonEmpty xs}
18+ -> {auto prf : NonEmpty ys}
19+ -> Foobar
test/docs005/expectednew file+29
@@ -0,0 +1,29 @@
1+Data type docs005.Foobar : Type
2+ A foobar with an auto implicit
3+
4+Constructors:
5+ NewFoo : (xs : List String) ->
6+ (ys : List Nat) -> {auto prf : NonEmpty ys} -> Foobar
7+ New Foo
8+ Arguments:
9+ xs : List String -- Some xs
10+
11+ ys : List Nat -- Some ys
12+
13+ (implicit) prf1 : NonEmpty xs -- A prf
14+
15+ (auto implicit) prf : NonEmpty ys -- The prf
16+
17+docs005.NewFoo : (xs : List String) ->
18+ (ys : List Nat) -> {auto prf : NonEmpty ys} -> Foobar
19+ New Foo
20+ Arguments:
21+ xs : List String -- Some xs
22+
23+ ys : List Nat -- Some ys
24+
25+ (implicit) prf1 : NonEmpty xs -- A prf
26+
27+ (auto implicit) prf : NonEmpty ys -- The prf
28+
29+ The function is Total
test/docs005/inputnew file+2
@@ -0,0 +1,2 @@
1+:doc Foobar
2+:doc NewFoo
test/docs005/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} --quiet --nocolor docs005.idr < input
3+rm *.ibc