git.iko.soy/Idris-dev
on aeb032a help sign in
Idris-dev/src/Idris/Docs.hs
418 lines 18 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 prettyConstraints =
244 cat (punctuate (comma <> space) (map (pprintPTerm ppo params' [] infixes) constraints))
246 prettyParameters =
247 if any (isJust . snd) params
248 then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params)
249 else hsep (punctuate comma (map (prettyName True False params' . fst) params))
251pprintDocs ist (RecordDoc n doc ctor projs params)
252 = nest 4 (text "Record" <+> prettyName True (ppopt_impl ppo) [] n <>
253 if nullDocstring doc
254 then empty
255 else line <>
256 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc)
257 -- Parameters
258 <$> (if null params
259 then empty
260 else line <> nest 4 (text "Parameters:" <$> prettyParameters) <> line)
261 -- Constructor
262 <$> nest 4 (text "Constructor:" <$> pprintFDWithoutTotality ist False ctor)
263 -- Projections
264 <$> nest 4 (text "Projections:" <$> vsep (map (pprintFDWithoutTotality ist False) projs))
265 where
266 ppo = ppOptionIst ist
267 infixes = idris_infixes ist
269 pNames = [n | (n,_,_) <- params]
270 params' = zip pNames (repeat False)
272 prettyParameters =
273 if any isJust [d | (_,_,d) <- params]
274 then vsep (map (\(n,pt,d) -> prettyParam (n,pt) <+> maybe empty (showDoc ist) d) params)
275 else hsep (punctuate comma (map prettyParam [(n,pt) | (n,pt,_) <- params]))
276 prettyParam (n,pt) = prettyName True False params' n <+> text ":" <+> pprintPTerm ppo params' [] infixes pt
278pprintDocs ist (NamedImplementationDoc _cls doc)
279 = nest 4 (text "Named implementation:" <$> pprintFDWithoutTotality ist True doc)
281pprintDocs ist (ModDoc mod docs)
282 = nest 4 $ text "Module" <+> text (concat (intersperse "." mod)) <> colon <$>
283 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) docs
285-- | Determine a truncation function depending how much docs the user
286-- wants to see
287howMuch FullDocs = id
288howMuch OverviewDocs = overview
290-- | Given a fully-qualified, disambiguated name, construct the
291-- documentation object for it
292getDocs :: Name -> HowMuchDocs -> Idris Docs
293getDocs n@(NS n' ns) w | n' == modDocName
294 = do i <- getIState
295 case lookupCtxtExact n (idris_moduledocs i) of
296 Just doc -> return . ModDoc (reverse (map T.unpack ns)) $ howMuch w doc
297 Nothing -> fail $ "Module docs for " ++ show (reverse (map T.unpack ns)) ++
298 " do not exist! This shouldn't have happened and is a bug."
299getDocs n w
300 = do i <- getIState
301 docs <- if | Just ci <- lookupCtxtExact n (idris_interfaces i)
302 -> docInterface n ci
303 | Just ri <- lookupCtxtExact n (idris_records i)
304 -> docRecord n ri
305 | Just ti <- lookupCtxtExact n (idris_datatypes i)
306 -> docData n ti
307 | Just interface_ <- interfaceNameForImpl i n
308 -> do fd <- docFun n
309 return $ NamedImplementationDoc interface_ fd
310 | otherwise
311 -> do fd <- docFun n
312 return (FunDoc fd)
313 return $ fmap (howMuch w) docs
314 where interfaceNameForImpl :: IState -> Name -> Maybe Name
315 interfaceNameForImpl ist n =
316 listToMaybe [ cn
317 | (cn, ci) <- toAlist (idris_interfaces ist)
318 , n `elem` map fst (interface_implementations ci)
319 ]
321docData :: Name -> TypeInfo -> Idris Docs
322docData n ti
323 = do tdoc <- docFun n
324 cdocs <- mapM docFun (con_names ti)
325 return (DataDoc tdoc cdocs)
327docInterface :: Name -> InterfaceInfo -> Idris Docs
328docInterface n ci
329 = do i <- getIState
330 let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i
331 docstr = maybe emptyDocstring fst docStrings
332 params = map (\pn -> (pn, docStrings >>= (lookup pn . snd)))
333 (interface_params ci)
334 docsForImplementation impl = fromMaybe (emptyDocstring, []) .
335 flip lookupCtxtExact (idris_docstrings i) $
336 impl
337 implementations = map (\impl -> (namedImpl impl,
338 delabTy i impl,
339 docsForImplementation impl))
340 (nub (map fst (interface_implementations ci)))
341 (sub_interfaces, implementations') = partition (isSubInterface . (\(_,tm,_) -> tm)) implementations
342 super_interfaces = catMaybes $ map getDImpl (interface_default_super_interfaces ci)
343 mdocs <- mapM (docFun . fst) (interface_methods ci)
344 let ctorN = implementationCtorName ci
345 ctorDocs <- case basename ctorN of
346 SN _ -> return Nothing
347 _ -> fmap Just $ docFun ctorN
348 return $ InterfaceDoc
349 n docstr mdocs params (interface_constraints ci)
350 implementations' (map (\(_,tm,_) -> tm) sub_interfaces) super_interfaces
351 ctorDocs
352 where
353 namedImpl (NS n ns) = fmap (flip NS ns) (namedImpl n)
354 namedImpl n@(UN _) = Just n
355 namedImpl _ = Nothing
357 getDImpl (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ t _ _) = Just t
358 getDImpl _ = Nothing
360 isSubInterface (PPi (Constraint _ _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args'))
361 = nm == n && map getTm args == map getTm args'
362 isSubInterface (PPi _ _ _ _ pt)
363 = isSubInterface pt
364 isSubInterface _
365 = False
367docRecord :: Name -> RecordInfo -> Idris Docs
368docRecord n ri
369 = do i <- getIState
370 let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i
371 docstr = maybe emptyDocstring fst docStrings
372 params = map (\(pn,pt) -> (pn, pt, docStrings >>= (lookup (nsroot pn) . snd)))
373 (record_parameters ri)
374 pdocs <- mapM docFun (record_projections ri)
375 ctorDocs <- docFun $ record_constructor ri
376 return $ RecordDoc n docstr ctorDocs pdocs params
378docFun :: Name -> Idris FunDoc
379docFun n
380 = do i <- getIState
381 let (docstr, argDocs) = case lookupCtxt n (idris_docstrings i) of
382 [d] -> d
383 _ -> noDocs
384 let ty = delabTy i n
385 let args = getPArgNames ty argDocs
386 let infixes = idris_infixes i
387 let fixdecls = filter (\(Fix _ x) -> x == funName n) infixes
388 let f = case fixdecls of
389 [] -> Nothing
390 (Fix x _:_) -> Just x
392 return (FD n docstr args ty f)
393 where funName :: Name -> String
394 funName (UN n) = str n
395 funName (NS n _) = funName n
396 funName n = show n
398getPArgNames :: PTerm -> [(Name, Docstring DocTerm)] -> [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
399getPArgNames (PPi plicity name _ ty body) ds =
400 (name, ty, plicity, lookup name ds) : getPArgNames body ds
401getPArgNames _ _ = []
403pprintConstDocs :: IState -> Const -> String -> Doc OutputAnnotation
404pprintConstDocs ist c str = text "Primitive" <+> text (if constIsType c then "type" else "value") <+>
405 pprintPTerm (ppOptionIst ist) [] [] [] (PConstant NoFC c) <+> colon <+>
406 pprintPTerm (ppOptionIst ist) [] [] [] (t c) <>
407 nest 4 (line <> text str)
409 where t (Fl _) = PConstant NoFC $ AType ATFloat
410 t (BI _) = PConstant NoFC $ AType (ATInt ITBig)
411 t (Str _) = PConstant NoFC StrType
412 t (Ch c) = PConstant NoFC $ AType (ATInt ITChar)
413 t _ = PType NoFC
416pprintTypeDoc :: IState -> Doc OutputAnnotation
417pprintTypeDoc ist = prettyIst ist (PType emptyFC) <+> colon <+> type1Doc <+>
418 nest 4 (line <> text typeDescription)