chore: update stage0

stage0/src/Init/Lean/Elab/Quotation.lean

@@ -219,7 +219,7 @@ else if pat.isOfKind `Lean.Parser.Term.stxQuot then
     -- Splices should only appear inside a nullKind node, see next case
     if isAntiquotSplice quoted then unconditional $ fun _ => throwError quoted "unexpected antiquotation splice"
     else if anti.isOfKind `Lean.Parser.Term.id then { kind := kind, rhsFn :=  fun rhs => `(let $anti:id := discr; $rhs) }
-    else unconditional $ fun _ => throwError anti "syntax_match: antiquotation must be variable"
+    else unconditional $ fun _ => throwError anti ("match_syntax: antiquotation must be variable " ++ toString anti)
   | _ =>
     -- quotation is a single antiquotation splice => bind args array
     if isAntiquotSplicePat quoted then
@@ -230,7 +230,7 @@ else if pat.isOfKind `Lean.Parser.Term.stxQuot then
       let argPats := quoted.getArgs.map $ fun arg => Syntax.node `Lean.Parser.Term.stxQuot #[mkAtom "`(", arg, mkAtom ")"];
       { kind := quoted.getKind, argPats := argPats }
 else
-  unconditional $ fun _ => throwError pat "syntax_match: unexpected pattern kind"
+  unconditional $ fun _ => throwError pat ("match_syntax: unexpected pattern kind " ++ toString pat)
 
 -- Assuming that the first pattern of the alternative is taken, replace it with patterns (if any) for its
 -- child nodes.
@@ -282,7 +282,7 @@ private partial def getAntiquotVarsAux : Syntax → TermElabM (List Syntax)
     | `(($e)) => e
     | _       => anti;
     if anti.isOfKind `Lean.Parser.Term.id then pure [anti]
-    else throwError anti "syntax_match: antiquotation must be variable"
+    else throwError anti ("match_syntax: antiquotation must be variable " ++ toString anti)
   else
     List.join <$> args.toList.mapM getAntiquotVarsAux
 | _ => pure []
@@ -321,7 +321,7 @@ let alts := stx.getArg 3;
 alts ← alts.getArgs.mapM $ fun alt => do {
   let pats := alt.getArg 1;
   pat ← if pats.getArgs.size == 1 then pure $ pats.getArg 0
-    else throwError stx.val "syntax_match: expected exactly one pattern per alternative";
+    else throwError stx.val "match_syntax: expected exactly one pattern per alternative";
   let pat := if pat.isOfKind `Lean.Parser.Term.stxQuot then pat.setArg 1 $ elimAntiquotChoices $ pat.getArg 1 else pat;
   let rhs := alt.getArg 3;
   pure ([pat], rhs)

stage0/src/Init/Lean/Parser/Command.lean

@@ -9,20 +9,14 @@ import Init.Lean.Parser.Term
 namespace Lean
 namespace Parser
 
-@[init mkBuiltinParsingTablesRef]
-constant builtinCommandParsingTable : IO.Ref ParsingTables := arbitrary _
-
 @[init] def regBuiltinCommandParserAttr : IO Unit :=
-registerBuiltinParserAttribute `builtinCommandParser `Lean.Parser.builtinCommandParsingTable
+registerBuiltinParserAttribute `builtinCommandParser `command
 
-def mkCommandParserAttribute : IO ParserAttribute :=
-registerParserAttribute `commandParser "command" "command parser" (some builtinCommandParsingTable)
-
-@[init mkCommandParserAttribute]
-constant commandParserAttribute : ParserAttribute := arbitrary _
+@[init] def regCommandParserAttribute : IO Unit :=
+registerParserAttribute `commandParser `command
 
 @[inline] def commandParser {k : ParserKind} (rbp : Nat := 0) : Parser k :=
-{ fn := fun _ => commandParserAttribute.runParserFn rbp }
+categoryParser `command rbp
 
 /--
   Syntax quotation for terms and (lists of) commands. We prefer terms, so ambiguous quotations like

stage0/src/Init/Lean/Parser/Level.lean

@@ -9,20 +9,14 @@ import Init.Lean.Parser.Parser
 namespace Lean
 namespace Parser
 
-@[init mkBuiltinParsingTablesRef]
-constant builtinLevelParsingTable : IO.Ref ParsingTables := arbitrary _
-
 @[init] def regBuiltinLevelParserAttr : IO Unit :=
-registerBuiltinParserAttribute `builtinLevelParser `Lean.Parser.builtinLevelParsingTable
+registerBuiltinParserAttribute `builtinLevelParser `level
 
-def mkLevelParserAttribute : IO ParserAttribute :=
-registerParserAttribute `levelParser "level" "universe level parser" (some builtinLevelParsingTable)
-
-@[init mkLevelParserAttribute]
-constant levelParserAttribute : ParserAttribute := arbitrary _
+@[init] def regLevelParserAttribute : IO Unit :=
+registerParserAttribute `levelParser `level
 
 @[inline] def levelParser {k : ParserKind} (rbp : Nat := 0) : Parser k :=
-{ fn := fun _ => levelParserAttribute.runParserFn rbp }
+categoryParser `level rbp
 
 namespace Level
 

stage0/src/Init/Lean/Parser/Parser.lean

@@ -1261,12 +1261,12 @@ private def mkResult (s : ParserState) (iniSz : Nat) : ParserState :=
 if s.stackSize == iniSz + 1 then s
 else s.mkNode nullKind iniSz -- throw error instead?
 
-def leadingParser (kind : String) (tables : ParsingTables) : ParserFn leading :=
+def leadingParser (kind : Name) (tables : ParsingTables) : ParserFn leading :=
 fun a c s =>
   let iniSz   := s.stackSize;
   let (s, ps) := indexed tables.leadingTable c s;
   if ps.isEmpty then
-    s.mkError kind
+    s.mkError (toString kind)
   else
     let s       := longestMatchFn ps a c s;
     mkResult s iniSz
@@ -1293,7 +1293,7 @@ partial def trailingLoop (tables : ParsingTables) (rbp : Nat) (c : ParserContext
         let s    := s.popSyntax;
         trailingLoop left s
 
-def prattParser (kind : String) (tables : ParsingTables) : ParserFn leading :=
+def prattParser (kind : Name) (tables : ParsingTables) : ParserFn leading :=
 fun rbp c s =>
   let s := leadingParser kind tables rbp c s;
   if s.hasError then s
@@ -1302,15 +1302,76 @@ fun rbp c s =>
     let s    := s.popSyntax;
     trailingLoop tables rbp c left s
 
-def mkBuiltinTokenTable : IO (IO.Ref TokenTable) :=
-IO.mkRef {}
+abbrev CategoryParserFn := Name → ParserFn leading
 
-@[init mkBuiltinTokenTable]
-constant builtinTokenTable : IO.Ref TokenTable := arbitrary _
+def mkCategoryParserFnRef : IO (IO.Ref CategoryParserFn) :=
+IO.mkRef $ fun _ _ => whitespace
 
-abbrev TokenTableAttributeExtensionState := List TokenConfig × TokenTable
+@[init mkCategoryParserFnRef]
+constant categoryParserFnRef : IO.Ref CategoryParserFn := arbitrary _
 
-abbrev TokenTableAttributeExtension := PersistentEnvExtension TokenConfig TokenConfig TokenTableAttributeExtensionState
+def mkCategoryParserFnExtension : IO (EnvExtension CategoryParserFn) :=
+registerEnvExtension $ categoryParserFnRef.get
+
+@[init mkCategoryParserFnExtension]
+def categoryParserFnExtension : EnvExtension CategoryParserFn := arbitrary _
+
+def categoryParserFn (catName : Name) : ParserFn leading :=
+fun rbp ctx s => categoryParserFnExtension.getState ctx.env catName rbp ctx s
+
+def categoryParser {k} (catName : Name) (rbp : Nat) : Parser k :=
+{ fn := fun _ => categoryParserFn catName rbp }
+
+def mkBuiltinTokenTable : IO (IO.Ref TokenTable) := IO.mkRef {}
+@[init mkBuiltinTokenTable] constant builtinTokenTable : IO.Ref TokenTable := arbitrary _
+
+/- Global table with all SyntaxNodeKind's -/
+def mkBuiltinSyntaxNodeKindSetRef : IO (IO.Ref SyntaxNodeKindSet) := IO.mkRef {}
+@[init mkBuiltinSyntaxNodeKindSetRef] constant builtinSyntaxNodeKindSetRef : IO.Ref SyntaxNodeKindSet := arbitrary _
+
+abbrev ParserCategories := PersistentHashMap Name ParsingTables
+
+def mkBuiltinParserCategories : IO (IO.Ref ParserCategories) := IO.mkRef {}
+@[init mkBuiltinParserCategories] constant builtinParserCategoriesRef : IO.Ref ParserCategories := arbitrary _
+
+private def addParserCategory (categories : ParserCategories) (catName : Name) : Except String ParserCategories :=
+if categories.contains catName then
+  throw ("parser category '" ++ toString catName ++ "' has already been defined")
+else
+  pure $ categories.insert catName {}
+
+private def addBuiltinParserCategory (catName : Name) : IO Unit := do
+categories ← builtinParserCategoriesRef.get;
+categories ← IO.ofExcept $ addParserCategory categories catName;
+builtinParserCategoriesRef.set categories
+
+inductive ParserExtensionOleanEntry
+| token    (val : TokenConfig) : ParserExtensionOleanEntry
+| kind     (val : SyntaxNodeKind) : ParserExtensionOleanEntry
+| category (catName : Name)
+| parser   (catName : Name) (declName : Name) : ParserExtensionOleanEntry
+
+inductive ParserExtensionEntry
+| token    (val : TokenConfig) : ParserExtensionEntry
+| kind     (val : SyntaxNodeKind) : ParserExtensionEntry
+| category (catName : Name)
+| parser   (catName : Name) (declName : Name) (k : ParserKind) (p : Parser k) : ParserExtensionEntry
+
+structure ParserExtensionState :=
+(tokens     : TokenTable := {})
+(kinds      : SyntaxNodeKindSet := {})
+(categories : ParserCategories := {})
+(newEntries : List ParserExtensionOleanEntry := [])
+
+instance ParserExtensionState.inhabited : Inhabited ParserExtensionState := ⟨{}⟩
+
+abbrev ParserExtension := PersistentEnvExtension ParserExtensionOleanEntry ParserExtensionEntry ParserExtensionState
+
+private def ParserExtension.mkInitial : IO ParserExtensionState := do
+tokens     ← builtinTokenTable.get;
+kinds      ← builtinSyntaxNodeKindSetRef.get;
+categories ← builtinParserCategoriesRef.get;
+pure { tokens := tokens, kinds := kinds, categories := categories }
 
 private def mergePrecendences (msgPreamble : String) (sym : String) : Option Nat → Option Nat → Except String (Option Nat)
 | none,   b      => pure b
@@ -1320,111 +1381,216 @@ private def mergePrecendences (msgPreamble : String) (sym : String) : Option Nat
   else
     throw $ msgPreamble ++ "precedence mismatch for '" ++ toString sym ++ "', previous: " ++ toString a ++ ", new: " ++ toString b
 
-private def addTokenConfig (table : TokenTable) (tk : TokenConfig) : Except String TokenTable := do
+private def addTokenConfig (tokens : TokenTable) (tk : TokenConfig) : Except String TokenTable := do
 if tk.val == "" then throw "invalid empty symbol"
-else match table.find tk.val with
-  | none       => pure $ table.insert tk.val tk
+else match tokens.find tk.val with
+  | none       => pure $ tokens.insert tk.val tk
   | some oldTk => do
     lbp     ← mergePrecendences "" tk.val oldTk.lbp tk.lbp;
     lbpNoWs ← mergePrecendences "(no whitespace) " tk.val oldTk.lbpNoWs tk.lbpNoWs;
-    pure $ table.insert tk.val { lbp := lbp, lbpNoWs := lbpNoWs, .. tk }
+    pure $ tokens.insert tk.val { lbp := lbp, lbpNoWs := lbpNoWs, .. tk }
+
+def throwUnknownParserCategory {α} (catName : Name) : ExceptT String Id α :=
+throw ("unknown parser category '" ++ toString catName ++ "'")
+
+def addLeadingParser (categories : ParserCategories) (catName : Name) (parserName : Name) (p : Parser) : Except String ParserCategories :=
+let addTokens (tks : List TokenConfig) : Except String ParserCategories :=
+  match categories.find? catName with
+  | none        => throwUnknownParserCategory catName
+  | some tables =>
+    let tks    := tks.map $ fun tk => mkNameSimple tk.val;
+    let tables := tks.eraseDups.foldl (fun (tables : ParsingTables) tk => { leadingTable := tables.leadingTable.insert tk p, .. tables }) tables;
+    pure (categories.insert catName tables);
+match p.info.firstTokens with
+| FirstTokens.tokens tks    => addTokens tks
+| FirstTokens.optTokens tks => addTokens tks
+| _ => throw ("invalid parser '" ++ toString parserName ++ "', initial token is not statically known")
+
+private def addTrailingParserAux (tables : ParsingTables) (p : TrailingParser) : ParsingTables :=
+let addTokens (tks : List TokenConfig) : ParsingTables :=
+  let tks := tks.map $ fun tk => mkNameSimple tk.val;
+  tks.eraseDups.foldl (fun (tables : ParsingTables) tk => { trailingTable := tables.trailingTable.insert tk p, .. tables }) tables;
+match p.info.firstTokens with
+| FirstTokens.tokens tks    => addTokens tks
+| FirstTokens.optTokens tks => addTokens tks
+| _                         => { trailingParsers := p :: tables.trailingParsers, .. tables }
+
+def addTrailingParser (categories : ParserCategories) (catName : Name) (p : TrailingParser) : Except String ParserCategories :=
+match categories.find? catName with
+| none        => throwUnknownParserCategory catName
+| some tables => pure $ categories.insert catName (addTrailingParserAux tables p)
+
+def addParser {k} (categories : ParserCategories) (catName : Name) (declName : Name) (p : Parser k) : Except String ParserCategories :=
+match k, p with
+| leading, p  => addLeadingParser categories catName declName p
+| trailing, p => addTrailingParser categories catName p
 
 def addParserTokens (tokenTable : TokenTable) (info : ParserInfo) : Except String TokenTable :=
 let newTokens := info.collectTokens [];
 newTokens.foldlM addTokenConfig tokenTable
 
-private def mkImportedTokenTable (es : Array (Array TokenConfig)) : IO TokenTableAttributeExtensionState := do
-table ← builtinTokenTable.get;
-table ← es.foldlM
-  (fun table tokens =>
-    tokens.foldlM
-      (fun table tk => IO.ofExcept (addTokenConfig table tk))
-      table)
-  table;
-pure ([], table)
+private def updateBuiltinTokens (info : ParserInfo) (declName : Name) : IO Unit := do
+tokenTable ← builtinTokenTable.swap {};
+match addParserTokens tokenTable info with
+| Except.ok tokenTable => builtinTokenTable.set tokenTable
+| Except.error msg     => throw (IO.userError ("invalid builtin parser '" ++ toString declName ++ "', " ++ msg))
 
-private def addTokenTableEntry (s : TokenTableAttributeExtensionState) (tk : TokenConfig) : TokenTableAttributeExtensionState :=
-match addTokenConfig s.2 tk with
-| Except.ok table => (tk :: s.1, table)
-| _               => unreachable!
+def addBuiltinParser {k} (catName : Name) (declName : Name) (p : Parser k) : IO Unit := do
+categories ← builtinParserCategoriesRef.get;
+categories ← IO.ofExcept $ addParser categories catName declName p;
+builtinParserCategoriesRef.set categories;
+builtinSyntaxNodeKindSetRef.modify p.info.collectKinds;
+updateBuiltinTokens p.info declName
 
-/- We use a TokenTable attribute to make sure they are scoped.
-   Users do not directly use this attribute. They use them indirectly when
-   they use parser attributes. -/
-structure TokenTableAttribute :=
-(attr : AttributeImpl)
-(ext  : TokenTableAttributeExtension)
+def addBuiltinLeadingParserNew (catName : Name) (declName : Name) (p : Parser) : IO Unit :=
+addBuiltinParser catName declName p
 
-instance TokenTableAttribute.inhabited : Inhabited TokenTableAttribute := ⟨{ attr := arbitrary _, ext := arbitrary _ }⟩
+def addBuiltinTrailingParserNew (catName : Name) (declName : Name) (p : TrailingParser) : IO Unit :=
+addBuiltinParser catName declName p
 
-private def addTokenAux (env : Environment) (ext : TokenTableAttributeExtension) (tk : TokenConfig) : Except String Environment := do
-let s := ext.getState env;
--- Recall that addTokenTableEntry is pure, and assumes `addTokenConfig` does not fail.
--- So, we must run it here to handle exception.
-addTokenConfig s.2 tk;
-pure $ ext.addEntry env tk
+-- TODO DELETE --
+def mkBuiltinParsingTablesRef : IO (IO.Ref ParsingTables) := IO.mkRef {}
+@[init mkBuiltinParsingTablesRef] constant builtinTermParsingTable : IO.Ref ParsingTables := arbitrary _
+@[init mkBuiltinParsingTablesRef] constant builtinLevelParsingTable : IO.Ref ParsingTables := arbitrary _
+@[init mkBuiltinParsingTablesRef] constant builtinCommandParsingTable : IO.Ref ParsingTables := arbitrary _
+def addBuiltinLeadingParser (tablesRef : IO.Ref ParsingTables) (declName : Name) (p : Parser) : IO Unit :=
+condM (tablesRef.ptrEq builtinTermParsingTable) (addBuiltinLeadingParserNew `term declName p) $
+condM (tablesRef.ptrEq builtinLevelParsingTable) (addBuiltinLeadingParserNew `level declName p) $
+(addBuiltinLeadingParserNew `command declName p)
+def addBuiltinTrailingParser (tablesRef : IO.Ref ParsingTables) (declName : Name) (p : TrailingParser) : IO Unit :=
+condM (tablesRef.ptrEq builtinTermParsingTable) (addBuiltinTrailingParserNew `term declName p) $
+condM (tablesRef.ptrEq builtinLevelParsingTable) (addBuiltinTrailingParserNew `level declName p) $
+(addBuiltinTrailingParserNew `command declName p)
+--- END TODO DELETE --
 
-def mkTokenTableAttribute : IO TokenTableAttribute := do
-ext : TokenTableAttributeExtension ← registerPersistentEnvExtension {
-  name            := `_tokens_,
-  mkInitial       := do table ← builtinTokenTable.get; pure ([], table),
-  addImportedFn   := fun env => mkImportedTokenTable,
-  addEntryFn      := addTokenTableEntry,
-  exportEntriesFn := fun s => s.1.reverse.toArray,
-  statsFn         := fun s => format "number of local entries: " ++ format s.1.length
-};
-let attrImpl : AttributeImpl := {
-  name  := `_tokens_,
-  descr := "internal token table attribute",
-  add   := fun env decl args persistent => pure env -- TODO
-};
-registerAttribute attrImpl;
-pure { ext := ext, attr := attrImpl }
+private def ParserExtension.addEntry (s : ParserExtensionState) (e : ParserExtensionEntry) : ParserExtensionState :=
+match e with
+| ParserExtensionEntry.token tk =>
+  match addTokenConfig s.tokens tk with
+  | Except.ok tokens => { tokens := tokens, newEntries := ParserExtensionOleanEntry.token tk :: s.newEntries, .. s }
+  | _                => unreachable!
+| ParserExtensionEntry.kind k =>
+  { kinds := s.kinds.insert k, newEntries := ParserExtensionOleanEntry.kind k :: s.newEntries, .. s }
+| ParserExtensionEntry.category catName =>
+  if s.categories.contains catName then s
+  else { categories := s.categories.insert catName {}, newEntries := ParserExtensionOleanEntry.category catName :: s.newEntries, .. s }
+| ParserExtensionEntry.parser catName declName _ parser =>
+  match addParser s.categories catName declName parser with
+  | Except.ok categories => { categories := categories, newEntries := ParserExtensionOleanEntry.parser catName declName :: s.newEntries }
+  | _ => unreachable!
 
-@[init mkTokenTableAttribute]
-constant tokenTableAttribute : TokenTableAttribute := arbitrary _
+def compileParserDescr (categories : ParserCategories) : forall {k : ParserKind}, ParserDescrCore k → Except String (Parser k)
+| _, ParserDescr.andthen d₁ d₂                       => andthen <$> compileParserDescr d₁ <*> compileParserDescr d₂
+| _, ParserDescr.orelse d₁ d₂                        => orelse <$> compileParserDescr d₁ <*> compileParserDescr d₂
+| _, ParserDescr.optional d                          => optional <$> compileParserDescr d
+| _, ParserDescr.lookahead d                         => lookahead <$> compileParserDescr d
+| _, ParserDescr.try d                               => try <$> compileParserDescr d
+| _, ParserDescr.many d                              => many <$> compileParserDescr d
+| _, ParserDescr.many1 d                             => many1 <$> compileParserDescr d
+| _, ParserDescr.sepBy d₁ d₂                         => sepBy <$> compileParserDescr d₁ <*> compileParserDescr d₂
+| _, ParserDescr.sepBy1 d₁ d₂                        => sepBy1 <$> compileParserDescr d₁ <*> compileParserDescr d₂
+| _, ParserDescr.node k d                            => node k <$> compileParserDescr d
+| _, ParserDescr.symbol tk lbp                       => pure $ symbol tk lbp
+| _, ParserDescr.unicodeSymbol tk₁ tk₂ lbp           => pure $ unicodeSymbol tk₁ tk₂ lbp
+| ParserKind.leading, ParserDescr.parser catName rbp =>
+  match categories.find? catName with
+  | some _ => pure $ categoryParser catName rbp
+  | none   => throwUnknownParserCategory catName
+| ParserKind.trailing, ParserDescr.pushLeading => pure $ pushLeading
 
-def addToken (env : Environment) (tk : TokenConfig) : Except String Environment :=
-addTokenAux env tokenTableAttribute.2 tk
+unsafe def mkParserOfConstantUnsafe (env : Environment) (categories : ParserCategories) (constName : Name)
+    : Except String (Sigma (fun (k : ParserKind) => Parser k)) :=
+match env.find? constName with
+| none      => throw ("unknow constant '" ++ toString constName ++ "'")
+| some info =>
+  match info.type with
+  | Expr.const `Lean.Parser.TrailingParser _ _ => do
+    p ← env.evalConst (Parser trailing) constName;
+    pure ⟨trailing, p⟩
+  | Expr.app (Expr.const `Lean.Parser.Parser _ _) (Expr.const `Lean.ParserKind.leading _ _) _ => do
+    p ← env.evalConst (Parser leading) constName;
+    pure ⟨leading, p⟩
+  | Expr.const `Lean.ParserDescr _ _ => do
+    d ← env.evalConst ParserDescr constName;
+    p ← compileParserDescr categories d;
+    pure ⟨leading, p⟩
+  | Expr.const `Lean.TrailingParserDescr _ _ => do
+    d ← env.evalConst TrailingParserDescr constName;
+    p ← compileParserDescr categories d;
+    pure ⟨trailing, p⟩
+  | _ => throw ("unexpected parser type at '" ++ toString constName ++ "' (`ParserDescr`, `TrailingParserDescr`, `Parser` or `TrailingParser` expected")
 
-/- Global table with all SyntaxNodeKind's -/
-def mkSyntaxNodeKindSetRef : IO (IO.Ref SyntaxNodeKindSet) := IO.mkRef {}
-@[init mkSyntaxNodeKindSetRef]
-constant syntaxNodeKindSetRef : IO.Ref SyntaxNodeKindSet := arbitrary _
+@[implementedBy mkParserOfConstantUnsafe]
+constant mkParserOfConstant (env : Environment) (categories : ParserCategories) (constName : Name) : Except String (Sigma (fun (k : ParserKind) => Parser k)) :=
+arbitrary _
 
-def updateBuiltinSyntaxNodeKinds (pinfo : ParserInfo) : IO Unit :=
-syntaxNodeKindSetRef.modify pinfo.collectKinds
+private def ParserExtension.addImported (env : Environment) (es : Array (Array ParserExtensionOleanEntry)) : IO ParserExtensionState := do
+s ← ParserExtension.mkInitial;
+es.foldlM
+  (fun s entries =>
+    entries.foldlM
+      (fun s entry =>
+       match entry with
+       | ParserExtensionOleanEntry.token tk => do
+         tokens ← IO.ofExcept (addTokenConfig s.tokens tk);
+         pure { tokens := tokens, .. s }
+       | ParserExtensionOleanEntry.kind k =>
+         pure { kinds := s.kinds.insert k, .. s }
+       | ParserExtensionOleanEntry.category catName => do
+         categories ← IO.ofExcept (addParserCategory s.categories catName);
+         pure { categories := categories, .. s }
+       | ParserExtensionOleanEntry.parser catName declName =>
+         match mkParserOfConstant env s.categories declName with
+        | Except.ok p     =>
+          match addParser s.categories catName declName p.2 with
+          | Except.ok categories => pure { categories := categories, .. s }
+          | Except.error ex      => throw (IO.userError ex)
+        | Except.error ex => throw (IO.userError ex))
+      s)
+  s
 
-abbrev SyntaxNodeKindExtensionState := List SyntaxNodeKind × SyntaxNodeKindSet
-
-def mkSyntaxNodeKindExtension : IO (PersistentEnvExtension SyntaxNodeKind SyntaxNodeKind SyntaxNodeKindExtensionState) :=
+def mkParserExtension : IO ParserExtension :=
 registerPersistentEnvExtension {
-  name            := `stxNodeKind,
-  mkInitial       := do s ← syntaxNodeKindSetRef.get; pure ([], s),
-  addEntryFn      := fun (s : SyntaxNodeKindExtensionState) e => (e :: s.1, s.2.insert e),
-  addImportedFn   := fun _ es => do
-    s ← syntaxNodeKindSetRef.get;
-    let s := mkStateFromImportedEntries SyntaxNodeKindSet.insert s es;
-    pure ([], s),
-  exportEntriesFn := fun (s : SyntaxNodeKindExtensionState) => s.1.reverse.toArray
+  name            := `parserExt,
+  mkInitial       := ParserExtension.mkInitial,
+  addImportedFn   := ParserExtension.addImported,
+  addEntryFn      := ParserExtension.addEntry,
+  exportEntriesFn := fun s => s.newEntries.reverse.toArray,
+  statsFn         := fun s => format "number of local entries: " ++ format s.newEntries.length
 }
 
-@[init mkSyntaxNodeKindExtension]
-constant syntaxNodeKindExtension : PersistentEnvExtension SyntaxNodeKind SyntaxNodeKind SyntaxNodeKindExtensionState := arbitrary _
+@[init mkParserExtension]
+constant parserExtension : ParserExtension := arbitrary _
+
+def categoryParserFnImpl (catName : Name) : ParserFn leading :=
+fun rbp ctx s =>
+  let categories := (parserExtension.getState ctx.env).categories;
+  match categories.find? catName with
+  | some tables => prattParser catName tables rbp ctx s
+  | none        => s.mkUnexpectedError ("unknown parser category '" ++ toString catName ++ "'")
+
+@[init] def setCategoryParserFnRef : IO Unit :=
+categoryParserFnRef.set categoryParserFnImpl
+
+def addToken (env : Environment) (tk : TokenConfig) : Except String Environment := do
+-- Recall that `ParserExtension.addEntry` is pure, and assumes `addTokenConfig` does not fail.
+-- So, we must run it here to handle exception.
+addTokenConfig (parserExtension.getState env).tokens tk;
+pure $ parserExtension.addEntry env $ ParserExtensionEntry.token tk
 
 def addSyntaxNodeKind (env : Environment) (k : SyntaxNodeKind) : Environment :=
-syntaxNodeKindExtension.addEntry env k
+parserExtension.addEntry env $ ParserExtensionEntry.kind k
 
 def isValidSyntaxNodeKind (env : Environment) (k : SyntaxNodeKind) : Bool :=
-let s := syntaxNodeKindExtension.getState env;
-s.2.contains k || k == `choice
+let kinds := (parserExtension.getState env).kinds;
+kinds.contains k || k == `choice
 
 def getSyntaxNodeKinds (env : Environment) : List SyntaxNodeKind := do
-let s := syntaxNodeKindExtension.getState env;
-s.2.foldl (fun ks k _ => k::ks) []
+let kinds := (parserExtension.getState env).kinds;
+kinds.foldl (fun ks k _ => k::ks) []
 
 def getTokenTable (env : Environment) : TokenTable :=
-(tokenTableAttribute.ext.getState env).2
+(parserExtension.getState env).tokens
 
 def mkInputContext (input : String) (fileName : String) : InputContext :=
 { input    := input,
@@ -1439,295 +1605,109 @@ def mkParserContext (env : Environment) (ctx : InputContext) : ParserContext :=
 def mkParserState (input : String) : ParserState :=
 { cache := initCacheForInput input }
 
-def runParser (env : Environment) (tables : ParsingTables) (input : String) (fileName := "<input>") (kind := "<main>") : Except String Syntax :=
-let c := mkParserContext env (mkInputContext input fileName);
-let s := mkParserState input;
-let s := whitespace c s;
-let s := prattParser kind tables (0 : Nat) c s;
-if s.hasError then
-  Except.error (s.toErrorMsg c)
-else
-  Except.ok s.stxStack.back
+def runParserCategory (env : Environment) (catName : Name) (input : String) (fileName := "<input>") : Except String Syntax :=
+let categories := (parserExtension.getState env).categories;
+match categories.find? catName with
+| some tables =>
+  let c := mkParserContext env (mkInputContext input fileName);
+  let s := mkParserState input;
+  let s := whitespace c s;
+  let s := prattParser catName tables (0 : Nat) c s;
+  if s.hasError then
+    Except.error (s.toErrorMsg c)
+  else
+    Except.ok s.stxStack.back
+| none => throwUnknownParserCategory catName
 
-def mkBuiltinParsingTablesRef : IO (IO.Ref ParsingTables) :=
-IO.mkRef {}
-
-@[init mkBuiltinParsingTablesRef]
-constant builtinTermParsingTable : IO.Ref ParsingTables := arbitrary _
-
-private def updateBuiltinTokens (info : ParserInfo) (declName : Name) : IO Unit := do
-tokenTable ← builtinTokenTable.swap {};
-match addParserTokens tokenTable info with
-| Except.ok tokenTable => builtinTokenTable.set tokenTable
-| Except.error msg     => throw (IO.userError ("invalid builtin parser '" ++ toString declName ++ "', " ++ msg))
-
-def addLeadingParser (tables : ParsingTables) (parserName : Name) (p : Parser) : Except String ParsingTables :=
-let addTokens (tks : List TokenConfig) : ParsingTables :=
-  let tks := tks.map $ fun tk => mkNameSimple tk.val;
-  tks.eraseDups.foldl (fun (tables : ParsingTables) tk => { leadingTable := tables.leadingTable.insert tk p, .. tables }) tables;
-match p.info.firstTokens with
-| FirstTokens.tokens tks    => pure $ addTokens tks
-| FirstTokens.optTokens tks => pure $ addTokens tks
-| _ => throw ("invalid builtin parser '" ++ toString parserName ++ "', initial token is not statically known")
-
-def addTrailingParser (tables : ParsingTables) (p : TrailingParser) : ParsingTables :=
-let addTokens (tks : List TokenConfig) : ParsingTables :=
-  let tks := tks.map $ fun tk => mkNameSimple tk.val;
-  tks.eraseDups.foldl (fun (tables : ParsingTables) tk => { trailingTable := tables.trailingTable.insert tk p, .. tables }) tables;
-match p.info.firstTokens with
-| FirstTokens.tokens tks    => addTokens tks
-| FirstTokens.optTokens tks => addTokens tks
-| _                         => { trailingParsers := p :: tables.trailingParsers, .. tables }
-
-def addParser {k} (tables : ParsingTables) (declName : Name) (p : Parser k) : Except String ParsingTables :=
-match k, p with
-| leading, p  => addLeadingParser tables declName p
-| trailing, p => pure $ addTrailingParser tables p
-
-def addBuiltinParser {k} (tablesRef : IO.Ref ParsingTables) (declName : Name) (p : Parser k) : IO Unit := do
-tables ← tablesRef.get;
-tablesRef.reset;
-updateBuiltinTokens p.info declName;
-updateBuiltinSyntaxNodeKinds p.info;
-tables ← IO.ofExcept $ addParser tables declName p;
-tablesRef.set tables
-
-def addBuiltinLeadingParser (tablesRef : IO.Ref ParsingTables) (declName : Name) (p : Parser) : IO Unit :=
-addBuiltinParser tablesRef declName p
-
-def addBuiltinTrailingParser (tablesRef : IO.Ref ParsingTables) (declName : Name) (p : TrailingParser) : IO Unit :=
-addBuiltinParser tablesRef declName p
-
-def declareBuiltinParser (env : Environment) (addFnName : Name) (refDeclName : Name) (declName : Name) : IO Environment :=
+def declareBuiltinParser (env : Environment) (addFnName : Name) (catName : Name) (declName : Name) : IO Environment :=
 let name := `_regBuiltinParser ++ declName;
 let type := mkApp (mkConst `IO) (mkConst `Unit);
-let val  := mkAppN (mkConst addFnName) #[mkConst refDeclName, toExpr declName, mkConst declName];
+let val  := mkAppN (mkConst addFnName) #[toExpr catName, toExpr declName, mkConst declName];
 let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false };
 match env.addAndCompile {} decl with
 -- TODO: pretty print error
 | Except.error _ => throw (IO.userError ("failed to emit registration code for builtin parser '" ++ toString declName ++ "'"))
 | Except.ok env  => IO.ofExcept (setInitAttr env name)
 
-def declareLeadingBuiltinParser (env : Environment) (refDeclName : Name) (declName : Name) : IO Environment :=
-declareBuiltinParser env `Lean.Parser.addBuiltinLeadingParser refDeclName declName
+def declareLeadingBuiltinParser (env : Environment) (catName : Name) (declName : Name) : IO Environment :=
+declareBuiltinParser env `Lean.Parser.addBuiltinLeadingParserNew catName declName
 
-def declareTrailingBuiltinParser (env : Environment) (refDeclName : Name) (declName : Name) : IO Environment :=
-declareBuiltinParser env `Lean.Parser.addBuiltinTrailingParser refDeclName declName
+def declareTrailingBuiltinParser (env : Environment) (catName : Name) (declName : Name) : IO Environment :=
+declareBuiltinParser env `Lean.Parser.addBuiltinTrailingParserNew catName declName
+
+private def BuiltinParserAttribute.add (attrName : Name) (catName : Name)
+    (env : Environment) (declName : Name) (args : Syntax) (persistent : Bool) : IO Environment := do
+when args.hasArgs $ throw (IO.userError ("invalid attribute '" ++ toString attrName ++ "', unexpected argument"));
+unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString attrName ++ "', must be persistent"));
+match env.find? declName with
+| none  => throw "unknown declaration"
+| some decl =>
+  match decl.type with
+ | Expr.const `Lean.Parser.TrailingParser _ _ =>
+   declareTrailingBuiltinParser env catName declName
+ | Expr.app (Expr.const `Lean.Parser.Parser _ _) (Expr.const `Lean.ParserKind.leading _ _) _ =>
+   declareLeadingBuiltinParser env catName declName
+ | _ =>
+   throw (IO.userError ("unexpected parser type at '" ++ toString declName ++ "' (`Parser` or `TrailingParser` expected"))
 
 /-
 The parsing tables for builtin parsers are "stored" in the extracted source code.
 -/
-def registerBuiltinParserAttribute (attrName : Name) (refDeclName : Name) : IO Unit :=
+def registerBuiltinParserAttribute (attrName : Name) (catName : Name) : IO Unit := do
+addBuiltinParserCategory catName;
 registerAttribute {
- name  := attrName,
- descr := "Builtin parser",
- add   := fun env declName args persistent => do {
-   when args.hasArgs $ throw (IO.userError ("invalid attribute '" ++ toString attrName ++ "', unexpected argument"));
-   unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString attrName ++ "', must be persistent"));
-   match env.find? declName with
-   | none  => throw "unknown declaration"
-   | some decl =>
-     match decl.type with
-     | Expr.const `Lean.Parser.TrailingParser _ _ =>
-       declareTrailingBuiltinParser env refDeclName declName
-     | Expr.app (Expr.const `Lean.Parser.Parser _ _) (Expr.const `Lean.ParserKind.leading _ _) _ =>
-       declareLeadingBuiltinParser env refDeclName declName
-     | _ =>
-       throw (IO.userError ("unexpected parser type at '" ++ toString declName ++ "' (`Parser` or `TrailingParser` expected"))
- },
+ name            := attrName,
+ descr           := "Builtin parser",
+ add             := BuiltinParserAttribute.add attrName catName,
  applicationTime := AttributeApplicationTime.afterCompilation
 }
 
-@[noinline] unsafe def runBuiltinParserUnsafe (kind : String) (ref : IO.Ref ParsingTables) : ParserFn leading :=
-fun a c s =>
-match unsafeIO (do tables ← ref.get; pure $ prattParser kind tables a c s) with
-| Except.ok s => s
-| _           => s.mkError "failed to access builtin reference"
-
-@[implementedBy runBuiltinParserUnsafe]
-constant runBuiltinParser (kind : String) (ref : IO.Ref ParsingTables) : ParserFn leading := arbitrary _
-
-structure ParserAttributeEntry :=
-(parserName : Name)
-(kind       : ParserKind)
-(parser     : Parser kind)
-
-structure ParserAttributeExtensionState :=
-(newEntries : List Name := [])
-(tables     : ParsingTables := {})
-
-instance ParserAttributeExtensionState.inhabited : Inhabited ParserAttributeExtensionState :=
-⟨{}⟩
-
-abbrev ParserAttributeExtension := PersistentEnvExtension Name ParserAttributeEntry ParserAttributeExtensionState
-
-structure ParserAttribute :=
-(attr : AttributeImpl)
-(ext  : ParserAttributeExtension)
-(kind : String)
-
-namespace ParserAttribute
-
-instance : Inhabited ParserAttribute := ⟨{ attr := arbitrary _, ext := arbitrary _, kind := "" }⟩
-
-def runParserFn (attr : ParserAttribute) : ParserFn leading :=
-fun a c s =>
-  let tables : ParsingTables := (attr.ext.getState c.env).tables;
-  prattParser attr.kind tables a c s
-
-def mkParser (attr : ParserAttribute) (rbp : Nat) : Parser leading :=
-{ fn := fun _ => attr.runParserFn rbp }
-
-end ParserAttribute
-
-abbrev ParserAttributeTable := HashMap Name ParserAttribute
-
-def mkParserAttributeTable : IO (IO.Ref ParserAttributeTable) :=
-IO.mkRef {}
-
-@[init mkParserAttributeTable]
-constant parserAttributeTableRef : IO.Ref ParserAttributeTable := arbitrary _
-
-def compileParserDescr (table : ParserAttributeTable) : forall {k : ParserKind}, ParserDescrCore k → Except String (Parser k)
-| _, ParserDescr.andthen d₁ d₂                 => andthen <$> compileParserDescr d₁ <*> compileParserDescr d₂
-| _, ParserDescr.orelse d₁ d₂                  => orelse <$> compileParserDescr d₁ <*> compileParserDescr d₂
-| _, ParserDescr.optional d                    => optional <$> compileParserDescr d
-| _, ParserDescr.lookahead d                   => lookahead <$> compileParserDescr d
-| _, ParserDescr.try d                         => try <$> compileParserDescr d
-| _, ParserDescr.many d                        => many <$> compileParserDescr d
-| _, ParserDescr.many1 d                       => many1 <$> compileParserDescr d
-| _, ParserDescr.sepBy d₁ d₂                   => sepBy <$> compileParserDescr d₁ <*> compileParserDescr d₂
-| _, ParserDescr.sepBy1 d₁ d₂                  => sepBy1 <$> compileParserDescr d₁ <*> compileParserDescr d₂
-| _, ParserDescr.node k d                      => node k <$> compileParserDescr d
-| _, ParserDescr.symbol tk lbp                 => pure $ symbol tk lbp
-| _, ParserDescr.unicodeSymbol tk₁ tk₂ lbp     => pure $ unicodeSymbol tk₁ tk₂ lbp
-| ParserKind.leading, ParserDescr.parser n rbp =>
-  match table.find? n with
-  | some attr => pure $ attr.mkParser rbp
-  | none      => throw ("unknow parser kind '" ++ toString n ++ "'")
-| ParserKind.trailing, ParserDescr.pushLeading => pure $ pushLeading
-
-unsafe def mkParserOfConstantUnsafe (env : Environment) (table : ParserAttributeTable) (constName : Name)
-    : Except String (Sigma (fun (k : ParserKind) => Parser k)) :=
-match env.find? constName with
-| none      => throw ("unknow constant '" ++ toString constName ++ "'")
-| some info =>
-  match info.type with
-  | Expr.const `Lean.Parser.TrailingParser _ _ => do
-    p ← env.evalConst (Parser trailing) constName;
-    pure ⟨trailing, p⟩
-  | Expr.app (Expr.const `Lean.Parser.Parser _ _) (Expr.const `Lean.ParserKind.leading _ _) _ => do
-    p ← env.evalConst (Parser leading) constName;
-    pure ⟨leading, p⟩
-  | Expr.const `Lean.ParserDescr _ _ => do
-    d ← env.evalConst ParserDescr constName;
-    p ← compileParserDescr table d;
-    pure ⟨leading, p⟩
-  | Expr.const `Lean.TrailingParserDescr _ _ => do
-    d ← env.evalConst TrailingParserDescr constName;
-    p ← compileParserDescr table d;
-    pure ⟨trailing, p⟩
-  | _ => throw ("unexpected parser type at '" ++ toString constName ++ "' (`ParserDescr`, `TrailingParserDescr`, `Parser` or `TrailingParser` expected")
-
-@[implementedBy mkParserOfConstantUnsafe]
-constant mkParserOfConstant (env : Environment) (table : ParserAttributeTable) (constName : Name) : Except String (Sigma (fun (k : ParserKind) => Parser k)) :=
-arbitrary _
-
-private def addImportedParsers (builtinTables : Option (IO.Ref ParsingTables)) (env : Environment) (es : Array (Array Name)) : IO ParserAttributeExtensionState := do
-tables ← match builtinTables with
-| some tables => tables.get
-| none        => pure {};
-attrTable ← parserAttributeTableRef.get;
-tables ← es.foldlM
-  (fun tables constNames =>
-    constNames.foldlM
-      (fun tables constName =>
-        match mkParserOfConstant env attrTable constName with
-        | Except.ok p     =>
-          match addParser tables constName p.2 with
-          | Except.ok tables => pure tables
-          | Except.error ex  => throw (IO.userError ex)
-        | Except.error ex => throw (IO.userError ex))
-      tables)
-  tables;
-pure { tables := tables }
-
-private def addParserAttributeEntry (s : ParserAttributeExtensionState) (e : ParserAttributeEntry) : ParserAttributeExtensionState :=
-match e with
-| { parserName := parserName, parser := p, .. } =>
-  match addParser s.tables parserName p with
-  | Except.ok tables => { newEntries := parserName :: s.newEntries, tables := tables }
-  | Except.error _   => unreachable!
-
-private def addParserAttribute (env : Environment) (ext : ParserAttributeExtension) (constName : Name) (persistent : Bool) : IO Environment := do
-attrTable ← parserAttributeTableRef.get;
-match mkParserOfConstant env attrTable constName with
+private def ParserAttribute.add (attrName : Name) (catName : Name) (env : Environment) (declName : Name) (args : Syntax) (persistent : Bool) : IO Environment := do
+when args.hasArgs $ throw (IO.userError ("invalid attribute '" ++ toString attrName ++ "', unexpected argument"));
+let categories := (parserExtension.getState env).categories;
+match mkParserOfConstant env categories declName with
 | Except.error ex => throw (IO.userError ex)
 | Except.ok p     => do
-  let parser := p.2;
-  let tokens := parser.info.collectTokens [];
+  let parserKind := p.1;
+  let parser     := p.2;
+  let tokens     := parser.info.collectTokens [];
   env ← tokens.foldlM
     (fun env token =>
       match addToken env token with
       | Except.ok env    => pure env
-      | Except.error msg => throw (IO.userError ("invalid parser '" ++ toString constName ++ "', " ++ msg)))
+      | Except.error msg => throw (IO.userError ("invalid parser '" ++ toString declName ++ "', " ++ msg)))
     env;
   let kinds := parser.info.collectKinds {};
   let env := kinds.foldl (fun env kind _ => addSyntaxNodeKind env kind) env;
-  let entry : ParserAttributeEntry := { parserName := constName, kind := p.1, parser := parser };
-  let s : ParserAttributeExtensionState := ext.getState env;
-  -- Remark: addEntry does not handle exceptions. So, we use `addParser` here to make sure it does not throw an exception.
-  match addParser s.tables constName parser with
-  | Except.ok _     => pure $ ext.addEntry env entry
+  match addParser categories catName declName parser with
+  | Except.ok _     => pure $ parserExtension.addEntry env $ ParserExtensionEntry.parser catName declName parserKind parser
   | Except.error ex => throw (IO.userError ex)
 
-private def ParserAttribute.mkInitial (builtinTablesRef : Option (IO.Ref ParsingTables)) : IO (ParserAttributeExtensionState) :=
-match builtinTablesRef with
-| none           => pure {}
-| some tablesRef => do tables ← tablesRef.get; pure { tables := tables }
-
 /-
 Parser attribute that can be optionally initialized with
 a builtin parser attribute.
 
 TODO: support for scoped attributes.
 -/
-def registerParserAttribute (attrName : Name) (kind : String) (descr : String) (builtinTables : Option (IO.Ref ParsingTables) := none) : IO ParserAttribute := do
-let kindSym := mkNameSimple kind;
-attrTable ← parserAttributeTableRef.get;
-when (attrTable.contains kindSym) $ throw (IO.userError ("parser attribute '" ++ kind ++ "' has already been defined"));
-ext : PersistentEnvExtension Name ParserAttributeEntry ParserAttributeExtensionState ← registerPersistentEnvExtension {
-  name            := attrName,
-  mkInitial       := ParserAttribute.mkInitial builtinTables,
-  addImportedFn   := addImportedParsers builtinTables,
-  addEntryFn      := addParserAttributeEntry,
-  exportEntriesFn := fun s => s.newEntries.reverse.toArray,
-  statsFn         := fun s => format "number of local entries: " ++ format s.newEntries.length
-};
+def registerParserAttribute (attrName : Name) (catName : Name) : IO Unit := do
 let attrImpl : AttributeImpl := {
   name            := attrName,
-  descr           := descr,
-  add             := fun env constName _ persistent => addParserAttribute env ext constName persistent,
+  descr           := "parser",
+  add             := ParserAttribute.add attrName catName,
   applicationTime := AttributeApplicationTime.afterCompilation
 };
-let attr : ParserAttribute := { ext := ext, attr := attrImpl, kind := kind };
-parserAttributeTableRef.modify $ fun table => table.insert kindSym attr;
-registerAttribute attrImpl;
-pure attr
+registerAttribute attrImpl
 
 -- declare `termParser` here since it is used everywhere via antiquotations
 
 @[init] def regBuiltinTermParserAttr : IO Unit :=
-registerBuiltinParserAttribute `builtinTermParser `Lean.Parser.builtinTermParsingTable
+registerBuiltinParserAttribute `builtinTermParser `term
 
-def mkTermParserAttribute : IO ParserAttribute :=
-registerParserAttribute `termParser "term" "term parser" (some builtinTermParsingTable)
-
-@[init mkTermParserAttribute]
-constant termParserAttribute : ParserAttribute := arbitrary _
+@[init] def regTermParserAttribute : IO Unit :=
+registerParserAttribute `termParser `term
 
 @[inline] def termParser {k : ParserKind} (rbp : Nat := 0) : Parser k :=
-{ fn := fun _ => termParserAttribute.runParserFn rbp }
+categoryParser `term rbp
 
 def dollarSymbol {k : ParserKind} : Parser k := symbol "$" 1
 

stage0/src/Init/System/IO.lean

@@ -253,6 +253,8 @@ constant Ref.set {α : Type} (r : @& Ref α) (a : α) : IO Unit  := arbitrary _
 constant Ref.swap {α : Type} (r : @& Ref α) (a : α) : IO α    := arbitrary _
 @[extern "lean_io_ref_reset"]
 constant Ref.reset {α : Type} (r : @& Ref α) : IO Unit        := arbitrary _
+@[extern "lean_io_ref_ptr_eq"]
+constant Ref.ptrEq {α : Type} (r1 r2 : @& Ref α) : IO Bool    := arbitrary _
 end Prim
 
 section
@@ -262,6 +264,7 @@ variables {m : Type → Type} [Monad m] [MonadIO m]
 @[inline] def Ref.set {α : Type} (r : Ref α) (a : α) : m Unit := Prim.liftIO (Prim.Ref.set r a)
 @[inline] def Ref.swap {α : Type} (r : Ref α) (a : α) : m α := Prim.liftIO (Prim.Ref.swap r a)
 @[inline] def Ref.reset {α : Type} (r : Ref α) : m Unit := Prim.liftIO (Prim.Ref.reset r)
+@[inline] def Ref.ptrEq {α : Type} (r1 r2 : Ref α) : m Bool := Prim.liftIO (Prim.Ref.ptrEq r1 r2)
 @[inline] def Ref.modify {α : Type} (r : Ref α) (f : α → α) : m Unit := do
 v ← r.get;
 r.reset;

stage0/src/runtime/io.cpp

@@ -354,6 +354,12 @@ extern "C" obj_res lean_io_ref_swap(b_obj_arg ref, obj_arg a, obj_arg) {
     }
 }
 
+extern "C" obj_res lean_io_ref_ptr_eq(b_obj_arg ref1, b_obj_arg ref2, obj_arg) {
+    // TODO: ref_maybe_mt
+    bool r = ref1 == ref2; // lean_to_ref(ref1)->m_value == lean_to_ref(ref2)->m_value;
+    return set_io_result(box(r));
+}
+
 void initialize_io() {
     g_io_error_nullptr_read = mk_string("null reference read");
     mark_persistent(g_io_error_nullptr_read);

stage0/stdlib/Init/Lean/Elab/Command.c

@@ -191,6 +191,7 @@ lean_object* l_Lean_Elab_Command_CommandElabM_inhabited(lean_object*);
 lean_object* l_Lean_Elab_Command_mkBuiltinCommandElabTable(lean_object*);
 lean_object* l_Lean_Elab_Command_addOpenDecl(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Command_11__toCommandResult(lean_object*, lean_object*);
+extern lean_object* l_Lean_Parser_addBuiltinLeadingParser___closed__1;
 lean_object* l___private_Init_Lean_Elab_Command_13__addScopes___main___closed__1;
 lean_object* l_Lean_Elab_Command_elabCommand___closed__6;
 lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabVariables___closed__3;
@@ -220,7 +221,6 @@ extern lean_object* l_Lean_Elab_Term_elabTerm___closed__6;
 lean_object* l_PersistentHashMap_findAtAux___main___at_Lean_Elab_Command_elabCommand___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabNotation___closed__2;
 lean_object* l_Lean_Elab_Command_elabExport___closed__3;
-extern lean_object* l_Lean_Parser_mkCommandParserAttribute___closed__4;
 lean_object* l_Lean_Elab_Command_dbgTrace(lean_object*);
 lean_object* lean_nat_sub(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Command_5__getBetterRef(lean_object*, lean_object*, lean_object*);
@@ -310,6 +310,7 @@ lean_object* l_Lean_Elab_Command_getScopes(lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_findAux___main___at_Lean_Elab_Command_elabCommand___spec__3___boxed(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_List_foldlM___main___at___private_Init_Lean_Elab_Term_3__addMacroStack___spec__1___closed__3;
 lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabUniverses___closed__2;
+uint8_t l_List_elem___main___at_Lean_Parser_addLeadingParser___spec__7(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Command_6__prettyPrint(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabExport(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_builtinCommandElabTable;
@@ -333,7 +334,6 @@ lean_object* l_Lean_Elab_Command_CommandElabM_monadLog___lambda__1___boxed(lean_
 extern lean_object* l_List_head_x21___rarg___closed__2;
 lean_object* l_PersistentHashMap_containsAux___main___at_Lean_Elab_Command_addBuiltinCommandElab___spec__5___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabVariable___closed__2;
-extern lean_object* l_Lean_Parser_registerParserAttribute___closed__5;
 extern lean_object* l_Lean_Parser_Command_open___elambda__1___closed__2;
 uint8_t l_Array_contains___at_Lean_findField_x3f___main___spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_CommandElabM_MonadQuotation___closed__1;
@@ -346,6 +346,7 @@ lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabExport___closed__2;
 lean_object* l_Lean_Elab_Command_elabSetOption___closed__1;
 lean_object* l_Lean_Elab_Command_Scope_inhabited___closed__1;
 lean_object* l_Lean_Elab_Command_elabSetOption___closed__2;
+extern lean_object* l___private_Init_Lean_Parser_Parser_8__addParserCategory___closed__2;
 lean_object* l_Lean_Elab_Command_liftIOCore___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_liftIO___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_empty___at_Lean_Elab_Command_mkBuiltinCommandElabTable___spec__3;
@@ -358,7 +359,6 @@ lean_object* l_Lean_Elab_Command_modifyScope___closed__1;
 lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabCheck(lean_object*);
 lean_object* l_Array_filterAux___main___at_Lean_Elab_Command_sortDeclLevelParams___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_PersistentHashMap_containsAux___main___at_Lean_Elab_Command_addBuiltinCommandElab___spec__5(lean_object*, size_t, lean_object*);
-uint8_t l_List_elem___main___at_Lean_Parser_addLeadingParser___spec__4(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_declareBuiltinCommandElab___closed__6;
 lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabEnd(lean_object*);
 lean_object* l_Lean_Elab_Command_throwAlreadyDeclaredUniverseLevel___rarg___closed__1;
@@ -3933,7 +3933,7 @@ x_27 = l_Lean_Name_toStringWithSep___main(x_26, x_1);
 x_28 = l_Lean_Elab_Command_addBuiltinCommandElab___closed__1;
 x_29 = lean_string_append(x_28, x_27);
 lean_dec(x_27);
-x_30 = l_Lean_Parser_registerParserAttribute___closed__5;
+x_30 = l___private_Init_Lean_Parser_Parser_8__addParserCategory___closed__2;
 x_31 = lean_string_append(x_29, x_30);
 lean_ctor_set_tag(x_6, 1);
 lean_ctor_set(x_6, 0, x_31);
@@ -4036,7 +4036,7 @@ x_51 = l_Lean_Name_toStringWithSep___main(x_50, x_1);
 x_52 = l_Lean_Elab_Command_addBuiltinCommandElab___closed__1;
 x_53 = lean_string_append(x_52, x_51);
 lean_dec(x_51);
-x_54 = l_Lean_Parser_registerParserAttribute___closed__5;
+x_54 = l___private_Init_Lean_Parser_Parser_8__addParserCategory___closed__2;
 x_55 = lean_string_append(x_53, x_54);
 x_56 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_56, 0, x_55);
@@ -4733,7 +4733,7 @@ lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_obj
 x_2 = l_Lean_Elab_Command_mkCommandElabAttribute___closed__2;
 x_3 = l___regBuiltinParser_Lean_Parser_Command_antiquot___closed__2;
 x_4 = l_Lean_Elab_Command_mkCommandElabAttribute___closed__3;
-x_5 = l_Lean_Parser_mkCommandParserAttribute___closed__4;
+x_5 = l_Lean_Parser_addBuiltinLeadingParser___closed__1;
 x_6 = l_Lean_Elab_Command_builtinCommandElabTable;
 x_7 = l_Lean_Elab_mkElabAttribute___rarg(x_2, x_3, x_4, x_5, x_6, x_1);
 return x_7;
@@ -9832,7 +9832,7 @@ lean_inc(x_6);
 x_7 = lean_ctor_get(x_5, 1);
 lean_inc(x_7);
 lean_dec(x_5);
-x_8 = l_List_elem___main___at_Lean_Parser_addLeadingParser___spec__4(x_4, x_6);
+x_8 = l_List_elem___main___at_Lean_Parser_addLeadingParser___spec__7(x_4, x_6);
 lean_dec(x_6);
 if (x_8 == 0)
 {
@@ -19479,7 +19479,7 @@ x_11 = lean_unsigned_to_nat(1u);
 x_12 = lean_nat_add(x_3, x_11);
 lean_dec(x_3);
 x_13 = l_Lean_Syntax_getId(x_10);
-x_14 = l_List_elem___main___at_Lean_Parser_addLeadingParser___spec__4(x_13, x_4);
+x_14 = l_List_elem___main___at_Lean_Parser_addLeadingParser___spec__7(x_13, x_4);
 if (x_14 == 0)
 {
 lean_object* x_15; 
@@ -20156,7 +20156,7 @@ else
 {
 lean_object* x_8; uint8_t x_9; 
 x_8 = lean_array_fget(x_2, x_3);
-x_9 = l_List_elem___main___at_Lean_Parser_addLeadingParser___spec__4(x_8, x_1);
+x_9 = l_List_elem___main___at_Lean_Parser_addLeadingParser___spec__7(x_8, x_1);
 lean_dec(x_8);
 if (x_9 == 0)
 {

stage0/stdlib/Init/Lean/Elab/Declaration.c

@@ -82,12 +82,12 @@ lean_object* l_Lean_Elab_Command_modifyScope___at_Lean_Elab_Command_elabAxiom___
 extern lean_object* l_Lean_Parser_Command_namespace___elambda__1___closed__1;
 extern lean_object* l___regBuiltinParser_Lean_Parser_Command_antiquot___closed__2;
 lean_object* l_Lean_Elab_Command_throwError___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+uint8_t l_List_elem___main___at_Lean_Parser_addLeadingParser___spec__7(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabConstant___closed__7;
 lean_object* l_Lean_Elab_Command_modifyScope___at_Lean_Elab_Command_elabAxiom___spec__3(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Term_hole___elambda__1___closed__1;
 lean_object* l_Lean_Elab_Command_elabTheorem(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Elab_Command_modifyScope___closed__1;
-uint8_t l_List_elem___main___at_Lean_Parser_addLeadingParser___spec__4(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabDef(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Elab_Command_withDeclId___closed__3;
 lean_object* l_Lean_Elab_Command_elabAxiom___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -2942,7 +2942,7 @@ x_11 = lean_unsigned_to_nat(1u);
 x_12 = lean_nat_add(x_3, x_11);
 lean_dec(x_3);
 x_13 = l_Lean_Syntax_getId(x_10);
-x_14 = l_List_elem___main___at_Lean_Parser_addLeadingParser___spec__4(x_13, x_4);
+x_14 = l_List_elem___main___at_Lean_Parser_addLeadingParser___spec__7(x_13, x_4);
 if (x_14 == 0)
 {
 lean_object* x_15; 

stage0/stdlib/Init/Lean/Elab/Definition.c

@@ -78,6 +78,7 @@ lean_object* l_Lean_Elab_Command_collectUsedFVars(lean_object*, lean_object*, le
 lean_object* l_Lean_Elab_Command_withUsedWhen___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Command_namespace___elambda__1___closed__1;
 lean_object* l_Lean_Elab_Command_throwError___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+uint8_t l_List_elem___main___at_Lean_Parser_addLeadingParser___spec__7(lean_object*, lean_object*);
 lean_object* l_Lean_LocalInstances_erase(lean_object*, lean_object*);
 lean_object* l_Lean_CollectFVars_main___main(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_withUsedWhen_x27(lean_object*);
@@ -86,7 +87,6 @@ lean_object* l_Lean_Elab_Term_getLocalInsts(lean_object*, lean_object*);
 extern lean_object* l_Lean_Elab_Command_modifyScope___closed__1;
 lean_object* l_Lean_Elab_Command_elabDefLike___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 uint8_t l_Lean_Elab_Command_DefKind_isTheorem(uint8_t);
-uint8_t l_List_elem___main___at_Lean_Parser_addLeadingParser___spec__4(lean_object*, lean_object*);
 extern lean_object* l_Lean_Elab_Command_withDeclId___closed__3;
 lean_object* l_Lean_Elab_Command_sortDeclLevelParams(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Command_elabDefVal___closed__3;
@@ -4261,7 +4261,7 @@ x_11 = lean_unsigned_to_nat(1u);
 x_12 = lean_nat_add(x_3, x_11);
 lean_dec(x_3);
 x_13 = l_Lean_Syntax_getId(x_10);
-x_14 = l_List_elem___main___at_Lean_Parser_addLeadingParser___spec__4(x_13, x_4);
+x_14 = l_List_elem___main___at_Lean_Parser_addLeadingParser___spec__7(x_13, x_4);
 if (x_14 == 0)
 {
 lean_object* x_15; 

stage0/stdlib/Init/Lean/Elab/Level.c

@@ -61,6 +61,7 @@ lean_object* l_Lean_Elab_Level_mkFreshId(lean_object*);
 lean_object* l_Lean_Elab_Level_elabLevel___main___closed__3;
 lean_object* l_ReaderT_bind___at_Lean_Elab_Level_LevelElabM_MonadLog___spec__2(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Level_LevelElabM_MonadLog___closed__1;
+uint8_t l_List_elem___main___at_Lean_Parser_addLeadingParser___spec__7(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Level_elabLevel___main___closed__9;
 lean_object* l_Lean_Elab_mkMessage___at_Lean_Elab_Level_elabLevel___main___spec__2(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_FileMap_toPosition(lean_object*, lean_object*);
@@ -69,7 +70,6 @@ lean_object* l_Lean_Elab_Level_mkFreshId___rarg(lean_object*);
 lean_object* l_Lean_Elab_Level_elabLevel___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_back___at___private_Init_Lean_Parser_Parser_6__updateCache___spec__1(lean_object*);
 extern lean_object* l_Lean_Parser_Level_ident___elambda__1___closed__1;
-uint8_t l_List_elem___main___at_Lean_Parser_addLeadingParser___spec__4(lean_object*, lean_object*);
 lean_object* l_Lean_mkLevelMVar(lean_object*);
 lean_object* l_Lean_Elab_Level_LevelElabM_MonadLog___lambda__4(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Level_LevelElabM_MonadLog;
@@ -1156,7 +1156,7 @@ lean_dec(x_4);
 x_50 = lean_unsigned_to_nat(0u);
 x_51 = l_Lean_Syntax_getIdAt(x_1, x_50);
 x_52 = lean_ctor_get(x_2, 3);
-x_53 = l_List_elem___main___at_Lean_Parser_addLeadingParser___spec__4(x_51, x_52);
+x_53 = l_List_elem___main___at_Lean_Parser_addLeadingParser___spec__7(x_51, x_52);
 if (x_53 == 0)
 {
 lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; uint8_t x_58; 

stage0/stdlib/Init/Lean/Elab/Quotation.c

@@ -73,6 +73,7 @@ lean_object* l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___lambda__5(lea
 lean_object* l_ReaderT_map___at_Lean_Elab_Term_oldGetAntiquotVars___spec__1(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___closed__34;
 lean_object* l_List_foldl___main___at___private_Init_Lean_Elab_Quotation_14__toPreterm___main___spec__6(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Format_pretty(lean_object*, lean_object*);
 lean_object* l_List_map___main___at___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___spec__7(lean_object*);
 lean_object* l_List_filterAux___main___at___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___spec__11___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__6;
@@ -135,7 +136,6 @@ lean_object* l___private_Init_Lean_Elab_Quotation_14__toPreterm___main___closed_
 lean_object* l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___elambda__2___closed__4;
 lean_object* l_Lean_Elab_Term_antiquotKind_x3f___boxed(lean_object*);
 lean_object* l_Lean_Parser_mkInputContext(lean_object*, lean_object*);
-lean_object* l_Lean_Parser_ParserAttribute_runParserFn(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__64;
 lean_object* lean_array_push(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__1;
@@ -163,6 +163,7 @@ lean_object* l___private_Init_Lean_Elab_Quotation_12__letBindRhss___main___close
 lean_object* l_List_foldl___main___at___private_Init_Lean_Elab_Quotation_14__toPreterm___main___spec__8(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_stxQuot_expand___closed__24;
 lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__48;
+extern lean_object* l_Lean_Parser_addBuiltinLeadingParser___closed__6;
 lean_object* lean_string_utf8_byte_size(lean_object*);
 lean_object* l_Lean_mkAtom(lean_object*);
 lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__2;
@@ -190,7 +191,6 @@ lean_object* l_Lean_Elab_Term_stxQuot_expand___closed__26;
 lean_object* l_Lean_Elab_Term_antiquotKind_x3f___closed__1;
 lean_object* l___private_Init_Lean_Elab_Quotation_1__quoteName___main(lean_object*);
 lean_object* l___private_Init_Lean_Elab_Quotation_3__quoteList___main___rarg___lambda__1___closed__7;
-extern lean_object* l_Lean_Parser_termParserAttribute;
 extern lean_object* l_Lean_nameToExprAux___main___closed__3;
 lean_object* lean_nat_add(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__9;
@@ -338,6 +338,7 @@ lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed
 lean_object* l_List_filterAux___main___at___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___spec__6___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* l_List_foldl___main___at___private_Init_Lean_Elab_Quotation_14__toPreterm___main___spec__7(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Term_explicitUniv___elambda__1___closed__1;
+extern lean_object* l_Lean_Options_empty;
 extern lean_object* l_Lean_Parser_Term_beq___elambda__1___closed__1;
 lean_object* l_List_foldl___main___at___private_Init_Lean_Elab_Quotation_14__toPreterm___main___spec__11(lean_object*, lean_object*, lean_object*);
 lean_object* l_List_mapM___main___at___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___spec__10___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@@ -377,6 +378,7 @@ extern lean_object* l___private_Init_Lean_Meta_Message_1__run_x3f___rarg___close
 lean_object* l_Lean_Elab_Term_stxQuot_expand___closed__20;
 lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__61;
 uint8_t l_Lean_Syntax_isAtom(lean_object*);
+lean_object* l_Lean_Parser_categoryParserFn(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_nullKind___closed__2;
 extern lean_object* l_Lean_Parser_Term_if___elambda__1___closed__1;
 lean_object* l_List_foldl___main___at___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___spec__3___boxed(lean_object*, lean_object*);
@@ -550,6 +552,7 @@ lean_object* l___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___cl
 lean_object* l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Elab_Quotation_3__quoteList___main___rarg___lambda__1___closed__6;
 extern lean_object* l_Lean_Meta_DiscrTree_Trie_format___main___rarg___closed__1;
+lean_object* l_Lean_Syntax_formatStxAux___main(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_nameToExprAux___main___closed__6;
 lean_object* l_List_toArrayAux___main___rarg(lean_object*, lean_object*);
 lean_object* l_ReaderT_pure___at_Lean_Elab_Term_HeadInfo_Inhabited___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
@@ -5806,7 +5809,7 @@ lean_object* _init_l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___lambda_
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("syntax_match: unexpected pattern kind");
+x_1 = lean_mk_string("match_syntax: unexpected pattern kind ");
 return x_1;
 }
 }
@@ -5833,10 +5836,23 @@ return x_2;
 lean_object* l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
-lean_object* x_5; lean_object* x_6; 
-x_5 = l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___lambda__1___closed__3;
-x_6 = l_Lean_Elab_Term_throwError___rarg(x_1, x_5, x_3, x_4);
-return x_6;
+lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; 
+x_5 = lean_box(0);
+x_6 = lean_unsigned_to_nat(0u);
+lean_inc(x_1);
+x_7 = l_Lean_Syntax_formatStxAux___main(x_5, x_6, x_1);
+x_8 = l_Lean_Options_empty;
+x_9 = l_Lean_Format_pretty(x_7, x_8);
+x_10 = lean_alloc_ctor(2, 1, 0);
+lean_ctor_set(x_10, 0, x_9);
+x_11 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_11, 0, x_10);
+x_12 = l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___lambda__1___closed__3;
+x_13 = lean_alloc_ctor(8, 2, 0);
+lean_ctor_set(x_13, 0, x_12);
+lean_ctor_set(x_13, 1, x_11);
+x_14 = l_Lean_Elab_Term_throwError___rarg(x_1, x_13, x_3, x_4);
+return x_14;
 }
 }
 lean_object* _init_l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___lambda__2___closed__1() {
@@ -6064,7 +6080,7 @@ lean_object* _init_l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___lambda_
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("syntax_match: antiquotation must be variable");
+x_1 = lean_mk_string("match_syntax: antiquotation must be variable ");
 return x_1;
 }
 }
@@ -6091,10 +6107,23 @@ return x_2;
 lean_object* l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___lambda__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
 _start:
 {
-lean_object* x_5; lean_object* x_6; 
-x_5 = l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___lambda__3___closed__3;
-x_6 = l_Lean_Elab_Term_throwError___rarg(x_1, x_5, x_3, x_4);
-return x_6;
+lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; 
+x_5 = lean_box(0);
+x_6 = lean_unsigned_to_nat(0u);
+lean_inc(x_1);
+x_7 = l_Lean_Syntax_formatStxAux___main(x_5, x_6, x_1);
+x_8 = l_Lean_Options_empty;
+x_9 = l_Lean_Format_pretty(x_7, x_8);
+x_10 = lean_alloc_ctor(2, 1, 0);
+lean_ctor_set(x_10, 0, x_9);
+x_11 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_11, 0, x_10);
+x_12 = l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___lambda__3___closed__3;
+x_13 = lean_alloc_ctor(8, 2, 0);
+lean_ctor_set(x_13, 0, x_12);
+lean_ctor_set(x_13, 1, x_11);
+x_14 = l_Lean_Elab_Term_throwError___rarg(x_1, x_13, x_3, x_4);
+return x_14;
 }
 }
 lean_object* l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___lambda__4(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
@@ -11403,93 +11432,93 @@ x_23 = l_Lean_Syntax_isOfKind(x_21, x_22);
 if (x_23 == 0)
 {
 x_24 = x_21;
-goto block_32;
+goto block_40;
 }
 else
 {
-lean_object* x_33; lean_object* x_34; lean_object* x_35; uint8_t x_36; 
-x_33 = l_Lean_Syntax_getArgs(x_21);
-x_34 = lean_array_get_size(x_33);
-lean_dec(x_33);
-x_35 = lean_unsigned_to_nat(3u);
-x_36 = lean_nat_dec_eq(x_34, x_35);
-lean_dec(x_34);
-if (x_36 == 0)
-{
-x_24 = x_21;
-goto block_32;
-}
-else
-{
-lean_object* x_37; lean_object* x_38; uint8_t x_39; 
-x_37 = l_Lean_Syntax_getArg(x_21, x_20);
-x_38 = l_Lean_nullKind___closed__2;
-lean_inc(x_37);
-x_39 = l_Lean_Syntax_isOfKind(x_37, x_38);
-if (x_39 == 0)
-{
-lean_dec(x_37);
-x_24 = x_21;
-goto block_32;
-}
-else
-{
-lean_object* x_40; lean_object* x_41; lean_object* x_42; uint8_t x_43; 
-x_40 = l_Lean_Syntax_getArgs(x_37);
-x_41 = lean_array_get_size(x_40);
-lean_dec(x_40);
-x_42 = lean_unsigned_to_nat(2u);
-x_43 = lean_nat_dec_eq(x_41, x_42);
+lean_object* x_41; lean_object* x_42; lean_object* x_43; uint8_t x_44; 
+x_41 = l_Lean_Syntax_getArgs(x_21);
+x_42 = lean_array_get_size(x_41);
 lean_dec(x_41);
-if (x_43 == 0)
+x_43 = lean_unsigned_to_nat(3u);
+x_44 = lean_nat_dec_eq(x_42, x_43);
+lean_dec(x_42);
+if (x_44 == 0)
 {
-lean_dec(x_37);
 x_24 = x_21;
-goto block_32;
+goto block_40;
 }
 else
 {
-lean_object* x_44; lean_object* x_45; lean_object* x_46; uint8_t x_47; 
-x_44 = lean_unsigned_to_nat(0u);
-x_45 = l_Lean_Syntax_getArg(x_37, x_44);
-x_46 = l_Lean_Syntax_getArg(x_37, x_20);
-lean_dec(x_37);
-lean_inc(x_46);
-x_47 = l_Lean_Syntax_isOfKind(x_46, x_38);
+lean_object* x_45; lean_object* x_46; uint8_t x_47; 
+x_45 = l_Lean_Syntax_getArg(x_21, x_20);
+x_46 = l_Lean_nullKind___closed__2;
+lean_inc(x_45);
+x_47 = l_Lean_Syntax_isOfKind(x_45, x_46);
 if (x_47 == 0)
 {
-lean_dec(x_46);
 lean_dec(x_45);
 x_24 = x_21;
-goto block_32;
+goto block_40;
 }
 else
 {
-lean_object* x_48; lean_object* x_49; uint8_t x_50; 
-x_48 = l_Lean_Syntax_getArgs(x_46);
-lean_dec(x_46);
+lean_object* x_48; lean_object* x_49; lean_object* x_50; uint8_t x_51; 
+x_48 = l_Lean_Syntax_getArgs(x_45);
 x_49 = lean_array_get_size(x_48);
 lean_dec(x_48);
-x_50 = lean_nat_dec_eq(x_49, x_44);
+x_50 = lean_unsigned_to_nat(2u);
+x_51 = lean_nat_dec_eq(x_49, x_50);
 lean_dec(x_49);
-if (x_50 == 0)
+if (x_51 == 0)
 {
 lean_dec(x_45);
 x_24 = x_21;
-goto block_32;
+goto block_40;
+}
+else
+{
+lean_object* x_52; lean_object* x_53; lean_object* x_54; uint8_t x_55; 
+x_52 = lean_unsigned_to_nat(0u);
+x_53 = l_Lean_Syntax_getArg(x_45, x_52);
+x_54 = l_Lean_Syntax_getArg(x_45, x_20);
+lean_dec(x_45);
+lean_inc(x_54);
+x_55 = l_Lean_Syntax_isOfKind(x_54, x_46);
+if (x_55 == 0)
+{
+lean_dec(x_54);
+lean_dec(x_53);
+x_24 = x_21;
+goto block_40;
+}
+else
+{
+lean_object* x_56; lean_object* x_57; uint8_t x_58; 
+x_56 = l_Lean_Syntax_getArgs(x_54);
+lean_dec(x_54);
+x_57 = lean_array_get_size(x_56);
+lean_dec(x_56);
+x_58 = lean_nat_dec_eq(x_57, x_52);
+lean_dec(x_57);
+if (x_58 == 0)
+{
+lean_dec(x_53);
+x_24 = x_21;
+goto block_40;
 }
 else
 {
 lean_dec(x_21);
-x_24 = x_45;
-goto block_32;
+x_24 = x_53;
+goto block_40;
 }
 }
 }
 }
 }
 }
-block_32:
+block_40:
 {
 lean_object* x_25; uint8_t x_26; 
 x_25 = l_Lean_Parser_Term_id___elambda__1___closed__2;
@@ -11497,36 +11526,49 @@ lean_inc(x_24);
 x_26 = l_Lean_Syntax_isOfKind(x_24, x_25);
 if (x_26 == 0)
 {
-lean_object* x_27; lean_object* x_28; 
-x_27 = l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___lambda__3___closed__3;
-x_28 = l_Lean_Elab_Term_throwError___rarg(x_24, x_27, x_2, x_3);
-return x_28;
+lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; 
+x_27 = lean_box(0);
+x_28 = lean_unsigned_to_nat(0u);
+lean_inc(x_24);
+x_29 = l_Lean_Syntax_formatStxAux___main(x_27, x_28, x_24);
+x_30 = l_Lean_Options_empty;
+x_31 = l_Lean_Format_pretty(x_29, x_30);
+x_32 = lean_alloc_ctor(2, 1, 0);
+lean_ctor_set(x_32, 0, x_31);
+x_33 = lean_alloc_ctor(0, 1, 0);
+lean_ctor_set(x_33, 0, x_32);
+x_34 = l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___lambda__3___closed__3;
+x_35 = lean_alloc_ctor(8, 2, 0);
+lean_ctor_set(x_35, 0, x_34);
+lean_ctor_set(x_35, 1, x_33);
+x_36 = l_Lean_Elab_Term_throwError___rarg(x_24, x_35, x_2, x_3);
+return x_36;
 }
 else
 {
-lean_object* x_29; lean_object* x_30; lean_object* x_31; 
+lean_object* x_37; lean_object* x_38; lean_object* x_39; 
 lean_dec(x_2);
-x_29 = lean_box(0);
-x_30 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_30, 0, x_24);
-lean_ctor_set(x_30, 1, x_29);
-x_31 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_31, 0, x_30);
-lean_ctor_set(x_31, 1, x_3);
-return x_31;
+x_37 = lean_box(0);
+x_38 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_38, 0, x_24);
+lean_ctor_set(x_38, 1, x_37);
+x_39 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_39, 0, x_38);
+lean_ctor_set(x_39, 1, x_3);
+return x_39;
 }
 }
 }
 }
 else
 {
-lean_object* x_51; lean_object* x_52; 
+lean_object* x_59; lean_object* x_60; 
 lean_dec(x_2);
-x_51 = lean_box(0);
-x_52 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_52, 0, x_51);
-lean_ctor_set(x_52, 1, x_3);
-return x_52;
+x_59 = lean_box(0);
+x_60 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_60, 0, x_59);
+lean_ctor_set(x_60, 1, x_3);
+return x_60;
 }
 }
 }
@@ -14055,7 +14097,7 @@ lean_object* _init_l_Array_umapMAux___main___at_Lean_Elab_Term_match__syntax_exp
 _start:
 {
 lean_object* x_1; 
-x_1 = lean_mk_string("syntax_match: expected exactly one pattern per alternative");
+x_1 = lean_mk_string("match_syntax: expected exactly one pattern per alternative");
 return x_1;
 }
 }
@@ -24835,9 +24877,9 @@ x_6 = l_Lean_Parser_mkParserContext(x_1, x_5);
 x_7 = l_Lean_Parser_mkParserState(x_2);
 lean_dec(x_2);
 x_8 = l_Lean_Parser_ParserState_setPos(x_7, x_3);
-x_9 = l_Lean_Parser_termParserAttribute;
+x_9 = l_Lean_Parser_addBuiltinLeadingParser___closed__6;
 x_10 = l_Lean_Parser_appPrec;
-x_11 = l_Lean_Parser_ParserAttribute_runParserFn(x_9, x_10, x_6, x_8);
+x_11 = l_Lean_Parser_categoryParserFn(x_9, x_10, x_6, x_8);
 x_12 = lean_ctor_get(x_11, 3);
 lean_inc(x_12);
 if (lean_obj_tag(x_12) == 0)

stage0/stdlib/Init/Lean/Elab/Term.c

@@ -428,7 +428,6 @@ lean_object* l_Lean_Elab_Term_getCurrMacroScope(lean_object*, lean_object*);
 lean_object* l_Lean_MetavarContext_assignExpr(lean_object*, lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_findAux___main___at_Lean_Elab_Term_elabTerm___spec__3(lean_object*, size_t, lean_object*);
 lean_object* l_Lean_Elab_Term_applyResult___boxed(lean_object*, lean_object*, lean_object*);
-extern lean_object* l_Lean_Parser_mkTermParserAttribute___closed__4;
 lean_object* l_Lean_Elab_Term_throwUnexpectedSyntax___rarg___closed__7;
 lean_object* l_Lean_Elab_Term_mkTermElabAttribute(lean_object*);
 lean_object* l_List_foldlM___main___at___private_Init_Lean_Elab_Term_3__addMacroStack___spec__1___closed__3;
@@ -449,7 +448,6 @@ lean_object* l_Lean_FileMap_toPosition(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_liftLevelM(lean_object*);
 lean_object* l_Lean_Elab_Term_elabProp(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Elab_Term_resolveName___closed__8;
-extern lean_object* l_Lean_Parser_registerParserAttribute___closed__5;
 lean_object* l_Lean_LocalDecl_toExpr(lean_object*);
 lean_object* l_Lean_Elab_Term_termElabAttribute___closed__5;
 lean_object* l_ReaderT_lift___at___private_Init_Lean_Elab_Term_13__resumePostponed___spec__1(lean_object*);
@@ -459,6 +457,7 @@ size_t l_USize_mul(size_t, size_t);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabArrayLit(lean_object*);
 lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabSort___closed__1;
 lean_object* l_Lean_Elab_mkMessageAt___at_Lean_Elab_Term_throwError___spec__3(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
+extern lean_object* l___private_Init_Lean_Parser_Parser_8__addParserCategory___closed__2;
 lean_object* l_PersistentHashMap_insertAtCollisionNodeAux___main___at_Lean_Elab_Term_addBuiltinTermElab___spec__9(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_HashMapImp_expand___at_Lean_Elab_Term_addBuiltinTermElab___spec__12(lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Term_hole___elambda__1___closed__1;
@@ -732,6 +731,7 @@ lean_object* l_List_filterAuxM___main___at___private_Init_Lean_Elab_Term_17__syn
 lean_object* l_Lean_Elab_Term_elabListLit___closed__3;
 lean_object* l_Lean_mkNatLit(lean_object*);
 lean_object* l_Lean_mkStrLit(lean_object*);
+extern lean_object* l_Lean_Parser_addBuiltinLeadingParser___closed__5;
 lean_object* l_Lean_Elab_Term_addContext(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_MessageData_coeOfOptExpr___closed__1;
 extern lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__2;
@@ -3655,7 +3655,7 @@ x_27 = l_Lean_Name_toStringWithSep___main(x_26, x_1);
 x_28 = l_Lean_Elab_Term_addBuiltinTermElab___closed__1;
 x_29 = lean_string_append(x_28, x_27);
 lean_dec(x_27);
-x_30 = l_Lean_Parser_registerParserAttribute___closed__5;
+x_30 = l___private_Init_Lean_Parser_Parser_8__addParserCategory___closed__2;
 x_31 = lean_string_append(x_29, x_30);
 lean_ctor_set_tag(x_6, 1);
 lean_ctor_set(x_6, 0, x_31);
@@ -3758,7 +3758,7 @@ x_51 = l_Lean_Name_toStringWithSep___main(x_50, x_1);
 x_52 = l_Lean_Elab_Term_addBuiltinTermElab___closed__1;
 x_53 = lean_string_append(x_52, x_51);
 lean_dec(x_51);
-x_54 = l_Lean_Parser_registerParserAttribute___closed__5;
+x_54 = l___private_Init_Lean_Parser_Parser_8__addParserCategory___closed__2;
 x_55 = lean_string_append(x_53, x_54);
 x_56 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_56, 0, x_55);
@@ -4465,7 +4465,7 @@ lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_obj
 x_2 = l_Lean_Elab_Term_mkTermElabAttribute___closed__2;
 x_3 = l_Lean_Parser_Term_explicitUniv___elambda__1___closed__2;
 x_4 = l_Lean_Elab_Term_mkTermElabAttribute___closed__3;
-x_5 = l_Lean_Parser_mkTermParserAttribute___closed__4;
+x_5 = l_Lean_Parser_addBuiltinLeadingParser___closed__5;
 x_6 = l_Lean_Elab_Term_builtinTermElabTable;
 x_7 = l_Lean_Elab_mkElabAttribute___rarg(x_2, x_3, x_4, x_5, x_6, x_1);
 return x_7;

stage0/stdlib/Init/Lean/Elab/Util.c

@@ -71,7 +71,6 @@ lean_object* lean_nat_add(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_checkSyntaxNodeKindAtNamespaces___main(lean_object*, lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_insert___at___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___spec__2___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_PersistentHashMap_insertAux___main___at___private_Init_Lean_Elab_Util_5__ElabAttribute_addExtensionEntry___spec__3(lean_object*);
-extern lean_object* l_Lean_Parser_mkParserOfConstantUnsafe___closed__2;
 lean_object* l_IO_ofExcept___at___private_Init_Lean_Elab_Util_6__ElabAttribute_add___spec__1___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Elab_mkElabAttribute___rarg___lambda__2(lean_object*);
 lean_object* l_Lean_Elab_ElabAttribute_inhabited___closed__6;
@@ -216,6 +215,7 @@ lean_object* lean_usize_to_nat(size_t);
 lean_object* l_Lean_SMap_empty___at_Lean_Elab_ElabAttribute_inhabited___spec__1___closed__3;
 lean_object* l_AssocList_replace___main___at___private_Init_Lean_Elab_Util_4__ElabAttribute_addImportedParsers___spec__11___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_SMap_empty___at_Lean_Elab_ElabAttributeExtensionState_inhabited___spec__1___closed__2;
+extern lean_object* l_Lean_Parser_mkParserOfConstantUnsafe___closed__3;
 lean_object* l_IO_ofExcept___at___private_Init_Lean_Elab_Util_6__ElabAttribute_add___spec__1(lean_object*, lean_object*);
 lean_object* l_Lean_SMap_empty___at_Lean_Elab_ElabAttribute_inhabited___spec__1(lean_object*);
 lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Util_5__ElabAttribute_addExtensionEntry___spec__5___rarg(size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@@ -890,7 +890,7 @@ lean_dec(x_2);
 lean_dec(x_1);
 x_5 = l_Lean_Name_toString___closed__1;
 x_6 = l_Lean_Name_toStringWithSep___main(x_5, x_3);
-x_7 = l_Lean_Parser_mkParserOfConstantUnsafe___closed__2;
+x_7 = l_Lean_Parser_mkParserOfConstantUnsafe___closed__3;
 x_8 = lean_string_append(x_7, x_6);
 lean_dec(x_6);
 x_9 = l_Char_HasRepr___closed__1;

stage0/stdlib/Init/Lean/Parser/Level.c

@@ -30,12 +30,10 @@ lean_object* l_Lean_Parser_regBuiltinLevelParserAttr(lean_object*);
 lean_object* l_Lean_Parser_Level_num___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Level_hole___closed__5;
 lean_object* l_Lean_Parser_Level_hole___closed__3;
-lean_object* l_Lean_Parser_levelParserAttribute;
 lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Level_max___elambda__1___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Prod_HasRepr___rarg___closed__1;
 lean_object* l_Lean_Parser_regBuiltinLevelParserAttr___closed__2;
 lean_object* l_Lean_Parser_Level_ident;
-lean_object* l_Lean_Parser_levelParser___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinParser_Lean_Parser_Level_num(lean_object*);
 extern lean_object* l_Lean_Level_LevelToFormat_Result_format___main___closed__1;
 lean_object* l_Lean_Parser_ParserState_pushSyntax(lean_object*, lean_object*);
@@ -45,16 +43,15 @@ lean_object* l___regBuiltinParser_Lean_Parser_Level_max(lean_object*);
 lean_object* l_Lean_Parser_ParserState_mkNode(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Level_max___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Level_num___elambda__1___closed__1;
-lean_object* l_Lean_Parser_regBuiltinLevelParserAttr___closed__4;
+lean_object* l_Lean_Parser_Level_max___closed__7;
 lean_object* l_Lean_Parser_Level_paren___closed__7;
 lean_object* l_Lean_Parser_Level_addLit___elambda__1___closed__5;
 lean_object* l_Lean_Parser_Level_hole___elambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_symbolOrIdentInfo(lean_object*);
-lean_object* l_Lean_Parser_ParserAttribute_runParserFn(lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Parser_addBuiltinParser(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_get_size(lean_object*);
 lean_object* l_Lean_Parser_Level_ident___elambda__1___closed__3;
 lean_object* lean_string_append(lean_object*, lean_object*);
+extern lean_object* l_Lean_Parser_addBuiltinLeadingParser___closed__4;
 lean_object* l_Lean_Parser_tokenFn(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Level_paren___closed__5;
 lean_object* l_Lean_Parser_Level_hole___elambda__1___closed__8;
@@ -64,7 +61,7 @@ lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Level_num___closed__1;
 lean_object* l_Lean_Parser_ParserState_mkErrorsAt(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Level_imax___closed__3;
-lean_object* l_Lean_Parser_builtinLevelParsingTable;
+extern lean_object* l_Lean_Parser_builtinLevelParsingTable;
 lean_object* l_Lean_Parser_Level_addLit___elambda__1___closed__6;
 lean_object* l_Lean_Parser_Level_max___elambda__1___closed__2;
 extern lean_object* l_Lean_Parser_numLit___closed__1;
@@ -72,13 +69,11 @@ lean_object* l_Lean_Parser_Level_max___closed__3;
 lean_object* l_Lean_Parser_Level_max___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Level_imax___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Level_paren___elambda__1(lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Parser_regBuiltinLevelParserAttr___closed__3;
 lean_object* l_Lean_Parser_Level_imax___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Level_ident___closed__3;
 lean_object* l___regBuiltinParser_Lean_Parser_Level_paren(lean_object*);
 uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
 extern lean_object* l_Lean_Name_appendIndexAfter___closed__1;
-lean_object* l_Lean_Parser_levelParser___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_nodeInfo(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Level_addLit___elambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Level_imax___elambda__1___closed__2;
@@ -86,12 +81,14 @@ lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__7;
 lean_object* l_Lean_Parser_symbolOrIdentFnAux(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Level_paren;
 lean_object* l_Lean_Parser_Level_addLit___elambda__1___closed__2;
+lean_object* l_Lean_Parser_Level_paren___closed__10;
 lean_object* l_Lean_Parser_Level_num___elambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_levelParser___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Level_addLit___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Level_max___closed__6;
 lean_object* l_Lean_Parser_Level_addLit___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Level_imax;
+lean_object* l_Lean_Parser_regLevelParserAttribute___closed__1;
 extern lean_object* l_Char_HasRepr___closed__1;
 lean_object* l_Lean_Parser_Level_hole;
 extern lean_object* l_Lean_Level_LevelToFormat_Result_format___main___closed__5;
@@ -100,6 +97,8 @@ lean_object* l_Lean_Parser_levelParser(uint8_t, lean_object*);
 lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Level_max___elambda__1___spec__1(uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Level_num___elambda__1___closed__3;
 lean_object* lean_name_mk_string(lean_object*, lean_object*);
+lean_object* l_Lean_Parser_regLevelParserAttribute___closed__2;
+lean_object* l_Lean_Parser_regLevelParserAttribute(lean_object*);
 lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__11;
 lean_object* l_Lean_Parser_Level_imax___elambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Level_ident___closed__1;
@@ -107,19 +106,17 @@ lean_object* l_Lean_Parser_registerBuiltinParserAttribute(lean_object*, lean_obj
 lean_object* l_Lean_Parser_Level_addLit___closed__5;
 lean_object* l_Lean_Parser_Level_addLit___closed__3;
 lean_object* l_Lean_Parser_Level_imax___closed__2;
-extern lean_object* l_Lean_Parser_ParserAttribute_Inhabited___closed__4;
 lean_object* l_Lean_Parser_Level_ident___elambda__1___closed__4;
 lean_object* l_Array_back___at___private_Init_Lean_Parser_Parser_6__updateCache___spec__1(lean_object*);
-lean_object* l_Lean_Parser_mkLevelParserAttribute___closed__5;
 lean_object* l_Lean_Parser_ParserState_restore(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Level_ident___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Level_paren___closed__4;
-lean_object* l_Lean_Parser_registerParserAttribute(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Parser_mkLevelParserAttribute___closed__3;
+lean_object* l_Lean_Parser_registerParserAttribute(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Level_imax___elambda__1___closed__3;
-lean_object* l_Lean_Parser_mkBuiltinParsingTablesRef(lean_object*);
+lean_object* l_Lean_Parser_addBuiltinLeadingParser(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Level_paren___closed__9;
 lean_object* l_Lean_Parser_Level_addLit___closed__7;
+lean_object* l_Lean_Parser_categoryParserFn(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__6;
 lean_object* l_Lean_Parser_Level_hole___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Level_hole___elambda__1___closed__1;
@@ -134,6 +131,7 @@ lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__3;
 lean_object* l_Lean_Parser_mergeOrElseErrors(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Level_max;
 lean_object* l_Lean_Parser_Level_num;
+lean_object* l_Lean_Parser_categoryParser(uint8_t, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Level_max___closed__5;
 lean_object* l_Lean_Parser_Level_num___closed__3;
 lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__10;
@@ -156,29 +154,25 @@ lean_object* l_Lean_Parser_Level_addLit___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Level_max___elambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l___regBuiltinParser_Lean_Parser_Level_ident(lean_object*);
 lean_object* l_Lean_Parser_Level_addLit;
+lean_object* l_Lean_Parser_addBuiltinTrailingParser(lean_object*, lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Syntax_getKind___closed__3;
 lean_object* l_Lean_Parser_mkAntiquot(uint8_t, lean_object*, lean_object*, uint8_t);
 lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__13;
 lean_object* l_Lean_Parser_Level_max___elambda__1___closed__5;
-lean_object* l_Lean_Parser_mkLevelParserAttribute___closed__1;
 lean_object* l_Lean_Parser_Level_imax___elambda__1___closed__5;
 lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__14;
 lean_object* l_Lean_Parser_Level_max___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Level_imax___closed__1;
 lean_object* l_Lean_Parser_Level_imax___closed__6;
-lean_object* l_Lean_Parser_mkLevelParserAttribute___closed__2;
 lean_object* l_Lean_Parser_Level_addLit___closed__4;
 lean_object* l_Lean_Parser_ParserState_mkUnexpectedError(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Level_paren___closed__6;
 lean_object* l___regBuiltinParser_Lean_Parser_Level_imax(lean_object*);
 lean_object* l_Lean_Parser_Level_imax___closed__4;
 lean_object* l_Lean_Parser_numLitFn___rarg(lean_object*, lean_object*);
-extern lean_object* l_Lean_Parser_Parser_inhabited___closed__1;
-lean_object* l_Lean_Parser_mkLevelParserAttribute___closed__4;
 lean_object* l_Lean_Parser_Level_paren___closed__8;
 lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Level_hole___closed__4;
-lean_object* l_Lean_Parser_mkLevelParserAttribute(lean_object*);
 lean_object* l_Lean_Parser_Level_addLit___closed__1;
 lean_object* l_Lean_Parser_Level_max___closed__1;
 lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__5;
@@ -204,35 +198,17 @@ x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_Lean_Parser_regBuiltinLevelParserAttr___closed__3() {
-_start:
-{
-lean_object* x_1; 
-x_1 = lean_mk_string("builtinLevelParsingTable");
-return x_1;
-}
-}
-lean_object* _init_l_Lean_Parser_regBuiltinLevelParserAttr___closed__4() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_declareLeadingBuiltinParser___closed__1;
-x_2 = l_Lean_Parser_regBuiltinLevelParserAttr___closed__3;
-x_3 = lean_name_mk_string(x_1, x_2);
-return x_3;
-}
-}
 lean_object* l_Lean_Parser_regBuiltinLevelParserAttr(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_2 = l_Lean_Parser_regBuiltinLevelParserAttr___closed__2;
-x_3 = l_Lean_Parser_regBuiltinLevelParserAttr___closed__4;
+x_3 = l_Lean_Parser_addBuiltinLeadingParser___closed__4;
 x_4 = l_Lean_Parser_registerBuiltinParserAttribute(x_2, x_3, x_1);
 return x_4;
 }
 }
-lean_object* _init_l_Lean_Parser_mkLevelParserAttribute___closed__1() {
+lean_object* _init_l_Lean_Parser_regLevelParserAttribute___closed__1() {
 _start:
 {
 lean_object* x_1; 
@@ -240,83 +216,33 @@ x_1 = lean_mk_string("levelParser");
 return x_1;
 }
 }
-lean_object* _init_l_Lean_Parser_mkLevelParserAttribute___closed__2() {
+lean_object* _init_l_Lean_Parser_regLevelParserAttribute___closed__2() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_Lean_Parser_mkLevelParserAttribute___closed__1;
+x_2 = l_Lean_Parser_regLevelParserAttribute___closed__1;
 x_3 = lean_name_mk_string(x_1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_Lean_Parser_mkLevelParserAttribute___closed__3() {
+lean_object* l_Lean_Parser_regLevelParserAttribute(lean_object* x_1) {
 _start:
 {
-lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_Parser_builtinLevelParsingTable;
-x_2 = lean_alloc_ctor(1, 1, 0);
-lean_ctor_set(x_2, 0, x_1);
-return x_2;
-}
-}
-lean_object* _init_l_Lean_Parser_mkLevelParserAttribute___closed__4() {
-_start:
-{
-lean_object* x_1; 
-x_1 = lean_mk_string("level");
-return x_1;
-}
-}
-lean_object* _init_l_Lean_Parser_mkLevelParserAttribute___closed__5() {
-_start:
-{
-lean_object* x_1; 
-x_1 = lean_mk_string("universe level parser");
-return x_1;
-}
-}
-lean_object* l_Lean_Parser_mkLevelParserAttribute(lean_object* x_1) {
-_start:
-{
-lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
-x_2 = l_Lean_Parser_mkLevelParserAttribute___closed__2;
-x_3 = l_Lean_Parser_mkLevelParserAttribute___closed__4;
-x_4 = l_Lean_Parser_mkLevelParserAttribute___closed__5;
-x_5 = l_Lean_Parser_mkLevelParserAttribute___closed__3;
-x_6 = l_Lean_Parser_registerParserAttribute(x_2, x_3, x_4, x_5, x_1);
-return x_6;
-}
-}
-lean_object* l_Lean_Parser_levelParser___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
-_start:
-{
-lean_object* x_5; lean_object* x_6; 
-x_5 = l_Lean_Parser_levelParserAttribute;
-x_6 = l_Lean_Parser_ParserAttribute_runParserFn(x_5, x_1, x_3, x_4);
-return x_6;
+lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_2 = l_Lean_Parser_regLevelParserAttribute___closed__2;
+x_3 = l_Lean_Parser_addBuiltinLeadingParser___closed__4;
+x_4 = l_Lean_Parser_registerParserAttribute(x_2, x_3, x_1);
+return x_4;
 }
 }
 lean_object* l_Lean_Parser_levelParser(uint8_t x_1, lean_object* x_2) {
 _start:
 {
-lean_object* x_3; lean_object* x_4; lean_object* x_5; 
-x_3 = lean_alloc_closure((void*)(l_Lean_Parser_levelParser___lambda__1___boxed), 4, 1);
-lean_closure_set(x_3, 0, x_2);
-x_4 = l_Lean_Parser_Parser_inhabited___closed__1;
-x_5 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_5, 0, x_4);
-lean_ctor_set(x_5, 1, x_3);
-return x_5;
-}
-}
-lean_object* l_Lean_Parser_levelParser___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
-_start:
-{
-lean_object* x_5; 
-x_5 = l_Lean_Parser_levelParser___lambda__1(x_1, x_2, x_3, x_4);
-lean_dec(x_2);
-return x_5;
+lean_object* x_3; lean_object* x_4; 
+x_3 = l_Lean_Parser_addBuiltinLeadingParser___closed__4;
+x_4 = l_Lean_Parser_categoryParser(x_1, x_3, x_2);
+return x_4;
 }
 }
 lean_object* l_Lean_Parser_levelParser___boxed(lean_object* x_1, lean_object* x_2) {
@@ -585,10 +511,10 @@ lean_inc(x_18);
 if (lean_obj_tag(x_18) == 0)
 {
 lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; 
-x_19 = l_Lean_Parser_levelParserAttribute;
+x_19 = l_Lean_Parser_addBuiltinLeadingParser___closed__4;
 x_20 = lean_unsigned_to_nat(0u);
 lean_inc(x_2);
-x_21 = l_Lean_Parser_ParserAttribute_runParserFn(x_19, x_20, x_2, x_17);
+x_21 = l_Lean_Parser_categoryParserFn(x_19, x_20, x_2, x_17);
 x_22 = lean_ctor_get(x_21, 3);
 lean_inc(x_22);
 if (lean_obj_tag(x_22) == 0)
@@ -714,6 +640,17 @@ return x_3;
 lean_object* _init_l_Lean_Parser_Level_paren___closed__3() {
 _start:
 {
+uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_1 = 0;
+x_2 = l_Lean_Parser_addBuiltinLeadingParser___closed__4;
+x_3 = lean_unsigned_to_nat(0u);
+x_4 = l_Lean_Parser_categoryParser(x_1, x_2, x_3);
+return x_4;
+}
+}
+lean_object* _init_l_Lean_Parser_Level_paren___closed__4() {
+_start:
+{
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
 x_2 = l_Lean_Parser_Level_paren___elambda__1___closed__8;
@@ -721,49 +658,51 @@ x_3 = l_Lean_Parser_symbolInfo(x_2, x_1);
 return x_3;
 }
 }
-lean_object* _init_l_Lean_Parser_Level_paren___closed__4() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Parser_inhabited___closed__1;
-x_2 = l_Lean_Parser_Level_paren___closed__3;
-x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
-return x_3;
-}
-}
 lean_object* _init_l_Lean_Parser_Level_paren___closed__5() {
 _start:
 {
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Level_paren___closed__2;
-x_2 = l_Lean_Parser_Level_paren___closed__4;
-x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
-return x_3;
+lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_1 = l_Lean_Parser_Level_paren___closed__3;
+x_2 = lean_ctor_get(x_1, 0);
+lean_inc(x_2);
+x_3 = l_Lean_Parser_Level_paren___closed__4;
+x_4 = l_Lean_Parser_andthenInfo(x_2, x_3);
+return x_4;
 }
 }
 lean_object* _init_l_Lean_Parser_Level_paren___closed__6() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Level_paren___elambda__1___closed__4;
+x_1 = l_Lean_Parser_Level_paren___closed__2;
 x_2 = l_Lean_Parser_Level_paren___closed__5;
-x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
+x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
 return x_3;
 }
 }
 lean_object* _init_l_Lean_Parser_Level_paren___closed__7() {
 _start:
 {
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Parser_Level_paren___elambda__1___closed__4;
+x_2 = l_Lean_Parser_Level_paren___closed__6;
+x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
+return x_3;
+}
+}
+lean_object* _init_l_Lean_Parser_Level_paren___closed__8() {
+_start:
+{
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_1 = l_Lean_Parser_Level_paren___elambda__1___closed__6;
 x_2 = lean_ctor_get(x_1, 0);
 lean_inc(x_2);
-x_3 = l_Lean_Parser_Level_paren___closed__6;
+x_3 = l_Lean_Parser_Level_paren___closed__7;
 x_4 = l_Lean_Parser_orelseInfo(x_2, x_3);
 return x_4;
 }
 }
-lean_object* _init_l_Lean_Parser_Level_paren___closed__8() {
+lean_object* _init_l_Lean_Parser_Level_paren___closed__9() {
 _start:
 {
 lean_object* x_1; 
@@ -771,12 +710,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Level_paren___elambda__1), 3, 0);
 return x_1;
 }
 }
-lean_object* _init_l_Lean_Parser_Level_paren___closed__9() {
+lean_object* _init_l_Lean_Parser_Level_paren___closed__10() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Level_paren___closed__7;
-x_2 = l_Lean_Parser_Level_paren___closed__8;
+x_1 = l_Lean_Parser_Level_paren___closed__8;
+x_2 = l_Lean_Parser_Level_paren___closed__9;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);
@@ -787,20 +726,19 @@ lean_object* _init_l_Lean_Parser_Level_paren() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_Lean_Parser_Level_paren___closed__9;
+x_1 = l_Lean_Parser_Level_paren___closed__10;
 return x_1;
 }
 }
 lean_object* l___regBuiltinParser_Lean_Parser_Level_paren(lean_object* x_1) {
 _start:
 {
-uint8_t x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
-x_2 = 0;
-x_3 = l_Lean_Parser_builtinLevelParsingTable;
-x_4 = l_Lean_Parser_Level_paren___elambda__1___closed__4;
-x_5 = l_Lean_Parser_Level_paren;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
+x_2 = l_Lean_Parser_builtinLevelParsingTable;
+x_3 = l_Lean_Parser_Level_paren___elambda__1___closed__4;
+x_4 = l_Lean_Parser_Level_paren;
+x_5 = l_Lean_Parser_addBuiltinLeadingParser(x_2, x_3, x_4, x_1);
+return x_5;
 }
 }
 lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Level_max___elambda__1___spec__1(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
@@ -813,10 +751,10 @@ x_6 = lean_array_get_size(x_5);
 lean_dec(x_5);
 x_7 = lean_ctor_get(x_4, 1);
 lean_inc(x_7);
-x_8 = l_Lean_Parser_levelParserAttribute;
+x_8 = l_Lean_Parser_addBuiltinLeadingParser___closed__4;
 x_9 = l_Lean_Parser_appPrec;
 lean_inc(x_3);
-x_10 = l_Lean_Parser_ParserAttribute_runParserFn(x_8, x_9, x_3, x_4);
+x_10 = l_Lean_Parser_categoryParserFn(x_8, x_9, x_3, x_4);
 x_11 = lean_ctor_get(x_10, 3);
 lean_inc(x_11);
 if (lean_obj_tag(x_11) == 0)
@@ -996,10 +934,10 @@ x_21 = lean_ctor_get(x_19, 0);
 lean_inc(x_21);
 x_22 = lean_array_get_size(x_21);
 lean_dec(x_21);
-x_23 = l_Lean_Parser_levelParserAttribute;
+x_23 = l_Lean_Parser_addBuiltinLeadingParser___closed__4;
 x_24 = l_Lean_Parser_appPrec;
 lean_inc(x_2);
-x_25 = l_Lean_Parser_ParserAttribute_runParserFn(x_23, x_24, x_2, x_19);
+x_25 = l_Lean_Parser_categoryParserFn(x_23, x_24, x_2, x_19);
 x_26 = lean_ctor_get(x_25, 3);
 lean_inc(x_26);
 if (lean_obj_tag(x_26) == 0)
@@ -1059,36 +997,49 @@ return x_2;
 lean_object* _init_l_Lean_Parser_Level_max___closed__2() {
 _start:
 {
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Level_max___closed__1;
-x_2 = l_Lean_Parser_Parser_inhabited___closed__1;
-x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
-return x_3;
+uint8_t x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_1 = 0;
+x_2 = l_Lean_Parser_addBuiltinLeadingParser___closed__4;
+x_3 = l_Lean_Parser_appPrec;
+x_4 = l_Lean_Parser_categoryParser(x_1, x_2, x_3);
+return x_4;
 }
 }
 lean_object* _init_l_Lean_Parser_Level_max___closed__3() {
 _start:
 {
+lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_1 = l_Lean_Parser_Level_max___closed__2;
+x_2 = lean_ctor_get(x_1, 0);
+lean_inc(x_2);
+x_3 = l_Lean_Parser_Level_max___closed__1;
+x_4 = l_Lean_Parser_andthenInfo(x_3, x_2);
+return x_4;
+}
+}
+lean_object* _init_l_Lean_Parser_Level_max___closed__4() {
+_start:
+{
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Lean_Parser_Level_max___elambda__1___closed__1;
-x_2 = l_Lean_Parser_Level_max___closed__2;
+x_2 = l_Lean_Parser_Level_max___closed__3;
 x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_Lean_Parser_Level_max___closed__4() {
+lean_object* _init_l_Lean_Parser_Level_max___closed__5() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_1 = l_Lean_Parser_Level_max___elambda__1___closed__3;
 x_2 = lean_ctor_get(x_1, 0);
 lean_inc(x_2);
-x_3 = l_Lean_Parser_Level_max___closed__3;
+x_3 = l_Lean_Parser_Level_max___closed__4;
 x_4 = l_Lean_Parser_orelseInfo(x_2, x_3);
 return x_4;
 }
 }
-lean_object* _init_l_Lean_Parser_Level_max___closed__5() {
+lean_object* _init_l_Lean_Parser_Level_max___closed__6() {
 _start:
 {
 lean_object* x_1; 
@@ -1096,12 +1047,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Level_max___elambda__1), 3, 0);
 return x_1;
 }
 }
-lean_object* _init_l_Lean_Parser_Level_max___closed__6() {
+lean_object* _init_l_Lean_Parser_Level_max___closed__7() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Level_max___closed__4;
-x_2 = l_Lean_Parser_Level_max___closed__5;
+x_1 = l_Lean_Parser_Level_max___closed__5;
+x_2 = l_Lean_Parser_Level_max___closed__6;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);
@@ -1112,7 +1063,7 @@ lean_object* _init_l_Lean_Parser_Level_max() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_Lean_Parser_Level_max___closed__6;
+x_1 = l_Lean_Parser_Level_max___closed__7;
 return x_1;
 }
 }
@@ -1130,13 +1081,12 @@ return x_6;
 lean_object* l___regBuiltinParser_Lean_Parser_Level_max(lean_object* x_1) {
 _start:
 {
-uint8_t x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
-x_2 = 0;
-x_3 = l_Lean_Parser_builtinLevelParsingTable;
-x_4 = l_Lean_Parser_Level_max___elambda__1___closed__1;
-x_5 = l_Lean_Parser_Level_max;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
+x_2 = l_Lean_Parser_builtinLevelParsingTable;
+x_3 = l_Lean_Parser_Level_max___elambda__1___closed__1;
+x_4 = l_Lean_Parser_Level_max;
+x_5 = l_Lean_Parser_addBuiltinLeadingParser(x_2, x_3, x_4, x_1);
+return x_5;
 }
 }
 lean_object* _init_l_Lean_Parser_Level_imax___elambda__1___closed__1() {
@@ -1268,10 +1218,10 @@ x_21 = lean_ctor_get(x_19, 0);
 lean_inc(x_21);
 x_22 = lean_array_get_size(x_21);
 lean_dec(x_21);
-x_23 = l_Lean_Parser_levelParserAttribute;
+x_23 = l_Lean_Parser_addBuiltinLeadingParser___closed__4;
 x_24 = l_Lean_Parser_appPrec;
 lean_inc(x_2);
-x_25 = l_Lean_Parser_ParserAttribute_runParserFn(x_23, x_24, x_2, x_19);
+x_25 = l_Lean_Parser_categoryParserFn(x_23, x_24, x_2, x_19);
 x_26 = lean_ctor_get(x_25, 3);
 lean_inc(x_26);
 if (lean_obj_tag(x_26) == 0)
@@ -1331,11 +1281,13 @@ return x_2;
 lean_object* _init_l_Lean_Parser_Level_imax___closed__2() {
 _start:
 {
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Level_imax___closed__1;
-x_2 = l_Lean_Parser_Parser_inhabited___closed__1;
-x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
-return x_3;
+lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
+x_1 = l_Lean_Parser_Level_max___closed__2;
+x_2 = lean_ctor_get(x_1, 0);
+lean_inc(x_2);
+x_3 = l_Lean_Parser_Level_imax___closed__1;
+x_4 = l_Lean_Parser_andthenInfo(x_3, x_2);
+return x_4;
 }
 }
 lean_object* _init_l_Lean_Parser_Level_imax___closed__3() {
@@ -1391,13 +1343,12 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Level_imax(lean_object* x_1) {
 _start:
 {
-uint8_t x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
-x_2 = 0;
-x_3 = l_Lean_Parser_builtinLevelParsingTable;
-x_4 = l_Lean_Parser_Level_imax___elambda__1___closed__1;
-x_5 = l_Lean_Parser_Level_imax;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
+x_2 = l_Lean_Parser_builtinLevelParsingTable;
+x_3 = l_Lean_Parser_Level_imax___elambda__1___closed__1;
+x_4 = l_Lean_Parser_Level_imax;
+x_5 = l_Lean_Parser_addBuiltinLeadingParser(x_2, x_3, x_4, x_1);
+return x_5;
 }
 }
 lean_object* _init_l_Lean_Parser_Level_hole___elambda__1___closed__1() {
@@ -1668,13 +1619,12 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Level_hole(lean_object* x_1) {
 _start:
 {
-uint8_t x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
-x_2 = 0;
-x_3 = l_Lean_Parser_builtinLevelParsingTable;
-x_4 = l_Lean_Parser_Level_hole___elambda__1___closed__2;
-x_5 = l_Lean_Parser_Level_hole;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
+x_2 = l_Lean_Parser_builtinLevelParsingTable;
+x_3 = l_Lean_Parser_Level_hole___elambda__1___closed__2;
+x_4 = l_Lean_Parser_Level_hole;
+x_5 = l_Lean_Parser_addBuiltinLeadingParser(x_2, x_3, x_4, x_1);
+return x_5;
 }
 }
 lean_object* _init_l_Lean_Parser_Level_num___elambda__1___closed__1() {
@@ -1832,13 +1782,12 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Level_num(lean_object* x_1) {
 _start:
 {
-uint8_t x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
-x_2 = 0;
-x_3 = l_Lean_Parser_builtinLevelParsingTable;
-x_4 = l_Lean_Parser_Level_num___elambda__1___closed__2;
-x_5 = l_Lean_Parser_Level_num;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
+x_2 = l_Lean_Parser_builtinLevelParsingTable;
+x_3 = l_Lean_Parser_Level_num___elambda__1___closed__2;
+x_4 = l_Lean_Parser_Level_num;
+x_5 = l_Lean_Parser_addBuiltinLeadingParser(x_2, x_3, x_4, x_1);
+return x_5;
 }
 }
 lean_object* _init_l_Lean_Parser_Level_ident___elambda__1___closed__1() {
@@ -2007,13 +1956,12 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Level_ident(lean_object* x_1) {
 _start:
 {
-uint8_t x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
-x_2 = 0;
-x_3 = l_Lean_Parser_builtinLevelParsingTable;
-x_4 = l_Lean_Parser_Level_ident___elambda__1___closed__1;
-x_5 = l_Lean_Parser_Level_ident;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
+x_2 = l_Lean_Parser_builtinLevelParsingTable;
+x_3 = l_Lean_Parser_Level_ident___elambda__1___closed__1;
+x_4 = l_Lean_Parser_Level_ident;
+x_5 = l_Lean_Parser_addBuiltinLeadingParser(x_2, x_3, x_4, x_1);
+return x_5;
 }
 }
 lean_object* _init_l_Lean_Parser_Level_addLit___elambda__1___closed__1() {
@@ -2250,13 +2198,12 @@ return x_1;
 lean_object* l___regBuiltinParser_Lean_Parser_Level_addLit(lean_object* x_1) {
 _start:
 {
-uint8_t x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; 
-x_2 = 1;
-x_3 = l_Lean_Parser_builtinLevelParsingTable;
-x_4 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
-x_5 = l_Lean_Parser_Level_addLit;
-x_6 = l_Lean_Parser_addBuiltinParser(x_2, x_3, x_4, x_5, x_1);
-return x_6;
+lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; 
+x_2 = l_Lean_Parser_builtinLevelParsingTable;
+x_3 = l_Lean_Parser_Level_addLit___elambda__1___closed__2;
+x_4 = l_Lean_Parser_Level_addLit;
+x_5 = l_Lean_Parser_addBuiltinTrailingParser(x_2, x_3, x_4, x_1);
+return x_5;
 }
 }
 lean_object* initialize_Init_Lean_Parser_Parser(lean_object*);
@@ -2268,36 +2215,19 @@ _G_initialized = true;
 res = initialize_Init_Lean_Parser_Parser(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
-res = l_Lean_Parser_mkBuiltinParsingTablesRef(lean_io_mk_world());
-if (lean_io_result_is_error(res)) return res;
-l_Lean_Parser_builtinLevelParsingTable = lean_io_result_get_value(res);
-lean_mark_persistent(l_Lean_Parser_builtinLevelParsingTable);
-lean_dec_ref(res);
 l_Lean_Parser_regBuiltinLevelParserAttr___closed__1 = _init_l_Lean_Parser_regBuiltinLevelParserAttr___closed__1();
 lean_mark_persistent(l_Lean_Parser_regBuiltinLevelParserAttr___closed__1);
 l_Lean_Parser_regBuiltinLevelParserAttr___closed__2 = _init_l_Lean_Parser_regBuiltinLevelParserAttr___closed__2();
 lean_mark_persistent(l_Lean_Parser_regBuiltinLevelParserAttr___closed__2);
-l_Lean_Parser_regBuiltinLevelParserAttr___closed__3 = _init_l_Lean_Parser_regBuiltinLevelParserAttr___closed__3();
-lean_mark_persistent(l_Lean_Parser_regBuiltinLevelParserAttr___closed__3);
-l_Lean_Parser_regBuiltinLevelParserAttr___closed__4 = _init_l_Lean_Parser_regBuiltinLevelParserAttr___closed__4();
-lean_mark_persistent(l_Lean_Parser_regBuiltinLevelParserAttr___closed__4);
 res = l_Lean_Parser_regBuiltinLevelParserAttr(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
-l_Lean_Parser_mkLevelParserAttribute___closed__1 = _init_l_Lean_Parser_mkLevelParserAttribute___closed__1();
-lean_mark_persistent(l_Lean_Parser_mkLevelParserAttribute___closed__1);
-l_Lean_Parser_mkLevelParserAttribute___closed__2 = _init_l_Lean_Parser_mkLevelParserAttribute___closed__2();
-lean_mark_persistent(l_Lean_Parser_mkLevelParserAttribute___closed__2);
-l_Lean_Parser_mkLevelParserAttribute___closed__3 = _init_l_Lean_Parser_mkLevelParserAttribute___closed__3();
-lean_mark_persistent(l_Lean_Parser_mkLevelParserAttribute___closed__3);
-l_Lean_Parser_mkLevelParserAttribute___closed__4 = _init_l_Lean_Parser_mkLevelParserAttribute___closed__4();
-lean_mark_persistent(l_Lean_Parser_mkLevelParserAttribute___closed__4);
-l_Lean_Parser_mkLevelParserAttribute___closed__5 = _init_l_Lean_Parser_mkLevelParserAttribute___closed__5();
-lean_mark_persistent(l_Lean_Parser_mkLevelParserAttribute___closed__5);
-res = l_Lean_Parser_mkLevelParserAttribute(lean_io_mk_world());
+l_Lean_Parser_regLevelParserAttribute___closed__1 = _init_l_Lean_Parser_regLevelParserAttribute___closed__1();
+lean_mark_persistent(l_Lean_Parser_regLevelParserAttribute___closed__1);
+l_Lean_Parser_regLevelParserAttribute___closed__2 = _init_l_Lean_Parser_regLevelParserAttribute___closed__2();
+lean_mark_persistent(l_Lean_Parser_regLevelParserAttribute___closed__2);
+res = l_Lean_Parser_regLevelParserAttribute(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
-l_Lean_Parser_levelParserAttribute = lean_io_result_get_value(res);
-lean_mark_persistent(l_Lean_Parser_levelParserAttribute);
 lean_dec_ref(res);
 l_Lean_Parser_Level_paren___elambda__1___closed__1 = _init_l_Lean_Parser_Level_paren___elambda__1___closed__1();
 lean_mark_persistent(l_Lean_Parser_Level_paren___elambda__1___closed__1);
@@ -2345,6 +2275,8 @@ l_Lean_Parser_Level_paren___closed__8 = _init_l_Lean_Parser_Level_paren___closed
 lean_mark_persistent(l_Lean_Parser_Level_paren___closed__8);
 l_Lean_Parser_Level_paren___closed__9 = _init_l_Lean_Parser_Level_paren___closed__9();
 lean_mark_persistent(l_Lean_Parser_Level_paren___closed__9);
+l_Lean_Parser_Level_paren___closed__10 = _init_l_Lean_Parser_Level_paren___closed__10();
+lean_mark_persistent(l_Lean_Parser_Level_paren___closed__10);
 l_Lean_Parser_Level_paren = _init_l_Lean_Parser_Level_paren();
 lean_mark_persistent(l_Lean_Parser_Level_paren);
 res = l___regBuiltinParser_Lean_Parser_Level_paren(lean_io_mk_world());
@@ -2374,6 +2306,8 @@ l_Lean_Parser_Level_max___closed__5 = _init_l_Lean_Parser_Level_max___closed__5(
 lean_mark_persistent(l_Lean_Parser_Level_max___closed__5);
 l_Lean_Parser_Level_max___closed__6 = _init_l_Lean_Parser_Level_max___closed__6();
 lean_mark_persistent(l_Lean_Parser_Level_max___closed__6);
+l_Lean_Parser_Level_max___closed__7 = _init_l_Lean_Parser_Level_max___closed__7();
+lean_mark_persistent(l_Lean_Parser_Level_max___closed__7);
 l_Lean_Parser_Level_max = _init_l_Lean_Parser_Level_max();
 lean_mark_persistent(l_Lean_Parser_Level_max);
 res = l___regBuiltinParser_Lean_Parser_Level_max(lean_io_mk_world());

stage0/stdlib/Init/Lean/Parser/Module.c

@@ -43,7 +43,6 @@ lean_object* l_Lean_Parser_Module_import;
 lean_object* l_Lean_Parser_Module_import___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Module_header___closed__4;
 lean_object* l_Lean_Parser_mkInputContext(lean_object*, lean_object*);
-lean_object* l_Lean_Parser_ParserAttribute_runParserFn(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_forMAux___main___at___private_Init_Lean_Parser_Module_4__testModuleParserAux___main___spec__10___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_push(lean_object*, lean_object*);
 lean_object* lean_array_get_size(lean_object*);
@@ -51,6 +50,7 @@ lean_object* l_Lean_Parser_Module_prelude___elambda__1___closed__1;
 lean_object* lean_string_append(lean_object*, lean_object*);
 lean_object* l_PersistentArray_forM___at___private_Init_Lean_Parser_Module_4__testModuleParserAux___main___spec__6(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_tokenFn(lean_object*, lean_object*);
+lean_object* l_Lean_Parser_Module_updateTokens___closed__1;
 lean_object* l_Lean_Parser_Module_import___closed__9;
 lean_object* l_Lean_Parser_isExitCommand___boxed(lean_object*);
 lean_object* l_PersistentArray_push___rarg(lean_object*, lean_object*);
@@ -68,6 +68,7 @@ lean_object* lean_nat_add(lean_object*, lean_object*);
 lean_object* l___private_Init_Lean_Parser_Module_2__mkEOI(lean_object*);
 lean_object* l_Lean_Parser_Module_prelude___closed__4;
 lean_object* l_IO_readTextFile___at_Lean_Parser_parseFile___spec__1(lean_object*, lean_object*);
+extern lean_object* l_Lean_Parser_addBuiltinLeadingParser___closed__2;
 lean_object* l_Lean_Parser_Module_header___elambda__1___closed__1;
 lean_object* l___private_Init_Lean_Parser_Module_4__testModuleParserAux___main___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_initCacheForInput(lean_object*);
@@ -112,6 +113,7 @@ lean_object* l_Array_forMAux___main___at___private_Init_Lean_Parser_Module_4__te
 uint8_t l_PersistentArray_isEmpty___rarg(lean_object*);
 lean_object* l_Lean_FileMap_toPosition(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_parseFileAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Parser_Trie_Inhabited(lean_object*);
 extern lean_object* l_Lean_Parser_Level_ident___elambda__1___closed__4;
 lean_object* l_PersistentArray_forMAux___main___at___private_Init_Lean_Parser_Module_4__testModuleParserAux___main___spec__7(lean_object*, lean_object*, lean_object*);
 lean_object* l_Array_back___at___private_Init_Lean_Parser_Parser_6__updateCache___spec__1(lean_object*);
@@ -121,8 +123,8 @@ lean_object* l_Lean_MessageLog_forM___at___private_Init_Lean_Parser_Module_4__te
 lean_object* l_Lean_Parser_Module_header;
 lean_object* l_Lean_Parser_Module_import___closed__6;
 lean_object* l_Lean_Parser_Module_header___closed__5;
+lean_object* l_Lean_Parser_categoryParserFn(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Module_prelude___closed__5;
-extern lean_object* l___private_Init_Lean_Parser_Parser_11__addTokenTableEntry___closed__1;
 lean_object* l_Lean_Parser_Module_import___closed__2;
 lean_object* l_Lean_Parser_ModuleParserState_inhabited;
 lean_object* l_Lean_Parser_Module_prelude___elambda__1___closed__5;
@@ -142,7 +144,6 @@ lean_object* l_Lean_Parser_Module_import___closed__7;
 lean_object* l___private_Init_Lean_Parser_Module_4__testModuleParserAux(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_symbolInfo(lean_object*, lean_object*);
 lean_object* l_Array_forMAux___main___at___private_Init_Lean_Parser_Module_4__testModuleParserAux___main___spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
-extern lean_object* l_Lean_Parser_commandParserAttribute;
 lean_object* l_Lean_Parser_Module_prelude___elambda__1___closed__6;
 lean_object* l_Lean_Parser_Module_prelude___closed__2;
 lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Module_header___elambda__1___spec__1(uint8_t, lean_object*, lean_object*, lean_object*);
@@ -1404,6 +1405,14 @@ x_6 = l_Lean_Parser_manyAux___main___at_Lean_Parser_Module_header___elambda__1__
 return x_6;
 }
 }
+lean_object* _init_l_Lean_Parser_Module_updateTokens___closed__1() {
+_start:
+{
+lean_object* x_1; 
+x_1 = l_Lean_Parser_Trie_Inhabited(lean_box(0));
+return x_1;
+}
+}
 lean_object* l_Lean_Parser_Module_updateTokens(lean_object* x_1) {
 _start:
 {
@@ -1421,7 +1430,7 @@ if (lean_obj_tag(x_6) == 0)
 {
 lean_object* x_7; lean_object* x_8; 
 lean_dec(x_6);
-x_7 = l___private_Init_Lean_Parser_Parser_11__addTokenTableEntry___closed__1;
+x_7 = l_Lean_Parser_Module_updateTokens___closed__1;
 x_8 = l_unreachable_x21___rarg(x_7);
 lean_ctor_set(x_1, 2, x_8);
 return x_1;
@@ -1454,7 +1463,7 @@ if (lean_obj_tag(x_15) == 0)
 {
 lean_object* x_16; lean_object* x_17; lean_object* x_18; 
 lean_dec(x_15);
-x_16 = l___private_Init_Lean_Parser_Parser_11__addTokenTableEntry___closed__1;
+x_16 = l_Lean_Parser_Module_updateTokens___closed__1;
 x_17 = l_unreachable_x21___rarg(x_16);
 x_18 = lean_alloc_ctor(0, 3, 0);
 lean_ctor_set(x_18, 0, x_10);
@@ -1757,10 +1766,10 @@ lean_ctor_set(x_15, 1, x_5);
 lean_ctor_set(x_15, 2, x_12);
 lean_ctor_set(x_15, 3, x_13);
 x_16 = l_Lean_Parser_whitespace___main(x_11, x_15);
-x_17 = l_Lean_Parser_commandParserAttribute;
+x_17 = l_Lean_Parser_addBuiltinLeadingParser___closed__2;
 x_18 = lean_unsigned_to_nat(0u);
 lean_inc(x_11);
-x_19 = l_Lean_Parser_ParserAttribute_runParserFn(x_17, x_18, x_11, x_16);
+x_19 = l_Lean_Parser_categoryParserFn(x_17, x_18, x_11, x_16);
 x_20 = lean_ctor_get(x_19, 3);
 lean_inc(x_20);
 if (lean_obj_tag(x_20) == 0)
@@ -1840,10 +1849,10 @@ lean_ctor_set(x_43, 1, x_5);
 lean_ctor_set(x_43, 2, x_40);
 lean_ctor_set(x_43, 3, x_41);
 x_44 = l_Lean_Parser_whitespace___main(x_39, x_43);
-x_45 = l_Lean_Parser_commandParserAttribute;
+x_45 = l_Lean_Parser_addBuiltinLeadingParser___closed__2;
 x_46 = lean_unsigned_to_nat(0u);
 lean_inc(x_39);
-x_47 = l_Lean_Parser_ParserAttribute_runParserFn(x_45, x_46, x_39, x_44);
+x_47 = l_Lean_Parser_categoryParserFn(x_45, x_46, x_39, x_44);
 x_48 = lean_ctor_get(x_47, 3);
 lean_inc(x_48);
 if (lean_obj_tag(x_48) == 0)
@@ -3107,6 +3116,8 @@ l_Lean_Parser_Module_header___closed__7 = _init_l_Lean_Parser_Module_header___cl
 lean_mark_persistent(l_Lean_Parser_Module_header___closed__7);
 l_Lean_Parser_Module_header = _init_l_Lean_Parser_Module_header();
 lean_mark_persistent(l_Lean_Parser_Module_header);
+l_Lean_Parser_Module_updateTokens___closed__1 = _init_l_Lean_Parser_Module_updateTokens___closed__1();
+lean_mark_persistent(l_Lean_Parser_Module_updateTokens___closed__1);
 l_Lean_Parser_ModuleParserState_inhabited___closed__1 = _init_l_Lean_Parser_ModuleParserState_inhabited___closed__1();
 lean_mark_persistent(l_Lean_Parser_ModuleParserState_inhabited___closed__1);
 l_Lean_Parser_ModuleParserState_inhabited = _init_l_Lean_Parser_ModuleParserState_inhabited();

stage0/stdlib/Init/System/IO.c

@@ -36,6 +36,7 @@ lean_object* l_IO_Prim_readTextFile___boxed(lean_object*, lean_object*);
 lean_object* l_IO_getEnv___rarg(lean_object*, lean_object*);
 lean_object* l_IO_FS_handle_close___rarg(lean_object*, lean_object*);
 lean_object* l_IO_FS_handle_flush___boxed(lean_object*, lean_object*);
+lean_object* l_IO_Ref_ptrEq___boxed(lean_object*, lean_object*);
 lean_object* l_IO_readTextFile___boxed(lean_object*, lean_object*);
 lean_object* lean_io_mk_ref(lean_object*, lean_object*);
 lean_object* l_unsafeIO___rarg(lean_object*);
@@ -140,6 +141,7 @@ lean_object* l_IO_print___at_Lean_HasRepr_HasEval___spec__2(lean_object*, lean_o
 lean_object* l_IO_lazyPure(lean_object*);
 lean_object* l_EStateM_Monad(lean_object*, lean_object*);
 lean_object* l_MonadExcept_orelse___at_EIO_HasOrelse___spec__1___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* lean_io_ref_ptr_eq(lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_println___at_Lean_HasRepr_HasEval___spec__1___boxed(lean_object*, lean_object*);
 lean_object* lean_io_prim_handle_is_eof(lean_object*, lean_object*);
 lean_object* lean_io_prim_handle_mk(lean_object*, uint8_t, uint8_t, lean_object*);
@@ -155,6 +157,7 @@ lean_object* l_IO_FS_handle_isEof(lean_object*, lean_object*);
 lean_object* l_IO_print___boxed(lean_object*, lean_object*);
 lean_object* l_IO_print___at_Lean_HasRepr_HasEval___spec__2___boxed(lean_object*, lean_object*);
 lean_object* l_IO_Ref_swap(lean_object*, lean_object*);
+lean_object* l_IO_Ref_ptrEq(lean_object*, lean_object*);
 lean_object* l_IO_Prim_Ref_swap___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_io_ref_set(lean_object*, lean_object*, lean_object*);
 lean_object* l_IO_appDir___rarg___lambda__1(lean_object*, lean_object*);
@@ -172,7 +175,9 @@ lean_object* l_IO_Error_HasToString___closed__1;
 lean_object* l_IO_FS_readFile(lean_object*);
 lean_object* l_IO_mkRef(lean_object*, lean_object*);
 lean_object* l_IO_Prim_iterate___at_IO_FS_handle_readToEnd___spec__3(lean_object*, lean_object*, lean_object*);
+lean_object* l_IO_Prim_Ref_ptrEq___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_MonadExcept_orelse___at_EIO_HasOrelse___spec__1(lean_object*, lean_object*);
+lean_object* l_IO_Ref_ptrEq___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_EIO_Monad(lean_object*);
 lean_object* l_IO_FS_handle_getLine(lean_object*, lean_object*);
 lean_object* l___private_Init_System_IO_1__putStr___boxed(lean_object*, lean_object*);
@@ -1631,6 +1636,16 @@ lean_dec(x_2);
 return x_4;
 }
 }
+lean_object* l_IO_Prim_Ref_ptrEq___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; 
+x_5 = lean_io_ref_ptr_eq(x_2, x_3, x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+return x_5;
+}
+}
 lean_object* l_IO_mkRef___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {
@@ -1778,6 +1793,36 @@ lean_dec(x_1);
 return x_3;
 }
 }
+lean_object* l_IO_Ref_ptrEq___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
+_start:
+{
+lean_object* x_5; lean_object* x_6; 
+x_5 = lean_alloc_closure((void*)(l_IO_Prim_Ref_ptrEq___boxed), 4, 3);
+lean_closure_set(x_5, 0, lean_box(0));
+lean_closure_set(x_5, 1, x_3);
+lean_closure_set(x_5, 2, x_4);
+x_6 = lean_apply_2(x_1, lean_box(0), x_5);
+return x_6;
+}
+}
+lean_object* l_IO_Ref_ptrEq(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = lean_alloc_closure((void*)(l_IO_Ref_ptrEq___rarg), 4, 0);
+return x_3;
+}
+}
+lean_object* l_IO_Ref_ptrEq___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l_IO_Ref_ptrEq(x_1, x_2);
+lean_dec(x_2);
+lean_dec(x_1);
+return x_3;
+}
+}
 lean_object* l_IO_Ref_modify___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
 _start:
 {