feat: support docstrings/hovers for sorts (#79)

This allows hovers to pop up for Sort, Type, and Prop.

Author: david-christiansen

src/highlighting/SubVerso/Highlighting/Code.lean

@@ -33,7 +33,7 @@ partial def Token.Kind.priority : Token.Kind → Nat
   | .const .. => 5
   | .anonCtor .. => 6
   | .option .. => 4
-  | .sort => 4
+  | .sort .. => 4
   | .keyword _ _ _ => 3
   | .docComment | .withType .. => 1
   | .unknown => 0
@@ -154,7 +154,7 @@ where
       go more
 
 def exprKind [Monad m] [MonadLiftT IO m] [MonadMCtx m] [MonadEnv m]
-    (ci : ContextInfo) (lctx : LocalContext) (expr : Expr)
+    (ci : ContextInfo) (lctx : LocalContext) (stx? : Option Syntax) (expr : Expr)
     (allowUnknownTyped : Bool := false)
     : ReaderT Context m (Option Token.Kind) := do
   let runMeta {α} (act : MetaM α) (lctx := lctx) : m α := ci.runMetaM lctx act
@@ -190,7 +190,13 @@ def exprKind [Monad m] [MonadLiftT IO m] [MonadMCtx m] [MonadEnv m]
 
       let sig ← ppSig name
       return some <| .const name sig docs false
-    | Expr.sort .. => return some .sort
+    | Expr.sort u =>
+      if let some stx := stx? then
+        let k := stx.getKind
+        dbg_trace stx
+        let docs? ← findDocString? (← getEnv) k
+        return some (.sort u docs?)
+      else return some (.sort u none)
     | Expr.lit (.strVal s) => return some <| .str s
     | Expr.mdata _ e =>
       findKind e
@@ -228,7 +234,7 @@ def isDefinition [Monad m] [MonadEnv m] [MonadLiftT IO m] [MonadFileMap m] (name
 def termInfoKind [Monad m] [MonadLiftT IO m] [MonadMCtx m] [MonadEnv m] [MonadFileMap m]
     (ci : ContextInfo) (termInfo : TermInfo) (allowUnknownTyped : Bool := false)
     : ReaderT Context m (Option Token.Kind) := do
-  let k ← exprKind ci termInfo.lctx termInfo.expr (allowUnknownTyped := allowUnknownTyped)
+  let k ← exprKind ci termInfo.lctx termInfo.stx termInfo.expr (allowUnknownTyped := allowUnknownTyped)
   if (← read).definitionsPossible then
     if let some (.const name sig docs _isDef) := k then
       (some ∘ .const name sig docs) <$> (fun _ctxt => isDefinition name termInfo.stx)
@@ -660,11 +666,11 @@ def highlightGoals
       if decl.isAuxDecl || decl.isImplementationDetail then continue
       match decl with
       | .cdecl _index fvar name type _ _ =>
-        let nk ← exprKind ci lctx (.fvar fvar)
+        let nk ← exprKind ci lctx none (.fvar fvar)
         let tyStr ← renderTagged none (← runMeta (ppExprTagged =<< instantiateMVars type))
         hyps := hyps.push (name, nk.getD .unknown, tyStr)
       | .ldecl _index fvar name type val _ _ =>
-        let nk ← exprKind ci lctx (.fvar fvar)
+        let nk ← exprKind ci lctx none (.fvar fvar)
         let tyDoc ← runMeta (ppExprTagged =<< instantiateMVars type)
         let valDoc ← runMeta (ppExprTagged =<< instantiateMVars val)
         let tyValStr ← renderTagged none <| .append <| #[tyDoc].append <|
@@ -819,9 +825,9 @@ partial def highlight'
         | some (n, _) => findDocString? (← getEnv) n
       let name := lookingAt.map (·.1)
       let occ := lookingAt.map fun (n, pos) => s!"{n}-{pos}"
-      if let .sort ← identKind trees ⟨stx⟩ then
+      if let .sort u docs? ← identKind trees ⟨stx⟩ then
         withTraceNode `SubVerso.Highlighting.Code (fun _ => pure m!"Sort") do
-          emitToken i ⟨.sort, x⟩
+          emitToken i ⟨.sort u docs?, x⟩
         return
       else
         emitToken i <| (⟨ ·,  x⟩) <|

src/highlighting/SubVerso/Highlighting/Highlighted.lean

@@ -35,9 +35,31 @@ private def altNameUnJson (json : Json) : Except String Name := do
     | other => .error s!"Expected a string or number as a name component, got '{other}'"
   pure n
 
-private local instance : ToJson Name := ⟨altNameJson⟩
-private local instance : FromJson Name := ⟨altNameUnJson⟩
+private local instance nameToJson : ToJson Name := ⟨altNameJson⟩
+private local instance nameFromJson : FromJson Name := ⟨altNameUnJson⟩
 
+private partial local instance : ToJson Level where
+  toJson := go
+where
+  go
+    | .zero => .arr #["zero"]
+    | .succ l => .arr #["succ", go l]
+    | .param n => .arr #["param", nameToJson.toJson n]
+    | .max l l' => .arr #["max", go l, go l']
+    | .imax l l' => .arr #["imax", go l, go l']
+    | .mvar ⟨m⟩ => .arr #["mvar", nameToJson.toJson m]
+
+private partial local instance : FromJson Level where
+  fromJson? v := go v
+where
+  go
+    | .arr #["zero"] => pure .zero
+    | .arr #["succ", l] => .succ <$> go l
+    | .arr #["param", n] => .param <$> nameFromJson.fromJson? n
+    | .arr #["max", l, l'] => .max <$> go l <*> go l'
+    | .arr #["imax", l, l'] => .imax <$> go l <*> go l'
+    | .arr #["mvar", m] => (.mvar ⟨·⟩) <$> nameFromJson.fromJson? m
+    | other => throw s!"Failed to decode {other} as a level"
 
 inductive Token.Kind where
   | /-- `occurrence` is a unique identifier that unites the various keyword tokens from a given production -/
@@ -48,15 +70,30 @@ inductive Token.Kind where
   | str (string : String)
   | option (name : Name) (declName : Name) (docs : Option String)
   | docComment
-  | sort
+  | sort (level : Level) (doc? : Option String)
   | /-- The token represents some otherwise-undescribed Expr whose type is known -/
     withType (type : String)
   | unknown
 deriving Repr, Inhabited, BEq, Hashable, ToJson, FromJson
 
+open Lean.Syntax in
+instance : Quote LevelMVarId where
+  quote | ⟨m⟩ => mkCApp ``LevelMVarId.mk #[quote m]
+
+open Lean.Syntax in
+private partial def quoteLevel : Level → Term
+  | .zero => mkCApp ``Level.zero #[]
+  | .succ l => mkCApp ``Level.succ #[quoteLevel l]
+  | .param n => mkCApp ``Level.param #[quote n]
+  | .max l l' => mkCApp ``Level.max #[quoteLevel l, quoteLevel l']
+  | .imax l l' => mkCApp ``Level.imax #[quoteLevel l, quoteLevel l']
+  | .mvar mv => mkCApp ``Level.mvar #[quote mv]
+
+instance : Quote Level := ⟨quoteLevel⟩
+
 open Token.Kind in
 open Syntax (mkCApp) in
-instance : Quote Token.Kind where
+partial instance : Quote Token.Kind where
   quote
     | .keyword n occ docs => mkCApp ``keyword #[quote n, quote occ, quote docs]
     | .const n sig docs isDef => mkCApp ``const #[quote n, quote sig, quote docs, quote isDef]
@@ -65,7 +102,7 @@ instance : Quote Token.Kind where
     | .var (.mk n) type => mkCApp ``var #[mkCApp ``FVarId.mk #[quote n], quote type]
     | .str s => mkCApp ``str #[quote s]
     | .docComment => mkCApp ``docComment #[]
-    | .sort => mkCApp ``sort #[]
+    | .sort l doc? => mkCApp ``sort #[quote l, quote doc?]
     | .withType t => mkCApp ``withType #[quote t]
     | .unknown => mkCApp ``unknown #[]