@@ -14,7 +14,7 @@ import Data.List
14-- TODO: Only include names with public/abstract accessibility
14-- TODO: Only include names with public/abstract accessibility
16data FunDoc = FD Name String
16data FunDoc = FD Name String
17− [(Name, PArg)] -- args
17+ [(Name, PTerm, Plicity)] -- args: name, ty, plicity
18 PTerm -- function type
18 PTerm -- function type
19 (Maybe Fixity)
19 (Maybe Fixity)
@@ -36,18 +36,18 @@ pprintFD imp (FD n doc args ty f)
36 then nest 4 $ text "Arguments:" <$> vsep argshow
36 then nest 4 $ text "Arguments:" <$> vsep argshow
37 else empty
37 else empty
39− where showArg (n, arg@(PExp _ _ _ _))
39+ where showArg (n, ty, arg@(Exp {}))
40− = Just $ bindingOf n False <> prettyImp imp (getTm arg) <>
40+ = Just $ bindingOf n False <+> colon <+> prettyImp imp ty <>
41− showDoc (pargdoc arg) <> line
41+ showDoc (pdocstr arg) <> line
42− showArg (n, arg@(PConstraint _ _ _ _))
42+ showArg (n, ty, arg@(Constraint {}))
43 = Just $ text "Class constraint" <+>
43 = Just $ text "Class constraint" <+>
44− prettyImp imp (getTm arg) <> showDoc (pargdoc arg) <> line
44+ prettyImp imp ty <> showDoc (pdocstr arg) <> line
45− showArg (n, arg@(PImp _ _ _ _ _ doc))
45+ showArg (n, ty, arg@(Imp {}))
46 | not (null doc)
46 | not (null doc)
47 = Just $ text "(implicit)" <+>
47 = Just $ text "(implicit)" <+>
48− bindingOf n True <+> colon <+> prettyImp imp (getTm arg)
48+ bindingOf n True <+> colon <+> prettyImp imp ty
49− <> showDoc (pargdoc arg) <> line
49+ <> showDoc (pdocstr arg) <> line
50− showArg (n, _) = Nothing
50+ showArg (n, _, _) = Nothing
@@ -93,10 +93,7 @@ docFun n
93 [str] -> str
93 [str] -> str
95 let ty = delabTy i n
95 let ty = delabTy i n
96− let argnames = getPArgNames ty
96+ let args = getPArgNames ty
97− let args = case lookupCtxt n (idris_implicits i) of
98− [args] -> zip argnames args
100 let infixes = idris_infixes i
97 let infixes = idris_infixes i
101 let fixdecls = filter (\(Fix _ x) -> x == funName n) infixes
98 let fixdecls = filter (\(Fix _ x) -> x == funName n) infixes
102 let f = case fixdecls of
99 let f = case fixdecls of
@@ -108,6 +105,6 @@ docFun n
108 funName (UN n) = str n
105 funName (UN n) = str n
109 funName (NS n _) = funName n
106 funName (NS n _) = funName n
111−getPArgNames :: PTerm -> [Name]
108+getPArgNames :: PTerm -> [(Name, PTerm, Plicity)]
112−getPArgNames (PPi plicity name ty body) = (name : getPArgNames body)
109+getPArgNames (PPi plicity name ty body) = ((name, ty, plicity) : getPArgNames body)
113getPArgNames _ = []
110getPArgNames _ = []