git.iko.soy/Idris-dev
on 54e4e41 help sign in
Idris-dev/src/Idris/Docs.hs
339 lines 15 kB history raw
1{-# LANGUAGE DeriveFunctor, PatternGuards, MultiWayIf #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3module Idris.Docs (pprintDocs, getDocs, pprintConstDocs, pprintTypeDoc, FunDoc, FunDoc'(..), Docs, Docs'(..)) where
5import Idris.AbsSyntax
6import Idris.AbsSyntaxTree
7import Idris.Delaborate
8import Idris.Core.TT
9import Idris.Core.Evaluate
10import Idris.Docstrings (Docstring, emptyDocstring, noDocs, nullDocstring, renderDocstring, DocTerm, renderDocTerm, overview)
12import Util.Pretty
14import Prelude hiding ((<$>))
16import Control.Arrow (first)
18import Data.Maybe
19import Data.List
20import qualified Data.Text as T
22-- TODO: Only include names with public/abstract accessibility
23--
24-- Issue #1573 on the Issue tracker.
25-- https://github.com/idris-lang/Idris-dev/issues/1573
26data FunDoc' d = FD Name d
27 [(Name, PTerm, Plicity, Maybe d)] -- args: name, ty, implicit, docs
28 PTerm -- function type
29 (Maybe Fixity)
30 deriving Functor
32type FunDoc = FunDoc' (Docstring DocTerm)
34data Docs' d = FunDoc (FunDoc' d)
35 | DataDoc (FunDoc' d) -- type constructor docs
36 [FunDoc' d] -- data constructor docs
37 | ClassDoc Name d -- class docs
38 [FunDoc' d] -- method docs
39 [(Name, Maybe d)] -- parameters and their docstrings
40 [(Maybe Name, PTerm, (d, [(Name, d)]))] -- instances: name for named instances, the constraint term, the docs
41 [PTerm] -- subclasses
42 [PTerm] -- superclasses
43 (Maybe (FunDoc' d)) -- explicit constructor
44 | NamedInstanceDoc Name (FunDoc' d) -- name is class
45 | ModDoc [String] -- Module name
46 d
47 deriving Functor
49type Docs = Docs' (Docstring DocTerm)
51showDoc ist d
52 | nullDocstring d = empty
53 | otherwise = text " -- " <>
54 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) d
56pprintFD :: IState -> Bool -> Bool -> FunDoc -> Doc OutputAnnotation
57pprintFD ist totalityFlag nsFlag (FD n doc args ty f)
58 = nest 4 (prettyName True nsFlag [] n <+> colon <+>
59 pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args
60 , not (T.isPrefixOf (T.pack "__") n') ] infixes ty <$>
61 -- show doc
62 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc <$>
63 -- show fixity
64 maybe empty (\f -> text (show f) <> line) f <>
65 -- show arguments doc
66 let argshow = showArgs args [] in
67 (if not (null argshow)
68 then nest 4 $ text "Arguments:" <$> vsep argshow
69 else empty) <>
70 -- show totality status
71 let totality = getTotality in
72 (if totalityFlag && not (null totality) then
73 line <> (vsep . map (\t -> text "The function is" <+> t) $ totality)
74 else
75 empty))
77 where ppo = ppOptionIst ist
78 infixes = idris_infixes ist
79 showArgs ((n, ty, Exp {}, Just d):args) bnd
80 = bindingOf n False <+> colon <+>
81 pprintPTerm ppo bnd [] infixes ty <>
82 showDoc ist d <> line
83 :
84 showArgs args ((n, False):bnd)
85 showArgs ((n, ty, Constraint {}, Just d):args) bnd
86 = text "Class constraint" <+>
87 pprintPTerm ppo bnd [] infixes ty <> showDoc ist d <> line
88 :
89 showArgs args ((n, True):bnd)
90 showArgs ((n, ty, Imp {}, Just d):args) bnd
91 = text "(implicit)" <+>
92 bindingOf n True <+> colon <+>
93 pprintPTerm ppo bnd [] infixes ty <>
94 showDoc ist d <> line
95 :
96 showArgs args ((n, True):bnd)
97 showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)
98 showArgs [] _ = []
99 getTotality = map (text . show) $ lookupTotal n (tt_ctxt ist)
101pprintFDWithTotality :: IState -> Bool -> FunDoc -> Doc OutputAnnotation
102pprintFDWithTotality ist = pprintFD ist True
104pprintFDWithoutTotality :: IState -> Bool -> FunDoc -> Doc OutputAnnotation
105pprintFDWithoutTotality ist = pprintFD ist False
107pprintDocs :: IState -> Docs -> Doc OutputAnnotation
108pprintDocs ist (FunDoc d) = pprintFDWithTotality ist True d
109pprintDocs ist (DataDoc t args)
110 = text "Data type" <+> pprintFDWithoutTotality ist True t <$>
111 if null args then text "No constructors."
112 else nest 4 (text "Constructors:" <> line <>
113 vsep (map (pprintFDWithoutTotality ist False) args))
114pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ctor)
115 = nest 4 (text "Type class" <+> prettyName True (ppopt_impl ppo) [] n <>
116 if nullDocstring doc
117 then empty
118 else line <> renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc)
119 <> line <$>
120 nest 4 (text "Parameters:" <$> prettyParameters)
121 <> line <$>
122 nest 4 (text "Methods:" <$>
123 vsep (map (pprintFDWithTotality ist False) meths))
124 <$>
125 maybe empty
126 ((<> line) . nest 4 .
127 (text "Instance constructor:" <$>) .
128 pprintFDWithoutTotality ist False)
129 ctor
130 <>
131 nest 4 (text "Instances:" <$>
132 vsep (if null instances then [text "<no instances>"]
133 else map pprintInstance normalInstances))
134 <>
135 (if null namedInstances then empty
136 else line <$> nest 4 (text "Named instances:" <$>
137 vsep (map pprintInstance namedInstances)))
138 <>
139 (if null subclasses then empty
140 else line <$> nest 4 (text "Subclasses:" <$>
141 vsep (map (dumpInstance . prettifySubclasses) subclasses)))
142 <>
143 (if null superclasses then empty
144 else line <$> nest 4 (text "Default superclass instances:" <$>
145 vsep (map dumpInstance superclasses)))
146 where
147 params' = zip pNames (repeat False)
149 (normalInstances, namedInstances) = partition (\(n, _, _) -> not $ isJust n)
150 instances
152 pNames = map fst params
154 ppo = ppOptionIst ist
155 infixes = idris_infixes ist
157 pprintInstance (mname, term, (doc, argDocs)) =
158 nest 4 (iname mname <> dumpInstance term <>
159 (if nullDocstring doc
160 then empty
161 else line <>
162 renderDocstring
163 (renderDocTerm
164 (pprintDelab ist)
165 (normaliseAll (tt_ctxt ist) []))
166 doc) <>
167 if null argDocs
168 then empty
169 else line <> vsep (map (prettyInstanceParam (map fst argDocs)) argDocs))
172 iname Nothing = empty
173 iname (Just n) = annName n <+> colon <> space
175 prettyInstanceParam params (name, doc) =
176 if nullDocstring doc
177 then empty
178 else prettyName True False (zip params (repeat False)) name <+>
179 showDoc ist doc
181-- if any (isJust . snd) params
182-- then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params)
183-- else hsep (punctuate comma (map (prettyName True False params' . fst) params))
185 dumpInstance :: PTerm -> Doc OutputAnnotation
186 dumpInstance = pprintPTerm ppo params' [] infixes
188 prettifySubclasses (PPi (Constraint _ _) _ _ tm _) = prettifySubclasses tm
189 prettifySubclasses (PPi plcity nm fc t1 t2) = PPi plcity (safeHead nm pNames) NoFC (prettifySubclasses t1) (prettifySubclasses t2)
190 prettifySubclasses (PApp fc ref args) = PApp fc ref $ updateArgs pNames args
191 prettifySubclasses tm = tm
193 safeHead _ (y:_) = y
194 safeHead x [] = x
196 updateArgs (p:ps) ((PExp prty opts _ ref):as) = (PExp prty opts p (updateRef p ref)) : updateArgs ps as
197 updateArgs ps (a:as) = a : updateArgs ps as
198 updateArgs _ _ = []
200 updateRef nm (PRef fc _ _) = PRef fc [] nm
201 updateRef _ pt = pt
203 isSubclass (PPi (Constraint _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args')) = nm == n && map getTm args == map getTm args'
204 isSubclass (PPi _ _ _ _ pt) = isSubclass pt
205 isSubclass _ = False
207 prettyParameters =
208 if any (isJust . snd) params
209 then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params)
210 else hsep (punctuate comma (map (prettyName True False params' . fst) params))
212pprintDocs ist (NamedInstanceDoc _cls doc)
213 = nest 4 (text "Named instance:" <$> pprintFDWithoutTotality ist True doc)
215pprintDocs ist (ModDoc mod docs)
216 = nest 4 $ text "Module" <+> text (concat (intersperse "." mod)) <> colon <$>
217 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) docs
219-- | Determine a truncation function depending how much docs the user
220-- wants to see
221howMuch FullDocs = id
222howMuch OverviewDocs = overview
224-- | Given a fully-qualified, disambiguated name, construct the
225-- documentation object for it
226getDocs :: Name -> HowMuchDocs -> Idris Docs
227getDocs n@(NS n' ns) w | n' == modDocName
228 = do i <- getIState
229 case lookupCtxtExact n (idris_moduledocs i) of
230 Just doc -> return . ModDoc (reverse (map T.unpack ns)) $ howMuch w doc
231 Nothing -> fail $ "Module docs for " ++ show (reverse (map T.unpack ns)) ++
232 " do not exist! This shouldn't have happened and is a bug."
233getDocs n w
234 = do i <- getIState
235 docs <- if | Just ci <- lookupCtxtExact n (idris_classes i)
236 -> docClass n ci
237 | Just ti <- lookupCtxtExact n (idris_datatypes i)
238 -> docData n ti
239 | Just class_ <- classNameForInst i n
240 -> do fd <- docFun n
241 return $ NamedInstanceDoc class_ fd
242 | otherwise
243 -> do fd <- docFun n
244 return (FunDoc fd)
245 return $ fmap (howMuch w) docs
246 where classNameForInst :: IState -> Name -> Maybe Name
247 classNameForInst ist n =
248 listToMaybe [ cn
249 | (cn, ci) <- toAlist (idris_classes ist)
250 , n `elem` map fst (class_instances ci)
251 ]
253docData :: Name -> TypeInfo -> Idris Docs
254docData n ti
255 = do tdoc <- docFun n
256 cdocs <- mapM docFun (con_names ti)
257 return (DataDoc tdoc cdocs)
259docClass :: Name -> ClassInfo -> Idris Docs
260docClass n ci
261 = do i <- getIState
262 let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i
263 docstr = maybe emptyDocstring fst docStrings
264 params = map (\pn -> (pn, docStrings >>= (lookup pn . snd)))
265 (class_params ci)
266 docsForInstance inst = fromMaybe (emptyDocstring, []) .
267 flip lookupCtxtExact (idris_docstrings i) $
268 inst
269 instances = map (\inst -> (namedInst inst,
270 delabTy i inst,
271 docsForInstance inst))
272 (nub (map fst (class_instances ci)))
273 (subclasses, instances') = partition (isSubclass . (\(_,tm,_) -> tm)) instances
274 superclasses = catMaybes $ map getDInst (class_default_superclasses ci)
275 mdocs <- mapM (docFun . fst) (class_methods ci)
276 let ctorN = instanceCtorName ci
277 ctorDocs <- case basename ctorN of
278 SN _ -> return Nothing
279 _ -> fmap Just $ docFun ctorN
280 return $ ClassDoc
281 n docstr mdocs params
282 instances' (map (\(_,tm,_) -> tm) subclasses) superclasses
283 ctorDocs
284 where
285 namedInst (NS n ns) = fmap (flip NS ns) (namedInst n)
286 namedInst n@(UN _) = Just n
287 namedInst _ = Nothing
289 getDInst (PInstance _ _ _ _ _ _ _ _ t _ _) = Just t
290 getDInst _ = Nothing
292 isSubclass (PPi (Constraint _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args'))
293 = nm == n && map getTm args == map getTm args'
294 isSubclass (PPi _ _ _ _ pt)
295 = isSubclass pt
296 isSubclass _
297 = False
299docFun :: Name -> Idris FunDoc
300docFun n
301 = do i <- getIState
302 let (docstr, argDocs) = case lookupCtxt n (idris_docstrings i) of
303 [d] -> d
304 _ -> noDocs
305 let ty = delabTy i n
306 let args = getPArgNames ty argDocs
307 let infixes = idris_infixes i
308 let fixdecls = filter (\(Fix _ x) -> x == funName n) infixes
309 let f = case fixdecls of
310 [] -> Nothing
311 (Fix x _:_) -> Just x
313 return (FD n docstr args ty f)
314 where funName :: Name -> String
315 funName (UN n) = str n
316 funName (NS n _) = funName n
317 funName n = show n
319getPArgNames :: PTerm -> [(Name, Docstring DocTerm)] -> [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
320getPArgNames (PPi plicity name _ ty body) ds =
321 (name, ty, plicity, lookup name ds) : getPArgNames body ds
322getPArgNames _ _ = []
324pprintConstDocs :: IState -> Const -> String -> Doc OutputAnnotation
325pprintConstDocs ist c str = text "Primitive" <+> text (if constIsType c then "type" else "value") <+>
326 pprintPTerm (ppOptionIst ist) [] [] [] (PConstant NoFC c) <+> colon <+>
327 pprintPTerm (ppOptionIst ist) [] [] [] (t c) <>
328 nest 4 (line <> text str)
330 where t (Fl _) = PConstant NoFC $ AType ATFloat
331 t (BI _) = PConstant NoFC $ AType (ATInt ITBig)
332 t (Str _) = PConstant NoFC StrType
333 t (Ch c) = PConstant NoFC $ AType (ATInt ITChar)
334 t _ = PType NoFC
337pprintTypeDoc :: IState -> Doc OutputAnnotation
338pprintTypeDoc ist = prettyIst ist (PType emptyFC) <+> colon <+> type1Doc <+>
339 nest 4 (line <> text typeDescription)