From 243cda497e66ecfd5b598429c0e59d5dacb780cb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 10 Jun 2020 15:07:41 -0700 Subject: [PATCH] chore: remove `leadingNodePrec` and `trailingNodePrec` --- src/Lean/Parser/Parser.lean | 10 ++---- stage0/src/Lean/Parser/Parser.lean | 10 ++---- stage0/stdlib/Lean/Parser/Parser.c | 56 ------------------------------ 3 files changed, 4 insertions(+), 72 deletions(-) diff --git a/src/Lean/Parser/Parser.lean b/src/Lean/Parser/Parser.lean index 2f807f9dd5..258f7613e0 100644 --- a/src/Lean/Parser/Parser.lean +++ b/src/Lean/Parser/Parser.lean @@ -1095,12 +1095,6 @@ let asciiSym := asciiSym.trim; { info := unicodeSymbolInfo sym asciiSym, fn := unicodeSymbolFn sym asciiSym } -@[inline] def leadingNodePrec (n : SyntaxNodeKind) (prec : Nat) (p : Parser) : Parser := -leadingNode n prec p - -@[inline] def trailingNodePrec (n : SyntaxNodeKind) (prec : Nat) (p : Parser) : TrailingParser := -trailingNode n prec p - def mkAtomicInfo (k : String) : ParserInfo := { firstTokens := FirstTokens.tokens [ k ] } @@ -1751,8 +1745,8 @@ def compileParserDescr (categories : ParserCategories) : ParserDescr → Except | ParserDescr.many1 d => many1 <$> compileParserDescr d | ParserDescr.sepBy d₁ d₂ => sepBy <$> compileParserDescr d₁ <*> compileParserDescr d₂ | ParserDescr.sepBy1 d₁ d₂ => sepBy1 <$> compileParserDescr d₁ <*> compileParserDescr d₂ -| ParserDescr.node k prec d => leadingNodePrec k prec <$> compileParserDescr d -| ParserDescr.trailingNode k prec d => trailingNodePrec k prec <$> compileParserDescr d +| ParserDescr.node k prec d => leadingNode k prec <$> compileParserDescr d +| ParserDescr.trailingNode k prec d => trailingNode k prec <$> compileParserDescr d | ParserDescr.symbol tk => pure $ symbol tk | ParserDescr.numLit => pure $ numLit | ParserDescr.strLit => pure $ strLit diff --git a/stage0/src/Lean/Parser/Parser.lean b/stage0/src/Lean/Parser/Parser.lean index 2f807f9dd5..258f7613e0 100644 --- a/stage0/src/Lean/Parser/Parser.lean +++ b/stage0/src/Lean/Parser/Parser.lean @@ -1095,12 +1095,6 @@ let asciiSym := asciiSym.trim; { info := unicodeSymbolInfo sym asciiSym, fn := unicodeSymbolFn sym asciiSym } -@[inline] def leadingNodePrec (n : SyntaxNodeKind) (prec : Nat) (p : Parser) : Parser := -leadingNode n prec p - -@[inline] def trailingNodePrec (n : SyntaxNodeKind) (prec : Nat) (p : Parser) : TrailingParser := -trailingNode n prec p - def mkAtomicInfo (k : String) : ParserInfo := { firstTokens := FirstTokens.tokens [ k ] } @@ -1751,8 +1745,8 @@ def compileParserDescr (categories : ParserCategories) : ParserDescr → Except | ParserDescr.many1 d => many1 <$> compileParserDescr d | ParserDescr.sepBy d₁ d₂ => sepBy <$> compileParserDescr d₁ <*> compileParserDescr d₂ | ParserDescr.sepBy1 d₁ d₂ => sepBy1 <$> compileParserDescr d₁ <*> compileParserDescr d₂ -| ParserDescr.node k prec d => leadingNodePrec k prec <$> compileParserDescr d -| ParserDescr.trailingNode k prec d => trailingNodePrec k prec <$> compileParserDescr d +| ParserDescr.node k prec d => leadingNode k prec <$> compileParserDescr d +| ParserDescr.trailingNode k prec d => trailingNode k prec <$> compileParserDescr d | ParserDescr.symbol tk => pure $ symbol tk | ParserDescr.numLit => pure $ numLit | ParserDescr.strLit => pure $ strLit diff --git a/stage0/stdlib/Lean/Parser/Parser.c b/stage0/stdlib/Lean/Parser/Parser.c index b2568c8174..eaf4bb0f0d 100644 --- a/stage0/stdlib/Lean/Parser/Parser.c +++ b/stage0/stdlib/Lean/Parser/Parser.c @@ -67,7 +67,6 @@ lean_object* l_Lean_Parser_sepByInfo(lean_object*, lean_object*); lean_object* l_Lean_Parser_ParserState_shrinkStack___boxed(lean_object*, lean_object*); lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_Parser_mkCategoryParserFnExtension___spec__1___lambda__1(lean_object*, lean_object*, lean_object*); lean_object* lean_nat_div(lean_object*, lean_object*); -lean_object* l_Lean_Parser_trailingNodePrec(lean_object*, lean_object*, lean_object*); lean_object* l_RBNode_find___main___at_Lean_Parser_TokenMap_insert___spec__1___rarg___boxed(lean_object*, lean_object*); lean_object* l_Lean_Parser_decimalNumberFn___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Syntax_foldSepRevArgsM(lean_object*, lean_object*); @@ -580,7 +579,6 @@ extern lean_object* l_Lean_charLitKind; extern lean_object* l_List_reprAux___main___rarg___closed__1; lean_object* l_Lean_Parser_takeUntilFn___main___at_Lean_Parser_hexNumberFn___spec__3___boxed(lean_object*, lean_object*); lean_object* l_Lean_Parser_TokenMap_Inhabited(lean_object*); -lean_object* l_Lean_Parser_leadingNodePrec(lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Parser_categoryParserFnExtension___elambda__1___rarg___boxed(lean_object*); lean_object* l_Lean_Parser_regTermParserAttribute___closed__2; lean_object* l_Lean_Parser_rawIdent; @@ -10756,60 +10754,6 @@ lean_dec(x_1); return x_3; } } -lean_object* l_Lean_Parser_leadingNodePrec(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; -x_4 = lean_alloc_closure((void*)(l_Lean_Parser_checkPrecFn___boxed), 3, 1); -lean_closure_set(x_4, 0, x_2); -x_5 = lean_ctor_get(x_3, 0); -lean_inc(x_5); -lean_inc(x_1); -x_6 = l_Lean_Parser_nodeInfo(x_1, x_5); -x_7 = lean_ctor_get(x_3, 1); -lean_inc(x_7); -lean_dec(x_3); -x_8 = lean_alloc_closure((void*)(l_Lean_Parser_nodeFn), 4, 2); -lean_closure_set(x_8, 0, x_1); -lean_closure_set(x_8, 1, x_7); -x_9 = l_Lean_Parser_epsilonInfo; -x_10 = l_Lean_Parser_andthenInfo(x_9, x_6); -x_11 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2); -lean_closure_set(x_11, 0, x_4); -lean_closure_set(x_11, 1, x_8); -x_12 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_12, 0, x_10); -lean_ctor_set(x_12, 1, x_11); -return x_12; -} -} -lean_object* l_Lean_Parser_trailingNodePrec(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; -x_4 = lean_alloc_closure((void*)(l_Lean_Parser_checkPrecFn___boxed), 3, 1); -lean_closure_set(x_4, 0, x_2); -x_5 = lean_ctor_get(x_3, 0); -lean_inc(x_5); -lean_inc(x_1); -x_6 = l_Lean_Parser_nodeInfo(x_1, x_5); -x_7 = lean_ctor_get(x_3, 1); -lean_inc(x_7); -lean_dec(x_3); -x_8 = lean_alloc_closure((void*)(l_Lean_Parser_trailingNodeFn), 4, 2); -lean_closure_set(x_8, 0, x_1); -lean_closure_set(x_8, 1, x_7); -x_9 = l_Lean_Parser_epsilonInfo; -x_10 = l_Lean_Parser_andthenInfo(x_9, x_6); -x_11 = lean_alloc_closure((void*)(l_Lean_Parser_andthenFn), 4, 2); -lean_closure_set(x_11, 0, x_4); -lean_closure_set(x_11, 1, x_8); -x_12 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_12, 0, x_10); -lean_ctor_set(x_12, 1, x_11); -return x_12; -} -} lean_object* l_Lean_Parser_mkAtomicInfo___elambda__1(lean_object* x_1) { _start: {