diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index 92dd3946e5..d23e9b9ac8 100644 --- a/src/Lean/Elab/Syntax.lean +++ b/src/Lean/Elab/Syntax.lean @@ -505,15 +505,6 @@ def expandMacroArgIntoSyntaxItem (stx : Syntax) : MacroM Syntax := else Macro.throwUnsupported -/- Convert `macro` head into a `syntax` command item -/ -def expandMacroHeadIntoSyntaxItem (stx : Syntax) : MacroM Syntax := - if stx.isIdent then - let info := stx.getHeadInfo.getD {} - let id := stx.getId - pure $ Syntax.node `Lean.Parser.Syntax.atom #[Syntax.mkStrLit (toString id) info] - else - expandMacroArgIntoSyntaxItem stx - /- Convert `macro` arg into a pattern element -/ def expandMacroArgIntoPattern (stx : Syntax) : MacroM Syntax := let k := stx.getKind @@ -525,13 +516,6 @@ def expandMacroArgIntoPattern (stx : Syntax) : MacroM Syntax := else Macro.throwUnsupported -/- Convert `macro` head into a pattern element -/ -def expandMacroHeadIntoPattern (stx : Syntax) : MacroM Syntax := - if stx.isIdent then - pure $ mkAtomFrom stx (toString stx.getId) - else - expandMacroArgIntoPattern stx - def expandOptPrio (stx : Syntax) : Nat := if stx.isNone then 0 @@ -545,13 +529,13 @@ def expandMacro (currNamespace : Name) (stx : Syntax) : CommandElabM Syntax := d let args := stx[4].getArgs let cat := stx[6] -- build parser - let stxPart ← liftMacroM <| expandMacroHeadIntoSyntaxItem head + let stxPart ← liftMacroM <| expandMacroArgIntoSyntaxItem head let stxParts ← liftMacroM <| args.mapM expandMacroArgIntoSyntaxItem let stxParts := #[stxPart] ++ stxParts -- kind let kind ← mkNameFromParserSyntax cat.getId (mkNullNode stxParts) -- build macro rules - let patHead ← liftMacroM <| expandMacroHeadIntoPattern head + let patHead ← liftMacroM <| expandMacroArgIntoPattern head let patArgs ← liftMacroM <| args.mapM expandMacroArgIntoPattern /- The command `syntax [] ...` adds the current namespace to the syntax node kind. So, we must include current namespace when we create a pattern for the following `macro_rules` commands. -/ @@ -595,13 +579,13 @@ def expandElab (currNamespace : Name) (stx : Syntax) : CommandElabM Syntax := do let rhs := stx[9] let catName := cat.getId -- build parser - let stxPart ← liftMacroM <| expandMacroHeadIntoSyntaxItem head + let stxPart ← liftMacroM <| expandMacroArgIntoSyntaxItem head let stxParts ← liftMacroM <| args.mapM expandMacroArgIntoSyntaxItem let stxParts := #[stxPart] ++ stxParts -- kind let kind ← mkNameFromParserSyntax cat.getId (mkNullNode stxParts) -- build pattern for `martch_syntax - let patHead ← liftMacroM <| expandMacroHeadIntoPattern head + let patHead ← liftMacroM <| expandMacroArgIntoPattern head let patArgs ← liftMacroM <| args.mapM expandMacroArgIntoPattern let pat := Syntax.node (currNamespace ++ kind) (#[patHead] ++ patArgs) let kindId := mkIdentFrom ref kind diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean index ef5d19a3c5..1dfcfbf2f7 100644 --- a/src/Lean/Parser/Syntax.lean +++ b/src/Lean/Parser/Syntax.lean @@ -69,7 +69,7 @@ def optKindPrio : Parser := optional ("[" >> (parserKindPrio <|> parserKind <|> @[builtinCommandParser] def syntaxCat := parser! "declare_syntax_cat " >> ident def macroArgSimple := parser! ident >> checkNoWsBefore "no space before ':'" >> ":" >> syntaxParser maxPrec def macroArg := strLit <|> atomic macroArgSimple -def macroHead := macroArg <|> ident +def macroHead := macroArg def macroTailTactic : Parser := atomic (" : " >> identEq "tactic") >> darrow >> ("`(" >> toggleInsideQuot Tactic.seq1 >> ")" <|> termParser) def macroTailCommand : Parser := atomic (" : " >> identEq "command") >> darrow >> ("`(" >> toggleInsideQuot (many1Unbox commandParser) >> ")" <|> termParser) def macroTailDefault : Parser := atomic (" : " >> ident) >> darrow >> (("`(" >> toggleInsideQuot (categoryParserOfStack 2) >> ")") <|> termParser) diff --git a/tests/lean/macroStack.lean b/tests/lean/macroStack.lean index 5480a9390d..aab0b96cfd 100644 --- a/tests/lean/macroStack.lean +++ b/tests/lean/macroStack.lean @@ -1,4 +1,4 @@ - +-- def f1 := if h:x then 1 else 0 @@ -10,8 +10,8 @@ if h:(x > 0) then 1 else 0 def x := <- get -macro foo! x:term:max : term => `(let x := "hello"; $x + x) -macro bla! x:term:max : term => `(fun (x : Nat) => if foo! ($x + x) < 1 then true else false) +macro "foo!" x:term:max : term => `(let x := "hello"; $x + x) +macro "bla!" x:term:max : term => `(fun (x : Nat) => if foo! ($x + x) < 1 then true else false) def f (x : Nat) := bla! x diff --git a/tests/lean/namelit.lean b/tests/lean/namelit.lean index f6ecef7e40..bafc47d9a3 100644 --- a/tests/lean/namelit.lean +++ b/tests/lean/namelit.lean @@ -1,4 +1,4 @@ - +-- #check `foo #check `foo.bla @@ -7,8 +7,8 @@ #check `«foo bla».boo.«hello world» #check `foo.«hello» -macro dummy1 : term => `(`hello) -macro dummy2 : term => `(`hello.«world !!!») +macro "dummy1" : term => `(`hello) +macro "dummy2" : term => `(`hello.«world !!!») #check dummy1 #check dummy2 diff --git a/tests/lean/run/108.lean b/tests/lean/run/108.lean index f07d647b03..9af601e3a6 100644 --- a/tests/lean/run/108.lean +++ b/tests/lean/run/108.lean @@ -1,6 +1,4 @@ - - -macro m n:ident : command => `(def $n := 1) +macro "m" n:ident : command => `(def $n := 1) m foo diff --git a/tests/lean/run/extmacro.lean b/tests/lean/run/extmacro.lean index 483bf56380..b700c16ba5 100644 --- a/tests/lean/run/extmacro.lean +++ b/tests/lean/run/extmacro.lean @@ -1,6 +1,4 @@ - - -macro ext_tactic t:tactic "=>" newT:tactic : command => `(macro_rules | `($t) => `($newT)) +macro "ext_tactic" t:tactic "=>" newT:tactic : command => `(macro_rules | `($t) => `($newT)) syntax "trivial" : tactic diff --git a/tests/lean/run/macro_macro.lean b/tests/lean/run/macro_macro.lean index 6ff125bc51..0d2758242c 100644 --- a/tests/lean/run/macro_macro.lean +++ b/tests/lean/run/macro_macro.lean @@ -1,6 +1,8 @@ +macro "mk_m " id:ident v:str n:num c:char : command => + let tk : Lean.Syntax := Lean.Syntax.mkStrLit id.getId.toString + `(macro $tk:strLit : term => `(fun (x : String) => x ++ $v ++ toString $n ++ toString $c)) - -macro mk_m id:ident v:str n:num c:char : command => `(macro $id:ident : term => `(fun (x : String) => x ++ $v ++ toString $n ++ toString $c)) +#print " ---- " mk_m foo "bla" 10 'a' mk_m boo "hello" 3 'b' diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean index 03cbf8701b..f37867c268 100644 --- a/tests/lean/run/newfrontend1.lean +++ b/tests/lean/run/newfrontend1.lean @@ -63,9 +63,9 @@ by { assumption } -macro intro3 : tactic => `(intro; intro; intro) -macro check2 x:term : command => `(#check $x #check $x) -macro foo x:term "," y:term : term => `($x + $y + $x) +macro "intro3" : tactic => `(intro; intro; intro) +macro "check2" x:term : command => `(#check $x #check $x) +macro "foo" x:term "," y:term : term => `($x + $y + $x) set_option pp.all false diff --git a/tests/lean/weirdmacro.lean b/tests/lean/weirdmacro.lean new file mode 100644 index 0000000000..44f96e72d7 --- /dev/null +++ b/tests/lean/weirdmacro.lean @@ -0,0 +1,4 @@ +macro term x:term : term => `($x) + +#check term 10 +-- 10 diff --git a/tests/lean/weirdmacro.lean.expected.out b/tests/lean/weirdmacro.lean.expected.out new file mode 100644 index 0000000000..e377c0dc13 --- /dev/null +++ b/tests/lean/weirdmacro.lean.expected.out @@ -0,0 +1,4 @@ +weirdmacro.lean:1:6: error: expected no space before ':' or string literal +weirdmacro.lean:1:30: error: elaboration function for 'antiquot' has not been implemented +weirdmacro.lean:1:32: error: expected term +weirdmacro.lean:3:7: error: unknown identifier 'term'