chore: update stage0

2020-01-21 09:11:04 -08:00 · 2020-01-21 09:11:04 -08:00 · 35383bf862
commit 35383bf862
parent 8fb710c31e
6 changed files with 5071 additions and 5928 deletions
--- a/stage0/src/Init/Lean/Elab/Syntax.lean
+++ b/stage0/src/Init/Lean/Elab/Syntax.lean
@ -34,7 +34,6 @@ else
 /- The translator from `syntax` to `ParserDescr` syntax uses the following modes -/
 inductive ToParserDescrMode
 | anyCat -- Node kind `Lean.Parser.Syntax.cat` is allowed for any category
-| noCat  -- Node kind `Lean.Parser.Syntax.cat` is not allowed for any category
 | exceptCat (catName : Name) -- Node kind `Lean.Parser.Syntax.cat` is allowed if the category is not `catName`
 | toPushLeading (catName : Name) -- Node kind `Lean.Parser.Syntax.cat` is allowed if the category is `catName`, and it is translated into `ParserDescr.pushLeading`

@ -49,8 +48,8 @@ fun mode => match mode, first with

@[inline] private def withNoPushLeading {α} (x : ToParserDescrM α) : ToParserDescrM α :=
 fun mode => match mode with
-  | ToParserDescrMode.toPushLeading _ => x ToParserDescrMode.noCat
-  | mode                              => x mode
+  | ToParserDescrMode.toPushLeading cat => x (ToParserDescrMode.exceptCat cat)
+  | mode                                => x mode

 partial def toParserDescrAux : Syntax → ToParserDescrM Syntax
 | stx =>
@ -75,18 +74,17 @@ partial def toParserDescrAux : Syntax → ToParserDescrM Syntax
        markAsTrailingParser; -- mark as trailing par
        `(ParserDescr.pushLeading)
      else
-        liftM $ throwError (stx.getArg 3) ("invalid occurrence of '" ++ cat ++ "', '" ++ cat' ++ "', atom, or literal expected")
+        let rbp := rbp?.getD 0;
+        `(ParserDescr.parser $(quote cat) $(quote rbp))
    | ToParserDescrMode.anyCat =>
      let rbp := rbp?.getD 0;
      `(ParserDescr.parser $(quote cat) $(quote rbp))
    | ToParserDescrMode.exceptCat cat' =>
      if cat == cat' then
-        liftM $ throwError (stx.getArg 3) ("invalid occurrence of '" ++ cat ++ "', simple parser categories do not allow left recursion (try `pratt` category)")
+        liftM $ throwError (stx.getArg 3) ("invalid occurrence of '" ++ cat ++ "', parser algorithm does not allow this form of left recursion")
      else
        let rbp := rbp?.getD 0;
        `(ParserDescr.parser $(quote cat) $(quote rbp))
-    | ToParserDescrMode.noCat  =>
-      liftM $ throwError (stx.getArg 3) ("invalid occurrence of '" ++ cat ++ "', atom or literal expected")
  else if kind == `Lean.Parser.Syntax.atom then do
    match (stx.getArg 0).isStrLit? with
    | some atom =>
@ -135,8 +133,8 @@ partial def toParserDescrAux : Syntax → ToParserDescrM Syntax
  Given a `stx` of category `syntax`, return a pair `(newStx, trailingParser)`,
  where `newStx` is of category `term`. After elaboration, `newStx` should have type
  `TrailingParserDescr` if `trailingParser == true`, and `ParserDescr` otherwise. -/
-def toParserDescr (stx : Syntax) (catName : Name) (isSimpleCategory : Bool)  : TermElabM (Syntax × Bool) :=
-let mode := if isSimpleCategory then ToParserDescrMode.exceptCat catName else ToParserDescrMode.toPushLeading catName;
+def toParserDescr (stx : Syntax) (catName : Name) : TermElabM (Syntax × Bool) :=
+let mode := ToParserDescrMode.toPushLeading catName;
 (toParserDescrAux stx mode).run false

 end Term
@ -146,20 +144,9 @@ namespace Command
@[builtinCommandElab syntaxCat] def elabDeclareSyntaxCat : CommandElab :=
 fun stx => do
  let catName  := stx.getIdAt 1;
-  -- kind is of the form `optional (":" >> (nonReservedSymbol "simple" <|> nonReservedSymbol "pratt"))`
-  let kind     := stx.getArg 2;
-  let isSimple :=
-    if kind.isNone then true
-    else match kind.getArg 1 with
-    | Syntax.atom _ "simple" => true
-    | _                      => false;
  let attrName := catName.appendAfter "Parser";
  env ← getEnv;
-  env ← liftIO stx $
-    if isSimple then
-      Parser.registerSimpleParserCategory env attrName catName
-    else
-      Parser.registerPrattParserCategory env attrName catName;
+  env ← liftIO stx $ Parser.registerParserCategory env attrName catName;
  setEnv env

 def mkFreshKind (catName : Name) : CommandElabM Name := do
@ -185,10 +172,9 @@ fun stx => do
  env ← getEnv;
  let cat := (stx.getIdAt 4).eraseMacroScopes;
  unless (Parser.isParserCategory env cat) $ throwError (stx.getArg 4) ("unknown category '" ++ cat ++ "'");
-  let isSimpleCategory := Parser.isSimpleParserCategory env cat;
  kind ← elabKind (stx.getArg 1) cat;
  let catParserId := mkIdentFrom stx (cat.appendAfter "Parser");
-  (val, trailingParser) ← runTermElabM none $ fun _ => Term.toParserDescr (stx.getArg 2) cat isSimpleCategory;
+  (val, trailingParser) ← runTermElabM none $ fun _ => Term.toParserDescr (stx.getArg 2) cat;
  type ← if trailingParser then `(Lean.TrailingParserDescr) else `(Lean.ParserDescr);
  -- TODO: meaningful, unhygienic def name for selective parser `open`ing?
  d ← `(@[$catParserId:ident] def myParser : $type := ParserDescr.node $(quote kind) $val);
--- a/stage0/src/Init/Lean/Parser/Parser.lean
+++ b/stage0/src/Init/Lean/Parser/Parser.lean
@ -1276,46 +1276,36 @@ end TokenMap

 structure PrattParsingTables :=
 (leadingTable    : TokenMap Parser := {})
+(leadingParsers  : List Parser := []) -- for supporting parsers we cannot obtain first token
 (trailingTable   : TokenMap TrailingParser := {})
 (trailingParsers : List TrailingParser := []) -- for supporting parsers such as function application

 instance PrattParsingTables.inhabited : Inhabited PrattParsingTables := ⟨{}⟩

 /--
-  Each parser category is implemented using Pratt's parser or a sequence of parsers (`simple` constructor).
+  Each parser category is implemented using Pratt's parser.
  The system comes equipped with the following categories: `level`, `term`, `tactic`, and `command`.
  Users and plugins may define extra categories.

