git.iko.soy/Idris-dev
on master help sign in
Properly pretty-print typeclasses for REPL command ':doc'
71bdbbbPaul Koerbitz
src/Idris/Docs.hs+29−5
compare with master
unifiedsplit
@@ -27,6 +27,8 @@ data Docs = FunDoc FunDoc
27 [FunDoc] -- data constructor docs
27 [FunDoc] -- data constructor docs
28 | ClassDoc Name Docstring -- class docs
28 | ClassDoc Name Docstring -- class docs
29 [FunDoc] -- method docs
29 [FunDoc] -- method docs
30+ [Name] -- parameter docs
31+ [PTerm] -- instances
30 deriving Show
32 deriving Show
31
33
32showDoc d | nullDocstring d = empty
34showDoc d | nullDocstring d = empty
@@ -66,16 +68,35 @@ pprintFD imp (FD n doc args ty f)
66 showArgs [] _ = []
68 showArgs [] _ = []
67
69
68
70
69−
71+pprintDocs :: Bool -> Docs -> Doc OutputAnnotation
70pprintDocs imp (FunDoc d) = pprintFD imp d
72pprintDocs imp (FunDoc d) = pprintFD imp d
71pprintDocs imp (DataDoc t args)
73pprintDocs imp (DataDoc t args)
72 = text "Data type" <+> pprintFD imp t <$>
74 = text "Data type" <+> pprintFD imp t <$>
73 nest 4 (text "Constructors:" <> line <>
75 nest 4 (text "Constructors:" <> line <>
74 vsep (map (pprintFD imp) args))
76 vsep (map (pprintFD imp) args))
75−pprintDocs imp (ClassDoc n doc meths)
77+pprintDocs imp (ClassDoc n doc meths params instances)
76− = text "Type class" <+> prettyName imp [] n <$> -- parameters?
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 <$>
77 nest 4 (text "Methods:" <$>
84 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
79
100
80getDocs :: Name -> Idris Docs
101getDocs :: Name -> Idris Docs
81getDocs n
102getDocs n
@@ -96,11 +117,14 @@ docData n ti
96docClass :: Name -> ClassInfo -> Idris Docs
117docClass :: Name -> ClassInfo -> Idris Docs
97docClass n ci
118docClass n ci
98 = do i <- getIState
119 = do i <- getIState
120+ ctxt <- getContext
99 let docstr = case lookupCtxt n (idris_docstrings i) of
121 let docstr = case lookupCtxt n (idris_docstrings i) of
100 [str] -> fst str
122 [str] -> fst str
101 _ -> emptyDocstring
123 _ -> emptyDocstring
124+ params = class_params ci
125+ instances = map (delabTy i) (class_instances ci)
102 mdocs <- mapM docFun (map fst (class_methods ci))
126 mdocs <- mapM docFun (map fst (class_methods ci))
103− return (ClassDoc n docstr mdocs)
127+ return $ ClassDoc n docstr mdocs params instances
104
128
105docFun :: Name -> Idris FunDoc
129docFun :: Name -> Idris FunDoc
106docFun n
130docFun n
src/Idris/IdrisDoc.hs+9−9
@@ -147,9 +147,9 @@ removeOrphans list =
147 let children = S.fromList $ concatMap (names . (\(_, d, _) -> d)) list
147 let children = S.fromList $ concatMap (names . (\(_, d, _) -> d)) list
148 in filter ((`S.notMember` children) . (\(n, _, _) -> n)) list
148 in filter ((`S.notMember` children) . (\(n, _, _) -> n)) list
149
149
150− where names (Just (DataDoc _ fds)) = map (\(FD n _ _ _ _) -> n) fds
150+ where names (Just (DataDoc _ fds)) = map (\(FD n _ _ _ _) -> n) fds
151− names (Just (ClassDoc _ _ fds)) = map (\(FD n _ _ _ _) -> n) fds
151+ names (Just (ClassDoc _ _ fds _ _)) = map (\(FD n _ _ _ _) -> n) fds
152− names _ = []
152+ names _ = []
153
153
154-- | Whether a Name names something which should be documented
154-- | Whether a Name names something which should be documented
155filterName :: Name -- ^ Name to check
155filterName :: Name -- ^ Name to check
@@ -187,11 +187,11 @@ referredNss (n, Just d, _) =
187 names = concatMap (extractPTermNames) ts
187 names = concatMap (extractPTermNames) ts
188 in S.map getNs $ S.fromList names
188 in S.map getNs $ S.fromList names
189
189
190− where getFunDocs (FunDoc f) = [f]
190+ where getFunDocs (FunDoc f) = [f]
191− getFunDocs (DataDoc f fs) = f:fs
191+ getFunDocs (DataDoc f fs) = f:fs
192− getFunDocs (ClassDoc _ _ fs) = fs
192+ getFunDocs (ClassDoc _ _ fs _ _) = fs
193− types (FD _ _ args t _) = t:(map second args)
193+ types (FD _ _ args t _) = t:(map second args)
194− second (_, x, _, _) = x
194+ second (_, x, _, _) = x
195
195
196
196
197-- | Returns an NsDict of containing all known namespaces and their contents
197-- | Returns an NsDict of containing all known namespaces and their contents
@@ -537,7 +537,7 @@ createOtherDoc :: IState -- ^ Needed to determine the types of names
537 -> H.Html -- ^ Resulting HTML
537 -> H.Html -- ^ Resulting HTML
538createOtherDoc ist (FunDoc fd) = createFunDoc ist fd
538createOtherDoc ist (FunDoc fd) = createFunDoc ist fd
539
539
540−createOtherDoc ist (ClassDoc n docstring fds) = do
540+createOtherDoc ist (ClassDoc n docstring fds _ _) = do
541 H.dt ! (A.id $ toValue $ show n) $ do
541 H.dt ! (A.id $ toValue $ show n) $ do
542 H.span ! class_ "word" $ do "class"; nbsp
542 H.span ! class_ "word" $ do "class"; nbsp
543 H.span ! class_ "name type"
543 H.span ! class_ "name type"