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:
Sebastian Ullrich 2020-12-14 13:55:01 +01:00
parent 0316c872b9
commit 7dc08328bb
11 changed files with 3416 additions and 3230 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
stage0/src/Lean/Elab/Syntax.lean generated
View file

@ -177,6 +177,7 @@ end Term
namespace Command
open Lean.Syntax
open Lean.Parser.Command
private def getCatSuffix (catName : Name) : String :=
match catName with
@ -506,15 +507,23 @@ def expandMacroArgIntoSyntaxItem (stx : Syntax) : MacroM Syntax :=
Macro.throwUnsupported
/- Convert `macro` arg into a pattern element -/
def expandMacroArgIntoPattern (stx : Syntax) : MacroM Syntax :=
let k := stx.getKind
if k == `Lean.Parser.Command.macroArgSimple then
let item := stx[0]
pure $ mkNode `antiquot #[mkAtom "$", mkNullNode, item, mkNullNode, mkNullNode]
else if k == strLitKind then
strLitToPattern stx
else
Macro.throwUnsupported
def expandMacroArgIntoPattern (stx : Syntax) : MacroM Syntax := do
match (← expandMacros stx) with
| `(macroArg|$id:ident:optional($stx)) =>
mkSplicePat `optional id "?"
| `(macroArg|$id:ident:many($stx)) =>
mkSplicePat `many id "*"
| `(macroArg|$id:ident:many1($stx)) =>
mkSplicePat `many id "*"
| `(macroArg|$id:ident:sepBy($stx, $sep:strLit $[, $stxsep]? $[, allowTrailingSep]?)) =>
mkSplicePat `sepBy id ((isStrLit? sep).get! ++ "*")
| `(macroArg|$id:ident:sepBy1($stx, $sep:strLit $[, $stxsep]? $[, allowTrailingSep]?)) =>
mkSplicePat `sepBy id ((isStrLit? sep).get! ++ "*")
| `(macroArg|$id:ident:$stx) => mkAntiquotNode id
| `(macroArg|$s:strLit) => strLitToPattern s
| _ => Macro.throwUnsupported
where mkSplicePat kind id suffix :=
mkNullNode #[mkAntiquotSuffixSpliceNode kind (mkAntiquotNode id) suffix]
def expandOptPrio (stx : Syntax) : Nat :=
if stx.isNone then

7
stage0/src/Lean/Syntax.lean generated
View file

@ -402,6 +402,10 @@ def getAntiquotSpliceSuffix (stx : Syntax) : Syntax :=
else
stx[1]
def mkAntiquotSpliceNode (kind : SyntaxNodeKind) (contents : Array Syntax) (suffix : String) (nesting := 0) : Syntax :=
let nesting := mkNullNode (mkArray nesting (mkAtom "$"))
mkNode (kind ++ `antiquot_splice) #[mkAtom "$", nesting, mkAtom "[", mkNullNode contents, mkAtom "]", mkAtom suffix]
-- `$x,*` etc.
def antiquotSuffixSplice? : Syntax → Option SyntaxNodeKind
| Syntax.node (Name.str k "antiquot_suffix_splice" _) args => some k
@ -414,5 +418,8 @@ def isAntiquotSuffixSplice (stx : Syntax) : Bool :=
def getAntiquotSuffixSpliceInner (stx : Syntax) : Syntax :=
stx[0]
def mkAntiquotSuffixSpliceNode (kind : SyntaxNodeKind) (inner : Syntax) (suffix : String) : Syntax :=
mkNode (kind ++ `antiquot_suffix_splice) #[inner, mkAtom suffix]
end Syntax
end Lean

2
stage0/stdlib/CMakeLists.txt generated
View file

File diff suppressed because one or more lines are too long

6
stage0/stdlib/Lean/Elab/MutualDef.c generated
View file

