max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-14 14:16:21 -08:00
parent ab8cbdc7e0
commit 2e668d9052
8 changed files with 2485 additions and 1265 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
stage0/src/Init/Lean/Elab/Command.lean
View file

@ -578,6 +578,11 @@ fun stx => do
env ← liftIO stx $ Parser.registerParserCategory env attrName catName;
setEnv env
@[builtinCommandElab syntax] def elabSyntax : CommandElab :=
fun stx =>
throwError stx ("not implemented yet " ++ toString stx)
@[inline] def withDeclId (declId : Syntax) (f : Name → CommandElabM Unit) : CommandElabM Unit := do
-- ident >> optional (".{" >> sepBy1 ident ", " >> "}")
let id := declId.getIdAt 0;

7
stage0/src/Init/Lean/Parser/Parser.lean
View file

@ -1513,10 +1513,13 @@ def compileParserDescr (categories : ParserCategories) : forall {k : ParserKind}
| _, 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.symbol tk lbp => pure $ symbolAux tk lbp
| _, ParserDescr.num => pure $ numLit
| _, ParserDescr.str => pure $ strLit
| _, ParserDescr.char => pure $ charLit
| _, ParserDescr.ident => pure $ identNoAntiquot -- Kha, do we need `ident` here?
| ParserKind.leading,
ParserDescr.nonReservedSymbol tk includeIdent => pure $ nonReservedSymbol tk includeIdent
| _, 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

8
stage0/src/Init/Lean/Parser/Syntax.lean
View file

