@@ -1,17 +1,20 @@
11module Idris.Docs where
22
33import Idris.AbsSyntax
4+import Idris.AbsSyntaxTree
45import Idris.Delaborate
56import Core.TT
67import Core.Evaluate
78
89import Data.Maybe
10+import Data.List
911
1012-- TODO: Only include names with public/abstract accessibility
1113
1214data FunDoc = Doc Name String
1315 [(Name, PArg)] -- args
1416 PTerm -- function type
17+ (Maybe Fixity)
1518
1619data Doc = FunDoc FunDoc
1720 | DataDoc FunDoc -- type constructor docs
@@ -23,12 +26,14 @@ showDoc "" = ""
2326showDoc x = " -- " ++ x
2427
2528instance Show FunDoc where
26− show (Doc n doc args ty)
29+ show (Doc n doc args ty f)
2730 = show n ++ " : " ++ show ty ++ "\n" ++ showDoc doc ++ "\n" ++
31+ maybe "" (\f -> show f ++ "\n\n") f ++
2832 let argshow = mapMaybe showArg args in
29− if (not (null argshow)) then "Arguments:\n\t" ++
30− showSep "\t" argshow
31− else ""
33+ if not (null argshow)
34+ then "Arguments:\n\t" ++ showSep "\t" argshow
35+ else ""
36+
3237 where showArg (n, arg@(PExp _ _ _ _))
3338 = Just $ showName n ++ show (getTm arg) ++
3439 showDoc (pargdoc arg) ++ "\n"
@@ -94,6 +99,12 @@ docFun n
9499 let args = case lookupCtxt Nothing n (idris_implicits i) of
95100 [args] -> zip argnames args
96101 _ -> []
97− return (Doc n docstr args (delab i ty))
102+ let infixes = idris_infixes i
103+ let fixdecls = filter (\(Fix _ x) -> x `isSuffixOf` (show n)) infixes
104+ let f = case fixdecls of
105+ [] -> Nothing
106+ (Fix x _:_) -> Just x
107+
108+ return (Doc n docstr args (delab i ty) f)
98109
99110