feat: add mkSimprocPatternFromExpr for creating patterns from expressions with metavariables

src/Lean/Meta/Sym/Pattern.lean

@@ -17,6 +17,7 @@ import Lean.Meta.Sym.ProofInstInfo
 import Lean.Meta.Sym.AlphaShareBuilder
 import Lean.Meta.Sym.Offset
 import Lean.Meta.Sym.Eta
+import Lean.Meta.AbstractMVars
 import Init.Data.List.MapIdx
 import Init.Data.Nat.Linear
 import Std.Do.Triple.Basic
@@ -260,6 +261,45 @@ public def mkEqPatternFromDecl (declName : Name) : MetaM (Pattern × Expr) := do
     let_expr Eq _ lhs rhs := type | throwError "conclusion is not a equality{indentExpr type}"
     return (lhs, rhs)
 
+/--
+Like `mkPatternCore` but takes a lambda expression instead of a forall type.
+Uses `lambdaBoundedTelescope` to open binders and detect instance/proof arguments.
+-/
+def mkPatternCoreFromLambda (lam : Expr) (levelParams : List Name)
+    (varTypes : Array Expr) (pattern : Expr) : MetaM Pattern := do
+  let fnInfos ← mkProofInstInfoMapFor pattern
+  let checkTypeMask := mkCheckTypeMask pattern varTypes.size
+  let checkTypeMask? := if checkTypeMask.all (· == false) then none else some checkTypeMask
+  let varInfos? ← lambdaBoundedTelescope lam varTypes.size fun xs _ =>
+    mkProofInstArgInfo? xs
+  return { levelParams, varTypes, pattern, fnInfos, varInfos?, checkTypeMask? }
+
+def mkPatternFromLambda (levelParams : List Name) (lam : Expr) : MetaM Pattern := do
+  let rec go (pattern : Expr) (varTypes : Array Expr) : MetaM Pattern := do
+    if let .lam _ d b _ := pattern then
+      return (← go b (varTypes.push d))
+    let pattern ← preprocessType pattern
+    mkPatternCoreFromLambda lam levelParams varTypes pattern
+  go lam #[]
+
+/--
+Creates a `Pattern` from an expression containing metavariables.
+
+Metavariables in `e` become pattern variables (wildcards). For example,
+`Nat.succ ?m` produces a pattern matching `Nat.succ _` with discrimination
+tree keys `[Nat.succ, *]`.
+
+This is used for user-registered simproc patterns where the user provides
+an expression with underscores (elaborated as metavariables) to specify
+what the simproc should match.
+-/
+public def mkSimprocPatternFromExpr (e : Expr) : MetaM Pattern := do
+  let result ← abstractMVars e
+  let levelParams := result.paramNames.mapIdx fun i _ => Name.num uvarPrefix i
+  let us := levelParams.toList.map mkLevelParam
+  let expr := result.expr.instantiateLevelParamsArray result.paramNames us.toArray
+  mkPatternFromLambda levelParams.toList expr
+
 structure UnifyM.Context where
   pattern   : Pattern
   unify     : Bool := true

tests/elab/pattern.lean

@@ -0,0 +1,31 @@
+import Lean
+
+open Lean
+open Lean.Meta
+open Lean.Meta.Sym
+open Lean.Meta.Sym.Simp
+
+/--
+trace: [Meta.Tactic] Adding: Nat.succ ?m.1 to the discrimination tree
+[Meta.Tactic] Generated keys: [Nat.succ, *]
+[Meta.Tactic] We will try to retrieve: Nat.succ 42
+[Meta.Tactic] Normal match result: [true]
+[Meta.Tactic] overapplied match result: [(true, 0)]
+-/
+#guard_msgs in
+set_option trace.Meta.Tactic true in
+#eval show MetaM Unit from do
+  let natMVar ← mkFreshExprMVar (mkConst ``Nat)
+  let exprToAdd := mkApp (mkConst ``Nat.succ) natMVar
+  trace[Meta.Tactic] "Adding: {exprToAdd} to the discrimination tree"
+  let pattern ← mkSimprocPatternFromExpr exprToAdd
+  let keys := pattern.mkDiscrTreeKeys
+  trace[Meta.Tactic] "Generated keys: {keys}"
+  let d : DiscrTree Bool := {}
+  let d := d.insertKeyValue keys true
+  let exprToAdd := mkApp (mkConst ``Nat.succ) (mkNatLit 42)
+  trace[Meta.Tactic] "We will try to retrieve: {exprToAdd}"
+  let normalMatch ← d.getMatch exprToAdd
+  trace[Meta.Tactic] "Normal match result: {normalMatch}"
+  let matchWithExtra ← d.getMatchWithExtra exprToAdd
+  trace[Meta.Tactic] "overapplied match result: {matchWithExtra}"