feat(library/init/lean/syntax): primitives for creating and testing string and nat literals

library/init/lean/compiler/externattr.lean

@@ -42,6 +42,17 @@ structure ExternAttrData :=
 
 @[export lean.mk_extern_attr_data_core] def mkExternAttrData := ExternAttrData.mk
 
+private def syntaxToExternAttrData (s : Syntax) : Except String ExternAttrData :=
+match s with
+| Syntax.missing := Except.ok { entries := [ ExternEntry.adhoc `all ] }
+| Syntax.node _ args _ :=
+  if args.size == 0 then Except.error "unexpected kind of argument"
+  else
+    let i := 0 in
+    -- TODO
+    Except.ok { entries := [] }
+| _ := Except.error "unexpected kind of argument"
+
 -- def mkExternAttr : IO (ParametricAttribute ExternAttrData) :=
 -- registerParametricAttribute `extern "builtin and foreign functions" $ λ env declName stx,
 

library/init/lean/parser/parser.lean

@@ -464,9 +464,6 @@ def quotedCharFn : BasicParserFn
     else
       s.mkError "invalid escape sequence"
 
-def strLitKind : SyntaxNodeKind := `strLit
-def numLitKind : SyntaxNodeKind := `numLit
-
 /-- Push `(Syntax.node tk <new-atom>)` into syntax stack -/
 def mkNodeToken (n : SyntaxNodeKind) (startPos : Nat) : BasicParserFn :=
 λ c s,
@@ -477,9 +474,8 @@ let val       := input.extract startPos stopPos in
 let s         := whitespace c s in
 let wsStopPos := s.pos in
 let trailing  := { Substring . str := input, startPos := stopPos, stopPos := wsStopPos } in
-let atom      := Syntax.atom (some { leading := leading, pos := startPos, trailing := trailing }) val in
-let tk        := Syntax.node n (Array.singleton atom) [] in
-s.pushSyntax tk
+let info      := { SourceInfo . leading := leading, pos := startPos, trailing := trailing } in
+s.pushSyntax (mkLit n val (some info))
 
 partial def strLitFnAux (startPos : Nat) : BasicParserFn
 | c s :=
@@ -501,6 +497,7 @@ def decimalNumberFn (startPos : Nat) : BasicParserFn :=
   let i     := s.pos in
   let curr  := input.get i in
   let s :=
+    /- TODO(Leo): should we use a different kind for numerals containing decimal points? -/
     if curr == '.' then
       let i    := input.next i in
       let curr := input.get i in

library/init/lean/syntax.lean

@@ -33,6 +33,8 @@ abbrev SyntaxNodeKind := Name
 
 @[pattern] def choiceKind : SyntaxNodeKind := `choice
 @[pattern] def nullKind : SyntaxNodeKind := `null
+def strLitKind : SyntaxNodeKind := `strLit
+def numLitKind : SyntaxNodeKind := `numLit
 
 /- Syntax AST -/
 
@@ -207,19 +209,119 @@ protected partial def formatStx : Syntax → Format
 instance : HasFormat Syntax := ⟨Syntax.formatStx⟩
 instance : HasToString Syntax := ⟨toString ∘ format⟩
 
+end Syntax
+
 /- Helper functions for creating Syntax objects using C++ -/
 
 @[export lean.mk_syntax_atom_core]
 def mkSimpleAtom (val : String) : Syntax :=
-atom none val
+Syntax.atom none val
 
 @[export lean.mk_syntax_ident_core]
 def mkSimpleIdent (val : Name) : Syntax :=
-ident none (toString val).toSubstring val [] []
+Syntax.ident none (toString val).toSubstring val [] []
 
 @[export lean.mk_syntax_list_core]
 def mkListNode (args : Array Syntax) : Syntax :=
-node nullKind args []
+Syntax.node nullKind args []
+
+/- Helper functions for creating string and numeric literals -/
+
+def mkLit (kind : SyntaxNodeKind) (val : String) (info : Option SourceInfo := none) : Syntax :=
+let atom := Syntax.atom info val in
+Syntax.node kind (Array.singleton atom) []
+
+def mkStrLit (val : String) (info : Option SourceInfo := none) : Syntax :=
+mkLit strLitKind val info
+
+def mkNumLit (val : String) (info : Option SourceInfo := none) : Syntax :=
+mkLit numLitKind val info
+
+@[export lean.mk_syntax_str_lit_core]
+def mkStrLitAux (val : String) : Syntax :=
+mkStrLit val
+
+@[export lean.mk_syntax_num_lit_core]
+def mkNumLitAux (val : Nat) : Syntax :=
+mkNumLit (toString val)
+
+def Syntax.isStrLit : Syntax → Option String
+| (Syntax.node k args _) :=
+  if k == strLitKind && args.size == 1 then
+    match args.get 0 with
+    | (Syntax.atom _ val) := some val
+    | _ := none
+  else
+    none
+| _ := none
+
+/- Recall that we don't have special Syntax constructors for storing numeric atoms.
+   The idea is to have an extensible approach where embedded DSLs may have new kind of atoms and/or
+   different ways of representing them. So, our atoms contain just the parsed string.
+   The main Lean parser uses the kind `numLitKind` for storing natural numbers that can be encoded
+   in binary, octal, decimal and hexadecimal format. `isNatLit` implements a "decoder"
+   for Syntax objects representing these numerals. -/
+
+private partial def decodeBinLitAux (s : String) : Nat → Nat → Option Nat
+| i val :=
+  if s.atEnd i then some val
+  else
+    let c := s.get i in
+    if c == '0' then decodeBinLitAux (s.next i) (2*val)
+    else if c == '1' then decodeBinLitAux (s.next i) (2*val + 1)
+    else none
+
+private partial def decodeOctalLitAux (s : String) : Nat → Nat → Option Nat
+| i val :=
+  if s.atEnd i then some val
+  else
+    let c := s.get i in
+    if '0' ≤ c && c ≤ '7' then decodeOctalLitAux (s.next i) (8*val + c.toNat - '0'.toNat)
+    else none
+
+private partial def decodeHexLitAux (s : String) : Nat → Nat → Option Nat
+| i val :=
+  if s.atEnd i then some val
+  else
+    let c := s.get i in
+    if '0' ≤ c && c ≤ '9' then decodeHexLitAux (s.next i) (16*val + c.toNat - '0'.toNat)
+    else if 'a' ≤ c && c ≤ 'f' then decodeHexLitAux (s.next i) (16*val + 10 + c.toNat - 'a'.toNat)
+    else if 'A' ≤ c && c ≤ 'F' then decodeHexLitAux (s.next i) (16*val + 10 + c.toNat - 'A'.toNat)
+    else none
+
+private partial def decodeDecimalLitAux (s : String) : Nat → Nat → Option Nat
+| i val :=
+  if s.atEnd i then some val
+  else
+    let c := s.get i in
+    if '0' ≤ c && c ≤ '9' then decodeDecimalLitAux (s.next i) (10*val + c.toNat - '0'.toNat)
+    else none
+
+private def decodeNatLitVal (s : String) : Option Nat :=
+let len := s.length in
+if len == 0 then none
+else
+  let c := s.get 0 in
+  if c == '0' then
+    if len == 1 then some 0
+    else
+     let c := s.get 1 in
+     if c == 'x' || c == 'X' then decodeHexLitAux s 2 0
+     else if c == 'b' || c == 'B' then decodeBinLitAux s 2 0
+     else if c == 'o' || c == 'O' then decodeOctalLitAux s 2 0
+     else if c.isDigit then decodeDecimalLitAux s 0 0
+     else none
+  else if c.isDigit then decodeDecimalLitAux s 0 0
+  else none
+
+def Syntax.isNatLit : Syntax → Option Nat
+| (Syntax.node k args _) :=
+  if k == strLitKind && args.size == 1 then
+    match args.get 0 with
+    | (Syntax.atom _ val) := decodeNatLitVal val
+    | _ := none
+  else
+    none
+| _ := none
 
-end Syntax
 end Lean

src/frontends/lean/decl_attributes.cpp

@@ -79,10 +79,14 @@ expr decl_attributes::parse_attr_arg(parser & p, name const & attr_id) {
 object* mk_syntax_atom_core(object*);
 object* mk_syntax_ident_core(object*);
 object* mk_syntax_list_core(object*);
+object* mk_syntax_str_lit_core(object*);
+object* mk_syntax_num_lit_core(object*);
 
 syntax mk_syntax_atom(string_ref const & s) { return syntax(mk_syntax_atom_core(s.to_obj_arg())); }
 syntax mk_syntax_ident(name const & n) { return syntax(mk_syntax_ident_core(n.to_obj_arg())); }
 syntax mk_syntax_list(buffer<syntax> const & args) { return syntax(mk_syntax_list_core(to_array(args))); }
+syntax mk_syntax_str_lit(string_ref const & s) { return syntax(mk_syntax_str_lit_core(s.to_obj_arg())); }
+syntax mk_syntax_num_lit(nat const & n) { return syntax(mk_syntax_num_lit_core(n.to_obj_arg())); }
 
 syntax decl_attributes::expr_to_syntax(expr const & e) {
     buffer<expr> args;
@@ -98,10 +102,10 @@ syntax decl_attributes::expr_to_syntax(expr const & e) {
             literal const & val = lit_value(arg);
             switch (val.kind()) {
             case literal_kind::Nat:
-                new_args.push_back(mk_syntax_atom(string_ref(val.get_nat().to_std_string())));
+                new_args.push_back(mk_syntax_num_lit(val.get_nat()));
                 break;
             case literal_kind::String:
-                new_args.push_back(mk_syntax_atom(val.get_string()));
+                new_args.push_back(mk_syntax_str_lit(val.get_string()));
                 break;
             }
         } else {

src/stage0/init/lean/compiler/externattr.cpp

@@ -27,6 +27,7 @@ obj* l_Lean_ExternEntry_backend(obj*);
 namespace lean {
 obj* nat_sub(obj*, obj*);
 }
+obj* l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___boxed(obj*);
 namespace lean {
 obj* mk_adhoc_ext_entry_core(obj*);
 }
@@ -45,13 +46,15 @@ obj* mk_extern_call_core(obj*, obj*, obj*);
 }
 obj* l_String_Iterator_remainingBytes___main(obj*);
 obj* l_Lean_isExtern___boxed(obj*, obj*);
-obj* l___private_init_lean_compiler_externattr_1__parseOptNum(obj*, obj*, obj*);
+obj* l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__1;
 obj* l_List_foldl___main___at_Lean_mkSimpleFnCall___spec__1(obj*, obj*);
+obj* l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__3;
 namespace lean {
 obj* string_push(obj*, uint32);
 }
 obj* l_Lean_ExternEntry_backend___boxed(obj*);
 obj* l_Lean_expandExternPatternAux___boxed(obj*, obj*, obj*, obj*);
+obj* l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__2;
 namespace lean {
 obj* expand_extern_pattern_core(obj*, obj*);
 }
@@ -75,13 +78,16 @@ namespace lean {
 uint8 nat_dec_eq(obj*, obj*);
 }
 extern obj* l_Prod_HasRepr___rarg___closed__1;
+obj* l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData(obj*);
+obj* l___private_init_lean_compiler_externattr_2__parseOptNum(obj*, obj*, obj*);
 uint8 l_UInt32_decEq(uint32, uint32);
 namespace lean {
 obj* mk_inline_ext_entry_core(obj*, obj*);
 }
 obj* l_Lean_getExternAttrData___boxed(obj*, obj*);
+obj* l_Array_size(obj*, obj*);
 obj* l_Lean_getExternEntryForAux(obj*, obj*);
-obj* l___private_init_lean_compiler_externattr_1__parseOptNum___main(obj*, obj*, obj*);
+obj* l___private_init_lean_compiler_externattr_2__parseOptNum___main(obj*, obj*, obj*);
 obj* l_Lean_getExternEntryForAux___main___boxed(obj*, obj*);
 uint8 l_String_Iterator_hasNext___main(obj*);
 obj* l_Lean_getExternEntryForAux___main(obj*, obj*);
@@ -163,7 +169,102 @@ return x_3;
 }
 }
 }
-obj* l___private_init_lean_compiler_externattr_1__parseOptNum___main(obj* x_1, obj* x_2, obj* x_3) {
+obj* _init_l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__1() {
+_start:
+{
+obj* x_1; obj* x_2; obj* x_3; obj* x_4; obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; 
+x_1 = lean::box(0);
+x_2 = lean::box(0);
+x_3 = lean::mk_string("all");
+x_4 = lean_name_mk_string(x_2, x_3);
+x_5 = lean::alloc_cnstr(0, 1, 0);
+lean::cnstr_set(x_5, 0, x_4);
+x_6 = lean::box(0);
+x_7 = lean::alloc_cnstr(1, 2, 0);
+lean::cnstr_set(x_7, 0, x_5);
+lean::cnstr_set(x_7, 1, x_6);
+x_8 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_8, 0, x_1);
+lean::cnstr_set(x_8, 1, x_7);
+x_9 = lean::alloc_cnstr(1, 1, 0);
+lean::cnstr_set(x_9, 0, x_8);
+return x_9;
+}
+}
+obj* _init_l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__2() {
+_start:
+{
+obj* x_1; obj* x_2; obj* x_3; obj* x_4; 
+x_1 = lean::box(0);
+x_2 = lean::box(0);
+x_3 = lean::alloc_cnstr(0, 2, 0);
+lean::cnstr_set(x_3, 0, x_1);
+lean::cnstr_set(x_3, 1, x_2);
+x_4 = lean::alloc_cnstr(1, 1, 0);
+lean::cnstr_set(x_4, 0, x_3);
+return x_4;
+}
+}
+obj* _init_l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__3() {
+_start:
+{
+obj* x_1; obj* x_2; 
+x_1 = lean::mk_string("unexpected kind of argument");
+x_2 = lean::alloc_cnstr(0, 1, 0);
+lean::cnstr_set(x_2, 0, x_1);
+return x_2;
+}
+}
+obj* l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData(obj* x_1) {
+_start:
+{
+switch (lean::obj_tag(x_1)) {
+case 0:
+{
+obj* x_2; 
+x_2 = l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__1;
+return x_2;
+}
+case 1:
+{
+obj* x_3; obj* x_4; obj* x_5; uint8 x_6; 
+x_3 = lean::cnstr_get(x_1, 1);
+x_4 = lean::array_get_size(x_3);
+x_5 = lean::mk_nat_obj(0u);
+x_6 = lean::nat_dec_eq(x_4, x_5);
+lean::dec(x_4);
+if (x_6 == 0)
+{
+obj* x_7; 
+x_7 = l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__2;
+return x_7;
+}
+else
+{
+obj* x_8; 
+x_8 = l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__3;
+return x_8;
+}
+}
+default: 
+{
+obj* x_9; 
+x_9 = l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__3;
+return x_9;
+}
+}
+}
+}
+obj* l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___boxed(obj* x_1) {
+_start:
+{
+obj* x_2; 
+x_2 = l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData(x_1);
+lean::dec(x_1);
+return x_2;
+}
+}
+obj* l___private_init_lean_compiler_externattr_2__parseOptNum___main(obj* x_1, obj* x_2, obj* x_3) {
 _start:
 {
 obj* x_4; uint8 x_5; 
@@ -247,11 +348,11 @@ return x_25;
 }
 }
 }
