From 8f9fa8d04cecee324120ed73818cb63bf8056894 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 28 Jun 2021 10:08:42 -0700 Subject: [PATCH] refactor: add `BuiltinTactic.lean` --- src/Lean/Elab/Tactic.lean | 1 + src/Lean/Elab/Tactic/Basic.lean | 252 ----------------------- src/Lean/Elab/Tactic/BuiltinTactic.lean | 263 ++++++++++++++++++++++++ 3 files changed, 264 insertions(+), 252 deletions(-) create mode 100644 src/Lean/Elab/Tactic/BuiltinTactic.lean diff --git a/src/Lean/Elab/Tactic.lean b/src/Lean/Elab/Tactic.lean index ee1081c5a8..fb800b76a5 100644 --- a/src/Lean/Elab/Tactic.lean +++ b/src/Lean/Elab/Tactic.lean @@ -13,3 +13,4 @@ import Lean.Elab.Tactic.Match import Lean.Elab.Tactic.Rewrite import Lean.Elab.Tactic.Location import Lean.Elab.Tactic.Simp +import Lean.Elab.Tactic.BuiltinTactic diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index 967a0b0427..2fdd00d44b 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -341,9 +341,6 @@ def closeMainGoal (val : Expr) (checkUnassigned := true): TacticM Unit := do let gs ← tactic mvarId pure ((), gs) -@[builtinTactic Lean.Parser.Tactic.«done»] def evalDone : Tactic := fun _ => - done - def tryTactic? (tactic : TacticM α) : TacticM (Option α) := do try pure (some (← tactic)) @@ -378,156 +375,10 @@ def tagUntaggedGoals (parentTag : Name) (newSuffix : Name) (newGoals : List MVar idx := idx + 1 pure mctx -@[builtinTactic seq1] def evalSeq1 : Tactic := fun stx => do - let args := stx[0].getArgs - for i in [:args.size] do - if i % 2 == 0 then - evalTactic args[i] - else - saveTacticInfoForToken args[i] -- add `TacticInfo` node for `;` - -@[builtinTactic paren] def evalParen : Tactic := fun stx => - evalTactic stx[1] - -/- Evaluate `many (group (tactic >> optional ";")) -/ -private def evalManyTacticOptSemi (stx : Syntax) : TacticM Unit := do - stx.forArgsM fun seqElem => do - evalTactic seqElem[0] - saveTacticInfoForToken seqElem[1] -- add TacticInfo node for `;` - -@[builtinTactic tacticSeq1Indented] def evalTacticSeq1Indented : Tactic := fun stx => - evalManyTacticOptSemi stx[0] - -@[builtinTactic tacticSeqBracketed] def evalTacticSeqBracketed : Tactic := fun stx => do - let initInfo ← mkInitialTacticInfo stx[0] - withRef stx[2] <| closeUsingOrAdmit do - -- save state before/after entering focus on `{` - withInfoContext (pure ()) initInfo - evalManyTacticOptSemi stx[1] - -@[builtinTactic Parser.Tactic.focus] def evalFocus : Tactic := fun stx => do - let mkInfo ← mkInitialTacticInfo stx[0] - focus do - -- show focused state on `focus` - withInfoContext (pure ()) mkInfo - evalTactic stx[1] - -private def getOptRotation (stx : Syntax) : Nat := - if stx.isNone then 1 else stx[0].toNat - -@[builtinTactic Parser.Tactic.rotateLeft] def evalRotateLeft : Tactic := fun stx => do - let n := getOptRotation stx[1] - setGoals <| (← getGoals).rotateLeft n - -@[builtinTactic Parser.Tactic.rotateRight] def evalRotateRight : Tactic := fun stx => do - let n := getOptRotation stx[1] - setGoals <| (← getGoals).rotateRight n - -@[builtinTactic Parser.Tactic.open] def evalOpen : Tactic := fun stx => do - try - pushScope - let openDecls ← elabOpenDecl stx[1] - withTheReader Core.Context (fun ctx => { ctx with openDecls := openDecls }) do - evalTactic stx[3] - finally - popScope - -@[builtinTactic Parser.Tactic.set_option] def elabSetOption : Tactic := fun stx => do - let options ← Elab.elabSetOption stx[1] stx[2] - withTheReader Core.Context (fun ctx => { ctx with maxRecDepth := maxRecDepth.get options, options := options }) do - evalTactic stx[4] - -@[builtinTactic Parser.Tactic.allGoals] def evalAllGoals : Tactic := fun stx => do - let mvarIds ← getGoals - let mut mvarIdsNew := #[] - for mvarId in mvarIds do - unless (← isExprMVarAssigned mvarId) do - setGoals [mvarId] - try - evalTactic stx[1] - mvarIdsNew := mvarIdsNew ++ (← getUnsolvedGoals) - catch ex => - logException ex - mvarIdsNew := mvarIdsNew.push mvarId - setGoals mvarIdsNew.toList - -@[builtinTactic tacticSeq] def evalTacticSeq : Tactic := fun stx => - evalTactic stx[0] - -partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit := - if h : i < tactics.size then - let tactic := tactics.get ⟨i, h⟩ - catchInternalId unsupportedSyntaxExceptionId - (evalTactic tactic) - (fun _ => evalChoiceAux tactics (i+1)) - else - throwUnsupportedSyntax - -@[builtinTactic choice] def evalChoice : Tactic := fun stx => - evalChoiceAux stx.getArgs 0 - -@[builtinTactic skip] def evalSkip : Tactic := fun stx => pure () - -@[builtinTactic unknown] def evalUnknown : Tactic := fun stx => do - addCompletionInfo <| CompletionInfo.tactic stx (← getGoals) - -@[builtinTactic failIfSuccess] def evalFailIfSuccess : Tactic := fun stx => do - let tactic := stx[1] - if (← try evalTactic tactic; pure true catch _ => pure false) then - throwError "tactic succeeded" - -@[builtinTactic traceState] def evalTraceState : Tactic := fun stx => do - let gs ← getUnsolvedGoals - logInfo (goalsToMessageData gs) - -@[builtinTactic Lean.Parser.Tactic.assumption] def evalAssumption : Tactic := fun stx => - liftMetaTactic fun mvarId => do Meta.assumption mvarId; pure [] - -@[builtinTactic Lean.Parser.Tactic.contradiction] def evalContradiction : Tactic := fun stx => - liftMetaTactic fun mvarId => do Meta.contradiction mvarId; pure [] - -@[builtinTactic Lean.Parser.Tactic.intro] def evalIntro : Tactic := fun stx => do - match stx with - | `(tactic| intro) => introStep `_ - | `(tactic| intro $h:ident) => introStep h.getId - | `(tactic| intro _) => introStep `_ - | `(tactic| intro $pat:term) => evalTactic (← `(tactic| intro h; match h with | $pat:term => ?_; try clear h)) - | `(tactic| intro $h:term $hs:term*) => evalTactic (← `(tactic| intro $h:term; intro $hs:term*)) - | _ => throwUnsupportedSyntax -where - introStep (n : Name) : TacticM Unit := - liftMetaTactic fun mvarId => do - let (_, mvarId) ← Meta.intro mvarId n - pure [mvarId] - -@[builtinTactic Lean.Parser.Tactic.introMatch] def evalIntroMatch : Tactic := fun stx => do - let matchAlts := stx[1] - let stxNew ← liftMacroM <| Term.expandMatchAltsIntoMatchTactic stx matchAlts - withMacroExpansion stx stxNew <| evalTactic stxNew - -private def getIntrosSize : Expr → Nat - | Expr.forallE _ _ b _ => getIntrosSize b + 1 - | Expr.letE _ _ _ b _ => getIntrosSize b + 1 - | Expr.mdata _ b _ => getIntrosSize b - | _ => 0 - /- Recall that `ident' := ident <|> Term.hole` -/ def getNameOfIdent' (id : Syntax) : Name := if id.isIdent then id.getId else `_ -@[builtinTactic «intros»] def evalIntros : Tactic := fun stx => - match stx with - | `(tactic| intros) => liftMetaTactic fun mvarId => do - let type ← Meta.getMVarType mvarId - let type ← instantiateMVars type - let n := getIntrosSize type - let (_, mvarId) ← Meta.introN mvarId n - pure [mvarId] - | `(tactic| intros $ids*) => liftMetaTactic fun mvarId => do - let (_, mvarId) ← Meta.introN mvarId ids.size (ids.map getNameOfIdent').toList - pure [mvarId] - | _ => throwUnsupportedSyntax - def getFVarId (id : Syntax) : TacticM FVarId := withRef id do let fvar? ← Term.isLocalIdent? id; match fvar? with @@ -537,56 +388,6 @@ def getFVarId (id : Syntax) : TacticM FVarId := withRef id do def getFVarIds (ids : Array Syntax) : TacticM (Array FVarId) := do withMainContext do ids.mapM getFVarId -@[builtinTactic Lean.Parser.Tactic.revert] def evalRevert : Tactic := fun stx => - match stx with - | `(tactic| revert $hs*) => do - let (_, mvarId) ← Meta.revert (← getMainGoal) (← getFVarIds hs) - replaceMainGoal [mvarId] - | _ => throwUnsupportedSyntax - -/- Sort free variables using an order `x < y` iff `x` was defined after `y` -/ -private def sortFVarIds (fvarIds : Array FVarId) : TacticM (Array FVarId) := - withMainContext do - let lctx ← getLCtx - return fvarIds.qsort fun fvarId₁ fvarId₂ => - match lctx.find? fvarId₁, lctx.find? fvarId₂ with - | some d₁, some d₂ => d₁.index > d₂.index - | some _, none => false - | none, some _ => true - | none, none => Name.quickLt fvarId₁ fvarId₂ - -@[builtinTactic Lean.Parser.Tactic.clear] def evalClear : Tactic := fun stx => - match stx with - | `(tactic| clear $hs*) => do - let fvarIds ← getFVarIds hs - let fvarIds ← sortFVarIds fvarIds - for fvarId in fvarIds do - withMainContext do - let mvarId ← clear (← getMainGoal) fvarId - replaceMainGoal [mvarId] - | _ => throwUnsupportedSyntax - -def forEachVar (hs : Array Syntax) (tac : MVarId → FVarId → MetaM MVarId) : TacticM Unit := do - for h in hs do - withMainContext do - let fvarId ← getFVarId h - let mvarId ← tac (← getMainGoal) (← getFVarId h) - replaceMainGoal [mvarId] - -@[builtinTactic Lean.Parser.Tactic.subst] def evalSubst : Tactic := fun stx => - match stx with - | `(tactic| subst $hs*) => forEachVar hs Meta.subst - | _ => throwUnsupportedSyntax - -/-- - First method searches for a metavariable `g` s.t. `tag` is a suffix of its name. - If none is found, then it searches for a metavariable `g` s.t. `tag` is a prefix of its name. -/ -private def findTag? (mvarIds : List MVarId) (tag : Name) : TacticM (Option MVarId) := do - let mvarId? ← mvarIds.findM? fun mvarId => return tag.isSuffixOf (← getMVarDecl mvarId).userName - match mvarId? with - | some mvarId => return mvarId - | none => mvarIds.findM? fun mvarId => return tag.isPrefixOf (← getMVarDecl mvarId).userName - /-- Use position of `=> $body` for error messages. If there is a line break before `body`, the message will be displayed on `=>` only, @@ -594,59 +395,6 @@ private def findTag? (mvarIds : List MVarId) (tag : Name) : TacticM (Option MVar def withCaseRef [Monad m] [MonadRef m] (arrow body : Syntax) (x : m α) : m α := withRef (mkNullNode #[arrow, body]) x -@[builtinTactic «case»] def evalCase : Tactic - | stx@`(tactic| case $tag $hs* =>%$arr $tac:tacticSeq) => do - let tag := tag.getId - let gs ← getUnsolvedGoals - let some g ← findTag? gs tag | throwError "tag not found" - let gs := gs.erase g - let mut g := g - unless hs.isEmpty do - let mvarDecl ← getMVarDecl g - let mut lctx := mvarDecl.lctx - let mut hs := hs - let n := lctx.numIndices - for i in [:n] do - let j := n - i - 1 - match lctx.getAt? j with - | none => pure () - | some localDecl => - if localDecl.userName.hasMacroScopes then - let h := hs.back - if h.isIdent then - let newName := h.getId - lctx := lctx.setUserName localDecl.fvarId newName - hs := hs.pop - if hs.isEmpty then - break - unless hs.isEmpty do - logError m!"too many variable names provided at 'case'" - let mvarNew ← mkFreshExprMVarAt lctx mvarDecl.localInstances mvarDecl.type MetavarKind.syntheticOpaque mvarDecl.userName - assignExprMVar g mvarNew - g := mvarNew.mvarId! - setGoals [g] - let savedTag ← getMVarTag g - setMVarTag g Name.anonymous - try - withCaseRef arr tac do - closeUsingOrAdmit (withTacticInfoContext stx (evalTactic tac)) - finally - setMVarTag g savedTag - done - setGoals gs - | _ => throwUnsupportedSyntax - -@[builtinTactic «first»] partial def evalFirst : Tactic := fun stx => do - let tacs := stx[1].getArgs - if tacs.isEmpty then throwUnsupportedSyntax - loop tacs 0 -where - loop (tacs : Array Syntax) (i : Nat) := - if i == tacs.size - 1 then - evalTactic tacs[i][1] - else - evalTactic tacs[i][1] <|> loop tacs (i+1) - builtin_initialize registerTraceClass `Elab.tactic end Lean.Elab.Tactic diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean new file mode 100644 index 0000000000..ef2111354b --- /dev/null +++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean @@ -0,0 +1,263 @@ +/- +Copyright (c) 2021 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +import Lean.Elab.Tactic.Basic + +namespace Lean.Elab.Tactic +open Meta + +@[builtinTactic Lean.Parser.Tactic.«done»] def evalDone : Tactic := fun _ => + done + +@[builtinTactic seq1] def evalSeq1 : Tactic := fun stx => do + let args := stx[0].getArgs + for i in [:args.size] do + if i % 2 == 0 then + evalTactic args[i] + else + saveTacticInfoForToken args[i] -- add `TacticInfo` node for `;` + +@[builtinTactic paren] def evalParen : Tactic := fun stx => + evalTactic stx[1] + +/- Evaluate `many (group (tactic >> optional ";")) -/ +private def evalManyTacticOptSemi (stx : Syntax) : TacticM Unit := do + stx.forArgsM fun seqElem => do + evalTactic seqElem[0] + saveTacticInfoForToken seqElem[1] -- add TacticInfo node for `;` + +@[builtinTactic tacticSeq1Indented] def evalTacticSeq1Indented : Tactic := fun stx => + evalManyTacticOptSemi stx[0] + +@[builtinTactic tacticSeqBracketed] def evalTacticSeqBracketed : Tactic := fun stx => do + let initInfo ← mkInitialTacticInfo stx[0] + withRef stx[2] <| closeUsingOrAdmit do + -- save state before/after entering focus on `{` + withInfoContext (pure ()) initInfo + evalManyTacticOptSemi stx[1] + +@[builtinTactic Parser.Tactic.focus] def evalFocus : Tactic := fun stx => do + let mkInfo ← mkInitialTacticInfo stx[0] + focus do + -- show focused state on `focus` + withInfoContext (pure ()) mkInfo + evalTactic stx[1] + +private def getOptRotation (stx : Syntax) : Nat := + if stx.isNone then 1 else stx[0].toNat + +@[builtinTactic Parser.Tactic.rotateLeft] def evalRotateLeft : Tactic := fun stx => do + let n := getOptRotation stx[1] + setGoals <| (← getGoals).rotateLeft n + +@[builtinTactic Parser.Tactic.rotateRight] def evalRotateRight : Tactic := fun stx => do + let n := getOptRotation stx[1] + setGoals <| (← getGoals).rotateRight n + +@[builtinTactic Parser.Tactic.open] def evalOpen : Tactic := fun stx => do + try + pushScope + let openDecls ← elabOpenDecl stx[1] + withTheReader Core.Context (fun ctx => { ctx with openDecls := openDecls }) do + evalTactic stx[3] + finally + popScope + +@[builtinTactic Parser.Tactic.set_option] def elabSetOption : Tactic := fun stx => do + let options ← Elab.elabSetOption stx[1] stx[2] + withTheReader Core.Context (fun ctx => { ctx with maxRecDepth := maxRecDepth.get options, options := options }) do + evalTactic stx[4] + +@[builtinTactic Parser.Tactic.allGoals] def evalAllGoals : Tactic := fun stx => do + let mvarIds ← getGoals + let mut mvarIdsNew := #[] + for mvarId in mvarIds do + unless (← isExprMVarAssigned mvarId) do + setGoals [mvarId] + try + evalTactic stx[1] + mvarIdsNew := mvarIdsNew ++ (← getUnsolvedGoals) + catch ex => + logException ex + mvarIdsNew := mvarIdsNew.push mvarId + setGoals mvarIdsNew.toList + +@[builtinTactic tacticSeq] def evalTacticSeq : Tactic := fun stx => + evalTactic stx[0] + +partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit := + if h : i < tactics.size then + let tactic := tactics.get ⟨i, h⟩ + catchInternalId unsupportedSyntaxExceptionId + (evalTactic tactic) + (fun _ => evalChoiceAux tactics (i+1)) + else + throwUnsupportedSyntax + +@[builtinTactic choice] def evalChoice : Tactic := fun stx => + evalChoiceAux stx.getArgs 0 + +@[builtinTactic skip] def evalSkip : Tactic := fun stx => pure () + +@[builtinTactic unknown] def evalUnknown : Tactic := fun stx => do + addCompletionInfo <| CompletionInfo.tactic stx (← getGoals) + +@[builtinTactic failIfSuccess] def evalFailIfSuccess : Tactic := fun stx => do + let tactic := stx[1] + if (← try evalTactic tactic; pure true catch _ => pure false) then + throwError "tactic succeeded" + +@[builtinTactic traceState] def evalTraceState : Tactic := fun stx => do + let gs ← getUnsolvedGoals + logInfo (goalsToMessageData gs) + +@[builtinTactic Lean.Parser.Tactic.assumption] def evalAssumption : Tactic := fun stx => + liftMetaTactic fun mvarId => do Meta.assumption mvarId; pure [] + +@[builtinTactic Lean.Parser.Tactic.contradiction] def evalContradiction : Tactic := fun stx => + liftMetaTactic fun mvarId => do Meta.contradiction mvarId; pure [] + +@[builtinTactic Lean.Parser.Tactic.intro] def evalIntro : Tactic := fun stx => do + match stx with + | `(tactic| intro) => introStep `_ + | `(tactic| intro $h:ident) => introStep h.getId + | `(tactic| intro _) => introStep `_ + | `(tactic| intro $pat:term) => evalTactic (← `(tactic| intro h; match h with | $pat:term => ?_; try clear h)) + | `(tactic| intro $h:term $hs:term*) => evalTactic (← `(tactic| intro $h:term; intro $hs:term*)) + | _ => throwUnsupportedSyntax +where + introStep (n : Name) : TacticM Unit := + liftMetaTactic fun mvarId => do + let (_, mvarId) ← Meta.intro mvarId n + pure [mvarId] + +@[builtinTactic Lean.Parser.Tactic.introMatch] def evalIntroMatch : Tactic := fun stx => do + let matchAlts := stx[1] + let stxNew ← liftMacroM <| Term.expandMatchAltsIntoMatchTactic stx matchAlts + withMacroExpansion stx stxNew <| evalTactic stxNew + +private def getIntrosSize : Expr → Nat + | Expr.forallE _ _ b _ => getIntrosSize b + 1 + | Expr.letE _ _ _ b _ => getIntrosSize b + 1 + | Expr.mdata _ b _ => getIntrosSize b + | _ => 0 + +@[builtinTactic «intros»] def evalIntros : Tactic := fun stx => + match stx with + | `(tactic| intros) => liftMetaTactic fun mvarId => do + let type ← Meta.getMVarType mvarId + let type ← instantiateMVars type + let n := getIntrosSize type + let (_, mvarId) ← Meta.introN mvarId n + pure [mvarId] + | `(tactic| intros $ids*) => liftMetaTactic fun mvarId => do + let (_, mvarId) ← Meta.introN mvarId ids.size (ids.map getNameOfIdent').toList + pure [mvarId] + | _ => throwUnsupportedSyntax + +@[builtinTactic Lean.Parser.Tactic.revert] def evalRevert : Tactic := fun stx => + match stx with + | `(tactic| revert $hs*) => do + let (_, mvarId) ← Meta.revert (← getMainGoal) (← getFVarIds hs) + replaceMainGoal [mvarId] + | _ => throwUnsupportedSyntax + +/- Sort free variables using an order `x < y` iff `x` was defined after `y` -/ +private def sortFVarIds (fvarIds : Array FVarId) : TacticM (Array FVarId) := + withMainContext do + let lctx ← getLCtx + return fvarIds.qsort fun fvarId₁ fvarId₂ => + match lctx.find? fvarId₁, lctx.find? fvarId₂ with + | some d₁, some d₂ => d₁.index > d₂.index + | some _, none => false + | none, some _ => true + | none, none => Name.quickLt fvarId₁ fvarId₂ + +@[builtinTactic Lean.Parser.Tactic.clear] def evalClear : Tactic := fun stx => + match stx with + | `(tactic| clear $hs*) => do + let fvarIds ← getFVarIds hs + let fvarIds ← sortFVarIds fvarIds + for fvarId in fvarIds do + withMainContext do + let mvarId ← clear (← getMainGoal) fvarId + replaceMainGoal [mvarId] + | _ => throwUnsupportedSyntax + +def forEachVar (hs : Array Syntax) (tac : MVarId → FVarId → MetaM MVarId) : TacticM Unit := do + for h in hs do + withMainContext do + let fvarId ← getFVarId h + let mvarId ← tac (← getMainGoal) (← getFVarId h) + replaceMainGoal [mvarId] + +@[builtinTactic Lean.Parser.Tactic.subst] def evalSubst : Tactic := fun stx => + match stx with + | `(tactic| subst $hs*) => forEachVar hs Meta.subst + | _ => throwUnsupportedSyntax + +/-- + First method searches for a metavariable `g` s.t. `tag` is a suffix of its name. + If none is found, then it searches for a metavariable `g` s.t. `tag` is a prefix of its name. -/ +private def findTag? (mvarIds : List MVarId) (tag : Name) : TacticM (Option MVarId) := do + let mvarId? ← mvarIds.findM? fun mvarId => return tag.isSuffixOf (← getMVarDecl mvarId).userName + match mvarId? with + | some mvarId => return mvarId + | none => mvarIds.findM? fun mvarId => return tag.isPrefixOf (← getMVarDecl mvarId).userName + +@[builtinTactic «case»] def evalCase : Tactic + | stx@`(tactic| case $tag $hs* =>%$arr $tac:tacticSeq) => do + let tag := tag.getId + let gs ← getUnsolvedGoals + let some g ← findTag? gs tag | throwError "tag not found" + let gs := gs.erase g + let mut g := g + unless hs.isEmpty do + let mvarDecl ← getMVarDecl g + let mut lctx := mvarDecl.lctx + let mut hs := hs + let n := lctx.numIndices + for i in [:n] do + let j := n - i - 1 + match lctx.getAt? j with + | none => pure () + | some localDecl => + if localDecl.userName.hasMacroScopes then + let h := hs.back + if h.isIdent then + let newName := h.getId + lctx := lctx.setUserName localDecl.fvarId newName + hs := hs.pop + if hs.isEmpty then + break + unless hs.isEmpty do + logError m!"too many variable names provided at 'case'" + let mvarNew ← mkFreshExprMVarAt lctx mvarDecl.localInstances mvarDecl.type MetavarKind.syntheticOpaque mvarDecl.userName + assignExprMVar g mvarNew + g := mvarNew.mvarId! + setGoals [g] + let savedTag ← getMVarTag g + setMVarTag g Name.anonymous + try + withCaseRef arr tac do + closeUsingOrAdmit (withTacticInfoContext stx (evalTactic tac)) + finally + setMVarTag g savedTag + done + setGoals gs + | _ => throwUnsupportedSyntax + +@[builtinTactic «first»] partial def evalFirst : Tactic := fun stx => do + let tacs := stx[1].getArgs + if tacs.isEmpty then throwUnsupportedSyntax + loop tacs 0 +where + loop (tacs : Array Syntax) (i : Nat) := + if i == tacs.size - 1 then + evalTactic tacs[i][1] + else + evalTactic tacs[i][1] <|> loop tacs (i+1) + +end Lean.Elab.Tactic