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