feat: adaptations for leanprover/lean4#3210

Aesop/Index.lean

@@ -14,8 +14,8 @@ open Lean.Meta
 namespace Aesop
 
 structure Index (α : Type) [BEq α] [Hashable α] where
-  byTarget : DiscrTree α 
-  byHyp : DiscrTree α 
+  byTarget : DiscrTree α
+  byHyp : DiscrTree α
   unindexed : PHashSet α
   deriving Inhabited
 

Aesop/Search/Expansion/Simp.lean

@@ -9,6 +9,7 @@ import Aesop.Script
 import Aesop.RuleSet
 
 open Lean Lean.Meta
+open Lean.Elab.Tactic (mkSimpOnly)
 open Simp (UsedSimps)
 
 namespace Aesop
@@ -48,7 +49,8 @@ def mkNormSimpOnlySyntax (inGoal : MVarId) (normSimpUseHyps : Bool)
     Elab.Tactic.mkSimpOnly originalStx usedTheorems
   return ⟨stx⟩
 
-def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs)
+def simpGoal (mvarId : MVarId) (ctx : Simp.Context)
+    (simprocs : Simp.SimprocsArray)
     (discharge? : Option Simp.Discharge := none)
     (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[])
     (usedSimps : UsedSimps := {}) : MetaM SimpResult := do
@@ -66,7 +68,8 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs)
     return .solved usedSimps
 
 def simpGoalWithAllHypotheses (mvarId : MVarId) (ctx : Simp.Context)
-    (simprocs : Simprocs := {}) (discharge? : Option Simp.Discharge := none)
+    (simprocs : Simp.SimprocsArray := {})
+    (discharge? : Option Simp.Discharge := none)
     (simplifyTarget : Bool := true) (usedSimps : UsedSimps := {}) :
     MetaM SimpResult :=
   mvarId.withContext do
@@ -79,7 +82,8 @@ def simpGoalWithAllHypotheses (mvarId : MVarId) (ctx : Simp.Context)
     Aesop.simpGoal mvarId ctx simprocs discharge? simplifyTarget fvarIdsToSimp
       usedSimps
 
-def simpAll (mvarId : MVarId) (ctx : Simp.Context) (simprocs : Simprocs := {})
+def simpAll (mvarId : MVarId) (ctx : Simp.Context)
+    (simprocs : Simp.SimprocsArray := {})
     (usedSimps : UsedSimps := {}) : MetaM SimpResult := do
   let ctx := { ctx with config.failIfUnchanged := false }
   match ← Lean.Meta.simpAll mvarId ctx simprocs usedSimps with

Aesop/Search/SearchM.lean

@@ -83,7 +83,6 @@ protected def run (ruleSet : RuleSet) (options : Aesop.Options')
   let t ← mkInitialTree goal
   let normSimpContext := {
     config := simpConfig
-    unfoldGround := simpConfig.ground
     maxDischargeDepth := UInt32.ofNatTruncate simpConfig.maxDischargeDepth
     simpTheorems := ruleSet.globalNormSimpTheorems
     congrTheorems := ← getSimpCongrTheorems

Aesop/Util/Tactic.lean

@@ -72,25 +72,24 @@ where
   -- is slow but correct.
   pre (e : Expr) : StateRefT (HashSet Name) SimpM Simp.Step := do
     let some decl := e.getAppFn'.constName?
-      | return .visit { expr := e }
+      | return .continue
     match unfold? decl with
     | none =>
-      return .visit { expr := e }
+      return .continue
     | some none =>
       if let some e' ← delta? e (λ n => n == decl) then
         modify (·.insert decl)
         return .done { expr := e' }
       else
-        return .visit { expr := e }
+        return .continue
     | some (some unfoldThm) =>
       let result? ← withReducible <|
         Simp.tryTheorem? e
           { origin := .decl unfoldThm
             proof := mkConst unfoldThm
             rfl := ← isRflTheorem unfoldThm }
-          (fun _ => return none)
       match result? with
-      | none   => return .visit { expr := e }
+      | none   => return .continue
       | some r =>
         modify (·.insert decl)
         match (← reduceMatcher? r.expr) with

AesopTest/List.lean

@@ -16,7 +16,6 @@ set_option aesop.check.script true
 -- use `sorry` because it generates lots of warnings.
 axiom ADMIT : ∀ {α : Sort _}, α
 
-@[aesop safe cases]
 class IsEmpty (α : Sort _) where
   false : α → False
 

lake-manifest.json

@@ -4,10 +4,10 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "f8258756d05d8232eaeb715e9f9bbebb9e06dbe7",
+   "rev": "efe7a0cbb3735244d2233ff55b06b6a40c287c67",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "bump/v4.6.0",
+   "inputRev": "fixes_3210",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "aesop",

lakefile.lean

@@ -13,4 +13,4 @@ lean_lib AesopTest {
   globs := #[.submodules "AesopTest"]
 }
 
-require std from git "https://github.com/leanprover/std4" @ "bump/v4.6.0"
+require std from git "https://github.com/leanprover/std4" @ "fixes_3210"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2024-01-23
+leanprover/lean4:nightly-2024-02-01