git.iko.soy/Idris-dev
on 385dcbf help sign in
Idris-dev/src/Idris/Docs.hs
422 lines 19 kB history raw
1{-|
2Module : Idris.Docs
3Description : Data structures and utilities to work with Idris Documentation.
4Copyright :
5License : BSD3
6Maintainer : The Idris Community.
7-}
9{-# LANGUAGE DeriveFunctor, MultiWayIf, PatternGuards #-}
10{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
12module Idris.Docs (
13 pprintDocs
14 , getDocs, pprintConstDocs, pprintTypeDoc
15 , FunDoc, FunDoc'(..), Docs, Docs'(..)
16 ) where
18import Idris.AbsSyntax (FixDecl(..), Fixity, IState(..), Idris,
19 InterfaceInfo(..), PArg'(..), PDecl'(..), PPOption(..),
20 PTerm(..), Plicity(..), RecordInfo(..), basename,
21 getIState, modDocName, ppOptionIst, pprintPTerm,
22 prettyIst, prettyName, type1Doc, typeDescription)
23import Idris.Core.Evaluate
24import Idris.Core.TT
25import Idris.Delaborate
26import Idris.Docstrings (DocTerm, Docstring, emptyDocstring, noDocs,
27 nullDocstring, overview, renderDocTerm,
28 renderDocstring)
29import Idris.Options (HowMuchDocs(..))
31import Util.Pretty
33import Prelude hiding ((<$>))
35import Data.List
36import Data.Maybe
37import qualified Data.Text as T
39-- TODO: Only include names with public/export accessibility
40--
41-- Issue #1573 on the Issue tracker.
42-- https://github.com/idris-lang/Idris-dev/issues/1573
43data FunDoc' d = FD Name d
44 [(Name, PTerm, Plicity, Maybe d)] -- args: name, ty, implicit, docs
45 PTerm -- function type
46 (Maybe Fixity)
47 deriving Functor
49type FunDoc = FunDoc' (Docstring DocTerm)
51data Docs' d = FunDoc (FunDoc' d)
52 | DataDoc (FunDoc' d) -- type constructor docs
53 [FunDoc' d] -- data constructor docs
54 | InterfaceDoc Name d -- interface docs
55 [FunDoc' d] -- method docs
56 [(Name, Maybe d)] -- parameters and their docstrings
57 [PTerm] -- parameter constraints
58 [(Maybe Name, PTerm, (d, [(Name, d)]))] -- implementations: name for named implementations, the constraint term, the docs
59 [PTerm] -- sub interfaces
60 [PTerm] -- super interfaces
61 (Maybe (FunDoc' d)) -- explicit constructor
62 | RecordDoc Name d -- record docs
63 (FunDoc' d) -- data constructor docs
64 [FunDoc' d] -- projection docs
65 [(Name, PTerm, Maybe d)] -- parameters with type and doc
66 | NamedImplementationDoc Name (FunDoc' d) -- name is interface
67 | ModDoc [String] -- Module name
68 d
69 deriving Functor
71type Docs = Docs' (Docstring DocTerm)
73showDoc ist d
74 | nullDocstring d = empty
75 | otherwise = text " -- " <>
76 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) d
78pprintFD :: IState -> Bool -> Bool -> FunDoc -> Doc OutputAnnotation
79pprintFD ist totalityFlag nsFlag (FD n doc args ty f) =
80 nest 4 (prettyName True nsFlag [] n
81 <+> colon
82 <+> pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args
83 , not (T.isPrefixOf (T.pack "__") n') ] infixes ty
84 -- show doc
85 <$> renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc
86 -- show fixity
87 <$> maybe empty (\f -> text (show f) <> line) f
88 -- show arguments doc
89 <> let argshow = showArgs args [] in
90 (if not (null argshow)
91 then nest 4 $ text "Arguments:" <$> vsep argshow
92 else empty)
93 -- show totality status
94 <> let totality = getTotality in
95 (if totalityFlag && not (null totality)
96 then line <> (vsep . map (\t -> text "The function is" <+> t) $ totality)
97 else empty))
99 where
100 ppo = ppOptionIst ist
102 infixes = idris_infixes ist
104 -- Recurse over and show the Function's Documented arguments
105 showArgs ((n, ty, Exp {}, Just d):args) bnd = -- Explicitly bound.
106 bindingOf n False
107 <+> colon
108 <+> pprintPTerm ppo bnd [] infixes ty
109 <> showDoc ist d
110 <> line : showArgs args ((n, False):bnd)
111 showArgs ((n, ty, Constraint {}, Just d):args) bnd = -- Interface constraints.
112 text "Interface constraint"
113 <+> pprintPTerm ppo bnd [] infixes ty
114 <> showDoc ist d
115 <> line : showArgs args ((n, True):bnd)
116 showArgs ((n, ty, Imp {}, Just d):args) bnd = -- Implicit arguments.
117 text "(implicit)"
118 <+> bindingOf n True
119 <+> colon
120 <+> pprintPTerm ppo bnd [] infixes ty
121 <> showDoc ist d
122 <> line : showArgs args ((n, True):bnd)
123 showArgs ((n, ty, TacImp{}, Just d):args) bnd = -- Tacit implicits
124 text "(auto implicit)"
125 <+> bindingOf n True
126 <+> colon
127 <+> pprintPTerm ppo bnd [] infixes ty
128 <> showDoc ist d
129 <> line : showArgs args ((n, True):bnd)
130 showArgs ((n, _, _, _):args) bnd = -- Anything else
131 showArgs args ((n, True):bnd)
132 showArgs [] _ = [] -- end of arguments
134 getTotality = map (text . show) $ lookupTotal n (tt_ctxt ist)
136pprintFDWithTotality :: IState -> Bool -> FunDoc -> Doc OutputAnnotation
137pprintFDWithTotality ist = pprintFD ist True
139pprintFDWithoutTotality :: IState -> Bool -> FunDoc -> Doc OutputAnnotation
140pprintFDWithoutTotality ist = pprintFD ist False
142pprintDocs :: IState -> Docs -> Doc OutputAnnotation
143pprintDocs ist (FunDoc d) = pprintFDWithTotality ist True d
144pprintDocs ist (DataDoc t args)
145 = text "Data type" <+> pprintFDWithoutTotality ist True t <$>
146 if null args then text "No constructors."
147 else nest 4 (text "Constructors:" <> line <>
148 vsep (map (pprintFDWithoutTotality ist False) args))
149pprintDocs ist (InterfaceDoc n doc meths params constraints implementations sub_interfaces super_interfaces ctor)
150 = nest 4 (text "Interface" <+> prettyName True (ppopt_impl ppo) [] n <>
151 if nullDocstring doc
152 then empty
153 else line <> renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc)
154 <> line <$>
155 nest 4 (text "Parameters:" <$> prettyParameters)
157 <> (if null constraints
158 then empty
159 else line <$> nest 4 (text "Constraints:" <$> prettyConstraints))
161 <> line <$>
162 nest 4 (text "Methods:" <$>
163 vsep (map (pprintFDWithTotality ist False) meths))
164 <$>
165 maybe empty
166 ((<> line) . nest 4 .
167 (text "Implementation constructor:" <$>) .
168 pprintFDWithoutTotality ist False)
169 ctor
170 <>
171 nest 4 (text "Implementations:" <$>
172 vsep (if null implementations then [text "<no implementations>"]
173 else map pprintImplementation normalImplementations))
174 <>
175 (if null namedImplementations then empty
176 else line <$> nest 4 (text "Named implementations:" <$>
177 vsep (map pprintImplementation namedImplementations)))
178 <>
179 (if null sub_interfaces then empty
180 else line <$> nest 4 (text "Child interfaces:" <$>
181 vsep (map (dumpImplementation . prettifySubInterfaces) sub_interfaces)))
182 <>
183 (if null super_interfaces then empty
184 else line <$> nest 4 (text "Default parent implementations:" <$>
185 vsep (map dumpImplementation super_interfaces)))
186 where
187 params' = zip pNames (repeat False)
189 (normalImplementations, namedImplementations) = partition (\(n, _, _) -> not $ isJust n)
190 implementations
192 pNames = map fst params
194 ppo = ppOptionIst ist
195 infixes = idris_infixes ist
197 pprintImplementation (mname, term, (doc, argDocs)) =
198 nest 4 (iname mname <> dumpImplementation term <>
199 (if nullDocstring doc
200 then empty
201 else line <>
202 renderDocstring
203 (renderDocTerm
204 (pprintDelab ist)
205 (normaliseAll (tt_ctxt ist) []))
206 doc) <>
207 if null argDocs
208 then empty
209 else line <> vsep (map (prettyImplementationParam (map fst argDocs)) argDocs))
212 iname Nothing = empty
213 iname (Just n) = annName n <+> colon <> space
215 prettyImplementationParam params (name, doc) =
216 if nullDocstring doc
217 then empty
218 else prettyName True False (zip params (repeat False)) name <+>
219 showDoc ist doc
221-- if any (isJust . snd) params
222-- then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params)
223-- else hsep (punctuate comma (map (prettyName True False params' . fst) params))
225 dumpImplementation :: PTerm -> Doc OutputAnnotation
226 dumpImplementation = pprintPTerm ppo params' [] infixes
228 prettifySubInterfaces (PPi (Constraint _ _ _) _ _ tm _) = prettifySubInterfaces tm
229 prettifySubInterfaces (PPi plcity nm fc t1 t2) = PPi plcity (safeHead nm pNames) NoFC (prettifySubInterfaces t1) (prettifySubInterfaces t2)
230 prettifySubInterfaces (PApp fc ref args) = PApp fc ref $ updateArgs pNames args
231 prettifySubInterfaces tm = tm
233 safeHead _ (y:_) = y
234 safeHead x [] = x
236 updateArgs (p:ps) ((PExp prty opts _ ref):as) = (PExp prty opts p (updateRef p ref)) : updateArgs ps as
237 updateArgs ps (a:as) = a : updateArgs ps as
238 updateArgs _ _ = []
240 updateRef nm (PRef fc _ _) = PRef fc [] nm
241 updateRef _ pt = pt
243 isSubInterface (PPi (Constraint _ _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args')) = nm == n && map getTm args == map getTm args'
244 isSubInterface (PPi _ _ _ _ pt) = isSubInterface pt
245 isSubInterface _ = False
247 prettyConstraints =
248 cat (punctuate (comma <> space) (map (pprintPTerm ppo params' [] infixes) constraints))
250 prettyParameters =
251 if any (isJust . snd) params
252 then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params)
253 else hsep (punctuate comma (map (prettyName True False params' . fst) params))
255pprintDocs ist (RecordDoc n doc ctor projs params)
256 = nest 4 (text "Record" <+> prettyName True (ppopt_impl ppo) [] n <>
257 if nullDocstring doc
258 then empty
259 else line <>
260 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc)
261 -- Parameters
262 <$> (if null params
263 then empty
264 else line <> nest 4 (text "Parameters:" <$> prettyParameters) <> line)
265 -- Constructor
266 <$> nest 4 (text "Constructor:" <$> pprintFDWithoutTotality ist False ctor)
267 -- Projections
268 <$> nest 4 (text "Projections:" <$> vsep (map (pprintFDWithoutTotality ist False) projs))
269 where
270 ppo = ppOptionIst ist
271 infixes = idris_infixes ist
273 pNames = [n | (n,_,_) <- params]
274 params' = zip pNames (repeat False)
276 prettyParameters =
277 if any isJust [d | (_,_,d) <- params]
278 then vsep (map (\(n,pt,d) -> prettyParam (n,pt) <+> maybe empty (showDoc ist) d) params)
279 else hsep (punctuate comma (map prettyParam [(n,pt) | (n,pt,_) <- params]))
280 prettyParam (n,pt) = prettyName True False params' n <+> text ":" <+> pprintPTerm ppo params' [] infixes pt
282pprintDocs ist (NamedImplementationDoc _cls doc)
283 = nest 4 (text "Named implementation:" <$> pprintFDWithoutTotality ist True doc)
285pprintDocs ist (ModDoc mod docs)
286 = nest 4 $ text "Module" <+> text (concat (intersperse "." mod)) <> colon <$>
287 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) docs
289-- | Determine a truncation function depending how much docs the user
290-- wants to see
291howMuch FullDocs = id
292howMuch OverviewDocs = overview
294-- | Given a fully-qualified, disambiguated name, construct the
295-- documentation object for it
296getDocs :: Name -> HowMuchDocs -> Idris Docs
297getDocs n@(NS n' ns) w | n' == modDocName
298 = do i <- getIState
299 case lookupCtxtExact n (idris_moduledocs i) of
300 Just doc -> return . ModDoc (reverse (map T.unpack ns)) $ howMuch w doc
301 Nothing -> fail $ "Module docs for " ++ show (reverse (map T.unpack ns)) ++
302 " do not exist! This shouldn't have happened and is a bug."
303getDocs n w
304 = do i <- getIState
305 docs <- if | Just ci <- lookupCtxtExact n (idris_interfaces i)
306 -> docInterface n ci
307 | Just ri <- lookupCtxtExact n (idris_records i)
308 -> docRecord n ri
309 | Just ti <- lookupCtxtExact n (idris_datatypes i)
310 -> docData n ti
311 | Just interface_ <- interfaceNameForImpl i n
312 -> do fd <- docFun n
313 return $ NamedImplementationDoc interface_ fd
314 | otherwise
315 -> do fd <- docFun n
316 return (FunDoc fd)
317 return $ fmap (howMuch w) docs
318 where interfaceNameForImpl :: IState -> Name -> Maybe Name
319 interfaceNameForImpl ist n =
320 listToMaybe [ cn
321 | (cn, ci) <- toAlist (idris_interfaces ist)
322 , n `elem` map fst (interface_implementations ci)
323 ]
325docData :: Name -> TypeInfo -> Idris Docs
326docData n ti
327 = do tdoc <- docFun n
328 cdocs <- mapM docFun (con_names ti)
329 return (DataDoc tdoc cdocs)
331docInterface :: Name -> InterfaceInfo -> Idris Docs
332docInterface n ci
333 = do i <- getIState
334 let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i
335 docstr = maybe emptyDocstring fst docStrings
336 params = map (\pn -> (pn, docStrings >>= (lookup pn . snd)))
337 (interface_params ci)
338 docsForImplementation impl = fromMaybe (emptyDocstring, []) .
339 flip lookupCtxtExact (idris_docstrings i) $
340 impl
341 implementations = map (\impl -> (namedImpl impl,
342 delabTy i impl,
343 docsForImplementation impl))
344 (nub (map fst (interface_implementations ci)))
345 (sub_interfaces, implementations') = partition (isSubInterface . (\(_,tm,_) -> tm)) implementations
346 super_interfaces = catMaybes $ map getDImpl (interface_default_super_interfaces ci)
347 mdocs <- mapM (docFun . fst) (interface_methods ci)
348 let ctorN = implementationCtorName ci
349 ctorDocs <- case basename ctorN of
350 SN _ -> return Nothing
351 _ -> fmap Just $ docFun ctorN
352 return $ InterfaceDoc
353 n docstr mdocs params (interface_constraints ci)
354 implementations' (map (\(_,tm,_) -> tm) sub_interfaces) super_interfaces
355 ctorDocs
356 where
357 namedImpl (NS n ns) = fmap (flip NS ns) (namedImpl n)
358 namedImpl n@(UN _) = Just n
359 namedImpl _ = Nothing
361 getDImpl (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ t _ _) = Just t
362 getDImpl _ = Nothing
364 isSubInterface (PPi (Constraint _ _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args'))
365 = nm == n && map getTm args == map getTm args'
366 isSubInterface (PPi _ _ _ _ pt)
367 = isSubInterface pt
368 isSubInterface _
369 = False
371docRecord :: Name -> RecordInfo -> Idris Docs
372docRecord n ri
373 = do i <- getIState
374 let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i
375 docstr = maybe emptyDocstring fst docStrings
376 params = map (\(pn,pt) -> (pn, pt, docStrings >>= (lookup (nsroot pn) . snd)))
377 (record_parameters ri)
378 pdocs <- mapM docFun (record_projections ri)
379 ctorDocs <- docFun $ record_constructor ri
380 return $ RecordDoc n docstr ctorDocs pdocs params
382docFun :: Name -> Idris FunDoc
383docFun n
384 = do i <- getIState
385 let (docstr, argDocs) = case lookupCtxt n (idris_docstrings i) of
386 [d] -> d
387 _ -> noDocs
388 let ty = delabTy i n
389 let args = getPArgNames ty argDocs
390 let infixes = idris_infixes i
391 let fixdecls = filter (\(Fix _ x) -> x == funName n) infixes
392 let f = case fixdecls of
393 [] -> Nothing
394 (Fix x _:_) -> Just x
396 return (FD n docstr args ty f)
397 where funName :: Name -> String
398 funName (UN n) = str n
399 funName (NS n _) = funName n
400 funName n = show n
402getPArgNames :: PTerm -> [(Name, Docstring DocTerm)] -> [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
403getPArgNames (PPi plicity name _ ty body) ds =
404 (name, ty, plicity, lookup name ds) : getPArgNames body ds
405getPArgNames _ _ = []
407pprintConstDocs :: IState -> Const -> String -> Doc OutputAnnotation
408pprintConstDocs ist c str = text "Primitive" <+> text (if constIsType c then "type" else "value") <+>
409 pprintPTerm (ppOptionIst ist) [] [] [] (PConstant NoFC c) <+> colon <+>
410 pprintPTerm (ppOptionIst ist) [] [] [] (t c) <>
411 nest 4 (line <> text str)
413 where t (Fl _) = PConstant NoFC $ AType ATFloat
414 t (BI _) = PConstant NoFC $ AType (ATInt ITBig)
415 t (Str _) = PConstant NoFC StrType
416 t (Ch c) = PConstant NoFC $ AType (ATInt ITChar)
417 t _ = PType NoFC
420pprintTypeDoc :: IState -> Doc OutputAnnotation
421pprintTypeDoc ist = prettyIst ist (PType emptyFC) <+> colon <+> type1Doc <+>
422 nest 4 (line <> text typeDescription)