From 6f0e9452b2e4438afde69a442883178008ad62ca Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 30 Aug 2020 14:08:30 -0700 Subject: [PATCH] chore: remove `begin ... end` syntax We should use `by { ... }` from now on. cc @Kha --- src/Lean/Elab/App.lean | 10 ++++------ src/Lean/Elab/Tactic/Basic.lean | 5 +---- src/Lean/Elab/Term.lean | 6 ------ src/Lean/Parser/Tactic.lean | 1 - src/Lean/Parser/Term.lean | 1 - tests/lean/match3.lean | 4 ++-- tests/lean/run/newfrontend1.lean | 2 +- 7 files changed, 8 insertions(+), 21 deletions(-) diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 7d9007e745..bb6da8c897 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -236,12 +236,10 @@ private partial def elabAppArgsAux : ElabAppArgsCtx → Expr → Expr → TermEl match evalSyntaxConstant env tacticDecl with | Except.error err => throwError err | Except.ok tacticSyntax => do - tacticBlock ← `(begin $(tacticSyntax.getArgs)* end); - -- tacticBlock does not have any position information - -- use ctx.ref.getHeadInfo if available - let tacticBlock := match ctx.ref.getHeadInfo with - | some info => tacticBlock.replaceInfo info - | _ => tacticBlock; + tacticBlock ← `(by { $(tacticSyntax.getArgs)* }); + -- tacticBlock does not have any position information. + -- So, we use ctx.ref + let tacticBlock := tacticBlock.copyInfo ctx.ref; let d := d.getArg! 0; -- `autoParam type := by tactic` ==> `type` argElab ← elabArg e (Arg.stx tacticBlock) d; elabAppArgsAux ctx (mkApp e argElab) (b.instantiate1 argElab) diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index faf4a37fb6..74afd4edf2 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -372,12 +372,9 @@ fun stx => match_syntax stx with @[builtinTactic paren] def evalParen : Tactic := fun stx => evalTactic (stx.getArg 1) -@[builtinTactic nestedTacticBlock] def evalNestedTacticBlock : Tactic := +@[builtinTactic nestedTacticBlockCurly] def evalNestedTacticBlock : Tactic := fun stx => focus (evalTactic (stx.getArg 1)) -@[builtinTactic nestedTacticBlockCurly] def evalNestedTacticBlockCurly : Tactic := -evalNestedTacticBlock - @[builtinTactic «case»] def evalCase : Tactic := fun stx => match_syntax stx with | `(tactic| case $tag $tac) => do diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index ff3fed54d7..166cc04d2b 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -972,12 +972,6 @@ ref ← getRef; registerSyntheticMVar ref mvarId $ SyntheticMVarKind.tactic tacticCode; pure mvar -@[builtinTermElab tacticBlock] def elabTacticBlock : TermElab := -fun stx expectedType? => - match expectedType? with - | some expectedType => mkTacticMVar expectedType (stx.getArg 1) - | none => throwError ("invalid tactic block, expected type has not been provided") - @[builtinTermElab byTactic] def elabByTactic : TermElab := fun stx expectedType? => match expectedType? with diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean index 34b7a92b2b..e144a3155e 100644 --- a/src/Lean/Parser/Tactic.lean +++ b/src/Lean/Parser/Tactic.lean @@ -60,7 +60,6 @@ def matchAlts : Parser := withPosition $ fun pos => (optional "| ") >> sepBy1 ma @[builtinTacticParser] def «match» := parser! nonReservedSymbol "match " >> sepBy1 Term.matchDiscr ", " >> Term.optType >> " with " >> matchAlts @[builtinTacticParser] def «injection» := parser! nonReservedSymbol "injection " >> termParser >> withIds @[builtinTacticParser] def paren := parser! "(" >> nonEmptySeq >> ")" -@[builtinTacticParser] def nestedTacticBlock := parser! "begin " >> seq >> "end" @[builtinTacticParser] def nestedTacticBlockCurly := parser! "{" >> seq >> "}" @[builtinTacticParser] def orelse := tparser!:2 " <|> " >> tacticParser 1 diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index f3104e2db9..32d77b8575 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -222,7 +222,6 @@ stx.isAntiquot || stx.isIdent @[builtinTermParser] def seqRight := tparser! infixR " *> " 60 @[builtinTermParser] def map := tparser! infixR " <$> " 100 -@[builtinTermParser] def tacticBlock := parser! "begin " >> Tactic.seq >> "end" @[builtinTermParser] def byTactic := parser!:leadPrec "by " >> Tactic.nonEmptySeq @[builtinTermParser] def funBinder.quot : Parser := parser! "`(funBinder|" >> toggleInsideQuot funBinder >> ")" diff --git a/tests/lean/match3.lean b/tests/lean/match3.lean index 6e7565c58a..6f1fc3f0c7 100644 --- a/tests/lean/match3.lean +++ b/tests/lean/match3.lean @@ -33,10 +33,10 @@ match a', h₁, h₂ with | _, rfl, h₂ => h₂ theorem ex6 {α β : Sort u} {b : β} {a a' : α} (h₁ : a = a') (h₂ : a' ≅ b) : a ≅ b := -begin +by { subst h₁; assumption -end +} theorem ex7 (a : Bool) (p q : Prop) (h₁ : a = true → p) (h₂ : a = false → q) : p ∨ q := match h:a with diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean index 098adf3cb4..1737758b08 100644 --- a/tests/lean/run/newfrontend1.lean +++ b/tests/lean/run/newfrontend1.lean @@ -119,7 +119,7 @@ by { namespace Foo def Prod.mk := 1 #check (⟨2, 3⟩ : Prod _ _) -} Foo +end Foo theorem simple10 (x y z : Nat) : y = z → x = x → x = y → x = z := by {