git.iko.soy/Idris-dev
on 63ff875 help sign in
Idris-dev/src/Idris/Docs.hs
383 lines 17 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 | RecordDoc Name d -- record docs
45 (FunDoc' d) -- data constructor docs
46 [FunDoc' d] -- projection docs
47 [(Name, PTerm, Maybe d)] -- parameters with type and doc
48 | NamedInstanceDoc Name (FunDoc' d) -- name is class
49 | ModDoc [String] -- Module name
50 d
51 deriving Functor
53type Docs = Docs' (Docstring DocTerm)
55showDoc ist d
56 | nullDocstring d = empty
57 | otherwise = text " -- " <>
58 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) d
60pprintFD :: IState -> Bool -> Bool -> FunDoc -> Doc OutputAnnotation
61pprintFD ist totalityFlag nsFlag (FD n doc args ty f)
62 = nest 4 (prettyName True nsFlag [] n <+> colon <+>
63 pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args
64 , not (T.isPrefixOf (T.pack "__") n') ] infixes ty <$>
65 -- show doc
66 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc <$>
67 -- show fixity
68 maybe empty (\f -> text (show f) <> line) f <>
69 -- show arguments doc
70 let argshow = showArgs args [] in
71 (if not (null argshow)
72 then nest 4 $ text "Arguments:" <$> vsep argshow
73 else empty) <>
74 -- show totality status
75 let totality = getTotality in
76 (if totalityFlag && not (null totality) then
77 line <> (vsep . map (\t -> text "The function is" <+> t) $ totality)
78 else
79 empty))
81 where ppo = ppOptionIst ist
82 infixes = idris_infixes ist
83 showArgs ((n, ty, Exp {}, Just d):args) bnd
84 = bindingOf n False <+> colon <+>
85 pprintPTerm ppo bnd [] infixes ty <>
86 showDoc ist d <> line
87 :
88 showArgs args ((n, False):bnd)
89 showArgs ((n, ty, Constraint {}, Just d):args) bnd
90 = text "Class constraint" <+>
91 pprintPTerm ppo bnd [] infixes ty <> showDoc ist d <> line
92 :
93 showArgs args ((n, True):bnd)
94 showArgs ((n, ty, Imp {}, Just d):args) bnd
95 = text "(implicit)" <+>
96 bindingOf n True <+> colon <+>
97 pprintPTerm ppo bnd [] infixes ty <>
98 showDoc ist d <> line
99 :
100 showArgs args ((n, True):bnd)
101 showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)
102 showArgs [] _ = []
103 getTotality = map (text . show) $ lookupTotal n (tt_ctxt ist)
105pprintFDWithTotality :: IState -> Bool -> FunDoc -> Doc OutputAnnotation
106pprintFDWithTotality ist = pprintFD ist True
108pprintFDWithoutTotality :: IState -> Bool -> FunDoc -> Doc OutputAnnotation
109pprintFDWithoutTotality ist = pprintFD ist False
111pprintDocs :: IState -> Docs -> Doc OutputAnnotation
112pprintDocs ist (FunDoc d) = pprintFDWithTotality ist True d
113pprintDocs ist (DataDoc t args)
114 = text "Data type" <+> pprintFDWithoutTotality ist True t <$>
115 if null args then text "No constructors."
116 else nest 4 (text "Constructors:" <> line <>
117 vsep (map (pprintFDWithoutTotality ist False) args))
118pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ctor)
119 = nest 4 (text "Type class" <+> prettyName True (ppopt_impl ppo) [] n <>
120 if nullDocstring doc
121 then empty
122 else line <> renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc)
123 <> line <$>
124 nest 4 (text "Parameters:" <$> prettyParameters)
125 <> line <$>
126 nest 4 (text "Methods:" <$>
127 vsep (map (pprintFDWithTotality ist False) meths))
128 <$>
129 maybe empty
130 ((<> line) . nest 4 .
131 (text "Instance constructor:" <$>) .
132 pprintFDWithoutTotality ist False)
133 ctor
134 <>
135 nest 4 (text "Instances:" <$>
136 vsep (if null instances then [text "<no instances>"]
137 else map pprintInstance normalInstances))
138 <>
139 (if null namedInstances then empty
140 else line <$> nest 4 (text "Named instances:" <$>
141 vsep (map pprintInstance namedInstances)))
142 <>
143 (if null subclasses then empty
144 else line <$> nest 4 (text "Subclasses:" <$>
145 vsep (map (dumpInstance . prettifySubclasses) subclasses)))
146 <>
147 (if null superclasses then empty
148 else line <$> nest 4 (text "Default superclass instances:" <$>
149 vsep (map dumpInstance superclasses)))
150 where
151 params' = zip pNames (repeat False)
153 (normalInstances, namedInstances) = partition (\(n, _, _) -> not $ isJust n)
154 instances
156 pNames = map fst params
158 ppo = ppOptionIst ist
159 infixes = idris_infixes ist
161 pprintInstance (mname, term, (doc, argDocs)) =
162 nest 4 (iname mname <> dumpInstance term <>
163 (if nullDocstring doc
164 then empty
165 else line <>
166 renderDocstring
167 (renderDocTerm
168 (pprintDelab ist)
169 (normaliseAll (tt_ctxt ist) []))
170 doc) <>
171 if null argDocs
172 then empty
173 else line <> vsep (map (prettyInstanceParam (map fst argDocs)) argDocs))
176 iname Nothing = empty
177 iname (Just n) = annName n <+> colon <> space
179 prettyInstanceParam params (name, doc) =
180 if nullDocstring doc
181 then empty
182 else prettyName True False (zip params (repeat False)) name <+>
183 showDoc ist doc
185-- if any (isJust . snd) params
186-- then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params)
187-- else hsep (punctuate comma (map (prettyName True False params' . fst) params))
189 dumpInstance :: PTerm -> Doc OutputAnnotation
190 dumpInstance = pprintPTerm ppo params' [] infixes
192 prettifySubclasses (PPi (Constraint _ _) _ _ tm _) = prettifySubclasses tm
193 prettifySubclasses (PPi plcity nm fc t1 t2) = PPi plcity (safeHead nm pNames) NoFC (prettifySubclasses t1) (prettifySubclasses t2)
194 prettifySubclasses (PApp fc ref args) = PApp fc ref $ updateArgs pNames args
195 prettifySubclasses tm = tm
197 safeHead _ (y:_) = y
198 safeHead x [] = x
200 updateArgs (p:ps) ((PExp prty opts _ ref):as) = (PExp prty opts p (updateRef p ref)) : updateArgs ps as
201 updateArgs ps (a:as) = a : updateArgs ps as
202 updateArgs _ _ = []
204 updateRef nm (PRef fc _ _) = PRef fc [] nm
205 updateRef _ pt = pt
207 isSubclass (PPi (Constraint _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args')) = nm == n && map getTm args == map getTm args'
208 isSubclass (PPi _ _ _ _ pt) = isSubclass pt
209 isSubclass _ = False
211 prettyParameters =
212 if any (isJust . snd) params
213 then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params)
214 else hsep (punctuate comma (map (prettyName True False params' . fst) params))
216pprintDocs ist (RecordDoc n doc ctor projs params)
217 = nest 4 (text "Record" <+> prettyName True (ppopt_impl ppo) [] n <>
218 if nullDocstring doc
219 then empty
220 else line <>
221 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc)
222 -- Parameters
223 <$> (if null params
224 then empty
225 else line <> nest 4 (text "Parameters:" <$> prettyParameters) <> line)
226 -- Constructor
227 <$> nest 4 (text "Constructor:" <$> pprintFDWithoutTotality ist False ctor)
228 -- Projections
229 <$> nest 4 (text "Projections:" <$> vsep (map (pprintFDWithoutTotality ist False) projs))
230 where
231 ppo = ppOptionIst ist
232 infixes = idris_infixes ist
234 pNames = [n | (n,_,_) <- params]
235 params' = zip pNames (repeat False)
237 prettyParameters =
238 if any isJust [d | (_,_,d) <- params]
239 then vsep (map (\(n,pt,d) -> prettyParam (n,pt) <+> maybe empty (showDoc ist) d) params)
240 else hsep (punctuate comma (map prettyParam [(n,pt) | (n,pt,_) <- params]))
241 prettyParam (n,pt) = prettyName True False params' n <+> text ":" <+> pprintPTerm ppo params' [] infixes pt
243pprintDocs ist (NamedInstanceDoc _cls doc)
244 = nest 4 (text "Named instance:" <$> pprintFDWithoutTotality ist True doc)
246pprintDocs ist (ModDoc mod docs)
247 = nest 4 $ text "Module" <+> text (concat (intersperse "." mod)) <> colon <$>
248 renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) docs
250-- | Determine a truncation function depending how much docs the user
251-- wants to see
252howMuch FullDocs = id
253howMuch OverviewDocs = overview
255-- | Given a fully-qualified, disambiguated name, construct the
256-- documentation object for it
257getDocs :: Name -> HowMuchDocs -> Idris Docs
258getDocs n@(NS n' ns) w | n' == modDocName
259 = do i <- getIState
260 case lookupCtxtExact n (idris_moduledocs i) of
261 Just doc -> return . ModDoc (reverse (map T.unpack ns)) $ howMuch w doc
262 Nothing -> fail $ "Module docs for " ++ show (reverse (map T.unpack ns)) ++
263 " do not exist! This shouldn't have happened and is a bug."
264getDocs n w
265 = do i <- getIState
266 docs <- if | Just ci <- lookupCtxtExact n (idris_classes i)
267 -> docClass n ci
268 | Just ri <- lookupCtxtExact n (idris_records i)
269 -> docRecord n ri
270 | Just ti <- lookupCtxtExact n (idris_datatypes i)
271 -> docData n ti
272 | Just class_ <- classNameForInst i n
273 -> do fd <- docFun n
274 return $ NamedInstanceDoc class_ fd
275 | otherwise
276 -> do fd <- docFun n
277 return (FunDoc fd)
278 return $ fmap (howMuch w) docs
279 where classNameForInst :: IState -> Name -> Maybe Name
280 classNameForInst ist n =
281 listToMaybe [ cn
282 | (cn, ci) <- toAlist (idris_classes ist)
283 , n `elem` map fst (class_instances ci)
284 ]
286docData :: Name -> TypeInfo -> Idris Docs
287docData n ti
288 = do tdoc <- docFun n
289 cdocs <- mapM docFun (con_names ti)
290 return (DataDoc tdoc cdocs)
292docClass :: Name -> ClassInfo -> Idris Docs
293docClass n ci
294 = do i <- getIState
295 let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i
296 docstr = maybe emptyDocstring fst docStrings
297 params = map (\pn -> (pn, docStrings >>= (lookup pn . snd)))
298 (class_params ci)
299 docsForInstance inst = fromMaybe (emptyDocstring, []) .
300 flip lookupCtxtExact (idris_docstrings i) $
301 inst
302 instances = map (\inst -> (namedInst inst,
303 delabTy i inst,
304 docsForInstance inst))
305 (nub (map fst (class_instances ci)))
306 (subclasses, instances') = partition (isSubclass . (\(_,tm,_) -> tm)) instances
307 superclasses = catMaybes $ map getDInst (class_default_superclasses ci)
308 mdocs <- mapM (docFun . fst) (class_methods ci)
309 let ctorN = instanceCtorName ci
310 ctorDocs <- case basename ctorN of
311 SN _ -> return Nothing
312 _ -> fmap Just $ docFun ctorN
313 return $ ClassDoc
314 n docstr mdocs params
315 instances' (map (\(_,tm,_) -> tm) subclasses) superclasses
316 ctorDocs
317 where
318 namedInst (NS n ns) = fmap (flip NS ns) (namedInst n)
319 namedInst n@(UN _) = Just n
320 namedInst _ = Nothing
322 getDInst (PInstance _ _ _ _ _ _ _ _ t _ _) = Just t
323 getDInst _ = Nothing
325 isSubclass (PPi (Constraint _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args'))
326 = nm == n && map getTm args == map getTm args'
327 isSubclass (PPi _ _ _ _ pt)
328 = isSubclass pt
329 isSubclass _
330 = False
332docRecord :: Name -> RecordInfo -> Idris Docs
333docRecord n ri
334 = do i <- getIState
335 let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i
336 docstr = maybe emptyDocstring fst docStrings
337 params = map (\(pn,pt) -> (pn, pt, docStrings >>= (lookup (nsroot pn) . snd)))
338 (record_parameters ri)
339 pdocs <- mapM docFun (record_projections ri)
340 ctorDocs <- docFun $ record_constructor ri
341 return $ RecordDoc n docstr ctorDocs pdocs params
343docFun :: Name -> Idris FunDoc
344docFun n
345 = do i <- getIState
346 let (docstr, argDocs) = case lookupCtxt n (idris_docstrings i) of
347 [d] -> d
348 _ -> noDocs
349 let ty = delabTy i n
350 let args = getPArgNames ty argDocs
351 let infixes = idris_infixes i
352 let fixdecls = filter (\(Fix _ x) -> x == funName n) infixes
353 let f = case fixdecls of
354 [] -> Nothing
355 (Fix x _:_) -> Just x
357 return (FD n docstr args ty f)
358 where funName :: Name -> String
359 funName (UN n) = str n
360 funName (NS n _) = funName n
361 funName n = show n
363getPArgNames :: PTerm -> [(Name, Docstring DocTerm)] -> [(Name, PTerm, Plicity, Maybe (Docstring DocTerm))]
364getPArgNames (PPi plicity name _ ty body) ds =
365 (name, ty, plicity, lookup name ds) : getPArgNames body ds
366getPArgNames _ _ = []
368pprintConstDocs :: IState -> Const -> String -> Doc OutputAnnotation
369pprintConstDocs ist c str = text "Primitive" <+> text (if constIsType c then "type" else "value") <+>
370 pprintPTerm (ppOptionIst ist) [] [] [] (PConstant NoFC c) <+> colon <+>
371 pprintPTerm (ppOptionIst ist) [] [] [] (t c) <>
372 nest 4 (line <> text str)
374 where t (Fl _) = PConstant NoFC $ AType ATFloat
375 t (BI _) = PConstant NoFC $ AType (ATInt ITBig)
376 t (Str _) = PConstant NoFC StrType
377 t (Ch c) = PConstant NoFC $ AType (ATInt ITChar)
378 t _ = PType NoFC
381pprintTypeDoc :: IState -> Doc OutputAnnotation
382pprintTypeDoc ist = prettyIst ist (PType emptyFC) <+> colon <+> type1Doc <+>
383 nest 4 (line <> text typeDescription)