From 0c2a5580cbc08df859b77b5cc7aedf05cbd818a7 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 18 Oct 2022 10:39:25 -0700 Subject: [PATCH] feat: enforce correct syntax kind in macros --- doc/macro_overview.md | 2 +- src/Init/Conv.lean | 6 +++--- src/Init/Notation.lean | 21 +++++++++++---------- src/Init/NotationExtra.lean | 3 +++ src/Init/System/IO.lean | 2 +- src/Init/Tactics.lean | 16 ++++++++-------- src/Init/WFTactics.lean | 2 +- src/Lean/Elab/Macro.lean | 3 ++- src/lake | 2 +- tests/lean/run/allGoals.lean | 2 +- tests/lean/run/newfrontend1.lean | 2 +- tests/lean/run/precDSL.lean | 4 ++-- 12 files changed, 35 insertions(+), 30 deletions(-) diff --git a/doc/macro_overview.md b/doc/macro_overview.md index d55f5a6f19..e69c39faec 100644 --- a/doc/macro_overview.md +++ b/doc/macro_overview.md @@ -302,7 +302,7 @@ To see the desugared definition of the actual expansion, we can again use ```lean set_option trace.Elab.definition true in -macro "exfalso" : tactic => `(apply False.elim) +macro "exfalso" : tactic => `(tactic| apply False.elim) /- Results in the expansion: diff --git a/src/Init/Conv.lean b/src/Init/Conv.lean index 105e783e19..bca97e0c30 100644 --- a/src/Init/Conv.lean +++ b/src/Init/Conv.lean @@ -242,11 +242,11 @@ which only unfolds `@[reducible]` definitions). -/ macro "erw" s:rwRuleSeq : conv => `(conv| rw (config := { transparency := .default }) $s) /-- `args` traverses into all arguments. Synonym for `congr`. -/ -macro "args" : conv => `(congr) +macro "args" : conv => `(conv| congr) /-- `left` traverses into the left argument. Synonym for `lhs`. -/ -macro "left" : conv => `(lhs) +macro "left" : conv => `(conv| lhs) /-- `right` traverses into the right argument. Synonym for `rhs`. -/ -macro "right" : conv => `(rhs) +macro "right" : conv => `(conv| rhs) /-- `intro` traverses into binders. Synonym for `ext`. -/ macro "intro" xs:(colGt ident)* : conv => `(conv| ext $xs*) diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index a167f0f66b..3b52d13f15 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -110,17 +110,17 @@ end Lean Maximum precedence used in term parsers, in particular for terms in function position (`ident`, `paren`, ...) -/ -macro "max" : prec => `(1024) +macro "max" : prec => `(prec| 1024) /-- Precedence used for application arguments (`do`, `by`, ...). -/ -macro "arg" : prec => `(1023) +macro "arg" : prec => `(prec| 1023) /-- Precedence used for terms not supposed to be used as arguments (`let`, `have`, ...). -/ -macro "lead" : prec => `(1022) +macro "lead" : prec => `(prec| 1022) /-- Parentheses are used for grouping precedence expressions. -/ macro "(" p:prec ")" : prec => return p /-- Minimum precedence used in term parsers. -/ -macro "min" : prec => `(10) +macro "min" : prec => `(prec| 10) /-- `(min+1)` (we can only write `min+1` after `Meta.lean`) -/ -macro "min1" : prec => `(11) +macro "min1" : prec => `(prec| 11) /-- `max:prec` as a term. It is equivalent to `eval_prec max` for `eval_prec` defined at `Meta.lean`. We use `max_prec` to workaround bootstrapping issues. @@ -128,13 +128,13 @@ We use `max_prec` to workaround bootstrapping issues. macro "max_prec" : term => `(1024) /-- The default priority `default = 1000`, which is used when no priority is set. -/ -macro "default" : prio => `(1000) +macro "default" : prio => `(prio| 1000) /-- The standardized "low" priority `low = 100`, for things that should be lower than default priority. -/ -macro "low" : prio => `(100) +macro "low" : prio => `(prio| 100) /-- The standardized "medium" priority `med = 1000`. This is the same as `default`. -/ -macro "mid" : prio => `(1000) +macro "mid" : prio => `(prio| 1000) /-- The standardized "high" priority `high = 10000`, for things that should be higher than default priority. -/ -macro "high" : prio => `(10000) +macro "high" : prio => `(prio| 10000) /-- Parentheses are used for grouping priority expressions. -/ macro "(" p:prio ")" : prio => return p @@ -476,7 +476,8 @@ macro_rules -- Declare `this` as a keyword that unhygienically binds to a scope-less `this` assumption (or other binding). -- The keyword prevents declaring a `this` binding except through metaprogramming, as is done by `have`/`show`. /-- Special identifier introduced by "anonymous" `have : ...`, `suffices p ...` etc. -/ -macro tk:"this" : term => return Syntax.ident tk.getHeadInfo "this".toSubstring `this [] +macro tk:"this" : term => + return (⟨(Syntax.ident tk.getHeadInfo "this".toSubstring `this [])⟩ : TSyntax `term) /-- Category for carrying raw syntax trees between macros; any content is printed as is by the pretty printer. diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean index ba88703276..6a927e77bc 100644 --- a/src/Init/NotationExtra.lean +++ b/src/Init/NotationExtra.lean @@ -77,12 +77,15 @@ end Lean open Lean +section +open TSyntax.Compat macro "∃ " xs:explicitBinders ", " b:term : term => expandExplicitBinders ``Exists xs b macro "exists" xs:explicitBinders ", " b:term : term => expandExplicitBinders ``Exists xs b macro "Σ" xs:explicitBinders ", " b:term : term => expandExplicitBinders ``Sigma xs b macro "Σ'" xs:explicitBinders ", " b:term : term => expandExplicitBinders ``PSigma xs b macro:35 xs:bracketedExplicitBinders " × " b:term:35 : term => expandBrackedBinders ``Sigma xs b macro:35 xs:bracketedExplicitBinders " ×' " b:term:35 : term => expandBrackedBinders ``PSigma xs b +end -- enforce indentation of calc steps so we know when to stop parsing them syntax calcStep := ppIndent(colGe term " := " withPosition(term)) diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index 0dfc862c0a..f4d9e4be4b 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -209,7 +209,7 @@ def sleep (ms : UInt32) : BaseIO Unit := return t.get local macro "nonempty_list" : tactic => - `(exact Nat.zero_lt_succ _) + `(tactic| exact Nat.zero_lt_succ _) /-- Wait until any of the tasks in the given list has finished, then return its result. -/ @[extern "lean_io_wait_any"] opaque waitAny (tasks : @& List (Task α)) diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 55ad675de4..3f0a3fc8d7 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -257,13 +257,13 @@ syntax (name := refl) "eq_refl" : tactic This is supposed to be an extensible tactic and users can add their own support for new reflexive relations. -/ -macro "rfl" : tactic => `(eq_refl) +macro "rfl" : tactic => `(tactic| eq_refl) /-- `rfl'` is similar to `rfl`, but disables smart unfolding and unfolds all kinds of definitions, theorems included (relevant for declarations defined by well-founded recursion). -/ -macro "rfl'" : tactic => `(set_option smartUnfolding false in with_unfolding_all rfl) +macro "rfl'" : tactic => `(tactic| set_option smartUnfolding false in with_unfolding_all rfl) /-- `ac_rfl` proves equalities up to application of an associative and commutative operator. @@ -283,16 +283,16 @@ a warning whenever a proof uses `sorry`, so you aren't likely to miss it, but you can double check if a theorem depends on `sorry` by using `#print axioms my_thm` and looking for `sorryAx` in the axiom list. -/ -macro "sorry" : tactic => `(exact @sorryAx _ false) +macro "sorry" : tactic => `(tactic| exact @sorryAx _ false) /-- `admit` is a shorthand for `exact sorry`. -/ -macro "admit" : tactic => `(exact @sorryAx _ false) +macro "admit" : tactic => `(tactic| exact @sorryAx _ false) /-- `infer_instance` is an abbreviation for `exact inferInstance`. It synthesizes a value of any target type by typeclass inference. -/ -macro "infer_instance" : tactic => `(exact inferInstance) +macro "infer_instance" : tactic => `(tactic| exact inferInstance) /-- Optional configuration option for tactics -/ syntax config := atomic(" (" &"config") " := " term ")" @@ -360,7 +360,7 @@ macro (name := rwSeq) "rw" c:(config)? s:rwRuleSeq l:(location)? : tactic => match s with | `(rwRuleSeq| [$rs,*]%$rbrak) => -- We show the `rfl` state on `]` - `(tactic| rewrite $(c)? [$rs,*] $(l)?; with_annotate_state $rbrak (try (with_reducible rfl))) + `(tactic| (rewrite $(c)? [$rs,*] $(l)?; with_annotate_state $rbrak (try (with_reducible rfl)))) | _ => Macro.throwUnsupported /-- @@ -647,7 +647,7 @@ it is defined as `repeat sorry`. It is useful when working on the middle of a complex proofs, and less messy than commenting the remainder of the proof. -/ -macro "stop" tacticSeq : tactic => `(repeat sorry) +macro "stop" tacticSeq : tactic => `(tactic| repeat sorry) /-- The tactic `specialize h a₁ ... aₙ` works on local hypothesis `h`. @@ -706,7 +706,7 @@ when working on a long tactic proof, by using `save` after expensive tactics. (TODO: do this automatically and transparently so that users don't have to use this combinator explicitly.) -/ -macro (name := save) "save" : tactic => `(skip) +macro (name := save) "save" : tactic => `(tactic| skip) /-- The tactic `sleep ms` sleeps for `ms` milliseconds and does nothing. diff --git a/src/Init/WFTactics.lean b/src/Init/WFTactics.lean index 04cff0d007..c32bd34a2b 100644 --- a/src/Init/WFTactics.lean +++ b/src/Init/WFTactics.lean @@ -10,7 +10,7 @@ import Init.WF /-- Unfold definitions commonly used in well founded relation definitions. This is primarily intended for internal use in `decreasing_tactic`. -/ macro "simp_wf" : tactic => - `(simp [invImage, InvImage, Prod.lex, sizeOfWFRel, + `(tactic| simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel, WellFoundedRelation.rel]) /-- Extensible helper tactic for `decreasing_tactic`. This handles the "base case" diff --git a/src/Lean/Elab/Macro.lean b/src/Lean/Elab/Macro.lean index 2148877203..59c7fec754 100644 --- a/src/Lean/Elab/Macro.lean +++ b/src/Lean/Elab/Macro.lean @@ -33,8 +33,9 @@ open Lean.Parser.Command let macroRulesCmd ← if rhs.getArgs.size == 1 then -- `rhs` is a `term` let rhs := ⟨rhs[0]⟩ - `($[$doc?:docComment]? macro_rules | `($pat) => $rhs) + `($[$doc?:docComment]? macro_rules | `($pat) => Functor.map (@TSyntax.raw $(quote cat.getId.eraseMacroScopes)) $rhs) else + -- TODO(gabriel): remove after bootstrap -- `rhs` is of the form `` `( $body ) `` let rhsBody := ⟨rhs[1]⟩ `($[$doc?:docComment]? macro_rules | `($pat) => `($rhsBody)) diff --git a/src/lake b/src/lake index b843041aa4..8546900b81 160000 --- a/src/lake +++ b/src/lake @@ -1 +1 @@ -Subproject commit b843041aa4589ee093a67794967421e347f33482 +Subproject commit 8546900b81abb8df291d95bd615819a28b4fdc15 diff --git a/tests/lean/run/allGoals.lean b/tests/lean/run/allGoals.lean index 575b046b5e..e0b10b8d30 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 => `(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/newfrontend1.lean b/tests/lean/run/newfrontend1.lean index ddf384726b..f7f7279c1f 100644 --- a/tests/lean/run/newfrontend1.lean +++ b/tests/lean/run/newfrontend1.lean @@ -63,7 +63,7 @@ by { assumption } -macro "intro3" : tactic => `(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) diff --git a/tests/lean/run/precDSL.lean b/tests/lean/run/precDSL.lean index d933758a62..a411ff4993 100644 --- a/tests/lean/run/precDSL.lean +++ b/tests/lean/run/precDSL.lean @@ -8,8 +8,8 @@ macro_rules #check id fn x => x + 1 #check id function x => x + 1 -macro "addPrec" : prec => `(65) -macro "mulPrec" : prec => `(70) +macro "addPrec" : prec => `(prec| 65) +macro "mulPrec" : prec => `(prec| 70) infix:addPrec " +' " => Nat.add infix:mulPrec " *' " => Nat.mul