git.iko.soy/Idris-dev
on de45d29 help sign in
Idris-dev/src/Idris/Docs.hs
203 lines 8.5 kB history raw
1{-# LANGUAGE PatternGuards #-}
2module Idris.Docs (pprintDocs, getDocs, pprintConstDocs, FunDoc(..), 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 [PTerm] -- superclasses
33 deriving Show
35showDoc d | nullDocstring d = empty
36 | otherwise = text " -- " <> renderDocstring d
38pprintFD :: IState -> FunDoc -> Doc OutputAnnotation
39pprintFD ist (FD n doc args ty f)
40 = nest 4 (prettyName True (ppopt_impl ppo) [] n <+> colon <+>
41 pprintPTerm ppo [] [ n | (n@(UN n'),_,_,_) <- args
42 , not (T.isPrefixOf (T.pack "__") n') ] infixes ty <$>
43 renderDocstring doc <$>
44 maybe empty (\f -> text (show f) <> line) f <>
45 let argshow = showArgs args [] in
46 if not (null argshow)
47 then nest 4 $ text "Arguments:" <$> vsep argshow
48 else empty)
50 where ppo = ppOptionIst ist
51 infixes = idris_infixes ist
52 showArgs ((n, ty, Exp {}, Just d):args) bnd
53 = bindingOf n False <+> colon <+>
54 pprintPTerm ppo bnd [] infixes ty <>
55 showDoc d <> line
56 :
57 showArgs args ((n, False):bnd)
58 showArgs ((n, ty, Constraint {}, Just d):args) bnd
59 = text "Class constraint" <+>
60 pprintPTerm ppo bnd [] infixes ty <> showDoc d <> line
61 :
62 showArgs args ((n, True):bnd)
63 showArgs ((n, ty, Imp {}, Just d):args) bnd
64 = text "(implicit)" <+>
65 bindingOf n True <+> colon <+>
66 pprintPTerm ppo bnd [] infixes ty <>
67 showDoc d <> line
68 :
69 showArgs args ((n, True):bnd)
70 showArgs ((n, _, _, _):args) bnd = showArgs args ((n, True):bnd)
71 showArgs [] _ = []
74pprintDocs :: IState -> Docs -> Doc OutputAnnotation
75pprintDocs ist (FunDoc d) = pprintFD ist d
76pprintDocs ist (DataDoc t args)
77 = text "Data type" <+> pprintFD ist t <$>
78 if null args then text "No constructors."
79 else nest 4 (text "Constructors:" <> line <>
80 vsep (map (pprintFD ist) args))
81pprintDocs ist (ClassDoc n doc meths params instances superclasses)
82 = nest 4 (text "Type class" <+> prettyName True (ppopt_impl ppo) [] n <>
83 if nullDocstring doc then empty else line <> renderDocstring doc)
84 <> line <$>
85 nest 4 (text "Parameters:" <$> prettyParameters)
86 <> line <$>
87 nest 4 (text "Methods:" <$>
88 vsep (map (pprintFD ist) meths))
89 <$>
90 nest 4 (text "Instances:" <$>
91 vsep (if null instances' then [text "<no instances>"]
92 else map dumpInstance instances'))
93 <>
94 (if null subclasses then empty
95 else line <$> nest 4 (text "Subclasses:" <$>
96 vsep (map (dumpInstance . prettifySubclasses) subclasses)))
97 <>
98 (if null superclasses then empty
99 else line <$> nest 4 (text "Default superclass instances:" <$>
100 vsep (map dumpInstance superclasses)))
101 where
102 params' = zip pNames (repeat False)
104 pNames = map fst params
106 ppo = ppOptionIst ist
107 infixes = idris_infixes ist
109 dumpInstance :: PTerm -> Doc OutputAnnotation
110 dumpInstance = pprintPTerm ppo params' [] infixes
112 prettifySubclasses (PPi (Constraint _ _) _ tm _) = prettifySubclasses tm
113 prettifySubclasses (PPi plcity nm t1 t2) = PPi plcity (safeHead nm pNames) (prettifySubclasses t1) (prettifySubclasses t2)
114 prettifySubclasses (PApp fc ref args) = PApp fc ref $ updateArgs pNames args
115 prettifySubclasses tm = tm
117 safeHead _ (y:_) = y
118 safeHead x [] = x
120 updateArgs (p:ps) ((PExp prty opts _ ref):as) = (PExp prty opts p (updateRef p ref)) : updateArgs ps as
121 updateArgs ps (a:as) = a : updateArgs ps as
122 updateArgs _ _ = []
124 updateRef nm (PRef fc _) = PRef fc nm
125 updateRef _ pt = pt
127 isSubclass (PPi (Constraint _ _) _ (PApp _ _ args) (PApp _ (PRef _ nm) args')) = nm == n && map getTm args == map getTm args'
128 isSubclass (PPi _ _ _ pt) = isSubclass pt
129 isSubclass _ = False
131 (subclasses, instances') = partition isSubclass instances
133 prettyParameters = if any (isJust . snd) params
134 then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty showDoc md) params)
135 else hsep (punctuate comma (map (prettyName True False params' . fst) params))
137getDocs :: Name -> Idris Docs
138getDocs n
139 = do i <- getIState
140 case lookupCtxt n (idris_classes i) of
141 [ci] -> docClass n ci
142 _ -> case lookupCtxt n (idris_datatypes i) of
143 [ti] -> docData n ti
144 _ -> do fd <- docFun n
145 return (FunDoc fd)
147docData :: Name -> TypeInfo -> Idris Docs
148docData n ti
149 = do tdoc <- docFun n
150 cdocs <- mapM docFun (con_names ti)
151 return (DataDoc tdoc cdocs)
153docClass :: Name -> ClassInfo -> Idris Docs
154docClass n ci
155 = do i <- getIState
156 let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i
157 docstr = maybe emptyDocstring fst docStrings
158 params = map (\pn -> (pn, docStrings >>= (lookup pn . snd))) (class_params ci)
159 instances = map (delabTy i) (class_instances ci)
160 superclasses = catMaybes $ map getDInst (class_default_superclasses ci)
161 mdocs <- mapM (docFun . fst) (class_methods ci)
162 return $ ClassDoc n docstr mdocs params instances superclasses
163 where
164 getDInst (PInstance _ _ _ _ _ t _ _) = Just t
165 getDInst _ = Nothing
167docFun :: Name -> Idris FunDoc
168docFun n
169 = do i <- getIState
170 let (docstr, argDocs) = case lookupCtxt n (idris_docstrings i) of
171 [d] -> d
172 _ -> noDocs
173 let ty = delabTy i n
174 let args = getPArgNames ty argDocs
175 let infixes = idris_infixes i
176 let fixdecls = filter (\(Fix _ x) -> x == funName n) infixes
177 let f = case fixdecls of
178 [] -> Nothing
179 (Fix x _:_) -> Just x
181 return (FD n docstr args ty f)
182 where funName :: Name -> String
183 funName (UN n) = str n
184 funName (NS n _) = funName n
185 funName n
186 | n == falseTy = "_|_"
188getPArgNames :: PTerm -> [(Name, Docstring)] -> [(Name, PTerm, Plicity, Maybe Docstring)]
189getPArgNames (PPi plicity name ty body) ds =
190 (name, ty, plicity, lookup name ds) : getPArgNames body ds
191getPArgNames _ _ = []
193pprintConstDocs :: IState -> Const -> String -> Doc OutputAnnotation
194pprintConstDocs ist c str = text "Primitive" <+> text (if constIsType c then "type" else "value") <+>
195 pprintPTerm (ppOptionIst ist) [] [] [] (PConstant c) <+> colon <+>
196 pprintPTerm (ppOptionIst ist) [] [] [] (t c) <>
197 nest 4 (line <> text str)
199 where t (Fl _) = PConstant $ AType ATFloat
200 t (BI _) = PConstant $ AType (ATInt ITBig)
201 t (Str _) = PConstant StrType
202 t (Ch c) = PConstant $ AType (ATInt ITChar)
203 t _ = PType