@ -348,7 +348,6 @@ uint8_t l_Array_anyMUnsafe_any___at_Lean_Elab_Term_MutualClosure_getModifiersFor
extern lean_object* l_Lean_instInhabitedExpr;
lean_object* l_Lean_Elab_checkNotAlreadyDeclared___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_elabHeaders___spec__4___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_reverse___rarg(lean_object*);
extern lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqNDRecImp___closed__6;
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_check___lambda__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_getAllUserLevelNames___boxed(lean_object*);
extern lean_object* l_Lean_KernelException_toMessageData___closed__15;
@ -396,6 +395,7 @@ lean_object* l_Lean_Elab_expandDeclIdCore(lean_object*);
lean_object* l_Array_anyMUnsafe_any___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_isExample___spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_MutualClosure_Replacement_apply_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_elabAttr___at_Lean_Elab_Command_elabMutualDef___spec__4___lambda__1(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Syntax_mkAntiquotSpliceNode___closed__5;
lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_MutualDef_0__Lean_Elab_Term_MutualClosure_mkInitialUsedFVarsMap___spec__1(lean_object*, size_t, size_t, lean_object*);
lean_object* l_Array_anyMUnsafe_any___at_Lean_Elab_Term_isAutoImplicit___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_MutualClosure_pushMain___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -5201,7 +5201,7 @@ lean_ctor_set(x_37, 0, x_36);
lean_ctor_set(x_37, 1, x_35);
x_38 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_261____closed__26;
x_39 = l_Lean_mkAtomFrom(x_1, x_38);
x_40 = l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqNDRecImp___closed__6;
x_40 = l_Lean_Syntax_mkAntiquotSpliceNode___closed__5;
x_41 = lean_array_push(x_40, x_29);
x_42 = lean_array_push(x_41, x_33);
x_43 = lean_array_push(x_42, x_37);
@ -5238,7 +5238,7 @@ lean_ctor_set(x_60, 0, x_59);
lean_ctor_set(x_60, 1, x_58);
x_61 = l_Std_Range_myMacro____x40_Init_Data_Range___hyg_261____closed__26;
x_62 = l_Lean_mkAtomFrom(x_1, x_61);
x_63 = l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqNDRecImp___closed__6;
x_63 = l_Lean_Syntax_mkAntiquotSpliceNode___closed__5;
x_64 = lean_array_push(x_63, x_52);
x_65 = lean_array_push(x_64, x_56);
x_66 = lean_array_push(x_65, x_60);

4483
stage0/stdlib/Lean/Elab/Syntax.c generated
View file

File diff suppressed because it is too large Load diff

10
stage0/stdlib/Lean/Elab/Term.c generated
View file

@ -594,7 +594,6 @@ lean_object* l_Lean_Elab_throwAutoBoundImplicitLocal___at_Lean_Elab_Term_resolve
lean_object* l_Lean_FileMap_toPosition(lean_object*, lean_object*);
lean_object* l___private_Init_Util_0__mkPanicMessageWithDecl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_throwPostpone___at_Lean_Elab_Term_tryPostpone___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqNDRecImp___closed__6;
extern lean_object* l_Lean_instInhabitedKeyedDeclsAttribute___closed__1;
extern lean_object* l_Lean_KernelException_toMessageData___closed__15;
lean_object* l_Lean_Elab_Term_liftLevelM(lean_object*);
@ -652,6 +651,7 @@ lean_object* l_Lean_Elab_Term_elabSyntheticHole___closed__4;
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Term_0__Lean_Elab_Term_elabTermAux___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_ensureHasTypeAux_match__1(lean_object*);
lean_object* l_Lean_addTrace___at___private_Lean_Elab_Term_0__Lean_Elab_Term_postponeElabTerm___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Syntax_mkAntiquotSpliceNode___closed__5;
uint8_t l_Lean_Elab_Term_Context_autoBoundImplicit___default;
lean_object* l_Lean_Elab_Term_registerMVarErrorImplicitArgInfo___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_throwTypeMismatchError(lean_object*);
@ -14714,7 +14714,7 @@ lean_ctor_set(x_194, 0, x_192);
lean_inc(x_4);
x_195 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_195, 0, x_4);
x_196 = l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqNDRecImp___closed__6;
x_196 = l_Lean_Syntax_mkAntiquotSpliceNode___closed__5;
x_197 = lean_array_push(x_196, x_187);
x_198 = lean_array_push(x_197, x_29);
x_199 = lean_array_push(x_198, x_20);
@ -14770,7 +14770,7 @@ lean_ctor_set(x_210, 0, x_207);
lean_inc(x_4);
x_211 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_211, 0, x_4);
x_212 = l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqNDRecImp___closed__6;
x_212 = l_Lean_Syntax_mkAntiquotSpliceNode___closed__5;
x_213 = lean_array_push(x_212, x_208);
x_214 = lean_array_push(x_213, x_29);
x_215 = lean_array_push(x_214, x_20);
@ -15634,7 +15634,7 @@ lean_ctor_set(x_373, 0, x_368);
lean_inc(x_4);
x_374 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_374, 0, x_4);
x_375 = l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqNDRecImp___closed__6;
x_375 = l_Lean_Syntax_mkAntiquotSpliceNode___closed__5;
x_376 = lean_array_push(x_375, x_370);
x_377 = lean_array_push(x_376, x_371);
x_378 = lean_array_push(x_377, x_20);
@ -16676,7 +16676,7 @@ lean_ctor_set(x_561, 0, x_555);
lean_inc(x_4);
x_562 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_562, 0, x_4);
x_563 = l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqNDRecImp___closed__6;
x_563 = l_Lean_Syntax_mkAntiquotSpliceNode___closed__5;
x_564 = lean_array_push(x_563, x_557);
x_565 = lean_array_push(x_564, x_558);
x_566 = lean_array_push(x_565, x_559);

22
stage0/stdlib/Lean/Meta/AppBuilder.c generated
View file

