git.iko.soy/Idris-dev
on 13ebfcf help sign in
Idris-dev/src/Idris/Docs.hs
269 lines 12 kB history raw
1{-# LANGUAGE DeriveFunctor, PatternGuards #-}
2module Idris.Docs (pprintDocs, getDocs, pprintConstDocs, FunDoc, FunDoc'(..), Docs, 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, DocTerm, renderDocTerm, overview)
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' d = FD Name d
22 [(Name, PTerm, Plicity, Maybe d)] -- args: name, ty, implicit, docs
23 PTerm -- function type
24 (Maybe Fixity)
25 deriving Functor
27type FunDoc = FunDoc' (Docstring DocTerm)
29data Docs' d = FunDoc (FunDoc' d)
30 | DataDoc (FunDoc' d) -- type constructor docs
31 [FunDoc' d] -- data constructor docs
32 | ClassDoc Name d -- class docs
33 [FunDoc' d] -- method docs
34 [(Name, Maybe d)] -- parameters and their docstrings
35 [(PTerm, (d, [(Name, d)]))] -- instances
36 [PTerm] -- subclasses
37 [PTerm] -- superclasses
38 | ModDoc [String] -- Module name
39 d
40 deriving Functor
42type Docs = Docs' (Docstring DocTerm)
44showDoc ist d
45 | nullDocstring d = empty
46 | otherwise = text " -- " <>
47 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) d
49pprintFD :: IState -> FunDoc -> Doc OutputAnnotation
50pprintFD ist (FD n doc args ty f)
51 = nest 4 (prettyName True (ppopt_impl ppo) [] n <+> colon <+>
52 pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args
53 , not (T.isPrefixOf (T.pack "__") n') ] infixes ty <$>
54 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc <$>
55 maybe empty (\f -> text (show f) <> line) f <>
56 let argshow = showArgs args [] in
57 if not (null argshow)
58 then nest 4 $ text "Arguments:" <$> vsep argshow
59 else empty)
61 where ppo = ppOptionIst ist
62 infixes = idris_infixes ist
63 showArgs ((n, ty, Exp {}, Just d):args) bnd
64 = bindingOf n False <+> colon <+>
65 pprintPTerm ppo bnd [] infixes ty <>
66 showDoc ist d <> line
67 :
68 showArgs args ((n, False):bnd)
69 showArgs ((n, ty, Constraint {}, Just d):args) bnd
70 = text "Class constraint" <+>
71 pprintPTerm ppo bnd [] infixes ty <> showDoc ist d <> line
72 :
73 showArgs args ((n, True):bnd)
74 showArgs ((n, ty, Imp {}, Just d):args) bnd
75 = text "(implicit)" <+>
76 bindingOf n True <+> colon <+>
77 pprintPTerm ppo bnd [] infixes ty <>
78 showDoc ist d <> line
79 :
80 showArgs args ((n, True):bnd)
81 showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)
82 showArgs [] _ = []
85pprintDocs :: IState -> Docs -> Doc OutputAnnotation
86pprintDocs ist (FunDoc d) = pprintFD ist d
87pprintDocs ist (DataDoc t args)
88 = text "Data type" <+> pprintFD ist t <$>
89 if null args then text "No constructors."
90 else nest 4 (text "Constructors:" <> line <>
91 vsep (map (pprintFD ist) args))
92pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses)
93 = nest 4 (text "Type class" <+> prettyName True (ppopt_impl ppo) [] n <>
94 if nullDocstring doc
95 then empty
96 else line <> renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc)
97 <> line <$>
98 nest 4 (text "Parameters:" <$> prettyParameters)
99 <> line <$>
100 nest 4 (text "Methods:" <$>
101 vsep (map (pprintFD ist) meths))
102 <$>
103 nest 4 (text "Instances:" <$>
104 vsep (if null instances then [text "<no instances>"]
105 else map pprintInstance instances))
106 <>
107 (if null subclasses then empty
108 else line <$> nest 4 (text "Subclasses:" <$>
109 vsep (map (dumpInstance . prettifySubclasses) subclasses)))
110 <>
111 (if null superclasses then empty
112 else line <$> nest 4 (text "Default superclass instances:" <$>
113 vsep (map dumpInstance superclasses)))
114 where
115 params' = zip pNames (repeat False)
117 pNames = map fst params
119 ppo = ppOptionIst ist
120 infixes = idris_infixes ist
122 pprintInstance (term, (doc, argDocs)) =
123 nest 4 (dumpInstance term <>
124 (if nullDocstring doc
125 then empty
126 else line <>
127 renderDocstring
128 (renderDocTerm
129 (pprintDelab ist)
130 (normaliseAll (tt_ctxt ist) []))
131 doc) <>
132 if null argDocs
133 then empty
134 else line <> vsep (map (prettyInstanceParam (map fst argDocs)) argDocs))
136 prettyInstanceParam params (name, doc) =
137 if nullDocstring doc
138 then empty
139 else prettyName True False (zip params (repeat False)) name <+>
140 showDoc ist doc
142-- if any (isJust . snd) params
143-- then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params)
144-- else hsep (punctuate comma (map (prettyName True False params' . fst) params))
146 dumpInstance :: PTerm -> Doc OutputAnnotation
147 dumpInstance = pprintPTerm ppo params' [] infixes
149 prettifySubclasses (PPi (Constraint _ _) _ tm _) = prettifySubclasses tm
150 prettifySubclasses (PPi plcity nm t1 t2) = PPi plcity (safeHead nm pNames) (prettifySubclasses t1) (prettifySubclasses t2)
151 prettifySubclasses (PApp fc ref args) = PApp fc ref $ updateArgs pNames args
152 prettifySubclasses tm = tm
154 safeHead _ (y:_) = y
155 safeHead x [] = x
157 updateArgs (p:ps) ((PExp prty opts _ ref):as) = (PExp prty opts p (updateRef p ref)) : updateArgs ps as
158 updateArgs ps (a:as) = a : updateArgs ps as
159 updateArgs _ _ = []
161 updateRef nm (PRef fc _) = PRef fc nm
162 updateRef _ pt = pt
164 isSubclass (PPi (Constraint _ _) _ (PApp _ _ args) (PApp _ (PRef _ nm) args')) = nm == n && map getTm args == map getTm args'
165 isSubclass (PPi _ _ _ pt) = isSubclass pt
166 isSubclass _ = False
168 prettyParameters =
169 if any (isJust . snd) params
170 then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params)
171 else hsep (punctuate comma (map (prettyName True False params' . fst) params))
173pprintDocs ist (ModDoc mod docs)
174 = nest 4 $ text "Module" <+> text (concat (intersperse "." mod)) <> colon <$>
175 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) docs
177-- | Determine a truncation function depending how much docs the user
178-- wants to see
179howMuch FullDocs = id
180howMuch OverviewDocs = overview
182-- | Given a fully-qualified, disambiguated name, construct the
183-- documentation object for it
184getDocs :: Name -> HowMuchDocs -> Idris Docs
185getDocs n@(NS n' ns) w | n' == modDocName
186 = do i <- getIState
187 case lookupCtxtExact n (idris_moduledocs i) of
188 Just doc -> return . ModDoc (reverse (map T.unpack ns)) $ howMuch w doc
189 Nothing -> fail $ "Module docs for " ++ show (reverse (map T.unpack ns)) ++
190 " do not exist! This shouldn't have happened and is a bug."
191getDocs n w
192 = do i <- getIState
193 docs <- case lookupCtxt n (idris_classes i) of
194 [ci] -> docClass n ci
195 _ -> case lookupCtxt n (idris_datatypes i) of
196 [ti] -> docData n ti
197 _ -> do fd <- docFun n
198 return (FunDoc fd)
199 return $ fmap (howMuch w) docs
201docData :: Name -> TypeInfo -> Idris Docs
202docData n ti
203 = do tdoc <- docFun n
204 cdocs <- mapM docFun (con_names ti)
205 return (DataDoc tdoc cdocs)
207docClass :: Name -> ClassInfo -> Idris Docs
208docClass n ci
209 = do i <- getIState
210 let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i
211 docstr = maybe emptyDocstring fst docStrings
212 params = map (\pn -> (pn, docStrings >>= (lookup pn . snd))) (class_params ci)
213 instanceDocs = map (fromMaybe (emptyDocstring, []) .
214 listToMaybe .
215 flip lookupCtxt (idris_docstrings i))
216 (class_instances ci)
217 instances = zip (map (delabTy i) (class_instances ci)) instanceDocs
218 (subclasses, instances') = partition (isSubclass . fst) instances
219 superclasses = catMaybes $ map getDInst (class_default_superclasses ci)
220 mdocs <- mapM (docFun . fst) (class_methods ci)
221 return $ ClassDoc
222 n docstr mdocs params
223 instances' (map fst subclasses) superclasses
224 where
225 getDInst (PInstance _ _ _ _ _ _ _ t _ _) = Just t
226 getDInst _ = Nothing
228 isSubclass (PPi (Constraint _ _) _ (PApp _ _ args) (PApp _ (PRef _ nm) args'))
229 = nm == n && map getTm args == map getTm args'
230 isSubclass (PPi _ _ _ pt)
231 = isSubclass pt
232 isSubclass _
233 = False
235docFun :: Name -> Idris FunDoc
236docFun n
237 = do i <- getIState
238 let (docstr, argDocs) = case lookupCtxt n (idris_docstrings i) of
239 [d] -> d
240 _ -> noDocs
241 let ty = delabTy i n
242 let args = getPArgNames ty argDocs
243 let infixes = idris_infixes i
244 let fixdecls = filter (\(Fix _ x) -> x == funName n) infixes
245 let f = case fixdecls of
246 [] -> Nothing
247 (Fix x _:_) -> Just x
249 return (FD n docstr args ty f)
250 where funName :: Name -> String
251 funName (UN n) = str n
252 funName (NS n _) = funName n
254getPArgNames :: PTerm -> [(Name, Docstring DocTerm)] -> [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
255getPArgNames (PPi plicity name ty body) ds =
256 (name, ty, plicity, lookup name ds) : getPArgNames body ds
257getPArgNames _ _ = []
259pprintConstDocs :: IState -> Const -> String -> Doc OutputAnnotation
260pprintConstDocs ist c str = text "Primitive" <+> text (if constIsType c then "type" else "value") <+>
261 pprintPTerm (ppOptionIst ist) [] [] [] (PConstant c) <+> colon <+>
262 pprintPTerm (ppOptionIst ist) [] [] [] (t c) <>
263 nest 4 (line <> text str)
265 where t (Fl _) = PConstant $ AType ATFloat
266 t (BI _) = PConstant $ AType (ATInt ITBig)
267 t (Str _) = PConstant StrType
268 t (Ch c) = PConstant $ AType (ATInt ITChar)
269 t _ = PType