feat: adaptations for leanprover/lean4#3210 (#98)

Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
Co-authored-by: Jannis Limperg <jannis@limperg.de>

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