diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 1cb63d0768..05cf3974c5 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -1480,31 +1480,15 @@ instance : Inhabited ParserDescrNew := ⟨ParserDescrNew.symbol ""⟩ abbrev TrailingParserDescrNew := ParserDescrNew inductive ParserDescr - | andthen : ParserDescr → ParserDescr → ParserDescr - | orelse : ParserDescr → ParserDescr → ParserDescr - | optional : ParserDescr → ParserDescr - | lookahead : ParserDescr → ParserDescr - | «try» : ParserDescr → ParserDescr - | many : ParserDescr → ParserDescr - | many1 : ParserDescr → ParserDescr - | sepBy : ParserDescr → ParserDescr → Bool → ParserDescr - | sepBy1 : ParserDescr → ParserDescr → Bool → ParserDescr - | node : Name → Nat → ParserDescr → ParserDescr - | trailingNode : Name → Nat → ParserDescr → ParserDescr - | symbol : String → ParserDescr - | nonReservedSymbol : String → Bool → ParserDescr - | noWs : ParserDescr - | numLit : ParserDescr - | strLit : ParserDescr - | charLit : ParserDescr - | nameLit : ParserDescr - | interpolatedStr : ParserDescr → ParserDescr -- interpolated string - | ident : ParserDescr - | cat : Name → Nat → ParserDescr - | parser : Name → ParserDescr - | notFollowedBy : ParserDescr → ParserDescr - | withPosition : ParserDescr → ParserDescr - | checkCol : Bool → ParserDescr + | const (name : Name) + | unary (name : Name) (p : ParserDescr) + | binary (name : Name) (p₁ p₂ : ParserDescr) + | node (kind : SyntaxNodeKind) (prec : Nat) (p : ParserDescr) + | trailingNode (kind : SyntaxNodeKind) (prec : Nat) (p : ParserDescr) + | symbol (val : String) + | nonReservedSymbol (val : String) (includeIdent : Bool) + | cat (catName : Name) (rbp : Nat) + | parser (declName : Name) instance : Inhabited ParserDescr := ⟨ParserDescr.symbol ""⟩ abbrev TrailingParserDescr := ParserDescr diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index 1bff460719..4d274e66c7 100644 --- a/src/Lean/Elab/Syntax.lean +++ b/src/Lean/Elab/Syntax.lean @@ -27,7 +27,7 @@ private def mkParserSeq (ds : Array Syntax) : TermElabM Syntax := do else let mut r := ds[0] for d in ds[1:ds.size] do - r ← `(ParserDescrNew.binary `andthen $r $d) + r ← `(ParserDescr.binary `andthen $r $d) return r structure ToParserDescrContext := @@ -90,7 +90,7 @@ partial def toParserDescrAux (stx : Syntax) : ToParserDescrM Syntax := do let env ← getEnv if Parser.isParserCategory env cat then let prec := prec?.getD 0 - `(ParserDescrNew.cat $(quote cat) $(quote prec)) + `(ParserDescr.cat $(quote cat) $(quote prec)) else -- `cat` is not a valid category name. Thus, we test whether it is a valid constant let candidates ← resolveGlobalConst cat @@ -101,81 +101,81 @@ partial def toParserDescrAux (stx : Syntax) : ToParserDescrM Syntax := do match info.type with | Expr.const `Lean.Parser.TrailingParser _ _ => true | Expr.const `Lean.Parser.Parser _ _ => true - | Expr.const `Lean.ParserDescrNew _ _ => true - | Expr.const `Lean.TrailingParserDescrNew _ _ => true + | Expr.const `Lean.ParserDescr _ _ => true + | Expr.const `Lean.TrailingParserDescr _ _ => true | _ => false match candidates with | [] => throwErrorAt! stx[3] "unknown category '{cat}' or parser declaration" | [c] => unless prec?.isNone do throwErrorAt stx[3] "unexpected precedence" - `(ParserDescrNew.parser $(quote c)) + `(ParserDescr.parser $(quote c)) | cs => throwErrorAt! stx[3] "ambiguous parser declaration {cs}" else if kind == `Lean.Parser.Syntax.atom then match stx[0].isStrLit? with | some atom => if (← read).leadingIdentAsSymbol then - `(ParserDescrNew.nonReservedSymbol $(quote atom) false) + `(ParserDescr.nonReservedSymbol $(quote atom) false) else - `(ParserDescrNew.symbol $(quote atom)) + `(ParserDescr.symbol $(quote atom)) | none => throwUnsupportedSyntax else if kind == `Lean.Parser.Syntax.num then - `(ParserDescrNew.const `num) + `(ParserDescr.const `num) else if kind == `Lean.Parser.Syntax.str then - `(ParserDescrNew.const `str) + `(ParserDescr.const `str) else if kind == `Lean.Parser.Syntax.char then - `(ParserDescrNew.const `char) + `(ParserDescr.const `char) else if kind == `Lean.Parser.Syntax.ident then - `(ParserDescrNew.const `ident) + `(ParserDescr.const `ident) else if kind == `Lean.Parser.Syntax.noWs then - `(ParserDescrNew.const `noWs) + `(ParserDescr.const `noWs) else if kind == `Lean.Parser.Syntax.try then let d ← withoutLeftRec $ toParserDescrAux stx[1] - `(ParserDescrNew.unary `try $d) + `(ParserDescr.unary `try $d) else if kind == `Lean.Parser.Syntax.withPosition then let d ← withoutLeftRec $ toParserDescrAux stx[1] - `(ParserDescrNew.unary `withPosition $d) + `(ParserDescr.unary `withPosition $d) else if kind == `Lean.Parser.Syntax.checkColGt then - `(ParserDescrNew.const `colGt) + `(ParserDescr.const `colGt) else if kind == `Lean.Parser.Syntax.checkColGe then - `(ParserDescrNew.const `colGe) + `(ParserDescr.const `colGe) else if kind == `Lean.Parser.Syntax.notFollowedBy then let d ← withoutLeftRec $ toParserDescrAux stx[1] - `(ParserDescrNew.unary `notFollowedBy $d) + `(ParserDescr.unary `notFollowedBy $d) else if kind == `Lean.Parser.Syntax.lookahead then let d ← withoutLeftRec $ toParserDescrAux stx[1] - `(ParserDescrNew.unary `lookahead $d) + `(ParserDescr.unary `lookahead $d) else if kind == `Lean.Parser.Syntax.interpolatedStr then let d ← withoutLeftRec $ toParserDescrAux stx[1] - `(ParserDescrNew.unary `interpolatedStr $d) + `(ParserDescr.unary `interpolatedStr $d) else if kind == `Lean.Parser.Syntax.sepBy then let allowTrailingSep := !stx[1].isNone let d₁ ← withoutLeftRec $ toParserDescrAux stx[2] let d₂ ← withoutLeftRec $ toParserDescrAux stx[3] if allowTrailingSep then - `(ParserDescrNew.binary `sepByT $d₁ $d₂) + `(ParserDescr.binary `sepByT $d₁ $d₂) else - `(ParserDescrNew.binary `sepBy $d₁ $d₂) + `(ParserDescr.binary `sepBy $d₁ $d₂) else if kind == `Lean.Parser.Syntax.sepBy1 then let allowTrailingSep := !stx[1].isNone let d₁ ← withoutLeftRec $ toParserDescrAux stx[2] let d₂ ← withoutLeftRec $ toParserDescrAux stx[3] if allowTrailingSep then - `(ParserDescrNew.binary `sepByT $d₁ $d₂) + `(ParserDescr.binary `sepByT $d₁ $d₂) else - `(ParserDescrNew.binary `sepBy1 $d₁ $d₂) + `(ParserDescr.binary `sepBy1 $d₁ $d₂) else if kind == `Lean.Parser.Syntax.many then let d ← withoutLeftRec $ toParserDescrAux stx[0] - `(ParserDescrNew.unary `many $d) + `(ParserDescr.unary `many $d) else if kind == `Lean.Parser.Syntax.many1 then let d ← withoutLeftRec $ toParserDescrAux stx[0] - `(ParserDescrNew.unary `many1 $d) + `(ParserDescr.unary `many1 $d) else if kind == `Lean.Parser.Syntax.optional then let d ← withoutLeftRec $ toParserDescrAux stx[0] - `(ParserDescrNew.unary `optional $d) + `(ParserDescr.unary `optional $d) else if kind == `Lean.Parser.Syntax.orelse then let d₁ ← withoutLeftRec $ toParserDescrAux stx[0] let d₂ ← withoutLeftRec $ toParserDescrAux stx[2] - `(ParserDescrNew.binary `orelse $d₁ $d₂) + `(ParserDescr.binary `orelse $d₁ $d₂) else let stxNew? ← liftM (liftMacroM (expandMacro? stx) : TermElabM _) match stxNew? with @@ -204,10 +204,10 @@ private def declareSyntaxCatQuotParser (catName : Name) : CommandElabM Unit := d let quotSymbol := "`(" ++ getCatSuffix catName ++ "|" let kind := catName ++ `quot let cmd ← `( - @[termParser] def $(mkIdent kind) : Lean.ParserDescrNew := - Lean.ParserDescrNew.node $(quote kind) $(quote Lean.Parser.maxPrec) - (Lean.ParserDescrNew.binary `andthen (Lean.ParserDescrNew.symbol $(quote quotSymbol)) - (Lean.ParserDescrNew.binary `andthen (Lean.ParserDescrNew.cat $(quote catName) 0) (Lean.ParserDescrNew.symbol ")")))) + @[termParser] def $(mkIdent kind) : Lean.ParserDescr := + Lean.ParserDescr.node $(quote kind) $(quote Lean.Parser.maxPrec) + (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol $(quote quotSymbol)) + (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.cat $(quote catName) 0) (Lean.ParserDescr.symbol ")")))) elabCommand cmd @[builtinCommandElab syntaxCat] def elabDeclareSyntaxCat : CommandElab := fun stx => do @@ -280,11 +280,11 @@ def «syntax» := parser! "syntax " >> optPrecedence >> optKindPrio >> many let (val, trailingParser) ← runTermElabM none fun _ => Term.toParserDescr syntaxParser cat let d ← if trailingParser then - `(@[$catParserId:ident $(quote prio):numLit] def $(mkIdentFrom stx kind) : Lean.TrailingParserDescrNew := - ParserDescrNew.trailingNode $(quote stxNodeKind) $(quote prec) $val) + `(@[$catParserId:ident $(quote prio):numLit] def $(mkIdentFrom stx kind) : Lean.TrailingParserDescr := + ParserDescr.trailingNode $(quote stxNodeKind) $(quote prec) $val) else - `(@[$catParserId:ident $(quote prio):numLit] def $(mkIdentFrom stx kind) : Lean.ParserDescrNew := - ParserDescrNew.node $(quote stxNodeKind) $(quote prec) $val) + `(@[$catParserId:ident $(quote prio):numLit] def $(mkIdentFrom stx kind) : Lean.ParserDescr := + ParserDescr.node $(quote stxNodeKind) $(quote prec) $val) trace `Elab fun _ => d withMacroExpansion stx d $ elabCommand d @@ -294,7 +294,7 @@ def syntaxAbbrev := parser! "syntax " >> ident >> " := " >> many1 syntaxParser @[builtinCommandElab «syntaxAbbrev»] def elabSyntaxAbbrev : CommandElab := fun stx => do let declName := stx[1] let (val, _) ← runTermElabM none $ fun _ => Term.toParserDescr stx[3] Name.anonymous - let stx' ← `(def $declName : Lean.ParserDescrNew := $val) + let stx' ← `(def $declName : Lean.ParserDescr := $val) withMacroExpansion stx stx' $ elabCommand stx' /- diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index 243d109f7c..812917d548 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -163,7 +163,7 @@ private def ParserExtensionAddEntry (s : ParserExtensionState) (e : ParserExtens | _ => unreachable! unsafe def mkParserOfConstantUnsafe - (categories : ParserCategories) (constName : Name) (compileParserDescr : ParserDescrNew → ImportM Parser) : ImportM (Bool × Parser) := do + (categories : ParserCategories) (constName : Name) (compileParserDescr : ParserDescr → ImportM Parser) : ImportM (Bool × Parser) := do let env := (← read).env let opts := (← read).opts match env.find? constName with @@ -176,19 +176,19 @@ unsafe def mkParserOfConstantUnsafe | Expr.const `Lean.Parser.Parser _ _ => let p ← IO.ofExcept $ env.evalConst Parser opts constName pure ⟨true, p⟩ - | Expr.const `Lean.ParserDescrNew _ _ => - let d ← IO.ofExcept $ env.evalConst ParserDescrNew opts constName + | Expr.const `Lean.ParserDescr _ _ => + let d ← IO.ofExcept $ env.evalConst ParserDescr opts constName let p ← compileParserDescr d pure ⟨true, p⟩ - | Expr.const `Lean.TrailingParserDescrNew _ _ => - let d ← IO.ofExcept $ env.evalConst TrailingParserDescrNew opts constName + | Expr.const `Lean.TrailingParserDescr _ _ => + let d ← IO.ofExcept $ env.evalConst TrailingParserDescr opts constName let p ← compileParserDescr d pure ⟨false, p⟩ | _ => throw ↑s!"unexpected parser type at '{constName}' (`ParserDescr`, `TrailingParserDescr`, `Parser` or `TrailingParser` expected" @[implementedBy mkParserOfConstantUnsafe] constant mkParserOfConstantAux - (categories : ParserCategories) (constName : Name) (compileParserDescr : ParserDescrNew → ImportM Parser) : ImportM (Bool × Parser) + (categories : ParserCategories) (constName : Name) (compileParserDescr : ParserDescr → ImportM Parser) : ImportM (Bool × Parser) /- Parser aliases for making `ParserDescr` extensible -/ inductive AliasValue (α : Type) @@ -258,19 +258,19 @@ builtin_initialize registerParserAliasCore "sepByT" (AliasValue.binary (sepBy (allowTrailingSep := true))) registerParserAliasCore "sepBy1T" (AliasValue.binary (sepBy1 (allowTrailingSep := true))) -partial def compileParserDescr (categories : ParserCategories) (d : ParserDescrNew) : ImportM Parser := - let rec visit : ParserDescrNew → ImportM Parser - | ParserDescrNew.const n => getConstAlias parserAliasesRef n - | ParserDescrNew.unary n d => return (← getUnaryAlias parserAliasesRef n) (← visit d) - | ParserDescrNew.binary n d₁ d₂ => return (← getBinaryAlias parserAliasesRef n) (← visit d₁) (← visit d₂) - | ParserDescrNew.node k prec d => return leadingNode k prec (← visit d) - | ParserDescrNew.trailingNode k prec d => return trailingNode k prec (← visit d) - | ParserDescrNew.symbol tk => return symbol tk - | ParserDescrNew.nonReservedSymbol tk includeIdent => return nonReservedSymbol tk includeIdent - | ParserDescrNew.parser constName => do +partial def compileParserDescr (categories : ParserCategories) (d : ParserDescr) : ImportM Parser := + let rec visit : ParserDescr → ImportM Parser + | ParserDescr.const n => getConstAlias parserAliasesRef n + | ParserDescr.unary n d => return (← getUnaryAlias parserAliasesRef n) (← visit d) + | ParserDescr.binary n d₁ d₂ => return (← getBinaryAlias parserAliasesRef n) (← visit d₁) (← visit d₂) + | ParserDescr.node k prec d => return leadingNode k prec (← visit d) + | ParserDescr.trailingNode k prec d => return trailingNode k prec (← visit d) + | ParserDescr.symbol tk => return symbol tk + | ParserDescr.nonReservedSymbol tk includeIdent => return nonReservedSymbol tk includeIdent + | ParserDescr.parser constName => do let (_, p) ← mkParserOfConstantAux categories constName visit; pure p - | ParserDescrNew.cat catName prec => + | ParserDescr.cat catName prec => match getCategory categories catName with | some _ => pure $ categoryParser catName prec | none => IO.ofExcept $ throwUnknownParserCategory catName diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean index 61e64b20d0..14834dcbb4 100644 --- a/src/Lean/ParserCompiler.lean +++ b/src/Lean/ParserCompiler.lean @@ -114,25 +114,25 @@ def compileCategoryParser {α} (ctx : Context α) (declName : Name) (builtin : B addAttribute c' (if builtin then ctx.categoryAttr.defn.builtinName else ctx.categoryAttr.defn.name) (mkNullNode #[mkIdent kind]) variables {α} (ctx : Context α) in -def compileEmbeddedParsers : ParserDescrNew → MetaM Unit - | ParserDescrNew.const _ => pure () - | ParserDescrNew.unary _ d => compileEmbeddedParsers d - | ParserDescrNew.binary _ d₁ d₂ => compileEmbeddedParsers d₁ *> compileEmbeddedParsers d₂ - | ParserDescrNew.parser constName => discard $ compileParserExpr ctx (mkConst constName) (force := false) - | ParserDescrNew.node _ _ d => compileEmbeddedParsers d - | ParserDescrNew.trailingNode _ _ d => compileEmbeddedParsers d - | ParserDescrNew.symbol _ => pure () - | ParserDescrNew.nonReservedSymbol _ _ => pure () - | ParserDescrNew.cat _ _ => pure () +def compileEmbeddedParsers : ParserDescr → MetaM Unit + | ParserDescr.const _ => pure () + | ParserDescr.unary _ d => compileEmbeddedParsers d + | ParserDescr.binary _ d₁ d₂ => compileEmbeddedParsers d₁ *> compileEmbeddedParsers d₂ + | ParserDescr.parser constName => discard $ compileParserExpr ctx (mkConst constName) (force := false) + | ParserDescr.node _ _ d => compileEmbeddedParsers d + | ParserDescr.trailingNode _ _ d => compileEmbeddedParsers d + | ParserDescr.symbol _ => pure () + | ParserDescr.nonReservedSymbol _ _ => pure () + | ParserDescr.cat _ _ => pure () /-- Precondition: `α` must match `ctx.tyName`. -/ unsafe def registerParserCompiler {α} (ctx : Context α) : IO Unit := do Parser.registerParserAttributeHook { postAdd := fun catName constName builtin => do let info ← getConstInfo constName - if info.type.isConstOf `Lean.ParserDescrNew || info.type.isConstOf `Lean.TrailingParserDescrNew then - let d ← evalConstCheck ParserDescrNew `Lean.ParserDescrNew constName <|> - evalConstCheck TrailingParserDescrNew `Lean.TrailingParserDescrNew constName + if info.type.isConstOf `Lean.ParserDescr || info.type.isConstOf `Lean.TrailingParserDescr then + let d ← evalConstCheck ParserDescr `Lean.ParserDescr constName <|> + evalConstCheck TrailingParserDescr `Lean.TrailingParserDescr constName compileEmbeddedParsers ctx d $.run' else if catName.isAnonymous then diff --git a/src/Lean/PrettyPrinter/Basic.lean b/src/Lean/PrettyPrinter/Basic.lean index 1e7f420cc5..11ce863f89 100644 --- a/src/Lean/PrettyPrinter/Basic.lean +++ b/src/Lean/PrettyPrinter/Basic.lean @@ -13,14 +13,14 @@ namespace PrettyPrinter See `orelse.parenthesizer` for example -/ builtin_initialize backtrackExceptionId : InternalExceptionId ← registerInternalExceptionId `backtrackFormatter -unsafe def runForNodeKind {α} (attr : KeyedDeclsAttribute α) (k : SyntaxNodeKind) (interp : ParserDescrNew → CoreM α) : CoreM α := do +unsafe def runForNodeKind {α} (attr : KeyedDeclsAttribute α) (k : SyntaxNodeKind) (interp : ParserDescr → CoreM α) : CoreM α := do match attr.getValues (← getEnv) k with | p::_ => pure p | _ => -- assume `k` is from a `ParserDescr`, in which case we assume it's also the declaration name let info ← getConstInfo k - if info.type.isConstOf `Lean.ParserDescrNew || info.type.isConstOf `Lean.TrailingParserDescrNew then - let d ← evalConst ParserDescrNew k + if info.type.isConstOf `Lean.ParserDescr || info.type.isConstOf `Lean.TrailingParserDescr then + let d ← evalConst ParserDescr k interp d else throwError! "no declaration of attribute [{attr.defn.name}] found for '{k}'" diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index 1fa9b9e1fd..8bb47e05ae 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -158,7 +158,7 @@ constant mkAntiquot.formatter' (name : String) (kind : Option SyntaxNodeKind) (a -- break up big mutual recursion @[extern "lean_pretty_printer_formatter_interpret_parser_descr"] -constant interpretParserDescr' : ParserDescrNew → CoreM Formatter := arbitrary _ +constant interpretParserDescr' : ParserDescr → CoreM Formatter := arbitrary _ unsafe def formatterForKindUnsafe (k : SyntaxNodeKind) : Formatter := do (← liftM $ runForNodeKind formatterAttribute k interpretParserDescr') @@ -433,16 +433,16 @@ builtin_initialize registerFormatterAlias "sepBy1T" (AliasValue.binary sepBy1.formatter) @[export lean_pretty_printer_formatter_interpret_parser_descr] -unsafe def interpretParserDescr : ParserDescrNew → CoreM Formatter - | ParserDescrNew.const n => liftIO $ getConstAlias formatterAliasesRef n - | ParserDescrNew.unary n d => return (← liftIO $ getUnaryAlias formatterAliasesRef n) (← interpretParserDescr d) - | ParserDescrNew.binary n d₁ d₂ => return (← liftIO $ getBinaryAlias formatterAliasesRef n) (← interpretParserDescr d₁) (← interpretParserDescr d₂) - | ParserDescrNew.node k prec d => return node.formatter k (← interpretParserDescr d) - | ParserDescrNew.trailingNode k prec d => return trailingNode.formatter k prec (← interpretParserDescr d) - | ParserDescrNew.symbol tk => return symbol.formatter tk - | ParserDescrNew.nonReservedSymbol tk includeIdent => return nonReservedSymbol.formatter tk - | ParserDescrNew.parser constName => combinatorFormatterAttribute.runDeclFor constName - | ParserDescrNew.cat catName prec => return categoryParser.formatter catName +unsafe def interpretParserDescr : ParserDescr → CoreM Formatter + | ParserDescr.const n => liftIO $ getConstAlias formatterAliasesRef n + | ParserDescr.unary n d => return (← liftIO $ getUnaryAlias formatterAliasesRef n) (← interpretParserDescr d) + | ParserDescr.binary n d₁ d₂ => return (← liftIO $ getBinaryAlias formatterAliasesRef n) (← interpretParserDescr d₁) (← interpretParserDescr d₂) + | ParserDescr.node k prec d => return node.formatter k (← interpretParserDescr d) + | ParserDescr.trailingNode k prec d => return trailingNode.formatter k prec (← interpretParserDescr d) + | ParserDescr.symbol tk => return symbol.formatter tk + | ParserDescr.nonReservedSymbol tk includeIdent => return nonReservedSymbol.formatter tk + | ParserDescr.parser constName => combinatorFormatterAttribute.runDeclFor constName + | ParserDescr.cat catName prec => return categoryParser.formatter catName end Formatter open Formatter diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index 333ce1de88..a81ec748d1 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -270,7 +270,7 @@ def throwError {α} (msg : MessageData) : ParenthesizerM α := -- break up big mutual recursion @[extern "lean_pretty_printer_parenthesizer_interpret_parser_descr"] -constant interpretParserDescr' : ParserDescrNew → CoreM Parenthesizer := arbitrary _ +constant interpretParserDescr' : ParserDescr → CoreM Parenthesizer := arbitrary _ unsafe def parenthesizerForKindUnsafe (k : SyntaxNodeKind) : Parenthesizer := do (← liftM $ runForNodeKind parenthesizerAttribute k interpretParserDescr') @@ -512,16 +512,16 @@ builtin_initialize registerParenthesizerAlias "sepBy1T" (AliasValue.binary sepBy1.parenthesizer) @[export lean_pretty_printer_parenthesizer_interpret_parser_descr] -unsafe def interpretParserDescr : ParserDescrNew → CoreM Parenthesizer - | ParserDescrNew.const n => liftIO $ getConstAlias parenthesizerAliasesRef n - | ParserDescrNew.unary n d => return (← liftIO $ getUnaryAlias parenthesizerAliasesRef n) (← interpretParserDescr d) - | ParserDescrNew.binary n d₁ d₂ => return (← liftIO $ getBinaryAlias parenthesizerAliasesRef n) (← interpretParserDescr d₁) (← interpretParserDescr d₂) - | ParserDescrNew.node k prec d => return leadingNode.parenthesizer k prec (← interpretParserDescr d) - | ParserDescrNew.trailingNode k prec d => return trailingNode.parenthesizer k prec (← interpretParserDescr d) - | ParserDescrNew.symbol tk => return symbol.parenthesizer tk - | ParserDescrNew.nonReservedSymbol tk includeIdent => return nonReservedSymbol.parenthesizer tk includeIdent - | ParserDescrNew.parser constName => combinatorParenthesizerAttribute.runDeclFor constName - | ParserDescrNew.cat catName prec => return categoryParser.parenthesizer catName prec +unsafe def interpretParserDescr : ParserDescr → CoreM Parenthesizer + | ParserDescr.const n => liftIO $ getConstAlias parenthesizerAliasesRef n + | ParserDescr.unary n d => return (← liftIO $ getUnaryAlias parenthesizerAliasesRef n) (← interpretParserDescr d) + | ParserDescr.binary n d₁ d₂ => return (← liftIO $ getBinaryAlias parenthesizerAliasesRef n) (← interpretParserDescr d₁) (← interpretParserDescr d₂) + | ParserDescr.node k prec d => return leadingNode.parenthesizer k prec (← interpretParserDescr d) + | ParserDescr.trailingNode k prec d => return trailingNode.parenthesizer k prec (← interpretParserDescr d) + | ParserDescr.symbol tk => return symbol.parenthesizer tk + | ParserDescr.nonReservedSymbol tk includeIdent => return nonReservedSymbol.parenthesizer tk includeIdent + | ParserDescr.parser constName => combinatorParenthesizerAttribute.runDeclFor constName + | ParserDescr.cat catName prec => return categoryParser.parenthesizer catName prec end Parenthesizer open Parenthesizer