-obj* l___private_init_lean_compiler_externattr_1__parseOptNum(obj* x_1, obj* x_2, obj* x_3) {
+obj* l___private_init_lean_compiler_externattr_2__parseOptNum(obj* x_1, obj* x_2, obj* x_3) {
 _start:
 {
 obj* x_4; 
-x_4 = l___private_init_lean_compiler_externattr_1__parseOptNum___main(x_1, x_2, x_3);
+x_4 = l___private_init_lean_compiler_externattr_2__parseOptNum___main(x_1, x_2, x_3);
 return x_4;
 }
 }
@@ -295,7 +396,7 @@ else
 obj* x_16; obj* x_17; obj* x_18; obj* x_19; obj* x_20; obj* x_21; obj* x_22; 
 x_16 = l_String_Iterator_next___main(x_3);
 x_17 = l_String_Iterator_remainingBytes___main(x_16);
-x_18 = l___private_init_lean_compiler_externattr_1__parseOptNum___main(x_17, x_16, x_5);
+x_18 = l___private_init_lean_compiler_externattr_2__parseOptNum___main(x_17, x_16, x_5);
 x_19 = lean::cnstr_get(x_18, 0);
 lean::inc(x_19);
 x_20 = lean::cnstr_get(x_18, 1);
@@ -892,6 +993,12 @@ REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("Lean"), "mkInlin
 REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("Lean"), "mkStdExtEntry"), 2, lean::mk_std_ext_entry_core);
 REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("Lean"), "mkForeignExtEntry"), 2, lean::mk_foreign_ext_entry_core);
 REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("Lean"), "mkExternAttrData"), 2, lean::mk_extern_attr_data_core);
