chore: compatibility shims for HashMap, plus wider overall compat (#39)

.github/workflows/ci.yml

@@ -9,6 +9,9 @@ jobs:
     strategy:
       matrix:
         toolchain:
+          - "4.0.0"
+          - "4.1.0"
+          - "4.2.0"
           - "4.3.0"
           - "4.4.0"
           - "4.5.0"
@@ -18,7 +21,7 @@ jobs:
           - "4.9.0"
           - "4.10.0"
           - "4.11.0-rc1"
-          - "nightly-2024-08-08"
+          - "nightly-2024-08-09"
         platform:
           - os: ubuntu-latest
             installer: |

Extract.lean

@@ -3,6 +3,7 @@ Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: David Thrane Christiansen
 -/
+import SubVerso.Compat
 import SubVerso.Examples.Env
 
 open Lean
@@ -13,7 +14,7 @@ def main : (args : List String) → IO UInt32
     try
       initSearchPath (← findSysroot)
       let modName := mod.toName
-      let env ← importModules #[{module := modName, runtimeOnly := false}] {}
+      let env ← SubVerso.Compat.importModules #[{module := modName, runtimeOnly := false}] {}
       let modExamples := highlighted.getState env
       let useful := relevant modName modExamples
       let exJson := Json.mkObj useful

Tests.lean

@@ -14,7 +14,7 @@ open Lean Elab Command
 open SubVerso.Examples.Slice
 
 elab "#test_slicing" s:str out:ident c:command : command => do
-  let {original, residual, sliced} ← sliceSyntax c
+  let {original := _, residual, sliced} ← sliceSyntax c
 
   let mut log := ""
 
@@ -24,7 +24,7 @@ elab "#test_slicing" s:str out:ident c:command : command => do
     log := log ++ s!"Slice {s}:\n{Syntax.prettyPrint stx}"
 
   let use := s.getString
-  if let some stx := sliced.find? use then
+  if let some stx := sliced[use]? then
     elabCommand stx
   else
     logInfo m!"Slice '{use}' not found"

src/compat/SubVerso/Compat.lean

@@ -29,16 +29,28 @@ def realizeNameNoOverloads
 
 
 elab "%first_succeeding" "[" es:term,* "]" : term <= ty => do
+  let mut errs := #[]
   for e in es.getElems do
     try
       let expr ←
         withReader ({· with errToSorry := false}) <|
-            elabTerm e (some ty)
-      return expr
-    catch _ =>
+            elabTermEnsuringType e (some ty)
+      let ty' ← Meta.inferType expr
+      if ← Meta.isDefEq ty ty' then
+        return expr
+    catch err =>
+      errs := errs.push (e, err)
       continue
-  throwError "No alternative succeeded"
+  let msgErrs := errs.toList.map fun (tm, msg) => m!"{tm}: {indentD msg.toMessageData}"
+  throwError m!"No alternative succeeded. Attempts were: " ++
+    indentD (MessageData.joinSep msgErrs Format.line)
+
+open Command in
+elab "%if_bound" x:ident cmd:command : command => do
+  if (← getEnv).contains x.getId then elabCommand cmd
 
+def importModules (imports : Array Import) (opts : Options) (trustLevel : UInt32 := 0) : IO Environment :=
+  Lean.importModules (%first_succeeding [imports, imports.toList]) opts (trustLevel := trustLevel)
 
 def mkRefIdentFVar [Monad m] [MonadEnv m] (id : FVarId) : m Lean.Lsp.RefIdent := do
   pure %first_succeeding [
@@ -60,3 +72,46 @@ def refIdentCase (ri : Lsp.RefIdent)
 
 abbrev Parsec (α : Type) : Type :=
   %first_succeeding [(Lean.Parsec α : Type), (Lean.Parsec String.Iterator α : Type)]
+
+def HashMap := %first_succeeding [Std.HashMap, Lean.HashMap]
+def HashSet := %first_succeeding [Std.HashSet, Lean.HashSet]
+
+namespace HashMap
+
+instance [BEq α] [Hashable α] : Membership α (HashMap α β) :=
+  %first_succeeding [
+    inferInstanceAs (Membership α (Std.HashMap α β)),
+    ⟨fun k hm => hm.contains k⟩
+  ]
+
+instance [BEq α] [Hashable α] {x : α} {hm : HashMap α β} : Decidable (x ∈ hm) :=
+  %first_succeeding [
+    inferInstanceAs (Decidable (x ∈ (hm : Std.HashMap α β))),
+    inferInstanceAs (Decidable (hm.contains x = true))
+  ]
+
+instance instGetElemHashMap [BEq α] [Hashable α] [Inhabited β] : GetElem (HashMap α β) α β (fun m a => a ∈ m) :=
+  %first_succeeding [
+    inferInstanceAs (GetElem (Std.HashMap α β) α β (fun m a => a ∈ m)),
+    ⟨fun m a _ok => m.find! a⟩,
+    ⟨fun m a _ok => m.find! a, fun m a => Lean.HashMap.find? m a, fun m a => Lean.HashMap.find! m a⟩
+  ]
+
+def get? {_ : BEq α} {_ : Hashable α} : HashMap α β → α → Option β :=
+  %first_defined [Std.HashMap.get?, Lean.HashMap.find?]
+
+def get! {_ : BEq α} {_ : Hashable α} [Inhabited β] : HashMap α β → α → β :=
+  %first_defined [Std.HashMap.get!, Lean.HashMap.find!]
+
+def getD {_ : BEq α} {_ : Hashable α} [Inhabited β] : HashMap α β → α → β → β :=
+  %first_defined [Std.HashMap.getD, Lean.HashMap.findD]
+
+
+%if_bound GetElem?
+  instance [BEq α] [Hashable α] [Inhabited β] : GetElem? (HashMap α β) α β (fun m a => a ∈ m) :=
+    %first_succeeding [
+      inferInstanceAs (GetElem? (Std.HashMap α β) α β (fun m a => a ∈ m)),
+      @GetElem?.mk _ _ _ _ instGetElemHashMap (fun m a => m.get? a) (fun m a => m.get! a)
+    ]
+
+instance [BEq α] [Hashable α] : EmptyCollection (HashMap α β) := ⟨%first_succeeding [Std.HashMap.empty, Lean.HashMap.empty]⟩

src/examples/SubVerso/Examples/Slice.lean

@@ -11,8 +11,8 @@ import SubVerso.Compat
 import SubVerso.Examples.Slice.Attribute
 
 
-open Lean hiding Parsec
-open SubVerso.Compat (Parsec)
+open Lean hiding Parsec HashMap
+open SubVerso.Compat (Parsec HashMap)
 
 namespace SubVerso.Examples.Slice
 
@@ -160,7 +160,6 @@ private partial def removeRanges (env : Environment) (rngs : Array String.Range)
         pure <| .node info kind newSubs
     else pure stx
 
-
 private def getSlices (slices : Array SliceCommand) : Except String (HashMap String (Array String.Range)) := do
   let mut opened : HashMap String (String.Pos) := {}
   let mut closed : HashMap String (Array String.Range) := {}
@@ -170,8 +169,8 @@ private def getSlices (slices : Array SliceCommand) : Except String (HashMap Str
       if opened.contains name then .error s!"Slice '{name}' opened twice"
       else opened := opened.insert name rng.stop
     | .endRange name pos =>
-      if let some p := opened.find? name then
-        closed := closed.insert name <| closed.findD name #[] |>.push ⟨p, pos.start⟩
+      if let some p := opened[name]? then
+        closed := closed.insert name <| closed.getD name #[] |>.push ⟨p, pos.start⟩
         opened := opened.erase name
       else .error s!"Slice '{name}' not open"
   pure closed

src/highlighting/SubVerso/Highlighting/Code.lean

@@ -10,10 +10,12 @@ import Lean.Widget.TaggedText
 import SubVerso.Compat
 import SubVerso.Highlighting.Highlighted
 
-open Lean Elab
+open Lean hiding HashMap
+open Elab
 open Lean.Widget (TaggedText)
 open Lean.Widget
 open Lean.PrettyPrinter (InfoPerPos)
+open SubVerso.Compat (HashMap)
 
 initialize registerTraceClass `SubVerso.Highlighting.Code
 
@@ -73,7 +75,7 @@ structure State (α : Type u) where
 def State.init [BEq α] [Hashable α] : State α := {}
 
 def insert [Monad m] [MonadState (State α) m] [BEq α] [Hashable α] (x : α) : m Nat := do
-  if let some i := (← get).indices.find? x then
+  if let some i := (← get).indices[x]? then
     pure i
   else
     let i := (← get).contents.size
@@ -139,7 +141,7 @@ 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? (← Compat.mkRefIdentFVar id) then
+      if let some y := ids[(← Compat.mkRefIdentFVar id)]? then
         Compat.refIdentCase y
           (onFVar := fun x => do
             let ty ← instantiateMVars (← runMeta <| Meta.inferType expr)