git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4708 from jfdm/show-visibility-in-docs

Show visibility in doc comments.

commit4efeda8867fbff14c371531bc0c49d335b78de3d authorJan de Muijnck-Hughes <jfdm@users.noreply.github.com> dateThu 16 May 2019, 11:14 (7 years ago) parentc8f7604dbf060c
12 files changed+41−21
compare with master
unifiedsplit
CHANGELOG.md+1 src/Idris/Core/Evaluate.hs+7 src/Idris/Docs.hs+11−6 test/docs001/expected+1−1 test/docs002/expected+3−3 test/docs003/expected+3−1 test/docs004/expected+3−3 test/docs005/expected+3−1 test/docs006/expected+1−1 test/idrisdoc009/expected+2 test/interactive005/expected+3−3 test/interfaces001/expected+3−2
CHANGELOG.md+1
@@ -9,6 +9,7 @@
99+ Modules no longer require building if imports have changed but all
1010 interfaces (i.e. types for names declared `export` and definitions of names
1111 declared `public export`) are unchanged.
12++ The result of calling `:doc` now details the accessbility of items as well as their totality.
1213
1314## Miscellaneous updates
1415+ Compiler flag `--optimise-nat-like-types` enables compilation
src/Idris/Core/Evaluate.hs+7
@@ -24,6 +24,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC,
2424 lookupNames, lookupTyName, lookupTyNameExact, lookupTy, lookupTyExact,
2525 lookupP, lookupP_all, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupDefAccExact, lookupVal,
2626 mapDefCtxt, tcReducible,
27+ lookupTotalAccessibility,
2728 lookupTotal, lookupTotalExact, lookupInjectiveExact,
2829 lookupRigCount, lookupRigCountExact,
2930 lookupNameTotal, lookupMetaInformation, lookupTyEnv, isTCDict,
@@ -1167,6 +1168,12 @@ lookupDefAcc n mkpublic ctxt
11671168 where mkp (d, _, inj, a, _, _) = if mkpublic && (not (n == sUN "io_bind" || n == sUN "io_pure"))
11681169 then (d, Public) else (d, a)
11691170
1171+lookupTotalAccessibility :: Name -> Context -> [(Totality,Accessibility)]
1172+lookupTotalAccessibility n ctxt = fmap unpack $ lookupCtxt n (definitions ctxt)
1173+
1174+ where
1175+ unpack ((_,_,_,a,t,_)) = (t,a)
1176+
11701177lookupDefAccExact :: Name -> Bool -> Context ->
11711178 Maybe (Def, Accessibility)
11721179lookupDefAccExact n mkpublic ctxt
src/Idris/Docs.hs+11−6
@@ -94,11 +94,9 @@ pprintFD ist totalityFlag nsFlag (FD n doc args ty f) =
9494 (if not (null argshow)
9595 then nest 4 $ text "Arguments:" <$> vsep argshow
9696 else empty)
97− -- show totality status
98− <> let totality = getTotality in
99− (if totalityFlag && not (null totality)
100− then line <> (vsep . map (\t -> text "The function is" <+> t) $ totality)
101− else empty))
97+ -- show totality and visibility status
98+ <> showTotalVisibility
99+ )
102100
103101 where
104102 ppo = ppOptionIst ist
@@ -135,7 +133,14 @@ pprintFD ist totalityFlag nsFlag (FD n doc args ty f) =
135133 showArgs args ((n, True):bnd)
136134 showArgs [] _ = [] -- end of arguments
137135
138− getTotality = map (text . show) $ lookupTotal n (tt_ctxt ist)
136+ showTotalVisibility =
137+ case lookupTotalAccessibility n (tt_ctxt ist) of
138+ [] -> empty
139+ xs -> line <> vsep (map (doShowTotalVisibility) xs)
140+
141+ doShowTotalVisibility (t,v) = if totalityFlag
142+ then text "The function is:" <+> ((text . show) t) <+> (text "&") <+> ((text . show) v)
143+ else text "The function is:" <+> ((text . show) v)
139144
140145pprintFDWithTotality :: IState -> Bool -> FunDoc -> Doc OutputAnnotation
141146pprintFDWithTotality ist = pprintFD ist True
test/docs001/expected+1−1
@@ -8,7 +8,7 @@ Methods:
88 m : C t => t
99 member of interface
1010
11− The function is Total
11+ The function is: Total & public export
1212Implementations:
1313 C A
1414 implementation of interface
test/docs002/expected+3−3
@@ -1,12 +1,12 @@
11T1 : Type
22 Some documentation
33
4− The function is Total
4+ The function is: Total & public export
55T2 : Type
66 Some other documentation
77
8− The function is Total
8+ The function is: Total & public export
99T3 : Int
1010 Some provided postulate
1111
12− The function is not yet checked for totality
12+ The function is: not yet checked for totality & public export
test/docs003/expected+3−1
@@ -8,7 +8,7 @@ Methods:
88 map : Functor f => (func : a -> b) -> f a -> f b
99 Apply a function across everything of type 'a' in a parameterised type
1010
11− The function is Total
11+ The function is: Total & public export
1212Implementations:
1313 Functor (Pair a)
1414 Functor List
@@ -33,7 +33,9 @@ Named implementation:
3333 docs003.mine : Functor List
3434
3535
36+ The function is: public export
3637Named implementation:
3738 docs003.another : Functor List
3839 More functors!
3940
41+ The function is: public export
test/docs004/expected+3−3
@@ -7,12 +7,12 @@ Main.MkFoo : (bar : Nat) -> (baz : Bool) -> Foo a
77
88 baz : Bool -- A field baz
99
10− The function is Total
10+ The function is: Total & public export
1111Main.Foo.bar : (rec : Foo a) -> Nat
1212 A field bar
1313
14− The function is Total
14+ The function is: Total & public export
1515Main.Foo.baz : (rec : Foo a) -> Bool
1616 A field baz
1717
18− The function is Total
18+ The function is: Total & public export
test/docs005/expected+3−1
@@ -1,6 +1,7 @@
11Data type docs005.Foobar : Type
22 A foobar with an auto implicit
33
4+ The function is: public export
45Constructors:
56 NewFoo : (xs : List String) ->
67 (ys : List Nat) -> {auto prf : NonEmpty ys} -> Foobar
@@ -14,6 +15,7 @@ Constructors:
1415
1516 (auto implicit) prf : NonEmpty ys -- The prf
1617
18+ The function is: public export
1719docs005.NewFoo : (xs : List String) ->
1820 (ys : List Nat) -> {auto prf : NonEmpty ys} -> Foobar
1921 New Foo
@@ -26,4 +28,4 @@ docs005.NewFoo : (xs : List String) ->
2628
2729 (auto implicit) prf : NonEmpty ys -- The prf
2830
29− The function is Total
31+ The function is: Total & public export
test/docs006/expected+1−1
@@ -11,6 +11,6 @@ Methods:
1111 m : Foo t => t
1212 member of interface
1313
14− The function is Total
14+ The function is: Total & public export
1515Implementations:
1616 <no implementations>
test/idrisdoc009/expected+2
@@ -1,10 +1,12 @@
11Data type Test.Test : Type
22 Docs for datatype Test.
33
4+ The function is: public export
45Constructors:
56 MkTest : Test
67
78
9+ The function is: public export
810Module Test:
911 Docs for module Test.
1012
test/interactive005/expected+3−3
@@ -3,7 +3,7 @@ Hello, World
33Main.main : IO ()
44 This is a docstring
55
6− The function is Total
6+ The function is: Total & public export
77Main.main is Total
88Hello, World
99id : a -> a
@@ -27,10 +27,10 @@ Main.main : IO ()
2727 is a
2828 docstring
2929
30− The function is Total
30+ The function is: Total & public export
3131Main.main : IO ()
3232 This is a docstring
3333
34− The function is Total
34+ The function is: Total & public export
3535Nat2 : Type
3636Invalid filename for compiler output "Test.idr"
test/interfaces001/expected+3−2
@@ -8,7 +8,7 @@ Methods:
88 myShow : MyShow a => (x : a) -> String
99 The shower
1010
11− The function is Total
11+ The function is: Total & public export
1212Implementation constructor:
1313 MkMyShow : (myShow : a -> String) -> MyShow a
1414 Build a MyShow
@@ -17,6 +17,7 @@ Implementation constructor:
1717
1818 myShow : a -> String -- The shower
1919
20+ The function is: public export
2021Implementations:
2122 MyShow Integer
2223MkMyShow : (myShow : a -> String) -> MyShow a
@@ -26,4 +27,4 @@ MkMyShow : (myShow : a -> String) -> MyShow a
2627
2728 myShow : a -> String -- The shower
2829
29− The function is Total
30+ The function is: Total & public export