Merge remote-tracking branch 'origin/master' into forward-code

Aesop/Builder/Cases.lean

@@ -21,8 +21,7 @@ def check (decl : Name) (p : CasesPattern) : MetaM Unit :=
       throwError "expected pattern '{p}' ({toString p}) to be an application of '{decl}'"
 
 def toIndexingMode (p : CasesPattern) : MetaM IndexingMode :=
-  withoutModifyingState do
-    .hyps <$> DiscrTree.mkPath (← p.toExpr) discrTreeConfig
+  withoutModifyingState do .hyps <$> mkDiscrTreePath (← p.toExpr)
 
 end CasesPattern
 

Aesop/Builder/Forward.lean

@@ -33,7 +33,7 @@ def getForwardIndexingMode (type : Expr)
       match args.get? i with
       | some arg =>
         let argT := (← arg.mvarId!.getDecl).type
-        let keys ← DiscrTree.mkPath argT discrTreeConfig
+        let keys ← mkDiscrTreePath argT
         return .hyps keys
       | none => throwError
         "aesop: internal error: immediate arg for forward rule is out of range"
@@ -50,7 +50,7 @@ def getImmediatePremises  (type : Expr) (pat? : Option RulePattern) :
       for h : i in [:args.size] do
         if isPatternInstantiated i then
           continue
