git.iko.soy/Idris-dev
on bba09bd help sign in
Idris-dev/src/Idris/Docs.hs
113 lines 3.7 kB history raw
1module Idris.Docs where
3import Idris.AbsSyntax
4import Idris.AbsSyntaxTree
5import Idris.Delaborate
6import Core.TT
7import Core.Evaluate
9import Data.Maybe
10import Data.List
12-- TODO: Only include names with public/abstract accessibility
14data FunDoc = Doc Name String
15 [(Name, PArg)] -- args
16 PTerm -- function type
17 (Maybe Fixity)
19data Doc = FunDoc FunDoc
20 | DataDoc FunDoc -- type constructor docs
21 [FunDoc] -- data constructor docs
22 | ClassDoc Name String -- class docs
23 [FunDoc] -- method docs
25showDoc "" = ""
26showDoc x = " -- " ++ x
28instance Show FunDoc where
29 show (Doc n doc args ty f)
30 = show n ++ " : " ++ show ty ++ "\n" ++ showDoc doc ++ "\n" ++
31 maybe "" (\f -> show f ++ "\n\n") f ++
32 let argshow = mapMaybe showArg args in
33 if not (null argshow)
34 then "Arguments:\n\t" ++ showSep "\t" argshow
35 else ""
37 where showArg (n, arg@(PExp _ _ _ _))
38 = Just $ showName n ++ show (getTm arg) ++
39 showDoc (pargdoc arg) ++ "\n"
40 showArg (n, arg@(PConstraint _ _ _ _))
41 = Just $ "Class constraint " ++
42 show (getTm arg) ++ showDoc (pargdoc arg)
43 ++ "\n"
44 showArg (n, arg@(PImp _ _ _ _ _ doc))
45 | not (null doc)
46 = Just $ "(implicit) " ++
47 show n ++ " : " ++ show (getTm arg)
48 ++ showDoc (pargdoc arg) ++ "\n"
49 showArg (n, _) = Nothing
51 showName (MN _ _) = ""
52 showName x = show x ++ " : "
54instance Show Doc where
56 show (FunDoc d) = show d
57 show (DataDoc t args) = "Data type " ++ show t ++
58 "\nConstructors:\n\n" ++
59 showSep "\n" (map show args)
60 show (ClassDoc n doc meths)
61 = "Type class " ++ show n ++ -- parameters?
62 "\nMethods:\n\n" ++
63 showSep "\n" (map show meths)
65getDocs :: Name -> Idris Doc
66getDocs n
67 = do i <- getIState
68 case lookupCtxt n (idris_classes i) of
69 [ci] -> docClass n ci
70 _ -> case lookupCtxt n (idris_datatypes i) of
71 [ti] -> docData n ti
72 _ -> do fd <- docFun n
73 return (FunDoc fd)
75docData :: Name -> TypeInfo -> Idris Doc
76docData n ti
77 = do tdoc <- docFun n
78 cdocs <- mapM docFun (con_names ti)
79 return (DataDoc tdoc cdocs)
81docClass :: Name -> ClassInfo -> Idris Doc
82docClass n ci
83 = do i <- getIState
84 let docstr = case lookupCtxt n (idris_docstrings i) of
85 [str] -> str
86 _ -> ""
87 mdocs <- mapM docFun (map fst (class_methods ci))
88 return (ClassDoc n docstr mdocs)
90docFun :: Name -> Idris FunDoc
91docFun n
92 = do i <- getIState
93 let docstr = case lookupCtxt n (idris_docstrings i) of
94 [str] -> str
95 _ -> ""
96 let ty = case lookupTy n (tt_ctxt i) of
97 (t : _) -> t
98 let argnames = map fst (getArgTys ty)
99 let args = case lookupCtxt n (idris_implicits i) of
100 [args] -> zip argnames args
101 _ -> []
102 let infixes = idris_infixes i
103 let fixdecls = filter (\(Fix _ x) -> x == funName n) infixes
104 let f = case fixdecls of
105 [] -> Nothing
106 (Fix x _:_) -> Just x
108 return (Doc n docstr args (delab i ty) f)
109 where funName :: Name -> String
110 funName (UN n) = n
111 funName (NS n _) = funName n