diff --git a/src/Lean/Elab/ElabRules.lean b/src/Lean/Elab/ElabRules.lean index af767ea8e1..07062ac698 100644 --- a/src/Lean/Elab/ElabRules.lean +++ b/src/Lean/Elab/ElabRules.lean @@ -76,20 +76,20 @@ def elabElabRulesAux (doc? : Option Syntax) (attrKind : Syntax) (k : SyntaxNodeK do elabElabRulesAux doc? attrKind (← resolveSyntaxKind kind.getId) cat? expty? alts | _ => throwUnsupportedSyntax -@[builtinMacro Lean.Parser.Command.elab] -def expandElab : Macro +@[builtinCommandElab Lean.Parser.Command.elab] +def elabElab : CommandElab | `($[$doc?:docComment]? $attrKind:attrKind elab$[:$prec?]? $[(name := $name?)]? $[(priority := $prio?)]? $args:macroArg* : $cat $[<= $expectedType?]? => $rhs) => do - let prio ← evalOptPrio prio? + let prio ← liftMacroM <| evalOptPrio prio? let (stxParts, patArgs) := (← args.mapM expandMacroArg).unzip -- name let name ← match name? with | some name => pure name.getId - | none => mkNameFromParserSyntax cat.getId (mkNullNode stxParts) - let pat := mkNode ((← Macro.getCurrNamespace) ++ name) patArgs + | none => liftMacroM <| mkNameFromParserSyntax cat.getId (mkNullNode stxParts) + let pat := mkNode ((← getCurrNamespace) ++ name) patArgs `($[$doc?:docComment]? $attrKind:attrKind syntax$[:$prec?]? (name := $(← mkIdentFromRef name)) (priority := $(quote prio)) $[$stxParts]* : $cat - $[$doc?:docComment]? elab_rules : $cat $[<= $expectedType?]? | `($pat) => $rhs) - | _ => Macro.throwUnsupported + $[$doc?:docComment]? elab_rules : $cat $[<= $expectedType?]? | `($pat) => $rhs) >>= elabCommand + | _ => throwUnsupportedSyntax end Lean.Elab.Command diff --git a/src/Lean/Elab/Macro.lean b/src/Lean/Elab/Macro.lean index 4fda0d6e01..3878a60a0a 100644 --- a/src/Lean/Elab/Macro.lean +++ b/src/Lean/Elab/Macro.lean @@ -10,19 +10,19 @@ open Lean.Syntax open Lean.Parser.Term hiding macroArg open Lean.Parser.Command -@[builtinMacro Lean.Parser.Command.macro] def expandMacro : Macro +@[builtinCommandElab Lean.Parser.Command.macro] def elabMacro : CommandElab | `($[$doc?:docComment]? $attrKind:attrKind macro%$tk$[:$prec?]? $[(name := $name?)]? $[(priority := $prio?)]? $args:macroArg* : $cat => $rhs) => do - let prio ← evalOptPrio prio? + let prio ← liftMacroM <| evalOptPrio prio? let (stxParts, patArgs) := (← args.mapM expandMacroArg).unzip -- name let name ← match name? with | some name => pure name.getId - | none => mkNameFromParserSyntax cat.getId (mkNullNode stxParts) + | none => liftMacroM <| mkNameFromParserSyntax cat.getId (mkNullNode stxParts) /- 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 := mkNode ((← Macro.getCurrNamespace) ++ name) patArgs + let pat := mkNode ((← getCurrNamespace) ++ name) patArgs let stxCmd ← `($[$doc?:docComment]? $attrKind:attrKind syntax%$tk$[:$prec?]? (name := $(← mkIdentFromRef name)) (priority := $(quote prio)) $[$stxParts]* : $cat) let macroRulesCmd ← if rhs.getArgs.size == 1 then @@ -33,7 +33,7 @@ open Lean.Parser.Command -- `rhs` is of the form `` `( $body ) `` let rhsBody := rhs[1] `($[$doc?:docComment]? macro_rules%$tk | `($pat) => `($rhsBody)) - return mkNullNode #[stxCmd, macroRulesCmd] - | _ => Macro.throwUnsupported + elabCommand <| mkNullNode #[stxCmd, macroRulesCmd] + | _ => throwUnsupportedSyntax end Lean.Elab.Command diff --git a/src/Lean/Elab/MacroArgUtil.lean b/src/Lean/Elab/MacroArgUtil.lean index 9b17e0e79b..ea65ff82fb 100644 --- a/src/Lean/Elab/MacroArgUtil.lean +++ b/src/Lean/Elab/MacroArgUtil.lean @@ -11,33 +11,49 @@ open Lean.Parser.Term hiding macroArg open Lean.Parser.Command /- Convert `macro` arg into a `syntax` command item and a pattern element -/ -def expandMacroArg (stx : Syntax) : MacroM (Syntax × Syntax) := do - let (id?, id, stx) ← match (← expandMacros stx) with +partial def expandMacroArg (stx : Syntax) : CommandElabM (Syntax × Syntax) := do + let (id?, id, stx) ← match (← liftMacroM <| expandMacros stx) with | `(macroArg| $id:ident:$stx) => pure (some id, id, stx) | `(macroArg| $stx:stx) => pure (none, (← `(x)), stx) - | _ => Macro.throwUnsupported + | _ => throwUnsupportedSyntax let pat ← match stx with - | `(stx| $s:str) => pure <| mkNode `token_antiquot #[← strLitToPattern s, mkAtom "%", mkAtom "$", id] - | `(stx| &$s:str) => pure <| mkNode `token_antiquot #[← strLitToPattern s, mkAtom "%", mkAtom "$", id] - | `(stx| optional($_)) => pure <| mkSplicePat `optional id "?" - | `(stx| many($_)) => pure <| mkSplicePat `many id "*" - | `(stx| many1($_)) => pure <| mkSplicePat `many id "*" - | `(stx| sepBy($_, $sep:str $[, $stxsep]? $[, allowTrailingSep]?)) => - pure <| mkSplicePat `sepBy id ((isStrLit? sep).get! ++ "*") - | `(stx| sepBy1($_, $sep:str $[, $stxsep]? $[, allowTrailingSep]?)) => - pure <| mkSplicePat `sepBy id ((isStrLit? sep).get! ++ "*") + | `(stx| $s:str) => pure <| mkNode `token_antiquot #[← liftMacroM <| strLitToPattern s, mkAtom "%", mkAtom "$", id] + | `(stx| &$s:str) => pure <| mkNode `token_antiquot #[← liftMacroM <| strLitToPattern s, mkAtom "%", mkAtom "$", id] + | `(stx| optional($stx)) => mkSplicePat `optional stx id "?" + | `(stx| many($stx)) => mkSplicePat `many stx id "*" + | `(stx| many1($stx)) => mkSplicePat `many stx id "*" + | `(stx| sepBy($stx, $sep:str $[, $stxsep]? $[, allowTrailingSep]?)) => + mkSplicePat `sepBy stx id ((isStrLit? sep).get! ++ "*") + | `(stx| sepBy1($stx, $sep:str $[, $stxsep]? $[, allowTrailingSep]?)) => + mkSplicePat `sepBy stx id ((isStrLit? sep).get! ++ "*") + -- NOTE: all `interpolatedStr(·)` reuse the same node kind + | `(stx| interpolatedStr(term)) => pure <| Syntax.mkAntiquotNode interpolatedStrKind id | _ => match id? with -- if there is a binding, we assume the user knows what they are doing - | some id => - if stx.isOfKind ``Lean.Parser.Syntax.cat then - let parser := stx[0].getId.eraseMacroScopes - pure <| mkAntiquotNode id (kind := parser) (isPseudoKind := true) - else - pure <| mkAntiquotNode id + | some id => mkAntiquotNode stx id -- otherwise `group` the syntax to enforce arity 1, e.g. for `noWs` - | none => return (← `(stx| group($stx)), mkAntiquotNode id) + | none => return (← `(stx| group($stx)), (← mkAntiquotNode stx id)) pure (stx, pat) -where mkSplicePat kind id suffix := - mkNullNode #[mkAntiquotSuffixSpliceNode kind (mkAntiquotNode id) suffix] +where + mkSplicePat kind stx id suffix := + return mkNullNode #[mkAntiquotSuffixSpliceNode kind (← mkAntiquotNode stx id) suffix] + mkAntiquotNode + | `(stx| ($stx)), term => mkAntiquotNode stx term + | `(stx| $id:ident$[:$p:prec]?), term => do + let kind ← match (← Elab.Term.resolveParserName id) with + -- a syntax abbrev, assume kind == decl name + | [(c, _)] => pure c + | cs@(_ :: _ :: _) => throwError "ambiguous parser declaration {cs.map (·.1)}" + | [] => + 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 + else + throwError "unknown parser declaration/category/alias '{id}'" + pure <| Syntax.mkAntiquotNode kind term + | stx, term => + pure <| Syntax.mkAntiquotNode Name.anonymous term (isPseudoKind := true) end Lean.Elab.Command diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index 3014b45c30..b199b46678 100644 --- a/src/Lean/Elab/Syntax.lean +++ b/src/Lean/Elab/Syntax.lean @@ -57,6 +57,27 @@ 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 [] + /-- Given a `stx` of category `syntax`, return a pair `(newStx, lhsPrec?)`, where `newStx` is of category `term`. After elaboration, `newStx` should have type @@ -106,27 +127,6 @@ where let args ← args.mapIdxM fun i arg => withReader (fun ctx => { ctx with first := ctx.first && i.val == 0 }) do process arg mkParserSeq args - /- 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`. -/ - resolveParserName (parserName : Syntax) : ToParserDescrM (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 [] - ensureNoPrec (stx : Syntax) := unless stx[1].isNone do throwErrorAt stx[1] "unexpected precedence" diff --git a/src/Lean/Parser.lean b/src/Lean/Parser.lean index ba067f1d59..e9b849b1d3 100644 --- a/src/Lean/Parser.lean +++ b/src/Lean/Parser.lean @@ -22,12 +22,12 @@ builtin_initialize register_parser_alias "ws" checkWsBefore register_parser_alias "noWs" checkNoWsBefore register_parser_alias "linebreak" checkLinebreakBefore - register_parser_alias "num" numLit - register_parser_alias "str" strLit - register_parser_alias "char" charLit - register_parser_alias "name" nameLit - register_parser_alias "scientific" scientificLit - register_parser_alias ident + register_parser_alias (kind := numLitKind) "num" numLit + register_parser_alias (kind := strLitKind) "str" strLit + register_parser_alias (kind := charLitKind) "char" charLit + register_parser_alias (kind := nameLitKind) "name" nameLit + register_parser_alias (kind := scientificLitKind) "scientific" scientificLit + register_parser_alias (kind := identKind) "ident" ident register_parser_alias "colGt" checkColGt register_parser_alias "colGe" checkColGe register_parser_alias lookahead @@ -38,7 +38,7 @@ builtin_initialize register_parser_alias many1Indent register_parser_alias optional register_parser_alias withPosition - register_parser_alias interpolatedStr + register_parser_alias (kind := interpolatedStrKind) interpolatedStr register_parser_alias orelse register_parser_alias andthen diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index ad8a7c6384..64dfa21000 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -203,10 +203,13 @@ def getBinaryAlias {α} (mapRef : IO.Ref (AliasTable α)) (aliasName : Name) : I abbrev ParserAliasValue := AliasValue Parser builtin_initialize parserAliasesRef : IO.Ref (NameMap ParserAliasValue) ← IO.mkRef {} +builtin_initialize parserAlias2kindRef : IO.Ref (NameMap SyntaxNodeKind) ← IO.mkRef {} --- Later, we define macro registerParserAlias! which registers a parser, formatter and parenthesizer -def registerAlias (aliasName : Name) (p : ParserAliasValue) : IO Unit := do +-- Later, we define macro `register_parser_alias` which registers a parser, formatter and parenthesizer +def registerAlias (aliasName : Name) (p : ParserAliasValue) (kind? : Option SyntaxNodeKind := none) : IO Unit := do registerAliasCore parserAliasesRef aliasName p + if let some kind := kind? then + parserAlias2kindRef.modify (·.insert aliasName kind) instance : Coe Parser ParserAliasValue := { coe := AliasValue.const } instance : Coe (Parser → Parser) ParserAliasValue := { coe := AliasValue.unary } @@ -217,6 +220,9 @@ def isParserAlias (aliasName : Name) : IO Bool := do | some _ => pure true | _ => pure false +def getSyntaxKindOfParserAlias? (aliasName : Name) : IO (Option SyntaxNodeKind) := + return (← parserAlias2kindRef.get).find? aliasName + def ensureUnaryParserAlias (aliasName : Name) : IO Unit := discard $ getUnaryAlias parserAliasesRef aliasName diff --git a/src/Lean/Parser/Extra.lean b/src/Lean/Parser/Extra.lean index 4eb72e17b4..35f027026e 100644 --- a/src/Lean/Parser/Extra.lean +++ b/src/Lean/Parser/Extra.lean @@ -169,9 +169,11 @@ attribute [runBuiltinParserAttributeHooks] ppHardSpace ppSpace ppLine ppGroup ppRealGroup ppRealFill ppIndent ppDedent ppAllowUngrouped ppDedentIfGrouped ppHardLineUnlessUngrouped -macro "register_parser_alias" aliasName?:optional(strLit) declName:ident : term => +macro "register_parser_alias" kind?:group("(" &"kind" " := " term ")")? aliasName?:optional(strLit) declName:ident : term => do + let [(fullDeclName, [])] ← Macro.resolveGlobalName declName.getId | + Macro.throwError "expected non-overloaded constant name" let aliasName := aliasName?.getD (Syntax.mkStrLit declName.getId.toString) - `(do Parser.registerAlias $aliasName $declName + `(do Parser.registerAlias $aliasName $declName (kind? := some $(kind?.map (·[3]) |>.getD (quote fullDeclName))) PrettyPrinter.Formatter.registerAlias $aliasName $(mkIdentFrom declName (declName.getId ++ `formatter)) PrettyPrinter.Parenthesizer.registerAlias $aliasName $(mkIdentFrom declName (declName.getId ++ `parenthesizer))) diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index 08d8c829cc..eaff61d972 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -240,7 +240,7 @@ def categoryFormatterCore (cat : Name) : Formatter := do -- TODO: We could use elaborator data here to format the chosen child when available formatterForKind (← getCur).getKind else if cat == `rawStx then - withAntiquot.formatter (mkAntiquot.formatter' cat.toString none) (push stx.formatStx *> goLeft) + withAntiquot.formatter (mkAntiquot.formatter' cat.toString cat (isPseudoKind := true)) (push stx.formatStx *> goLeft) else withAntiquot.formatter (mkAntiquot.formatter' cat.toString cat (isPseudoKind := true)) (formatterForKind stx.getKind) modify fun st => { st with mustBeGrouped := true, isUngrouped := !st.mustBeGrouped } diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean index a617bfb36f..309a609f96 100644 --- a/src/Lean/Syntax.lean +++ b/src/Lean/Syntax.lean @@ -382,8 +382,7 @@ def isAntiquot : Syntax → Bool | Syntax.node _ (Name.str _ "antiquot" _) _ => true | _ => false --- TODO: `kind` should not be optional for best `TSyntax` usage -def mkAntiquotNode (term : Syntax) (nesting := 0) (name : Option String := none) (kind := `pseudo) (isPseudoKind := false) : Syntax := +def mkAntiquotNode (kind : Name) (term : Syntax) (nesting := 0) (name : Option String := none) (isPseudoKind := false) : Syntax := let nesting := mkNullNode (mkArray nesting (mkAtom "$")) let term := if term.isIdent then term