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

chore: remove leadingNodePrec and trailingNodePrec

Browse source
This commit is contained in:
Leonardo de Moura 2020-06-10 15:07:41 -07:00
parent cdc2dbe28d
commit 243cda497e
3 changed files with 4 additions and 72 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Lean/Parser/Parser.lean
View file

@ -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

10
stage0/src/Lean/Parser/Parser.lean
View file

@ -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

56
stage0/stdlib/Lean/Parser/Parser.c
View file

@ -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:
{