@@ -0,0 +1,97 @@
1+module Idris.Docs where
2+
3+import Idris.AbsSyntax
4+import Idris.Delaborate
5+import Core.TT
6+import Core.Evaluate
7+
8+import Data.Maybe
9+
10+data FunDoc = Doc Name String
11+ [(Name, PArg)] -- args
12+ PTerm -- function type
13+
14+data Doc = FunDoc FunDoc
15+ | DataDoc FunDoc -- type constructor docs
16+ [FunDoc] -- data constructor docs
17+ | ClassDoc Name String -- class docs
18+ [FunDoc] -- method docs
19+
20+showDoc "" = ""
21+showDoc x = " -- " ++ x ++ "\n"
22+
23+instance Show FunDoc where
24+ show (Doc n doc args ty)
25+ = show n ++ " : " ++ show ty ++ "\n" ++ showDoc doc ++
26+ let argshow = mapMaybe showArg args in
27+ if (not (null argshow)) then "Arguments:\n\t" ++
28+ showSep "\t" argshow
29+ else ""
30+ where showArg (n, arg@(PExp _ _ _ _))
31+ = Just $ showName n ++ show (getTm arg) ++
32+ showDoc (pargdoc arg) ++ "\n"
33+ showArg (n, arg@(PConstraint _ _ _ _))
34+ = Just $ "Class constraint " ++
35+ show (getTm arg) ++ showDoc (pargdoc arg)
36+ ++ "\n"
37+ showArg (n, arg@(PImp _ _ _ _ doc))
38+ | not (null doc)
39+ = Just $ "(implicit) " ++
40+ show n ++ " : " ++ show (getTm arg)
41+ ++ showDoc (pargdoc arg) ++ "\n"
42+ showArg (n, _) = Nothing
43+
44+ showName (MN _ _) = ""
45+ showName x = show x ++ " : "
46+
47+instance Show Doc where
48+
49+ show (FunDoc d) = show d
50+ show (DataDoc t args) = "Data type " ++ show t ++
51+ "\nConstructors:\n\n" ++
52+ showSep "\n" (map show args)
53+ show (ClassDoc n doc meths)
54+ = "Type class " ++ show n ++ -- parameters?
55+ "\nMethods:\n\n" ++
56+ showSep "\n" (map show meths)
57+
58+getDocs :: Name -> Idris Doc
59+getDocs n
60+ = do i <- getIState
61+ case lookupCtxt Nothing n (idris_classes i) of
62+ [ci] -> docClass n ci
63+ _ -> case lookupCtxt Nothing n (idris_datatypes i) of
64+ [ti] -> docData n ti
65+ _ -> do fd <- docFun n
66+ return (FunDoc fd)
67+
68+docData :: Name -> TypeInfo -> Idris Doc
69+docData n ti
70+ = do tdoc <- docFun n
71+ cdocs <- mapM docFun (con_names ti)
72+ return (DataDoc tdoc cdocs)
73+
74+docClass :: Name -> ClassInfo -> Idris Doc
75+docClass n ci
76+ = do i <- getIState
77+ let docstr = case lookupCtxt Nothing n (idris_docstrings i) of
78+ [str] -> str
79+ _ -> ""
80+ mdocs <- mapM docFun (map fst (class_methods ci))
81+ return (ClassDoc n docstr mdocs)
82+
83+docFun :: Name -> Idris FunDoc
84+docFun n
85+ = do i <- getIState
86+ let docstr = case lookupCtxt Nothing n (idris_docstrings i) of
87+ [str] -> str
88+ _ -> ""
89+ let ty = case lookupTy Nothing n (tt_ctxt i) of
90+ (t : _) -> t
91+ let argnames = map fst (getArgTys ty)
92+ let args = case lookupCtxt Nothing n (idris_implicits i) of
93+ [args] -> zip argnames args
94+ _ -> []
95+ return (Doc n docstr args (delab i ty))
96+
97+