-  We current support two kinds of parser categories.
-  - `pratt` which is ideal for implementing big categories and supports left-recursion,
-     but each parser is left recursive or starts with an atom.
-     A parser `syntax term "<=" ident "<" term : index` is not allowed here because
-     it doesn't start with atom nor with the `index` catagory.
+  The field `leadingIdentAsSymbol` specifies how the parsing table
+  lookup function behaves for identifiers.  The function `prattParser`
+  uses two tables `leadingTable` and `trailingTable`. They map tokens
+  to parsers. If `leadingIdentAsSymbol == false` and the leading token
+  is an identifier, then `prattParser` just executes the parsers
+  associated with the auxiliary token "ident".  If
+  `leadingIdentAsSymbol == true` and the leading token is an
+  identifier `<foo>`, then `prattParser` combines the parsers
+  associated with the token `<foo>` with the parsers associated with
+  the auxiliary token "ident".  We use this feature and the
+  `nonReservedSymbol` parser to implement the `tactic` parsers.  We
+  use this approach to avoid creating a reserved symbol for each
+  builtin tactic (e.g., `apply`, `assumption`, etc.).  That is, users
+  may still use these symbols as identifiers (e.g., naming a
+  function). -/
+structure ParserCategory :=
+(tables : PrattParsingTables) (leadingIdentAsSymbol : Bool)

-     The field `leadingIdentAsSymbol` specifies how the parsing table
-     lookup function behaves for identifiers.  The function
-     `prattParser` uses two tables `leadingTable` and
-     `trailingTable`. They map tokens to parsers. If
-     `leadingIdentAsSymbol == false` and the leading token is an
-     identifier, then `prattParser` just executes the parsers
-     associated with the auxiliary token "ident".  If
-     `leadingIdentAsSymbol == true` and the leading token is an
-     identifier `<foo>`, then `prattParser` combines the parsers
-     associated with the token `<foo>` with the parsers associated
-     with the auxiliary token "ident".  We use this feature and the
-     `nonReservedSymbol` parser to implement the `tactic` parsers.  We
-     use this approach to avoid creating a reserved symbol for each
-     builtin tactic (e.g., `apply`, `assumption`, etc.).  That is,
-     users may still use these symbols as identifiers (e.g., naming a
-     function).
-
-  - `simple`  which is ideal for small categories which are not left recursive.
-    This kind of category is implemented using the longestMatch combinator. -/
-inductive ParserCategory
-| pratt  (tables : PrattParsingTables) (leadingIdentAsSymbol : Bool) : ParserCategory
-| simple (parsers : List Parser) : ParserCategory
-
-instance ParserCategory.inhabited : Inhabited ParserCategory := ⟨ParserCategory.simple []⟩
+instance ParserCategory.inhabited : Inhabited ParserCategory := ⟨{ tables := {}, leadingIdentAsSymbol := false }⟩

 abbrev ParserCategories := PersistentHashMap Name ParserCategory

