merge master

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
@@ -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

@@ -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,12 @@ open DiscrTree
 
 -- For `type = ∀ (x₁, ..., xₙ), T`, returns keys that match `T * ... *` (with
 -- `n` stars).
-def getConclusionDiscrTreeKeys (type : Expr) (config : ConfigWithKey) :
+
+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.
 

AesopTest/List.lean

@@ -892,7 +892,7 @@ theorem last_append (l₁ l₂ : List α) (h : l₂ ≠ []) :
   last (l₁ ++ l₂) (append_ne_nil_of_right_ne_nil l₁ h) = last l₂ h := by
   induction l₁ <;> aesop
 
-theorem last_concat {a : α} (l : List α) : last (concat l a) (concat_ne_nil a l) = a := by
+theorem last_concat {a : α} (l : List α) : last (concat l a) (by exact X.concat_ne_nil a l) = a := by
   aesop
 
 @[simp] theorem last_singleton (a : α) : last [a] (cons_ne_nil a []) = a := rfl

AesopTest/RulePattern.lean

@@ -44,8 +44,8 @@ axiom triangle (a b : Int) : |a + b| ≤ |a| + |b|
 
 example : |a + b| ≤ |c + d| := by
   aesop!
-  guard_hyp fwd_1 : |c + d| ≤ |c| + |d|
-  guard_hyp fwd   : |a + b| ≤ |a| + |b|
+  guard_hyp fwd   : |c + d| ≤ |c| + |d|
+  guard_hyp fwd_1 : |a + b| ≤ |a| + |b|
   falso
 
 @[aesop safe apply (pattern := (0 : Nat))]

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "13c202289cae0db69d997904de3c4d43c9222ea8",
+   "rev": "2e82cd8e5d6462f20ffd810ea0e9460475e0b455",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",