git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/src/Idris/Docs.hs
205 lines 8.9 kB history raw
1{-# LANGUAGE PatternGuards #-}
2module Idris.Docs (pprintDocs, getDocs, pprintConstDocs, FunDoc(..), Docs (..)) where
4import Idris.AbsSyntax
5import Idris.AbsSyntaxTree
6import Idris.Delaborate
7import Idris.Core.TT
8import Idris.Core.Evaluate
9import Idris.Docstrings (Docstring, emptyDocstring, noDocs, nullDocstring, renderDocstring)
11import Util.Pretty
13import Data.Maybe
14import Data.List
15import qualified Data.Text as T
17-- TODO: Only include names with public/abstract accessibility
18--
19-- Issue #1573 on the Issue tracker.
20-- https://github.com/idris-lang/Idris-dev/issues/1573
21data FunDoc = FD Name (Docstring (Maybe Term))
22 [(Name, PTerm, Plicity, Maybe (Docstring (Maybe Term)))] -- args: name, ty, implicit, docs
23 PTerm -- function type
24 (Maybe Fixity)
25 deriving Show
27data Docs = FunDoc FunDoc
28 | DataDoc FunDoc -- type constructor docs
29 [FunDoc] -- data constructor docs
30 | ClassDoc Name (Docstring (Maybe Term))-- class docs
31 [FunDoc] -- method docs
32 [(Name, Maybe (Docstring (Maybe Term)))] -- parameters and their docstrings
33 [PTerm] -- instances
34 [PTerm] -- superclasses
35 deriving Show
37showDoc ist d | nullDocstring d = empty
38 | otherwise = text " -- " <> renderDocstring (pprintDelab ist) (normaliseAll (tt_ctxt ist) []) d
40pprintFD :: IState -> FunDoc -> Doc OutputAnnotation
41pprintFD ist (FD n doc args ty f)
42 = nest 4 (prettyName True (ppopt_impl ppo) [] n <+> colon <+>
43 pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args
44 , not (T.isPrefixOf (T.pack "__") n') ] infixes ty <$>
45 renderDocstring (pprintDelab ist) (normaliseAll (tt_ctxt ist) []) doc <$>
46 maybe empty (\f -> text (show f) <> line) f <>
47 let argshow = showArgs args [] in
48 if not (null argshow)
49 then nest 4 $ text "Arguments:" <$> vsep argshow
50 else empty)
52 where ppo = ppOptionIst ist
53 infixes = idris_infixes ist
54 showArgs ((n, ty, Exp {}, Just d):args) bnd
55 = bindingOf n False <+> colon <+>
56 pprintPTerm ppo bnd [] infixes ty <>
57 showDoc ist d <> line
58 :
59 showArgs args ((n, False):bnd)
60 showArgs ((n, ty, Constraint {}, Just d):args) bnd
61 = text "Class constraint" <+>
62 pprintPTerm ppo bnd [] infixes ty <> showDoc ist d <> line
63 :
64 showArgs args ((n, True):bnd)
65 showArgs ((n, ty, Imp {}, Just d):args) bnd
66 = text "(implicit)" <+>
67 bindingOf n True <+> colon <+>
68 pprintPTerm ppo bnd [] infixes ty <>
69 showDoc ist d <> line
70 :
71 showArgs args ((n, True):bnd)
72 showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)
73 showArgs [] _ = []
76pprintDocs :: IState -> Docs -> Doc OutputAnnotation
77pprintDocs ist (FunDoc d) = pprintFD ist d
78pprintDocs ist (DataDoc t args)
79 = text "Data type" <+> pprintFD ist t <$>
80 if null args then text "No constructors."
81 else nest 4 (text "Constructors:" <> line <>
82 vsep (map (pprintFD ist) args))
83pprintDocs ist (ClassDoc n doc meths params instances superclasses)
84 = nest 4 (text "Type class" <+> prettyName True (ppopt_impl ppo) [] n <>
85 if nullDocstring doc
86 then empty
87 else line <> renderDocstring (pprintDelab ist) (normaliseAll (tt_ctxt ist) []) doc)
88 <> line <$>
89 nest 4 (text "Parameters:" <$> prettyParameters)
90 <> line <$>
91 nest 4 (text "Methods:" <$>
92 vsep (map (pprintFD ist) meths))
93 <$>
94 nest 4 (text "Instances:" <$>
95 vsep (if null instances' then [text "<no instances>"]
96 else map dumpInstance instances'))
97 <>
98 (if null subclasses then empty
99 else line <$> nest 4 (text "Subclasses:" <$>
100 vsep (map (dumpInstance . prettifySubclasses) subclasses)))
101 <>
102 (if null superclasses then empty
103 else line <$> nest 4 (text "Default superclass instances:" <$>
104 vsep (map dumpInstance superclasses)))
105 where
106 params' = zip pNames (repeat False)
108 pNames = map fst params
110 ppo = ppOptionIst ist
111 infixes = idris_infixes ist
113 dumpInstance :: PTerm -> Doc OutputAnnotation
114 dumpInstance = pprintPTerm ppo params' [] infixes
116 prettifySubclasses (PPi (Constraint _ _) _ tm _) = prettifySubclasses tm
117 prettifySubclasses (PPi plcity nm t1 t2) = PPi plcity (safeHead nm pNames) (prettifySubclasses t1) (prettifySubclasses t2)
118 prettifySubclasses (PApp fc ref args) = PApp fc ref $ updateArgs pNames args
119 prettifySubclasses tm = tm
121 safeHead _ (y:_) = y
122 safeHead x [] = x
124 updateArgs (p:ps) ((PExp prty opts _ ref):as) = (PExp prty opts p (updateRef p ref)) : updateArgs ps as
125 updateArgs ps (a:as) = a : updateArgs ps as
126 updateArgs _ _ = []
128 updateRef nm (PRef fc _) = PRef fc nm
129 updateRef _ pt = pt
131 isSubclass (PPi (Constraint _ _) _ (PApp _ _ args) (PApp _ (PRef _ nm) args')) = nm == n && map getTm args == map getTm args'
132 isSubclass (PPi _ _ _ pt) = isSubclass pt
133 isSubclass _ = False
135 (subclasses, instances') = partition isSubclass instances
137 prettyParameters = if any (isJust . snd) params
138 then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params)
139 else hsep (punctuate comma (map (prettyName True False params' . fst) params))
141getDocs :: Name -> Idris Docs
142getDocs n
143 = do i <- getIState
144 case lookupCtxt n (idris_classes i) of
145 [ci] -> docClass n ci
146 _ -> case lookupCtxt n (idris_datatypes i) of
147 [ti] -> docData n ti
148 _ -> do fd <- docFun n
149 return (FunDoc fd)
151docData :: Name -> TypeInfo -> Idris Docs
152docData n ti
153 = do tdoc <- docFun n
154 cdocs <- mapM docFun (con_names ti)
155 return (DataDoc tdoc cdocs)
157docClass :: Name -> ClassInfo -> Idris Docs
158docClass n ci
159 = do i <- getIState
160 let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i
161 docstr = maybe emptyDocstring fst docStrings
162 params = map (\pn -> (pn, docStrings >>= (lookup pn . snd))) (class_params ci)
163 instances = map (delabTy i) (class_instances ci)
164 superclasses = catMaybes $ map getDInst (class_default_superclasses ci)
165 mdocs <- mapM (docFun . fst) (class_methods ci)
166 return $ ClassDoc n docstr mdocs params instances superclasses
167 where
168 getDInst (PInstance _ _ _ _ _ t _ _) = Just t
169 getDInst _ = Nothing
171docFun :: Name -> Idris FunDoc
172docFun n
173 = do i <- getIState
174 let (docstr, argDocs) = case lookupCtxt n (idris_docstrings i) of
175 [d] -> d
176 _ -> noDocs
177 let ty = delabTy i n
178 let args = getPArgNames ty argDocs
179 let infixes = idris_infixes i
180 let fixdecls = filter (\(Fix _ x) -> x == funName n) infixes
181 let f = case fixdecls of
182 [] -> Nothing
183 (Fix x _:_) -> Just x
185 return (FD n docstr args ty f)
186 where funName :: Name -> String
187 funName (UN n) = str n
188 funName (NS n _) = funName n
190getPArgNames :: PTerm -> [(Name, Docstring (Maybe Term))] -> [(Name, PTerm, Plicity, Maybe (Docstring (Maybe Term)))]
191getPArgNames (PPi plicity name ty body) ds =
192 (name, ty, plicity, lookup name ds) : getPArgNames body ds
193getPArgNames _ _ = []
195pprintConstDocs :: IState -> Const -> String -> Doc OutputAnnotation
196pprintConstDocs ist c str = text "Primitive" <+> text (if constIsType c then "type" else "value") <+>
197 pprintPTerm (ppOptionIst ist) [] [] [] (PConstant c) <+> colon <+>
198 pprintPTerm (ppOptionIst ist) [] [] [] (t c) <>
199 nest 4 (line <> text str)
201 where t (Fl _) = PConstant $ AType ATFloat
202 t (BI _) = PConstant $ AType (ATInt ITBig)
203 t (Str _) = PConstant StrType
204 t (Ch c) = PConstant $ AType (ATInt ITChar)
205 t _ = PType