From d15e2b37568872bca1fef4cceb1dbf28c495b5dc Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 24 Apr 2021 11:25:08 +0200 Subject: [PATCH] refactor: make `notation` and `macro` macros again --- src/Lean/Elab/Attributes.lean | 8 ++--- src/Lean/Elab/DefView.lean | 4 +-- src/Lean/Elab/Syntax.lean | 63 ++++++++++++++++------------------- src/Lean/Elab/Util.lean | 13 ++++---- 4 files changed, 40 insertions(+), 48 deletions(-) diff --git a/src/Lean/Elab/Attributes.lean b/src/Lean/Elab/Attributes.lean index 9e39d984a2..dade21c8e3 100644 --- a/src/Lean/Elab/Attributes.lean +++ b/src/Lean/Elab/Attributes.lean @@ -30,12 +30,12 @@ instance : Inhabited Attribute where attrKind := leading_parser optional («scoped» <|> «local») ``` -/ -def toAttributeKind [Monad m] [MonadResolveName m] [MonadError m] (attrKindStx : Syntax) : m AttributeKind := do +def toAttributeKind (attrKindStx : Syntax) : MacroM AttributeKind := do if attrKindStx[0].isNone then return AttributeKind.global else if attrKindStx[0][0].getKind == ``Lean.Parser.Term.scoped then - if (← getCurrNamespace).isAnonymous then - throwError "scoped attributes must be used inside namespaces" + if (← Macro.getCurrNamespace).isAnonymous then + throw <| Macro.Exception.error (← getRef) "scoped attributes must be used inside namespaces" return AttributeKind.scoped else return AttributeKind.local @@ -45,7 +45,7 @@ def mkAttrKindGlobal : Syntax := def elabAttr {m} [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMacroAdapter m] [MonadRecDepth m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] (attrInstance : Syntax) : m Attribute := do /- attrInstance := ppGroup $ leading_parser attrKind >> attrParser -/ - let attrKind ← toAttributeKind attrInstance[0] + let attrKind ← liftMacroM <| toAttributeKind attrInstance[0] let attr := attrInstance[1] let attr ← liftMacroM <| expandMacros attr let attrName ← diff --git a/src/Lean/Elab/DefView.lean b/src/Lean/Elab/DefView.lean index a4456c34dc..3c6ae9e450 100644 --- a/src/Lean/Elab/DefView.lean +++ b/src/Lean/Elab/DefView.lean @@ -120,7 +120,7 @@ partial def main (type : Syntax) : CommandElabM Name := do if str.isEmpty then mkFreshInstanceName else - mkUnusedBaseName <| Name.mkSimple ("inst" ++ str) + liftMacroM <| mkUnusedBaseName <| Name.mkSimple ("inst" ++ str) end MkInstanceName @@ -139,7 +139,7 @@ def mkDefViewOfConstant (modifiers : Modifiers) (stx : Syntax) : CommandElabM De def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView := do -- leading_parser Term.attrKind >> "instance " >> optNamedPrio >> optional declId >> declSig >> declVal - let attrKind ← toAttributeKind stx[0] + let attrKind ← liftMacroM <| toAttributeKind stx[0] let prio ← liftMacroM <| expandOptNamedPrio stx[2] let attrStx ← `(attr| instance $(quote prio):numLit) let (binders, type) := expandDeclSig stx[4] diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index 0971afe269..015145a4a3 100644 --- a/src/Lean/Elab/Syntax.lean +++ b/src/Lean/Elab/Syntax.lean @@ -240,7 +240,7 @@ private def declareSyntaxCatQuotParser (catName : Name) : CommandElabM Unit := d ``` It generates the names `term_+_` and `term[_,]` -/ -partial def mkNameFromParserSyntax (catName : Name) (stx : Syntax) : CommandElabM Name := +partial def mkNameFromParserSyntax (catName : Name) (stx : Syntax) : MacroM Name := do mkUnusedBaseName <| Name.mkSimple <| appendCatName <| visit stx "" where visit (stx : Syntax) (acc : String) : String := @@ -295,7 +295,7 @@ private partial def isAtomLikeSyntax (stx : Syntax) : Bool := | none => precDefault let name ← match name? with | some name => pure name.getId - | none => mkNameFromParserSyntax cat syntaxParser + | none => liftMacroM <| mkNameFromParserSyntax cat syntaxParser let prio ← liftMacroM <| evalOptPrio prio? let stxNodeKind := (← getCurrNamespace) ++ name let catParserId := mkIdentFrom stx (cat.appendAfter "Parser") @@ -422,14 +422,14 @@ private partial def antiquote (vars : Array Syntax) : Syntax → Syntax | stx => stx /- Convert `notation` command lhs item into a `syntax` command item -/ -def expandNotationItemIntoSyntaxItem (stx : Syntax) : CommandElabM Syntax := +def expandNotationItemIntoSyntaxItem (stx : Syntax) : MacroM Syntax := let k := stx.getKind if k == `Lean.Parser.Command.identPrec then pure $ Syntax.node `Lean.Parser.Syntax.cat #[mkIdentFrom stx `term, stx[1]] else if k == strLitKind then pure $ Syntax.node `Lean.Parser.Syntax.atom #[stx] else - throwUnsupportedSyntax + Macro.throwUnsupported def strLitToPattern (stx: Syntax) : MacroM Syntax := match stx.isStrLit? with @@ -437,22 +437,22 @@ def strLitToPattern (stx: Syntax) : MacroM Syntax := | none => Macro.throwUnsupported /- Convert `notation` command lhs item into a pattern element -/ -def expandNotationItemIntoPattern (stx : Syntax) : CommandElabM Syntax := +def expandNotationItemIntoPattern (stx : Syntax) : MacroM Syntax := let k := stx.getKind if k == `Lean.Parser.Command.identPrec then mkAntiquotNode stx[0] else if k == strLitKind then - liftMacroM <| strLitToPattern stx + strLitToPattern stx else - throwUnsupportedSyntax + Macro.throwUnsupported /-- Try to derive a `SimpleDelab` from a notation. The notation must be of the form `notation ... => c var_1 ... var_n` where `c` is a declaration in the current scope and the `var_i` are a permutation of the LHS vars. -/ -def mkSimpleDelab (attrKind : Syntax) (vars : Array Syntax) (pat qrhs : Syntax) : OptionT CommandElabM Syntax := do +def mkSimpleDelab (attrKind : Syntax) (vars : Array Syntax) (pat qrhs : Syntax) : OptionT MacroM Syntax := do match qrhs with | `($c:ident $args*) => - let [(c, [])] ← resolveGlobalName c.getId | failure + let [(c, [])] ← Macro.resolveGlobalName c.getId | failure guard <| args.all (Syntax.isIdent ∘ getAntiquotTerm) guard <| args.allDiff -- replace head constant with (unused) antiquotation so we're not dependent on the exact pretty printing of the head @@ -461,13 +461,13 @@ def mkSimpleDelab (attrKind : Syntax) (vars : Array Syntax) (pat qrhs : Syntax) | `($qrhs) => `($pat) | _ => throw ()) | `($c:ident) => - let [(c, [])] ← resolveGlobalName c.getId | failure + let [(c, [])] ← Macro.resolveGlobalName c.getId | failure `(@[$attrKind:attrKind appUnexpander $(mkIdent c):ident] def unexpand : Lean.PrettyPrinter.Unexpander := fun _ => `($pat)) | _ => failure private def expandNotationAux (ref : Syntax) - (currNamespace : Name) (attrKind : Syntax) (prec? : Option Syntax) (name? : Option Syntax) (prio? : Option Syntax) (items : Array Syntax) (rhs : Syntax) : CommandElabM Syntax := do - let prio ← liftMacroM <| evalOptPrio prio? + (currNamespace : Name) (attrKind : Syntax) (prec? : Option Syntax) (name? : Option Syntax) (prio? : Option Syntax) (items : Array Syntax) (rhs : Syntax) : MacroM Syntax := do + let prio ← evalOptPrio prio? -- build parser let syntaxParts ← items.mapM expandNotationItemIntoSyntaxItem let cat := mkIdentFrom ref `term @@ -490,15 +490,12 @@ private def expandNotationAux (ref : Syntax) | some delabDecl => mkNullNode #[stxDecl, macroDecl, delabDecl] | none => mkNullNode #[stxDecl, macroDecl] -@[builtinCommandElab «notation»] def expandNotation : CommandElab := - adaptExpander fun stx => do - let currNamespace ← getCurrNamespace - match stx with - | `($attrKind:attrKind notation $[: $prec? ]? $[(name := $name?)]? $[(priority := $prio?)]? $items* => $rhs) => - -- trigger scoped checks early and only once - let _ ← toAttributeKind attrKind - expandNotationAux stx currNamespace attrKind prec? name? prio? items rhs - | _ => throwUnsupportedSyntax +@[builtinMacro Lean.Parser.Command.notation] def expandNotation : Macro + | stx@`($attrKind:attrKind notation $[: $prec? ]? $[(name := $name?)]? $[(priority := $prio?)]? $items* => $rhs) => do + -- trigger scoped checks early and only once + let _ ← toAttributeKind attrKind + expandNotationAux stx (← Macro.getCurrNamespace) attrKind prec? name? prio? items rhs + | _ => Macro.throwUnsupported /- Convert `macro` argument into a `syntax` command item -/ def expandMacroArgIntoSyntaxItem : Macro @@ -531,28 +528,28 @@ def expandMacroArgIntoPattern (stx : Syntax) : MacroM Syntax := do /- «macro» := leading_parser suppressInsideQuot (Term.attrKind >> "macro " >> optPrecedence >> optNamedName >> optNamedPrio >> macroHead >> many macroArg >> macroTail) -/ -def expandMacro (currNamespace : Name) (stx : Syntax) : CommandElabM Syntax := do +@[builtinMacro Lean.Parser.Command.macro] def expandMacro : Macro := fun stx => do let attrKind := stx[0] let prec := stx[2].getOptional? - let name? ← liftMacroM <| expandOptNamedName stx[3] - let prio ← liftMacroM <| expandOptNamedPrio stx[4] + let name? ← expandOptNamedName stx[3] + let prio ← expandOptNamedPrio stx[4] let head := stx[5] let args := stx[6].getArgs let cat := stx[8] -- build parser - let stxPart ← liftMacroM <| expandMacroArgIntoSyntaxItem head - let stxParts ← liftMacroM <| args.mapM expandMacroArgIntoSyntaxItem + let stxPart ← expandMacroArgIntoSyntaxItem head + let stxParts ← args.mapM expandMacroArgIntoSyntaxItem let stxParts := #[stxPart] ++ stxParts -- name let name ← match name? with | some name => pure name | none => mkNameFromParserSyntax cat.getId (mkNullNode stxParts) -- build macro rules - let patHead ← liftMacroM <| expandMacroArgIntoPattern head - let patArgs ← liftMacroM <| args.mapM expandMacroArgIntoPattern + let patHead ← expandMacroArgIntoPattern head + let patArgs ← 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. -/ - let pat := Syntax.node (currNamespace ++ name) (#[patHead] ++ patArgs) + let pat := Syntax.node ((← Macro.getCurrNamespace) ++ name) (#[patHead] ++ patArgs) if stx.getArgs.size == 11 then -- `stx` is of the form `macro $head $args* : $cat => term` let rhs := stx[10] @@ -566,10 +563,6 @@ def expandMacro (currNamespace : Name) (stx : Syntax) : CommandElabM Syntax := d let macroRulesCmd ← `(macro_rules | `($pat) => `($rhsBody)) return mkNullNode #[stxCmd, macroRulesCmd] -@[builtinCommandElab «macro»] def elabMacro : CommandElab := - adaptExpander fun stx => do - expandMacro (← getCurrNamespace) stx - builtin_initialize registerTraceClass `Elab.syntax @@ -602,8 +595,8 @@ def expandElab (currNamespace : Name) (stx : Syntax) : CommandElabM Syntax := do -- name let name ← match name? with | some name => pure name - | none => mkNameFromParserSyntax cat.getId (mkNullNode stxParts) - -- build pattern for `martch_syntax + | none => liftMacroM <| mkNameFromParserSyntax cat.getId (mkNullNode stxParts) + -- build pattern for syntax `match` let patHead ← liftMacroM <| expandMacroArgIntoPattern head let patArgs ← liftMacroM <| args.mapM expandMacroArgIntoPattern let pat := Syntax.node (currNamespace ++ name) (#[patHead] ++ patArgs) diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean index 963ee5759a..c467766686 100644 --- a/src/Lean/Elab/Util.lean +++ b/src/Lean/Elab/Util.lean @@ -182,17 +182,16 @@ private def expandMacro? (env : Environment) (stx : Syntax) : MacroM (Option Syn @[inline] def adaptMacro {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m] [MonadError m] [MonadResolveName m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] (x : Macro) (stx : Syntax) : m Syntax := liftMacroM (x stx) -partial def mkUnusedBaseName [Monad m] [MonadEnv m] [MonadResolveName m] (baseName : Name) : m Name := do - let currNamespace ← getCurrNamespace - let env ← getEnv - if env.contains (currNamespace ++ baseName) then - let rec loop (idx : Nat) := +partial def mkUnusedBaseName (baseName : Name) : MacroM Name := do + let currNamespace ← Macro.getCurrNamespace + if ← Macro.hasDecl (currNamespace ++ baseName) then + let rec loop (idx : Nat) := do let name := baseName.appendIndexAfter idx - if env.contains (currNamespace ++ name) then + if ← Macro.hasDecl (currNamespace ++ name) then loop (idx+1) else name - return loop 1 + loop 1 else return baseName