feat: add evalMatch for tactics

src/Lean/Elab/Tactic.lean

@@ -9,3 +9,4 @@ import Lean.Elab.Tactic.ElabTerm
 import Lean.Elab.Tactic.Induction
 import Lean.Elab.Tactic.Generalize
 import Lean.Elab.Tactic.Injection
+import Lean.Elab.Tactic.Match

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -23,34 +23,38 @@ withRef stx $ liftTermElabM $ adaptReader (fun (ctx : Term.Context) => { ctx wit
   Term.synthesizeSyntheticMVars mayPostpone;
   instantiateMVars e
 
+def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (mayPostpone := false) : TacticM Expr := do
+e ← elabTerm stx expectedType? mayPostpone;
+ensureHasType expectedType? e
+
 @[builtinTactic «exact»] def evalExact : Tactic :=
 fun stx => match_syntax stx with
   | `(tactic| exact $e) => do
     (g, gs) ← getMainGoal;
     withMVarContext g $ do {
       decl ← getMVarDecl g;
-      val  ← elabTerm e decl.type;
-      val  ← ensureHasType decl.type val;
+      val  ← elabTermEnsuringType e decl.type;
       ensureHasNoMVars val;
       assignExprMVar g val
     };
     setGoals gs
   | _ => throwUnsupportedSyntax
 
+def refineCore (mvarId : MVarId) (stx : Syntax) (tagSuffix : Name) : TacticM (List MVarId) :=
+withMVarContext mvarId do
+  decl ← getMVarDecl mvarId;
+  val  ← elabTermEnsuringType stx decl.type;
+  assignExprMVar mvarId val;
+  newMVarIds ← getMVarsNoDelayed val;
+  let newMVarIds := newMVarIds.toList;
+  tagUntaggedGoals decl.userName tagSuffix newMVarIds;
+  pure newMVarIds
+
 @[builtinTactic «refine»] def evalRefine : Tactic :=
 fun stx => match_syntax stx with
   | `(tactic| refine $e) => do
     (g, gs) ← getMainGoal;
-    gs' ← withMVarContext g $ do {
-      decl ← getMVarDecl g;
-      val  ← elabTerm e decl.type;
-      val  ← ensureHasType decl.type val;
-      assignExprMVar g val;
-      gs'  ← getMVarsNoDelayed val;
-      let gs' := gs'.toList;
-      tagUntaggedGoals decl.userName `refine gs';
-      pure gs'
-    };
+    gs' ← refineCore g e `refine;
     setGoals (gs' ++ gs)
   | _ => throwUnsupportedSyntax
 

src/Lean/Elab/Tactic/Induction.lean

@@ -235,7 +235,7 @@ else do
     pure { recName := recName, altVars := altVars, altRHSs := altRHSs }
 
 -- Return true if `stx` is a term occurring in the RHS of the induction/cases tactic
-private def isTermRHS (rhs : Syntax) : Bool :=
+def isHoleRHS (rhs : Syntax) : Bool :=
 rhs.isOfKind `Lean.Parser.Term.namedHole || rhs.isOfKind `Lean.Parser.Term.hole
 
 private def processResult (altRHSs : Array Syntax) (result : Array Meta.InductionSubgoal) : TacticM Unit := do
@@ -251,10 +251,9 @@ else do
       let rhs     := altRHSs.get! i;
       let ref     := rhs;
       let mvarId  := subgoal.mvarId;
-      if isTermRHS rhs then withMVarContext mvarId $ withRef rhs do
+      if isHoleRHS rhs then withMVarContext mvarId $ withRef rhs do
         mvarDecl ← getMVarDecl mvarId;
-        val ← elabTerm rhs mvarDecl.type;
-        val ← ensureHasType mvarDecl.type val;
+        val ← elabTermEnsuringType rhs mvarDecl.type;
         assignExprMVar mvarId val;
         gs' ← getMVarsNoDelayed val;
         let gs' := gs'.toList;

src/Lean/Elab/Tactic/Match.lean

@@ -0,0 +1,48 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Elab.Match
+import Lean.Elab.Tactic.Basic
+import Lean.Elab.Tactic.Induction
+
+namespace Lean
+namespace Elab
+namespace Tactic
+
+private def mkAuxiliaryMatchTermAux (matchTac : Syntax) : StateT (Array Syntax) MacroM Syntax := do
+let alts := (matchTac.getArg 5).getArgs;
+newAlts ← alts.mapSepElemsM fun alt => do {
+  let alt    := alt.updateKind `Lean.Parser.Term.matchAlt;
+  let holeOrTactic := alt.getArg 2;
+  if isHoleRHS holeOrTactic then
+    pure alt
+  else withFreshMacroScope do
+    newHole ← `(?rhs);
+    let newHoleId := newHole.getArg 1;
+    newCase ← `(tactic| case $newHoleId $holeOrTactic);
+    modify fun cases => cases.push newCase;
+    pure $ alt.setArg 2 newHole
+};
+let result  := matchTac.updateKind `Lean.Parser.Term.match;
+let result  := result.setArg 5 (mkNullNode newAlts);
+pure result
+
+private def mkAuxiliaryMatchTerm (matchTac : Syntax) : MacroM (Syntax × Array Syntax) :=
+(mkAuxiliaryMatchTermAux matchTac).run #[]
+
+def mkTacticSeq (ref : Syntax) (tacs : Array Syntax) : Syntax :=
+let seq := mkSepStx tacs (mkAtomFrom ref "; ");
+Syntax.node `Lean.Parser.Tactic.seq #[seq]
+
+@[builtinTactic Lean.Parser.Tactic.match] def evalMatch : Tactic :=
+fun stx => do
+  (matchTerm, cases) ← liftMacroM $ mkAuxiliaryMatchTerm stx;
+  refineMatchTerm ← `(tactic| refine $matchTerm);
+  let stxNew := mkTacticSeq stx (#[refineMatchTerm] ++ cases);
+  withMacroExpansion stx stxNew $ evalTactic stxNew
+
+end Tactic
+end Elab
+end Lean

src/Lean/Parser/Tactic.lean

@@ -41,7 +41,8 @@ def ident' : Parser := ident <|> underscore
 @[builtinTacticParser] def «failIfSuccess» := parser! nonReservedSymbol "failIfSuccess " >> tacticParser
 @[builtinTacticParser] def «generalize» := parser! nonReservedSymbol "generalize" >> optional (try (ident >> " : ")) >> termParser 51 >> " = " >> ident
 def majorPremise := parser! optional (try (ident >> " : ")) >> termParser
-def inductionAlt  : Parser := nodeWithAntiquot "inductionAlt" `Lean.Parser.Tactic.inductionAlt $ ident' >> many ident' >> darrow >> (Term.hole <|> Term.namedHole <|> tacticParser)
+def holeOrTactic := Term.hole <|> Term.namedHole <|> tacticParser
+def inductionAlt  : Parser := nodeWithAntiquot "inductionAlt" `Lean.Parser.Tactic.inductionAlt $ ident' >> many ident' >> darrow >> holeOrTactic
 def inductionAlts : Parser := withPosition $ fun pos => "|" >> sepBy1 inductionAlt (checkColGe pos.column "alternatives must be indented" >> "|")
 def withAlts : Parser := optional (" with " >> inductionAlts)
 def usingRec : Parser := optional (" using " >> ident)
@@ -50,7 +51,7 @@ def generalizingVars := optional (" generalizing " >> many1 ident)
 @[builtinTacticParser] def «cases»      := parser! nonReservedSymbol "cases " >> majorPremise >> withAlts
 def withIds : Parser := optional (" with " >> many1 ident')
 
-def matchAlt  : Parser :=  group (sepBy1 termParser ", " >> darrow >> tacticParser)
+def matchAlt  : Parser := parser! sepBy1 termParser ", " >> darrow >> holeOrTactic
 def matchAlts : Parser := withPosition $ fun pos => (optional "| ") >> sepBy1 matchAlt (checkColGe pos.column "alternatives must be indented" >> "|")
 @[builtinTacticParser] def «match»      := parser! nonReservedSymbol "match " >> sepBy1 Term.matchDiscr ", " >> Term.optType >> " with " >> matchAlts
 @[builtinTacticParser] def «injection»  := parser! nonReservedSymbol "injection " >> termParser >> withIds

tests/lean/run/matchtac.lean

@@ -0,0 +1,23 @@
+new_frontend
+
+theorem tst1 {α : Type} {p : Prop} (xs : List α) (h₁ : (a : α) → (as : List α) → xs = a :: as → p) (h₂ : xs = [] → p) : p :=
+begin
+  match h:xs with
+  | []    => exact h₂ h
+  | z::zs => { apply h₁ z zs; assumption }
+end
+
+theorem tst2 {α : Type} {p : Prop} (xs : List α) (h₁ : (a : α) → (as : List α) → xs = a :: as → p) (h₂ : xs = [] → p) : p :=
+begin
+  match h:xs with
+  | []    => ?nilCase
+  | z::zs => ?consCase;
+  case consCase exact h₁ z zs h;
+  case nilCase exact h₂ h;
+end
+
+def tst3 {α β γ : Type} (h : α × β × γ) : β × α × γ :=
+begin
+  match h with
+  | (a, b, c) => exact (b, a, c)
+end