71bdbbb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Properly pretty-print typeclasses for REPL command ':doc'

This requires adding info about the parameters and instances to the ClassDoc constructor of the Docs datatype.

commit71bdbbb3b4c1205c47a4281d7cca08c27a316ef8 authorPaul Koerbitz <paul.koerbitz@theppro.com> dateThu 1 May 2014, 00:58 (12 years ago) parenta1726a2

2 files changed+38−14

compare with master

unifiedsplit

src/Idris/Docs.hs+29−5 src/Idris/IdrisDoc.hs+9−9

src/Idris/Docs.hs+29−5

@@ -27,6 +27,8 @@ data Docs = FunDoc FunDoc

2727 [FunDoc] -- data constructor docs

2828 | ClassDoc Name Docstring -- class docs

2929 [FunDoc] -- method docs

30+ [Name] -- parameter docs

31+ [PTerm] -- instances

3032 deriving Show

3133

3234showDoc d | nullDocstring d = empty

@@ -66,16 +68,35 @@ pprintFD imp (FD n doc args ty f)

6668 showArgs [] _ = []

6769

6870

69−

71+pprintDocs :: Bool -> Docs -> Doc OutputAnnotation

7072pprintDocs imp (FunDoc d) = pprintFD imp d

7173pprintDocs imp (DataDoc t args)

7274 = text "Data type" <+> pprintFD imp t <$>

7375 nest 4 (text "Constructors:" <> line <>

7476 vsep (map (pprintFD imp) args))

75−pprintDocs imp (ClassDoc n doc meths)

76− = text "Type class" <+> prettyName imp [] n <$> -- parameters?

77+pprintDocs imp (ClassDoc n doc meths params instances)

78+ = nest 4 (text "Type class" <+> prettyName imp [] n <>

79+ if nullDocstring doc then empty else line <> renderDocstring doc)

80+ <> line <$>

81+ nest 4 (text "Parameters:" <$>

82+ hsep (punctuate comma (map (prettyName False params') params)))

83+ <> line <$>

7784 nest 4 (text "Methods:" <$>

78− vsep (map (pprintFD imp) meths))

85+ vsep (map (pprintFD imp) meths))

86+ <$>

87+ nest 4 (text "Instances:" <$>

88+ let instances' = filter (not . hasConstraint) instances

89+ in vsep (if null instances' then [text "<no instances>"]

90+ else map dumpInstance instances'))

91+ where

92+ params' = zip params (repeat False)

93+

94+ dumpInstance :: PTerm -> Doc OutputAnnotation

95+ dumpInstance = pprintPTerm imp params' []

96+

97+ hasConstraint (PPi (Constraint _ _) _ _ _) = True

98+ hasConstraint (PPi _ _ _ pt) = hasConstraint pt

99+ hasConstraint _ = False

79100

80101getDocs :: Name -> Idris Docs

81102getDocs n

@@ -96,11 +117,14 @@ docData n ti

96117docClass :: Name -> ClassInfo -> Idris Docs

97118docClass n ci

98119 = do i <- getIState

120+ ctxt <- getContext

99121 let docstr = case lookupCtxt n (idris_docstrings i) of

100122 [str] -> fst str

101123 _ -> emptyDocstring

124+ params = class_params ci

125+ instances = map (delabTy i) (class_instances ci)

102126 mdocs <- mapM docFun (map fst (class_methods ci))

103− return (ClassDoc n docstr mdocs)

127+ return $ ClassDoc n docstr mdocs params instances

104128

105129docFun :: Name -> Idris FunDoc

106130docFun n

src/Idris/IdrisDoc.hs+9−9

@@ -147,9 +147,9 @@ removeOrphans list =

147147 let children = S.fromList $ concatMap (names . (\(_, d, _) -> d)) list

148148 in filter ((`S.notMember` children) . (\(n, _, _) -> n)) list

149149

150− where names (Just (DataDoc _ fds)) = map (\(FD n _ _ _ _) -> n) fds

151− names (Just (ClassDoc _ _ fds)) = map (\(FD n _ _ _ _) -> n) fds

152− names _ = []

150+ where names (Just (DataDoc _ fds)) = map (\(FD n _ _ _ _) -> n) fds

151+ names (Just (ClassDoc _ _ fds _ _)) = map (\(FD n _ _ _ _) -> n) fds

152+ names _ = []

153153

154154-- | Whether a Name names something which should be documented

155155filterName :: Name -- ^ Name to check

@@ -187,11 +187,11 @@ referredNss (n, Just d, _) =

187187 names = concatMap (extractPTermNames) ts

188188 in S.map getNs $ S.fromList names

189189

190− where getFunDocs (FunDoc f) = [f]

191− getFunDocs (DataDoc f fs) = f:fs

192− getFunDocs (ClassDoc _ _ fs) = fs

193− types (FD _ _ args t _) = t:(map second args)

194− second (_, x, _, _) = x

190+ where getFunDocs (FunDoc f) = [f]

191+ getFunDocs (DataDoc f fs) = f:fs

192+ getFunDocs (ClassDoc _ _ fs _ _) = fs

193+ types (FD _ _ args t _) = t:(map second args)

194+ second (_, x, _, _) = x

195195

196196

197197-- | Returns an NsDict of containing all known namespaces and their contents

@@ -537,7 +537,7 @@ createOtherDoc :: IState -- ^ Needed to determine the types of names

537537 -> H.Html -- ^ Resulting HTML

538538createOtherDoc ist (FunDoc fd) = createFunDoc ist fd

539539

540−createOtherDoc ist (ClassDoc n docstring fds) = do

540+createOtherDoc ist (ClassDoc n docstring fds _ _) = do

541541 H.dt ! (A.id $ toValue $ show n) $ do

542542 H.span ! class_ "word" $ do "class"; nbsp

543543 H.span ! class_ "name type"