@ -22,18 +22,20 @@ categoryParser `syntax rbp
namespace Syntax
@[builtinSyntaxParser] def paren := parser! "(" >> many1 syntaxParser >> ")"
@[builtinSyntaxParser] def cat := parser! ident
@[builtinSyntaxParser] def atom := parser! strLit
@[builtinSyntaxParser] def cat := parser! ident >> optional (":" >> numLit)
@[builtinSyntaxParser] def atom := parser! strLit >> optional (":" >> numLit)
@[builtinSyntaxParser] def num := parser! nonReservedSymbol "num"
@[builtinSyntaxParser] def str := parser! nonReservedSymbol "str"
@[builtinSyntaxParser] def char := parser! nonReservedSymbol "char"
@[builtinSyntaxParser] def ident := parser! nonReservedSymbol "ident"
@[builtinSyntaxParser] def try := parser! nonReservedSymbol "try " >> syntaxParser
@[builtinSyntaxParser] def lookahead := parser! nonReservedSymbol "lookahead " >> syntaxParser
@[builtinSyntaxParser] def optional := parser! nonReservedSymbol "optional " >> syntaxParser
@[builtinSyntaxParser] def sepBy := parser! nonReservedSymbol "sepBy " >> syntaxParser >> syntaxParser
@[builtinSyntaxParser] def sepBy1 := parser! nonReservedSymbol "sepBy1 " >> syntaxParser >> syntaxParser
@[builtinSyntaxParser] def many := tparser! pushLeading >> symbolAux "*" none
@[builtinSyntaxParser] def many1 := tparser! pushLeading >> symbolAux "+" none
@[builtinSyntaxParser] def optional := tparser! pushLeading >> symbolAux "?" none
@[builtinSyntaxParser] def orelse := tparser! infixR " <|> " 2
end Syntax

14
stage0/src/Init/LeanExt.lean
View file

@ -40,13 +40,16 @@ inductive ParserDescrCore : ParserKind → Type
| sepBy {k : ParserKind} : ParserDescrCore k → ParserDescrCore k → ParserDescrCore k
| sepBy1 {k : ParserKind} : ParserDescrCore k → ParserDescrCore k → ParserDescrCore k
| node {k : ParserKind} : Name → ParserDescrCore k → ParserDescrCore k
| symbol {k : ParserKind} : String → Nat → ParserDescrCore k
| unicodeSymbol {k : ParserKind} : String → String → Nat → ParserDescrCore k
| symbol {k : ParserKind} : String → Option Nat → ParserDescrCore k
| nonReservedSymbol : String → Bool → ParserDescrCore ParserKind.leading
| num {k : ParserKind} : ParserDescrCore k
| str {k : ParserKind} : ParserDescrCore k
| char {k : ParserKind} : ParserDescrCore k
| ident {k : ParserKind} : ParserDescrCore k
| pushLeading : ParserDescrCore ParserKind.trailing
| parser : Name → Nat → ParserDescrCore ParserKind.leading
instance ParserDescrCore.inhabited {k} : Inhabited (ParserDescrCore k) := ⟨ParserDescrCore.symbol "" 0⟩
instance ParserDescrCore.inhabited {k} : Inhabited (ParserDescrCore k) := ⟨ParserDescrCore.symbol "" none⟩
abbrev ParserDescr := ParserDescrCore ParserKind.leading
abbrev TrailingParserDescr := ParserDescrCore ParserKind.trailing
@ -62,8 +65,11 @@ abbrev TrailingParserDescr := ParserDescrCore ParserKind.trailing
@[matchPattern] abbrev ParserDescr.sepBy1 := @ParserDescrCore.sepBy1
@[matchPattern] abbrev ParserDescr.node := @ParserDescrCore.node
@[matchPattern] abbrev ParserDescr.symbol := @ParserDescrCore.symbol
@[matchPattern] abbrev ParserDescr.num := @ParserDescrCore.num
@[matchPattern] abbrev ParserDescr.str := @ParserDescrCore.str
@[matchPattern] abbrev ParserDescr.char := @ParserDescrCore.char
@[matchPattern] abbrev ParserDescr.ident := @ParserDescrCore.ident
@[matchPattern] abbrev ParserDescr.nonReservedSymbol := @ParserDescrCore.nonReservedSymbol
@[matchPattern] abbrev ParserDescr.unicodeSymbol := @ParserDescrCore.unicodeSymbol
@[matchPattern] abbrev ParserDescr.pushLeading := @ParserDescrCore.pushLeading
@[matchPattern] abbrev ParserDescr.parser := @ParserDescrCore.parser

111
stage0/stdlib/Init/Lean/Elab/Command.c
View file

@ -21,6 +21,7 @@ extern lean_object* l_Lean_Name_toString___closed__1;
lean_object* l_Lean_Elab_Command_registerBuiltinCommandElabAttr___closed__4;
lean_object* l_Lean_Elab_Command_elabSection(lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabNamespace(lean_object*);
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__2;
lean_object* l_Lean_extractMacroScopes(lean_object*);
lean_object* l_PersistentHashMap_contains___at_Lean_Elab_Command_addBuiltinCommandElab___spec__4___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_commandElabAttribute___closed__3;
@ -161,6 +162,7 @@ extern lean_object* l_Lean_Meta_MetaHasEval___rarg___closed__4;
extern lean_object* l_Lean_Parser_Command_mixfix___elambda__1___closed__2;
lean_object* l_Lean_Name_getNumParts___main(lean_object*);
lean_object* l_Lean_Elab_Command_elabOpen(lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__1;
lean_object* l_Lean_Elab_mkMessageAt___at_Lean_Elab_Command_throwError___spec__3(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabSetOption___closed__3;
extern lean_object* l_Lean_LocalContext_Inhabited___closed__1;
@ -326,6 +328,7 @@ extern lean_object* l_Lean_Parser_declareBuiltinParser___closed__7;
lean_object* l_Lean_Elab_Command_elabOpenOnly(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Options_empty;
extern lean_object* l_Lean_Parser_Command_variable___elambda__1___closed__2;
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__3;
lean_object* l_ReaderT_read___at_Lean_Elab_Command_CommandElabM_monadLog___spec__1(lean_object*, lean_object*);
uint8_t l_coeDecidableEq(uint8_t);
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabExport___closed__1;
@ -343,6 +346,7 @@ lean_object* l_PersistentHashMap_containsAux___main___at_Lean_Elab_Command_addBu
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabVariable___closed__2;
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_elabSyntax___closed__3;
lean_object* l_Lean_Elab_Command_CommandElabM_MonadQuotation___closed__1;
lean_object* l_Lean_Elab_mkElabAttribute___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabEnd___closed__2;
@ -359,6 +363,7 @@ lean_object* l_PersistentHashMap_empty___at_Lean_Elab_Command_mkBuiltinCommandEl
lean_object* l_mkHashMapImp___rarg(lean_object*);
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabOpen(lean_object*);
lean_object* l_Lean_Elab_Command_elabEnd(lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax(lean_object*);
lean_object* l_Array_iterateMAux___main___at_Array_append___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_modifyScope___closed__1;
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabCheck(lean_object*);
@ -447,6 +452,7 @@ lean_object* l_Array_iterateMAux___main___at_Lean_Elab_Command_withDeclId___spec
lean_object* l_Lean_Elab_Command_CommandElabM_monadLog___closed__5;
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabUniverse___closed__2;
lean_object* l___private_Init_Lean_Elab_Command_14__addScopes___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabSyntax___closed__1;
lean_object* l_Lean_Elab_Command_withIncRecDepth(lean_object*);
lean_object* lean_panic_fn(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_registerBuiltinCommandElabAttr___closed__3;
@ -460,6 +466,7 @@ lean_object* l_Lean_Syntax_foldArgsAuxM___main___at_Lean_Elab_Command_elabOpenSi
lean_object* l_Lean_Syntax_getOptionalIdent_x3f(lean_object*);
lean_object* l_Array_filterAux___main___at_Lean_Elab_Command_sortDeclLevelParams___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_mkCommandElabAttribute___closed__2;
lean_object* l_Lean_Elab_Command_elabSyntax___closed__2;
lean_object* l_Lean_Elab_Command_elabNamespace(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabReserve___rarg(lean_object*);
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabMixfix(lean_object*);
@ -474,6 +481,7 @@ lean_object* l_Lean_Elab_Command_logUnknownDecl___closed__1;
lean_object* l_Lean_Syntax_getPos(lean_object*);
lean_object* l_Lean_Elab_Command_State_inhabited;
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabMixfix___closed__2;
lean_object* l_Lean_Elab_Command_elabSyntax(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabOpenHiding___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_getOpenDecls(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_throwAlreadyDeclaredUniverseLevel___rarg___closed__4;
@ -576,6 +584,7 @@ lean_object* l_List_foldlM___main___at___private_Init_Lean_Elab_Command_7__addMa
lean_object* l_Lean_Elab_Command_mkMessageAux(lean_object*, lean_object*, lean_object*, uint8_t);
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Command_10__mkTermState___boxed(lean_object*);
extern lean_object* l_Lean_Parser_Command_syntax___elambda__1___closed__1;
lean_object* l_Lean_Elab_Command_commandElabAttribute___closed__5;
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabNamespace___closed__1;
lean_object* l_Lean_Elab_Command_CommandElabM_MonadQuotation___closed__3;
@ -18813,6 +18822,93 @@ x_5 = l_Lean_Elab_Command_addBuiltinCommandElab(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* _init_l_Lean_Elab_Command_elabSyntax___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("not implemented yet ");
return x_1;
}
}
lean_object* _init_l_Lean_Elab_Command_elabSyntax___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Command_elabSyntax___closed__1;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Elab_Command_elabSyntax___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Elab_Command_elabSyntax___closed__2;
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* l_Lean_Elab_Command_elabSyntax(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; 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;
x_4 = lean_box(0);
x_5 = lean_unsigned_to_nat(0u);
lean_inc(x_1);
x_6 = l_Lean_Syntax_formatStxAux___main(x_4, x_5, x_1);
x_7 = l_Lean_Options_empty;
x_8 = l_Lean_Format_pretty(x_6, x_7);
x_9 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_9, 0, x_8);
x_10 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_10, 0, x_9);
x_11 = l_Lean_Elab_Command_elabSyntax___closed__3;
x_12 = lean_alloc_ctor(8, 2, 0);
lean_ctor_set(x_12, 0, x_11);
lean_ctor_set(x_12, 1, x_10);
x_13 = l_Lean_Elab_Command_throwError___rarg(x_1, x_12, x_2, x_3);
return x_13;
}
}
lean_object* _init_l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("elabSyntax");
return x_1;
}
}
lean_object* _init_l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Elab_Command_declareBuiltinCommandElab___closed__3;
x_2 = l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Command_elabSyntax), 3, 0);
return x_1;
}
}
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_2 = l_Lean_Parser_Command_syntax___elambda__1___closed__1;
x_3 = l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__2;
x_4 = l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__3;
x_5 = l_Lean_Elab_Command_addBuiltinCommandElab(x_2, x_3, x_4, x_1);
return x_5;
}
}
lean_object* l_Lean_Elab_Command_modifyScope___at_Lean_Elab_Command_withDeclId___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -22614,6 +22710,21 @@ lean_mark_persistent(l___regBuiltinCommandElab_Lean_Elab_Command_elabDeclareSynt
res = l___regBuiltinCommandElab_Lean_Elab_Command_elabDeclareSyntaxCat(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Elab_Command_elabSyntax___closed__1 = _init_l_Lean_Elab_Command_elabSyntax___closed__1();
lean_mark_persistent(l_Lean_Elab_Command_elabSyntax___closed__1);
l_Lean_Elab_Command_elabSyntax___closed__2 = _init_l_Lean_Elab_Command_elabSyntax___closed__2();
lean_mark_persistent(l_Lean_Elab_Command_elabSyntax___closed__2);
l_Lean_Elab_Command_elabSyntax___closed__3 = _init_l_Lean_Elab_Command_elabSyntax___closed__3();
lean_mark_persistent(l_Lean_Elab_Command_elabSyntax___closed__3);
l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__1 = _init_l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__1();
lean_mark_persistent(l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__1);
l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__2 = _init_l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__2();
lean_mark_persistent(l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__2);
l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__3 = _init_l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__3();
lean_mark_persistent(l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax___closed__3);
res = l___regBuiltinCommandElab_Lean_Elab_Command_elabSyntax(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Elab_Command_withDeclId___closed__1 = _init_l_Lean_Elab_Command_withDeclId___closed__1();
lean_mark_persistent(l_Lean_Elab_Command_withDeclId___closed__1);
l_Lean_Elab_Command_withDeclId___closed__2 = _init_l_Lean_Elab_Command_withDeclId___closed__2();

1966
stage0/stdlib/Init/Lean/Parser/Parser.c
View file

File diff suppressed because it is too large Load diff

1517
stage0/stdlib/Init/Lean/Parser/Syntax.c
View file

File diff suppressed because it is too large Load diff

122
stage0/stdlib/Init/LeanExt.c
View file

@ -18,13 +18,16 @@ lean_object* l_Lean_ParserDescr_orelse(uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_optional(uint8_t, lean_object*);
lean_object* l_Lean_ParserDescr_lookahead(uint8_t, lean_object*);
lean_object* l_Lean_ParserDescr_many(uint8_t, lean_object*);
lean_object* l_Lean_ParserDescr_ident(uint8_t);
lean_object* l_Lean_ParserDescr_andthen___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_char(uint8_t);
extern lean_object* l_String_splitAux___main___closed__1;
lean_object* l_Lean_ParserDescr_try(uint8_t, lean_object*);
lean_object* l_Lean_ParserDescr_unicodeSymbol(uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_str(uint8_t);
lean_object* l_Lean_ParserDescrCore_inhabited(uint8_t);
lean_object* l_Lean_ParserDescr_many1(uint8_t, lean_object*);
lean_object* l_Lean_ParserDescr_many___boxed(lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_num___boxed(lean_object*);
lean_object* l_Lean_ParserDescr_many1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_parser(lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_lookahead___boxed(lean_object*, lean_object*);
@ -33,13 +36,16 @@ lean_object* l_Lean_ParserDescr_andthen(uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_symbol___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_node(uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_try___boxed(lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_ident___boxed(lean_object*);
lean_object* l_Lean_ParserDescr_str___boxed(lean_object*);
lean_object* l_Lean_ParserDescr_node___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_nonReservedSymbol___boxed(lean_object*, lean_object*);
lean_object* l_Lean_ParserDescrCore_inhabited___boxed(lean_object*);
lean_object* l_Lean_ParserDescr_sepBy1(uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_unicodeSymbol___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_char___boxed(lean_object*);
lean_object* l_Lean_ParserDescr_orelse___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_sepBy___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_num(uint8_t);
lean_object* l_Lean_ParserDescr_symbol(uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_optional___boxed(lean_object*, lean_object*);
lean_object* l_Lean_ParserDescr_nonReservedSymbol(lean_object*, uint8_t);
@ -48,11 +54,11 @@ lean_object* l_Lean_ParserDescrCore_inhabited(uint8_t x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = l_String_splitAux___main___closed__1;
x_3 = lean_unsigned_to_nat(0u);
x_2 = lean_box(0);
x_3 = l_String_splitAux___main___closed__1;
x_4 = lean_alloc_ctor(10, 2, 1);
lean_ctor_set(x_4, 0, x_2);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set(x_4, 0, x_3);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set_uint8(x_4, sizeof(void*)*2, x_1);
return x_4;
}
@ -293,11 +299,87 @@ x_5 = l_Lean_ParserDescr_symbol(x_4, x_2, x_3);
return x_5;
}
}
lean_object* l_Lean_ParserDescr_num(uint8_t x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_ctor(12, 0, 1);
lean_ctor_set_uint8(x_2, 0, x_1);
return x_2;
}
}
lean_object* l_Lean_ParserDescr_num___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = lean_unbox(x_1);
lean_dec(x_1);
x_3 = l_Lean_ParserDescr_num(x_2);
return x_3;
}
}
lean_object* l_Lean_ParserDescr_str(uint8_t x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_ctor(13, 0, 1);
lean_ctor_set_uint8(x_2, 0, x_1);
return x_2;
}
}
lean_object* l_Lean_ParserDescr_str___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = lean_unbox(x_1);
lean_dec(x_1);
x_3 = l_Lean_ParserDescr_str(x_2);
return x_3;
}
}
lean_object* l_Lean_ParserDescr_char(uint8_t x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_ctor(14, 0, 1);
lean_ctor_set_uint8(x_2, 0, x_1);
return x_2;
}
}
lean_object* l_Lean_ParserDescr_char___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = lean_unbox(x_1);
lean_dec(x_1);
x_3 = l_Lean_ParserDescr_char(x_2);
return x_3;
}
}
lean_object* l_Lean_ParserDescr_ident(uint8_t x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_ctor(15, 0, 1);
lean_ctor_set_uint8(x_2, 0, x_1);
return x_2;
}
}
lean_object* l_Lean_ParserDescr_ident___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; lean_object* x_3;
x_2 = lean_unbox(x_1);
lean_dec(x_1);
x_3 = l_Lean_ParserDescr_ident(x_2);
return x_3;
}
}
lean_object* l_Lean_ParserDescr_nonReservedSymbol(lean_object* x_1, uint8_t x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_ctor(12, 1, 1);
x_3 = lean_alloc_ctor(11, 1, 1);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set_uint8(x_3, sizeof(void*)*1, x_2);
return x_3;
@ -313,33 +395,11 @@ x_4 = l_Lean_ParserDescr_nonReservedSymbol(x_1, x_3);
return x_4;
}
}
lean_object* l_Lean_ParserDescr_unicodeSymbol(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = lean_alloc_ctor(11, 3, 1);
lean_ctor_set(x_5, 0, x_2);
lean_ctor_set(x_5, 1, x_3);
lean_ctor_set(x_5, 2, x_4);
lean_ctor_set_uint8(x_5, sizeof(void*)*3, x_1);
return x_5;
}
}
lean_object* l_Lean_ParserDescr_unicodeSymbol___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
uint8_t x_5; lean_object* x_6;
x_5 = lean_unbox(x_1);
lean_dec(x_1);
x_6 = l_Lean_ParserDescr_unicodeSymbol(x_5, x_2, x_3, x_4);
return x_6;
}
}
lean_object* _init_l_Lean_ParserDescr_pushLeading() {
_start:
{
lean_object* x_1;
x_1 = lean_box(13);
x_1 = lean_box(16);
return x_1;
}
}
@ -347,7 +407,7 @@ lean_object* l_Lean_ParserDescr_parser(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_ctor(14, 2, 0);
x_3 = lean_alloc_ctor(17, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;