git.iko.soy/Idris-dev
on 08ddbaa help sign in
Idris-dev/src/Idris/Docs.hs
127 lines 4.5 kB history raw
1{-# LANGUAGE PatternGuards #-}
2module Idris.Docs where
4import Idris.AbsSyntax
5import Idris.AbsSyntaxTree
6import Idris.Delaborate
7import Idris.Core.TT
8import Idris.Core.Evaluate
9import Idris.Docstrings
11import Util.Pretty
13import Data.Maybe
14import Data.List
15import qualified Data.Text as T
17-- TODO: Only include names with public/abstract accessibility
19data FunDoc = FD Name Docstring
20 [(Name, PTerm, Plicity, Maybe Docstring)] -- args: name, ty, implicit, docs
21 PTerm -- function type
22 (Maybe Fixity)
23 deriving Show
25data Docs = FunDoc FunDoc
26 | DataDoc FunDoc -- type constructor docs
27 [FunDoc] -- data constructor docs
28 | ClassDoc Name Docstring -- class docs
29 [FunDoc] -- method docs
30 deriving Show
32showDoc d | nullDocstring d = empty
33 | otherwise = text " -- " <> renderDocstring d
35pprintFD :: Bool -> FunDoc -> Doc OutputAnnotation
36pprintFD imp (FD n doc args ty f)
37 = nest 4 (prettyName imp [] n <+> colon <+>
38 pprintPTerm imp [] [ n | (n@(UN n'),_,_,_) <- args
39 , not (T.isPrefixOf (T.pack "__") n') ] ty <$>
40 renderDocstring doc <$>
41 maybe empty (\f -> text (show f) <> line) f <>
42 let argshow = showArgs args [] in
43 if not (null argshow)
44 then nest 4 $ text "Arguments:" <$> vsep argshow
45 else empty)
47 where showArgs ((n, ty, Exp {}, Just d):args) bnd
48 = bindingOf n False <+> colon <+>
49 pprintPTerm imp bnd [] ty <>
50 showDoc d <> line
51 :
52 showArgs args ((n, False):bnd)
53 showArgs ((n, ty, Constraint {}, Just d):args) bnd
54 = text "Class constraint" <+>
55 pprintPTerm imp bnd [] ty <> showDoc d <> line
56 :
57 showArgs args ((n, True):bnd)
58 showArgs ((n, ty, Imp {}, Just d):args) bnd
59 = text "(implicit)" <+>
60 bindingOf n True <+> colon <+>
61 pprintPTerm imp bnd [] ty <>
62 showDoc d <> line
63 :
64 showArgs args ((n, True):bnd)
65 showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)
66 showArgs [] _ = []
70pprintDocs imp (FunDoc d) = pprintFD imp d
71pprintDocs imp (DataDoc t args)
72 = text "Data type" <+> pprintFD imp t <$>
73 nest 4 (text "Constructors:" <> line <>
74 vsep (map (pprintFD imp) args))
75pprintDocs imp (ClassDoc n doc meths)
76 = text "Type class" <+> prettyName imp [] n <$> -- parameters?
77 nest 4 (text "Methods:" <$>
78 vsep (map (pprintFD imp) meths))
80getDocs :: Name -> Idris Docs
81getDocs n
82 = do i <- getIState
83 case lookupCtxt n (idris_classes i) of
84 [ci] -> docClass n ci
85 _ -> case lookupCtxt n (idris_datatypes i) of
86 [ti] -> docData n ti
87 _ -> do fd <- docFun n
88 return (FunDoc fd)
90docData :: Name -> TypeInfo -> Idris Docs
91docData n ti
92 = do tdoc <- docFun n
93 cdocs <- mapM docFun (con_names ti)
94 return (DataDoc tdoc cdocs)
96docClass :: Name -> ClassInfo -> Idris Docs
97docClass n ci
98 = do i <- getIState
99 let docstr = case lookupCtxt n (idris_docstrings i) of
100 [str] -> fst str
101 _ -> emptyDocstring
102 mdocs <- mapM docFun (map fst (class_methods ci))
103 return (ClassDoc n docstr mdocs)
105docFun :: Name -> Idris FunDoc
106docFun n
107 = do i <- getIState
108 let (docstr, argDocs) = case lookupCtxt n (idris_docstrings i) of
109 [d] -> d
110 _ -> noDocs
111 let ty = delabTy i n
112 let args = getPArgNames ty argDocs
113 let infixes = idris_infixes i
114 let fixdecls = filter (\(Fix _ x) -> x == funName n) infixes
115 let f = case fixdecls of
116 [] -> Nothing
117 (Fix x _:_) -> Just x
119 return (FD n docstr args ty f)
120 where funName :: Name -> String
121 funName (UN n) = str n
122 funName (NS n _) = funName n
124getPArgNames :: PTerm -> [(Name, Docstring)] -> [(Name, PTerm, Plicity, Maybe Docstring)]
125getPArgNames (PPi plicity name ty body) ds =
126 (name, ty, plicity, lookup name ds) : getPArgNames body ds
127getPArgNames _ _ = []