From fb4d90a58b684f2cd50b503d7f3f246323d74068 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 17 Oct 2022 15:34:04 -0700 Subject: [PATCH] feat: dynamic quotations for categories --- doc/examples/bintree.lean | 5 +-- src/Init/Conv.lean | 16 ++++----- src/Init/Data/Array/Mem.lean | 2 +- src/Init/Data/List/BasicAux.lean | 2 +- src/Init/Meta.lean | 2 +- src/Init/Tactics.lean | 24 ++++++------- src/Init/WFTactics.lean | 5 +-- src/Lean/Elab/Binders.lean | 2 +- src/Lean/Elab/BuiltinCommand.lean | 20 ++++++----- src/Lean/Elab/Command.lean | 9 ++--- src/Lean/Elab/Deriving/Inhabited.lean | 7 ++-- src/Lean/Elab/Deriving/Repr.lean | 2 +- src/Lean/Elab/MacroArgUtil.lean | 27 +++++++------- src/Lean/Elab/Quotation.lean | 36 ++++++------------- src/Lean/Elab/Syntax.lean | 51 ++++++++++++--------------- src/Lean/Parser/Do.lean | 2 -- src/Lean/Parser/Extension.lean | 51 +++++++++++++++++++++++---- src/Lean/Parser/Syntax.lean | 15 ++------ src/Lean/Parser/Term.lean | 8 +---- src/Lean/Server/Rpc/Deriving.lean | 4 +-- src/lake | 2 +- tests/lean/1163.lean | 2 +- tests/lean/StxQuot.lean | 4 +++ tests/lean/StxQuot.lean.expected.out | 1 + tests/lean/interactive/hover.lean | 2 +- tests/lean/run/allGoals.lean | 2 +- tests/lean/run/doNotation3.lean | 2 +- tests/lean/run/eqThm.lean | 2 +- tests/lean/run/impLambdaTac.lean | 2 +- tests/lean/run/macroParams.lean | 2 +- tests/lean/run/maze.lean | 7 ++-- tests/lean/run/newfrontend1.lean | 4 +-- tests/lean/rwWithoutOffsetCnstrs.lean | 2 +- tests/lean/traceClassScopes.lean | 4 +-- tests/pkg/user_attr/UserAttr/Tst.lean | 2 +- 35 files changed, 170 insertions(+), 160 deletions(-) diff --git a/doc/examples/bintree.lean b/doc/examples/bintree.lean index 9b92366388..ff62f88c42 100644 --- a/doc/examples/bintree.lean +++ b/doc/examples/bintree.lean @@ -176,7 +176,8 @@ The modifier `local` specifies the scope of the macro. /-- The `have_eq lhs rhs` tactic (tries to) prove that `lhs = rhs`, and then replaces `lhs` with `rhs`. -/ local macro "have_eq " lhs:term:max rhs:term:max : tactic => - `((have h : $lhs = $rhs := + `(tactic| + (have h : $lhs = $rhs := -- TODO: replace with linarith by simp_arith at *; apply Nat.le_antisymm <;> assumption try subst $lhs)) @@ -191,7 +192,7 @@ useful if `e` is the condition of an `if`-statement. -/ /-- `by_cases' e` is a shorthand form `by_cases e <;> simp[*]` -/ local macro "by_cases' " e:term : tactic => - `(by_cases $e <;> simp [*]) + `(tactic| by_cases $e <;> simp [*]) /-! diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean index f83dbd9d21..105e783e19 100644 --- a/src/Init/Conv.lean +++ b/src/Init/Conv.lean @@ -169,13 +169,13 @@ syntax (name := paren) "(" convSeq ")" : conv /-- `rfl` closes one conv goal "trivially", by using reflexivity (that is, no rewriting). -/ -macro "rfl" : conv => `(tactic => rfl) +macro "rfl" : conv => `(conv| tactic => rfl) /-- `done` succeeds iff there are no goals remaining. -/ -macro "done" : conv => `(tactic' => done) +macro "done" : conv => `(conv| tactic' => done) /-- `trace_state` prints the current goal state. -/ -macro "trace_state" : conv => `(tactic' => trace_state) +macro "trace_state" : conv => `(conv| tactic' => trace_state) /-- `all_goals tac` runs `tac` on each goal, concatenating the resulting goals, if any. -/ macro (name := allGoals) tk:"all_goals " s:convSeq : conv => @@ -225,7 +225,7 @@ resulting in `t'`, which becomes the new target subgoal. -/ syntax (name := convConvSeq) "conv" " => " convSeq : conv /-- `· conv` focuses on the main conv goal and tries to solve it using `s`. -/ -macro dot:("·" <|> ".") s:convSeq : conv => `({%$dot ($s) }) +macro dot:("·" <|> ".") s:convSeq : conv => `(conv| {%$dot ($s) }) /-- `fail_if_success t` fails if the tactic `t` succeeds. -/ @@ -234,12 +234,12 @@ macro (name := failIfSuccess) tk:"fail_if_success " s:convSeq : conv => /-- `rw [rules]` applies the given list of rewrite rules to the target. See the `rw` tactic for more information. -/ -macro "rw" c:(config)? s:rwRuleSeq : conv => `(rewrite $[$c]? $s) +macro "rw" c:(config)? s:rwRuleSeq : conv => `(conv| rewrite $[$c]? $s) /-- `erw [rules]` is a shorthand for `rw (config := { transparency := .default }) [rules]`. This does rewriting up to unfolding of regular definitions (by comparison to regular `rw` which only unfolds `@[reducible]` definitions). -/ -macro "erw" s:rwRuleSeq : conv => `(rw (config := { transparency := .default }) $s) +macro "erw" s:rwRuleSeq : conv => `(conv| rw (config := { transparency := .default }) $s) /-- `args` traverses into all arguments. Synonym for `congr`. -/ macro "args" : conv => `(congr) @@ -270,13 +270,13 @@ macro_rules There are no restrictions on `thm`, but strange results may occur if `thm` cannot be reasonably interpreted as proving one equality from a list of others. -/ -- TODO: error if non-conv subgoals? -macro "apply " e:term : conv => `(tactic => apply $e) +macro "apply " e:term : conv => `(conv| tactic => apply $e) /-- `first | conv | ...` runs each `conv` until one succeeds, or else fails. -/ syntax (name := first) "first " withPosition((colGe "|" convSeq)+) : conv /-- `try tac` runs `tac` and succeeds even if `tac` failed. -/ -macro "try " t:convSeq : conv => `(first | $t | skip) +macro "try " t:convSeq : conv => `(conv| first | $t | skip) macro:1 x:conv tk:" <;> " y:conv:0 : conv => `(conv| tactic' => (conv' => $x:conv) <;>%$tk (conv' => $y:conv)) diff --git a/src/Init/Data/Array/Mem.lean b/src/Init/Data/Array/Mem.lean index d3faebb330..1c6ec08e95 100644 --- a/src/Init/Data/Array/Mem.lean +++ b/src/Init/Data/Array/Mem.lean @@ -51,7 +51,7 @@ termination_by aux j _ => as.size - j `sizeOf arr[i] < sizeOf arr`, which is useful for well founded recursions over a nested inductive like `inductive T | mk : Array T → T`. -/ macro "array_get_dec" : tactic => - `(first + `(tactic| first | apply sizeOf_get | apply Nat.lt_trans (sizeOf_get ..); simp_arith) diff --git a/src/Init/Data/List/BasicAux.lean b/src/Init/Data/List/BasicAux.lean index 566881697f..5fda7289d8 100644 --- a/src/Init/Data/List/BasicAux.lean +++ b/src/Init/Data/List/BasicAux.lean @@ -125,7 +125,7 @@ theorem sizeOf_lt_of_mem [SizeOf α] {as : List α} (h : a ∈ as) : sizeOf a < `sizeOf a < sizeOf as` when `a ∈ as`, which is useful for well founded recursions over a nested inductive like `inductive T | mk : List T → T`. -/ macro "sizeOf_list_dec" : tactic => - `(first + `(tactic| first | apply sizeOf_lt_of_mem; assumption; done | apply Nat.lt_trans (sizeOf_lt_of_mem ?h) case' h => assumption diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index 8c42c2ce68..533fc8f809 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -1283,7 +1283,7 @@ namespace Parser.Tactic This does rewriting up to unfolding of regular definitions (by comparison to regular `rw` which only unfolds `@[reducible]` definitions). -/ macro "erw " s:rwRuleSeq loc:(location)? : tactic => - `(rw (config := { transparency := .default }) $s $(loc)?) + `(tactic| rw (config := { transparency := .default }) $s $(loc)?) syntax simpAllKind := atomic("(" &"all") " := " &"true" ")" syntax dsimpKind := atomic("(" &"dsimp") " := " &"true" ")" diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 2da5f26012..55ad675de4 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -236,7 +236,7 @@ and push it to the front `n` times. If `n` is omitted, it defaults to `1`. syntax (name := rotateRight) "rotate_right" (num)? : tactic /-- `try tac` runs `tac` and succeeds even if `tac` failed. -/ -macro "try " t:tacticSeq : tactic => `(first | $t | skip) +macro "try " t:tacticSeq : tactic => `(tactic| first | $t | skip) /-- `tac <;> tac'` runs `tac` on the main goal and `tac'` on each produced goal, @@ -464,7 +464,7 @@ syntax (name := unfold) "unfold " (colGt ident)+ (location)? : tactic Auxiliary macro for lifting have/suffices/let/... It makes sure the "continuation" `?_` is the main goal after refining. -/ -macro "refine_lift " e:term : tactic => `(focus (refine no_implicit_lambda% $e; rotate_right)) +macro "refine_lift " e:term : tactic => `(tactic| focus (refine no_implicit_lambda% $e; rotate_right)) /-- `have h : t := e` adds the hypothesis `h : t` to the current goal if `e` a term @@ -476,7 +476,7 @@ of type `t`. For example, given `h : p ∧ q ∧ r`, `have ⟨h₁, h₂, h₃⟩ := h` produces the hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`. -/ -macro "have " d:haveDecl : tactic => `(refine_lift have $d:haveDecl; ?_) +macro "have " d:haveDecl : tactic => `(tactic| refine_lift have $d:haveDecl; ?_) /-- Given a main goal `ctx ⊢ t`, `suffices h : t' from e` replaces the main goal with `ctx ⊢ t'`, @@ -485,7 +485,7 @@ Given a main goal `ctx ⊢ t`, `suffices h : t' from e` replaces the main goal w The variant `suffices h : t' by tac` is a shorthand for `suffices h : t' from by tac`. If `h :` is omitted, the name `this` is used. -/ -macro "suffices " d:sufficesDecl : tactic => `(refine_lift suffices $d; ?_) +macro "suffices " d:sufficesDecl : tactic => `(tactic| refine_lift suffices $d; ?_) /-- `let h : t := e` adds the hypothesis `h : t := e` to the current goal if `e` a term of type `t`. If `t` is omitted, it will be inferred. @@ -494,12 +494,12 @@ and it is convenient for types that have only applicable constructor. Example: given `h : p ∧ q ∧ r`, `let ⟨h₁, h₂, h₃⟩ := h` produces the hypotheses `h₁ : p`, `h₂ : q`, and `h₃ : r`. -/ -macro "let " d:letDecl : tactic => `(refine_lift let $d:letDecl; ?_) +macro "let " d:letDecl : tactic => `(tactic| refine_lift let $d:letDecl; ?_) /-- `show t` finds the first goal whose target unifies with `t`. It makes that the main goal, performs the unification, and replaces the target with the unified version of `t`. -/ -macro "show " e:term : tactic => `(refine_lift show $e from ?_) -- TODO: fix, see comment +macro "show " e:term : tactic => `(tactic| refine_lift show $e from ?_) -- TODO: fix, see comment /-- `let rec f : t := e` adds a recursive definition `f` to the current goal. The syntax is the same as term-mode `let rec`. -/ syntax (name := letrec) withPosition(atomic("let " &"rec ") letRecDecls) : tactic @@ -507,13 +507,13 @@ macro_rules | `(tactic| let rec $d) => `(tactic| refine_lift let rec $d; ?_) /-- Similar to `refine_lift`, but using `refine'` -/ -macro "refine_lift' " e:term : tactic => `(focus (refine' no_implicit_lambda% $e; rotate_right)) +macro "refine_lift' " e:term : tactic => `(tactic| focus (refine' no_implicit_lambda% $e; rotate_right)) /-- Similar to `have`, but using `refine'` -/ -macro "have' " d:haveDecl : tactic => `(refine_lift' have $d:haveDecl; ?_) +macro "have' " d:haveDecl : tactic => `(tactic| refine_lift' have $d:haveDecl; ?_) /-- Similar to `have`, but using `refine'` -/ -macro (priority := high) "have'" x:ident " := " p:term : tactic => `(have' $x : _ := $p) +macro (priority := high) "have'" x:ident " := " p:term : tactic => `(tactic| have' $x : _ := $p) /-- Similar to `let`, but using `refine'` -/ -macro "let' " d:letDecl : tactic => `(refine_lift' let $d:letDecl; ?_) +macro "let' " d:letDecl : tactic => `(tactic| refine_lift' let $d:letDecl; ?_) /-- The left hand side of an induction arm, `| foo a b c` or `| @foo a b c` @@ -678,7 +678,7 @@ example : ∀ x : Nat, x = x := by unhygienic exact Eq.refl x -- refer to x ``` -/ -macro "unhygienic " t:tacticSeq : tactic => `(set_option tactic.hygienic false in $t) +macro "unhygienic " t:tacticSeq : tactic => `(tactic| set_option tactic.hygienic false in $t) /-- `fail msg` is a tactic that always fails, and produces an error using the given message. -/ syntax (name := fail) "fail " (str)? : tactic @@ -812,7 +812,7 @@ to prove any side conditions that arise when constructing the term users are encouraged to extend `get_elem_tactic_trivial` instead of this tactic. -/ macro "get_elem_tactic" : tactic => - `(first + `(tactic| first | get_elem_tactic_trivial | fail "failed to prove index is valid, possible solutions: - Use `have`-expressions to prove the index is valid diff --git a/src/Init/WFTactics.lean b/src/Init/WFTactics.lean index e019a077e3..04cff0d007 100644 --- a/src/Init/WFTactics.lean +++ b/src/Init/WFTactics.lean @@ -32,7 +32,8 @@ macro_rules | `(tactic| decreasing_trivial) => `(tactic| apply Nat.pred_lt; assu lexicographic order lemmas and using `ts` to solve the base case. If it fails, it prints a message to help the user diagnose an ill-founded recursive definition. -/ macro "decreasing_with " ts:tacticSeq : tactic => - `((simp_wf + `(tactic| + (simp_wf repeat (first | apply Prod.Lex.right | apply Prod.Lex.left) repeat (first | apply PSigma.Lex.right | apply PSigma.Lex.left) first @@ -49,4 +50,4 @@ on the recursive definition, and it can also be globally extended by adding more definitions for `decreasing_tactic` (or `decreasing_trivial`, which this tactic calls). -/ macro "decreasing_tactic" : tactic => - `(decreasing_with first | decreasing_trivial | subst_vars; decreasing_trivial) + `(tactic| decreasing_with first | decreasing_trivial | subst_vars; decreasing_trivial) diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean index 2f2a1274fe..c18acbb2f8 100644 --- a/src/Lean/Elab/Binders.lean +++ b/src/Lean/Elab/Binders.lean @@ -247,7 +247,7 @@ def elabBinder (binder : Syntax) (x : Expr → TermElabM α) : TermElabM α := /-- If `binder` is a `_` or an identifier, return a `bracketedBinder` using `type` otherwise throw an exception. -/ def expandSimpleBinderWithType (type : Term) (binder : Syntax) : MacroM Syntax := if binder.isOfKind ``hole || binder.isIdent then - `(bracketedBinder| ($binder : $type)) + `(bracketedBinderF| ($binder : $type)) else Macro.throwErrorAt type "unexpected type ascription" diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean index fb6f711abd..663b5e3c00 100644 --- a/src/Lean/Elab/BuiltinCommand.lean +++ b/src/Lean/Elab/BuiltinCommand.lean @@ -138,9 +138,11 @@ private partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM modifyScope fun scope => { scope with openDecls := openDecls } | _ => throwUnsupportedSyntax +open Lean.Parser.Term + private def typelessBinder? : Syntax → Option (Array (TSyntax [`ident, `Lean.Parser.Term.hole]) × Bool) - | `(bracketedBinder|($ids*)) => some <| (ids, true) - | `(bracketedBinder|{$ids*}) => some <| (ids, false) + | `(bracketedBinderF|($ids*)) => some (ids, true) + | `(bracketedBinderF|{$ids*}) => some (ids, false) | _ => none /-- If `id` is an identifier, return true if `ids` contains `id`. -/ @@ -167,15 +169,15 @@ private def replaceBinderAnnotation (binder : TSyntax ``Parser.Term.bracketedBin let mut modifiedVarDecls := false for varDecl in varDecls do let (ids, ty?, explicit') ← match varDecl with - | `(bracketedBinder|($ids* $[: $ty?]? $(annot?)?)) => + | `(bracketedBinderF|($ids* $[: $ty?]? $(annot?)?)) => if annot?.isSome then for binderId in binderIds do if containsId ids binderId then throwErrorAt binderId "cannot update binder annotation of variables with default values/tactics" pure (ids, ty?, true) - | `(bracketedBinder|{$ids* $[: $ty?]?}) => + | `(bracketedBinderF|{$ids* $[: $ty?]?}) => pure (ids, ty?, false) - | `(bracketedBinder|[$id : $_]) => + | `(bracketedBinderF|[$id : $_]) => for binderId in binderIds do if binderId.raw.isIdent && binderId.raw.getId == id.getId then throwErrorAt binderId "cannot change the binder annotation of the previously declared local instance `{id.getId}`" @@ -194,9 +196,9 @@ private def replaceBinderAnnotation (binder : TSyntax ``Parser.Term.bracketedBin else let mkBinder (id : TSyntax [`ident, ``Parser.Term.hole]) (explicit : Bool) : CommandElabM (TSyntax ``Parser.Term.bracketedBinder) := if explicit then - `(bracketedBinder| ($id $[: $ty?]?)) + `(bracketedBinderF| ($id $[: $ty?]?)) else - `(bracketedBinder| {$id $[: $ty?]?}) + `(bracketedBinderF| {$id $[: $ty?]?}) for id in ids do if let some idx := binderIds.findIdx? fun binderId => binderId.raw.isIdent && binderId.raw.getId == id.raw.getId then binderIds := binderIds.eraseIdx idx @@ -209,9 +211,9 @@ private def replaceBinderAnnotation (binder : TSyntax ``Parser.Term.bracketedBin if binderIds.size != binderIdsIniSize then binderIds.mapM fun binderId => if explicit then - `(bracketedBinder| ($binderId)) + `(bracketedBinderF| ($binderId)) else - `(bracketedBinder| {$binderId}) + `(bracketedBinderF| {$binderId}) else return #[binder] diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 90fbc86635..4ff7c4450e 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -339,12 +339,13 @@ private def mkMetaContext : Meta.Context := { config := { foApprox := true, ctxApprox := true, quasiPatternApprox := true } } +open Lean.Parser.Term in /-- Return identifier names in the given bracketed binder. -/ def getBracketedBinderIds : Syntax → Array Name - | `(bracketedBinder|($ids* $[: $ty?]? $(_annot?)?)) => ids.map Syntax.getId - | `(bracketedBinder|{$ids* $[: $ty?]?}) => ids.map Syntax.getId - | `(bracketedBinder|[$id : $_]) => #[id.getId] - | `(bracketedBinder|[$_]) => #[Name.anonymous] + | `(bracketedBinderF|($ids* $[: $ty?]? $(_annot?)?)) => ids.map Syntax.getId + | `(bracketedBinderF|{$ids* $[: $ty?]?}) => ids.map Syntax.getId + | `(bracketedBinderF|[$id : $_]) => #[id.getId] + | `(bracketedBinderF|[$_]) => #[Name.anonymous] | _ => #[] private def mkTermContext (ctx : Context) (s : State) : Term.Context := Id.run do diff --git a/src/Lean/Elab/Deriving/Inhabited.lean b/src/Lean/Elab/Deriving/Inhabited.lean index ec19764cf0..2ffab264e5 100644 --- a/src/Lean/Elab/Deriving/Inhabited.lean +++ b/src/Lean/Elab/Deriving/Inhabited.lean @@ -6,8 +6,7 @@ Authors: Leonardo de Moura import Lean.Elab.Deriving.Basic namespace Lean.Elab -open Command -open Meta +open Command Meta Parser Term private abbrev IndexSet := RBTree Nat compare private abbrev LocalInst2Index := FVarIdMap Nat @@ -66,10 +65,10 @@ where for i in [:indVal.numParams + indVal.numIndices] do let arg := mkIdent (← mkFreshUserName `a) indArgs := indArgs.push arg - let binder ← `(bracketedBinder| { $arg:ident }) + let binder ← `(bracketedBinderF| { $arg:ident }) binders := binders.push binder if assumingParamIdxs.contains i then - let binder ← `(bracketedBinder| [Inhabited $arg:ident ]) + let binder ← `(bracketedBinderF| [Inhabited $arg:ident ]) binders := binders.push binder let type ← `(Inhabited (@$(mkIdent inductiveTypeName):ident $indArgs:ident*)) let mut ctorArgs := #[] diff --git a/src/Lean/Elab/Deriving/Repr.lean b/src/Lean/Elab/Deriving/Repr.lean index d7638f551a..461d21036a 100644 --- a/src/Lean/Elab/Deriving/Repr.lean +++ b/src/Lean/Elab/Deriving/Repr.lean @@ -16,7 +16,7 @@ open Std def mkReprHeader (indVal : InductiveVal) : TermElabM Header := do let header ← mkHeader `Repr 1 indVal return { header with - binders := header.binders.push (← `(bracketedBinder| (prec : Nat))) + binders := header.binders.push (← `(bracketedBinderF| (prec : Nat))) } def mkBodyForStruct (header : Header) (indVal : InductiveVal) : TermElabM Term := do diff --git a/src/Lean/Elab/MacroArgUtil.lean b/src/Lean/Elab/MacroArgUtil.lean index 1b84aeaac1..de59e5dedf 100644 --- a/src/Lean/Elab/MacroArgUtil.lean +++ b/src/Lean/Elab/MacroArgUtil.lean @@ -45,22 +45,23 @@ where return ⟨mkNullNode #[mkAntiquotSuffixSpliceNode kind (← mkAntiquotNode stx id) suffix]⟩ mkAntiquotNode : TSyntax `stx → Term → CommandElabM Term | `(stx| $id:ident$[:$_]?), term => do - let kind ← match (← Elab.Term.resolveParserName id) with - | [(`Lean.Parser.ident, _)] => pure identKind - | [(`Lean.Parser.Term.ident, _)] => pure identKind - | [(`Lean.Parser.strLit, _)] => pure strLitKind - -- a syntax abbrev, assume kind == decl name - | [(c, _)] => pure c - | cs@(_ :: _ :: _) => throwError "ambiguous parser declaration {cs.map (·.1)}" - | [] => + match (← liftTermElabM do Elab.Term.elabParserName? id) with + | some (.parser n _) => + let kind := match n with + | ``Parser.ident => identKind + | ``Parser.Term.ident => identKind + | ``Parser.strLit => strLitKind + | _ => n -- assume kind == decl name + return ⟨Syntax.mkAntiquotNode kind term⟩ + | some (.category cat) => + return ⟨Syntax.mkAntiquotNode cat term (isPseudoKind := true)⟩ + | none => let id := id.getId.eraseMacroScopes - if Parser.isParserCategory (← getEnv) id then - return ⟨Syntax.mkAntiquotNode id term (isPseudoKind := true)⟩ - else if (← Parser.isParserAlias id) then - pure <| (← Parser.getSyntaxKindOfParserAlias? id).getD Name.anonymous + if (← Parser.isParserAlias id) then + let kind := (← Parser.getSyntaxKindOfParserAlias? id).getD Name.anonymous + return ⟨Syntax.mkAntiquotNode kind term⟩ else throwError "unknown parser declaration/category/alias '{id}'" - pure ⟨Syntax.mkAntiquotNode kind term⟩ | stx, term => do -- can't match against `` `(stx| ($stxs*)) `` as `*` is interpreted as the `stx` operator if stx.raw.isOfKind ``Parser.Syntax.paren then diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean index 272cbf57fd..d5d455e7fc 100644 --- a/src/Lean/Elab/Quotation.lean +++ b/src/Lean/Elab/Quotation.lean @@ -10,6 +10,7 @@ import Lean.ResolveName import Lean.Elab.Term import Lean.Elab.Quotation.Util import Lean.Elab.Quotation.Precheck +import Lean.Elab.Syntax import Lean.Parser.Syntax namespace Lean.Elab.Term.Quotation @@ -218,30 +219,20 @@ def getQuotKind (stx : Syntax) : TermElabM SyntaxNodeKind := do match stx.getKind with | ``Parser.Command.quot => addNamedQuotInfo stx `command | ``Parser.Term.quot => addNamedQuotInfo stx `term - | ``Parser.Level.quot => addNamedQuotInfo stx `level | ``Parser.Tactic.quot => addNamedQuotInfo stx `tactic | ``Parser.Tactic.quotSeq => addNamedQuotInfo stx `tactic.seq - | ``Parser.Term.stx.quot => addNamedQuotInfo stx `stx - | ``Parser.Term.prec.quot => addNamedQuotInfo stx `prec - | ``Parser.Term.attr.quot => addNamedQuotInfo stx `attr - | ``Parser.Term.prio.quot => addNamedQuotInfo stx `prio - | ``Parser.Term.doElem.quot => addNamedQuotInfo stx `doElem | .str kind "quot" => addNamedQuotInfo stx kind - | ``dynamicQuot => - match (← resolveGlobalConstWithInfos stx[1]) with - | [parser] => pure parser - | _ => throwError "unknown parser {stx[1]}" + | ``dynamicQuot => match ← elabParserName stx[1] with + | .parser n _ => return n + | .category c => return c | k => throwError "unexpected quotation kind {k}" -def stxQuot.expand (stx : Syntax) : TermElabM Syntax := do - let stx := if stx.getNumArgs == 1 then stx[0] else stx +def mkSyntaxQuotation (stx : Syntax) (kind : Name) : TermElabM Syntax := do /- Syntax quotations are monadic values depending on the current macro scope. For efficiency, we bind the macro scope once for each quotation, then build the syntax tree in a completely pure computation depending on this binding. Note that regular function calls do not introduce a new macro scope (i.e. we preserve referential transparency), so we can refer to this same `scp` inside `quoteSyntax` by including it literally in a syntax quotation. -/ - let kind ← getQuotKind stx - let stx ← quoteSyntax stx.getQuotContent `(Bind.bind MonadRef.mkInfoFromRefPos (fun info => Bind.bind getCurrMacroScope (fun scp => Bind.bind getMainModule (fun mainModule => Pure.pure (@TSyntax.mk $(quote kind) $stx))))) @@ -261,23 +252,18 @@ def stxQuot.expand (stx : Syntax) : TermElabM Syntax := do implementation is "self-stabilizing". It was in fact originally compiled by an unhygienic prototype implementation. -/ +def stxQuot.expand (stx : Syntax) : TermElabM Syntax := do + let stx := if stx.getNumArgs == 1 then stx[0] else stx + let kind ← getQuotKind stx + let stx ← quoteSyntax stx.getQuotContent + mkSyntaxQuotation stx kind + macro "elab_stx_quot" kind:ident : command => `(@[builtinTermElab $kind:ident] def elabQuot : TermElab := adaptExpander stxQuot.expand) --- - -elab_stx_quot Parser.Level.quot elab_stx_quot Parser.Term.quot -elab_stx_quot Parser.Term.funBinder.quot -elab_stx_quot Parser.Term.bracketedBinder.quot -elab_stx_quot Parser.Term.matchDiscr.quot elab_stx_quot Parser.Tactic.quot elab_stx_quot Parser.Tactic.quotSeq -elab_stx_quot Parser.Term.stx.quot -elab_stx_quot Parser.Term.prec.quot -elab_stx_quot Parser.Term.attr.quot -elab_stx_quot Parser.Term.prio.quot -elab_stx_quot Parser.Term.doElem.quot elab_stx_quot Parser.Term.dynamicQuot elab_stx_quot Parser.Command.quot diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index 86c50d586b..b499f4d223 100644 --- a/src/Lean/Elab/Syntax.lean +++ b/src/Lean/Elab/Syntax.lean @@ -79,26 +79,21 @@ def checkLeftRec (stx : Syntax) : ToParserDescrM Bool := do markAsTrailingParser (prec?.getD 0) return true -/-- Resolve the given parser name and return a list of candidates. - Each candidate is a pair `(resolvedParserName, isDescr)`. - `isDescr == true` if the type of `resolvedParserName` is a `ParserDescr`. -/ -def resolveParserName [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv m] [MonadError m] (parserName : Syntax) : m (List (Name × Bool)) := do - try - let candidates ← resolveGlobalConstWithInfos parserName - /- Convert `candidates` in a list of pairs `(c, isDescr)`, where `c` is the parser name, - and `isDescr` is true iff `c` has type `Lean.ParserDescr` or `Lean.TrailingParser` -/ - let env ← getEnv - return candidates.filterMap fun c => - match env.find? c with - | none => none - | some info => - match info.type with - | Expr.const ``Lean.Parser.TrailingParser _ => (c, false) - | Expr.const ``Lean.Parser.Parser _ => (c, false) - | Expr.const ``Lean.ParserDescr _ => (c, true) - | Expr.const ``Lean.TrailingParserDescr _ => (c, true) - | _ => none - catch _ => return [] +def elabParserName? (stx : Syntax.Ident) : TermElabM (Option Parser.ParserName) := do + match ← Parser.resolveParserName stx with + | [n@(.category cat)] => + addCategoryInfo stx cat + return n + | [n@(.parser parser _)] => + addTermInfo' stx (Lean.mkConst parser) + return n + | _::_::_ => throwErrorAt stx "ambiguous parser {stx}" + | [] => return none + +def elabParserName (stx : Syntax.Ident) : TermElabM Parser.ParserName := do + match ← elabParserName? stx with + | some n => return n + | none => throwErrorAt stx "unknown parser {stx}" open TSyntax.Compat in /-- @@ -161,7 +156,6 @@ where throwErrorAt stx "invalid atomic left recursive syntax" let prec? ← liftMacroM <| expandOptPrecedence stx[1] let prec := prec?.getD 0 - addCategoryInfo stx catName return (← `(ParserDescr.cat $(quote catName) $(quote prec)), 1) processAlias (id : Syntax) (args : Array Syntax) := do @@ -185,23 +179,22 @@ where return (stx, stackSz) processNullaryOrCat (stx : Syntax) := do - match (← resolveParserName stx[0]) with - | [(c, true)] => + match (← elabParserName? stx[0]) with + | some (.parser c (isDescr := true)) => ensureNoPrec stx -- `syntax _ :=` at least enforces this let stackSz := 1 return (mkIdentFrom stx c, stackSz) - | [(c, false)] => + | some (.parser c (isDescr := false)) => ensureNoPrec stx -- as usual, we assume that people using `Parser` know what they are doing let stackSz := 1 return (← `(ParserDescr.parser $(quote c)), stackSz) - | cs@(_ :: _ :: _) => throwError "ambiguous parser declaration {cs.map (·.1)}" - | [] => + | some (.category _) => + processParserCategory stx + | none => let id := stx[0].getId.eraseMacroScopes - if Parser.isParserCategory (← getEnv) id then - processParserCategory stx - else if (← Parser.isParserAlias id) then + if (← Parser.isParserAlias id) then ensureNoPrec stx processAlias stx[0] #[] else diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean index f0a2e630f0..3de10b9d8e 100644 --- a/src/Lean/Parser/Do.lean +++ b/src/Lean/Parser/Do.lean @@ -140,8 +140,6 @@ The second `notFollowedBy` prevents this problem. @[builtinTermParser] def «do» := leading_parser:argPrec ppAllowUngrouped >> "do " >> doSeq -@[builtinTermParser] def doElem.quot : Parser := leading_parser "`(doElem|" >> incQuotDepth doElemParser >> ")" - /- macros for using `unless`, `for`, `try`, `return` as terms. They expand into `do unless ...`, `do for ...`, `do try ...`, and `do return ...` -/ /-- `unless e do s` is a nicer way to write `if !e do s`. -/ @[builtinTermParser] def termUnless := leading_parser "unless " >> withForbidden "do" termParser >> "do " >> doSeq diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index 39a4f19e19..424ebdc74e 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -633,17 +633,56 @@ def withOpenDeclFn (p : ParserFn) : ParserFn := fun c s => fn := withOpenDeclFn p.fn } -def ParserContext.resolveName (ctx : ParserContext) (id : Name) : List (Name × List String) := - ResolveName.resolveGlobalName ctx.env ctx.currNamespace ctx.openDecls id +inductive ParserName + | category (cat : Name) + | parser (decl : Name) (isDescr : Bool) + -- TODO(gabriel): add parser aliases (this is blocked on doing IO in parsers) + deriving Repr + +/-- Resolve the given parser name and return a list of candidates. -/ +def resolveParserNameCore (env : Environment) (currNamespace : Name) + (openDecls : List OpenDecl) (ident : Ident) : List ParserName := Id.run do + let ⟨.ident (val := val) (preresolved := pre) ..⟩ := ident | return [] + + let rec isParser (name : Name) : Option Bool := + (env.find? name).bind fun ci => + match ci.type with + | .const ``Parser _ | .const ``TrailingParser _ => some false + | .const ``ParserDescr _ | .const ``TrailingParserDescr _ => some true + | _ => none + + for pre in pre do + if let .decl n [] := pre then + if let some isDescr := isParser n then + return [.parser n isDescr] + + let erased := val.eraseMacroScopes + + if isParserCategory env erased then + return [.category erased] + + ResolveName.resolveGlobalName env currNamespace openDecls val |>.filterMap fun + | (name, []) => (isParser name).map fun isDescr => .parser name isDescr + | _ => none + +/-- Resolve the given parser name and return a list of candidates. -/ +def ParserContext.resolveParserName (ctx : ParserContext) (id : Ident) : List ParserName := + Parser.resolveParserNameCore ctx.env ctx.currNamespace ctx.openDecls id + +/-- Resolve the given parser name and return a list of candidates. -/ +def resolveParserName (id : Ident) : CoreM (List ParserName) := + return resolveParserNameCore (← getEnv) (← getCurrNamespace) (← getOpenDecls) id def parserOfStackFn (offset : Nat) : ParserFn := fun ctx s => Id.run do let stack := s.stxStack if stack.size < offset + 1 then return s.mkUnexpectedError ("failed to determine parser using syntax stack, stack is too small") - let Syntax.ident (val := parserName) .. := stack.get! (stack.size - offset - 1) + let parserName@(.ident ..) := stack.get! (stack.size - offset - 1) | s.mkUnexpectedError ("failed to determine parser using syntax stack, the specified element on the stack is not an identifier") - match ctx.resolveName parserName with - | [(parserName, [])] => + match ctx.resolveParserName ⟨parserName⟩ with + | [.category cat] => + categoryParserFn cat ctx s + | [.parser parserName _] => let iniSz := s.stackSize let mut ctx' := ctx if !internal.parseQuotWithCurrentStage.get ctx'.options then @@ -656,7 +695,7 @@ def parserOfStackFn (offset : Nat) : ParserFn := fun ctx s => Id.run do else s | _::_::_ => s.mkUnexpectedError s!"ambiguous parser name {parserName}" - | _ => s.mkUnexpectedError s!"unknown parser {parserName}" + | [] => s.mkUnexpectedError s!"unknown parser {parserName}" def parserOfStack (offset : Nat) (prec : Nat := 0) : Parser := { fn := fun c s => parserOfStackFn offset { c with prec := prec } s } diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean index 1560f9701b..1a9fb66df2 100644 --- a/src/Lean/Parser/Syntax.lean +++ b/src/Lean/Parser/Syntax.lean @@ -39,14 +39,6 @@ namespace Syntax end Syntax -namespace Term - -@[builtinTermParser] def stx.quot : Parser := leading_parser "`(stx|" >> incQuotDepth syntaxParser >> ")" -@[builtinTermParser] def prec.quot : Parser := leading_parser "`(prec|" >> incQuotDepth precedenceParser >> ")" -@[builtinTermParser] def prio.quot : Parser := leading_parser "`(prio|" >> incQuotDepth priorityParser >> ")" - -end Term - namespace Command def namedName := leading_parser (atomic ("(" >> nonReservedSymbol "name") >> " := " >> ident >> ")") @@ -75,11 +67,8 @@ def catBehaviorSymbol := leading_parser nonReservedSymbol "symbol" def catBehavior := optional ("(" >> nonReservedSymbol "behavior" >> " := " >> (catBehaviorBoth <|> catBehaviorSymbol) >> ")") @[builtinCommandParser] def syntaxCat := leading_parser optional docComment >> "declare_syntax_cat " >> ident >> catBehavior def macroArg := leading_parser optional (atomic (ident >> checkNoWsBefore "no space before ':'" >> ":")) >> syntaxParser argPrec -def macroRhs (quotP : Parser) : Parser := leading_parser "`(" >> incQuotDepth quotP >> ")" <|> withPosition termParser -def macroTailTactic : Parser := atomic (" : " >> identEq "tactic") >> darrow >> macroRhs Tactic.seq1 -def macroTailCommand : Parser := atomic (" : " >> identEq "command") >> darrow >> macroRhs (many1Unbox commandParser) -def macroTailDefault : Parser := atomic (" : " >> ident) >> darrow >> macroRhs (categoryParserOfStack 2) -def macroTail := leading_parser macroTailTactic <|> macroTailCommand <|> macroTailDefault +def macroRhs : Parser := leading_parser withPosition termParser +def macroTail := leading_parser atomic (" : " >> ident) >> darrow >> macroRhs @[builtinCommandParser] def «macro» := leading_parser suppressInsideQuot (optional docComment >> optional Term.«attributes» >> Term.attrKind >> "macro " >> optPrecedence >> optNamedName >> optNamedPrio >> many1 macroArg >> macroTail) @[builtinCommandParser] def «elab_rules» := leading_parser suppressInsideQuot (optional docComment >> optional Term.«attributes» >> Term.attrKind >> "elab_rules" >> optKind >> optional (" : " >> ident) >> optional (" <= " >> ident) >> Term.matchAlts) diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 388ab2760c..21a2643716 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -448,12 +448,8 @@ See the Chapter "Quantifiers and Equality" in the manual "Theorem Proving in Lea -/ @[builtinTermParser] def subst := trailing_parser:75 " ▸ " >> sepBy1 (termParser 75) " ▸ " --- NOTE: Doesn't call `categoryParser` directly in contrast to most other "static" quotations, so call `evalInsideQuot` explicitly -@[builtinTermParser] def funBinder.quot : Parser := leading_parser "`(funBinder|" >> incQuotDepth (evalInsideQuot ``funBinder funBinder) >> ")" def bracketedBinderF := bracketedBinder -- no default arg -@[builtinTermParser] def bracketedBinder.quot : Parser := leading_parser "`(bracketedBinder|" >> incQuotDepth (evalInsideQuot ``bracketedBinderF bracketedBinder) >> ")" -@[builtinTermParser] def matchDiscr.quot : Parser := leading_parser "`(matchDiscr|" >> incQuotDepth (evalInsideQuot ``matchDiscr matchDiscr) >> ")" -@[builtinTermParser] def attr.quot : Parser := leading_parser "`(attr|" >> incQuotDepth attrParser >> ")" +instance : Coe (TSyntax ``bracketedBinderF) (TSyntax ``bracketedBinder) where coe s := ⟨s⟩ /-- `panic! msg` formally evaluates to `@Inhabited.default α` if the expected type @@ -491,8 +487,6 @@ end Term @[builtinTermParser default+1] def Tactic.quot : Parser := leading_parser "`(tactic|" >> incQuotDepth tacticParser >> ")" @[builtinTermParser] def Tactic.quotSeq : Parser := leading_parser "`(tactic|" >> incQuotDepth Tactic.seq1 >> ")" -@[builtinTermParser] def Level.quot : Parser := leading_parser "`(level|" >> incQuotDepth levelParser >> ")" - open Term in builtin_initialize register_parser_alias letDecl diff --git a/src/Lean/Server/Rpc/Deriving.lean b/src/Lean/Server/Rpc/Deriving.lean index 4c7c0d0abc..32e95ce673 100644 --- a/src/Lean/Server/Rpc/Deriving.lean +++ b/src/Lean/Server/Rpc/Deriving.lean @@ -72,7 +72,7 @@ private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr -- create the constructor let fieldStxs ← argVars.mapM fun arg => do let name := (← getFVarLocalDecl arg).userName - `(bracketedBinder| ($(mkIdent name) : Json)) + `(bracketedBinderF| ($(mkIdent name) : Json)) let pktCtor ← `(Parser.Command.ctor| | $ctorId:ident $[$fieldStxs]* : RpcEncodablePacket) @@ -124,7 +124,7 @@ private def deriveInstance (declNames : Array Name) : CommandElabM Bool := do elabCommand <| ← liftTermElabM do forallTelescopeReducing indVal.type fun params _ => do let encInstBinders ← (← params.filterM (isType ·)).mapM fun p => do - `(bracketedBinder| [RpcEncodable $(mkIdent (← getFVarLocalDecl p).userName):ident]) + `(bracketedBinderF| [RpcEncodable $(mkIdent (← getFVarLocalDecl p).userName):ident]) if isStructure (← getEnv) typeName then deriveStructureInstance indVal params encInstBinders else diff --git a/src/lake b/src/lake index 8d98d5616b..b843041aa4 160000 --- a/src/lake +++ b/src/lake @@ -1 +1 @@ -Subproject commit 8d98d5616bacc49700f63c78c30cefd00e040686 +Subproject commit b843041aa4589ee093a67794967421e347f33482 diff --git a/tests/lean/1163.lean b/tests/lean/1163.lean index e9279e1b2c..3017c47775 100644 --- a/tests/lean/1163.lean +++ b/tests/lean/1163.lean @@ -1,7 +1,7 @@ import Lean open Lean Elab Tactic -macro "obviously1" : tactic => `(exact sorryAx _) +macro "obviously1" : tactic => `(tactic| exact sorryAx _) theorem result1 : False := by obviously1 diff --git a/tests/lean/StxQuot.lean b/tests/lean/StxQuot.lean index 1cdf9e5bee..3395477905 100644 --- a/tests/lean/StxQuot.lean +++ b/tests/lean/StxQuot.lean @@ -114,3 +114,7 @@ syntax "foo" term : term | `(a) => pure "0" | `(b) => pure "1" | _ => pure "2" + +declare_syntax_cat mycat +syntax "mystx" : mycat +#eval run `(mycat| mystx) diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out index ef52cc3dc3..892520a604 100644 --- a/tests/lean/StxQuot.lean.expected.out +++ b/tests/lean/StxQuot.lean.expected.out @@ -55,3 +55,4 @@ StxQuot.lean:108:22-108:23: error: unknown identifier 'y' at quotation precheck; "(Term.fun\n \"fun\"\n (Term.basicFun\n [`x._@.UnhygienicMain._hyg.1 `y._@.UnhygienicMain._hyg.1]\n []\n \"=>\"\n (Term.app `x._@.UnhygienicMain._hyg.1 [`y._@.UnhygienicMain._hyg.1])))" "(Term.fun\n \"fun\"\n (Term.basicFun\n [(Term.anonymousCtor \"⟨\" [`x._@.UnhygienicMain._hyg.1 \",\" `y._@.UnhygienicMain._hyg.1] \"⟩\")]\n []\n \"=>\"\n `x._@.UnhygienicMain._hyg.1))" "1" +"(mycatMystx \"mystx\")" diff --git a/tests/lean/interactive/hover.lean b/tests/lean/interactive/hover.lean index 5b6390e959..f28ac46826 100644 --- a/tests/lean/interactive/hover.lean +++ b/tests/lean/interactive/hover.lean @@ -16,7 +16,7 @@ example (n : Nat) : True := by /-- My tactic -/ -macro "mytac" o:"only"? e:term : tactic => `(exact $e) +macro "mytac" o:"only"? e:term : tactic => `(tactic| exact $e) example : True := by mytac only True.intro diff --git a/tests/lean/run/allGoals.lean b/tests/lean/run/allGoals.lean index 58074ff0cd..575b046b5e 100644 --- a/tests/lean/run/allGoals.lean +++ b/tests/lean/run/allGoals.lean @@ -39,7 +39,7 @@ theorem Weekday.nextOfPrevious'' (d : Weekday) : previous (next d) = d ∧ next apply And.intro <;> cases d <;> rfl open Lean.Parser.Tactic in -macro "rwd " x:term : tactic => `(rw [$x:term]; done) +macro "rwd " x:term : tactic => `(tactic| rw [$x:term]; done) theorem ex (a b c : α) (h₁ : a = b) (h₂ : a = c) : b = a ∧ c = a := by apply And.intro <;> first | rwd h₁ | rwd h₂ diff --git a/tests/lean/run/doNotation3.lean b/tests/lean/run/doNotation3.lean index b31ca5087a..ccccf9151b 100644 --- a/tests/lean/run/doNotation3.lean +++ b/tests/lean/run/doNotation3.lean @@ -57,7 +57,7 @@ return () #eval gTest -macro "ret!" x:term : doElem => `(return $x) +macro "ret!" x:term : doElem => `(doElem| return $x) def f1 (x : Nat) : Nat := Id.run <| do let mut x := x diff --git a/tests/lean/run/eqThm.lean b/tests/lean/run/eqThm.lean index a6aa20d52f..4cbcb76345 100644 --- a/tests/lean/run/eqThm.lean +++ b/tests/lean/run/eqThm.lean @@ -6,7 +6,7 @@ def f : Nat → Bool → Nat | x+2, true => f x true | x+2, b => f x (not b) -macro "urfl" : tactic => `(set_option smartUnfolding false in rfl) +macro "urfl" : tactic => `(tactic| set_option smartUnfolding false in rfl) theorem f_main_eq : f x b = f.match_1 (fun _ _ => Nat) x b (fun _ => 1) (fun _ => 2) (fun _ => 3) (fun _ => 4) (fun x => f x true) (fun x b => f x (not b)) := by diff --git a/tests/lean/run/impLambdaTac.lean b/tests/lean/run/impLambdaTac.lean index 40c0a8f1c1..36f875c72a 100644 --- a/tests/lean/run/impLambdaTac.lean +++ b/tests/lean/run/impLambdaTac.lean @@ -10,7 +10,7 @@ example (P : Prop) : ∀ {p : P}, P := by example (P : Prop) : ∀ {p : P}, P := by exact no_implicit_lambda% id -macro "exact'" x:term : tactic => `(exact no_implicit_lambda% $x) +macro "exact'" x:term : tactic => `(tactic| exact no_implicit_lambda% $x) example (P : Prop) : ∀ {p : P}, P := by exact' id diff --git a/tests/lean/run/macroParams.lean b/tests/lean/run/macroParams.lean index a93296807b..a21bc49067 100644 --- a/tests/lean/run/macroParams.lean +++ b/tests/lean/run/macroParams.lean @@ -2,6 +2,6 @@ macro x:ident noWs "(" ys:term,* ")" : term => `($x $ys*) #check id(1) -macro "foo" &"only" : tactic => `(trivial) +macro "foo" &"only" : tactic => `(tactic| trivial) example : True := by foo only diff --git a/tests/lean/run/maze.lean b/tests/lean/run/maze.lean index 309aaca71a..a55d9eb6e0 100644 --- a/tests/lean/run/maze.lean +++ b/tests/lean/run/maze.lean @@ -278,9 +278,10 @@ elab t1:tactic " ⟨|⟩ " t2:tactic : tactic => elab "fail" m:term : tactic => throwError m -macro "out" : tactic => `(apply escape_north ⟨|⟩ apply escape_south ⟨|⟩ - apply escape_east ⟨|⟩ apply escape_west ⟨|⟩ - fail "not currently at maze boundary") +macro "out" : tactic => `(tactic| + apply escape_north ⟨|⟩ apply escape_south ⟨|⟩ + apply escape_east ⟨|⟩ apply escape_west ⟨|⟩ + fail "not currently at maze boundary") def maze1 := ┌───┐ │▓▓▓│ diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean index b118ccc847..ddf384726b 100644 --- a/tests/lean/run/newfrontend1.lean +++ b/tests/lean/run/newfrontend1.lean @@ -63,7 +63,7 @@ by { assumption } -macro "intro3" : tactic => `(intro; intro; intro) +macro "intro3" : tactic => `(tactic| intro; intro; intro) macro "check2" x:term : command => `(#check $x #check $x) macro "foo" x:term "," y:term : term => `($x + $y + $x) @@ -228,7 +228,7 @@ by { exact h1 } -macro "blabla" : tactic => `(assumption) +macro "blabla" : tactic => `(tactic| assumption) -- Tactic head symbols do not become reserved words def blabla := 100 diff --git a/tests/lean/rwWithoutOffsetCnstrs.lean b/tests/lean/rwWithoutOffsetCnstrs.lean index 2db3af5eea..2aabb58e22 100644 --- a/tests/lean/rwWithoutOffsetCnstrs.lean +++ b/tests/lean/rwWithoutOffsetCnstrs.lean @@ -1,6 +1,6 @@ open Lean.Parser.Tactic in macro "rw0" s:rwRuleSeq : tactic => - `(rw (config := { offsetCnstrs := false }) $s:rwRuleSeq) + `(tactic| rw (config := { offsetCnstrs := false }) $s:rwRuleSeq) example (m n : Nat) : Nat.ble (n+1) (n+0) = false := by rw0 [Nat.add_zero] diff --git a/tests/lean/traceClassScopes.lean b/tests/lean/traceClassScopes.lean index 4ff8e70f55..18c153b77e 100644 --- a/tests/lean/traceClassScopes.lean +++ b/tests/lean/traceClassScopes.lean @@ -1,7 +1,7 @@ import Lean macro "t" t:interpolatedStr(term) : doElem => - `(Macro.trace[Meta.debug] $t) + `(doElem| Macro.trace[Meta.debug] $t) macro "tstcmd" : command => do t "hello" @@ -13,7 +13,7 @@ tstcmd open Lean Meta macro "r" r:interpolatedStr(term) : doElem => - `(trace[Meta.debug] $r) + `(doElem| trace[Meta.debug] $r) set_option trace.Meta.debug true in #eval show MetaM _ from do r "world" diff --git a/tests/pkg/user_attr/UserAttr/Tst.lean b/tests/pkg/user_attr/UserAttr/Tst.lean index 4c91cb3602..621bd1ee3f 100644 --- a/tests/pkg/user_attr/UserAttr/Tst.lean +++ b/tests/pkg/user_attr/UserAttr/Tst.lean @@ -36,7 +36,7 @@ example : f x = id (x + 2) := by simp simp [my_simp] -macro "my_simp" : tactic => `(simp [my_simp]) +macro "my_simp" : tactic => `(tactic| simp [my_simp]) example : f x = id (x + 2) := by my_simp