git.iko.soy/Idris-dev
on dda9b49 help sign in
Idris-dev/src/Idris/Docs.hs
164 lines 6.4 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 [(Name, Maybe Docstring)] -- parameters and their docstrings
31 [PTerm] -- instances
32 deriving Show
34showDoc d | nullDocstring d = empty
35 | otherwise = text " -- " <> renderDocstring d
37pprintFD :: Bool -> FunDoc -> Doc OutputAnnotation
38pprintFD imp (FD n doc args ty f)
39 = nest 4 (prettyName imp [] n <+> colon <+>
40 pprintPTerm imp [] [ n | (n@(UN n'),_,_,_) <- args
41 , not (T.isPrefixOf (T.pack "__") n') ] ty <$>
42 renderDocstring doc <$>
43 maybe empty (\f -> text (show f) <> line) f <>
44 let argshow = showArgs args [] in
45 if not (null argshow)
46 then nest 4 $ text "Arguments:" <$> vsep argshow
47 else empty)
49 where showArgs ((n, ty, Exp {}, Just d):args) bnd
50 = bindingOf n False <+> colon <+>
51 pprintPTerm imp bnd [] ty <>
52 showDoc d <> line
53 :
54 showArgs args ((n, False):bnd)
55 showArgs ((n, ty, Constraint {}, Just d):args) bnd
56 = text "Class constraint" <+>
57 pprintPTerm imp bnd [] ty <> showDoc d <> line
58 :
59 showArgs args ((n, True):bnd)
60 showArgs ((n, ty, Imp {}, Just d):args) bnd
61 = text "(implicit)" <+>
62 bindingOf n True <+> colon <+>
63 pprintPTerm imp bnd [] ty <>
64 showDoc d <> line
65 :
66 showArgs args ((n, True):bnd)
67 showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)
68 showArgs [] _ = []
71pprintDocs :: Bool -> Docs -> Doc OutputAnnotation
72pprintDocs imp (FunDoc d) = pprintFD imp d
73pprintDocs imp (DataDoc t args)
74 = text "Data type" <+> pprintFD imp t <$>
75 nest 4 (text "Constructors:" <> line <>
76 vsep (map (pprintFD imp) args))
77pprintDocs imp (ClassDoc n doc meths params instances)
78 = nest 4 (text "Type class" <+> prettyName imp [] n <>
79 if nullDocstring doc then empty else line <> renderDocstring doc)
80 <> line <$>
81 nest 4 (text "Parameters:" <$> prettyParameters)
82 <> line <$>
83 nest 4 (text "Methods:" <$>
84 vsep (map (pprintFD imp) meths))
85 <$>
86 nest 4 (text "Instances:" <$>
87 vsep (if null instances' then [text "<no instances>"]
88 else map dumpInstance instances'))
89 <>
90 if null subclasses then empty
91 else line <$> nest 4 (text "Subclasses:" <$>
92 vsep (map (dumpInstance . remConstraint) subclasses))
93 where
94 params' = map (\x -> (fst x, False)) params
96 dumpInstance :: PTerm -> Doc OutputAnnotation
97 dumpInstance = pprintPTerm imp params' []
99 remConstraint (PPi (Constraint _ _) _ tm _) = tm
100 remConstraint (PPi x y z pt) = PPi x y z (remConstraint pt)
101 remConstraint p = p
103 hasConstraint (PPi (Constraint _ _) _ _ _) = True
104 hasConstraint (PPi _ _ _ pt) = hasConstraint pt
105 hasConstraint _ = False
107 (subclasses, instances') = partition hasConstraint instances
109 prettyParameters = if any (isJust . snd) params
110 then vsep (map (\(n,md) -> prettyName False params' n <+> maybe empty showDoc md) params)
111 else hsep (punctuate comma (map (prettyName False params' . fst) params))
113getDocs :: Name -> Idris Docs
114getDocs n
115 = do i <- getIState
116 case lookupCtxt n (idris_classes i) of
117 [ci] -> docClass n ci
118 _ -> case lookupCtxt n (idris_datatypes i) of
119 [ti] -> docData n ti
120 _ -> do fd <- docFun n
121 return (FunDoc fd)
123docData :: Name -> TypeInfo -> Idris Docs
124docData n ti
125 = do tdoc <- docFun n
126 cdocs <- mapM docFun (con_names ti)
127 return (DataDoc tdoc cdocs)
129docClass :: Name -> ClassInfo -> Idris Docs
130docClass n ci
131 = do i <- getIState
132 ctxt <- getContext
133 let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i
134 docstr = maybe emptyDocstring fst docStrings
135 params = map (\pn -> (pn, docStrings >>= (lookup pn . snd))) (class_params ci)
136 instances = map (delabTy i) (class_instances ci)
137 mdocs <- mapM (docFun .fst) (class_methods ci)
138 return $ ClassDoc n docstr mdocs params instances
140docFun :: Name -> Idris FunDoc
141docFun n
142 = do i <- getIState
143 let (docstr, argDocs) = case lookupCtxt n (idris_docstrings i) of
144 [d] -> d
145 _ -> noDocs
146 let ty = delabTy i n
147 let args = getPArgNames ty argDocs
148 let infixes = idris_infixes i
149 let fixdecls = filter (\(Fix _ x) -> x == funName n) infixes
150 let f = case fixdecls of
151 [] -> Nothing
152 (Fix x _:_) -> Just x
154 return (FD n docstr args ty f)
155 where funName :: Name -> String
156 funName (UN n) = str n
157 funName (NS n _) = funName n
158 funName n
159 | n == falseTy = "_|_"
161getPArgNames :: PTerm -> [(Name, Docstring)] -> [(Name, PTerm, Plicity, Maybe Docstring)]
162getPArgNames (PPi plicity name ty body) ds =
163 (name, ty, plicity, lookup name ds) : getPArgNames body ds
164getPArgNames _ _ = []