Also display methods of interfaces

Displaying implementations is a better harder at the moment, since
they're implemented via search hints...

src/Idris/DocString.idr

@@ -2,6 +2,10 @@ module Idris.DocString
 
 import Core.Context
 import Core.Core
+import Core.Env
+import Core.TT
+
+import Idris.Resugar
 import Idris.Syntax
 
 import Data.ANameMap
@@ -59,24 +63,36 @@ getDocsFor fc n
     showTotal n tot
         = "\nTotality: " ++ show tot
 
-    getConstructorDoc : Name -> Core (Maybe String)
-    getConstructorDoc con
+    getNameDoc : Name -> Core (Maybe String)
+    getNameDoc con
         = do defs <- get Ctxt
              Just def <- lookupCtxtExact con (gamma defs)
                   | Nothing => pure Nothing
              syn <- get Syn
              let [(n, str)] = lookupName con (docstrings syn)
                   | _ => pure Nothing
-             pure (Just (nameRoot n ++ "\n" ++ indent str))
+             ty <- normaliseHoles defs [] (type def)
+             pure (Just (nameRoot n ++ " : " ++ show !(resugar [] ty)
+                          ++ "\n" ++ indent str))
+
+    getIFaceDoc : (Name, IFaceInfo) -> Core String
+    getIFaceDoc (n, iface)
+        = do mdocs <- traverse getNameDoc (map fst (methods iface))
+             case mapMaybe id mdocs of
+                  [] => pure ""
+                  docs => pure $ "\nMethods:\n" ++ concat docs
 
-    -- TODO: If it's an interface, list the methods and implementations?
     getExtra : Name -> GlobalDef -> Core String
     getExtra n d
-        = case definition d of
+        = do syn <- get Syn
+             let [] = lookupName n (ifaces syn)
+                 | [ifacedata] => getIFaceDoc ifacedata
+                 | _ => pure "" -- shouldn't happen, we've resolved ambiguity by now
+             case definition d of
                PMDef _ _ _ _ _
                    => pure (showTotal n (totality d))
                TCon _ _ _ _ _ _ cons _
-                   => do cdocs <- traverse getConstructorDoc
+                   => do cdocs <- traverse getNameDoc
                                            !(traverse toFullNames cons)
                          case mapMaybe id cdocs of
                               [] => pure ""
@@ -84,10 +100,12 @@ getDocsFor fc n
                _ => pure ""
 
     showDoc : (Name, String) -> Core String
-    showDoc (n, "") = pure $ "No documentation for " ++ show n
     showDoc (n, str)
-        = do let doc = show n ++ "\n" ++ indent str
-             defs <- get Ctxt
-             def <- lookupCtxtExact n (gamma defs)
-             extra <- maybe (pure "") (getExtra n) def
+        = do defs <- get Ctxt
+             Just def <- lookupCtxtExact n (gamma defs)
+                  | Nothing => throw (UndefinedName fc n)
+             ty <- normaliseHoles defs [] (type def)
+             let doc = show n ++ " : " ++ show !(resugar [] ty)
+                              ++ "\n" ++ indent str
+             extra <- getExtra n def
              pure (doc ++ extra)

tests/idris2/docs001/expected

@@ -1,30 +1,48 @@
-Main> Prelude.plus
+Main> Prelude.plus : (1 _ : Nat) -> (1 _ : Nat) -> Nat
 	 Add two natural numbers.
 	 @ x the number to case-split on
 	 @ y the other numberpublic export
 
 Totality: total
-Main> Prelude.Nat
+Main> Prelude.Nat : Type
 	 Natural numbers: unbounded, unsigned integers which can be pattern matched.
 
 Constructors:
-Z
+Z : Nat
 	 Zero.
-S
+S : (1 _ : Nat) -> Nat
 	 Successor.
 
-Main> Prelude.List
+Main> Prelude.List : (1 _ : Type) -> Type
 	 Generic lists.
 
 Constructors:
-Nil
+Nil : List a
 	 Empty list
-::
+:: : (1 _ : a) -> (1 _ : List a) -> List a
 
-Main> Prelude.Show
+Main> Prelude.Show : Type -> Type
 	 Things that have a canonical `String` representation.
 
-Main> Prelude.show
+Methods:
+show : Show ty => ty -> String
+	 Convert a value to its `String` representation.
+	 @ x the value to convert
+showPrec : Show ty => Prec -> ty -> String
+	 Convert a value to its `String` representation in a certain precedence
+	 context.
+	
+	 A value should produce parentheses around itself if and only if the given
+	 precedence context is greater than or equal to the precedence of the
+	 outermost operation represented in the produced `String`.  *This is
+	 different from Haskell*, which requires it to be strictly greater.  `Open`
+	 should thus always produce *no* outermost parens, `App` should always
+	 produce outermost parens except on atomic values and those that provide
+	 their own bracketing, like `Pair` and `List`.
+	 @ d the precedence context.
+	 @ x the value to convert
+
+Main> Prelude.show : Show ty => ty -> String
 	 Convert a value to its `String` representation.
 	 @ x the value to convert