Use same DiscrTree config as simp for indexes (#184)

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 <$> (withConfigWithKey discrTreeConfig <| DiscrTree.mkPath (← p.toExpr))
+  withoutModifyingState do .hyps <$> mkDiscrTreePath (← p.toExpr)
 
 end CasesPattern
 

Aesop/Builder/Forward.lean

@@ -34,7 +34,7 @@ private def forwardIndexingModeCore (type : Expr)
       match args.get? i with
       | some arg =>
         let argT := (← arg.mvarId!.getDecl).type
-        let keys ← withConfigWithKey discrTreeConfig <| DiscrTree.mkPath argT
+        let keys ← mkDiscrTreePath argT
         return .hyps keys
       | none => throwError
         "aesop: internal error: immediate arg for forward rule is out of range"

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
-        withConfigWithKey discrTreeConfig <| DiscrTree.mkPath (← instantiateMVars e)
+        mkDiscrTreePath (← elabPattern stx)
 
 def IndexingMode.elab (stxs : Array Syntax) : ElabM IndexingMode :=
   .or <$> stxs.mapM elabSingleIndexingMode

Aesop/Index.lean

@@ -96,7 +96,7 @@ private def applicableByTargetRules (ri : Index α) (goal : MVarId)
     (include? : Rule α → Bool) :
     MetaM (Array (Rule α × Array IndexMatchLocation)) :=
   goal.withContext do
-    let rules ← withConfigWithKey discrTreeConfig <| ri.byTarget.getUnify (← goal.getType)
+    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
@@ -114,7 +114,7 @@ private def applicableByHypRules (ri : Index α) (goal : MVarId)
     for localDecl in ← getLCtx do
       if localDecl.isImplementationDetail then
         continue
-      let rules ← withConfigWithKey discrTreeConfig <| ri.byHyp.getUnify localDecl.type
+      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

@@ -35,7 +35,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

@@ -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/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
@@ -78,11 +79,10 @@ open DiscrTree
 
 -- For `type = ∀ (x₁, ..., xₙ), T`, returns keys that match `T * ... *` (with
 -- `n` stars).
-def getConclusionDiscrTreeKeys (type : Expr) (config : ConfigWithKey) :
-    MetaM (Array Key) :=
+def getConclusionDiscrTreeKeys (type : Expr) : MetaM (Array Key) :=
   withoutModifyingState do
     let (_, _, conclusion) ← forallMetaTelescope type
-    withConfigWithKey config <| mkPath conclusion
+    mkDiscrTreePath conclusion
     -- We use a meta telescope because `DiscrTree.mkPath` ignores metas (they
     -- turn into `Key.star`) but not fvars.