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

chore: use leadingNode and trailingNode in the old frontend

Browse source
This commit is contained in:
Leonardo de Moura 2020-06-10 15:04:48 -07:00
parent 1c09e63a29
commit cdc2dbe28d
8 changed files with 2 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/builtin_exprs.cpp
View file

@ -793,7 +793,7 @@ static expr parse_parser(parser & p, bool leading, pos_info const & pos) {
p.check_token_next(get_rbracket_tk(), "`]` expected");
}
expr e = p.parse_expr();
name n = leading ? get_lean_parser_leading_node_prec_name() : get_lean_parser_trailing_node_prec_name();
name n = leading ? get_lean_parser_leading_node_name() : get_lean_parser_trailing_node_name();
expr r = mk_app(mk_constant(n), quote(kind), prec, e);
if (leading && kind.is_string()) {
r = mk_app(mk_constant({"Lean", "Parser", "withAntiquot"}),

8
src/library/constants.cpp
View file

@ -124,8 +124,6 @@ name const * g_lean_mk_name_num = nullptr;
name const * g_lean_mk_name_str = nullptr;
name const * g_lean_parser_leading_node = nullptr;
name const * g_lean_parser_trailing_node = nullptr;
name const * g_lean_parser_leading_node_prec = nullptr;
name const * g_lean_parser_trailing_node_prec = nullptr;
name const * g_mut_quot = nullptr;
name const * g_nat = nullptr;
name const * g_nat_succ = nullptr;
@ -318,8 +316,6 @@ void initialize_constants() {
g_lean_mk_name_str = new name{"Lean", "mkNameStr"};
g_lean_parser_leading_node = new name{"Lean", "Parser", "leadingNode"};
g_lean_parser_trailing_node = new name{"Lean", "Parser", "trailingNode"};
g_lean_parser_leading_node_prec = new name{"Lean", "Parser", "leadingNodePrec"};
g_lean_parser_trailing_node_prec = new name{"Lean", "Parser", "trailingNodePrec"};
g_mut_quot = new name{"MutQuot"};
g_nat = new name{"Nat"};
g_nat_succ = new name{"Nat", "succ"};
@ -513,8 +509,6 @@ void finalize_constants() {
delete g_lean_mk_name_str;
delete g_lean_parser_leading_node;
delete g_lean_parser_trailing_node;
delete g_lean_parser_leading_node_prec;
delete g_lean_parser_trailing_node_prec;
delete g_mut_quot;
delete g_nat;
delete g_nat_succ;
@ -707,8 +701,6 @@ name const & get_lean_mk_name_num_name() { return *g_lean_mk_name_num; }
name const & get_lean_mk_name_str_name() { return *g_lean_mk_name_str; }
name const & get_lean_parser_leading_node_name() { return *g_lean_parser_leading_node; }
name const & get_lean_parser_trailing_node_name() { return *g_lean_parser_trailing_node; }
name const & get_lean_parser_leading_node_prec_name() { return *g_lean_parser_leading_node_prec; }
name const & get_lean_parser_trailing_node_prec_name() { return *g_lean_parser_trailing_node_prec; }
name const & get_mut_quot_name() { return *g_mut_quot; }
name const & get_nat_name() { return *g_nat; }
name const & get_nat_succ_name() { return *g_nat_succ; }

2
src/library/constants.h
View file

@ -126,8 +126,6 @@ name const & get_lean_mk_name_num_name();
name const & get_lean_mk_name_str_name();
name const & get_lean_parser_leading_node_name();
name const & get_lean_parser_trailing_node_name();
name const & get_lean_parser_leading_node_prec_name();
name const & get_lean_parser_trailing_node_prec_name();
name const & get_mut_quot_name();
name const & get_nat_name();
name const & get_nat_succ_name();

2
src/library/constants.txt
View file

@ -119,8 +119,6 @@ Lean.mkNameNum
Lean.mkNameStr
Lean.Parser.leadingNode
Lean.Parser.trailingNode
Lean.Parser.leadingNodePrec
Lean.Parser.trailingNodePrec
MutQuot
Nat
Nat.succ

2
stage0/src/frontends/lean/builtin_exprs.cpp
View file

@ -793,7 +793,7 @@ static expr parse_parser(parser & p, bool leading, pos_info const & pos) {
p.check_token_next(get_rbracket_tk(), "`]` expected");
}
expr e = p.parse_expr();
name n = leading ? get_lean_parser_leading_node_prec_name() : get_lean_parser_trailing_node_prec_name();
name n = leading ? get_lean_parser_leading_node_name() : get_lean_parser_trailing_node_name();
expr r = mk_app(mk_constant(n), quote(kind), prec, e);
if (leading && kind.is_string()) {
r = mk_app(mk_constant({"Lean", "Parser", "withAntiquot"}),

8
stage0/src/library/constants.cpp
View file

@ -124,8 +124,6 @@ name const * g_lean_mk_name_num = nullptr;
name const * g_lean_mk_name_str = nullptr;
name const * g_lean_parser_leading_node = nullptr;
name const * g_lean_parser_trailing_node = nullptr;
name const * g_lean_parser_leading_node_prec = nullptr;
name const * g_lean_parser_trailing_node_prec = nullptr;
name const * g_mut_quot = nullptr;
name const * g_nat = nullptr;
name const * g_nat_succ = nullptr;
@ -318,8 +316,6 @@ void initialize_constants() {
g_lean_mk_name_str = new name{"Lean", "mkNameStr"};
g_lean_parser_leading_node = new name{"Lean", "Parser", "leadingNode"};
g_lean_parser_trailing_node = new name{"Lean", "Parser", "trailingNode"};
g_lean_parser_leading_node_prec = new name{"Lean", "Parser", "leadingNodePrec"};
g_lean_parser_trailing_node_prec = new name{"Lean", "Parser", "trailingNodePrec"};
g_mut_quot = new name{"MutQuot"};
g_nat = new name{"Nat"};
g_nat_succ = new name{"Nat", "succ"};
@ -513,8 +509,6 @@ void finalize_constants() {
delete g_lean_mk_name_str;
delete g_lean_parser_leading_node;
delete g_lean_parser_trailing_node;
delete g_lean_parser_leading_node_prec;
delete g_lean_parser_trailing_node_prec;
delete g_mut_quot;
delete g_nat;
delete g_nat_succ;
@ -707,8 +701,6 @@ name const & get_lean_mk_name_num_name() { return *g_lean_mk_name_num; }
name const & get_lean_mk_name_str_name() { return *g_lean_mk_name_str; }
name const & get_lean_parser_leading_node_name() { return *g_lean_parser_leading_node; }
name const & get_lean_parser_trailing_node_name() { return *g_lean_parser_trailing_node; }
name const & get_lean_parser_leading_node_prec_name() { return *g_lean_parser_leading_node_prec; }
name const & get_lean_parser_trailing_node_prec_name() { return *g_lean_parser_trailing_node_prec; }
name const & get_mut_quot_name() { return *g_mut_quot; }
name const & get_nat_name() { return *g_nat; }
name const & get_nat_succ_name() { return *g_nat_succ; }

2
stage0/src/library/constants.h
View file

@ -126,8 +126,6 @@ name const & get_lean_mk_name_num_name();
name const & get_lean_mk_name_str_name();
name const & get_lean_parser_leading_node_name();
name const & get_lean_parser_trailing_node_name();
name const & get_lean_parser_leading_node_prec_name();
name const & get_lean_parser_trailing_node_prec_name();
name const & get_mut_quot_name();
name const & get_nat_name();
name const & get_nat_succ_name();

2
stage0/src/library/constants.txt
View file

@ -119,8 +119,6 @@ Lean.mkNameNum
Lean.mkNameStr
Lean.Parser.leadingNode
Lean.Parser.trailingNode
Lean.Parser.leadingNodePrec
Lean.Parser.trailingNodePrec
MutQuot
Nat
Nat.succ