-        let fvarId := (args[i]'h.2).fvarId!
+        let fvarId := args[i].fvarId!
         let ldecl ← fvarId.getDecl
         let isNondep : MetaM Bool :=
           args.allM (start := i + 1) λ arg => do

Aesop/Forward/RuleInfo.lean

@@ -94,7 +94,7 @@ def ofExpr (thm : Expr) (rulePattern? : Option RulePattern)
   let mut allDeps : Std.HashSet PremiseIndex := ∅
   for h : i in [:premises.size] do
     let mvarId := premises[i]
-    let typeDiscrTreeKeys ← DiscrTree.mkPath (← mvarId.getType) discrTreeConfig
+    let typeDiscrTreeKeys ← mkDiscrTreePath (← mvarId.getType)
     let mut deps : Std.HashSet PremiseIndex := ∅
     for dep in ← mvarId.getMVarDependencies do
       if let some idx := premiseToIdx[dep]? then

Aesop/Forward/Substitution.lean

@@ -141,7 +141,7 @@ def specializeRule (rule : Expr) (subst : Substitution) : MetaM Expr :=
         if let some inst := subst.find? ⟨i⟩ then
           args := args.push $ some inst.toExpr
         else
-          let fvarId := fvarIds[i]'h.2
+          let fvarId := fvarIds[i]
           args := args.push $ some fvarId
           remainingFVarIds := remainingFVarIds.push fvarId
       let result ← mkLambdaFVars remainingFVarIds (← mkAppOptM' rule args)

Aesop/Frontend/RuleExpr.lean

@@ -172,8 +172,7 @@ def elabSingleIndexingMode (stx : Syntax) : ElabM IndexingMode :=
   where
     elabKeys (stx : Syntax) : ElabM (Array DiscrTree.Key) :=
       show TermElabM _ from withoutModifyingState do
-        let e ← elabPattern stx
-        DiscrTree.mkPath (← instantiateMVars e) discrTreeConfig
+        mkDiscrTreePath (← elabPattern stx)
 
 def IndexingMode.elab (stxs : Array Syntax) : ElabM IndexingMode :=
   .or <$> stxs.mapM elabSingleIndexingMode
@@ -315,6 +314,8 @@ inductive Feature
 
 namespace Feature
 
+-- Workaround for codegen bug, see #182
+set_option compiler.extract_closed false in
 partial def «elab» (stx : Syntax) : ElabM Feature :=
   withRef stx do
     match stx with
@@ -330,7 +331,7 @@ partial def «elab» (stx : Syntax) : ElabM Feature :=
         let nonIdentAlts :=
           stx.getArgs.filter λ stx => ! stx.isOfKind ``Parser.featIdent
         if h : nonIdentAlts.size = 1 then
-          return ← «elab» $ nonIdentAlts[0]'(by simp [h])
+          return ← «elab» $ nonIdentAlts[0]
       throwUnsupportedSyntax
 
 end Feature

Aesop/Index.lean

@@ -98,7 +98,7 @@ private def applicableByTargetRules (ri : Index α) (goal : MVarId)
     (include? : Rule α → Bool) :
     MetaM (Array (Rule α × Array IndexMatchLocation)) :=
   goal.withContext do
-    let rules ← ri.byTarget.getUnify (← goal.getType) discrTreeConfig
+    let rules ← getUnify ri.byTarget (← goal.getType)
     let mut rs := Array.mkEmpty rules.size
       -- Assumption: include? is true for most rules.
     for r in rules do
@@ -116,7 +116,7 @@ private def applicableByHypRules (ri : Index α) (goal : MVarId)
     for localDecl in ← getLCtx do
       if localDecl.isImplementationDetail then
         continue
-      let rules ← ri.byHyp.getUnify localDecl.type discrTreeConfig
+      let rules ← getUnify ri.byHyp localDecl.type
       for r in rules do
         if include? r then
           rs := rs.push (r, #[.hyp localDecl])

Aesop/Index/Basic.lean

@@ -31,7 +31,7 @@ instance : ToFormat IndexingMode :=
   ⟨IndexingMode.format⟩
 
 def targetMatchingConclusion (type : Expr) : MetaM IndexingMode := do
-  let path ← getConclusionDiscrTreeKeys type discrTreeConfig
+  let path ← getConclusionDiscrTreeKeys type
   return target path
 
 def hypsMatchingConst (decl : Name) : MetaM IndexingMode := do

Aesop/Index/DiscrKeyConfig.lean

@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2024 Jannis Limperg. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jannis Limperg
+-/
+
+import Lean
+
+open Lean Lean.Meta
+
+namespace Aesop
+
+/-- The configuration used by all Aesop indices. -/
+-- I don't really know what I'm doing here. I'm just copying the config used
+-- by `simp`; see `Meta/Simp/Types.lean:mkIndexConfig`.
+def indexConfig : ConfigWithKey :=
+  ({ proj := .no, transparency := .reducible : Config }).toConfigWithKey
+
+def mkDiscrTreePath (e : Expr) : MetaM (Array DiscrTree.Key) :=
+  withConfigWithKey indexConfig $ DiscrTree.mkPath e
+
+def getUnify (t : DiscrTree α) (e : Expr) : MetaM (Array α) :=
+  withConfigWithKey indexConfig $ t.getUnify e
+
+def getMatch (t : DiscrTree α) (e : Expr) : MetaM (Array α) :=
+  withConfigWithKey indexConfig $ t.getMatch e
+
+end Aesop

Aesop/Index/DiscrTreeConfig.lean

@@ -1,16 +1,28 @@
 /-
-Copyright (c) 2021 Jannis Limperg. All rights reserved.
+Copyright (c) 2021-2024 Jannis Limperg. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
 
 import Lean
 
-open Lean.Meta
-
 namespace Aesop
 
-/-- Discrimination tree configuration used by all Aesop indices. -/
-def discrTreeConfig : WhnfCoreConfig := { iota := false }
+open Lean Lean.Meta
+
+/-- The configuration used by all Aesop indices. -/
+-- I don't really know what I'm doing here. I'm just copying the config used
+-- by `simp`; see `Meta/Simp/Types.lean:mkIndexConfig`.
+def indexConfig : ConfigWithKey :=
+  ({ proj := .no, transparency := .reducible : Config }).toConfigWithKey
+
+def mkDiscrTreePath (e : Expr) : MetaM (Array DiscrTree.Key) :=
+  withConfigWithKey indexConfig $ DiscrTree.mkPath e
+
+def getUnify (t : DiscrTree α) (e : Expr) : MetaM (Array α) :=
+  withConfigWithKey indexConfig $ t.getUnify e
+
+def getMatch (t : DiscrTree α) (e : Expr) : MetaM (Array α) :=
+  withConfigWithKey indexConfig $ t.getMatch e
 
 end Aesop

Aesop/Index/Forward.lean

@@ -72,7 +72,7 @@ Each returned pair `(r, i)` contains a rule `r` and the index `i` of the premise
 of `r` that likely unifies with `e`. -/
 def get (idx : ForwardIndex) (e : Expr) :
     MetaM (Array (ForwardRule × PremiseIndex)) :=
-  idx.tree.getUnify e discrTreeConfig
+  getUnify idx.tree e
 
 /-- Get the forward rule with the given rule name. -/
 def getRuleWithName? (n : RuleName) (idx : ForwardIndex) : Option ForwardRule :=

Aesop/Index/RulePattern.lean

@@ -81,7 +81,7 @@ section Get
 /-- Get rule pattern substitutions for the patterns that match `e`. -/
 def getSingle (e : Expr) (idx : RulePatternIndex) :
     BaseM (Array (RuleName × Substitution)) := do
-  let ms ← idx.tree.getUnify e discrTreeConfig
+  let ms ← getUnify idx.tree e
   ms.filterMapM λ { name := r, pattern } => do
     let some subst ← pattern.match e
       | return none

Aesop/RulePattern.lean

@@ -104,7 +104,7 @@ def «elab» (stx : Term) (rule : Expr) : TermElabM RulePattern :=
     forallTelescope (← inferType rule) λ fvars _ => do
       let pat := (← elabPattern stx).consumeMData
       let (pat, mvarIds) ← fvarsToMVars fvars pat
-      let discrTreeKeys ← DiscrTree.mkPath pat discrTreeConfig
+      let discrTreeKeys ← mkDiscrTreePath pat
       let (pat, mvarIdToPatternPos, lmvarIdToPatternPos) ← abstractMVars' pat
       let argMap := mvarIds.map (mvarIdToPatternPos[·]?)
       let levelArgMap := lmvarIds.map (lmvarIdToPatternPos[·]?)

Aesop/RuleSet.lean

@@ -415,23 +415,23 @@ def LocalRuleSet.erase (rs : LocalRuleSet) (f : RuleFilter) :
       Σ' a : Array (Name × SimpTheorems), a.size = rs.simpTheoremsArray.size :=
     ⟨rs.simpTheoremsArray, rfl⟩
   if let some id := f.matchesLocalNormSimpRule? then
-    if let some idx := localNormSimpRules.findIdx? (·.id == id) then
+    if let some idx := localNormSimpRules.findFinIdx? (·.id == id) then
       localNormSimpRules := localNormSimpRules.eraseIdx idx
   if let some decl := f.matchesSimpTheorem? then
     for h : i in [:rs.simpTheoremsArray.size] do
       have i_valid : i < simpTheoremsArray'.fst.size := by
-        simp_all [Membership.mem, simpTheoremsArray'.snd]
+        simp_all +zetaDelta [Membership.mem, simpTheoremsArray'.snd]
       let (name, simpTheorems) := simpTheoremsArray'.fst[i]
       if SimpTheorems.containsDecl simpTheorems decl then
         let origin := .decl decl (inv := false)
         simpTheoremsArray' :=
-          ⟨simpTheoremsArray'.fst.set ⟨i, i_valid⟩
+          ⟨simpTheoremsArray'.fst.set i
             (name, simpTheorems.eraseCore origin),
            by simp [simpTheoremsArray'.snd, Array.size_set]⟩
         anyErased := true
   let simpTheoremsArray := simpTheoremsArray'.fst
   let simpTheoremsArrayNonempty : 0 < simpTheoremsArray.size := by
-    simp [simpTheoremsArray'.snd, rs.simpTheoremsArrayNonempty]
+    simp [simpTheoremsArray, simpTheoremsArray'.snd, rs.simpTheoremsArrayNonempty]
   let rs := { rs with
     localNormSimpRules, simpTheoremsArray, simpTheoremsArrayNonempty
   }

Aesop/RuleTac/ElabRuleTerm.lean

@@ -81,7 +81,7 @@ def elabRuleTermForSimpCore (goal : MVarId) (term : Term) (ctx : Simp.Context)
     elabSimpTheorems (mkSimpArgs term) ctx simprocs isSimpAll
 
 def checkElabRuleTermForSimp (term : Term) (isSimpAll : Bool) : ElabM Unit := do
-  let ctx := { simpTheorems := #[{}] }
+  let ctx ← Simp.mkContext (simpTheorems := #[{}] )
   let simprocs := #[{}]
   discard $ elabRuleTermForSimpCore (← read).goal term ctx simprocs isSimpAll
 

Aesop/RuleTac/Tactic.lean

@@ -7,9 +7,8 @@ Authors: Jannis Limperg, Kaiyu Yang
 import Aesop.RuleTac.Basic
 import Aesop.Script.Step
 
-open Lean
-open Lean.Meta
-open Lean.Elab.Tactic (TacticM evalTactic run)
+open Lean Lean.Meta Lean.Elab.Tactic
+open Lean.Elab.Tactic (TacticM evalTactic withoutRecover)
 
 namespace Aesop.RuleTac
 
@@ -51,7 +50,8 @@ kind `tactic` or `tacticSeq`.
 def tacticStx (stx : Syntax) : RuleTac :=
   SingleRuleTac.toRuleTac λ input => do
     let preState ← saveState
-    let postGoals := (← run input.goal (evalTactic stx) |>.run').toArray
+    let tac := withoutRecover $ evalTactic stx
+    let postGoals := (← Elab.Tactic.run input.goal tac |>.run').toArray
     let postState ← saveState
     let tacticBuilder : Script.TacticBuilder := do
       if stx.isOfKind `tactic then

Aesop/Script/StructureDynamic.lean

@@ -60,7 +60,7 @@ def DynStructureM.run (x : DynStructureM α) (script : UScript) :
     MetaM (α × Bool) := do
   let mut steps : PHashMap MVarId (Nat × Step) := {}
   for h : i in [:script.size] do
-    let step := script[i]'h.2
+    let step := script[i]
     steps := steps.insert step.preGoal (i, step)
   let (a, s) ← ReaderT.run x { steps } |>.run {}
   return (a, s.perfect)

Aesop/Script/StructureStatic.lean

@@ -22,7 +22,7 @@ protected def StaticStructureM.run (script : UScript) (x : StaticStructureM α)
     CoreM (α × Bool) := do
   let mut steps : Std.HashMap MVarId (Nat × Step) := Std.HashMap.empty script.size
   for h : i in [:script.size] do
-    let step := script[i]'h.2
+    let step := script[i]
     if h : step.postGoals.size = 1 then
       if step.postGoals[0].goal == step.preGoal then
         continue

Aesop/Script/Util.lean

@@ -18,7 +18,7 @@ def findFirstStep? {α β : Type} (goals : Array α) (step? : α → Option β)
      (stepOrder : β → Nat) : Option (Nat × α × β) := Id.run do
   let mut firstStep? := none
   for h : pos in [:goals.size] do
-    let g := goals[pos]'h.2
+    let g := goals[pos]
     if let some step := step? g then
       if let some (_, _, currentFirstStep) := firstStep? then
         if stepOrder step < stepOrder currentFirstStep then

Aesop/Search/Expansion.lean

@@ -69,7 +69,7 @@ def addRapps (parentRef : GoalRef) (rule : RegularRule)
   let mut rrefs := Array.mkEmpty rapps.size
   let mut subgoals := Array.mkEmpty $ rapps.size * 3
   for h : i in [:rapps.size] do
-    let rapp := rapps[i]'h.2
+    let rapp := rapps[i]
     let successProbability :=
       parent.successProbability *
       (rapp.successProbability?.getD rule.successProbability)

Aesop/Search/Expansion/Simp.lean

@@ -44,7 +44,7 @@ def addLetDeclsToSimpTheorems (ctx : Simp.Context) : MetaM Simp.Context := do
     if ldecl.hasValue && ! ldecl.isImplementationDetail then
       simpTheoremsArray := simpTheoremsArray.modify 0 λ simpTheorems =>
         simpTheorems.addLetDeclToUnfold ldecl.fvarId
-  return { ctx with simpTheorems := simpTheoremsArray }
+  return ctx.setSimpTheorems simpTheoremsArray
 
 def addLetDeclsToSimpTheoremsUnlessZetaDelta (ctx : Simp.Context) :
     MetaM Simp.Context := do
@@ -58,7 +58,7 @@ def simpGoal (mvarId : MVarId) (ctx : Simp.Context)
     (simplifyTarget : Bool := true) (fvarIdsToSimp : Array FVarId := #[])
     (stats : Simp.Stats := {}) : MetaM SimpResult := do
   let mvarIdOld := mvarId
-  let ctx := { ctx with config.failIfUnchanged := false }
+  let ctx := ctx.setFailIfUnchanged false
   let (result, { usedTheorems := usedSimps, .. }) ←
     Meta.simpGoal mvarId ctx simprocs discharge? simplifyTarget fvarIdsToSimp
       stats
@@ -89,7 +89,7 @@ def simpAll (mvarId : MVarId) (ctx : Simp.Context)
     (simprocs : Simp.SimprocsArray) (stats : Simp.Stats := {}) :
     MetaM SimpResult :=
   mvarId.withContext do
-    let ctx := { ctx with config.failIfUnchanged := false }
+    let ctx := ctx.setFailIfUnchanged false
     let ctx ← addLetDeclsToSimpTheoremsUnlessZetaDelta ctx
     match ← Lean.Meta.simpAll mvarId ctx simprocs stats with
     | (none, stats) => return .solved stats.usedTheorems

Aesop/Search/SearchM.lean

@@ -15,7 +15,8 @@ open Lean.Meta
 
 namespace Aesop
 
-structure NormSimpContext extends Simp.Context where
+structure NormSimpContext where
+  toContext : Simp.Context
   enabled : Bool
   useHyps : Bool
   configStx? : Option Term
@@ -84,10 +85,8 @@ protected def run (ruleSet : LocalRuleSet) (options : Aesop.Options')
     BaseM (α × State Q × Tree × Stats) := do
   let t ← mkInitialTree goal ruleSet
   let normSimpContext := {
-    config := simpConfig
-    maxDischargeDepth := UInt32.ofNatTruncate simpConfig.maxDischargeDepth
-    simpTheorems := ruleSet.simpTheoremsArray.map (·.snd)
-    congrTheorems := ← getSimpCongrTheorems
+    toContext := ← Simp.mkContext simpConfig (simpTheorems := ruleSet.simpTheoremsArray.map (·.snd))
+      (congrTheorems := ← getSimpCongrTheorems)
     simprocs := ruleSet.simprocsArray.map (·.snd)
     configStx? := simpConfigStx?
     enabled := options.enableSimp

Aesop/Tree/TreeM.lean

@@ -108,7 +108,7 @@ def getRootGoal : TreeM GoalRef := do
   let cref ← getRootMVarCluster
   let grefs := (← cref.get).goals
   if h : grefs.size = 1 then
-    return grefs.get ⟨0, by simp [h]⟩
+    return grefs[0]
   else
     throwError "aesop: internal error: unexpected number of goals in root mvar cluster: {grefs.size}"
 

Aesop/Util/Basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg, Asta Halkjær From
 -/
 
+import Aesop.Index.DiscrTreeConfig
 import Aesop.Nanos
 import Aesop.Util.UnorderedArraySet
 import Batteries.Lean.Expr
@@ -77,18 +78,18 @@ open DiscrTree
 
 -- For `type = ∀ (x₁, ..., xₙ), T`, returns keys that match `T * ... *` (with
 -- `n` stars).
-def getConclusionDiscrTreeKeys (type : Expr) (config : WhnfCoreConfig) :
-    MetaM (Array Key) :=
+
+def getConclusionDiscrTreeKeys (type : Expr) : MetaM (Array Key) :=
   withoutModifyingState do
     let (_, _, conclusion) ← forallMetaTelescope type
-    mkPath conclusion config
+    mkDiscrTreePath conclusion
     -- We use a meta telescope because `DiscrTree.mkPath` ignores metas (they
     -- turn into `Key.star`) but not fvars.
 
 -- For a constant `d` with type `∀ (x₁, ..., xₙ), T`, returns keys that
 -- match `d * ... *` (with `n` stars).
 def getConstDiscrTreeKeys (decl : Name) : MetaM (Array Key) := do
-  let arity := (← getConstInfo decl).type.forallArity
+  let arity := (← getConstInfo decl).type.getNumHeadForalls
   let mut keys := Array.mkEmpty (arity + 1)
   keys := keys.push $ .const decl arity
   for _ in [0:arity] do
@@ -116,7 +117,7 @@ private partial def filterTrieM [Monad m] [Inhabited σ] (f : σ → α → m σ
       if h : i < children.size then
         let (key, t) := children[i]'h
         let (t, acc) ← filterTrieM f p acc t
-        go acc (i + 1) (children.set ⟨i, h⟩ (key, t))
+        go acc (i + 1) (children.set i (key, t))
       else
         return (children, acc)
 

Aesop/Util/Tactic/Unfold.lean

@@ -14,12 +14,7 @@ namespace Aesop
 -- Lean.Meta.unfoldLocalDecl.
 
 def mkUnfoldSimpContext : MetaM Simp.Context := do
-  return {
-    simpTheorems := #[]
-    congrTheorems := ← getSimpCongrTheorems
-    config := Simp.neutralConfig
-    dischargeDepth := 0
-  }
+  Simp.mkContext Simp.neutralConfig (simpTheorems := #[]) (congrTheorems := ← getSimpCongrTheorems)
 
 @[inline]
 def unfoldManyCore (ctx : Simp.Context) (unfold? : Name → Option (Option Name))