chore: ParserDescrNew => ParserDescr
This commit is contained in:
Leonardo de Moura
parent
4473d70366
commit
3bfc5248ca
7 changed files with 100 additions and 116 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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'
|
||||
|
||||
/-
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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}'"
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue