chore: update stage0
This commit is contained in:
parent
ed7edf5661
commit
efd3e0c928
8 changed files with 487 additions and 96 deletions
32
stage0/src/Lean/Parser/Basic.lean
generated
32
stage0/src/Lean/Parser/Basic.lean
generated
|
|
@ -120,9 +120,10 @@ instance InputContext.inhabited : Inhabited InputContext :=
|
|||
⟨{ input := "", fileName := "", fileMap := arbitrary _ }⟩
|
||||
|
||||
structure ParserContext extends InputContext :=
|
||||
(prec : Nat)
|
||||
(env : Environment)
|
||||
(tokens : TokenTable)
|
||||
(prec : Nat)
|
||||
(env : Environment)
|
||||
(tokens : TokenTable)
|
||||
(insideQuot : Bool := false)
|
||||
|
||||
structure Error :=
|
||||
(unexpected : String := "")
|
||||
|
|
@ -360,6 +361,31 @@ fun c s =>
|
|||
{ info := epsilonInfo,
|
||||
fn := checkPrecFn prec }
|
||||
|
||||
def checkInsideQuotFn : ParserFn :=
|
||||
fun c s =>
|
||||
if c.insideQuot then s
|
||||
else s.mkUnexpectedError "unexpected syntax outside syntax quotation"
|
||||
|
||||
@[inline] def checkInsideQuot : Parser :=
|
||||
{ info := epsilonInfo,
|
||||
fn := checkInsideQuotFn }
|
||||
|
||||
def checkOutsideQuotFn : ParserFn :=
|
||||
fun c s =>
|
||||
if !c.insideQuot then s
|
||||
else s.mkUnexpectedError "unexpected syntax inside syntax quotation"
|
||||
|
||||
@[inline] def checkOutsideQuot : Parser :=
|
||||
{ info := epsilonInfo,
|
||||
fn := checkOutsideQuotFn }
|
||||
|
||||
def toggleInsideQuotFn (p : ParserFn) : ParserFn :=
|
||||
fun c s => p { c with insideQuot := !c.insideQuot } s
|
||||
|
||||
@[inline] def toggleInsideQuot (p : Parser) : Parser :=
|
||||
{ info := epsilonInfo,
|
||||
fn := toggleInsideQuotFn p.fn }
|
||||
|
||||
@[inline] def leadingNode (n : SyntaxNodeKind) (prec : Nat) (p : Parser) : Parser :=
|
||||
checkPrec prec >> node n p
|
||||
|
||||
|
|
|
|||
6
stage0/src/Lean/PrettyPrinter/Parenthesizer.lean
generated
6
stage0/src/Lean/PrettyPrinter/Parenthesizer.lean
generated
|
|
@ -406,12 +406,18 @@ p ⟨0, 0⟩
|
|||
def setExpected.parenthesizer (expected : List String) (p : Parenthesizer) : Parenthesizer :=
|
||||
p
|
||||
|
||||
@[combinatorParenthesizer Lean.Parser.toggleInsideQuot]
|
||||
def toggleInsideQuot.parenthesizer (p : Parenthesizer) : Parenthesizer :=
|
||||
p
|
||||
|
||||
@[combinatorParenthesizer Lean.Parser.checkStackTop] def checkStackTop.parenthesizer : Parenthesizer := pure ()
|
||||
@[combinatorParenthesizer Lean.Parser.checkWsBefore] def checkWsBefore.parenthesizer : Parenthesizer := pure ()
|
||||
@[combinatorParenthesizer Lean.Parser.checkNoWsBefore] def checkNoWsBefore.parenthesizer : Parenthesizer := pure ()
|
||||
@[combinatorParenthesizer Lean.Parser.checkTailWs] def checkTailWs.parenthesizer : Parenthesizer := pure ()
|
||||
@[combinatorParenthesizer Lean.Parser.checkColGe] def checkColGe.parenthesizer : Parenthesizer := pure ()
|
||||
@[combinatorParenthesizer Lean.Parser.checkNoImmediateColon] def checkNoImmediateColon.parenthesizer : Parenthesizer := pure ()
|
||||
@[combinatorParenthesizer Lean.Parser.checkInsideQuot] def checkInsideQuot.parenthesizer : Parenthesizer := pure ()
|
||||
@[combinatorParenthesizer Lean.Parser.checkOutsideQuot] def checkOutsideQuot.parenthesizer : Parenthesizer := pure ()
|
||||
|
||||
@[combinatorParenthesizer Lean.Parser.pushNone] def pushNone.parenthesizer : Parenthesizer := goLeft
|
||||
|
||||
|
|
|
|||
64
stage0/stdlib/Lean/Elab/Quotation.c
generated
64
stage0/stdlib/Lean/Elab/Quotation.c
generated
|
|
@ -26185,7 +26185,7 @@ return x_1;
|
|||
lean_object* lean_parse_expr(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;
|
||||
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; uint8_t x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14;
|
||||
x_4 = l_Lean_Elab_Term_Quotation_oldParseExpr___closed__1;
|
||||
lean_inc(x_2);
|
||||
x_5 = l_Lean_Parser_mkInputContext(x_2, x_4);
|
||||
|
|
@ -26194,43 +26194,45 @@ lean_dec(x_2);
|
|||
x_7 = l_Lean_Parser_ParserState_setPos(x_6, x_3);
|
||||
x_8 = l_Lean_Parser_getTokenTable(x_1);
|
||||
x_9 = l_Lean_Parser_maxPrec;
|
||||
x_10 = lean_alloc_ctor(0, 4, 0);
|
||||
lean_ctor_set(x_10, 0, x_5);
|
||||
lean_ctor_set(x_10, 1, x_9);
|
||||
lean_ctor_set(x_10, 2, x_1);
|
||||
lean_ctor_set(x_10, 3, x_8);
|
||||
x_11 = l_Lean_Parser_termParser___closed__2;
|
||||
x_12 = l_Lean_Parser_categoryParser___elambda__1(x_11, x_9, x_10, x_7);
|
||||
x_13 = lean_ctor_get(x_12, 3);
|
||||
lean_inc(x_13);
|
||||
if (lean_obj_tag(x_13) == 0)
|
||||
{
|
||||
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18;
|
||||
x_14 = lean_ctor_get(x_12, 0);
|
||||
x_10 = 0;
|
||||
x_11 = lean_alloc_ctor(0, 4, 1);
|
||||
lean_ctor_set(x_11, 0, x_5);
|
||||
lean_ctor_set(x_11, 1, x_9);
|
||||
lean_ctor_set(x_11, 2, x_1);
|
||||
lean_ctor_set(x_11, 3, x_8);
|
||||
lean_ctor_set_uint8(x_11, sizeof(void*)*4, x_10);
|
||||
x_12 = l_Lean_Parser_termParser___closed__2;
|
||||
x_13 = l_Lean_Parser_categoryParser___elambda__1(x_12, x_9, x_11, x_7);
|
||||
x_14 = lean_ctor_get(x_13, 3);
|
||||
lean_inc(x_14);
|
||||
x_15 = lean_ctor_get(x_12, 1);
|
||||
if (lean_obj_tag(x_14) == 0)
|
||||
{
|
||||
lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19;
|
||||
x_15 = lean_ctor_get(x_13, 0);
|
||||
lean_inc(x_15);
|
||||
lean_dec(x_12);
|
||||
x_16 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_14);
|
||||
lean_dec(x_14);
|
||||
x_17 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_17, 0, x_16);
|
||||
lean_ctor_set(x_17, 1, x_15);
|
||||
x_18 = lean_alloc_ctor(1, 1, 0);
|
||||
x_16 = lean_ctor_get(x_13, 1);
|
||||
lean_inc(x_16);
|
||||
lean_dec(x_13);
|
||||
x_17 = l_Array_back___at_Lean_Syntax_Traverser_up___spec__2(x_15);
|
||||
lean_dec(x_15);
|
||||
x_18 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_18, 0, x_17);
|
||||
return x_18;
|
||||
lean_ctor_set(x_18, 1, x_16);
|
||||
x_19 = lean_alloc_ctor(1, 1, 0);
|
||||
lean_ctor_set(x_19, 0, x_18);
|
||||
return x_19;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_19; lean_object* x_20; lean_object* x_21;
|
||||
lean_dec(x_12);
|
||||
x_19 = lean_ctor_get(x_13, 0);
|
||||
lean_inc(x_19);
|
||||
lean_object* x_20; lean_object* x_21; lean_object* x_22;
|
||||
lean_dec(x_13);
|
||||
x_20 = l_Lean_Parser_Error_toString(x_19);
|
||||
x_21 = lean_alloc_ctor(0, 1, 0);
|
||||
lean_ctor_set(x_21, 0, x_20);
|
||||
return x_21;
|
||||
x_20 = lean_ctor_get(x_14, 0);
|
||||
lean_inc(x_20);
|
||||
lean_dec(x_14);
|
||||
x_21 = l_Lean_Parser_Error_toString(x_20);
|
||||
x_22 = lean_alloc_ctor(0, 1, 0);
|
||||
lean_ctor_set(x_22, 0, x_21);
|
||||
return x_22;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
285
stage0/stdlib/Lean/Parser/Basic.c
generated
285
stage0/stdlib/Lean/Parser/Basic.c
generated
|
|
@ -71,6 +71,7 @@ lean_object* l_Lean_Parser_optionaInfo___elambda__2(lean_object*, lean_object*);
|
|||
lean_object* l_Lean_Parser_ParserFn_inhabited___rarg(lean_object*);
|
||||
lean_object* l_Lean_Parser_binNumberFn___closed__1;
|
||||
lean_object* l_Lean_Parser_hexNumberFn___closed__1;
|
||||
lean_object* l_Lean_Parser_checkInsideQuotFn(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_foldSepRevArgs(lean_object*);
|
||||
lean_object* l_Lean_Parser_binNumberFn___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_numberFnAux(lean_object*, lean_object*);
|
||||
|
|
@ -270,6 +271,7 @@ lean_object* l_Lean_Parser_takeWhileFn(lean_object*, lean_object*, lean_object*)
|
|||
lean_object* l_Lean_Parser_numLit___closed__2;
|
||||
lean_object* l_Array_foldlStepMAux___main___at_Lean_Syntax_foldSepArgsM___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_nonReservedSymbolInfo___elambda__2(lean_object*);
|
||||
lean_object* l_Lean_Parser_checkOutsideQuot___closed__1;
|
||||
lean_object* l_Lean_Parser_initCacheForInput(lean_object*);
|
||||
lean_object* l_Lean_Parser_satisfyFn___at_Lean_Parser_identFnAux___main___spec__4(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_antiquotNestedExpr___elambda__1___closed__4;
|
||||
|
|
@ -398,6 +400,7 @@ lean_object* l_Lean_Parser_Error_HasBeq;
|
|||
lean_object* l_Lean_Parser_nonReservedSymbolInfo___closed__3;
|
||||
lean_object* l_Lean_Parser_Error_Inhabited___closed__1;
|
||||
lean_object* l_Lean_Parser_ParserState_shrinkStack(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_checkOutsideQuot___closed__2;
|
||||
uint8_t l_Lean_Parser_checkTailNoWs(lean_object*);
|
||||
lean_object* l_Lean_Parser_checkTailWs___boxed(lean_object*);
|
||||
lean_object* l_Lean_Parser_charLitFn(lean_object*, lean_object*);
|
||||
|
|
@ -493,6 +496,7 @@ lean_object* l_Lean_Parser_checkTailNoWs___boxed(lean_object*);
|
|||
lean_object* l_Lean_Parser_takeUntilFn(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_symbolNoWsInfo(lean_object*);
|
||||
lean_object* l_Lean_Parser_epsilonInfo___elambda__1___boxed(lean_object*);
|
||||
lean_object* l_Lean_Parser_checkOutsideQuot;
|
||||
lean_object* l_Lean_FileMap_toPosition(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_mkAtomicInfo___elambda__1(lean_object*);
|
||||
lean_object* l_Lean_Parser_anyOfFn(lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -500,11 +504,13 @@ lean_object* l_Lean_Parser_mkEmptySubstringAt(lean_object*, lean_object*);
|
|||
lean_object* l_Lean_Parser_takeWhileFn___at_Lean_Parser_binNumberFn___spec__2___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_strLitFnAux___main(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_Error_toString___closed__2;
|
||||
lean_object* l_Lean_Parser_checkInsideQuot;
|
||||
lean_object* l_Lean_Parser_nameLitNoAntiquot___closed__3;
|
||||
lean_object* l_Array_foldlStepMAux___main___at_Lean_Syntax_foldSepArgs___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_IO_Prim_Ref_get___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_longestMatchMkResult(lean_object*, lean_object*);
|
||||
size_t l_USize_mul(size_t, size_t);
|
||||
lean_object* l_Lean_Parser_toggleInsideQuot(lean_object*);
|
||||
lean_object* l_Lean_Parser_whitespace(lean_object*, lean_object*);
|
||||
lean_object* l_List_redLength___main___rarg(lean_object*);
|
||||
lean_object* l_Lean_Parser_rawCh(uint32_t, uint8_t);
|
||||
|
|
@ -523,6 +529,7 @@ lean_object* l_Lean_Parser_termParser(lean_object*);
|
|||
lean_object* l_Lean_Parser_sepByFn___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_FirstTokens_toStr___closed__3;
|
||||
lean_object* l_Lean_Parser_manyAux(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_checkInsideQuotFn___closed__1;
|
||||
lean_object* l_Lean_Parser_mkAntiquot___closed__7;
|
||||
uint8_t l_List_beq___main___at_Lean_Syntax_structEq___main___spec__3(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_pushNone___closed__1;
|
||||
|
|
@ -541,8 +548,10 @@ lean_object* l_Lean_Parser_rawIdentNoAntiquot___closed__2;
|
|||
size_t l_USize_land(size_t, size_t);
|
||||
lean_object* l_Lean_Parser_nameLit___elambda__1___closed__1;
|
||||
lean_object* l_Lean_Parser_mkAntiquot___elambda__2(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_checkOutsideQuotFn(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_categoryParserFn(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_foldlStepMAux___main___at_Array_foldSepByM___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_checkInsideQuot___closed__1;
|
||||
extern lean_object* l___private_Lean_Environment_5__envExtensionsRef;
|
||||
lean_object* l_Lean_Parser_mkCategoryParserFnExtension___closed__1;
|
||||
lean_object* l_Lean_Parser_sepBy1Info(lean_object*, lean_object*);
|
||||
|
|
@ -550,12 +559,14 @@ lean_object* l_Lean_Parser_quotedCharFn___closed__1;
|
|||
lean_object* l_Lean_Parser_charLitFnAux___closed__1;
|
||||
lean_object* l_Lean_Parser_symbolNoWs(lean_object*);
|
||||
lean_object* l_Lean_Parser_hexDigitFn___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_checkInsideQuotFn___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_ParserState_mergeErrors___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_foldSepBy(lean_object*);
|
||||
lean_object* l_Lean_Parser_categoryParserFnExtension___elambda__2(lean_object*);
|
||||
lean_object* l_Lean_Parser_trailingNode(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_mkAtomFrom(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_orelseInfo___elambda__2(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_checkInsideQuot___closed__2;
|
||||
lean_object* l_Lean_Parser_pushNone___closed__2;
|
||||
lean_object* l_Lean_Parser_quotedCharFn___boxed(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_sepBy1(lean_object*, lean_object*, uint8_t, uint8_t);
|
||||
|
|
@ -581,6 +592,7 @@ lean_object* l_Lean_Parser_symbol___boxed(lean_object*);
|
|||
lean_object* l_Array_iterateMAux___main___at_Lean_Syntax_foldArgs___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_charLit___elambda__1(lean_object*, lean_object*);
|
||||
uint8_t l_UInt32_decEq(uint32_t, uint32_t);
|
||||
lean_object* l_Lean_Parser_toggleInsideQuotFn(lean_object*, lean_object*, lean_object*);
|
||||
extern lean_object* l_Lean_Syntax_inhabited;
|
||||
lean_object* l_Lean_Parser_unquotedSymbolFn(lean_object*, lean_object*);
|
||||
lean_object* l_String_intercalate(lean_object*, lean_object*);
|
||||
|
|
@ -723,7 +735,9 @@ lean_object* l_Array_toList___rarg(lean_object*);
|
|||
lean_object* l_Lean_Parser_checkWsBeforeFn___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_optionalFn(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_nameLitFn___closed__1;
|
||||
lean_object* l_Lean_Parser_checkOutsideQuotFn___closed__1;
|
||||
lean_object* l_Std_PersistentHashMap_insertAux___main___at_Lean_Parser_SyntaxNodeKindSet_insert___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Parser_checkOutsideQuotFn___boxed(lean_object*, lean_object*);
|
||||
lean_object* lean_array_pop(lean_object*);
|
||||
lean_object* l_Lean_Parser_TokenMap_insert___rarg(lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_Lean_isIdFirst(uint32_t);
|
||||
|
|
@ -3969,6 +3983,225 @@ lean_ctor_set(x_4, 1, x_2);
|
|||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_checkInsideQuotFn___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("unexpected syntax outside syntax quotation");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_checkInsideQuotFn(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_3;
|
||||
x_3 = lean_ctor_get_uint8(x_1, sizeof(void*)*4);
|
||||
if (x_3 == 0)
|
||||
{
|
||||
lean_object* x_4; lean_object* x_5;
|
||||
x_4 = l_Lean_Parser_checkInsideQuotFn___closed__1;
|
||||
x_5 = l_Lean_Parser_ParserState_mkUnexpectedError(x_2, x_4);
|
||||
return x_5;
|
||||
}
|
||||
else
|
||||
{
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_checkInsideQuotFn___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l_Lean_Parser_checkInsideQuotFn(x_1, x_2);
|
||||
lean_dec(x_1);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_checkInsideQuot___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_checkInsideQuotFn___boxed), 2, 0);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_checkInsideQuot___closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_epsilonInfo;
|
||||
x_2 = l_Lean_Parser_checkInsideQuot___closed__1;
|
||||
x_3 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
lean_ctor_set(x_3, 1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_checkInsideQuot() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = l_Lean_Parser_checkInsideQuot___closed__2;
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_checkOutsideQuotFn___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_mk_string("unexpected syntax inside syntax quotation");
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_checkOutsideQuotFn(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_3;
|
||||
x_3 = lean_ctor_get_uint8(x_1, sizeof(void*)*4);
|
||||
if (x_3 == 0)
|
||||
{
|
||||
return x_2;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_4; lean_object* x_5;
|
||||
x_4 = l_Lean_Parser_checkOutsideQuotFn___closed__1;
|
||||
x_5 = l_Lean_Parser_ParserState_mkUnexpectedError(x_2, x_4);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_checkOutsideQuotFn___boxed(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3;
|
||||
x_3 = l_Lean_Parser_checkOutsideQuotFn(x_1, x_2);
|
||||
lean_dec(x_1);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_checkOutsideQuot___closed__1() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_checkOutsideQuotFn___boxed), 2, 0);
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_checkOutsideQuot___closed__2() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1; lean_object* x_2; lean_object* x_3;
|
||||
x_1 = l_Lean_Parser_epsilonInfo;
|
||||
x_2 = l_Lean_Parser_checkOutsideQuot___closed__1;
|
||||
x_3 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_3, 0, x_1);
|
||||
lean_ctor_set(x_3, 1, x_2);
|
||||
return x_3;
|
||||
}
|
||||
}
|
||||
lean_object* _init_l_Lean_Parser_checkOutsideQuot() {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_1;
|
||||
x_1 = l_Lean_Parser_checkOutsideQuot___closed__2;
|
||||
return x_1;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_toggleInsideQuotFn(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
uint8_t x_4;
|
||||
x_4 = lean_ctor_get_uint8(x_2, sizeof(void*)*4);
|
||||
if (x_4 == 0)
|
||||
{
|
||||
uint8_t x_5;
|
||||
x_5 = !lean_is_exclusive(x_2);
|
||||
if (x_5 == 0)
|
||||
{
|
||||
uint8_t x_6; lean_object* x_7;
|
||||
x_6 = 1;
|
||||
lean_ctor_set_uint8(x_2, sizeof(void*)*4, x_6);
|
||||
x_7 = lean_apply_2(x_1, x_2, x_3);
|
||||
return x_7;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; uint8_t x_12; lean_object* x_13; lean_object* x_14;
|
||||
x_8 = lean_ctor_get(x_2, 0);
|
||||
x_9 = lean_ctor_get(x_2, 1);
|
||||
x_10 = lean_ctor_get(x_2, 2);
|
||||
x_11 = lean_ctor_get(x_2, 3);
|
||||
lean_inc(x_11);
|
||||
lean_inc(x_10);
|
||||
lean_inc(x_9);
|
||||
lean_inc(x_8);
|
||||
lean_dec(x_2);
|
||||
x_12 = 1;
|
||||
x_13 = lean_alloc_ctor(0, 4, 1);
|
||||
lean_ctor_set(x_13, 0, x_8);
|
||||
lean_ctor_set(x_13, 1, x_9);
|
||||
lean_ctor_set(x_13, 2, x_10);
|
||||
lean_ctor_set(x_13, 3, x_11);
|
||||
lean_ctor_set_uint8(x_13, sizeof(void*)*4, x_12);
|
||||
x_14 = lean_apply_2(x_1, x_13, x_3);
|
||||
return x_14;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
uint8_t x_15;
|
||||
x_15 = !lean_is_exclusive(x_2);
|
||||
if (x_15 == 0)
|
||||
{
|
||||
uint8_t x_16; lean_object* x_17;
|
||||
x_16 = 0;
|
||||
lean_ctor_set_uint8(x_2, sizeof(void*)*4, x_16);
|
||||
x_17 = lean_apply_2(x_1, x_2, x_3);
|
||||
return x_17;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; uint8_t x_22; lean_object* x_23; lean_object* x_24;
|
||||
x_18 = lean_ctor_get(x_2, 0);
|
||||
x_19 = lean_ctor_get(x_2, 1);
|
||||
x_20 = lean_ctor_get(x_2, 2);
|
||||
x_21 = lean_ctor_get(x_2, 3);
|
||||
lean_inc(x_21);
|
||||
lean_inc(x_20);
|
||||
lean_inc(x_19);
|
||||
lean_inc(x_18);
|
||||
lean_dec(x_2);
|
||||
x_22 = 0;
|
||||
x_23 = lean_alloc_ctor(0, 4, 1);
|
||||
lean_ctor_set(x_23, 0, x_18);
|
||||
lean_ctor_set(x_23, 1, x_19);
|
||||
lean_ctor_set(x_23, 2, x_20);
|
||||
lean_ctor_set(x_23, 3, x_21);
|
||||
lean_ctor_set_uint8(x_23, sizeof(void*)*4, x_22);
|
||||
x_24 = lean_apply_2(x_1, x_23, x_3);
|
||||
return x_24;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_toggleInsideQuot(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
x_2 = lean_ctor_get(x_1, 1);
|
||||
lean_inc(x_2);
|
||||
lean_dec(x_1);
|
||||
x_3 = lean_alloc_closure((void*)(l_Lean_Parser_toggleInsideQuotFn), 3, 1);
|
||||
lean_closure_set(x_3, 0, x_2);
|
||||
x_4 = l_Lean_Parser_epsilonInfo;
|
||||
x_5 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_5, 0, x_4);
|
||||
lean_ctor_set(x_5, 1, x_3);
|
||||
return x_5;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_leadingNode(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -23569,21 +23802,23 @@ return x_7;
|
|||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
|
||||
lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11; lean_object* x_12; lean_object* x_13;
|
||||
x_8 = lean_ctor_get(x_3, 0);
|
||||
x_9 = lean_ctor_get(x_3, 2);
|
||||
x_10 = lean_ctor_get(x_3, 3);
|
||||
x_11 = lean_ctor_get_uint8(x_3, sizeof(void*)*4);
|
||||
lean_inc(x_10);
|
||||
lean_inc(x_9);
|
||||
lean_inc(x_8);
|
||||
lean_dec(x_3);
|
||||
x_11 = lean_alloc_ctor(0, 4, 0);
|
||||
lean_ctor_set(x_11, 0, x_8);
|
||||
lean_ctor_set(x_11, 1, x_2);
|
||||
lean_ctor_set(x_11, 2, x_9);
|
||||
lean_ctor_set(x_11, 3, x_10);
|
||||
x_12 = l_Lean_Parser_categoryParserFn(x_1, x_11, x_4);
|
||||
return x_12;
|
||||
x_12 = lean_alloc_ctor(0, 4, 1);
|
||||
lean_ctor_set(x_12, 0, x_8);
|
||||
lean_ctor_set(x_12, 1, x_2);
|
||||
lean_ctor_set(x_12, 2, x_9);
|
||||
lean_ctor_set(x_12, 3, x_10);
|
||||
lean_ctor_set_uint8(x_12, sizeof(void*)*4, x_11);
|
||||
x_13 = l_Lean_Parser_categoryParserFn(x_1, x_12, x_4);
|
||||
return x_13;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -26187,21 +26422,23 @@ return x_7;
|
|||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
|
||||
lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11; lean_object* x_12; lean_object* x_13;
|
||||
x_8 = lean_ctor_get(x_3, 0);
|
||||
x_9 = lean_ctor_get(x_3, 2);
|
||||
x_10 = lean_ctor_get(x_3, 3);
|
||||
x_11 = lean_ctor_get_uint8(x_3, sizeof(void*)*4);
|
||||
lean_inc(x_10);
|
||||
lean_inc(x_9);
|
||||
lean_inc(x_8);
|
||||
lean_dec(x_3);
|
||||
x_11 = lean_alloc_ctor(0, 4, 0);
|
||||
lean_ctor_set(x_11, 0, x_8);
|
||||
lean_ctor_set(x_11, 1, x_2);
|
||||
lean_ctor_set(x_11, 2, x_9);
|
||||
lean_ctor_set(x_11, 3, x_10);
|
||||
x_12 = l_Lean_Parser_categoryParserOfStackFn(x_1, x_11, x_4);
|
||||
return x_12;
|
||||
x_12 = lean_alloc_ctor(0, 4, 1);
|
||||
lean_ctor_set(x_12, 0, x_8);
|
||||
lean_ctor_set(x_12, 1, x_2);
|
||||
lean_ctor_set(x_12, 2, x_9);
|
||||
lean_ctor_set(x_12, 3, x_10);
|
||||
lean_ctor_set_uint8(x_12, sizeof(void*)*4, x_11);
|
||||
x_13 = l_Lean_Parser_categoryParserOfStackFn(x_1, x_12, x_4);
|
||||
return x_13;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -27778,6 +28015,22 @@ l_Lean_Parser_hasAndthen = _init_l_Lean_Parser_hasAndthen();
|
|||
lean_mark_persistent(l_Lean_Parser_hasAndthen);
|
||||
l_Lean_Parser_checkPrecFn___closed__1 = _init_l_Lean_Parser_checkPrecFn___closed__1();
|
||||
lean_mark_persistent(l_Lean_Parser_checkPrecFn___closed__1);
|
||||
l_Lean_Parser_checkInsideQuotFn___closed__1 = _init_l_Lean_Parser_checkInsideQuotFn___closed__1();
|
||||
lean_mark_persistent(l_Lean_Parser_checkInsideQuotFn___closed__1);
|
||||
l_Lean_Parser_checkInsideQuot___closed__1 = _init_l_Lean_Parser_checkInsideQuot___closed__1();
|
||||
lean_mark_persistent(l_Lean_Parser_checkInsideQuot___closed__1);
|
||||
l_Lean_Parser_checkInsideQuot___closed__2 = _init_l_Lean_Parser_checkInsideQuot___closed__2();
|
||||
lean_mark_persistent(l_Lean_Parser_checkInsideQuot___closed__2);
|
||||
l_Lean_Parser_checkInsideQuot = _init_l_Lean_Parser_checkInsideQuot();
|
||||
lean_mark_persistent(l_Lean_Parser_checkInsideQuot);
|
||||
l_Lean_Parser_checkOutsideQuotFn___closed__1 = _init_l_Lean_Parser_checkOutsideQuotFn___closed__1();
|
||||
lean_mark_persistent(l_Lean_Parser_checkOutsideQuotFn___closed__1);
|
||||
l_Lean_Parser_checkOutsideQuot___closed__1 = _init_l_Lean_Parser_checkOutsideQuot___closed__1();
|
||||
lean_mark_persistent(l_Lean_Parser_checkOutsideQuot___closed__1);
|
||||
l_Lean_Parser_checkOutsideQuot___closed__2 = _init_l_Lean_Parser_checkOutsideQuot___closed__2();
|
||||
lean_mark_persistent(l_Lean_Parser_checkOutsideQuot___closed__2);
|
||||
l_Lean_Parser_checkOutsideQuot = _init_l_Lean_Parser_checkOutsideQuot();
|
||||
lean_mark_persistent(l_Lean_Parser_checkOutsideQuot);
|
||||
l_Lean_Parser_hashOrelse___closed__1 = _init_l_Lean_Parser_hashOrelse___closed__1();
|
||||
lean_mark_persistent(l_Lean_Parser_hashOrelse___closed__1);
|
||||
l_Lean_Parser_hashOrelse = _init_l_Lean_Parser_hashOrelse();
|
||||
|
|
|
|||
16
stage0/stdlib/Lean/Parser/Extension.c
generated
16
stage0/stdlib/Lean/Parser/Extension.c
generated
|
|
@ -8074,15 +8074,17 @@ return x_4;
|
|||
lean_object* l_Lean_Parser_mkParserContext(lean_object* x_1, lean_object* x_2) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_3; lean_object* x_4; lean_object* x_5;
|
||||
lean_object* x_3; lean_object* x_4; uint8_t x_5; lean_object* x_6;
|
||||
x_3 = l_Lean_Parser_getTokenTable(x_1);
|
||||
x_4 = lean_unsigned_to_nat(0u);
|
||||
x_5 = lean_alloc_ctor(0, 4, 0);
|
||||
lean_ctor_set(x_5, 0, x_2);
|
||||
lean_ctor_set(x_5, 1, x_4);
|
||||
lean_ctor_set(x_5, 2, x_1);
|
||||
lean_ctor_set(x_5, 3, x_3);
|
||||
return x_5;
|
||||
x_5 = 0;
|
||||
x_6 = lean_alloc_ctor(0, 4, 1);
|
||||
lean_ctor_set(x_6, 0, x_2);
|
||||
lean_ctor_set(x_6, 1, x_4);
|
||||
lean_ctor_set(x_6, 2, x_1);
|
||||
lean_ctor_set(x_6, 3, x_3);
|
||||
lean_ctor_set_uint8(x_6, sizeof(void*)*4, x_5);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_Parser_mkParserState(lean_object* x_1) {
|
||||
|
|
|
|||
55
stage0/stdlib/Lean/Parser/Module.c
generated
55
stage0/stdlib/Lean/Parser/Module.c
generated
|
|
@ -1995,45 +1995,48 @@ return x_1;
|
|||
}
|
||||
else
|
||||
{
|
||||
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_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; uint8_t x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
|
||||
x_10 = lean_ctor_get(x_1, 0);
|
||||
x_11 = lean_ctor_get(x_1, 1);
|
||||
x_12 = lean_ctor_get(x_1, 2);
|
||||
x_13 = lean_ctor_get(x_1, 3);
|
||||
x_14 = lean_ctor_get_uint8(x_1, sizeof(void*)*4);
|
||||
lean_inc(x_13);
|
||||
lean_inc(x_12);
|
||||
lean_inc(x_11);
|
||||
lean_inc(x_10);
|
||||
lean_dec(x_1);
|
||||
x_14 = l_Lean_Parser_Module_header;
|
||||
x_15 = lean_ctor_get(x_14, 0);
|
||||
lean_inc(x_15);
|
||||
x_16 = l_Lean_Parser_addParserTokens(x_13, x_15);
|
||||
if (lean_obj_tag(x_16) == 0)
|
||||
x_15 = l_Lean_Parser_Module_header;
|
||||
x_16 = lean_ctor_get(x_15, 0);
|
||||
lean_inc(x_16);
|
||||
x_17 = l_Lean_Parser_addParserTokens(x_13, x_16);
|
||||
if (lean_obj_tag(x_17) == 0)
|
||||
{
|
||||
lean_object* x_17; lean_object* x_18; lean_object* x_19;
|
||||
lean_dec(x_16);
|
||||
x_17 = l_Lean_Parser_Module_updateTokens___closed__1;
|
||||
x_18 = l_unreachable_x21___rarg(x_17);
|
||||
x_19 = lean_alloc_ctor(0, 4, 0);
|
||||
lean_ctor_set(x_19, 0, x_10);
|
||||
lean_ctor_set(x_19, 1, x_11);
|
||||
lean_ctor_set(x_19, 2, x_12);
|
||||
lean_ctor_set(x_19, 3, x_18);
|
||||
return x_19;
|
||||
lean_object* x_18; lean_object* x_19; lean_object* x_20;
|
||||
lean_dec(x_17);
|
||||
x_18 = l_Lean_Parser_Module_updateTokens___closed__1;
|
||||
x_19 = l_unreachable_x21___rarg(x_18);
|
||||
x_20 = lean_alloc_ctor(0, 4, 1);
|
||||
lean_ctor_set(x_20, 0, x_10);
|
||||
lean_ctor_set(x_20, 1, x_11);
|
||||
lean_ctor_set(x_20, 2, x_12);
|
||||
lean_ctor_set(x_20, 3, x_19);
|
||||
lean_ctor_set_uint8(x_20, sizeof(void*)*4, x_14);
|
||||
return x_20;
|
||||
}
|
||||
else
|
||||
{
|
||||
lean_object* x_20; lean_object* x_21;
|
||||
x_20 = lean_ctor_get(x_16, 0);
|
||||
lean_inc(x_20);
|
||||
lean_dec(x_16);
|
||||
x_21 = lean_alloc_ctor(0, 4, 0);
|
||||
lean_ctor_set(x_21, 0, x_10);
|
||||
lean_ctor_set(x_21, 1, x_11);
|
||||
lean_ctor_set(x_21, 2, x_12);
|
||||
lean_ctor_set(x_21, 3, x_20);
|
||||
return x_21;
|
||||
lean_object* x_21; lean_object* x_22;
|
||||
x_21 = lean_ctor_get(x_17, 0);
|
||||
lean_inc(x_21);
|
||||
lean_dec(x_17);
|
||||
x_22 = lean_alloc_ctor(0, 4, 1);
|
||||
lean_ctor_set(x_22, 0, x_10);
|
||||
lean_ctor_set(x_22, 1, x_11);
|
||||
lean_ctor_set(x_22, 2, x_12);
|
||||
lean_ctor_set(x_22, 3, x_21);
|
||||
lean_ctor_set_uint8(x_22, sizeof(void*)*4, x_14);
|
||||
return x_22;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
28
stage0/stdlib/Lean/PrettyPrinter/Formatter.c
generated
28
stage0/stdlib/Lean/PrettyPrinter/Formatter.c
generated
|
|
@ -7359,7 +7359,7 @@ return x_5;
|
|||
lean_object* l_Lean_PrettyPrinter_Formatter_parseToken(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
|
||||
_start:
|
||||
{
|
||||
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_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16;
|
||||
x_6 = lean_ctor_get(x_5, 0);
|
||||
lean_inc(x_6);
|
||||
x_7 = l_String_splitAux___main___closed__1;
|
||||
|
|
@ -7370,21 +7370,23 @@ lean_ctor_set(x_9, 0, x_1);
|
|||
lean_ctor_set(x_9, 1, x_7);
|
||||
lean_ctor_set(x_9, 2, x_8);
|
||||
x_10 = lean_unsigned_to_nat(0u);
|
||||
x_11 = lean_alloc_ctor(0, 4, 0);
|
||||
lean_ctor_set(x_11, 0, x_9);
|
||||
lean_ctor_set(x_11, 1, x_10);
|
||||
lean_ctor_set(x_11, 2, x_6);
|
||||
lean_ctor_set(x_11, 3, x_2);
|
||||
x_12 = l_Lean_Parser_mkParserState(x_1);
|
||||
x_11 = 0;
|
||||
x_12 = lean_alloc_ctor(0, 4, 1);
|
||||
lean_ctor_set(x_12, 0, x_9);
|
||||
lean_ctor_set(x_12, 1, x_10);
|
||||
lean_ctor_set(x_12, 2, x_6);
|
||||
lean_ctor_set(x_12, 3, x_2);
|
||||
lean_ctor_set_uint8(x_12, sizeof(void*)*4, x_11);
|
||||
x_13 = l_Lean_Parser_mkParserState(x_1);
|
||||
lean_dec(x_1);
|
||||
x_13 = l_Lean_Parser_tokenFn(x_11, x_12);
|
||||
x_14 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_14, 0, x_13);
|
||||
lean_ctor_set(x_14, 1, x_3);
|
||||
x_14 = l_Lean_Parser_tokenFn(x_12, x_13);
|
||||
x_15 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_15, 0, x_14);
|
||||
lean_ctor_set(x_15, 1, x_5);
|
||||
return x_15;
|
||||
lean_ctor_set(x_15, 1, x_3);
|
||||
x_16 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_16, 0, x_15);
|
||||
lean_ctor_set(x_16, 1, x_5);
|
||||
return x_16;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_PrettyPrinter_Formatter_parseToken___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
|
||||
|
|
|
|||
97
stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c
generated
97
stage0/stdlib/Lean/PrettyPrinter/Parenthesizer.c
generated
|
|
@ -77,6 +77,7 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_trailingNode_parenthesizer___lam
|
|||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkStackTop_parenthesizer___boxed(lean_object*);
|
||||
lean_object* lean_expr_update_mdata(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_MonadTraverser_goRight___at_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___spec__4___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkOutsideQuot_parenthesizer___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_identNoAntiquot_parenthesizer___boxed(lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_compileParserBody___main___closed__8;
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__8;
|
||||
|
|
@ -165,8 +166,10 @@ lean_object* l_Array_iterateM_u2082Aux___main___at_Lean_PrettyPrinter_Parenthesi
|
|||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_tactic_parenthesizer___lambda__1___closed__2;
|
||||
lean_object* l_Lean_Meta_forallTelescope___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_List_range(lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_toggleInsideQuot_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_compileParserBody___main___closed__21;
|
||||
lean_object* l_Array_iterateM_u2082Aux___main___at_Lean_PrettyPrinter_Parenthesizer_compileParserBody___main___spec__13(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkOutsideQuot_parenthesizer___boxed(lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_mkCombinatorParenthesizerAttribute___closed__1;
|
||||
lean_object* l_Lean_PrettyPrinter_parenthesizeCommand(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Syntax_setTailInfo(lean_object*, lean_object*);
|
||||
|
|
@ -407,6 +410,7 @@ lean_object* l_Array_iterateM_u2082Aux___main___at_Lean_PrettyPrinter_Parenthesi
|
|||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__11;
|
||||
lean_object* l_Lean_Syntax_MonadTraverser_getCur___at_Lean_PrettyPrinter_Parenthesizer_visitArgs___spec__1___boxed(lean_object*);
|
||||
extern lean_object* l_Lean_Expr_ReplaceImpl_replaceUnsafeM___main___closed__2;
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkOutsideQuot_parenthesizer___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_SMap_empty___at_Lean_PrettyPrinter_parenthesizerAttribute___spec__1___closed__2;
|
||||
lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__13;
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_symbol_parenthesizer___boxed(lean_object*);
|
||||
|
|
@ -435,6 +439,7 @@ lean_object* lean_expr_update_let(lean_object*, lean_object*, lean_object*, lean
|
|||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_compileParserBody___main___closed__7;
|
||||
lean_object* l_StateT_get___at_Lean_PrettyPrinter_Parenthesizer_ParenthesizerM_monadTraverser___spec__1___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_IO_ofExcept___at_Lean_PrettyPrinter_Parenthesizer_compileParenthesizerDescr___main___spec__1(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkOutsideQuot_parenthesizer(lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_mkParenthesizerOfConstantUnsafe(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_ParenthesizerM_monadTraverser___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
uint8_t l_Lean_Expr_Data_binderInfo(uint64_t);
|
||||
|
|
@ -569,6 +574,7 @@ lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkNoImmediateColon_parenthesi
|
|||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_identNoAntiquot_parenthesizer(lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_maybeParenthesize___closed__1;
|
||||
lean_object* l_ReaderT_bind___at_Lean_PrettyPrinter_Parenthesizer_term_parenthesizer___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkInsideQuot_parenthesizer___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_Meta_lambdaTelescope___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_parenthesizeCommand___closed__1;
|
||||
lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__9;
|
||||
|
|
@ -586,6 +592,7 @@ lean_object* l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lea
|
|||
lean_object* l_Lean_mkForall(lean_object*, uint8_t, lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateM_u2082Aux___main___at_Lean_PrettyPrinter_Parenthesizer_compileParserBody___main___spec__24___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Array_iterateM_u2082Aux___main___at_Lean_PrettyPrinter_Parenthesizer_compileParserBody___main___spec__19(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkInsideQuot_parenthesizer(lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_mkCategoryParenthesizerAttribute___closed__1;
|
||||
lean_object* l_Lean_Syntax_MonadTraverser_goUp___at_Lean_PrettyPrinter_Parenthesizer_visitArgs___spec__4(lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_compileParserBody___main___lambda__34___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
|
|
@ -600,6 +607,7 @@ lean_object* l_Array_iterateM_u2082Aux___main___at_Lean_PrettyPrinter_Parenthesi
|
|||
lean_object* l_Std_PersistentArray_forM___at_IO_runMeta___spec__3(lean_object*, lean_object*);
|
||||
uint8_t l_Lean_Meta_TransparencyMode_lt(uint8_t, uint8_t);
|
||||
extern lean_object* l_PUnit_Inhabited;
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkInsideQuot_parenthesizer___rarg___boxed(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_compileParserBody___main___lambda__33(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_mkParenthesizerAttribute___closed__3;
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_nameLitNoAntiquot_parenthesizer(lean_object*);
|
||||
|
|
@ -700,6 +708,7 @@ extern lean_object* l_Lean_Parser_mkParserOfConstantUnsafe___closed__5;
|
|||
extern lean_object* l_Lean_defaultMaxRecDepth;
|
||||
lean_object* l_Lean_PrettyPrinter_categoryParenthesizerAttribute___closed__3;
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_symbolNoWs_parenthesizer___rarg(lean_object*, lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkInsideQuot_parenthesizer___boxed(lean_object*);
|
||||
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_compileParserBody___main___closed__15;
|
||||
lean_object* l_Lean_PrettyPrinter_categoryParenthesizerAttribute___closed__4;
|
||||
|
|
@ -13357,6 +13366,14 @@ lean_dec(x_1);
|
|||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_toggleInsideQuot_parenthesizer(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_6;
|
||||
x_6 = lean_apply_4(x_1, x_2, x_3, x_4, x_5);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkStackTop_parenthesizer___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
|
|
@ -13597,6 +13614,86 @@ lean_dec(x_1);
|
|||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkInsideQuot_parenthesizer___rarg(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;
|
||||
x_4 = lean_box(0);
|
||||
x_5 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_5, 0, x_4);
|
||||
lean_ctor_set(x_5, 1, x_1);
|
||||
x_6 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_6, 0, x_5);
|
||||
lean_ctor_set(x_6, 1, x_3);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkInsideQuot_parenthesizer(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_checkInsideQuot_parenthesizer___rarg___boxed), 3, 0);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkInsideQuot_parenthesizer___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = l_Lean_PrettyPrinter_Parenthesizer_checkInsideQuot_parenthesizer___rarg(x_1, x_2, x_3);
|
||||
lean_dec(x_2);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkInsideQuot_parenthesizer___boxed(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = l_Lean_PrettyPrinter_Parenthesizer_checkInsideQuot_parenthesizer(x_1);
|
||||
lean_dec(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkOutsideQuot_parenthesizer___rarg(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;
|
||||
x_4 = lean_box(0);
|
||||
x_5 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_5, 0, x_4);
|
||||
lean_ctor_set(x_5, 1, x_1);
|
||||
x_6 = lean_alloc_ctor(0, 2, 0);
|
||||
lean_ctor_set(x_6, 0, x_5);
|
||||
lean_ctor_set(x_6, 1, x_3);
|
||||
return x_6;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkOutsideQuot_parenthesizer(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = lean_alloc_closure((void*)(l_Lean_PrettyPrinter_Parenthesizer_checkOutsideQuot_parenthesizer___rarg___boxed), 3, 0);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkOutsideQuot_parenthesizer___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_4;
|
||||
x_4 = l_Lean_PrettyPrinter_Parenthesizer_checkOutsideQuot_parenthesizer___rarg(x_1, x_2, x_3);
|
||||
lean_dec(x_2);
|
||||
return x_4;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_checkOutsideQuot_parenthesizer___boxed(lean_object* x_1) {
|
||||
_start:
|
||||
{
|
||||
lean_object* x_2;
|
||||
x_2 = l_Lean_PrettyPrinter_Parenthesizer_checkOutsideQuot_parenthesizer(x_1);
|
||||
lean_dec(x_1);
|
||||
return x_2;
|
||||
}
|
||||
}
|
||||
lean_object* l_Lean_PrettyPrinter_Parenthesizer_pushNone_parenthesizer___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
|
||||
_start:
|
||||
{
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue