feat: add compatilibity shim system

.github/workflows/ci.yml

@@ -14,6 +14,7 @@ jobs:
           - "leanprover/lean4:4.5.0"
           - "leanprover/lean4:4.6.0"
           - "leanprover/lean4:4.7.0"
+          - "leanprover/lean4:nightly-2024-04-07"
     name: Build and test
     runs-on: ubuntu-latest
     steps:

lakefile.lean

@@ -4,6 +4,10 @@ open Lake DSL
 package «subverso» where
   -- add package configuration options here
 
+lean_lib SubVersoCompat where
+  srcDir := "src/compat"
+  roots := #[`SubVerso.Compat]
+
 lean_lib SubVersoHighlighting where
   srcDir := "src/highlighting"
   roots := #[`SubVerso.Highlighting]

src/compat/SubVerso/Compat.lean

@@ -0,0 +1,54 @@
+import Lean
+
+open Lean Elab Term
+
+namespace SubVerso.Compat
+
+elab "%first_defined" "[" xs:ident,* "]" : term => do
+  let env ← getEnv
+  for x in xs.getElems do
+    if env.contains x.getId then
+      let expr ← elabTerm x none
+      return expr
+  throwError "None of the names exist"
+
+
+def realizeNameNoOverloads
+    [Monad m] [MonadEnv m] [MonadLiftT CoreM m] [MonadError m]
+    [MonadInfoTree m] [MonadResolveName m]
+    (ident : Syntax) : m Name :=
+  %first_defined [
+    Lean.Elab.realizeGlobalConstNoOverloadWithInfo,
+    Lean.Elab.resolveGlobalConstNoOverloadWithInfo
+  ] ident
+
+
+elab "%first_succeeding" "[" es:term,* "]" : term <= ty => do
+  for e in es.getElems do
+    try
+      let expr ←
+        withReader ({· with errToSorry := false}) <|
+            elabTerm e (some ty)
+      return expr
+    catch _ =>
+      continue
+  throwError "No alternative succeeded"
+
+
+def mkRefIdentFVar [Monad m] [MonadEnv m] (id : FVarId) : m Lean.Lsp.RefIdent := do
+  pure %first_succeeding [
+    .fvar (← getEnv).mainModule id,
+    .fvar id
+  ]
+
+def refIdentCase (ri : Lsp.RefIdent)
+    (onFVar : FVarId → α)
+    (onConst : Name → α) : α :=
+  %first_succeeding [
+    match ri with
+    | .fvar _ id => onFVar id
+    | .const _ x => onConst x,
+    match ri with
+    | .fvar id => onFVar id
+    | .const x => onConst x
+  ]

src/examples/SubVerso/Examples.lean

@@ -1,4 +1,5 @@
 import SubVerso.Highlighting
+import SubVerso.Compat
 import SubVerso.Examples.Env
 import Lean.Environment
 
@@ -83,7 +84,7 @@ where
   asBool (stx : TSyntax `term) : TermElabM Bool := do
     match stx with
     | `($x:ident) =>
-      match ← resolveGlobalConstNoOverloadWithInfo x with
+      match ← Compat.realizeNameNoOverloads x with
       | ``true => pure true
       | ``false => pure false
       | other => throwErrorAt stx "Expected Boolean literal, got {other}"

src/highlighting/SubVerso/Highlighting/Code.lean

@@ -1,6 +1,7 @@
 import Lean
 import Lean.Widget.TaggedText
 
+import SubVerso.Compat
 import SubVerso.Highlighting.Highlighted
 
 open Lean Elab
@@ -116,20 +117,21 @@ def exprKind [Monad m] [MonadLiftT IO m] [MonadMCtx m] [MonadEnv m]
   match ← instantiateMVars expr with
   | Expr.fvar id =>
     let seen ←
-      if let some y := ids.find? (.fvar id) then
-        match y with
-        | .fvar x =>
-          let ty ← instantiateMVars (← runMeta <| Meta.inferType expr)
-          let tyStr := toString (← runMeta <| Meta.ppExpr ty)
-          if let some localDecl := lctx.find? x then
-            if localDecl.isAuxDecl then
-              let e ← runMeta <| Meta.ppExpr expr
-              return some (.const (toString e) tyStr none)
-          return some (.var x tyStr)
-        | .const x =>
-          let sig := toString (← runMeta (PrettyPrinter.ppSignature x)).1
-          let docs ← findDocString? (← getEnv) x
-          return some (.const x sig docs)
+      if let some y := ids.find? (← Compat.mkRefIdentFVar id) then
+        Compat.refIdentCase y
+          (onFVar := fun x => do
+            let ty ← instantiateMVars (← runMeta <| Meta.inferType expr)
+            let tyStr := toString (← runMeta <| Meta.ppExpr ty)
+            if let some localDecl := lctx.find? x then
+              if localDecl.isAuxDecl then
+                let e ← runMeta <| Meta.ppExpr expr
+                -- FIXME the mkSimple is a bit of a kludge
+                return some (.const (.mkSimple (toString e)) tyStr none)
+            return some (.var x tyStr))
+          (onConst := fun x => do
+            let sig := toString (← runMeta (PrettyPrinter.ppSignature x)).1
+            let docs ← findDocString? (← getEnv) x
+            return some (.const x sig docs))
       else
         let ty ← instantiateMVars (← runMeta <| Meta.inferType expr)
         let tyStr := toString (← runMeta <| Meta.ppExpr ty)