@ -1364,6 +1354,7 @@ def leadingParser (kind : Name) (tables : PrattParsingTables) (leadingIdentAsSym
 fun a c s =>
  let iniSz   := s.stackSize;
  let (s, ps) := indexed tables.leadingTable c s leadingIdentAsSymbol;
+  let ps      := tables.leadingParsers ++ ps;
  if ps.isEmpty then
    s.mkError (toString kind)
  else
@ -1520,22 +1511,20 @@ else
 /-- All builtin parser categories are Pratt's parsers -/
 private def addBuiltinParserCategory (catName : Name) (leadingIdentAsSymbol : Bool) : IO Unit := do
 categories ← builtinParserCategoriesRef.get;
-categories ← IO.ofExcept $ addParserCategoryCore categories catName $ ParserCategory.pratt {} leadingIdentAsSymbol;
+categories ← IO.ofExcept $ addParserCategoryCore categories catName { tables := {}, leadingIdentAsSymbol := leadingIdentAsSymbol};
 builtinParserCategoriesRef.set categories

 inductive ParserExtensionOleanEntry
-| token          (val : TokenConfig) : ParserExtensionOleanEntry
-| kind           (val : SyntaxNodeKind) : ParserExtensionOleanEntry
-| prattCategory  (catName : Name) (leadingIdentAsSymbol : Bool)
-| simpleCategory (catName : Name)
-| parser         (catName : Name) (declName : Name) : ParserExtensionOleanEntry
+| token     (val : TokenConfig) : ParserExtensionOleanEntry
+| kind      (val : SyntaxNodeKind) : ParserExtensionOleanEntry
+| category  (catName : Name) (leadingIdentAsSymbol : Bool)
+| parser    (catName : Name) (declName : Name) : ParserExtensionOleanEntry

 inductive ParserExtensionEntry
-| token          (val : TokenConfig) : ParserExtensionEntry
-| kind           (val : SyntaxNodeKind) : ParserExtensionEntry
-| prattCategory  (catName : Name) (leadingIdentAsSymbol : Bool)
-| simpleCategory (catName : Name)
-| parser         (catName : Name) (declName : Name) (k : ParserKind) (p : Parser k) : ParserExtensionEntry
+| token     (val : TokenConfig) : ParserExtensionEntry
+| kind      (val : SyntaxNodeKind) : ParserExtensionEntry
+| category  (catName : Name) (leadingIdentAsSymbol : Bool)
+| parser    (catName : Name) (declName : Name) (k : ParserKind) (p : Parser k) : ParserExtensionEntry

 structure ParserExtensionState :=
 (tokens      : TokenTable := {})
@ -1576,19 +1565,19 @@ throw ("unknown parser category '" ++ toString catName ++ "'")

 def addLeadingParser (categories : ParserCategories) (catName : Name) (parserName : Name) (p : Parser) : Except String ParserCategories :=
 match categories.find? catName with
-| none =>
+| none     =>
  throwUnknownParserCategory catName
-| some (ParserCategory.simple parsers) =>
-  pure $ categories.insert catName (ParserCategory.simple (p::parsers))
-| some (ParserCategory.pratt tables i) =>
+| some cat =>
  let addTokens (tks : List TokenConfig) : Except String ParserCategories :=
    let tks    := tks.map $ fun tk => mkNameSimple tk.val;
-    let tables := tks.eraseDups.foldl (fun (tables : PrattParsingTables) tk => { leadingTable := tables.leadingTable.insert tk p, .. tables }) tables;
-    pure $ categories.insert catName (ParserCategory.pratt tables i);
+    let tables := tks.eraseDups.foldl (fun (tables : PrattParsingTables) tk => { leadingTable := tables.leadingTable.insert tk p, .. tables }) cat.tables;
+    pure $ categories.insert catName { tables := tables, .. cat };
  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")
+  | _ =>
+    let tables := { leadingParsers := p :: cat.tables.leadingParsers, .. cat.tables };
+    pure $ categories.insert catName { tables := tables, .. cat }

 private def addTrailingParserAux (tables : PrattParsingTables) (p : TrailingParser) : PrattParsingTables :=
 let addTokens (tks : List TokenConfig) : PrattParsingTables :=
@ -1601,9 +1590,8 @@ match p.info.firstTokens with

 def addTrailingParser (categories : ParserCategories) (catName : Name) (p : TrailingParser) : Except String ParserCategories :=
 match categories.find? catName with
-| none                                 => throwUnknownParserCategory catName
-| some (ParserCategory.simple _)       => throw ("parser category '" ++ toString catName ++ "' does not support trailing parsers")
-| some (ParserCategory.pratt tables i) => pure $ categories.insert catName $ ParserCategory.pratt (addTrailingParserAux tables p) i
+| none     => throwUnknownParserCategory catName
+| some cat => pure $ categories.insert catName { tables := addTrailingParserAux cat.tables p, .. cat }

 def addParser {k} (categories : ParserCategories) (catName : Name) (declName : Name) (p : Parser k) : Except String ParserCategories :=
 match k, p with
@ -1641,14 +1629,10 @@ match e with
  | _                => unreachable!
 | ParserExtensionEntry.kind k =>
  { kinds := s.kinds.insert k, newEntries := ParserExtensionOleanEntry.kind k :: s.newEntries, .. s }
-| ParserExtensionEntry.prattCategory catName leadingIdentAsSymbol =>
+| ParserExtensionEntry.category catName leadingIdentAsSymbol =>
  if s.categories.contains catName then s
-  else { categories := s.categories.insert catName (ParserCategory.pratt {} leadingIdentAsSymbol),
-         newEntries := ParserExtensionOleanEntry.prattCategory catName leadingIdentAsSymbol :: s.newEntries, .. s }
-| ParserExtensionEntry.simpleCategory catName =>
-  if s.categories.contains catName then s
-  else { categories := s.categories.insert catName (ParserCategory.simple []),
-         newEntries := ParserExtensionOleanEntry.simpleCategory catName :: s.newEntries, .. s }
+  else { categories := s.categories.insert catName { tables := {}, leadingIdentAsSymbol := leadingIdentAsSymbol },
+         newEntries := ParserExtensionOleanEntry.category catName leadingIdentAsSymbol :: 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, .. s }
@ -1716,11 +1700,8 @@ es.foldlM
         pure { tokens := tokens, .. s }
       | ParserExtensionOleanEntry.kind k =>
         pure { kinds := s.kinds.insert k, .. s }
-       | ParserExtensionOleanEntry.prattCategory catName leadingIdentAsSymbol => do
-         categories ← IO.ofExcept (addParserCategoryCore s.categories catName (ParserCategory.pratt {} leadingIdentAsSymbol));
-         pure { categories := categories, .. s }
-       | ParserExtensionOleanEntry.simpleCategory catName => do
-         categories ← IO.ofExcept (addParserCategoryCore s.categories catName (ParserCategory.simple []));
+       | ParserExtensionOleanEntry.category catName leadingIdentAsSymbol => do
+         categories ← IO.ofExcept (addParserCategoryCore s.categories catName { tables := {}, leadingIdentAsSymbol := leadingIdentAsSymbol});
         pure { categories := categories, .. s }
       | ParserExtensionOleanEntry.parser catName declName =>
         match mkParserOfConstant env s.categories declName with
@ -1760,35 +1741,18 @@ let env := parserExtension.setState env { nextKindIdx := idx+1, .. s };
 def isParserCategory (env : Environment) (catName : Name) : Bool :=
 (parserExtension.getState env).categories.contains catName

-def isSimpleParserCategory (env : Environment) (catName : Name) : Bool :=
-match (parserExtension.getState env).categories.find? catName with
-| some (ParserCategory.simple _) => true
-| _                              => false
-
-def isPrattParserCategory (env : Environment) (catName : Name) : Bool :=
-match (parserExtension.getState env).categories.find? catName with
-| some (ParserCategory.pratt _ _) => true
-| _                               => false
-
-def addPrattParserCategory (env : Environment) (catName : Name) (leadingIdentAsSymbol : Bool) : Except String Environment := do
+def addParserCategory (env : Environment) (catName : Name) (leadingIdentAsSymbol : Bool) : Except String Environment := do
 if isParserCategory env catName then
  throwParserCategoryAlreadyDefined catName
 else
-  pure $ parserExtension.addEntry env $ ParserExtensionEntry.prattCategory catName leadingIdentAsSymbol
-
-def addSimpleParserCategory (env : Environment) (catName : Name) : Except String Environment := do
-if isParserCategory env catName then
-  throwParserCategoryAlreadyDefined catName
-else
-  pure $ parserExtension.addEntry env $ ParserExtensionEntry.simpleCategory catName
+  pure $ parserExtension.addEntry env $ ParserExtensionEntry.category catName leadingIdentAsSymbol

 def categoryParserFnImpl (catName : Name) : ParserFn leading :=
 fun rbp ctx s =>
  let categories := (parserExtension.getState ctx.env).categories;
  match categories.find? catName with
-  | some (ParserCategory.pratt tables leadingIdentAsSymbol) => prattParser catName tables leadingIdentAsSymbol rbp ctx s
-  | some (ParserCategory.simple parsers)                    => longestMatchFn parsers rbp ctx s
-  | none                                                    => s.mkUnexpectedError ("unknown parser category '" ++ toString catName ++ "'")
+  | some cat => prattParser catName cat.tables cat.leadingIdentAsSymbol rbp ctx s
+  | none     => s.mkUnexpectedError ("unknown parser category '" ++ toString catName ++ "'")

@[init] def setCategoryParserFnRef : IO Unit :=
 categoryParserFnRef.set categoryParserFnImpl
@ -1829,16 +1793,15 @@ def mkParserState (input : String) : ParserState :=
 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 (ParserCategory.pratt tables leadingIdentAsSymbol) =>
+| some cat =>
  let c := mkParserContext env (mkInputContext input fileName);
  let s := mkParserState input;
  let s := whitespace c s;
-  let s := prattParser catName tables leadingIdentAsSymbol (0 : Nat) c s;
+  let s := prattParser catName cat.tables cat.leadingIdentAsSymbol (0 : Nat) c s;
  if s.hasError then
    Except.error (s.toErrorMsg c)
  else
    Except.ok s.stxStack.back
-| some _ => throw "runParserCategory does not support simple parsers yet"
 | none => throwUnknownParserCategory catName

 def declareBuiltinParser (env : Environment) (addFnName : Name) (catName : Name) (declName : Name) : IO Environment :=
@ -1922,12 +1885,8 @@ registerAttributeImplBuilder `parserAttr $ fun args =>
  | [DataValue.ofName attrName, DataValue.ofName catName] => pure $ mkParserAttributeImpl attrName catName
  | _ => throw ("invalid parser attribute implementation builder arguments")

-def registerPrattParserCategory (env : Environment) (attrName : Name) (catName : Name) (leadingIdentAsSymbol := false) : IO Environment := do
-env ← IO.ofExcept $ addPrattParserCategory env catName leadingIdentAsSymbol;
-registerAttributeOfBuilder env `parserAttr [DataValue.ofName attrName, DataValue.ofName catName]
-
-def registerSimpleParserCategory (env : Environment) (attrName : Name) (catName : Name) : IO Environment := do
-env ← IO.ofExcept $ addSimpleParserCategory env catName;
+def registerParserCategory (env : Environment) (attrName : Name) (catName : Name) (leadingIdentAsSymbol := false) : IO Environment := do
+env ← IO.ofExcept $ addParserCategory env catName leadingIdentAsSymbol;
 registerAttributeOfBuilder env `parserAttr [DataValue.ofName attrName, DataValue.ofName catName]

 -- declare `termParser` here since it is used everywhere via antiquotations
--- a/stage0/src/Init/Lean/Parser/Syntax.lean
+++ b/stage0/src/Init/Lean/Parser/Syntax.lean
@ -63,7 +63,7 @@ def identPrec  := parser! ident >> optPrecedence
@[builtinCommandParser] def «notation»    := parser! "notation" >> many (strLitPrec <|> quotedSymbolPrec <|> identPrec) >> (" := " <|> darrow) >> termParser
@[builtinCommandParser] def «macro_rules» := parser! "macro_rules" >> many1Indent Term.matchAlt "'match' alternatives must be indented"
@[builtinCommandParser] def «syntax»      := parser! "syntax " >> optional ("[" >> ident >> "]") >> many1 syntaxParser >> " : " >> ident
-@[builtinCommandParser] def syntaxCat     := parser! "declare_syntax_cat " >> ident >> optional (":" >> (nonReservedSymbol "simple" <|> nonReservedSymbol "pratt"))
+@[builtinCommandParser] def syntaxCat     := parser! "declare_syntax_cat " >> ident
 def macroArgType   := nonReservedSymbol "ident" <|> nonReservedSymbol "num" <|> nonReservedSymbol "str" <|> nonReservedSymbol "char" <|> (ident >> optPrecedence)
 def macroArgSimple := parser! ident >> checkNoWsBefore "no space before ':'" >> ":" >> macroArgType
 def macroArg  := try strLitPrec <|> try macroArgSimple
--- a/stage0/stdlib/Init/Lean/Elab/Syntax.c
+++ b/stage0/stdlib/Init/Lean/Elab/Syntax.c
--- a/stage0/stdlib/Init/Lean/Parser/Parser.c
+++ b/stage0/stdlib/Init/Lean/Parser/Parser.c
--- a/stage0/stdlib/Init/Lean/Parser/Syntax.c
+++ b/stage0/stdlib/Init/Lean/Parser/Syntax.c
@ -17,12 +17,10 @@ lean_object* l_Lean_Parser_Command_infixl___elambda__1___closed__8;
 lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Command_notation___elambda__1___spec__1(uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Command_macroHead___closed__3;
 lean_object* l_Lean_Parser_Command_syntax___elambda__1___closed__6;
-lean_object* l_Lean_Parser_Command_syntaxCat___elambda__1___closed__15;
 lean_object* l_Lean_Parser_Syntax_orelse___closed__5;
 lean_object* l_Lean_Parser_Syntax_many___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Command_prefix___elambda__1___closed__8;
 lean_object* l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__1;
-lean_object* l_Lean_Parser_Command_syntaxCat___elambda__1___closed__14;
 lean_object* l_Lean_Parser_Syntax_str___elambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Command_infixl___closed__5;
 lean_object* l_Lean_Parser_Syntax_char;
@ -151,7 +149,6 @@ extern lean_object* l_Lean_Parser_Term_listLit___elambda__1___closed__5;
 lean_object* l_Lean_Parser_Syntax_ident___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Command_macro___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Command_macroHead___closed__1;
-lean_object* l_Lean_Parser_Command_syntaxCat___closed__11;
 lean_object* l_Lean_Parser_precedence___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Syntax_ident___elambda__1___closed__1;
 lean_object* l_Lean_Parser_optPrecedence;
@ -216,7 +213,6 @@ lean_object* l_Lean_Parser_Command_infix___closed__4;
 lean_object* l_Lean_Parser_Syntax_char___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Command_prefix___closed__4;
 lean_object* l_Lean_Parser_Command_infixl___closed__3;
-lean_object* l_Lean_Parser_Command_syntaxCat___elambda__1___closed__16;
 lean_object* l_Lean_Parser_Syntax_lookahead___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Command_infix___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Command_macro___closed__3;
@ -261,7 +257,6 @@ lean_object* l_Lean_Parser_Command_mixfixSymbol___closed__4;
 lean_object* l_Lean_Parser_Command_strLitPrec___elambda__1___closed__2;
 lean_object* l_Lean_Parser_quotedSymbol(uint8_t);
 lean_object* l_Lean_Parser_Syntax_num___elambda__1___closed__1;
-lean_object* l_Lean_Parser_Command_syntaxCat___elambda__1___closed__10;
 lean_object* lean_nat_sub(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Syntax_sepBy1___closed__2;
 lean_object* l_Lean_Parser_precedence___elambda__1(lean_object*, lean_object*, lean_object*);
@ -281,7 +276,6 @@ lean_object* l_Lean_Parser_nonReservedSymbolInfo(lean_object*, uint8_t);
 lean_object* l_Lean_Parser_Syntax_str___closed__2;
 lean_object* l_Lean_Parser_Syntax_optional___closed__4;
 lean_object* l_Lean_Parser_Command_syntax___elambda__1___closed__7;
-lean_object* l_Lean_Parser_Command_syntaxCat___closed__7;
 lean_object* l_Lean_Parser_Command_syntax___closed__3;
 lean_object* l_Lean_Parser_Syntax_orelse___closed__3;
 lean_object* l_Lean_Parser_Command_macroArgType___closed__3;
@ -309,7 +303,6 @@ lean_object* l_Lean_Parser_optionaInfo(lean_object*);
 lean_object* l_Lean_Parser_Command_syntaxCat___elambda__1(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Lean_Parser_Term_tacticStxQuot___closed__2;
 lean_object* l_Lean_Parser_Syntax_paren___closed__5;
-lean_object* l_Lean_Parser_Command_syntaxCat___closed__12;
 lean_object* l_Lean_Parser_Command_prefix___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Syntax_optional___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Syntax_paren___elambda__1___closed__4;
@ -327,7 +320,6 @@ lean_object* l_Lean_Parser_Command_postfix___elambda__1___closed__5;
 lean_object* l_Lean_Parser_Command_macroArgType___closed__5;
 lean_object* l_Lean_Parser_Command_syntax___closed__10;
 lean_object* l_Lean_Parser_Syntax_ident;
-lean_object* l_Lean_Parser_Command_syntaxCat___elambda__1___closed__12;
 lean_object* l_Lean_Parser_Syntax_num___closed__4;
 lean_object* l_Lean_Parser_categoryParserOfStack(uint8_t, lean_object*, lean_object*);
 extern lean_object* l_Char_HasRepr___closed__1;
@ -359,7 +351,6 @@ extern lean_object* l_Lean_Parser_Term_haveAssign___elambda__1___closed__5;
 lean_object* l_Lean_Parser_manyAux___main___at_Lean_Parser_Command_macro__rules___elambda__1___spec__2(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Command_syntax___elambda__1___closed__5;
 extern lean_object* l_Lean_Parser_Level_paren___elambda__1___closed__11;
-lean_object* l_Lean_Parser_Command_syntaxCat___closed__10;
 lean_object* l_Lean_Parser_Syntax_char___elambda__1___closed__2;
 lean_object* l_Lean_Parser_Command_mixfixKind___closed__1;
 lean_object* l_Lean_Parser_Command_reserve___elambda__1___closed__3;
@ -375,7 +366,6 @@ lean_object* l_Lean_Parser_Command_infixr___closed__5;
 lean_object* l_Lean_Parser_maxPrec___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Command_infixr___closed__3;
 lean_object* l_Lean_Parser_Command_identPrec___elambda__1___closed__1;
-lean_object* l_Lean_Parser_Command_syntaxCat___elambda__1___closed__11;
 lean_object* l_Lean_Parser_Command_macroTail___closed__4;
 lean_object* l_Lean_Parser_Syntax_lookahead___elambda__1___closed__6;
 lean_object* l_Lean_Parser_registerBuiltinParserAttribute(lean_object*, lean_object*, uint8_t, lean_object*);
@ -542,7 +532,6 @@ lean_object* l_Lean_Parser_strLitFn___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Command_syntaxCat___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Syntax_ident___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Command_mixfixSymbol;
-lean_object* l_Lean_Parser_Command_syntaxCat___closed__8;
 lean_object* l_Lean_Parser_Command_quotedSymbolPrec___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Syntax_sepBy1___closed__3;
 lean_object* l_Lean_Parser_Syntax_sepBy1___closed__5;
@ -565,7 +554,6 @@ lean_object* l_Lean_Parser_Command_macro___elambda__1___closed__8;
 extern lean_object* l_Lean_Level_LevelToFormat_Result_format___main___closed__3;
 lean_object* l_Lean_Parser_Syntax_orelse___closed__2;
 lean_object* l_Lean_Parser_Command_syntax___elambda__1___closed__4;
-lean_object* l_Lean_Parser_Command_syntaxCat___elambda__1___closed__17;
 lean_object* l_Lean_Parser_Syntax_char___closed__3;
 lean_object* l_Lean_Parser_Syntax_optional___elambda__1___closed__3;
 lean_object* l_Lean_Parser_Command_notation___elambda__1___closed__7;
@ -589,7 +577,6 @@ lean_object* l_Lean_Parser_Command_reserve___elambda__1___closed__6;
 lean_object* l_Lean_Parser_Command_quotedSymbolPrec___elambda__1___closed__1;
 lean_object* l_Lean_Parser_Command_macro___closed__8;
 lean_object* l_Lean_Parser_Command_mixfixKind___closed__4;
-lean_object* l_Lean_Parser_Command_syntaxCat___closed__9;
 lean_object* l_Lean_Parser_Command_macroArgSimple___closed__2;
 lean_object* l_Lean_Parser_Command_reserve___closed__7;
 lean_object* l_Lean_Parser_Syntax_optional___elambda__1___closed__5;
@ -662,7 +649,6 @@ lean_object* l_Lean_Parser_Command_macro___closed__4;
 lean_object* l_Lean_Parser_Syntax_orelse___elambda__1(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Parser_Syntax_optional___closed__1;
 lean_object* l_Lean_Parser_Syntax_cat___elambda__1___closed__1;
-lean_object* l_Lean_Parser_Command_syntaxCat___elambda__1___closed__13;
 lean_object* l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__4;
 lean_object* l_Lean_Parser_Command_quotedSymbolPrec___elambda__1___closed__3;
 lean_object* l_Lean_Parser_numLitFn___rarg(lean_object*, lean_object*);
@ -10498,80 +10484,6 @@ return x_2;
 lean_object* _init_l_Lean_Parser_Command_syntaxCat___elambda__1___closed__7() {
 _start:
 {
-lean_object* x_1; 
-x_1 = lean_mk_string("simple");
-return x_1;
-}
-}
-lean_object* _init_l_Lean_Parser_Command_syntaxCat___elambda__1___closed__8() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__7;
-x_2 = l_String_trim(x_1);
-return x_2;
-}
-}
-lean_object* _init_l_Lean_Parser_Command_syntaxCat___elambda__1___closed__9() {
-_start:
-{
-lean_object* x_1; 
-x_1 = lean_mk_string("pratt");
-return x_1;
-}
-}
-lean_object* _init_l_Lean_Parser_Command_syntaxCat___elambda__1___closed__10() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__9;
-x_2 = l_String_trim(x_1);
-return x_2;
-}
-}
-lean_object* _init_l_Lean_Parser_Command_syntaxCat___elambda__1___closed__11() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Char_HasRepr___closed__1;
-x_2 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__8;
-x_3 = lean_string_append(x_1, x_2);
-return x_3;
-}
-}
-lean_object* _init_l_Lean_Parser_Command_syntaxCat___elambda__1___closed__12() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__11;
-x_2 = l_Char_HasRepr___closed__1;
-x_3 = lean_string_append(x_1, x_2);
-return x_3;
-}
-}
-lean_object* _init_l_Lean_Parser_Command_syntaxCat___elambda__1___closed__13() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Char_HasRepr___closed__1;
-x_2 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__10;
-x_3 = lean_string_append(x_1, x_2);
-return x_3;
-}
-}
-lean_object* _init_l_Lean_Parser_Command_syntaxCat___elambda__1___closed__14() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__13;
-x_2 = l_Char_HasRepr___closed__1;
-x_3 = lean_string_append(x_1, x_2);
-return x_3;
-}
-}
-lean_object* _init_l_Lean_Parser_Command_syntaxCat___elambda__1___closed__15() {
-_start:
-{
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = l_Char_HasRepr___closed__1;
 x_2 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__6;
@ -10579,22 +10491,22 @@ x_3 = lean_string_append(x_1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_Lean_Parser_Command_syntaxCat___elambda__1___closed__16() {
+lean_object* _init_l_Lean_Parser_Command_syntaxCat___elambda__1___closed__8() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__15;
+x_1 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__7;
 x_2 = l_Char_HasRepr___closed__1;
 x_3 = lean_string_append(x_1, x_2);
 return x_3;
 }
 }
-lean_object* _init_l_Lean_Parser_Command_syntaxCat___elambda__1___closed__17() {
+lean_object* _init_l_Lean_Parser_Command_syntaxCat___elambda__1___closed__9() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
 x_1 = lean_box(0);
-x_2 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__16;
+x_2 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__8;
 x_3 = lean_alloc_ctor(1, 2, 0);
 lean_ctor_set(x_3, 0, x_2);
 lean_ctor_set(x_3, 1, x_1);
@ -10653,7 +10565,7 @@ return x_11;
 }
 else
 {
-lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_85; lean_object* x_86; 
+lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_29; lean_object* x_30; 
 lean_inc(x_10);
 x_16 = l_Lean_Parser_ParserState_restore(x_11, x_9, x_10);
 lean_dec(x_9);
@ -10662,285 +10574,88 @@ lean_inc(x_17);
 x_18 = lean_array_get_size(x_17);
 lean_dec(x_17);
 lean_inc(x_2);
-x_85 = l_Lean_Parser_tokenFn(x_2, x_16);
-x_86 = lean_ctor_get(x_85, 3);
-lean_inc(x_86);
-if (lean_obj_tag(x_86) == 0)
+x_29 = l_Lean_Parser_tokenFn(x_2, x_16);
+x_30 = lean_ctor_get(x_29, 3);
+lean_inc(x_30);
+if (lean_obj_tag(x_30) == 0)
 {
-lean_object* x_87; lean_object* x_88; 
-x_87 = lean_ctor_get(x_85, 0);
-lean_inc(x_87);
-x_88 = l_Array_back___at___private_Init_Lean_Parser_Parser_6__updateCache___spec__1(x_87);
-lean_dec(x_87);
-if (lean_obj_tag(x_88) == 2)
+lean_object* x_31; lean_object* x_32; 
+x_31 = lean_ctor_get(x_29, 0);
+lean_inc(x_31);
+x_32 = l_Array_back___at___private_Init_Lean_Parser_Parser_6__updateCache___spec__1(x_31);
+lean_dec(x_31);
+if (lean_obj_tag(x_32) == 2)
 {
-lean_object* x_89; lean_object* x_90; uint8_t x_91; 
-x_89 = lean_ctor_get(x_88, 1);
-lean_inc(x_89);
-lean_dec(x_88);
-x_90 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__6;
-x_91 = lean_string_dec_eq(x_89, x_90);
-lean_dec(x_89);
-if (x_91 == 0)
+lean_object* x_33; lean_object* x_34; uint8_t x_35; 
+x_33 = lean_ctor_get(x_32, 1);
+lean_inc(x_33);
+lean_dec(x_32);
+x_34 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__6;
+x_35 = lean_string_dec_eq(x_33, x_34);
+lean_dec(x_33);
+if (x_35 == 0)
 {
-lean_object* x_92; lean_object* x_93; 
-x_92 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__17;
+lean_object* x_36; lean_object* x_37; 
+x_36 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__9;
 lean_inc(x_10);
-x_93 = l_Lean_Parser_ParserState_mkErrorsAt(x_85, x_92, x_10);
-x_19 = x_93;
-goto block_84;
+x_37 = l_Lean_Parser_ParserState_mkErrorsAt(x_29, x_36, x_10);
+x_19 = x_37;
+goto block_28;
 }
 else
 {
-x_19 = x_85;
-goto block_84;
+x_19 = x_29;
+goto block_28;
 }
 }
 else
 {
-lean_object* x_94; lean_object* x_95; 
-lean_dec(x_88);
-x_94 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__17;
+lean_object* x_38; lean_object* x_39; 
+lean_dec(x_32);
+x_38 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__9;
 lean_inc(x_10);
-x_95 = l_Lean_Parser_ParserState_mkErrorsAt(x_85, x_94, x_10);
-x_19 = x_95;
-goto block_84;
+x_39 = l_Lean_Parser_ParserState_mkErrorsAt(x_29, x_38, x_10);
+x_19 = x_39;
+goto block_28;
 }
 }
 else
 {
-lean_object* x_96; lean_object* x_97; 
-lean_dec(x_86);
-x_96 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__17;
+lean_object* x_40; lean_object* x_41; 
+lean_dec(x_30);
+x_40 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__9;
 lean_inc(x_10);
-x_97 = l_Lean_Parser_ParserState_mkErrorsAt(x_85, x_96, x_10);
-x_19 = x_97;
-goto block_84;
+x_41 = l_Lean_Parser_ParserState_mkErrorsAt(x_29, x_40, x_10);
+x_19 = x_41;
+goto block_28;
 }
-block_84:
+block_28:
 {
 lean_object* x_20; 
 x_20 = lean_ctor_get(x_19, 3);
 lean_inc(x_20);
 if (lean_obj_tag(x_20) == 0)
 {
-lean_object* x_21; lean_object* x_22; 
-lean_inc(x_2);
+lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; 
 x_21 = lean_apply_3(x_5, x_1, x_2, x_19);
-x_22 = lean_ctor_get(x_21, 3);
-lean_inc(x_22);
-if (lean_obj_tag(x_22) == 0)
-{
-lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_47; lean_object* x_65; lean_object* x_66; 
-x_23 = lean_ctor_get(x_21, 0);
-lean_inc(x_23);
-x_24 = lean_array_get_size(x_23);
-lean_dec(x_23);
-x_25 = lean_ctor_get(x_21, 1);
-lean_inc(x_25);
-lean_inc(x_2);
-x_65 = l_Lean_Parser_tokenFn(x_2, x_21);
-x_66 = lean_ctor_get(x_65, 3);
-lean_inc(x_66);
-if (lean_obj_tag(x_66) == 0)
-{
-lean_object* x_67; lean_object* x_68; 
-x_67 = lean_ctor_get(x_65, 0);
-lean_inc(x_67);
-x_68 = l_Array_back___at___private_Init_Lean_Parser_Parser_6__updateCache___spec__1(x_67);
-lean_dec(x_67);
-if (lean_obj_tag(x_68) == 2)
-{
-lean_object* x_69; lean_object* x_70; uint8_t x_71; 
-x_69 = lean_ctor_get(x_68, 1);
-lean_inc(x_69);
-lean_dec(x_68);
-x_70 = l_Lean_Parser_mkAntiquot___closed__4;
-x_71 = lean_string_dec_eq(x_69, x_70);
-lean_dec(x_69);
-if (x_71 == 0)
-{
-lean_object* x_72; lean_object* x_73; 
-x_72 = l_Lean_Parser_precedence___elambda__1___closed__7;
-lean_inc(x_25);
-x_73 = l_Lean_Parser_ParserState_mkErrorsAt(x_65, x_72, x_25);
-x_47 = x_73;
-goto block_64;
-}
-else
-{
-x_47 = x_65;
-goto block_64;
-}
-}
-else
-{
-lean_object* x_74; lean_object* x_75; 
-lean_dec(x_68);
-x_74 = l_Lean_Parser_precedence___elambda__1___closed__7;
-lean_inc(x_25);
-x_75 = l_Lean_Parser_ParserState_mkErrorsAt(x_65, x_74, x_25);
-x_47 = x_75;
-goto block_64;
-}
-}
-else
-{
-lean_object* x_76; lean_object* x_77; 
-lean_dec(x_66);
-x_76 = l_Lean_Parser_precedence___elambda__1___closed__7;
-lean_inc(x_25);
-x_77 = l_Lean_Parser_ParserState_mkErrorsAt(x_65, x_76, x_25);
-x_47 = x_77;
-goto block_64;
-}
-block_46:
-{
-lean_object* x_27; 
-x_27 = lean_ctor_get(x_26, 3);
-lean_inc(x_27);
-if (lean_obj_tag(x_27) == 0)
-{
-lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; 
-lean_dec(x_25);
-x_28 = l_Lean_nullKind;
-x_29 = l_Lean_Parser_ParserState_mkNode(x_26, x_28, x_24);
-x_30 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__2;
-x_31 = l_Lean_Parser_ParserState_mkNode(x_29, x_30, x_18);
-x_32 = l_Lean_Parser_mergeOrElseErrors(x_31, x_13, x_10);
+x_22 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__2;
+x_23 = l_Lean_Parser_ParserState_mkNode(x_21, x_22, x_18);
+x_24 = l_Lean_Parser_mergeOrElseErrors(x_23, x_13, x_10);
 lean_dec(x_10);
-return x_32;
+return x_24;
 }
 else
 {
-lean_object* x_33; uint8_t x_34; 
-lean_dec(x_27);
-x_33 = lean_ctor_get(x_26, 1);
-lean_inc(x_33);
-x_34 = lean_nat_dec_eq(x_33, x_25);
-lean_dec(x_33);
-if (x_34 == 0)
-{
-lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; 
-lean_dec(x_25);
-x_35 = l_Lean_nullKind;
-x_36 = l_Lean_Parser_ParserState_mkNode(x_26, x_35, x_24);
-x_37 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__2;
-x_38 = l_Lean_Parser_ParserState_mkNode(x_36, x_37, x_18);
-x_39 = l_Lean_Parser_mergeOrElseErrors(x_38, x_13, x_10);
-lean_dec(x_10);
-return x_39;
-}
-else
-{
-lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; 
-x_40 = l_Lean_Parser_ParserState_restore(x_26, x_24, x_25);
-x_41 = l_Lean_nullKind;
-x_42 = l_Lean_Parser_ParserState_mkNode(x_40, x_41, x_24);
-x_43 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__2;
-x_44 = l_Lean_Parser_ParserState_mkNode(x_42, x_43, x_18);
-x_45 = l_Lean_Parser_mergeOrElseErrors(x_44, x_13, x_10);
-lean_dec(x_10);
-return x_45;
-}
-}
-}
-block_64:
-{
-lean_object* x_48; 
-x_48 = lean_ctor_get(x_47, 3);
-lean_inc(x_48);
-if (lean_obj_tag(x_48) == 0)
-{
-lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; 
-x_49 = lean_ctor_get(x_47, 0);
-lean_inc(x_49);
-x_50 = lean_array_get_size(x_49);
-lean_dec(x_49);
-x_51 = lean_ctor_get(x_47, 1);
-lean_inc(x_51);
-x_52 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__8;
-x_53 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__12;
-lean_inc(x_2);
-x_54 = l_Lean_Parser_nonReservedSymbolFnAux(x_52, x_53, x_2, x_47);
-x_55 = lean_ctor_get(x_54, 3);
-lean_inc(x_55);
-if (lean_obj_tag(x_55) == 0)
-{
-lean_dec(x_51);
-lean_dec(x_50);
-lean_dec(x_2);
-x_26 = x_54;
-goto block_46;
-}
-else
-{
-lean_object* x_56; lean_object* x_57; uint8_t x_58; 
-x_56 = lean_ctor_get(x_55, 0);
-lean_inc(x_56);
-lean_dec(x_55);
-x_57 = lean_ctor_get(x_54, 1);
-lean_inc(x_57);
-x_58 = lean_nat_dec_eq(x_57, x_51);
-lean_dec(x_57);
-if (x_58 == 0)
-{
-lean_dec(x_56);
-lean_dec(x_51);
-lean_dec(x_50);
-lean_dec(x_2);
-x_26 = x_54;
-goto block_46;
-}
-else
-{
-lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; 
-lean_inc(x_51);
-x_59 = l_Lean_Parser_ParserState_restore(x_54, x_50, x_51);
-lean_dec(x_50);
-x_60 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__10;
-x_61 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__14;
-x_62 = l_Lean_Parser_nonReservedSymbolFnAux(x_60, x_61, x_2, x_59);
-x_63 = l_Lean_Parser_mergeOrElseErrors(x_62, x_56, x_51);
-lean_dec(x_51);
-x_26 = x_63;
-goto block_46;
-}
-}
-}
-else
-{
-lean_dec(x_48);
-lean_dec(x_2);
-x_26 = x_47;
-goto block_46;
-}
-}
-}
-else
-{
-lean_object* x_78; lean_object* x_79; lean_object* x_80; 
-lean_dec(x_22);
-lean_dec(x_2);
-x_78 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__2;
-x_79 = l_Lean_Parser_ParserState_mkNode(x_21, x_78, x_18);
-x_80 = l_Lean_Parser_mergeOrElseErrors(x_79, x_13, x_10);
-lean_dec(x_10);
-return x_80;
-}
-}
-else
-{
-lean_object* x_81; lean_object* x_82; lean_object* x_83; 
+lean_object* x_25; lean_object* x_26; lean_object* x_27; 
 lean_dec(x_20);
 lean_dec(x_5);
 lean_dec(x_2);
 lean_dec(x_1);
-x_81 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__2;
-x_82 = l_Lean_Parser_ParserState_mkNode(x_19, x_81, x_18);
-x_83 = l_Lean_Parser_mergeOrElseErrors(x_82, x_13, x_10);
+x_25 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__2;
+x_26 = l_Lean_Parser_ParserState_mkNode(x_19, x_25, x_18);
+x_27 = l_Lean_Parser_mergeOrElseErrors(x_26, x_13, x_10);
 lean_dec(x_10);
-return x_83;
+return x_27;
 }
 }
 }
@ -10960,97 +10675,38 @@ return x_3;
 lean_object* _init_l_Lean_Parser_Command_syntaxCat___closed__2() {
 _start:
 {
-lean_object* x_1; uint8_t x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__8;
-x_2 = 0;
-x_3 = l_Lean_Parser_nonReservedSymbolInfo(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_ident___elambda__1___closed__4;
+x_2 = lean_ctor_get(x_1, 0);
+lean_inc(x_2);
+x_3 = l_Lean_Parser_Command_syntaxCat___closed__1;
+x_4 = l_Lean_Parser_andthenInfo(x_3, x_2);
+return x_4;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_syntaxCat___closed__3() {
 _start:
 {
-lean_object* x_1; uint8_t x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__10;
-x_2 = 0;
-x_3 = l_Lean_Parser_nonReservedSymbolInfo(x_1, x_2);
+lean_object* x_1; lean_object* x_2; lean_object* x_3; 
+x_1 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__2;
+x_2 = l_Lean_Parser_Command_syntaxCat___closed__2;
+x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
 return x_3;
 }
 }
 lean_object* _init_l_Lean_Parser_Command_syntaxCat___closed__4() {
 _start:
 {
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Command_syntaxCat___closed__2;
-x_2 = l_Lean_Parser_Command_syntaxCat___closed__3;
-x_3 = l_Lean_Parser_orelseInfo(x_1, x_2);
-return x_3;
-}
-}
-lean_object* _init_l_Lean_Parser_Command_syntaxCat___closed__5() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_mkAntiquot___closed__5;
-x_2 = l_Lean_Parser_Command_syntaxCat___closed__4;
-x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
-return x_3;
-}
-}
-lean_object* _init_l_Lean_Parser_Command_syntaxCat___closed__6() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; 
-x_1 = l_Lean_Parser_Command_syntaxCat___closed__5;
-x_2 = l_Lean_Parser_optionaInfo(x_1);
-return x_2;
-}
-}
-lean_object* _init_l_Lean_Parser_Command_syntaxCat___closed__7() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
-x_1 = l_Lean_Parser_Level_ident___elambda__1___closed__4;
-x_2 = lean_ctor_get(x_1, 0);
-lean_inc(x_2);
-x_3 = l_Lean_Parser_Command_syntaxCat___closed__6;
-x_4 = l_Lean_Parser_andthenInfo(x_2, x_3);
-return x_4;
-}
-}
-lean_object* _init_l_Lean_Parser_Command_syntaxCat___closed__8() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Command_syntaxCat___closed__1;
-x_2 = l_Lean_Parser_Command_syntaxCat___closed__7;
-x_3 = l_Lean_Parser_andthenInfo(x_1, x_2);
-return x_3;
-}
-}
-lean_object* _init_l_Lean_Parser_Command_syntaxCat___closed__9() {
-_start:
-{
-lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__2;
-x_2 = l_Lean_Parser_Command_syntaxCat___closed__8;
-x_3 = l_Lean_Parser_nodeInfo(x_1, x_2);
-return x_3;
-}
-}
-lean_object* _init_l_Lean_Parser_Command_syntaxCat___closed__10() {
-_start:
-{
 lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; 
 x_1 = l_Lean_Parser_Command_syntaxCat___elambda__1___closed__4;
 x_2 = lean_ctor_get(x_1, 0);
 lean_inc(x_2);
-x_3 = l_Lean_Parser_Command_syntaxCat___closed__9;
+x_3 = l_Lean_Parser_Command_syntaxCat___closed__3;
 x_4 = l_Lean_Parser_orelseInfo(x_2, x_3);
 return x_4;
 }
 }
-lean_object* _init_l_Lean_Parser_Command_syntaxCat___closed__11() {
+lean_object* _init_l_Lean_Parser_Command_syntaxCat___closed__5() {
 _start:
 {
 lean_object* x_1; 
@ -11058,12 +10714,12 @@ x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Command_syntaxCat___elambda__1),
 return x_1;
 }
 }
-lean_object* _init_l_Lean_Parser_Command_syntaxCat___closed__12() {
+lean_object* _init_l_Lean_Parser_Command_syntaxCat___closed__6() {
 _start:
 {
 lean_object* x_1; lean_object* x_2; lean_object* x_3; 
-x_1 = l_Lean_Parser_Command_syntaxCat___closed__10;
-x_2 = l_Lean_Parser_Command_syntaxCat___closed__11;
+x_1 = l_Lean_Parser_Command_syntaxCat___closed__4;
+x_2 = l_Lean_Parser_Command_syntaxCat___closed__5;
 x_3 = lean_alloc_ctor(0, 2, 0);
 lean_ctor_set(x_3, 0, x_1);
 lean_ctor_set(x_3, 1, x_2);
@ -11074,7 +10730,7 @@ lean_object* _init_l_Lean_Parser_Command_syntaxCat() {
 _start:
 {
 lean_object* x_1; 
-x_1 = l_Lean_Parser_Command_syntaxCat___closed__12;
+x_1 = l_Lean_Parser_Command_syntaxCat___closed__6;
 return x_1;
 }
 }
@ -15054,22 +14710,6 @@ l_Lean_Parser_Command_syntaxCat___elambda__1___closed__8 = _init_l_Lean_Parser_C
 lean_mark_persistent(l_Lean_Parser_Command_syntaxCat___elambda__1___closed__8);
 l_Lean_Parser_Command_syntaxCat___elambda__1___closed__9 = _init_l_Lean_Parser_Command_syntaxCat___elambda__1___closed__9();
 lean_mark_persistent(l_Lean_Parser_Command_syntaxCat___elambda__1___closed__9);
-l_Lean_Parser_Command_syntaxCat___elambda__1___closed__10 = _init_l_Lean_Parser_Command_syntaxCat___elambda__1___closed__10();
-lean_mark_persistent(l_Lean_Parser_Command_syntaxCat___elambda__1___closed__10);
-l_Lean_Parser_Command_syntaxCat___elambda__1___closed__11 = _init_l_Lean_Parser_Command_syntaxCat___elambda__1___closed__11();
-lean_mark_persistent(l_Lean_Parser_Command_syntaxCat___elambda__1___closed__11);
-l_Lean_Parser_Command_syntaxCat___elambda__1___closed__12 = _init_l_Lean_Parser_Command_syntaxCat___elambda__1___closed__12();
-lean_mark_persistent(l_Lean_Parser_Command_syntaxCat___elambda__1___closed__12);
-l_Lean_Parser_Command_syntaxCat___elambda__1___closed__13 = _init_l_Lean_Parser_Command_syntaxCat___elambda__1___closed__13();
-lean_mark_persistent(l_Lean_Parser_Command_syntaxCat___elambda__1___closed__13);
-l_Lean_Parser_Command_syntaxCat___elambda__1___closed__14 = _init_l_Lean_Parser_Command_syntaxCat___elambda__1___closed__14();
-lean_mark_persistent(l_Lean_Parser_Command_syntaxCat___elambda__1___closed__14);
-l_Lean_Parser_Command_syntaxCat___elambda__1___closed__15 = _init_l_Lean_Parser_Command_syntaxCat___elambda__1___closed__15();
-lean_mark_persistent(l_Lean_Parser_Command_syntaxCat___elambda__1___closed__15);
-l_Lean_Parser_Command_syntaxCat___elambda__1___closed__16 = _init_l_Lean_Parser_Command_syntaxCat___elambda__1___closed__16();
-lean_mark_persistent(l_Lean_Parser_Command_syntaxCat___elambda__1___closed__16);
-l_Lean_Parser_Command_syntaxCat___elambda__1___closed__17 = _init_l_Lean_Parser_Command_syntaxCat___elambda__1___closed__17();
-lean_mark_persistent(l_Lean_Parser_Command_syntaxCat___elambda__1___closed__17);
 l_Lean_Parser_Command_syntaxCat___closed__1 = _init_l_Lean_Parser_Command_syntaxCat___closed__1();
 lean_mark_persistent(l_Lean_Parser_Command_syntaxCat___closed__1);
 l_Lean_Parser_Command_syntaxCat___closed__2 = _init_l_Lean_Parser_Command_syntaxCat___closed__2();
@ -15082,18 +14722,6 @@ l_Lean_Parser_Command_syntaxCat___closed__5 = _init_l_Lean_Parser_Command_syntax
 lean_mark_persistent(l_Lean_Parser_Command_syntaxCat___closed__5);
 l_Lean_Parser_Command_syntaxCat___closed__6 = _init_l_Lean_Parser_Command_syntaxCat___closed__6();
 lean_mark_persistent(l_Lean_Parser_Command_syntaxCat___closed__6);
-l_Lean_Parser_Command_syntaxCat___closed__7 = _init_l_Lean_Parser_Command_syntaxCat___closed__7();
-lean_mark_persistent(l_Lean_Parser_Command_syntaxCat___closed__7);
-l_Lean_Parser_Command_syntaxCat___closed__8 = _init_l_Lean_Parser_Command_syntaxCat___closed__8();
-lean_mark_persistent(l_Lean_Parser_Command_syntaxCat___closed__8);
-l_Lean_Parser_Command_syntaxCat___closed__9 = _init_l_Lean_Parser_Command_syntaxCat___closed__9();
-lean_mark_persistent(l_Lean_Parser_Command_syntaxCat___closed__9);
-l_Lean_Parser_Command_syntaxCat___closed__10 = _init_l_Lean_Parser_Command_syntaxCat___closed__10();
-lean_mark_persistent(l_Lean_Parser_Command_syntaxCat___closed__10);
-l_Lean_Parser_Command_syntaxCat___closed__11 = _init_l_Lean_Parser_Command_syntaxCat___closed__11();
-lean_mark_persistent(l_Lean_Parser_Command_syntaxCat___closed__11);
-l_Lean_Parser_Command_syntaxCat___closed__12 = _init_l_Lean_Parser_Command_syntaxCat___closed__12();
-lean_mark_persistent(l_Lean_Parser_Command_syntaxCat___closed__12);
 l_Lean_Parser_Command_syntaxCat = _init_l_Lean_Parser_Command_syntaxCat();
 lean_mark_persistent(l_Lean_Parser_Command_syntaxCat);
 res = l___regBuiltinParser_Lean_Parser_Command_syntaxCat(lean_io_mk_world());