Pantograph/Delate.lean

@@ -66,7 +66,7 @@ def exprProjToApp (env: Environment) (e: Expr): Expr :=
 def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _
 
 /-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
-@[export pantograph_unfold_aux_lemmas]
+@[export pantograph_unfold_aux_lemmas_m]
 def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
   Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
 
@@ -164,6 +164,13 @@ Convert an expression to an equiavlent form with
 def instantiateAll (e: Expr): MetaM Expr := do
   let e ← instantiateDelayedMVars e
   let e ← unfoldAuxLemmas e
+  let e ← Core.transform e λ e' => do
+    match ← Meta.matchMatcherApp? e' with
+    | .none => return .continue e'
+    | .some mapp =>
+      let .some matcherInfo := (← getEnv).find? mapp.matcherName | panic! "Matcher must exist"
+      let f ← Meta.instantiateValueLevelParams matcherInfo mapp.matcherLevels.toList
+      return .visit (f.betaRev e'.getAppRevArgs (useZeta := true))
   return e
 
 structure DelayedMVarInvocation where

Test/Common.lean

@@ -108,7 +108,7 @@ def strToTermSyntax (s: String): CoreM Syntax := do
     (input := s)
     (fileName := ← getFileName) | panic! s!"Failed to parse {s}"
   return stx
-def parseSentence (s: String): Elab.TermElabM Expr := do
+def parseSentence (s : String) (expectedType? : Option Expr := .none) : Elab.TermElabM Expr := do
   let stx ← match Parser.runParserCategory
     (env := ← MonadEnv.getEnv)
     (catName := `term)
@@ -116,7 +116,7 @@ def parseSentence (s: String): Elab.TermElabM Expr := do
     (fileName := ← getFileName) with
     | .ok syn => pure syn
     | .error error => throwError "Failed to parse: {error}"
-  Elab.Term.elabTerm (stx := stx) .none
+  Elab.Term.elabTerm (stx := stx) expectedType?
 
 def runTacticOnMVar (tacticM: Elab.Tactic.TacticM Unit) (goal: MVarId): Elab.TermElabM (List MVarId) := do
     let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }

Test/Delate.lean

@@ -3,10 +3,9 @@ import Pantograph.Delate
 import Test.Common
 import Lean
 
-open Lean
+open Lean Pantograph
-namespace Pantograph.Test.Delate
 
-open Pantograph
+namespace Pantograph.Test.Delate
 
 deriving instance Repr, DecidableEq for Protocol.BoundExpression
 
@@ -113,6 +112,13 @@ def test_projection_exists (env: Environment) : IO LSpec.TestSeq:= runTest do
   checkEq "numParams" numParams 2
   checkEq "numFields" numFields 2
 
+def test_matcher : TestT Elab.TermElabM Unit := do
+  let t ← parseSentence "Nat → Nat"
+  let e ← parseSentence "fun (n : Nat) => match n with | 0 => 0 | k => k" (.some t)
+  let .some _ ← Meta.matchMatcherApp? e.bindingBody! | fail "Must be a matcher app"
+  let e' ← instantiateAll e
+  checkTrue "ok" <| ← Meta.isTypeCorrect e'
+
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [
     ("serializeName", do pure test_serializeName),
@@ -123,6 +129,7 @@ def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
     ("Instance", test_instance env),
     ("Projection Prod", test_projection_prod env),
     ("Projection Exists", test_projection_exists env),
+    ("Matcher", runTestTermElabM env test_matcher),
   ]
 
 end Pantograph.Test.Delate