chore: update stage0
This commit is contained in:
Leonardo de Moura
parent
f80e2c1db6
commit
c43d2c8a7f
4 changed files with 427 additions and 3 deletions
9
stage0/src/Lean/Elab/BuiltinNotation.lean
generated
9
stage0/src/Lean/Elab/BuiltinNotation.lean
generated
|
|
@ -364,4 +364,13 @@ private def elabCDot (stx : Syntax) (expectedType? : Option Expr) : TermElabM Ex
|
|||
mkEqNDRec (← mkMotive expectedAbst) h heq
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
@[builtinTermElab stateRefT] def elabStateRefT : TermElab := fun stx _ => do
|
||||
let σ ← elabType stx[1]
|
||||
let m ← elabTerm stx[2] (← mkArrow (mkSort levelOne) (mkSort levelOne))
|
||||
let ω ← mkFreshExprMVar (mkSort levelOne)
|
||||
let stWorld ← mkAppM `STWorld #[ω, m]
|
||||
mkInstMVar stWorld
|
||||
mkAppM `StateRefT' #[ω, σ, m]
|
||||
|
||||
|
||||
end Lean.Elab.Term
|
||||
|
|
|
|||
4
stage0/src/Lean/Parser/Term.lean
generated
4
stage0/src/Lean/Parser/Term.lean
generated
|
|
@ -259,8 +259,8 @@ def isIdent (stx : Syntax) : Bool :=
|
|||
@[builtinTermParser] def dbgTrace := parser!:leadPrec withPosition ("dbgTrace! " >> ((interpolatedStr termParser) <|> termParser)) >> optSemicolon termParser
|
||||
@[builtinTermParser] def assert := parser!:leadPrec withPosition ("assert! " >> termParser) >> optSemicolon termParser
|
||||
|
||||
-- Macro for avoiding exponentially big terms when using due to `STWorld`
|
||||
@[builtinTermParser] def stateRefT := parser! "StateRefTNew" >> termParser maxPrec >> termParser maxPrec
|
||||
-- Macro for avoiding exponentially big terms when using `STWorld`
|
||||
@[builtinTermParser] def stateRefT := parser! "StateRefT" >> termParser maxPrec >> termParser maxPrec
|
||||
|
||||
end Term
|
||||
|
||||
|
|
|
|||
415
stage0/stdlib/Lean/Elab/BuiltinNotation.c
generated
415
stage0/stdlib/Lean/Elab/BuiltinNotation.c
generated
|
|
@ -53,6 +53,7 @@ extern lean_object* l___kind_term____x40_Init_Data_ToString_Macro___hyg_2____clo
|
|||
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_Lean_Elab_getRefPos___at_Lean_Elab_Term_elabPanic___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_elabLetDeclCore___spec__1___rarg(lean_object*);
|
||||
lean_object* l_Lean_mkSort(lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_expandPrefixOp___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_953____closed__7;
|
||||
lean_object* l_Lean_Elab_Term_expandModN___closed__3;
|
||||
|
|
@ -356,6 +357,7 @@ lean_object* l_Lean_Elab_Term_expandDiv___closed__1;
|
|||
extern lean_object* l_Lean_Meta_mkDecide___rarg___closed__1;
|
||||
lean_object* l_Lean_Elab_Term_expandPow(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabNativeRefl___lambda__1___closed__5;
|
||||
lean_object* l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__1;
|
||||
lean_object* l___regBuiltin_Lean_Elab_Term_expandBAnd___closed__1;
|
||||
lean_object* l___regBuiltin_Lean_Elab_Term_expandProd(lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_expandAndM(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -374,6 +376,7 @@ lean_object* l_Lean_Elab_Term_expandUnreachable(lean_object*, lean_object*);
|
|||
extern lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___lambda__2___closed__10;
|
||||
lean_object* l_Lean_Elab_Term_ExpandFComp___closed__4;
|
||||
lean_object* l_Lean_Elab_Term_expandBAnd(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_mkInstMVar(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___regBuiltin_Lean_Elab_Term_expandEmptyC___closed__1;
|
||||
uint8_t l_Lean_Expr_hasExprMVar(lean_object*);
|
||||
lean_object* l_Lean_Meta_mkEqSymm___at_Lean_Elab_Term_elabSubst___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -448,6 +451,7 @@ lean_object* lean_st_mk_ref(lean_object*, lean_object*);
|
|||
lean_object* l___regBuiltin_Lean_Elab_Term_expandGT(lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_expandSub___closed__1;
|
||||
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabTParserMacroAux_match__1(lean_object*);
|
||||
lean_object* l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__2;
|
||||
lean_object* l___private_Lean_Meta_AppBuilder_0__Lean_Meta_mkEqNDRecImp(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___regBuiltin_Lean_Elab_Term_expandAnd___closed__2;
|
||||
lean_object* l___regBuiltin_Lean_Elab_Term_elabParen___closed__1;
|
||||
|
|
@ -490,6 +494,7 @@ lean_object* l___regBuiltin_Lean_Elab_Term_expandUMinus(lean_object*);
|
|||
lean_object* l_Lean_Elab_Term_expandBNe___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___regBuiltin_Lean_Elab_Term_expandOrM(lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabNativeRefl___lambda__1___closed__9;
|
||||
lean_object* l_Lean_Meta_mkArrow___at_Lean_Elab_Term_elabStateRefT___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Literal_type___closed__2;
|
||||
extern lean_object* l_Lean_myMacro____x40_Lean_Util_Trace___hyg_953____closed__19;
|
||||
extern lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_compileStxMatch___lambda__1___closed__2;
|
||||
|
|
@ -509,6 +514,7 @@ lean_object* l___regBuiltin_Lean_Elab_Term_expandAnd___closed__3;
|
|||
lean_object* l___regBuiltin_Lean_Elab_Term_elabDecide___closed__2;
|
||||
uint8_t l_Lean_Expr_isConstOf(lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Meta_mkLt___rarg___closed__4;
|
||||
lean_object* l_Lean_Elab_Term_elabStateRefT___closed__1;
|
||||
lean_object* l___regBuiltin_Lean_Elab_Term_elabPanic___closed__2;
|
||||
lean_object* l_Lean_Elab_Term_expandAssert___closed__13;
|
||||
lean_object* l_Lean_Elab_Term_expandMod___closed__3;
|
||||
|
|
@ -561,11 +567,13 @@ extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_299____clos
|
|||
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabClosedTerm(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_expandAssert___closed__6;
|
||||
lean_object* l_Lean_Elab_Term_expandLE___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabStateRefT___closed__2;
|
||||
lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_mkNativeReflAuxDecl___closed__1;
|
||||
lean_object* l_Lean_Elab_Term_expandShow___closed__6;
|
||||
lean_object* l_Lean_Elab_Term_expandBAnd___closed__1;
|
||||
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_mkNativeReflAuxDecl___closed__2;
|
||||
lean_object* l_Lean_Elab_Term_elabStateRefT___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_expandGE(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___regBuiltin_Lean_Elab_Term_elabDecide___closed__1;
|
||||
lean_object* l_Lean_Elab_Term_expandMul___boxed(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -585,6 +593,7 @@ lean_object* l_Lean_Elab_Term_ExpandFComp___closed__1;
|
|||
lean_object* l___regBuiltin_Lean_Elab_Term_expandIff___closed__3;
|
||||
lean_object* l_Lean_Elab_Term_expandModN___closed__2;
|
||||
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__25;
|
||||
lean_object* l_Lean_Elab_Term_elabStateRefT___closed__5;
|
||||
lean_object* l_Lean_Elab_Term_expandSubtype___closed__3;
|
||||
lean_object* l_Lean_Elab_Term_expandEq___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___regBuiltin_Lean_Elab_Term_expandModN___closed__3;
|
||||
|
|
@ -616,6 +625,7 @@ lean_object* l_Lean_Elab_Term_expandHave___closed__7;
|
|||
lean_object* l_Lean_Syntax_setArg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* lean_environment_main_module(lean_object*);
|
||||
extern lean_object* l___private_Init_LeanInit_0__Lean_quoteList___rarg___closed__7;
|
||||
lean_object* l_Lean_Elab_Term_elabStateRefT___closed__6;
|
||||
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__5;
|
||||
lean_object* l_Lean_Elab_Term_elabSubst_match__3___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__28;
|
||||
|
|
@ -704,6 +714,7 @@ lean_object* l_Lean_Elab_Term_elabSubst___lambda__6(lean_object*, lean_object*,
|
|||
uint8_t l_Lean_Expr_isFVar(lean_object*);
|
||||
lean_object* l___regBuiltin_Lean_Elab_Term_expandEq(lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_expandHave___closed__5;
|
||||
lean_object* l_Lean_mkForall(lean_object*, uint8_t, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabParserMacro___closed__1;
|
||||
lean_object* l_Lean_Elab_Term_expandNe___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -724,6 +735,7 @@ lean_object* l_Lean_Elab_Term_expandseqLeft___closed__4;
|
|||
lean_object* l_Lean_Elab_Term_expandUnreachable___rarg___closed__9;
|
||||
lean_object* l___regBuiltin_Lean_Elab_Term_expandDollar(lean_object*);
|
||||
extern lean_object* l_Lean_Meta_mkSorry___rarg___lambda__1___closed__2;
|
||||
lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_mkFreshExprMVarImpl(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_expandAssert___closed__19;
|
||||
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__9;
|
||||
lean_object* l_Lean_Elab_getRefPos___at_Lean_Elab_Term_elabPanic___spec__2___rarg(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -776,6 +788,7 @@ extern lean_object* l_Lean_Elab_Term_elabLetDeclCore___closed__9;
|
|||
lean_object* l___regBuiltin_Lean_Elab_Term_expandMul___closed__1;
|
||||
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__8;
|
||||
lean_object* l_Lean_Elab_Term_elabPanic___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_mkAppM___at___private_Lean_Elab_Term_0__Lean_Elab_Term_isMonad_x3f___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_expandseqRight___closed__4;
|
||||
lean_object* l_Lean_Elab_Term_expandseqLeft___closed__1;
|
||||
lean_object* l_Lean_Elab_Term_expandseq(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -788,7 +801,9 @@ lean_object* l___regBuiltin_Lean_Elab_Term_elabParserMacro___closed__1;
|
|||
lean_object* l_Lean_Elab_Term_mkPairs(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabAnonymousCtor___closed__5;
|
||||
lean_object* l_Lean_Elab_Term_expandSorry___rarg___closed__4;
|
||||
lean_object* l_Lean_Elab_Term_elabStateRefT___closed__3;
|
||||
lean_object* l_Lean_Elab_Term_expandInfix___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabStateRefT(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_expandseqLeft___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_mkStxLit(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___regBuiltin_Lean_Elab_Term_expandOrElse(lean_object*);
|
||||
|
|
@ -822,6 +837,7 @@ lean_object* l_Lean_Elab_Term_expandMap___boxed(lean_object*, lean_object*, lean
|
|||
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabParserMacroAux___closed__13;
|
||||
lean_object* l_Lean_Elab_Term_expandMap___closed__1;
|
||||
lean_object* l_Lean_Elab_Term_elabAnonymousCtor___closed__7;
|
||||
lean_object* l_Lean_Meta_mkArrow___at_Lean_Elab_Term_elabStateRefT___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___regBuiltin_Lean_Elab_Term_expandBEq(lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_expandMapRev___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_expandAssert___closed__9;
|
||||
|
|
@ -849,6 +865,7 @@ lean_object* l___regBuiltin_Lean_Elab_Term_expandLT___closed__1;
|
|||
lean_object* l_Lean_Elab_Term_expandAssert___closed__8;
|
||||
lean_object* l_Lean_Elab_Term_expandUnreachable___rarg___closed__5;
|
||||
lean_object* l_Lean_Elab_Term_expandHave___closed__6;
|
||||
extern lean_object* l_Lean_levelOne;
|
||||
extern lean_object* l_myMacro____x40_Init_Data_ToString_Macro___hyg_39____closed__8;
|
||||
lean_object* l_Lean_Elab_Term_expandMap(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l___regBuiltin_Lean_Elab_Term_expandGE___closed__3;
|
||||
|
|
@ -885,6 +902,7 @@ lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_getPropToDe
|
|||
lean_object* l_Lean_Meta_mkEqRefl___at_Lean_Elab_Term_elabNativeRefl___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_expandAnd___closed__2;
|
||||
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
|
||||
lean_object* l___regBuiltin_Lean_Elab_Term_elabStateRefT(lean_object*);
|
||||
lean_object* l___private_Lean_Elab_BuiltinNotation_0__Lean_Elab_Term_elabTParserMacroAux___closed__4;
|
||||
lean_object* l_Lean_Elab_Term_expandAdd___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_expandShow___closed__14;
|
||||
|
|
@ -893,6 +911,8 @@ lean_object* l_Lean_Elab_Term_expandGT___closed__2;
|
|||
lean_object* l_Lean_Elab_Term_expandAssert___closed__1;
|
||||
lean_object* l_Lean_Elab_Term_elabSubst_match__2___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_expandOrElse(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_elabStateRefT___closed__4;
|
||||
extern lean_object* l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryCoe___closed__3;
|
||||
lean_object* l_Lean_Elab_Term_expandUnreachable___rarg___closed__8;
|
||||
lean_object* l___regBuiltin_Lean_Elab_Term_expandseq(lean_object*);
|
||||
lean_object* l___regBuiltin_Lean_Elab_Term_elabAnonymousCtor___closed__1;
|
||||
|
|
@ -931,6 +951,7 @@ uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
|
|||
extern lean_object* l_Lean_Meta_mkArrow___rarg___closed__2;
|
||||
lean_object* l_Lean_Elab_Term_expandAndThen(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Elab_Term_expandAssert___closed__4;
|
||||
lean_object* l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__3;
|
||||
lean_object* l_Lean_Elab_Term_elabSubst___closed__1;
|
||||
static lean_object* _init_l_Lean_Elab_Term_expandDollar___closed__1() {
|
||||
_start:
|
||||
|
|
@ -15852,6 +15873,379 @@ x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
|
|||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Meta_mkArrow___at_Lean_Elab_Term_elabStateRefT___spec__1(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, lean_object* x_9) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_10; lean_object* x_11; uint8_t x_12;
|
||||
x_10 = l_Lean_Meta_mkArrow___rarg___closed__2;
|
||||
x_11 = l___private_Lean_CoreM_0__Lean_Core_mkFreshNameImp(x_10, x_7, x_8, x_9);
|
||||
x_12 = !lean_is_exclusive(x_11);
|
||||
if (x_12 == 0)
|
||||
{
|
||||
lean_object* x_13; uint8_t x_14; lean_object* x_15;
|
||||
x_13 = lean_ctor_get(x_11, 0);
|
||||
x_14 = 0;
|
||||
x_15 = l_Lean_mkForall(x_13, x_14, x_1, x_2);
|
||||
lean_ctor_set(x_11, 0, x_15);
|
||||
return x_11;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_16; lean_object* x_17; uint8_t x_18; lean_object* x_19; lean_object* x_20;
|
||||
x_16 = lean_ctor_get(x_11, 0);
|
||||
x_17 = lean_ctor_get(x_11, 1);
|
||||
lean_inc(x_17);
|
||||
lean_inc(x_16);
|
||||
lean_dec(x_11);
|
||||
x_18 = 0;
|
||||
x_19 = l_Lean_mkForall(x_16, x_18, x_1, x_2);
|
||||
x_20 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_20, 0, x_19);
|
||||
lean_ctor_set(x_20, 1, x_17);
|
||||
return x_20;
|
||||
}
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Term_elabStateRefT___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_levelOne;
|
||||
x_2 = l_Lean_mkSort(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Term_elabStateRefT___closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2;
|
||||
x_1 = l_Lean_Elab_Term_elabStateRefT___closed__1;
|
||||
x_2 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_2, 0, x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Term_elabStateRefT___closed__3() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("STWorld");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Term_elabStateRefT___closed__4() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = lean_box(0);
|
||||
x_2 = l_Lean_Elab_Term_elabStateRefT___closed__3;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Term_elabStateRefT___closed__5() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("StateRefT'");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l_Lean_Elab_Term_elabStateRefT___closed__6() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = lean_box(0);
|
||||
x_2 = l_Lean_Elab_Term_elabStateRefT___closed__5;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Elab_Term_elabStateRefT(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, lean_object* x_9) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_10; lean_object* x_11; lean_object* x_12;
|
||||
x_10 = lean_unsigned_to_nat(1u);
|
||||
x_11 = l_Lean_Syntax_getArg(x_1, x_10);
|
||||
lean_inc(x_8);
|
||||
lean_inc(x_7);
|
||||
lean_inc(x_6);
|
||||
lean_inc(x_5);
|
||||
lean_inc(x_4);
|
||||
lean_inc(x_3);
|
||||
x_12 = l_Lean_Elab_Term_elabType(x_11, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
|
||||
if (lean_obj_tag(x_12) == 0)
|
||||
{
|
||||
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; uint8_t x_22; lean_object* x_23;
|
||||
x_13 = lean_ctor_get(x_12, 0);
|
||||
lean_inc(x_13);
|
||||
x_14 = lean_ctor_get(x_12, 1);
|
||||
lean_inc(x_14);
|
||||
lean_dec(x_12);
|
||||
x_15 = l_Lean_Elab_Term_elabStateRefT___closed__1;
|
||||
x_16 = l_Lean_Meta_mkArrow___at_Lean_Elab_Term_elabStateRefT___spec__1(x_15, x_15, x_3, x_4, x_5, x_6, x_7, x_8, x_14);
|
||||
x_17 = lean_ctor_get(x_16, 0);
|
||||
lean_inc(x_17);
|
||||
x_18 = lean_ctor_get(x_16, 1);
|
||||
lean_inc(x_18);
|
||||
lean_dec(x_16);
|
||||
x_19 = lean_unsigned_to_nat(2u);
|
||||
x_20 = l_Lean_Syntax_getArg(x_1, x_19);
|
||||
x_21 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_21, 0, x_17);
|
||||
x_22 = 1;
|
||||
lean_inc(x_8);
|
||||
lean_inc(x_7);
|
||||
lean_inc(x_6);
|
||||
lean_inc(x_5);
|
||||
lean_inc(x_4);
|
||||
lean_inc(x_3);
|
||||
x_23 = l_Lean_Elab_Term_elabTerm(x_20, x_21, x_22, x_3, x_4, x_5, x_6, x_7, x_8, x_18);
|
||||
if (lean_obj_tag(x_23) == 0)
|
||||
{
|
||||
lean_object* x_24; lean_object* x_25; lean_object* x_26; uint8_t x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36;
|
||||
x_24 = lean_ctor_get(x_23, 0);
|
||||
lean_inc(x_24);
|
||||
x_25 = lean_ctor_get(x_23, 1);
|
||||
lean_inc(x_25);
|
||||
lean_dec(x_23);
|
||||
x_26 = l_Lean_Elab_Term_elabStateRefT___closed__2;
|
||||
x_27 = 0;
|
||||
x_28 = lean_box(0);
|
||||
lean_inc(x_5);
|
||||
x_29 = l___private_Lean_Meta_Basic_0__Lean_Meta_mkFreshExprMVarImpl(x_26, x_27, x_28, x_5, x_6, x_7, x_8, x_25);
|
||||
x_30 = lean_ctor_get(x_29, 0);
|
||||
lean_inc(x_30);
|
||||
x_31 = lean_ctor_get(x_29, 1);
|
||||
lean_inc(x_31);
|
||||
lean_dec(x_29);
|
||||
x_32 = l_Lean_mkAppStx___closed__9;
|
||||
lean_inc(x_30);
|
||||
x_33 = lean_array_push(x_32, x_30);
|
||||
lean_inc(x_24);
|
||||
x_34 = lean_array_push(x_33, x_24);
|
||||
x_35 = l_Lean_Elab_Term_elabStateRefT___closed__4;
|
||||
lean_inc(x_8);
|
||||
lean_inc(x_7);
|
||||
lean_inc(x_6);
|
||||
lean_inc(x_5);
|
||||
x_36 = l_Lean_Meta_mkAppM___at___private_Lean_Elab_Term_0__Lean_Elab_Term_isMonad_x3f___spec__1(x_35, x_34, x_3, x_4, x_5, x_6, x_7, x_8, x_31);
|
||||
if (lean_obj_tag(x_36) == 0)
|
||||
{
|
||||
lean_object* x_37; lean_object* x_38; lean_object* x_39;
|
||||
x_37 = lean_ctor_get(x_36, 0);
|
||||
lean_inc(x_37);
|
||||
x_38 = lean_ctor_get(x_36, 1);
|
||||
lean_inc(x_38);
|
||||
lean_dec(x_36);
|
||||
lean_inc(x_8);
|
||||
lean_inc(x_7);
|
||||
lean_inc(x_6);
|
||||
lean_inc(x_5);
|
||||
lean_inc(x_4);
|
||||
lean_inc(x_3);
|
||||
x_39 = l_Lean_Elab_Term_mkInstMVar(x_37, x_3, x_4, x_5, x_6, x_7, x_8, x_38);
|
||||
if (lean_obj_tag(x_39) == 0)
|
||||
{
|
||||
lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46;
|
||||
x_40 = lean_ctor_get(x_39, 1);
|
||||
lean_inc(x_40);
|
||||
lean_dec(x_39);
|
||||
x_41 = l___private_Lean_Elab_Term_0__Lean_Elab_Term_tryCoe___closed__3;
|
||||
x_42 = lean_array_push(x_41, x_30);
|
||||
x_43 = lean_array_push(x_42, x_13);
|
||||
x_44 = lean_array_push(x_43, x_24);
|
||||
x_45 = l_Lean_Elab_Term_elabStateRefT___closed__6;
|
||||
x_46 = l_Lean_Meta_mkAppM___at___private_Lean_Elab_Term_0__Lean_Elab_Term_isMonad_x3f___spec__1(x_45, x_44, x_3, x_4, x_5, x_6, x_7, x_8, x_40);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_3);
|
||||
return x_46;
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_47;
|
||||
lean_dec(x_30);
|
||||
lean_dec(x_24);
|
||||
lean_dec(x_13);
|
||||
lean_dec(x_8);
|
||||
lean_dec(x_7);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_3);
|
||||
x_47 = !lean_is_exclusive(x_39);
|
||||
if (x_47 == 0)
|
||||
{
|
||||
return x_39;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_48; lean_object* x_49; lean_object* x_50;
|
||||
x_48 = lean_ctor_get(x_39, 0);
|
||||
x_49 = lean_ctor_get(x_39, 1);
|
||||
lean_inc(x_49);
|
||||
lean_inc(x_48);
|
||||
lean_dec(x_39);
|
||||
x_50 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_50, 0, x_48);
|
||||
lean_ctor_set(x_50, 1, x_49);
|
||||
return x_50;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_51;
|
||||
lean_dec(x_30);
|
||||
lean_dec(x_24);
|
||||
lean_dec(x_13);
|
||||
lean_dec(x_8);
|
||||
lean_dec(x_7);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_3);
|
||||
x_51 = !lean_is_exclusive(x_36);
|
||||
if (x_51 == 0)
|
||||
{
|
||||
return x_36;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_52; lean_object* x_53; lean_object* x_54;
|
||||
x_52 = lean_ctor_get(x_36, 0);
|
||||
x_53 = lean_ctor_get(x_36, 1);
|
||||
lean_inc(x_53);
|
||||
lean_inc(x_52);
|
||||
lean_dec(x_36);
|
||||
x_54 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_54, 0, x_52);
|
||||
lean_ctor_set(x_54, 1, x_53);
|
||||
return x_54;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_55;
|
||||
lean_dec(x_13);
|
||||
lean_dec(x_8);
|
||||
lean_dec(x_7);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_3);
|
||||
x_55 = !lean_is_exclusive(x_23);
|
||||
if (x_55 == 0)
|
||||
{
|
||||
return x_23;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_56; lean_object* x_57; lean_object* x_58;
|
||||
x_56 = lean_ctor_get(x_23, 0);
|
||||
x_57 = lean_ctor_get(x_23, 1);
|
||||
lean_inc(x_57);
|
||||
lean_inc(x_56);
|
||||
lean_dec(x_23);
|
||||
x_58 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_58, 0, x_56);
|
||||
lean_ctor_set(x_58, 1, x_57);
|
||||
return x_58;
|
||||
}
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_59;
|
||||
lean_dec(x_8);
|
||||
lean_dec(x_7);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_3);
|
||||
x_59 = !lean_is_exclusive(x_12);
|
||||
if (x_59 == 0)
|
||||
{
|
||||
return x_12;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_60; lean_object* x_61; lean_object* x_62;
|
||||
x_60 = lean_ctor_get(x_12, 0);
|
||||
x_61 = lean_ctor_get(x_12, 1);
|
||||
lean_inc(x_61);
|
||||
lean_inc(x_60);
|
||||
lean_dec(x_12);
|
||||
x_62 = lean_alloc_ctor(1, 2, 0);
|
||||
lean_ctor_set(x_62, 0, x_60);
|
||||
lean_ctor_set(x_62, 1, x_61);
|
||||
return x_62;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Meta_mkArrow___at_Lean_Elab_Term_elabStateRefT___spec__1___boxed(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, lean_object* x_9) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_10;
|
||||
x_10 = l_Lean_Meta_mkArrow___at_Lean_Elab_Term_elabStateRefT___spec__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
|
||||
lean_dec(x_8);
|
||||
lean_dec(x_7);
|
||||
lean_dec(x_6);
|
||||
lean_dec(x_5);
|
||||
lean_dec(x_4);
|
||||
lean_dec(x_3);
|
||||
return x_10;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Elab_Term_elabStateRefT___boxed(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, lean_object* x_9) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_10;
|
||||
x_10 = l_Lean_Elab_Term_elabStateRefT(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
|
||||
lean_dec(x_2);
|
||||
lean_dec(x_1);
|
||||
return x_10;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("stateRefT");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_mkAppStx___closed__6;
|
||||
x_2 = l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__1;
|
||||
x_3 = lean_name_mk_string(x_1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
static lean_object* _init_l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__3() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabStateRefT___boxed), 9, 0);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* l___regBuiltin_Lean_Elab_Term_elabStateRefT(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_Elab_Term_termElabAttribute;
|
||||
x_3 = l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__2;
|
||||
x_4 = l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__3;
|
||||
x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* initialize_Init(lean_object*);
|
||||
lean_object* initialize_Init_Data_ToString(lean_object*);
|
||||
lean_object* initialize_Lean_Compiler_BorrowedAnnotation(lean_object*);
|
||||
|
|
@ -16951,6 +17345,27 @@ lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabSubst___closed__1);
|
|||
res = l___regBuiltin_Lean_Elab_Term_elabSubst(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
l_Lean_Elab_Term_elabStateRefT___closed__1 = _init_l_Lean_Elab_Term_elabStateRefT___closed__1();
|
||||
lean_mark_persistent(l_Lean_Elab_Term_elabStateRefT___closed__1);
|
||||
l_Lean_Elab_Term_elabStateRefT___closed__2 = _init_l_Lean_Elab_Term_elabStateRefT___closed__2();
|
||||
lean_mark_persistent(l_Lean_Elab_Term_elabStateRefT___closed__2);
|
||||
l_Lean_Elab_Term_elabStateRefT___closed__3 = _init_l_Lean_Elab_Term_elabStateRefT___closed__3();
|
||||
lean_mark_persistent(l_Lean_Elab_Term_elabStateRefT___closed__3);
|
||||
l_Lean_Elab_Term_elabStateRefT___closed__4 = _init_l_Lean_Elab_Term_elabStateRefT___closed__4();
|
||||
lean_mark_persistent(l_Lean_Elab_Term_elabStateRefT___closed__4);
|
||||
l_Lean_Elab_Term_elabStateRefT___closed__5 = _init_l_Lean_Elab_Term_elabStateRefT___closed__5();
|
||||
lean_mark_persistent(l_Lean_Elab_Term_elabStateRefT___closed__5);
|
||||
l_Lean_Elab_Term_elabStateRefT___closed__6 = _init_l_Lean_Elab_Term_elabStateRefT___closed__6();
|
||||
lean_mark_persistent(l_Lean_Elab_Term_elabStateRefT___closed__6);
|
||||
l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__1 = _init_l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__1();
|
||||
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__1);
|
||||
l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__2 = _init_l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__2();
|
||||
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__2);
|
||||
l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__3 = _init_l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__3();
|
||||
lean_mark_persistent(l___regBuiltin_Lean_Elab_Term_elabStateRefT___closed__3);
|
||||
res = l___regBuiltin_Lean_Elab_Term_elabStateRefT(lean_io_mk_world());
|
||||
if (lean_io_result_is_error(res)) return res;
|
||||
lean_dec_ref(res);
|
||||
return lean_io_result_mk_ok(lean_box(0));
|
||||
}
|
||||
#ifdef __cplusplus
|
||||
|
|
|
|||
2
stage0/stdlib/Lean/Parser/Term.c
generated
2
stage0/stdlib/Lean/Parser/Term.c
generated
|
|
@ -52916,7 +52916,7 @@ static lean_object* _init_l_Lean_Parser_Term_stateRefT___elambda__1___closed__5(
|
|||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("StateRefTNew");
|
||||
x_1 = lean_mk_string("StateRefT");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue