[ new ] list hints attached to a data type

src/Core/Options/Log.idr

@@ -83,6 +83,7 @@ knownTopics = [
     ("declare.record.projection.prefix", Nothing),
     ("declare.type", Nothing),
     ("desugar.idiom", Nothing),
+    ("doc.data", Nothing),
     ("doc.record", Nothing),
     ("doc.module", Nothing),
     ("elab", Nothing),

src/Core/TT.idr

@@ -1748,3 +1748,33 @@ export
 {vars : _} -> Pretty (Term vars) where
   pretty = pretty . show
   -- TODO: prettier output
+
+export
+allGlobals : Term vars -> NameMap ()
+allGlobals (Local fc isLet idx p) = empty
+allGlobals (Ref fc x name) = singleton name ()
+allGlobals (Meta fc x y xs) = empty
+allGlobals (Bind fc x b scope) = allGlobals scope
+allGlobals (App fc fn arg) = allGlobals fn `merge` allGlobals arg
+allGlobals (As fc x as pat) = allGlobals as `merge` allGlobals pat
+allGlobals (TDelayed fc x y) = allGlobals y
+allGlobals (TDelay fc x ty arg) = allGlobals ty `merge` allGlobals arg
+allGlobals (TForce fc x y) = allGlobals y
+allGlobals (PrimVal fc c) = empty
+allGlobals (Erased fc imp) = empty
+allGlobals (TType fc) = empty
+
+export
+returnName : Term vars -> Maybe Name
+returnName (Local fc isLet idx p) = Nothing
+returnName (Ref fc x name) = pure name
+returnName (Meta fc x y xs) = Nothing
+returnName (Bind fc x b scope) = returnName scope
+returnName (App fc fn arg) = returnName fn
+returnName (As fc x as pat) = returnName pat
+returnName (TDelayed fc x y) = returnName y
+returnName (TDelay fc x ty arg) = returnName arg
+returnName (TForce fc x y) = returnName y
+returnName (PrimVal fc c) = Nothing
+returnName (Erased fc imp) = Nothing
+returnName (TType fc) = Nothing

src/Idris/Doc/String.idr

@@ -226,6 +226,35 @@ getDocsForName fc n config
                     ]
                _ => pure conWithTypeDoc
 
+    ||| Look up the implementations corresponding to the type
+    getImplDocs : Name -> Core (List (Doc IdrisDocAnn))
+    getImplDocs nty
+        = do log "doc.data" 10 $ "Looking at \{show nty}"
+             defs <- get Ctxt
+             docss <- for (concat $ values $ typeHints defs) $ \ (impl, _) =>
+               do Just def <- lookupCtxtExact impl (gamma defs)
+                    | _ => pure []
+                  ty <- toFullNames !(normaliseHoles defs [] (type def))
+                  -- Check the return type is not the type itself to avoid
+                  -- the hints corresponding to the data constructors
+                  -- Alternatively we could verify the return name is an
+                  -- interface but hints are not limited to interfaces so...
+                  let Just rnm = returnName ty
+                    | _ => pure []
+                  let False = nty == rnm
+                    | _ => pure []
+                  let nms = allGlobals ty
+                  log "doc.data" 10 $ String.unlines
+                    [ "Candidate: " ++ show ty
+                    , "Containing names: " ++ show nms
+                    ]
+                  let Just _ = lookup nty nms
+                        | _ => pure []
+                  ty <- resugar [] ty
+                  pure [annotate (Decl n) $ prettyTerm ty]
+             pure $ concat docss
+
+    ||| The name corresponds to an implementation, typeset its type accordingly
     getImplDoc : Name -> Core (List (Doc IdrisDocAnn))
     getImplDoc n
         = do defs <- get Ctxt
@@ -357,7 +386,13 @@ getDocsForName fc n config
                                , [vcat [header "Constructors"
                                        , annotate Declarations $
                                            vcat $ map (indent 2) docs]])
-                pure (map (tot ++) cdoc)
+                let idoc = case !(getImplDocs n) of
+                             [] => []
+                             [doc] => [header "Hint" <++> annotate Declarations doc]
+                             docs  => [vcat [header "Hints"
+                                            , annotate Declarations $
+                                                vcat $ map (indent 2) docs]]
+                pure (map (\ cons => tot ++ cons ++ idoc) cdoc)
            _ => pure (Nothing, [])
 
     showDoc (MkConfig {longNames, dropFirst, getTotality}) (n, str)

tests/idris2/docs001/expected

@@ -11,6 +11,38 @@ Main> data Prelude.Nat : Type
       Zero.
     S : Nat -> Nat
       Successor.
+  Hints:
+    Cast Nat String
+    Cast Nat Integer
+    Cast Nat Int
+    Cast Nat Char
+    Cast Nat Double
+    Cast Nat Bits8
+    Cast Nat Bits16
+    Cast Nat Bits32
+    Cast Nat Bits64
+    Cast Nat Int8
+    Cast Nat Int16
+    Cast Nat Int32
+    Cast Nat Int64
+    Cast String Nat
+    Cast Double Nat
+    Cast Char Nat
+    Cast Int Nat
+    Cast Integer Nat
+    Cast Bits8 Nat
+    Cast Bits16 Nat
+    Cast Bits32 Nat
+    Cast Bits64 Nat
+    Cast Int8 Nat
+    Cast Int16 Nat
+    Cast Int32 Nat
+    Cast Int64 Nat
+    Eq Nat
+    Num Nat
+    Ord Nat
+    Range Nat
+    Show Nat
 Main> data Prelude.List : Type -> Type
   Generic lists.
   Totality: total
@@ -19,6 +51,18 @@ Main> data Prelude.List : Type -> Type
       Empty list
     (::) : a -> List a -> List a
       A non-empty list, consisting of a head element and the rest of the list.
+  Hints:
+    Alternative List
+    Applicative List
+    Eq a => Eq (List a)
+    Foldable List
+    Functor List
+    Monad List
+    Monoid (List a)
+    Ord a => Ord (List a)
+    Semigroup (List a)
+    Show a => Show (List a)
+    Traversable List
 Main> interface Prelude.Show : Type -> Type
   Things that have a canonical `String` representation.
   Parameters: ty