36bcf4b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Show visibility in doc comments.

Currently the result of `:doc` displays totality information for functions. However there are two scenarios where having the accessiblity/visibility information would be beneficial: 1. Type-level computations failing to reduce. A computed value in your type might fail to reduce in the definition of the computing function is not public c.f. exportation of functions computing type synonyms. A good numpty check would be to add this information to the doc output, much as we do for totality status. 2. Working with 'Exported' constructors. Much like exported functions, some data types might be exported rather than public exported. One has to assert the functions visibility by checking the source code, this is cumbersome. This commit adds visibility status to the documentation output. Such that if totality information is to be displayed we output the totality and accessibility information, otherwise we just output the accessibility information.

commit36bcf4b5a8f4dd05879d352ef68b02b61defab91 authorJan de Muijnck-Hughes <jan.deMuijnck-Hughes@glasgow.ac.uk> dateWed 8 May 2019, 21:16 (7 years ago) parent5eebc7b

2 files changed+18−6

compare with master

unifiedsplit

src/Idris/Core/Evaluate.hs+7 src/Idris/Docs.hs+11−6

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