feat: type signatures in Verso hovers

src/verso-blog/Verso/Genre/Blog/HighlightCode.lean

@@ -10,17 +10,18 @@ namespace Verso.Genre.Highlighted
 partial defmethod Highlighted.Token.Kind.priority : Highlighted.Token.Kind → Nat
   | .var .. => 2
   | .const .. => 5
+  | .option .. => 4
   | .sort => 4
   | .keyword _ _ => 3
   | .docComment => 1
   | .unknown => 0
 
 -- Find all info nodes whose canonical span matches the given syntax
-def infoForSyntax (t : InfoTree) (stx : Syntax) : List Info :=
-  t.collectNodesBottomUp fun _ info _ soFar =>
+def infoForSyntax (t : InfoTree) (stx : Syntax) : List (ContextInfo × Info) :=
+  t.collectNodesBottomUp fun ci info _ soFar =>
     if info.stx.getPos? true == stx.getPos? true &&
        info.stx.getTailPos? true == stx.getTailPos? true then
-      info :: soFar
+      (ci, info) :: soFar
     else soFar
 
 
@@ -105,47 +106,52 @@ where
       go more
 
 
-def identKind [Monad m] [MonadInfoTree m] [MonadLiftT IO m] [MonadFileMap m] [MonadEnv m] (ids : HashMap Lsp.RefIdent Lsp.RefIdent) (stx : TSyntax `ident) : m Token.Kind := do
+def identKind [Monad m] [MonadInfoTree m] [MonadLiftT IO m]  [MonadFileMap m] [MonadEnv m] [MonadMCtx m] (ids : HashMap Lsp.RefIdent Lsp.RefIdent) (stx : TSyntax `ident) : m Token.Kind := do
   let trees ← getInfoTrees
 
   let mut kind : Token.Kind := .unknown
 
   for t in trees do
-    for info in infoForSyntax t stx do
+    for (ci, info) in infoForSyntax t stx do
       match info with
-      | .ofTermInfo termInfo =>
-        match termInfo.expr with
+      | .ofTermInfo termInfo => do
+        let expr ← instantiateMVars termInfo.expr
+        let ty ← instantiateMVars (← ci.runMetaM info.lctx <| Meta.inferType expr)
+        let tyStr := toString (← ci.runMetaM info.lctx <| Meta.ppExpr ty)
+        match expr with
         | Expr.fvar id =>
           let seen ←
             if let some y := ids.find? (.fvar id) then
               match y with
               | .fvar x => pure <| .var x
               | .const x => do
                 let docs ← findDocString? (← getEnv) x
-                pure (.const x docs)
+                pure (.const x tyStr docs)
             else pure (.var id)
           if seen.priority > kind.priority then kind := seen
         | Expr.const name _ => --TODO universe vars
           let docs ← findDocString? (← getEnv) name
-          let seen := .const name docs
+          let seen := .const name tyStr docs
           if seen.priority > kind.priority then kind := seen
         | Expr.sort .. =>
           let seen := .sort
           if seen.priority > kind.priority then kind := seen
         | _ => continue
       | .ofFieldInfo fieldInfo =>
-          let docs ← findDocString? (← getEnv) fieldInfo.projName
-          let seen := .const fieldInfo.projName docs
-          if seen.priority > kind.priority then kind := seen
+        let ty ← instantiateMVars (← ci.runMetaM info.lctx <| Meta.inferType fieldInfo.val)
+        let tyStr := toString (← ci.runMetaM info.lctx <| Meta.ppExpr ty)
+        let docs ← findDocString? (← getEnv) fieldInfo.projName
+        let seen := .const fieldInfo.projName tyStr docs
+        if seen.priority > kind.priority then kind := seen
       | .ofFieldRedeclInfo _ => continue
       | .ofCustomInfo _ => continue
       | .ofMacroExpansionInfo _ => continue
       | .ofCompletionInfo _ => continue
       | .ofFVarAliasInfo _ => continue
       | .ofOptionInfo oi =>
-          let docs ← findDocString? (← getEnv) oi.declName
-          let seen := .const oi.declName docs
-          if seen.priority > kind.priority then kind := seen
+        let docs ← findDocString? (← getEnv) oi.declName
+        let seen := .option oi.declName docs
+        if seen.priority > kind.priority then kind := seen
       | .ofTacticInfo _ => continue
       | .ofUserWidgetInfo _ => continue
       | .ofCommandInfo _ => continue

src/verso-blog/Verso/Genre/Blog/Highlighted.lean

@@ -6,8 +6,9 @@ namespace Verso.Genre
 
 inductive Highlighted.Token.Kind where
   | keyword (name : Option Name) (docs : Option String)
-  | const (name : Name) (docs : Option String)
+  | const (name : Name) (type : String) (docs : Option String)
   | var (name : FVarId)
+  | option (name : Name) (docs : Option String)
   | docComment
   | sort
   | unknown
@@ -18,7 +19,8 @@ open Syntax (mkCApp) in
 instance : Quote Highlighted.Token.Kind where
   quote
     | .keyword n docs => mkCApp ``keyword #[quote n, quote docs]
-    | .const n docs => mkCApp ``const #[quote n, quote docs]
+    | .const n type docs => mkCApp ``const #[quote n, quote type, quote docs]
+    | .option n docs => mkCApp ``option #[quote n, quote docs]
     | .var (.mk n) => mkCApp ``var #[mkCApp ``FVarId.mk #[quote n]]
     | .docComment => mkCApp ``docComment #[]
     | .sort => mkCApp ``sort #[]

src/verso-blog/Verso/Genre/Blog/Template.lean

@@ -42,14 +42,16 @@ open HtmlT
 defmethod Highlighted.Token.Kind.«class» : Highlighted.Token.Kind → String
   | .var _ => "var"
   | .sort  => "sort"
-  | .const _ _ => "const"
+  | .const _ _ _ => "const"
+  | .option _ _ => "option"
   | .docComment => "doc-comment"
   | .keyword _ _ => "keyword"
   | .unknown => "unknown"
 
 defmethod Highlighted.Token.Kind.data : Highlighted.Token.Kind → String
-  | .const n _ => "const-" ++ toString n
+  | .const n _ _ => "const-" ++ toString n
   | .var ⟨v⟩ => "var-" ++ toString v
+  | .option n _ => "option-" ++ toString n
   | _ => ""
 
 
@@ -58,7 +60,12 @@ def hover (content : Html) : Html := {{
 }}
 
 defmethod Highlighted.Token.Kind.hover? : (tok : Highlighted.Token.Kind) → Option Html
-  | .const n doc | .keyword (some n) doc =>
+  | .const n ty doc =>
+    let docs := match doc with
+      | none => .empty
+      | some txt => {{<hr/><pre class="docstring">{{txt}}</pre>}}
+    some <| hover {{ {{toString n}} " : " {{ty}} {{docs}} }}
+  | .option n doc | .keyword (some n) doc =>
     let docs := match doc with
       | none => .empty
       | some txt => {{<hr/><pre class="docstring">{{txt}}</pre>}}