@@ -14,7 +14,7 @@ import Data.List
1414-- TODO: Only include names with public/abstract accessibility
1515
1616data FunDoc = FD Name String
17− [(Name, PArg)] -- args
17+ [(Name, PTerm, Plicity)] -- args: name, ty, plicity
1818 PTerm -- function type
1919 (Maybe Fixity)
2020
@@ -36,18 +36,18 @@ pprintFD imp (FD n doc args ty f)
3636 then nest 4 $ text "Arguments:" <$> vsep argshow
3737 else empty
3838
39− where showArg (n, arg@(PExp _ _ _ _))
40− = Just $ bindingOf n False <> prettyImp imp (getTm arg) <>
41− showDoc (pargdoc arg) <> line
42− showArg (n, arg@(PConstraint _ _ _ _))
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 {}))
4343 = Just $ text "Class constraint" <+>
44− prettyImp imp (getTm arg) <> showDoc (pargdoc arg) <> line
45− showArg (n, arg@(PImp _ _ _ _ _ doc))
44+ prettyImp imp ty <> showDoc (pdocstr arg) <> line
45+ showArg (n, ty, arg@(Imp {}))
4646 | not (null doc)
4747 = Just $ text "(implicit)" <+>
48− bindingOf n True <+> colon <+> prettyImp imp (getTm arg)
49− <> showDoc (pargdoc arg) <> line
50− showArg (n, _) = Nothing
48+ bindingOf n True <+> colon <+> prettyImp imp ty
49+ <> showDoc (pdocstr arg) <> line
50+ showArg (n, _, _) = Nothing
5151
5252
5353
@@ -93,10 +93,7 @@ docFun n
9393 [str] -> str
9494 _ -> ""
9595 let ty = delabTy i n
96− let argnames = getPArgNames ty
97− let args = case lookupCtxt n (idris_implicits i) of
98− [args] -> zip argnames args
99− _ -> []
96+ let args = getPArgNames ty
10097 let infixes = idris_infixes i
10198 let fixdecls = filter (\(Fix _ x) -> x == funName n) infixes
10299 let f = case fixdecls of
@@ -108,6 +105,6 @@ docFun n
108105 funName (UN n) = str n
109106 funName (NS n _) = funName n
110107
111−getPArgNames :: PTerm -> [Name]
112−getPArgNames (PPi plicity name ty body) = (name : getPArgNames body)
108+getPArgNames :: PTerm -> [(Name, PTerm, Plicity)]
109+getPArgNames (PPi plicity name ty body) = ((name, ty, plicity) : getPArgNames body)
113110getPArgNames _ = []