[ new ] add docs-for-type-of IDE command

[DanMax03]

Description

I've decided to try to implement the issue #3157 in this PR. Right now it's a draft as long as I haven't resolved several issues: 1) I haven't tested it yet, because I don't see any clear way to install Idris without touching the main one (which is connected to $HOME/.idris2) 2) The problem is, after getting the type of the hole, I have only IPTerm representation of it. Thus, for calling process (DocsFor ? modeOpt) I need to use either already done function, or to extract the type name somehow

Should this change go in the CHANGELOG?

Definitely yes as a feature implementation

• [ ] If this is a fix, user-facing change, a compiler change, or a new paper implementation, I have updated CHANGELOG_NEXT.md (and potentially also CONTRIBUTORS.md).

[DanMax03]

Requesting @ohad @gallais to comment

[gallais]

If you chase various definitions you can see:

-- In Idris.IDEMode.REPL
process (DocsFor n modeOpt)
    = replWrap $ Idris.REPL.process (Doc $ APTerm (PRef EmptyFC (UN $ mkUserName n)))

-- Idris.REPL
process (Doc dir)
    = do doc <- getDocs dir
         pure $ PrintedDoc doc

-- In Idris.Doc.String
getDocs (APTerm ptm) = getDocsForPTerm ptm

(...)

getDocsForPTerm (PRef fc name) = getDocsForName fc name MkConfig

So if you can get the name of the type's head constructor you should be golden with getsDocsForName. Luckily there's a bunch of functions for you:

-- If you want to go under Pis in case the term is a function that's not fully applied
-- In Core.TT.Views
underPis : (n : Int) -> Env Term vars -> Term vars ->
           (bnds : SnocList Name ** (Env Term (bnds <>> vars), Term (bnds <>> vars)))

-- To grab the head of the application (after stripping off types if necessary)
-- In Core.TT.Term
getFn : Term vars -> Term vars

And you can then check that whatever you get back from getFn is indeed a Ref (you probably also want to handle types that are PrimVal or TType). It may be easier to call getDocsForPTerm directly after unelaborating the head using a placeholder for the Env (but I do think it's important to get your hands on the head term first):

-- In Core.Env
mkEnv : FC -> (vs : List Name) -> Env Term vs

-- In TTImp.Unelab
unelab : {vars : _} ->
         {auto c : Ref Ctxt Defs} ->
         Env Term vars ->
         Term vars -> Core IRawImp