@ -36,7 +36,6 @@ lean_object* l_Lean_Meta_mkDecideProof___rarg___lambda__1(lean_object*, lean_obj
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkAppMArgs_loop___closed__1;
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqImp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkAppOptMAux___closed__8;
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
lean_object* l_Lean_Meta_mkExpectedTypeHint___at_Lean_Meta_mkDecideProof___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkEqMP___rarg___closed__1;
lean_object* l_Lean_Meta_mkAppM___rarg___lambda__1___closed__1;
@ -245,7 +244,6 @@ lean_object* l_Lean_Meta_mkAppOptM___rarg(lean_object*, lean_object*, lean_objec
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkCongrArgImp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkArrayLit___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkHEqTrans___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqNDRecImp___closed__6;
extern lean_object* l_Lean_KernelException_toMessageData___closed__15;
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkAppMFinal___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkLambda(lean_object*, uint8_t, lean_object*, lean_object*);
@ -269,6 +267,7 @@ lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkCongrFunImp___close
size_t lean_usize_of_nat(lean_object*);
lean_object* l_Lean_Meta_mkAppM___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MessageData_arrayExpr_toMessageData(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Syntax_mkAntiquotSpliceNode___closed__5;
extern lean_object* l_Lean_Parser_Tactic_myMacro____x40_Init_Notation___hyg_14025____closed__1;
lean_object* l_Lean_Meta_mkHEqRefl___rarg(lean_object*, lean_object*);
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqOfHEqImp___lambda__1___closed__1;
@ -7959,15 +7958,6 @@ lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
static lean_object* _init_l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqNDRecImp___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(6u);
x_2 = lean_mk_empty_array_with_capacity(x_1);
return x_2;
}
}
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqNDRecImp(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
@ -8079,7 +8069,7 @@ lean_ctor_set(x_38, 0, x_35);
lean_ctor_set(x_38, 1, x_37);
x_39 = l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqNDRecImp___closed__2;
x_40 = l_Lean_mkConst(x_39, x_38);
x_41 = l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqNDRecImp___closed__6;
x_41 = l_Lean_Syntax_mkAntiquotSpliceNode___closed__5;
x_42 = lean_array_push(x_41, x_24);
x_43 = lean_array_push(x_42, x_25);
x_44 = lean_array_push(x_43, x_1);
@ -8109,7 +8099,7 @@ lean_ctor_set(x_53, 0, x_50);
lean_ctor_set(x_53, 1, x_52);
x_54 = l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqNDRecImp___closed__2;
x_55 = l_Lean_mkConst(x_54, x_53);
x_56 = l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqNDRecImp___closed__6;
x_56 = l_Lean_Syntax_mkAntiquotSpliceNode___closed__5;
x_57 = lean_array_push(x_56, x_24);
x_58 = lean_array_push(x_57, x_25);
x_59 = lean_array_push(x_58, x_1);
@ -8556,7 +8546,7 @@ lean_ctor_set(x_39, 0, x_36);
lean_ctor_set(x_39, 1, x_38);
x_40 = l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqRecImp___closed__1;
x_41 = l_Lean_mkConst(x_40, x_39);
x_42 = l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqNDRecImp___closed__6;
x_42 = l_Lean_Syntax_mkAntiquotSpliceNode___closed__5;
x_43 = lean_array_push(x_42, x_24);
x_44 = lean_array_push(x_43, x_25);
x_45 = lean_array_push(x_44, x_1);
@ -8586,7 +8576,7 @@ lean_ctor_set(x_54, 0, x_51);
lean_ctor_set(x_54, 1, x_53);
x_55 = l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqRecImp___closed__1;
x_56 = l_Lean_mkConst(x_55, x_54);
x_57 = l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqNDRecImp___closed__6;
x_57 = l_Lean_Syntax_mkAntiquotSpliceNode___closed__5;
x_58 = lean_array_push(x_57, x_24);
x_59 = lean_array_push(x_58, x_25);
x_60 = lean_array_push(x_59, x_1);
@ -13124,8 +13114,6 @@ l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqNDRecImp___closed__4 = _init_l
lean_mark_persistent(l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqNDRecImp___closed__4);
l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqNDRecImp___closed__5 = _init_l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqNDRecImp___closed__5();
lean_mark_persistent(l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqNDRecImp___closed__5);
l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqNDRecImp___closed__6 = _init_l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqNDRecImp___closed__6();
lean_mark_persistent(l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqNDRecImp___closed__6);
l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqRecImp___closed__1 = _init_l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqRecImp___closed__1();
lean_mark_persistent(l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqRecImp___closed__1);
l_Lean_Meta_mkEqMP___rarg___closed__1 = _init_l_Lean_Meta_mkEqMP___rarg___closed__1();

17
stage0/stdlib/Lean/Parser/Basic.c generated
View file

@ -94,6 +94,7 @@ lean_object* l_Lean_Parser_checkInsideQuotFn(lean_object*, lean_object*);
lean_object* l_Lean_Parser_binNumberFn___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_ParserState_toErrorMsg_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Error_merge_match__1___rarg(lean_object*, lean_object*);
extern lean_object* l_Lean_Syntax_mkAntiquotSuffixSpliceNode___closed__1;
lean_object* l_Lean_Parser_numberFnAux(lean_object*, lean_object*);
lean_object* l_Lean_Parser_withAntiquotSuffixSpliceFn___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_withoutInfo(lean_object*);
@ -264,7 +265,6 @@ uint8_t l_Lean_Parser_ParserContext_insideQuot___default;
lean_object* l_Lean_Parser_checkPrecFn(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_orelseFnCore_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
extern lean_object* l_Lean_Syntax_antiquotSuffixSplice_x3f_match__1___rarg___closed__1;
extern lean_object* l_myMacro____x40_Init_Notation___hyg_49____closed__15;
lean_object* l_Lean_Parser_indexed___rarg(lean_object*, lean_object*, lean_object*, uint8_t);
lean_object* l_Std_RBNode_find___at_Lean_Parser_indexed___spec__6(lean_object*);
@ -426,7 +426,6 @@ lean_object* l_Lean_Parser_parserOfStackFnUnsafe___closed__4;
lean_object* l_Lean_Parser_ParserState_mkNode_match__1___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Parser_peekToken(lean_object*, lean_object*);
lean_object* l_Lean_Parser_Error_toString___closed__4;
lean_object* l_Lean_Parser_withAntiquotSuffixSpliceFn___lambda__1___closed__1;
lean_object* l_Lean_Parser_SyntaxNodeKindSet_insert(lean_object*, lean_object*);
extern lean_object* l_Lean_strLitKind___closed__1;
lean_object* l_Lean_Parser_atomic(lean_object*);
@ -28329,21 +28328,11 @@ lean_dec(x_1);
return x_4;
}
}
static lean_object* _init_l_Lean_Parser_withAntiquotSuffixSpliceFn___lambda__1___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Syntax_antiquotSuffixSplice_x3f_match__1___rarg___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Parser_withAntiquotSuffixSpliceFn___lambda__1(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;
x_4 = l_Lean_Parser_withAntiquotSuffixSpliceFn___lambda__1___closed__1;
x_4 = l_Lean_Syntax_mkAntiquotSuffixSpliceNode___closed__1;
x_5 = l_Lean_Name_append(x_1, x_4);
x_6 = lean_ctor_get(x_2, 0);
lean_inc(x_6);
@ -31152,8 +31141,6 @@ l_Lean_Parser_mkAntiquotScope___closed__6 = _init_l_Lean_Parser_mkAntiquotScope_
lean_mark_persistent(l_Lean_Parser_mkAntiquotScope___closed__6);
l_Lean_Parser_mkAntiquotScope___closed__7 = _init_l_Lean_Parser_mkAntiquotScope___closed__7();
lean_mark_persistent(l_Lean_Parser_mkAntiquotScope___closed__7);
l_Lean_Parser_withAntiquotSuffixSpliceFn___lambda__1___closed__1 = _init_l_Lean_Parser_withAntiquotSuffixSpliceFn___lambda__1___closed__1();
lean_mark_persistent(l_Lean_Parser_withAntiquotSuffixSpliceFn___lambda__1___closed__1);
l_Lean_Parser_sepByElemParser___closed__1 = _init_l_Lean_Parser_sepByElemParser___closed__1();
lean_mark_persistent(l_Lean_Parser_sepByElemParser___closed__1);
l_Lean_Parser_categoryParserOfStackFn___closed__1 = _init_l_Lean_Parser_categoryParserOfStackFn___closed__1();

1586
stage0/stdlib/Lean/Parser/Transform.c generated
View file

File diff suppressed because it is too large Load diff

330
stage0/stdlib/Lean/Server/ServerBin.c generated
View file

@ -1,330 +0,0 @@
// Lean compiler output
// Module: Lean.Server.ServerBin
// Imports: Init Init.System.IO Lean.Server
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
#pragma clang diagnostic ignored "-Wunused-label"
#elif defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wunused-parameter"
#pragma GCC diagnostic ignored "-Wunused-label"
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
#ifdef __cplusplus
extern "C" {
#endif
lean_object* lean_get_stdin(lean_object*);
lean_object* lean_io_error_to_string(lean_object*);
lean_object* _lean_main(lean_object*, lean_object*);
lean_object* lean_get_stderr(lean_object*);
lean_object* l_main___boxed__const__1;
lean_object* l_IO_getStdin___at_main___spec__1(lean_object*);
lean_object* lean_init_search_path(lean_object*, lean_object*);
lean_object* lean_get_stdout(lean_object*);
lean_object* l_IO_FS_Stream_putStrLn___at_Lean_Server_Test_runWithInputFile___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_initAndRunServer(lean_object*, lean_object*, lean_object*);
lean_object* l_IO_getStdin___at_main___spec__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_get_stdin(x_1);
return x_2;
}
}
static lean_object* _init_l_main___boxed__const__1() {
_start:
{
uint32_t x_1; lean_object* x_2;
x_1 = 0;
x_2 = lean_box_uint32(x_1);
return x_2;
}
}
lean_object* _lean_main(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
lean_dec(x_1);
x_3 = lean_get_stdin(x_2);
if (lean_obj_tag(x_3) == 0)
{
lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_4 = lean_ctor_get(x_3, 0);
lean_inc(x_4);
x_5 = lean_ctor_get(x_3, 1);
lean_inc(x_5);
lean_dec(x_3);
x_6 = lean_get_stdout(x_5);
if (lean_obj_tag(x_6) == 0)
{
lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = lean_ctor_get(x_6, 0);
lean_inc(x_7);
x_8 = lean_ctor_get(x_6, 1);
lean_inc(x_8);
lean_dec(x_6);
x_9 = lean_get_stderr(x_8);
if (lean_obj_tag(x_9) == 0)
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
x_11 = lean_ctor_get(x_9, 1);
lean_inc(x_11);
lean_dec(x_9);
x_12 = lean_box(0);
x_13 = lean_init_search_path(x_12, x_11);
if (lean_obj_tag(x_13) == 0)
{
lean_object* x_14; lean_object* x_15;
x_14 = lean_ctor_get(x_13, 1);
lean_inc(x_14);
lean_dec(x_13);
x_15 = l_Lean_Server_initAndRunServer(x_4, x_7, x_14);
if (lean_obj_tag(x_15) == 0)
{
uint8_t x_16;
lean_dec(x_10);
x_16 = !lean_is_exclusive(x_15);
if (x_16 == 0)
{
lean_object* x_17; lean_object* x_18;
x_17 = lean_ctor_get(x_15, 0);
lean_dec(x_17);
x_18 = l_main___boxed__const__1;
lean_ctor_set(x_15, 0, x_18);
return x_15;
}
else
{
lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_19 = lean_ctor_get(x_15, 1);
lean_inc(x_19);
lean_dec(x_15);
x_20 = l_main___boxed__const__1;
x_21 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_21, 0, x_20);
lean_ctor_set(x_21, 1, x_19);
return x_21;
}
}
else
{
lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_22 = lean_ctor_get(x_15, 0);
lean_inc(x_22);
x_23 = lean_ctor_get(x_15, 1);
lean_inc(x_23);
lean_dec(x_15);
x_24 = lean_io_error_to_string(x_22);
x_25 = l_IO_FS_Stream_putStrLn___at_Lean_Server_Test_runWithInputFile___spec__1(x_10, x_24, x_23);
if (lean_obj_tag(x_25) == 0)
{
uint8_t x_26;
x_26 = !lean_is_exclusive(x_25);
if (x_26 == 0)
{
lean_object* x_27; lean_object* x_28;
x_27 = lean_ctor_get(x_25, 0);
lean_dec(x_27);
x_28 = l_main___boxed__const__1;
lean_ctor_set(x_25, 0, x_28);
return x_25;
}
else
{
lean_object* x_29; lean_object* x_30; lean_object* x_31;
x_29 = lean_ctor_get(x_25, 1);
lean_inc(x_29);
lean_dec(x_25);
x_30 = l_main___boxed__const__1;
x_31 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_31, 0, x_30);
lean_ctor_set(x_31, 1, x_29);
return x_31;
}
}
else
{
uint8_t x_32;
x_32 = !lean_is_exclusive(x_25);
if (x_32 == 0)
{
return x_25;
}
else
{
lean_object* x_33; lean_object* x_34; lean_object* x_35;
x_33 = lean_ctor_get(x_25, 0);
x_34 = lean_ctor_get(x_25, 1);
lean_inc(x_34);
lean_inc(x_33);
lean_dec(x_25);
x_35 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_35, 0, x_33);
lean_ctor_set(x_35, 1, x_34);
return x_35;
}
}
}
}
else
{
uint8_t x_36;
lean_dec(x_10);
lean_dec(x_7);
lean_dec(x_4);
x_36 = !lean_is_exclusive(x_13);
if (x_36 == 0)
{
return x_13;
}
else
{
lean_object* x_37; lean_object* x_38; lean_object* x_39;
x_37 = lean_ctor_get(x_13, 0);
x_38 = lean_ctor_get(x_13, 1);
lean_inc(x_38);
lean_inc(x_37);
lean_dec(x_13);
x_39 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_39, 0, x_37);
lean_ctor_set(x_39, 1, x_38);
return x_39;
}
}
}
else
{
uint8_t x_40;
lean_dec(x_7);
lean_dec(x_4);
x_40 = !lean_is_exclusive(x_9);
if (x_40 == 0)
{
return x_9;
}
else
{
lean_object* x_41; lean_object* x_42; lean_object* x_43;
x_41 = lean_ctor_get(x_9, 0);
x_42 = lean_ctor_get(x_9, 1);
lean_inc(x_42);
lean_inc(x_41);
lean_dec(x_9);
x_43 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_43, 0, x_41);
lean_ctor_set(x_43, 1, x_42);
return x_43;
}
}
}
else
{
uint8_t x_44;
lean_dec(x_4);
x_44 = !lean_is_exclusive(x_6);
if (x_44 == 0)
{
return x_6;
}
else
{
lean_object* x_45; lean_object* x_46; lean_object* x_47;
x_45 = lean_ctor_get(x_6, 0);
x_46 = lean_ctor_get(x_6, 1);
lean_inc(x_46);
lean_inc(x_45);
lean_dec(x_6);
x_47 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_47, 0, x_45);
lean_ctor_set(x_47, 1, x_46);
return x_47;
}
}
}
else
{
uint8_t x_48;
x_48 = !lean_is_exclusive(x_3);
if (x_48 == 0)
{
return x_3;
}
else
{
lean_object* x_49; lean_object* x_50; lean_object* x_51;
x_49 = lean_ctor_get(x_3, 0);
x_50 = lean_ctor_get(x_3, 1);
lean_inc(x_50);
lean_inc(x_49);
lean_dec(x_3);
x_51 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_51, 0, x_49);
lean_ctor_set(x_51, 1, x_50);
return x_51;
}
}
}
}
lean_object* initialize_Init(lean_object*);
lean_object* initialize_Init_System_IO(lean_object*);
lean_object* initialize_Lean_Server(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Lean_Server_ServerBin(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_initialized = true;
res = initialize_Init(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_System_IO(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Server(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_main___boxed__const__1 = _init_l_main___boxed__const__1();
lean_mark_persistent(l_main___boxed__const__1);
return lean_io_result_mk_ok(lean_box(0));
}
void lean_initialize();
#if defined(WIN32) || defined(_WIN32)
#include <windows.h>
#endif
int main(int argc, char ** argv) {
#if defined(WIN32) || defined(_WIN32)
SetErrorMode(SEM_FAILCRITICALERRORS);
#endif
lean_object* in; lean_object* res;
lean_initialize();
res = initialize_Lean_Server_ServerBin(lean_io_mk_world());
lean_io_mark_end_initialization();
if (lean_io_result_is_ok(res)) {
lean_dec_ref(res);
lean_init_task_manager();
in = lean_box(0);
int i = argc;
while (i > 1) {
lean_object* n;
i--;
n = lean_alloc_ctor(1,2,0); lean_ctor_set(n, 0, lean_mk_string(argv[i])); lean_ctor_set(n, 1, in);
in = n;
}
res = _lean_main(in, lean_io_mk_world());
}
if (lean_io_result_is_ok(res)) {
int ret = lean_unbox(lean_io_result_get_value(res));
lean_dec_ref(res);
return ret;
} else {
lean_io_result_show_error(res);
lean_dec_ref(res);
return 1;
}
}
#ifdef __cplusplus
}
#endif

156
stage0/stdlib/Lean/Syntax.c generated
View file

@ -28,6 +28,7 @@ uint8_t l_Lean_Syntax_isAntiquotSuffixSplice(lean_object*);
lean_object* l_Lean_Syntax_replaceM___rarg___lambda__2(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getTailWithPos(lean_object*);
size_t l_USize_add(size_t, size_t);
lean_object* l_Lean_Syntax_mkAntiquotSpliceNode___closed__4;
lean_object* l_Lean_SyntaxNode_modifyArgs_match__1(lean_object*);
lean_object* l_Lean_Syntax_isQuot_match__1___rarg___closed__2;
lean_object* l_Lean_Syntax_mkAntiquotNode___closed__3;
@ -41,6 +42,7 @@ lean_object* l_List_map___at_Lean_Syntax_formatStxAux___spec__1___boxed(lean_obj
extern lean_object* l_Lean_nullKind;
lean_object* l_Lean_Syntax_getAntiquotSuffixSpliceInner(lean_object*);
lean_object* l_Lean_Syntax_reprint___closed__1;
extern lean_object* l_term_x5b___x5d___closed__9;
lean_object* l_Lean_Syntax_rewriteBottomUpM___rarg___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_modifyArg(lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
@ -49,6 +51,7 @@ lean_object* l_Lean_Syntax_replaceM___rarg___lambda__3(lean_object*, lean_object
lean_object* lean_array_uget(lean_object*, size_t);
lean_object* l_Lean_Format_joinSep___at_Lean_Syntax_formatStxAux___spec__2(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_ifNodeKind___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_mkAntiquotSuffixSpliceNode___closed__1;
lean_object* l_Lean_Syntax_mkAntiquotNode___closed__7;
lean_object* l_Lean_Syntax_Traverser_up(lean_object*);
lean_object* l_Lean_Syntax_antiquotSuffixSplice_x3f(lean_object*);
@ -60,6 +63,7 @@ lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
lean_object* l_Lean_SyntaxNode_withArgs_match__1(lean_object*);
lean_object* l_Lean_Syntax_rewriteBottomUpM_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_ifNode_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_mkAntiquotSuffixSpliceNode___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_MonadTraverser_getCur___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_ifNodeKind_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_MonadTraverser_goRight___rarg___lambda__1(lean_object*);
@ -74,6 +78,7 @@ extern lean_object* l_Array_empty___closed__1;
lean_object* l_Lean_Syntax_MonadTraverser_goRight(lean_object*);
lean_object* l_Lean_Syntax_isAntiquot_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_SyntaxNode_withArgs(lean_object*);
lean_object* l_Lean_Syntax_mkAntiquotSpliceNode(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_instInhabitedParserDescr___closed__1;
lean_object* l_List_map___at_Lean_Syntax_formatStxAux___spec__7___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_formatStxAux___closed__7;
@ -81,6 +86,7 @@ uint8_t lean_name_eq(lean_object*, lean_object*);
lean_object* l_Array_foldlMUnsafe_fold___at_Lean_Syntax_reprint___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_isQuot_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getAtomVal_x21___boxed(lean_object*);
lean_object* l_Lean_Syntax_mkAntiquotSuffixSpliceNode(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_setAtomVal_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_instInhabitedNat;
lean_object* l_Lean_Syntax_getAtomVal_x21___closed__1;
@ -105,6 +111,7 @@ lean_object* l_Lean_Syntax_updateTrailing_match__1___rarg(lean_object*, lean_obj
lean_object* l_Lean_Syntax_getAtomVal_x21___closed__4;
lean_object* l_Lean_Syntax_MonadTraverser_getCur___rarg___closed__1;
lean_object* l_Lean_Syntax_getAntiquotTerm___boxed(lean_object*);
lean_object* l_Lean_Syntax_mkAntiquotSpliceNode___closed__2;
uint8_t l_USize_decLt(size_t, size_t);
extern lean_object* l_term___x24_______closed__5;
lean_object* l_Lean_Syntax_MonadTraverser_goDown(lean_object*);
@ -150,6 +157,7 @@ lean_object* l_List_map___at_Lean_Syntax_formatStxAux___spec__4___boxed(lean_obj
lean_object* l_Lean_Syntax_formatStxAux___closed__5;
lean_object* l_Lean_Syntax_updateTrailing(lean_object*, lean_object*);
lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_mkAntiquotSpliceNode___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_myMacro____x40_Init_Notation___hyg_49____closed__13;
uint8_t l_List_beq___at_Lean_Syntax_structEq___spec__3(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_replaceM_match__2(lean_object*);
@ -158,6 +166,7 @@ lean_object* l_Lean_Syntax_MonadTraverser_getIdx(lean_object*);
lean_object* l_Lean_Syntax_asNode_match__1(lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Syntax_updateLeading___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_structEq___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_mkAntiquotSpliceNode___closed__1;
lean_object* l_Lean_Syntax_MonadTraverser_goLeft___rarg(lean_object*);
lean_object* l_Lean_Syntax_MonadTraverser_goDown___rarg(lean_object*, lean_object*);
lean_object* l_Lean_SyntaxNode_getKind_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -204,6 +213,7 @@ lean_object* l_addParenHeuristic(lean_object*);
lean_object* l_Lean_Syntax_isMissing___boxed(lean_object*);
lean_object* l_Lean_Syntax_setAtomVal_match__1(lean_object*);
lean_object* l___private_Lean_Syntax_0__Lean_Syntax_updateInfo_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_mkAntiquotSpliceNode___closed__3;
lean_object* l_Lean_Syntax_MonadTraverser_setCur(lean_object*);
lean_object* l_Lean_Syntax_MonadTraverser_goLeft___rarg___closed__1;
lean_object* l_Lean_SyntaxNode_modifyArgs(lean_object*, lean_object*);
@ -224,6 +234,7 @@ lean_object* l_Lean_Syntax_isAntiquotScope___boxed(lean_object*);
extern lean_object* l_instReprIterator___closed__2;
lean_object* l_Lean_Syntax_formatStxAux_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_map___at_Lean_Syntax_formatStxAux___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_mkAntiquotSpliceNode___closed__6;
lean_object* l___private_Lean_Syntax_0__Lean_Syntax_formatInfo_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getAtomVal_x21___closed__3;
lean_object* l_Lean_Syntax_MonadTraverser_goLeft___rarg___lambda__1(lean_object*);
@ -233,6 +244,7 @@ lean_object* l_Lean_Syntax_MonadTraverser_goUp(lean_object*);
lean_object* l_Lean_Syntax_mkAntiquotNode___closed__9;
uint8_t l_Lean_Syntax_isAntiquot(lean_object*);
lean_object* l_Lean_Syntax_ifNode___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_mkAntiquotSpliceNode___closed__5;
lean_object* l_Lean_Syntax_instToStringSyntax;
lean_object* l_Array_back___at_Lean_Syntax_Traverser_up___spec__2___boxed(lean_object*);
lean_object* l_Lean_SyntaxNode_getNumArgs___boxed(lean_object*);
@ -352,6 +364,7 @@ lean_object* l_Lean_Syntax_mkAntiquotNode___closed__11;
lean_object* l_Lean_Syntax_reprint(lean_object*);
lean_object* l_Lean_Syntax_antiquotScopeKind_x3f_match__1___rarg___closed__1;
lean_object* l_Lean_Syntax_MonadTraverser_getCur___rarg___lambda__1___boxed(lean_object*);
extern lean_object* l_term_x5b___x5d___closed__3;
lean_object* l_Lean_Syntax_ifNodeKind_match__1(lean_object*);
uint8_t lean_string_dec_eq(lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
@ -9098,6 +9111,100 @@ lean_dec(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Syntax_mkAntiquotSpliceNode___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("antiquot_splice");
return x_1;
}
}
static lean_object* _init_l_Lean_Syntax_mkAntiquotSpliceNode___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Syntax_mkAntiquotSpliceNode___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
static lean_object* _init_l_Lean_Syntax_mkAntiquotSpliceNode___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_term_x5b___x5d___closed__3;
x_2 = l_Lean_mkAtom(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Syntax_mkAntiquotSpliceNode___closed__4() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_term_x5b___x5d___closed__9;
x_2 = l_Lean_mkAtom(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Syntax_mkAntiquotSpliceNode___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(6u);
x_2 = lean_mk_empty_array_with_capacity(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Syntax_mkAntiquotSpliceNode___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Syntax_mkAntiquotSpliceNode___closed__5;
x_2 = l_Lean_Syntax_mkAntiquotNode___closed__1;
x_3 = lean_array_push(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Syntax_mkAntiquotSpliceNode(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_5 = l_Lean_Syntax_mkAntiquotNode___closed__1;
x_6 = lean_mk_array(x_4, x_5);
x_7 = l_Lean_nullKind;
x_8 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_8, 0, x_7);
lean_ctor_set(x_8, 1, x_6);
x_9 = l_Lean_Syntax_mkAntiquotSpliceNode___closed__2;
x_10 = l_Lean_Name_append(x_1, x_9);
x_11 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_11, 0, x_7);
lean_ctor_set(x_11, 1, x_2);
x_12 = l_Lean_mkAtom(x_3);
x_13 = l_Lean_Syntax_mkAntiquotSpliceNode___closed__6;
x_14 = lean_array_push(x_13, x_8);
x_15 = l_Lean_Syntax_mkAntiquotSpliceNode___closed__3;
x_16 = lean_array_push(x_14, x_15);
x_17 = lean_array_push(x_16, x_11);
x_18 = l_Lean_Syntax_mkAntiquotSpliceNode___closed__4;
x_19 = lean_array_push(x_17, x_18);
x_20 = lean_array_push(x_19, x_12);
x_21 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_21, 0, x_10);
lean_ctor_set(x_21, 1, x_20);
return x_21;
}
}
lean_object* l_Lean_Syntax_mkAntiquotSpliceNode___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l_Lean_Syntax_mkAntiquotSpliceNode(x_1, x_2, x_3, x_4);
lean_dec(x_1);
return x_5;
}
}
static lean_object* _init_l_Lean_Syntax_antiquotSuffixSplice_x3f_match__1___rarg___closed__1() {
_start:
{
@ -9274,6 +9381,41 @@ lean_dec(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Syntax_mkAntiquotSuffixSpliceNode___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Syntax_antiquotSuffixSplice_x3f_match__1___rarg___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Syntax_mkAntiquotSuffixSpliceNode(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;
x_4 = l_Lean_Syntax_mkAntiquotSuffixSpliceNode___closed__1;
x_5 = l_Lean_Name_append(x_1, x_4);
x_6 = l_Lean_mkAtom(x_3);
x_7 = l_Lean_Syntax_mkApp___closed__1;
x_8 = lean_array_push(x_7, x_2);
x_9 = lean_array_push(x_8, x_6);
x_10 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_10, 0, x_5);
lean_ctor_set(x_10, 1, x_9);
return x_10;
}
}
lean_object* l_Lean_Syntax_mkAntiquotSuffixSpliceNode___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Lean_Syntax_mkAntiquotSuffixSpliceNode(x_1, x_2, x_3);
lean_dec(x_1);
return x_4;
}
}
lean_object* initialize_Init(lean_object*);
lean_object* initialize_Lean_Data_Name(lean_object*);
lean_object* initialize_Lean_Data_Format(lean_object*);
@ -9379,8 +9521,22 @@ l_Lean_Syntax_antiquotKind_x3f___closed__1 = _init_l_Lean_Syntax_antiquotKind_x3
lean_mark_persistent(l_Lean_Syntax_antiquotKind_x3f___closed__1);
l_Lean_Syntax_antiquotScopeKind_x3f_match__1___rarg___closed__1 = _init_l_Lean_Syntax_antiquotScopeKind_x3f_match__1___rarg___closed__1();
lean_mark_persistent(l_Lean_Syntax_antiquotScopeKind_x3f_match__1___rarg___closed__1);
l_Lean_Syntax_mkAntiquotSpliceNode___closed__1 = _init_l_Lean_Syntax_mkAntiquotSpliceNode___closed__1();
lean_mark_persistent(l_Lean_Syntax_mkAntiquotSpliceNode___closed__1);
l_Lean_Syntax_mkAntiquotSpliceNode___closed__2 = _init_l_Lean_Syntax_mkAntiquotSpliceNode___closed__2();
lean_mark_persistent(l_Lean_Syntax_mkAntiquotSpliceNode___closed__2);
l_Lean_Syntax_mkAntiquotSpliceNode___closed__3 = _init_l_Lean_Syntax_mkAntiquotSpliceNode___closed__3();
lean_mark_persistent(l_Lean_Syntax_mkAntiquotSpliceNode___closed__3);
l_Lean_Syntax_mkAntiquotSpliceNode___closed__4 = _init_l_Lean_Syntax_mkAntiquotSpliceNode___closed__4();
lean_mark_persistent(l_Lean_Syntax_mkAntiquotSpliceNode___closed__4);
l_Lean_Syntax_mkAntiquotSpliceNode___closed__5 = _init_l_Lean_Syntax_mkAntiquotSpliceNode___closed__5();
lean_mark_persistent(l_Lean_Syntax_mkAntiquotSpliceNode___closed__5);
l_Lean_Syntax_mkAntiquotSpliceNode___closed__6 = _init_l_Lean_Syntax_mkAntiquotSpliceNode___closed__6();
lean_mark_persistent(l_Lean_Syntax_mkAntiquotSpliceNode___closed__6);
l_Lean_Syntax_antiquotSuffixSplice_x3f_match__1___rarg___closed__1 = _init_l_Lean_Syntax_antiquotSuffixSplice_x3f_match__1___rarg___closed__1();
lean_mark_persistent(l_Lean_Syntax_antiquotSuffixSplice_x3f_match__1___rarg___closed__1);
l_Lean_Syntax_mkAntiquotSuffixSpliceNode___closed__1 = _init_l_Lean_Syntax_mkAntiquotSuffixSpliceNode___closed__1();
lean_mark_persistent(l_Lean_Syntax_mkAntiquotSuffixSpliceNode___closed__1);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus