@@ -6,63 +6,62 @@ import Idris.Delaborate
66import Idris.Core.TT
77import Idris.Core.Evaluate
88
9+import Util.Pretty
10+
911import Data.Maybe
1012import Data.List
1113
1214-- TODO: Only include names with public/abstract accessibility
1315
14−data FunDoc = Doc Name String
15− [(Name, PArg)] -- args
16− PTerm -- function type
17− (Maybe Fixity)
18−
19−data Doc = FunDoc FunDoc
20− | DataDoc FunDoc -- type constructor docs
21− [FunDoc] -- data constructor docs
22− | ClassDoc Name String -- class docs
23− [FunDoc] -- method docs
24−
25−showDoc "" = ""
26−showDoc x = " -- " ++ x
27−
28−instance 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 ""
36−
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))
16+data FunDoc = FD Name String
17+ [(Name, PTerm, Plicity)] -- args: name, ty, plicity
18+ PTerm -- function type
19+ (Maybe Fixity)
20+
21+data Docs = FunDoc FunDoc
22+ | DataDoc FunDoc -- type constructor docs
23+ [FunDoc] -- data constructor docs
24+ | ClassDoc Name String -- class docs
25+ [FunDoc] -- method docs
26+
27+showDoc "" = empty
28+showDoc x = text " -- " <> text x
29+
30+pprintFD :: Bool -> FunDoc -> Doc OutputAnnotation
31+pprintFD imp (FD n doc args ty f)
32+ = nest 4 (prettyName imp [] n <+> colon <+> prettyImp imp ty <$> showDoc doc <$>
33+ maybe empty (\f -> text (show f) <> line) f <>
34+ let argshow = mapMaybe showArg args in
35+ if not (null argshow)
36+ then nest 4 $ text "Arguments:" <$> vsep argshow
37+ else empty)
38+
39+ where showArg (n, ty, arg@(Exp {}))
40+ = Just $ bindingOf n False <+> colon <+> prettyImp imp ty <>
41+ showDoc (pdocstr arg) <> line
42+ showArg (n, ty, arg@(Constraint {}))
43+ = Just $ text "Class constraint" <+>
44+ prettyImp imp ty <> showDoc (pdocstr arg) <> line
45+ showArg (n, ty, arg@(Imp {}))
4546 | not (null doc)
46− = Just $ "(implicit) " ++
47− show n ++ " : " ++ show (getTm arg)
48− ++ showDoc (pargdoc arg) ++ "\n"
49− showArg (n, _) = Nothing
50−
51− showName (MN _ _) = ""
52− showName x = show x ++ " : "
53−
54−instance Show Doc where
55−
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)
64−
65−getDocs :: Name -> Idris Doc
47+ = Just $ text "(implicit)" <+>
48+ bindingOf n True <+> colon <+> prettyImp imp ty
49+ <> showDoc (pdocstr arg) <> line
50+ showArg (n, _, _) = Nothing
51+
52+
53+
54+pprintDocs imp (FunDoc d) = pprintFD imp d
55+pprintDocs imp (DataDoc t args)
56+ = text "Data type" <+> pprintFD imp t <$>
57+ nest 4 (text "Constructors:" <> line <>
58+ vsep (map (pprintFD imp) args))
59+pprintDocs imp (ClassDoc n doc meths)
60+ = text "Type class" <+> prettyName imp [] n <$> -- parameters?
61+ nest 4 (text "Methods:" <$>
62+ vsep (map (pprintFD imp) meths))
63+
64+getDocs :: Name -> Idris Docs
6665getDocs n
6766 = do i <- getIState
6867 case lookupCtxt n (idris_classes i) of
@@ -72,13 +71,13 @@ getDocs n
7271 _ -> do fd <- docFun n
7372 return (FunDoc fd)
7473
75−docData :: Name -> TypeInfo -> Idris Doc
74+docData :: Name -> TypeInfo -> Idris Docs
7675docData n ti
7776 = do tdoc <- docFun n
7877 cdocs <- mapM docFun (con_names ti)
7978 return (DataDoc tdoc cdocs)
8079
81−docClass :: Name -> ClassInfo -> Idris Doc
80+docClass :: Name -> ClassInfo -> Idris Docs
8281docClass n ci
8382 = do i <- getIState
8483 let docstr = case lookupCtxt n (idris_docstrings i) of
@@ -93,21 +92,19 @@ docFun n
9392 let docstr = case lookupCtxt n (idris_docstrings i) of
9493 [str] -> str
9594 _ -> ""
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− _ -> []
95+ let ty = delabTy i n
96+ let args = getPArgNames ty
10297 let infixes = idris_infixes i
10398 let fixdecls = filter (\(Fix _ x) -> x == funName n) infixes
10499 let f = case fixdecls of
105100 [] -> Nothing
106101 (Fix x _:_) -> Just x
107102
108− return (Doc n docstr args (delab i ty) f)
103+ return (FD n docstr args ty f)
109104 where funName :: Name -> String
110105 funName (UN n) = str n
111106 funName (NS n _) = funName n
112107
113−
108+getPArgNames :: PTerm -> [(Name, PTerm, Plicity)]
109+getPArgNames (PPi plicity name ty body) = ((name, ty, plicity) : getPArgNames body)
110+getPArgNames _ = []