+l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__1 = _init_l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__1();
+lean::mark_persistent(l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__1);
+l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__2 = _init_l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__2();
+lean::mark_persistent(l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__2);
+l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__3 = _init_l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__3();
+lean::mark_persistent(l___private_init_lean_compiler_externattr_1__syntaxToExternAttrData___closed__3);
 REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("Lean"), "expandExternPatternAux"), 4, l_Lean_expandExternPatternAux___boxed);
 REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("Lean"), "expandExternPattern"), 2, lean::expand_extern_pattern_core);
 REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name("Lean"), "mkSimpleFnCall"), 2, l_Lean_mkSimpleFnCall);

src/stage0/init/lean/parser/parser.cpp

@@ -70,7 +70,6 @@ obj* l_Lean_Parser_commandParser___elambda__1(obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_regBuiltinCommandParserAttr___closed__1;
 obj* l_Lean_Parser_anyOfFn___boxed(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_longestMatchMkResult(obj*, obj*);
-obj* l_Array_mkArray(obj*, obj*, obj*);
 obj* l_Lean_Parser_andthenFn___rarg(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_ParserState_hasError___boxed(obj*);
 obj* l_Lean_Parser_symbolInfo(obj*, obj*);
@@ -121,6 +120,7 @@ obj* l___private_init_lean_parser_parser_4__tokenFnAux___main(obj*, obj*);
 obj* l_Lean_Parser_rawFn___main___rarg(obj*, uint8, obj*, obj*, obj*);
 obj* l_Lean_Parser_regBuiltinTestParserAttr___closed__2;
 obj* l_Lean_Parser_Parser_inhabited(uint8);
+extern obj* l_Lean_numLitKind;
 obj* l_Lean_Parser_unicodeSymbolFn(uint8);
 obj* l_Lean_Parser_registerBuiltinParserAttribute___lambda__1___closed__4;
 uint8 l_Lean_Parser_TokenConfig_beq___main(obj*, obj*);
@@ -206,7 +206,6 @@ obj* l_Lean_Parser_TokenMap_Inhabited(obj*);
 obj* l_Nat_repr(obj*);
 obj* l_Lean_Parser_mkNodeToken(obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_node(uint8, obj*, obj*);
-obj* l_Lean_Parser_numLitKind;
 obj* l_Lean_Parser_rawFn___main(uint8);
 obj* l_Lean_Parser_andthen___boxed(obj*, obj*, obj*);
 obj* l_Lean_Parser_nodeFn___main___boxed(obj*);
@@ -333,6 +332,7 @@ uint8 l_RBNode_isRed___main___rarg(obj*);
 obj* l_Lean_Parser_satisfyFn___main___boxed(obj*, obj*, obj*, obj*);
 obj* l_Lean_Parser_pushLeadingFn(obj*, obj*, obj*);
 obj* l_List_foldl___main___at_Lean_Parser_addBuiltinLeadingParser___spec__1(obj*, obj*, obj*);
+extern obj* l_Lean_strLitKind;
 obj* l_Lean_Parser_ident___closed__1;
 obj* l_Lean_Parser_addBuiltinLeadingParser___closed__2;
 obj* l_Lean_Parser_Parser_inhabited___lambda__1___boxed(obj*, obj*, obj*);
@@ -528,6 +528,7 @@ obj* l_Lean_Parser_registerBuiltinParserAttribute___lambda__1___closed__1;
 obj* l_Lean_Parser_hexDigitFn(obj*, obj*);
 obj* l_Lean_Parser_takeWhileFn___boxed(obj*, obj*, obj*);
 obj* l_Lean_Parser_insertToken(obj*, obj*, obj*);
+obj* l_Lean_mkLit(obj*, obj*, obj*);
 obj* l_Lean_Parser_trailingParser___boxed(obj*, obj*, obj*, obj*, obj*);
 obj* l_Lean_Name_append___main(obj*, obj*);
 uint8 l_Lean_isIdFirst(uint32);
@@ -544,7 +545,6 @@ obj* l_Lean_Parser_numLitFn(uint8, obj*);
 obj* l_Lean_FileMap_ofString(obj*);
 obj* l_Lean_Parser_isIdCont___main___boxed(obj*, obj*);
 obj* l_Lean_Parser_regBuiltinTestParserAttr___closed__1;
-obj* l_Lean_Parser_strLitKind;
 obj* l_Lean_Parser_sepByFn___main___boxed(obj*, obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_IO_Prim_Ref_reset(obj*, obj*, obj*);
 obj* l___private_init_lean_parser_parser_2__rawAux___main___boxed(obj*);
@@ -4419,30 +4419,10 @@ lean::dec(x_1);
 return x_3;
 }
 }
-obj* _init_l_Lean_Parser_strLitKind() {
-_start:
-{
-obj* x_1; obj* x_2; obj* x_3; 
-x_1 = lean::box(0);
-x_2 = lean::mk_string("strLit");
-x_3 = lean_name_mk_string(x_1, x_2);
-return x_3;
-}
-}
-obj* _init_l_Lean_Parser_numLitKind() {
-_start:
-{
-obj* x_1; obj* x_2; obj* x_3; 
-x_1 = lean::box(0);
-x_2 = lean::mk_string("numLit");
-x_3 = lean_name_mk_string(x_1, x_2);
-return x_3;
-}
-}
 obj* l_Lean_Parser_mkNodeToken(obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
 _start:
 {
-obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_15; obj* x_16; obj* x_17; obj* x_18; obj* x_19; 
+obj* x_5; obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_15; 
 x_5 = lean::cnstr_get(x_3, 1);
 x_6 = lean::cnstr_get(x_4, 1);
 lean::inc(x_6);
@@ -4467,18 +4447,9 @@ lean::cnstr_set(x_12, 1, x_2);
 lean::cnstr_set(x_12, 2, x_11);
 x_13 = lean::alloc_cnstr(1, 1, 0);
 lean::cnstr_set(x_13, 0, x_12);
-x_14 = lean::alloc_cnstr(2, 2, 0);
-lean::cnstr_set(x_14, 0, x_13);
-lean::cnstr_set(x_14, 1, x_8);
-x_15 = lean::mk_nat_obj(1u);
-x_16 = lean::mk_array(x_15, x_14);
-x_17 = lean::box(0);
-x_18 = lean::alloc_cnstr(1, 3, 0);
-lean::cnstr_set(x_18, 0, x_1);
-lean::cnstr_set(x_18, 1, x_16);
-lean::cnstr_set(x_18, 2, x_17);
-x_19 = l_Lean_Parser_ParserState_pushSyntax(x_9, x_18);
-return x_19;
+x_14 = l_Lean_mkLit(x_1, x_8, x_13);
+x_15 = l_Lean_Parser_ParserState_pushSyntax(x_9, x_14);
+return x_15;
 }
 }
 obj* l_Lean_Parser_mkNodeToken___boxed(obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
@@ -4539,7 +4510,7 @@ return x_15;
 else
 {
 obj* x_18; obj* x_19; 
-x_18 = l_Lean_Parser_strLitKind;
+x_18 = l_Lean_strLitKind;
 x_19 = l_Lean_Parser_mkNodeToken(x_18, x_1, x_2, x_9);
 return x_19;
 }
@@ -4638,7 +4609,7 @@ if (x_9 == 0)
 {
 obj* x_10; obj* x_11; 
 lean::dec(x_6);
-x_10 = l_Lean_Parser_numLitKind;
+x_10 = l_Lean_numLitKind;
 x_11 = l_Lean_Parser_mkNodeToken(x_10, x_1, x_2, x_4);
 return x_11;
 }
@@ -4653,7 +4624,7 @@ if (x_14 == 0)
 {
 obj* x_15; obj* x_16; 
 lean::dec(x_12);
-x_15 = l_Lean_Parser_numLitKind;
+x_15 = l_Lean_numLitKind;
 x_16 = l_Lean_Parser_mkNodeToken(x_15, x_1, x_2, x_4);
 return x_16;
 }
@@ -4662,7 +4633,7 @@ else
 obj* x_17; obj* x_18; obj* x_19; obj* x_20; 
 x_17 = l_Lean_Parser_ParserState_setPos(x_4, x_12);
 x_18 = l_Lean_Parser_takeUntilFn___main___at_Lean_Parser_decimalNumberFn___spec__2(x_2, x_17);
-x_19 = l_Lean_Parser_numLitKind;
+x_19 = l_Lean_numLitKind;
 x_20 = l_Lean_Parser_mkNodeToken(x_19, x_1, x_2, x_18);
 return x_20;
 }
@@ -4828,7 +4799,7 @@ if (lean::obj_tag(x_6) == 0)
 {
 obj* x_7; obj* x_8; obj* x_9; 
 x_7 = l_Lean_Parser_takeUntilFn___main___at_Lean_Parser_binNumberFn___spec__3(x_2, x_5);
-x_8 = l_Lean_Parser_numLitKind;
+x_8 = l_Lean_numLitKind;
 x_9 = l_Lean_Parser_mkNodeToken(x_8, x_1, x_2, x_7);
 return x_9;
 }
@@ -4836,7 +4807,7 @@ else
 {
 obj* x_10; obj* x_11; 
 lean::dec(x_6);
-x_10 = l_Lean_Parser_numLitKind;
+x_10 = l_Lean_numLitKind;
 x_11 = l_Lean_Parser_mkNodeToken(x_10, x_1, x_2, x_5);
 return x_11;
 }
@@ -5006,7 +4977,7 @@ if (lean::obj_tag(x_6) == 0)
 {
 obj* x_7; obj* x_8; obj* x_9; 
 x_7 = l_Lean_Parser_takeUntilFn___main___at_Lean_Parser_octalNumberFn___spec__3(x_2, x_5);
-x_8 = l_Lean_Parser_numLitKind;
+x_8 = l_Lean_numLitKind;
 x_9 = l_Lean_Parser_mkNodeToken(x_8, x_1, x_2, x_7);
 return x_9;
 }
@@ -5014,7 +4985,7 @@ else
 {
 obj* x_10; obj* x_11; 
 lean::dec(x_6);
-x_10 = l_Lean_Parser_numLitKind;
+x_10 = l_Lean_numLitKind;
 x_11 = l_Lean_Parser_mkNodeToken(x_10, x_1, x_2, x_5);
 return x_11;
 }
@@ -5374,7 +5345,7 @@ if (lean::obj_tag(x_6) == 0)
 {
 obj* x_7; obj* x_8; obj* x_9; 
 x_7 = l_Lean_Parser_takeUntilFn___main___at_Lean_Parser_hexNumberFn___spec__3(x_2, x_5);
-x_8 = l_Lean_Parser_numLitKind;
+x_8 = l_Lean_numLitKind;
 x_9 = l_Lean_Parser_mkNodeToken(x_8, x_1, x_2, x_7);
 return x_9;
 }
@@ -5382,7 +5353,7 @@ else
 {
 obj* x_10; obj* x_11; 
 lean::dec(x_6);
-x_10 = l_Lean_Parser_numLitKind;
+x_10 = l_Lean_numLitKind;
 x_11 = l_Lean_Parser_mkNodeToken(x_10, x_1, x_2, x_5);
 return x_11;
 }
@@ -7074,7 +7045,7 @@ x_5 = lean::cnstr_get(x_3, 0);
 lean::inc(x_5);
 x_6 = l_Array_back___at___private_init_lean_parser_parser_5__updateCache___spec__1(x_5);
 lean::dec(x_5);
-x_7 = l_Lean_Parser_numLitKind;
+x_7 = l_Lean_numLitKind;
 x_8 = l_Lean_Syntax_isOfKind___main(x_6, x_7);
 lean::dec(x_6);
 if (x_8 == 0)
@@ -7173,7 +7144,7 @@ x_5 = lean::cnstr_get(x_3, 0);
 lean::inc(x_5);
 x_6 = l_Array_back___at___private_init_lean_parser_parser_5__updateCache___spec__1(x_5);
 lean::dec(x_5);
-x_7 = l_Lean_Parser_strLitKind;
+x_7 = l_Lean_strLitKind;
 x_8 = l_Lean_Syntax_isOfKind___main(x_6, x_7);
 lean::dec(x_6);
 if (x_8 == 0)
@@ -18295,12 +18266,12 @@ lean::dec(x_19);
 x_20 = lean::cnstr_get(x_11, 0);
 lean::inc(x_20);
 lean::dec(x_11);
-x_21 = l_Lean_Parser_numLitKind;
+x_21 = l_Lean_numLitKind;
 x_22 = lean_name_dec_eq(x_20, x_21);
 if (x_22 == 0)
 {
 obj* x_23; uint8 x_24; 
-x_23 = l_Lean_Parser_strLitKind;
+x_23 = l_Lean_strLitKind;
 x_24 = lean_name_dec_eq(x_20, x_23);
 lean::dec(x_20);
 if (x_24 == 0)
@@ -18336,12 +18307,12 @@ lean::dec(x_3);
 x_29 = lean::cnstr_get(x_11, 0);
 lean::inc(x_29);
 lean::dec(x_11);
-x_30 = l_Lean_Parser_numLitKind;
+x_30 = l_Lean_numLitKind;
 x_31 = lean_name_dec_eq(x_29, x_30);
 if (x_31 == 0)
 {
 obj* x_32; uint8 x_33; 
-x_32 = l_Lean_Parser_strLitKind;
+x_32 = l_Lean_strLitKind;
 x_33 = lean_name_dec_eq(x_29, x_32);
 lean::dec(x_29);
 if (x_33 == 0)
@@ -22036,12 +22007,6 @@ REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name(lean::mk_const_na
 l_Lean_Parser_quotedCharFn___main___closed__1 = _init_l_Lean_Parser_quotedCharFn___main___closed__1();
 lean::mark_persistent(l_Lean_Parser_quotedCharFn___main___closed__1);
 REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "Parser"), "quotedCharFn"), 2, l_Lean_Parser_quotedCharFn___boxed);
-l_Lean_Parser_strLitKind = _init_l_Lean_Parser_strLitKind();
-lean::mark_persistent(l_Lean_Parser_strLitKind);
-lean::register_constant(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "Parser"), "strLitKind"), l_Lean_Parser_strLitKind);
-l_Lean_Parser_numLitKind = _init_l_Lean_Parser_numLitKind();
-lean::mark_persistent(l_Lean_Parser_numLitKind);
-lean::register_constant(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "Parser"), "numLitKind"), l_Lean_Parser_numLitKind);
 REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "Parser"), "mkNodeToken"), 4, l_Lean_Parser_mkNodeToken___boxed);
 REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "Parser"), "strLitFnAux"), 3, l_Lean_Parser_strLitFnAux___boxed);
 REGISTER_LEAN_FUNCTION(lean::mk_const_name(lean::mk_const_name(lean::mk_const_name("Lean"), "Parser"), "decimalNumberFn"), 3, l_Lean_Parser_decimalNumberFn___boxed);