michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(frontends/lean): explicit initialization/finalization

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-23 10:00:36 -07:00
parent 79cfb32ec7
commit 29d6bff785
25 changed files with 604 additions and 309 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/frontends/lean/builtin_cmds.cpp
View file

@ -347,8 +347,7 @@ environment erase_cache_cmd(parser & p) {
return p.env();
}
cmd_table init_cmd_table() {
cmd_table r;
void init_cmd_table(cmd_table & r) {
add_cmd(r, cmd_info("open", "create aliases for declarations, and use objects defined in other namespaces", open_cmd));
add_cmd(r, cmd_info("export", "create abbreviations for declarations, and export objects defined in other namespaces", export_cmd));
add_cmd(r, cmd_info("set_option", "set configuration option", set_option_cmd));
@ -372,13 +371,20 @@ cmd_table init_cmd_table() {
register_begin_end_cmds(r);
register_class_cmds(r);
register_tactic_hint_cmd(r);
return r;
}
static cmd_table * g_cmds = nullptr;
cmd_table get_builtin_cmds() {
static optional<cmd_table> r;
if (!r)
r = init_cmd_table();
return *r;
return *g_cmds;
}
void initialize_builtin_cmds() {
g_cmds = new cmd_table();
init_cmd_table(*g_cmds);
}
void finalize_builtin_cmds() {
delete g_cmds;
}
}

2
src/frontends/lean/builtin_cmds.h
View file

@ -8,4 +8,6 @@ Author: Leonardo de Moura
#include "frontends/lean/cmd_table.h"
namespace lean {
cmd_table get_builtin_cmds();
void initialize_builtin_cmds();
void finalize_builtin_cmds();
}

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

@ -21,19 +21,15 @@ Author: Leonardo de Moura
#include "frontends/lean/parser.h"
#include "frontends/lean/extra_info.h"
#include "frontends/lean/util.h"
#include "frontends/lean/tokens.h"
namespace lean {
namespace notation {
static name g_llevel_curly(".{"), g_rcurly("}"), g_in("in"), g_colon(":"), g_assign(":=");
static name g_comma(","), g_visible("[visible]"), g_from("from"), g_using("using");
static name g_then("then"), g_have("have"), g_by("by"), g_proof("proof"), g_qed("qed"), g_end("end");
static name g_take("take"), g_assume("assume"), g_show("show"), g_fun("fun");
static expr parse_Type(parser & p, unsigned, expr const *, pos_info const & pos) {
if (p.curr_is_token(g_llevel_curly)) {
if (p.curr_is_token(get_llevel_curly_tk())) {
p.next();
level l = p.parse_level();
p.check_token_next(g_rcurly, "invalid Type expression, '}' expected");
p.check_token_next(get_rcurly_tk(), "invalid Type expression, '}' expected");
return p.save_pos(mk_sort(l), pos);
} else {
return p.save_pos(mk_sort(mk_level_placeholder()), pos);
@ -46,10 +42,10 @@ static expr parse_Type_prime(parser & p, unsigned, expr const *, pos_info const
static expr parse_let(parser & p, pos_info const & pos);
static expr parse_let_body(parser & p, pos_info const & pos) {
if (p.curr_is_token(g_comma)) {
if (p.curr_is_token(get_comma_tk())) {
p.next();
return parse_let(p, pos);
} else if (p.curr_is_token(g_in)) {
} else if (p.curr_is_token(get_in_tk())) {
p.next();
return p.parse_expr();
} else {
@ -59,7 +55,7 @@ static expr parse_let_body(parser & p, pos_info const & pos) {
static void parse_let_modifiers(parser & p, bool & is_visible) {
while (true) {
if (p.curr_is_token(g_visible)) {
if (p.curr_is_token(get_visible_tk())) {
is_visible = true;
p.next();
} else {
@ -79,24 +75,24 @@ static expr parse_let(parser & p, pos_info const & pos) {
optional<expr> type;
expr value;
parse_let_modifiers(p, is_visible);
if (p.curr_is_token(g_assign)) {
if (p.curr_is_token(get_assign_tk())) {
p.next();
value = p.parse_expr();
} else if (p.curr_is_token(g_colon)) {
} else if (p.curr_is_token(get_colon_tk())) {
p.next();
type = p.parse_expr();
p.check_token_next(g_assign, "invalid declaration, ':=' expected");
p.check_token_next(get_assign_tk(), "invalid declaration, ':=' expected");
value = p.parse_expr();
} else {
parser::local_scope scope2(p);
buffer<expr> ps;
auto lenv = p.parse_binders(ps);
if (p.curr_is_token(g_colon)) {
if (p.curr_is_token(get_colon_tk())) {
p.next();
type = p.parse_scoped_expr(ps, lenv);
type = Pi(ps, *type, p);
}
p.check_token_next(g_assign, "invalid let declaration, ':=' expected");
p.check_token_next(get_assign_tk(), "invalid let declaration, ':=' expected");
value = p.parse_scoped_expr(ps, lenv);
value = Fun(ps, value, p);
}
@ -131,8 +127,9 @@ static expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const &
optional<expr> pre_tac = get_begin_end_pre_tactic(p.env());
optional<expr> r;
while (true) {
bool use_exact = (p.curr_is_token(g_have) || p.curr_is_token(g_show) || p.curr_is_token(g_assume) ||
p.curr_is_token(g_take) || p.curr_is_token(g_fun));
bool use_exact = (p.curr_is_token(get_have_tk()) || p.curr_is_token(get_show_tk()) ||
p.curr_is_token(get_assume_tk()) || p.curr_is_token(get_take_tk()) ||
p.curr_is_token(get_fun_tk()));
auto pos = p.pos();
expr tac = p.parse_expr();
if (use_exact)
@ -141,11 +138,11 @@ static expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const &
tac = p.mk_app({get_and_then_tac_fn(), *pre_tac, tac}, pos);
tac = p.mk_app(get_determ_tac_fn(), tac, pos);
r = r ? p.mk_app({get_and_then_tac_fn(), *r, tac}, pos) : tac;
if (p.curr_is_token(g_end)) {
if (p.curr_is_token(get_end_tk())) {
auto pos = p.pos();
p.next();
return p.mk_by(*r, pos);
} else if (p.curr_is_token(g_comma)) {
} else if (p.curr_is_token(get_comma_tk())) {
p.next();
} else {
throw parser_error("invalid begin-end, ',' or 'end' expected", p.pos());
@ -155,32 +152,32 @@ static expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const &
static expr parse_proof_qed_core(parser & p, pos_info const & pos) {
expr r = p.save_pos(mk_proof_qed_annotation(p.parse_expr()), pos);
p.check_token_next(g_qed, "invalid proof-qed, 'qed' expected");
p.check_token_next(get_qed_tk(), "invalid proof-qed, 'qed' expected");
return r;
}
static expr parse_proof(parser & p, expr const & prop) {
if (p.curr_is_token(g_from)) {
if (p.curr_is_token(get_from_tk())) {
// parse: 'from' expr
p.next();
return p.parse_expr();
} else if (p.curr_is_token(g_proof)) {
} else if (p.curr_is_token(get_proof_tk())) {
auto pos = p.pos();
p.next();
return parse_proof_qed_core(p, pos);
} else if (p.curr_is_token(g_by)) {
} else if (p.curr_is_token(get_by_tk())) {
// parse: 'by' tactic
auto pos = p.pos();
p.next();
expr t = p.parse_expr();
return p.mk_by(t, pos);
} else if (p.curr_is_token(g_using)) {
} else if (p.curr_is_token(get_using_tk())) {
// parse: 'using' locals* ',' proof
auto using_pos = p.pos();
p.next();
parser::local_scope scope(p);
buffer<expr> locals;
while (!p.curr_is_token(g_comma)) {
while (!p.curr_is_token(get_comma_tk())) {
auto id_pos = p.pos();
expr l = p.parse_expr();
if (!is_local(l))
@ -208,7 +205,7 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional<expr> con
bool is_visible = false;
name id;
expr prop;
if (p.curr_is_token(g_visible)) {
if (p.curr_is_token(get_visible_tk())) {
p.next();
is_visible = true;
id = p.mk_fresh_name();
@ -216,12 +213,12 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional<expr> con
} else if (p.curr_is_identifier()) {
id = p.get_name_val();
p.next();
if (p.curr_is_token(g_visible)) {
if (p.curr_is_token(get_visible_tk())) {
p.next();
p.check_token_next(g_colon, "invalid 'have' declaration, ':' expected");
p.check_token_next(get_colon_tk(), "invalid 'have' declaration, ':' expected");
is_visible = true;
prop = p.parse_expr();
} else if (p.curr_is_token(g_colon)) {
} else if (p.curr_is_token(get_colon_tk())) {
p.next();
prop = p.parse_expr();
} else {
@ -233,7 +230,7 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional<expr> con
id = p.mk_fresh_name();
prop = p.parse_expr();
}
p.check_token_next(g_comma, "invalid 'have' declaration, ',' expected");
p.check_token_next(get_comma_tk(), "invalid 'have' declaration, ',' expected");
expr proof;
if (prev_local) {
parser::local_scope scope(p);
@ -245,16 +242,16 @@ static expr parse_have_core(parser & p, pos_info const & pos, optional<expr> con
} else {
proof = parse_proof(p, prop);
}
p.check_token_next(g_comma, "invalid 'have' declaration, ',' expected");
p.check_token_next(get_comma_tk(), "invalid 'have' declaration, ',' expected");
parser::local_scope scope(p);
binder_info bi = mk_contextual_info(is_visible);
expr l = p.save_pos(mk_local(id, prop, bi), pos);
p.add_local(l);
expr body;
if (p.curr_is_token(g_then)) {
if (p.curr_is_token(get_then_tk())) {
auto then_pos = p.pos();
p.next();
p.check_token_next(g_have, "invalid 'then have' declaration, 'have' expected");
p.check_token_next(get_have_tk(), "invalid 'then have' declaration, 'have' expected");
body = parse_have_core(p, then_pos, some_expr(l));
} else {
body = p.parse_expr();
@ -269,19 +266,19 @@ static expr parse_have(parser & p, unsigned, expr const *, pos_info const & pos)
return parse_have_core(p, pos, none_expr());
}
static name H_show("H_show");
static name * H_show = nullptr;
static expr parse_show(parser & p, unsigned, expr const *, pos_info const & pos) {
expr prop = p.parse_expr();
p.check_token_next(g_comma, "invalid 'show' declaration, ',' expected");
p.check_token_next(get_comma_tk(), "invalid 'show' declaration, ',' expected");
expr proof = parse_proof(p, prop);
expr b = p.save_pos(mk_lambda(H_show, prop, Var(0)), pos);
expr b = p.save_pos(mk_lambda(*H_show, prop, Var(0)), pos);
expr r = p.mk_app(b, proof, pos);
return p.save_pos(mk_show_annotation(r), pos);
}
static name g_exists_elim("exists_elim");
static name * g_exists_elim = nullptr;
static expr parse_obtain(parser & p, unsigned, expr const *, pos_info const & pos) {
if (!p.env().find(g_exists_elim))
if (!p.env().find(*g_exists_elim))
throw parser_error("invalid use of 'obtain' expression, environment does not contain 'exists_elim' theorem", pos);
// exists_elim {A : Type} {P : A → Prop} {B : Prop} (H1 : ∃ x : A, P x) (H2 : ∀ (a : A) (H : P a), B)
buffer<expr> ps;
@ -291,7 +288,7 @@ static expr parse_obtain(parser & p, unsigned, expr const *, pos_info const & po
if (num_ps < 2)
throw parser_error("invalid 'obtain' expression, at least 2 binders expected", b_pos);
bool is_visible = false;
if (p.curr_is_token(g_visible)) {
if (p.curr_is_token(get_visible_tk())) {
p.next();
is_visible = true;
}
@ -299,10 +296,10 @@ static expr parse_obtain(parser & p, unsigned, expr const *, pos_info const & po
expr H = ps[num_ps-1];
ps[num_ps-1] = update_local(H, mlocal_type(H), local_info(H).update_contextual(false));
}
p.check_token_next(g_comma, "invalid 'obtain' expression, ',' expected");
p.check_token_next(g_from, "invalid 'obtain' expression, 'from' expected");
p.check_token_next(get_comma_tk(), "invalid 'obtain' expression, ',' expected");
p.check_token_next(get_from_tk(), "invalid 'obtain' expression, 'from' expected");
expr H1 = p.parse_expr();
p.check_token_next(g_comma, "invalid 'obtain' expression, ',' expected");
p.check_token_next(get_comma_tk(), "invalid 'obtain' expression, ',' expected");
expr b = p.parse_scoped_expr(ps, env);
expr H = ps[num_ps-1];
name H_name = local_pp_name(H);
@ -312,12 +309,12 @@ static expr parse_obtain(parser & p, unsigned, expr const *, pos_info const & po
expr a = ps[i];
expr H_aux = mk_local(p.mk_fresh_name(), H_name.append_after(i), mk_expr_placeholder(), mk_contextual_info(false));
expr H2 = Fun({a, H}, b);
b = mk_constant(g_exists_elim)(H_aux, H2);
b = mk_constant(*g_exists_elim)(H_aux, H2);
H = H_aux;
}
expr a = ps[0];
expr H2 = Fun({a, H}, b);
expr r = mk_constant(g_exists_elim)(H1, H2);
expr r = mk_constant(*g_exists_elim)(H1, H2);
return p.rec_save_pos(r, pos);
}
@ -345,7 +342,7 @@ static expr parse_explicit_expr(parser & p, unsigned, expr const *, pos_info con
static expr parse_including_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
buffer<expr> locals;
while (!p.curr_is_token(g_comma)) {
while (!p.curr_is_token(get_comma_tk())) {
auto pos = p.pos();
name id = p.check_id_next("invalid 'including', identifier expected");
if (auto it = p.get_local(id)) {
@ -416,19 +413,32 @@ parse_table init_led_table() {
return r;
}
}
bool is_show_aux_name(name const & n) { return n == notation::H_show; }
bool is_show_aux_name(name const & n) { return n == *notation::H_show; }
static parse_table * g_nud_table = nullptr;
static parse_table * g_led_table = nullptr;
parse_table get_builtin_nud_table() {
static optional<parse_table> r;
if (!r)
r = notation::init_nud_table();
return *r;
return *g_nud_table;
}
parse_table get_builtin_led_table() {
static optional<parse_table> r;
if (!r)
r = notation::init_led_table();
return *r;
return *g_led_table;
}
void initialize_builtin_exprs() {
notation::H_show = new name("H_show");
notation::g_exists_elim = new name("exists_elim");
g_nud_table = new parse_table();
*g_nud_table = notation::init_nud_table();
g_led_table = new parse_table();
*g_led_table = notation::init_led_table();
}
void finalize_builtin_exprs() {
delete g_led_table;
delete g_nud_table;
delete notation::H_show;
delete notation::g_exists_elim;
}
}

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

@ -10,4 +10,6 @@ namespace lean {
parse_table get_builtin_nud_table();
parse_table get_builtin_led_table();
bool is_show_aux_name(name const & n);
void initialize_builtin_exprs();
void finalize_builtin_exprs();
}

73
src/frontends/lean/decl_cmds.cpp
View file

@ -20,19 +20,9 @@ Author: Leonardo de Moura
#include "frontends/lean/parser.h"
#include "frontends/lean/util.h"
#include "frontends/lean/class.h"
#include "frontends/lean/tokens.h"
namespace lean {
static name g_llevel_curly(".{");
static name g_rcurly("}");
static name g_colon(":");
static name g_assign(":=");
static name g_definition("definition");
static name g_theorem("theorem");
static name g_opaque("opaque");
static name g_instance("[instance]");
static name g_coercion("[coercion]");
static name g_reducible("[reducible]");
environment universe_cmd(parser & p) {
name n = p.check_id_next("invalid universe declaration, identifier expected");
environment env = p.env();
@ -49,9 +39,9 @@ environment universe_cmd(parser & p) {
}
bool parse_univ_params(parser & p, buffer<name> & ps) {
if (p.curr_is_token(g_llevel_curly)) {
if (p.curr_is_token(get_llevel_curly_tk())) {
p.next();
while (!p.curr_is_token(g_rcurly)) {
while (!p.curr_is_token(get_rcurly_tk())) {
name l = p.check_id_next("invalid universe parameter, identifier expected");
p.add_local_level(l, mk_param_univ(l));
ps.push_back(l);
@ -74,9 +64,6 @@ void update_univ_parameters(buffer<name> & ls_buffer, name_set const & found, pa
});
}
static name g_axiom("axiom");
static name g_variable("variable");
static environment declare_var(parser & p, environment env,
name const & n, level_param_names const & ls, expr const & type,
bool is_axiom, optional<binder_info> const & _bi, pos_info const & pos) {
@ -92,10 +79,10 @@ static environment declare_var(parser & p, environment env,
name full_n = ns + n;
if (is_axiom) {
env = module::add(env, check(env, mk_axiom(full_n, ls, type)));
p.add_decl_index(full_n, pos, g_axiom, type);
p.add_decl_index(full_n, pos, get_axiom_tk(), type);
} else {
env = module::add(env, check(env, mk_var_decl(full_n, ls, type)));
p.add_decl_index(full_n, pos, g_variable, type);
p.add_decl_index(full_n, pos, get_variable_tk(), type);
}
if (!ns.is_anonymous())
env = add_expr_alias(env, n, full_n);
@ -123,17 +110,17 @@ environment variable_cmd_core(parser & p, bool is_axiom) {
optional<binder_info> bi = parse_binder_info(p);
name n = p.check_id_next("invalid declaration, identifier expected");
buffer<name> ls_buffer;
if (p.curr_is_token(g_llevel_curly) && in_section_or_context(p.env()))
if (p.curr_is_token(get_llevel_curly_tk()) && in_section_or_context(p.env()))
throw parser_error("invalid declaration, axioms/parameters occurring in sections cannot be universe polymorphic", p.pos());
optional<parser::local_scope> scope1;
if (!in_section_or_context(p.env()))
scope1.emplace(p);
parse_univ_params(p, ls_buffer);
expr type;
if (!p.curr_is_token(g_colon)) {
if (!p.curr_is_token(get_colon_tk())) {
buffer<expr> ps;
auto lenv = p.parse_binders(ps);
p.check_token_next(g_colon, "invalid declaration, ':' expected");
p.check_token_next(get_colon_tk(), "invalid declaration, ':' expected");
type = p.parse_scoped_expr(ps, lenv);
type = Pi(ps, type, p);
} else {
@ -173,13 +160,13 @@ struct decl_modifiers {
void parse(parser & p) {
while (true) {
if (p.curr_is_token(g_instance)) {
if (p.curr_is_token(get_instance_tk())) {
m_is_instance = true;
p.next();
} else if (p.curr_is_token(g_coercion)) {
} else if (p.curr_is_token(get_coercion_tk())) {
m_is_coercion = true;
p.next();
} else if (p.curr_is_token(g_reducible)) {
} else if (p.curr_is_token(get_reducible_tk())) {
m_is_reducible = true;
p.next();
} else {
@ -219,20 +206,20 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque, boo
// Parse modifiers
modifiers.parse(p);
if (p.curr_is_token(g_assign)) {
if (p.curr_is_token(get_assign_tk())) {
auto pos = p.pos();
p.next();
type = p.save_pos(mk_expr_placeholder(), pos);
value = p.parse_expr();
} else if (p.curr_is_token(g_colon)) {
} else if (p.curr_is_token(get_colon_tk())) {
p.next();
auto pos = p.pos();
type = p.parse_expr();
if (is_theorem && !p.curr_is_token(g_assign)) {
if (is_theorem && !p.curr_is_token(get_assign_tk())) {
check_end_of_theorem(p);
value = mk_expr_placeholder();
} else {
p.check_token_next(g_assign, "invalid declaration, ':=' expected");
p.check_token_next(get_assign_tk(), "invalid declaration, ':=' expected");
value = p.save_pos(p.parse_expr(), pos);
}
} else {
@ -240,19 +227,19 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque, boo
optional<local_environment> lenv;
lenv = p.parse_binders(ps);
auto pos = p.pos();
if (p.curr_is_token(g_colon)) {
if (p.curr_is_token(get_colon_tk())) {
p.next();
type = p.parse_scoped_expr(ps, *lenv);
if (is_theorem && !p.curr_is_token(g_assign)) {
if (is_theorem && !p.curr_is_token(get_assign_tk())) {
check_end_of_theorem(p);
value = p.save_pos(mk_expr_placeholder(), pos);
} else {
p.check_token_next(g_assign, "invalid declaration, ':=' expected");
p.check_token_next(get_assign_tk(), "invalid declaration, ':=' expected");
value = p.parse_scoped_expr(ps, *lenv);
}
} else {
type = p.save_pos(mk_expr_placeholder(), p.pos());
p.check_token_next(g_assign, "invalid declaration, ':=' expected");
p.check_token_next(get_assign_tk(), "invalid declaration, ':=' expected");
value = p.parse_scoped_expr(ps, *lenv);
}
type = Pi(ps, type, p);
@ -359,7 +346,7 @@ environment definition_cmd(parser & p) {
return definition_cmd_core(p, false, false, false, false);
}
environment opaque_definition_cmd(parser & p) {
p.check_token_next(g_definition, "invalid 'opaque' definition, 'definition' expected");
p.check_token_next(get_definition_tk(), "invalid 'opaque' definition, 'definition' expected");
return definition_cmd_core(p, false, true, false, false);
}
environment theorem_cmd(parser & p) {
@ -367,9 +354,9 @@ environment theorem_cmd(parser & p) {
}
environment private_definition_cmd(parser & p) {
bool is_theorem = false;
if (p.curr_is_token_or_id(g_definition)) {
if (p.curr_is_token_or_id(get_definition_tk())) {
p.next();
} else if (p.curr_is_token_or_id(g_theorem)) {
} else if (p.curr_is_token_or_id(get_theorem_tk())) {
p.next();
is_theorem = true;
} else {
@ -380,13 +367,13 @@ environment private_definition_cmd(parser & p) {
environment protected_definition_cmd(parser & p) {
bool is_theorem = false;
bool is_opaque = false;
if (p.curr_is_token_or_id(g_opaque)) {
if (p.curr_is_token_or_id(get_opaque_tk())) {
is_opaque = true;
p.next();
p.check_token_next(g_definition, "invalid 'protected' definition, 'definition' expected");
} else if (p.curr_is_token_or_id(g_definition)) {
p.check_token_next(get_definition_tk(), "invalid 'protected' definition, 'definition' expected");
} else if (p.curr_is_token_or_id(get_definition_tk())) {
p.next();
} else if (p.curr_is_token_or_id(g_theorem)) {
} else if (p.curr_is_token_or_id(get_theorem_tk())) {
p.next();
is_theorem = true;
is_opaque = true;
@ -396,15 +383,13 @@ environment protected_definition_cmd(parser & p) {
return definition_cmd_core(p, is_theorem, is_opaque, false, true);
}
static name g_lparen("("), g_lcurly("{"), g_ldcurly("⦃"), g_lbracket("[");
static environment variables_cmd(parser & p) {
auto pos = p.pos();
environment env = p.env();
while (true) {
optional<binder_info> bi = parse_binder_info(p);
buffer<name> ids;
while (!p.curr_is_token(g_colon)) {
while (!p.curr_is_token(get_colon_tk())) {
name id = p.check_id_next("invalid parameters declaration, identifier expected");
ids.push_back(id);
}
@ -426,8 +411,8 @@ static environment variables_cmd(parser & p) {
new_ls = append(ls, new_ls);
env = declare_var(p, env, id, new_ls, new_type, false, bi, pos);
}
if (!p.curr_is_token(g_lparen) && !p.curr_is_token(g_lcurly) &&
!p.curr_is_token(g_ldcurly) && !p.curr_is_token(g_lbracket))
if (!p.curr_is_token(get_lparen_tk()) && !p.curr_is_token(get_lcurly_tk()) &&
!p.curr_is_token(get_ldcurly_tk()) && !p.curr_is_token(get_lbracket_tk()))
break;
}
return env;

30
src/frontends/lean/elaborator.cpp
View file

@ -57,17 +57,6 @@ namespace lean {
// elaborator configuration options
static name * g_elaborator_local_instances = nullptr;
void initialize_elaborator() {
g_elaborator_local_instances = new name{"elaborator", "local_instances"};
register_bool_option(*g_elaborator_local_instances, LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES,
"(lean elaborator) use local declarates as class instances");
}
void finalize_elaborator() {
delete g_elaborator_local_instances;
}
bool get_elaborator_local_instances(options const & opts) {
return opts.get_bool(*g_elaborator_local_instances, LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES);
}
@ -1040,15 +1029,28 @@ public:
}
};
static name g_tmp_prefix = name::mk_internal_unique_name();
static name * g_tmp_prefix = nullptr;
std::tuple<expr, level_param_names> elaborate(elaborator_context & env, list<expr> const & ctx, expr const & e,
bool relax_main_opaque, bool ensure_type) {
return elaborator(env, name_generator(g_tmp_prefix))(ctx, e, ensure_type, relax_main_opaque);
return elaborator(env, name_generator(*g_tmp_prefix))(ctx, e, ensure_type, relax_main_opaque);
}
std::tuple<expr, expr, level_param_names> elaborate(elaborator_context & env, name const & n, expr const & t, expr const & v,
bool is_opaque) {
return elaborator(env, name_generator(g_tmp_prefix))(t, v, n, is_opaque);
return elaborator(env, name_generator(*g_tmp_prefix))(t, v, n, is_opaque);
}
void initialize_elaborator() {
g_elaborator_local_instances = new name{"elaborator", "local_instances"};
register_bool_option(*g_elaborator_local_instances, LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES,
"(lean elaborator) use local declarates as class instances");
g_tmp_prefix = new name(name::mk_internal_unique_name());
}
void finalize_elaborator() {
delete g_elaborator_local_instances;
delete g_tmp_prefix;
}
}

58
src/frontends/lean/inductive_cmd.cpp
View file

@ -24,16 +24,9 @@ Author: Leonardo de Moura
#include "frontends/lean/util.h"
#include "frontends/lean/class.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/tokens.h"
namespace lean {
static name g_assign(":=");
static name g_with("with");
static name g_colon(":");
static name g_comma(",");
static name g_lcurly("{");
static name g_rcurly("}");
static name g_class("[class]");
using inductive::intro_rule;
using inductive::inductive_decl;
using inductive::inductive_decl_name;
@ -54,11 +47,24 @@ intro_rule update_intro_rule(intro_rule const & r, expr const & t) {
return intro_rule(intro_rule_name(r), t);
}
static name g_tmp_prefix = name::mk_internal_unique_name();
static name * g_tmp_prefix = nullptr;
static name * g_inductive = nullptr;
static name * g_intro = nullptr;
static name * g_recursor = nullptr;
static name g_inductive("inductive");
static name g_intro("intro");
static name g_recursor("recursor");
void initialize_inductive_cmd() {
g_tmp_prefix = new name(name::mk_internal_unique_name());
g_inductive = new name("inductive");
g_intro = new name("intro");
g_recursor = new name("recursor");
}
void finalize_inductive_cmd() {
delete g_recursor;
delete g_intro;
delete g_inductive;
delete g_tmp_prefix;
}
struct inductive_cmd_fn {
typedef std::unique_ptr<type_checker> type_checker_ptr;
@ -67,7 +73,7 @@ struct inductive_cmd_fn {
modifiers():m_is_class(false) {}
void parse(parser & p) {
while (true) {
if (p.curr_is_token(g_class)) {
if (p.curr_is_token(get_class_tk())) {
m_is_class = true;
p.next();
} else {
@ -100,7 +106,7 @@ struct inductive_cmd_fn {
m_first = true;
m_using_explicit_levels = false;
m_num_params = 0;
name u_name(g_tmp_prefix, "u");
name u_name(*g_tmp_prefix, "u");
m_env = m_env.add_universe(u_name);
m_u = mk_global_univ(u_name);
m_infer_result_universe = false;
@ -125,12 +131,12 @@ struct inductive_cmd_fn {
// for intro rules, we append the name of the inductive datatype
check_atomic(id);
name full_id = *ind_name + id;
m_decl_info.emplace_back(full_id, g_intro, m_pos);
m_decl_info.emplace_back(full_id, *g_intro, m_pos);
return mk_pair(id, full_id);
} else {
name full_id = m_namespace + id;
m_decl_info.emplace_back(full_id, g_inductive, m_pos);
m_decl_info.emplace_back(mk_rec_name(full_id), g_recursor, m_pos);
m_decl_info.emplace_back(full_id, *g_inductive, m_pos);
m_decl_info.emplace_back(mk_rec_name(full_id), *g_recursor, m_pos);
return mk_pair(id, full_id);
}
}
@ -179,11 +185,11 @@ struct inductive_cmd_fn {
expr type;
buffer<expr> ps;
m_pos = m_p.pos();
if (m_p.curr_is_token(g_assign)) {
if (m_p.curr_is_token(get_assign_tk())) {
type = mk_sort(mk_level_placeholder());
} else if (!m_p.curr_is_token(g_colon)) {
} else if (!m_p.curr_is_token(get_colon_tk())) {
m_p.parse_binders(ps);
if (m_p.curr_is_token(g_colon)) {
if (m_p.curr_is_token(get_colon_tk())) {
m_p.next();
type = m_p.parse_scoped_expr(ps);
} else {
@ -293,18 +299,18 @@ struct inductive_cmd_fn {
while (true) {
name intro_name = parse_intro_decl_name(ind_name);
bool strict = true;
if (m_p.curr_is_token(g_lcurly)) {
if (m_p.curr_is_token(get_lcurly_tk())) {
m_p.next();
m_p.check_token_next(g_rcurly, "invalid introduction rule, '}' expected");
m_p.check_token_next(get_rcurly_tk(), "invalid introduction rule, '}' expected");
strict = false;
m_relaxed_implicit_infer.insert(intro_name);
}
m_p.check_token_next(g_colon, "invalid introduction rule, ':' expected");
m_p.check_token_next(get_colon_tk(), "invalid introduction rule, ':' expected");
expr intro_type = m_p.parse_scoped_expr(params, m_env);
intro_type = Pi(params, intro_type, m_p);
intro_type = infer_implicit(intro_type, params.size(), strict);
intros.push_back(intro_rule(intro_name, intro_type));
if (!m_p.curr_is_token(g_comma))
if (!m_p.curr_is_token(get_comma_tk()))
break;
m_p.next();
}
@ -325,7 +331,7 @@ struct inductive_cmd_fn {
m_modifiers.insert(d_name, mods);
expr d_type = parse_datatype_type();
bool empty_type = true;
if (m_p.curr_is_token(g_assign)) {
if (m_p.curr_is_token(get_assign_tk())) {
empty_type = false;
m_p.next();
}
@ -347,7 +353,7 @@ struct inductive_cmd_fn {
auto d_intro_rules = parse_intro_rules(d_name, params);
decls.push_back(inductive_decl(d_name, d_type, d_intro_rules));
}
if (!m_p.curr_is_token(g_with)) {
if (!m_p.curr_is_token(get_with_tk())) {
m_levels.append(m_explict_levels);
for (auto l : d_lvls) m_levels.push_back(l);
break;

2
src/frontends/lean/inductive_cmd.h
View file

@ -8,4 +8,6 @@ Author: Leonardo de Moura
#include "frontends/lean/cmd_table.h"
namespace lean {
void register_inductive_cmd(cmd_table & r);
void initialize_inductive_cmd();
void finalize_inductive_cmd();
}

12
src/frontends/lean/info_manager.cpp
View file

@ -75,8 +75,16 @@ struct tmp_info_data : public info_data_cell {
virtual void display(io_state_stream const &, unsigned) const { lean_unreachable(); } // LCOV_EXCL_LINE
};
static info_data g_dummy(new tmp_info_data(0));
info_data::info_data():info_data(g_dummy) {}
static info_data * g_dummy = nullptr;
void initialize_info_manager() {
g_dummy = new info_data(new tmp_info_data(0));
}
void finalize_info_manager() {
delete g_dummy;
}
info_data::info_data():info_data(*g_dummy) {}
info_data info_data::instantiate(substitution & s) const {
if (auto r = m_ptr->instantiate(s)) {

2
src/frontends/lean/info_manager.h
View file

@ -57,4 +57,6 @@ public:
void start_from(unsigned l);
unsigned get_processed_upto() const;
};
void initialize_info_manager();
void finalize_info_manager();
}

29
src/frontends/lean/init_module.cpp
View file

@ -15,12 +15,26 @@ Author: Leonardo de Moura
#include "frontends/lean/parser_config.h"
#include "frontends/lean/calc.h"
#include "frontends/lean/begin_end_ext.h"
#include "frontends/lean/builtin_cmds.h"
#include "frontends/lean/builtin_exprs.h"
#include "frontends/lean/inductive_cmd.h"
#include "frontends/lean/structure_cmd.h"
#include "frontends/lean/info_manager.h"
#include "frontends/lean/parse_table.h"
#include "frontends/lean/token_table.h"
#include "frontends/lean/scanner.h"
#include "frontends/lean/pp.h"
namespace lean {
void initialize_frontend_lean_module() {
initialize_tokens();
initialize_token_table();
initialize_parse_table();
initialize_builtin_cmds();
initialize_builtin_exprs();
initialize_elaborator();
initialize_pp_options();
initialize_scanner();
initialize_parser();
initialize_no_info();
initialize_extra_info();
@ -29,18 +43,31 @@ void initialize_frontend_lean_module() {
initialize_parser_config();
initialize_calc();
initialize_begin_end_ext();
initialize_inductive_cmd();
initialize_structure_cmd();
initialize_info_manager();
initialize_pp();
}
void finalize_frontend_lean_module() {
finalize_pp();
finalize_info_manager();
finalize_structure_cmd();
finalize_inductive_cmd();
finalize_begin_end_ext();
finalize_calc();
finalize_parser_config();
finalize_class();
finalize_tactic_hint();
finalize_tokens();
finalize_extra_info();
finalize_no_info();
finalize_parser();
finalize_scanner();
finalize_pp_options();
finalize_elaborator();
finalize_builtin_exprs();
finalize_builtin_cmds();
finalize_parse_table();
finalize_token_table();
finalize_tokens();
}
}

95
src/frontends/lean/notation_cmd.cpp
View file

@ -13,28 +13,9 @@ Author: Leonardo de Moura
#include "library/scoped_ext.h"
#include "library/explicit.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/tokens.h"
namespace lean {
static name g_max("max");
static name g_prev("prev");
static name g_colon(":");
static name g_comma(",");
static name g_assign(":=");
static name g_lparen("(");
static name g_rparen(")");
static name g_scoped("scoped");
static name g_foldr("foldr");
static name g_foldl("foldl");
static name g_binder("binder");
static name g_binders("binders");
static name g_infix("infix");
static name g_infixl("infixl");
static name g_infixr("infixr");
static name g_postfix("postfix");
static name g_prefix("prefix");
static name g_notation("notation");
static name g_call("call");
static std::string parse_symbol(parser & p, char const * msg) {
name n;
if (p.curr_is_identifier() || p.curr_is_quoted_symbol()) {
@ -51,7 +32,7 @@ static std::string parse_symbol(parser & p, char const * msg) {
static optional<unsigned> parse_optional_precedence(parser & p) {
if (p.curr_is_numeral()) {
return optional<unsigned>(p.parse_small_nat());
} else if (p.curr_is_token_or_id(g_max)) {
} else if (p.curr_is_token_or_id(get_max_tk())) {
p.next();
return optional<unsigned>(std::numeric_limits<unsigned>::max());
} else {
@ -68,7 +49,7 @@ static unsigned parse_precedence(parser & p, char const * msg) {
environment precedence_cmd(parser & p) {
std::string tk = parse_symbol(p, "invalid precedence declaration, quoted symbol or identifier expected");
p.check_token_next(g_colon, "invalid precedence declaration, ':' expected");
p.check_token_next(get_colon_tk(), "invalid precedence declaration, ':' expected");
unsigned prec = parse_precedence(p, "invalid precedence declaration, numeral or 'max' expected");
return add_token(p.env(), tk.c_str(), prec);
}
@ -136,7 +117,7 @@ using notation::action;
static pair<notation_entry, optional<token_entry>> parse_mixfix_notation(parser & p, mixfix_kind k, bool overload) {
std::string tk = parse_symbol(p, "invalid notation declaration, quoted symbol or identifier expected");
optional<unsigned> prec;
if (p.curr_is_token(g_colon)) {
if (p.curr_is_token(get_colon_tk())) {
p.next();
prec = parse_precedence(p, "invalid notation declaration, numeral or 'max' expected");
}
@ -153,7 +134,7 @@ static pair<notation_entry, optional<token_entry>> parse_mixfix_notation(parser
"solution: use the 'precedence' command", p.pos());
if (k == mixfix_kind::infixr && *prec == 0)
throw parser_error("invalid infixr declaration, precedence must be greater than zero", p.pos());
p.check_token_next(g_assign, "invalid notation declaration, ':=' expected");
p.check_token_next(get_assign_tk(), "invalid notation declaration, ':=' expected");
expr f = cleanup_section_notation(p, p.parse_expr());
char const * tks = tk.c_str();
switch (k) {
@ -197,7 +178,7 @@ static name parse_quoted_symbol_or_token(parser & p, buffer<token_entry> & new_t
auto tks = tk.to_string();
auto tkcs = tks.c_str();
p.next();
if (p.curr_is_token(g_colon)) {
if (p.curr_is_token(get_colon_tk())) {
p.next();
unsigned prec = parse_precedence(p, "invalid notation declaration, precedence (small numeral) expected");
auto old_prec = get_precedence(get_token_table(env), tkcs);
@ -221,13 +202,12 @@ static expr parse_notation_expr(parser & p, buffer<expr> const & locals) {
return cleanup_section_notation(p, abstract(r, locals.size(), locals.data()));
}
static expr g_local_type = mk_Prop(); // type used in notation local declarations, it is irrelevant
static void parse_notation_local(parser & p, buffer<expr> & locals) {
if (p.curr_is_identifier()) {
name n = p.get_name_val();
p.next();
expr l = mk_local(n, g_local_type); // remark: the type doesn't matter
expr local_type = mk_Prop(); // type used in notation local declarations, it is irrelevant
expr l = mk_local(n, local_type); // remark: the type doesn't matter
p.add_local_expr(n, l);
locals.push_back(l);
} else {
@ -249,63 +229,63 @@ unsigned get_precedence(environment const & env, buffer<token_entry> const & new
}
static action parse_action(parser & p, name const & prev_token, unsigned default_prec, buffer<expr> & locals, buffer<token_entry> & new_tokens) {
if (p.curr_is_token(g_colon)) {
if (p.curr_is_token(get_colon_tk())) {
p.next();
if (p.curr_is_numeral() || p.curr_is_token_or_id(g_max)) {
if (p.curr_is_numeral() || p.curr_is_token_or_id(get_max_tk())) {
unsigned prec = parse_precedence(p, "invalid notation declaration, small numeral expected");
return mk_expr_action(prec);
} else if (p.curr_is_token_or_id(g_prev)) {
} else if (p.curr_is_token_or_id(get_prev_tk())) {
p.next();
return mk_expr_action(get_precedence(p.env(), new_tokens, prev_token));
} else if (p.curr_is_string()) {
std::string fn = p.get_str_val();
p.next();
return mk_ext_lua_action(fn.c_str());
} else if (p.curr_is_token_or_id(g_scoped)) {
} else if (p.curr_is_token_or_id(get_scoped_tk())) {
p.next();
return mk_scoped_expr_action(mk_var(0));
} else {
p.check_token_next(g_lparen, "invalid notation declaration, '(', numeral or 'scoped' expected");
if (p.curr_is_token_or_id(g_foldl) || p.curr_is_token_or_id(g_foldr)) {
bool is_fold_right = p.curr_is_token_or_id(g_foldr);
p.check_token_next(get_lparen_tk(), "invalid notation declaration, '(', numeral or 'scoped' expected");
if (p.curr_is_token_or_id(get_foldl_tk()) || p.curr_is_token_or_id(get_foldr_tk())) {
bool is_fold_right = p.curr_is_token_or_id(get_foldr_tk());
p.next();
auto prec = parse_optional_precedence(p);
name sep = parse_quoted_symbol_or_token(p, new_tokens);
expr rec;
{
parser::local_scope scope(p);
p.check_token_next(g_lparen, "invalid fold notation argument, '(' expected");
p.check_token_next(get_lparen_tk(), "invalid fold notation argument, '(' expected");
parse_notation_local(p, locals);
parse_notation_local(p, locals);
p.check_token_next(g_comma, "invalid fold notation argument, ',' expected");
p.check_token_next(get_comma_tk(), "invalid fold notation argument, ',' expected");
rec = parse_notation_expr(p, locals);
p.check_token_next(g_rparen, "invalid fold notation argument, ')' expected");
p.check_token_next(get_rparen_tk(), "invalid fold notation argument, ')' expected");
locals.pop_back();
locals.pop_back();
}
expr ini = parse_notation_expr(p, locals);
optional<name> terminator;
if (!p.curr_is_token(g_rparen))
if (!p.curr_is_token(get_rparen_tk()))
terminator = parse_quoted_symbol_or_token(p, new_tokens);
p.check_token_next(g_rparen, "invalid fold notation argument, ')' expected");
p.check_token_next(get_rparen_tk(), "invalid fold notation argument, ')' expected");
return mk_exprs_action(sep, rec, ini, terminator, is_fold_right, prec ? *prec : 0);
} else if (p.curr_is_token_or_id(g_scoped)) {
} else if (p.curr_is_token_or_id(get_scoped_tk())) {
p.next();
auto prec = parse_optional_precedence(p);
expr rec;
{
parser::local_scope scope(p);
parse_notation_local(p, locals);
p.check_token_next(g_comma, "invalid scoped notation argument, ',' expected");
p.check_token_next(get_comma_tk(), "invalid scoped notation argument, ',' expected");
rec = parse_notation_expr(p, locals);
locals.pop_back();
}
p.check_token_next(g_rparen, "invalid scoped notation argument, ')' expected");
p.check_token_next(get_rparen_tk(), "invalid scoped notation argument, ')' expected");
return mk_scoped_expr_action(rec, prec ? *prec : 0);
} else if (p.curr_is_token_or_id(g_call)) {
} else if (p.curr_is_token_or_id(get_call_tk())) {
p.next();
name fn = p.check_id_next("invalid call notation argument, identifier expected");
p.check_token_next(g_rparen, "invalid call notation argument, ')' expected");
p.check_token_next(get_rparen_tk(), "invalid call notation argument, ')' expected");
return mk_ext_lua_action(fn.to_string().c_str());
} else {
throw parser_error("invalid notation declaration, 'foldl', 'foldr' or 'scoped' expected", p.pos());
@ -345,12 +325,12 @@ notation_entry parse_notation_core(parser & p, bool overload, buffer<token_entry
} else {
pt = get_nud_table(p.env());
}
while (!p.curr_is_token(g_assign)) {
while (!p.curr_is_token(get_assign_tk())) {
name tk = parse_quoted_symbol_or_token(p, new_tokens);
if (p.curr_is_token_or_id(g_binder)) {
if (p.curr_is_token_or_id(get_binder_tk())) {
p.next();
ts.push_back(transition(tk, mk_binder_action()));
} else if (p.curr_is_token_or_id(g_binders)) {
} else if (p.curr_is_token_or_id(get_binders_tk())) {
p.next();
ts.push_back(transition(tk, mk_binders_action()));
} else if (p.curr_is_identifier()) {
@ -358,11 +338,12 @@ notation_entry parse_notation_core(parser & p, bool overload, buffer<token_entry
name n = p.get_name_val();
p.next();
action a = parse_action(p, tk, default_prec, locals, new_tokens);
expr l = mk_local(n, g_local_type);
expr local_type = mk_Prop(); // type used in notation local declarations, it is irrelevant
expr l = mk_local(n, local_type);
p.add_local_expr(n, l);
locals.push_back(l);
ts.push_back(transition(tk, a));
} else if (p.curr_is_quoted_symbol() || p.curr_is_keyword() || p.curr_is_token(g_assign)) {
} else if (p.curr_is_quoted_symbol() || p.curr_is_keyword() || p.curr_is_token(get_assign_tk())) {
ts.push_back(transition(tk, mk_skip_action()));
} else {
throw parser_error("invalid notation declaration, quoted-symbol, identifier, 'binder', 'binders' expected", p.pos());
@ -401,24 +382,24 @@ environment notation_cmd_core(parser & p, bool overload) {
}
bool curr_is_notation_decl(parser & p) {
return p.curr_is_token(g_infix) || p.curr_is_token(g_infixl) || p.curr_is_token(g_infixr) ||
p.curr_is_token(g_postfix) || p.curr_is_token(g_prefix) || p.curr_is_token(g_notation);
return p.curr_is_token(get_infix_tk()) || p.curr_is_token(get_infixl_tk()) || p.curr_is_token(get_infixr_tk()) ||
p.curr_is_token(get_postfix_tk()) || p.curr_is_token(get_prefix_tk()) || p.curr_is_token(get_notation_tk());
}
notation_entry parse_notation(parser & p, bool overload, buffer<token_entry> & new_tokens) {
if (p.curr_is_token(g_infix) || p.curr_is_token(g_infixl)) {
if (p.curr_is_token(get_infix_tk()) || p.curr_is_token(get_infixl_tk())) {
p.next();
return parse_mixfix_notation(p, mixfix_kind::infixl, overload, new_tokens);
} else if (p.curr_is_token(g_infixr)) {
} else if (p.curr_is_token(get_infixr_tk())) {
p.next();
return parse_mixfix_notation(p, mixfix_kind::infixr, overload, new_tokens);
} else if (p.curr_is_token(g_postfix)) {
} else if (p.curr_is_token(get_postfix_tk())) {
p.next();
return parse_mixfix_notation(p, mixfix_kind::postfix, overload, new_tokens);
} else if (p.curr_is_token(g_prefix)) {
} else if (p.curr_is_token(get_prefix_tk())) {
p.next();
return parse_mixfix_notation(p, mixfix_kind::prefix, overload, new_tokens);
} else if (p.curr_is_token(g_notation)) {
} else if (p.curr_is_token(get_notation_tk())) {
p.next();
return parse_notation_core(p, overload, new_tokens);
} else {

31
src/frontends/lean/parse_table.cpp
View file

@ -213,21 +213,26 @@ void action_cell::dealloc() {
}
}
action mk_skip_action() {
static optional<action> r;
if (!r) r = action(new action_cell(action_kind::Skip));
return *r;
static action * g_skip_action = nullptr;
static action * g_binder_action = nullptr;
static action * g_binders_action = nullptr;
action mk_skip_action() { return *g_skip_action; }
action mk_binder_action() { return *g_binder_action; }
action mk_binders_action() { return *g_binders_action; }
void initialize_parse_table() {
g_skip_action = new action(new action_cell(action_kind::Skip));
g_binder_action = new action(new action_cell(action_kind::Binder));
g_binders_action = new action(new action_cell(action_kind::Binders));
}
action mk_binder_action() {
static optional<action> r;
if (!r) r = action(new action_cell(action_kind::Binder));
return *r;
}
action mk_binders_action() {
static optional<action> r;
if (!r) r = action(new action_cell(action_kind::Binders));
return *r;
void finalize_parse_table() {
delete g_binders_action;
delete g_binder_action;
delete g_skip_action;
}
action mk_expr_action(unsigned rbp) { return action(new expr_action_cell(rbp)); }
action mk_exprs_action(name const & sep, expr const & rec, expr const & ini,
optional<name> const & terminator, bool right, unsigned rbp) {

11
src/frontends/lean/parse_table.h
View file

@ -57,11 +57,10 @@ public:
action & operator=(action const & s);
action & operator=(action && s);
friend action mk_skip_action();
friend void initialize_parse_table();
friend action mk_expr_action(unsigned rbp);
friend action mk_exprs_action(name const & sep, expr const & rec, expr const & ini, optional<name> const & terminator, bool right, unsigned rbp);
friend action mk_binder_action();
friend action mk_binders_action();
friend action mk_exprs_action(name const & sep, expr const & rec, expr const & ini,
optional<name> const & terminator, bool right, unsigned rbp);
friend action mk_scoped_expr_action(expr const & rec, unsigned rbp, bool lambda);
friend action mk_ext_action(parse_fn const & fn);
friend action mk_ext_lua_action(char const * lua_fn);
@ -136,7 +135,11 @@ public:
void display(std::ostream & out) const;
};
void initialize_parse_table();
void finalize_parse_table();
}
typedef notation::parse_table parse_table;
void open_parse_table(lua_State * L);
inline void initialize_parse_table() { notation::initialize_parse_table(); }
inline void finalize_parse_table() { notation::finalize_parse_table(); }
}

120
src/frontends/lean/pp.cpp
View file

@ -27,25 +27,72 @@ Author: Leonardo de Moura
#include "frontends/lean/builtin_exprs.h"
namespace lean {
static format g_ellipsis_n_fmt = highlight(format("\u2026"));
static format g_ellipsis_fmt = highlight(format("..."));
static format g_placeholder_fmt = highlight(format("_"));
static format g_lambda_n_fmt = highlight_keyword(format("\u03BB"));
static format g_lambda_fmt = highlight_keyword(format("fun"));
static format g_forall_n_fmt = highlight_keyword(format("\u2200"));
static format g_forall_fmt = highlight_keyword(format("forall"));
static format g_pi_n_fmt = highlight_keyword(format("Π"));
static format g_pi_fmt = highlight_keyword(format("Pi"));
static format g_arrow_n_fmt = highlight_keyword(format("\u2192"));
static format g_arrow_fmt = highlight_keyword(format("->"));
static format g_let_fmt = highlight_keyword(format("let"));
static format g_in_fmt = highlight_keyword(format("in"));
static format g_assign_fmt = highlight_keyword(format(":="));
static format g_have_fmt = highlight_keyword(format("have"));
static format g_from_fmt = highlight_keyword(format("from"));
static format g_visible_fmt = highlight_keyword(format("[visible]"));
static format g_show_fmt = highlight_keyword(format("show"));
static format g_explicit_fmt = highlight_keyword(format("@"));
static format * g_ellipsis_n_fmt = nullptr;
static format * g_ellipsis_fmt = nullptr;
static format * g_placeholder_fmt = nullptr;
static format * g_lambda_n_fmt = nullptr;
static format * g_lambda_fmt = nullptr;
static format * g_forall_n_fmt = nullptr;
static format * g_forall_fmt = nullptr;
static format * g_pi_n_fmt = nullptr;
static format * g_pi_fmt = nullptr;
static format * g_arrow_n_fmt = nullptr;
static format * g_arrow_fmt = nullptr;
static format * g_let_fmt = nullptr;
static format * g_in_fmt = nullptr;
static format * g_assign_fmt = nullptr;
static format * g_have_fmt = nullptr;
static format * g_from_fmt = nullptr;
static format * g_visible_fmt = nullptr;
static format * g_show_fmt = nullptr;
static format * g_explicit_fmt = nullptr;
static name * g_tmp_prefix = nullptr;
void initialize_pp() {
g_ellipsis_n_fmt = new format(highlight(format("\u2026")));
g_ellipsis_fmt = new format(highlight(format("...")));
g_placeholder_fmt = new format(highlight(format("_")));
g_lambda_n_fmt = new format(highlight_keyword(format("\u03BB")));
g_lambda_fmt = new format(highlight_keyword(format("fun")));
g_forall_n_fmt = new format(highlight_keyword(format("\u2200")));
g_forall_fmt = new format(highlight_keyword(format("forall")));
g_pi_n_fmt = new format(highlight_keyword(format("Π")));
g_pi_fmt = new format(highlight_keyword(format("Pi")));
g_arrow_n_fmt = new format(highlight_keyword(format("\u2192")));
g_arrow_fmt = new format(highlight_keyword(format("->")));
g_let_fmt = new format(highlight_keyword(format("let")));
g_in_fmt = new format(highlight_keyword(format("in")));
g_assign_fmt = new format(highlight_keyword(format(":=")));
g_have_fmt = new format(highlight_keyword(format("have")));
g_from_fmt = new format(highlight_keyword(format("from")));
g_visible_fmt = new format(highlight_keyword(format("[visible]")));
g_show_fmt = new format(highlight_keyword(format("show")));
g_explicit_fmt = new format(highlight_keyword(format("@")));
g_tmp_prefix = new name(name::mk_internal_unique_name());
}
void finalize_pp() {
delete g_ellipsis_n_fmt;
delete g_ellipsis_fmt;
delete g_placeholder_fmt;
delete g_lambda_n_fmt;
delete g_lambda_fmt;
delete g_forall_n_fmt;
delete g_forall_fmt;
delete g_pi_n_fmt;
delete g_pi_fmt;
delete g_arrow_n_fmt;
delete g_arrow_fmt;
delete g_let_fmt;
delete g_in_fmt;
delete g_assign_fmt;
delete g_have_fmt;
delete g_from_fmt;
delete g_visible_fmt;
delete g_show_fmt;
delete g_explicit_fmt;
delete g_tmp_prefix;
}
name pretty_fn::mk_metavar_name(name const & m) {
if (auto it = m_purify_meta_table.find(m))
@ -162,7 +209,7 @@ auto pretty_fn::pp_coercion_fn(expr const & e, unsigned sz) -> result {
result res_fn = pp_coercion_fn(fn, sz-1);
format fn_fmt = res_fn.first;
if (m_implict && sz == 2 && has_implicit_args(fn))
fn_fmt = compose(g_explicit_fmt, fn_fmt);
fn_fmt = compose(*g_explicit_fmt, fn_fmt);
result res_arg = pp_child(app_arg(e), max_bp());
return mk_result(group(compose(fn_fmt, nest(m_indent, compose(line(), res_arg.first)))), max_bp()-1);
}
@ -272,9 +319,8 @@ auto pretty_fn::pp_local(expr const & e) -> result {
return mk_result(format(local_pp_name(e)));
}
static name g_tmp_prefix = name::mk_internal_unique_name();
bool pretty_fn::has_implicit_args(expr const & f) {
name_generator ngen(g_tmp_prefix);
name_generator ngen(*g_tmp_prefix);
try {
expr type = m_tc.whnf(m_tc.infer(f).first).first;
while (is_pi(type)) {
@ -295,7 +341,7 @@ auto pretty_fn::pp_app(expr const & e) -> result {
result res_fn = pp_child(fn, max_bp()-1);
format fn_fmt = res_fn.first;
if (m_implict && !is_app(fn) && has_implicit_args(fn))
fn_fmt = compose(g_explicit_fmt, fn_fmt);
fn_fmt = compose(*g_explicit_fmt, fn_fmt);
result res_arg = pp_child(app_arg(e), max_bp());
return mk_result(group(compose(fn_fmt, nest(m_indent, compose(line(), res_arg.first)))), max_bp()-1);
}
@ -352,7 +398,7 @@ auto pretty_fn::pp_lambda(expr const & e) -> result {
locals.push_back(p.second);
b = p.first;
}
format r = m_unicode ? g_lambda_n_fmt : g_lambda_fmt;
format r = m_unicode ? *g_lambda_n_fmt : *g_lambda_fmt;
r += pp_binders(locals);
r += compose(comma(), nest(m_indent, compose(line(), pp_child(b, 0).first)));
return mk_result(r, 0);
@ -369,7 +415,7 @@ auto pretty_fn::pp_pi(expr const & e) -> result {
if (is_default_arrow(e)) {
result lhs = pp_child(binding_domain(e), get_arrow_prec());
result rhs = pp_child(lift_free_vars(binding_body(e), 1), get_arrow_prec()-1);
format r = group(lhs.first + space() + (m_unicode ? g_arrow_n_fmt : g_arrow_fmt) + line() + rhs.first);
format r = group(lhs.first + space() + (m_unicode ? *g_arrow_n_fmt : *g_arrow_fmt) + line() + rhs.first);
return mk_result(r, get_arrow_prec()-1);
} else {
expr b = e;
@ -381,9 +427,9 @@ auto pretty_fn::pp_pi(expr const & e) -> result {
}
format r;
if (is_prop(b))
r = m_unicode ? g_forall_n_fmt : g_forall_fmt;
r = m_unicode ? *g_forall_n_fmt : *g_forall_fmt;
else
r = m_unicode ? g_pi_n_fmt : g_pi_fmt;
r = m_unicode ? *g_pi_n_fmt : *g_pi_fmt;
r += pp_binders(locals);
r += compose(comma(), nest(m_indent, compose(line(), pp_child(b, 0).first)));
return mk_result(r, 0);
@ -406,10 +452,10 @@ auto pretty_fn::pp_have(expr const & e) -> result {
format type_fmt = pp_child(mlocal_type(local), 0).first;
format proof_fmt = pp_child(proof, 0).first;
format body_fmt = pp_child(body, 0).first;
format r = g_have_fmt + space() + format(n) + space();
format r = *g_have_fmt + space() + format(n) + space();
if (binding_info(binding).is_contextual())
r += compose(g_visible_fmt, space());
r += colon() + nest(m_indent, line() + type_fmt + comma() + space() + g_from_fmt);
r += compose(*g_visible_fmt, space());
r += colon() + nest(m_indent, line() + type_fmt + comma() + space() + *g_from_fmt);
r = group(r);
r += nest(m_indent, line() + proof_fmt + comma());
r = group(r);
@ -424,7 +470,7 @@ auto pretty_fn::pp_show(expr const & e) -> result {
expr type = binding_domain(app_fn(s));
format type_fmt = pp_child(type, 0).first;
format proof_fmt = pp_child(proof, 0).first;
format r = g_show_fmt + space() + nest(5, type_fmt) + comma() + space() + g_from_fmt;
format r = *g_show_fmt + space() + nest(5, type_fmt) + comma() + space() + *g_from_fmt;
r = group(r);
r += nest(m_indent, compose(line(), proof_fmt));
return mk_result(group(r), 0);
@ -432,7 +478,7 @@ auto pretty_fn::pp_show(expr const & e) -> result {
auto pretty_fn::pp_explicit(expr const & e) -> result {
result res_arg = pp_child(get_explicit_arg(e), max_bp());
return mk_result(compose(g_explicit_fmt, res_arg.first), max_bp());
return mk_result(compose(*g_explicit_fmt, res_arg.first), max_bp());
}
auto pretty_fn::pp_macro(expr const & e) -> result {
@ -469,7 +515,7 @@ auto pretty_fn::pp_let(expr e) -> result {
}
if (decls.empty())
return pp(e);
format r = g_let_fmt;
format r = *g_let_fmt;
unsigned sz = decls.size();
for (unsigned i = 0; i < sz; i++) {
name const & n = decls[i].first;
@ -478,11 +524,11 @@ auto pretty_fn::pp_let(expr e) -> result {
format sep = i < sz - 1 ? comma() : format();
format entry = format(n);
format v_fmt = pp_child(v, 0).first;
entry += space() + g_assign_fmt + nest(m_indent, line() + v_fmt + sep);
entry += space() + *g_assign_fmt + nest(m_indent, line() + v_fmt + sep);
r += nest(3 + 1, beg + group(entry));
}
format b = pp_child(e, 0).first;
r += line() + g_in_fmt + space() + nest(2 + 1, b);
r += line() + *g_in_fmt + space() + nest(2 + 1, b);
return mk_result(r, 0);
}
@ -492,11 +538,11 @@ auto pretty_fn::pp_num(mpz const & n) -> result {
auto pretty_fn::pp(expr const & e) -> result {
if (m_depth > m_max_depth || m_num_steps > m_max_steps)
return mk_result(m_unicode ? g_ellipsis_n_fmt : g_ellipsis_fmt);
return mk_result(m_unicode ? *g_ellipsis_n_fmt : *g_ellipsis_fmt);
flet<unsigned> let_d(m_depth, m_depth+1);
m_num_steps++;
if (is_placeholder(e)) return mk_result(g_placeholder_fmt);
if (is_placeholder(e)) return mk_result(*g_placeholder_fmt);
if (is_show(e)) return pp_show(e);
if (is_have(e)) return pp_have(e);
if (is_let(e)) return pp_let(e);

2
src/frontends/lean/pp.h
View file

@ -88,4 +88,6 @@ public:
};
formatter_factory mk_pretty_formatter_factory();
void initialize_pp();
void finalize_pp();
}

44
src/frontends/lean/scanner.cpp
View file

@ -127,20 +127,21 @@ void scanner::check_not_eof(char const * error_msg) {
throw parser_exception(msg, m_stream_name.c_str(), line, pos);
}
static char const * g_end_error_str_msg = "unexpected end of string";
auto scanner::read_string() -> token_kind {
static char const * end_error_msg = "unexpected end of string";
lean_assert(curr() == '\"');
next();
m_buffer.clear();
while (true) {
check_not_eof(end_error_msg);
check_not_eof(g_end_error_str_msg);
char c = curr();
if (c == '\"') {
next();
return token_kind::String;
} else if (c == '\\') {
next();
check_not_eof(end_error_msg);
check_not_eof(g_end_error_str_msg);
c = curr();
if (c != '\\' && c != '\"' && c != 'n')
throw_exception("invalid escape sequence");
@ -248,20 +249,20 @@ bool scanner::consume(char const * str, char const * error_msg) {
static char const * g_begin_comment_block = "/-";
static char const * g_end_comment_block = "-/";
static char const * g_end_error_block_msg = "unexpected end of comment block";
void scanner::read_comment_block() {
static char const * end_error_msg = "unexpected end of comment block";
unsigned nesting = 1;
while (true) {
if (consume(g_begin_comment_block, end_error_msg)) {
if (consume(g_begin_comment_block, g_end_error_block_msg)) {
nesting++;
}
if (consume(g_end_comment_block, end_error_msg)) {
if (consume(g_end_comment_block, g_end_error_block_msg)) {
nesting--;
if (nesting == 0)
return;
}
check_not_eof(end_error_msg);
check_not_eof(g_end_error_block_msg);
next();
}
}
@ -346,8 +347,9 @@ static bool is_id_rest(buffer<char> const & cs, unsigned i) {
return is_letter_like_unicode(u) || is_super_sub_script_alnum_unicode(u);
}
static char const * g_error_key_msg = "unexpected token";
auto scanner::read_key_cmd_id() -> token_kind {
static char const * error_msg = "unexpected token";
buffer<char> cs;
next_utf_core(curr(), cs);
unsigned num_utfs = 1;
@ -410,7 +412,7 @@ auto scanner::read_key_cmd_id() -> token_kind {
}
if (id_sz == 0 && key_sz == 0)
throw_exception(error_msg);
throw_exception(g_error_key_msg);
if (id_sz > key_sz) {
move_back(cs.size() - id_sz, num_utfs - id_utf_sz);
m_name_val = name();
@ -433,9 +435,21 @@ auto scanner::read_key_cmd_id() -> token_kind {
}
}
static name g_begin_script_tk("(*");
static name g_begin_comment_tk("--");
static name g_begin_comment_block_tk("/-");
static name * g_begin_script_tk = nullptr;
static name * g_begin_comment_tk = nullptr;
static name * g_begin_comment_block_tk = nullptr;
void initialize_scanner() {
g_begin_script_tk = new name("(*");
g_begin_comment_tk = new name("--");
g_begin_comment_block_tk = new name("/-");
}
void finalize_scanner() {
delete g_begin_script_tk;
delete g_begin_comment_tk;
delete g_begin_comment_block_tk;
}
auto scanner::scan(environment const & env) -> token_kind {
m_tokens = &get_token_table(env);
@ -461,11 +475,11 @@ auto scanner::scan(environment const & env) -> token_kind {
if (k == token_kind::Keyword) {
// We treat '(--', '(*', '--' as "keywords.
name const & n = m_token_info->value();
if (n == g_begin_comment_tk)
if (n == *g_begin_comment_tk)
read_single_line_comment();
else if (n == g_begin_comment_block_tk)
else if (n == *g_begin_comment_block_tk)
read_comment_block();
else if (n == g_begin_script_tk)
else if (n == *g_begin_script_tk)
return read_script_block();
else
return k;

4
src/frontends/lean/scanner.h
View file

@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <string>
#include <iostream>
#include "util/name.h"
@ -11,7 +12,6 @@ Author: Leonardo de Moura
#include "kernel/environment.h"
#include "frontends/lean/token_table.h"
namespace lean {
/**
\brief Scanner. The behavior of the scanner is controlled using a token set.
@ -83,4 +83,6 @@ public:
std::string const & get_stream_name() const { return m_stream_name; }
};
std::ostream & operator<<(std::ostream & out, scanner::token_kind k);
void initialize_scanner();
void finalize_scanner();
}

39
src/frontends/lean/structure_cmd.cpp
View file

@ -19,19 +19,18 @@ Author: Leonardo de Moura
#include "frontends/lean/parser.h"
#include "frontends/lean/util.h"
#include "frontends/lean/decl_cmds.h"
#include "frontends/lean/tokens.h"
namespace lean {
static name g_assign(":=");
static name g_colon(":");
static name g_dcolon("::");
static name g_comma(",");
static name g_lparen("(");
static name g_rparen(")");
static name g_arrow("->");
static name g_extends("extends");
static name g_renaming("renaming");
static name * g_tmp_prefix = nullptr;
static name g_tmp_prefix = name::mk_internal_unique_name();
void initialize_structure_cmd() {
g_tmp_prefix = new name(name::mk_internal_unique_name());
}
void finalize_structure_cmd() {
delete g_tmp_prefix;
}
struct structure_cmd_fn {
typedef std::unique_ptr<type_checker> type_checker_ptr;
@ -55,7 +54,7 @@ struct structure_cmd_fn {
bool m_using_explicit_levels;
structure_cmd_fn(parser & p):m_p(p), m_env(p.env()), m_ngen(p.mk_ngen()), m_namespace(get_namespace(m_env)) {
name u_name(g_tmp_prefix, "u");
name u_name(*g_tmp_prefix, "u");
m_env = m_env.add_universe(u_name);
m_u = mk_global_univ(u_name);
m_infer_result_universe = false;
@ -75,29 +74,29 @@ struct structure_cmd_fn {
}
void parse_params() {
if (!m_p.curr_is_token(g_extends) && !m_p.curr_is_token(g_assign))
if (!m_p.curr_is_token(get_extends_tk()) && !m_p.curr_is_token(get_assign_tk()))
m_p.parse_binders(m_params);
for (expr const & l : m_params)
m_p.add_local(l);
}
void parse_extends() {
if (m_p.curr_is_token(g_extends)) {
if (m_p.curr_is_token(get_extends_tk())) {
m_p.next();
while (true) {
m_parents.push_back(m_p.parse_expr());
m_renames.push_back(rename_vector());
if (m_p.curr_is_token(g_renaming)) {
if (m_p.curr_is_token(get_renaming_tk())) {
m_p.next();
rename_vector & v = m_renames.back();
while (!m_p.curr_is_token(g_comma)) {
while (!m_p.curr_is_token(get_comma_tk())) {
name from = m_p.check_id_next("invalid 'renaming', identifier expected");
m_p.check_token_next(g_arrow, "invalid 'renaming', '->' expected");
m_p.check_token_next(get_arrow_tk(), "invalid 'renaming', '->' expected");
name to = m_p.check_id_next("invalid 'renaming', identifier expected");
v.emplace_back(from, to);
}
}
if (!m_p.curr_is_token(g_comma))
if (!m_p.curr_is_token(get_comma_tk()))
break;
m_p.next();
}
@ -106,7 +105,7 @@ struct structure_cmd_fn {
void parse_result_type() {
auto pos = m_p.pos();
if (m_p.curr_is_token(g_colon)) {
if (m_p.curr_is_token(get_colon_tk())) {
m_p.next();
m_type = m_p.parse_expr();
if (!is_sort(m_type))
@ -262,9 +261,9 @@ struct structure_cmd_fn {
parse_extends();
// TODO(Leo): process extends
parse_result_type();
m_p.check_token_next(g_assign, "invalid 'structure', ':=' expected");
m_p.check_token_next(get_assign_tk(), "invalid 'structure', ':=' expected");
m_mk = m_p.check_atomic_id_next("invalid 'structure', identifier expected");
m_p.check_token_next(g_dcolon, "invalid 'structure', '::' expected");
m_p.check_token_next(get_dcolon_tk(), "invalid 'structure', '::' expected");
m_p.parse_binders(m_fields, m_nentries);
m_type = Pi(m_params, m_type, m_p);
include_section_levels();

2
src/frontends/lean/structure_cmd.h
View file

@ -8,4 +8,6 @@ Author: Leonardo de Moura
#include "frontends/lean/cmd_table.h"
namespace lean {
void register_structure_cmd(cmd_table & r);
void initialize_structure_cmd();
void finalize_structure_cmd();
}

20
src/frontends/lean/token_table.cpp
View file

@ -67,8 +67,7 @@ static char const * g_arrow_unicode = "\u2192";
static char const * g_cup = "\u2294";
static char const * g_qed_unicode = "∎";
token_table init_token_table() {
token_table t;
void init_token_table(token_table & t) {
pair<char const *, unsigned> builtin[] =
{{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"have", 0}, {"show", 0}, {"obtain", 0}, {"by", 0}, {"then", 0},
{"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
@ -119,17 +118,22 @@ token_table init_token_table() {
t = add_command_token(t, it4->first, it4->second);
++it4;
}
return t;
}
static token_table * g_default_token_table = nullptr;
token_table mk_default_token_table() {
static optional<token_table> r;
if (!r)
r = init_token_table();
return *r;
return *g_default_token_table;
}
static token_table g_init(mk_default_token_table());
void initialize_token_table() {
g_default_token_table = new token_table();
init_token_table(*g_default_token_table);
}
void finalize_token_table() {
delete g_default_token_table;
}
token_table mk_token_table() { return token_table(); }

2
src/frontends/lean/token_table.h
View file

@ -49,4 +49,6 @@ optional<unsigned> get_precedence(token_table const & s, char const * token);
bool is_token(token_table const & s, char const * token);
token_info const * value_of(token_table const & s);
void open_token_table(lua_State * L);
void initialize_token_table();
void finalize_token_table();
}

148
src/frontends/lean/tokens.cpp
View file

@ -9,6 +9,7 @@ Author: Leonardo de Moura
namespace lean {
static name * g_period = nullptr;
static name * g_colon = nullptr;
static name * g_dcolon = nullptr;
static name * g_lparen = nullptr;
static name * g_rparen = nullptr;
static name * g_llevel_curly = nullptr;
@ -41,14 +42,51 @@ static name * g_decls = nullptr;
static name * g_hiding = nullptr;
static name * g_exposing = nullptr;
static name * g_renaming = nullptr;
static name * g_extends = nullptr;
static name * g_as = nullptr;
static name * g_on = nullptr;
static name * g_off = nullptr;
static name * g_none = nullptr;
static name * g_in = nullptr;
static name * g_assign = nullptr;
static name * g_visible = nullptr;
static name * g_from = nullptr;
static name * g_using = nullptr;
static name * g_then = nullptr;
static name * g_by = nullptr;
static name * g_proof = nullptr;
static name * g_qed = nullptr;
static name * g_end = nullptr;
static name * g_definition = nullptr;
static name * g_theorem = nullptr;
static name * g_axiom = nullptr;
static name * g_variable = nullptr;
static name * g_opaque = nullptr;
static name * g_instance = nullptr;
static name * g_coercion = nullptr;
static name * g_reducible = nullptr;
static name * g_with = nullptr;
static name * g_class = nullptr;
static name * g_prev = nullptr;
static name * g_scoped = nullptr;
static name * g_foldr = nullptr;
static name * g_foldl = nullptr;
static name * g_binder = nullptr;
static name * g_binders = nullptr;
static name * g_infix = nullptr;
static name * g_infixl = nullptr;
static name * g_infixr = nullptr;
static name * g_postfix = nullptr;
static name * g_prefix = nullptr;
static name * g_notation = nullptr;
static name * g_call = nullptr;
static name * g_persistent = nullptr;
static name * g_root = nullptr;
void initialize_tokens() {
g_period = new name(".");
g_colon = new name(":");
g_dcolon = new name("::");
g_lparen = new name("(");
g_rparen = new name(")");
g_llevel_curly = new name(".{");
@ -81,13 +119,84 @@ void initialize_tokens() {
g_hiding = new name("hiding");
g_exposing = new name("exposing");
g_renaming = new name("renaming");
g_extends = new name("extends");
g_as = new name("as");
g_on = new name("[on]");
g_off = new name("[off]");
g_none = new name("[none]");
g_in = new name("in");
g_assign = new name(":=");
g_visible = new name("[visible]");
g_from = new name("from");
g_using = new name("using");
g_then = new name("then");
g_by = new name("by");
g_proof = new name("proof");
g_qed = new name("qed");
g_end = new name("end");
g_definition = new name("definition");
g_theorem = new name("theorem");
g_opaque = new name("opaque");
g_axiom = new name("axiom");
g_variable = new name("variable");
g_instance = new name("[instance]");
g_coercion = new name("[coercion]");
g_reducible = new name("[reducible]");
g_with = new name("with");
g_class = new name("[class]");
g_prev = new name("prev");
g_scoped = new name("scoped");
g_foldr = new name("foldr");
g_foldl = new name("foldl");
g_binder = new name("binder");
g_binders = new name("binders");
g_infix = new name("infix");
g_infixl = new name("infixl");
g_infixr = new name("infixr");
g_postfix = new name("postfix");
g_prefix = new name("prefix");
g_notation = new name("notation");
g_call = new name("call");
g_persistent = new name("[persistent]");
g_root = new name("_root_");
}
void finalize_tokens() {
delete g_persistent;
delete g_root;
delete g_prev;
delete g_scoped;
delete g_foldr;
delete g_foldl;
delete g_binder;
delete g_binders;
delete g_infix;
delete g_infixl;
delete g_infixr;
delete g_postfix;
delete g_prefix;
delete g_notation;
delete g_call;
delete g_with;
delete g_class;
delete g_definition;
delete g_theorem;
delete g_opaque;
delete g_axiom;
delete g_variable;
delete g_instance;
delete g_coercion;
delete g_reducible;
delete g_in;
delete g_assign;
delete g_visible;
delete g_from;
delete g_using;
delete g_then;
delete g_by;
delete g_proof;
delete g_qed;
delete g_end;
delete g_raw;
delete g_true;
delete g_false;
@ -98,6 +207,7 @@ void finalize_tokens() {
delete g_hiding;
delete g_exposing;
delete g_renaming;
delete g_extends;
delete g_as;
delete g_on;
delete g_off;
@ -125,11 +235,13 @@ void finalize_tokens() {
delete g_rparen;
delete g_lparen;
delete g_colon;
delete g_dcolon;
delete g_period;
}
name const & get_period_tk() { return *g_period; }
name const & get_colon_tk() { return *g_colon; }
name const & get_dcolon_tk() { return *g_dcolon; }
name const & get_lparen_tk() { return *g_lparen; }
name const & get_rparen_tk() { return *g_rparen; }
name const & get_llevel_curly_tk() { return *g_llevel_curly; }
@ -162,8 +274,44 @@ name const & get_decls_tk() { return *g_decls; }
name const & get_hiding_tk() { return *g_hiding; }
name const & get_exposing_tk() { return *g_exposing; }
name const & get_renaming_tk() { return *g_renaming; }
name const & get_extends_tk() { return *g_extends; }
name const & get_as_tk() { return *g_as; }
name const & get_on_tk() { return *g_on; }
name const & get_off_tk() { return *g_off; }
name const & get_none_tk() { return *g_none; }
name const & get_in_tk() { return *g_in; }
name const & get_assign_tk() { return *g_assign; }
name const & get_visible_tk() { return *g_visible; }
name const & get_from_tk() { return *g_from; }
name const & get_using_tk() { return *g_using; }
name const & get_then_tk() { return *g_then; }
name const & get_by_tk() { return *g_by; }
name const & get_proof_tk() { return *g_proof; }
name const & get_qed_tk() { return *g_qed; }
name const & get_end_tk() { return *g_end; }
name const & get_definition_tk() { return *g_definition; }
name const & get_theorem_tk() { return *g_theorem; }
name const & get_axiom_tk() { return *g_axiom; }
name const & get_variable_tk() { return *g_variable; }
name const & get_opaque_tk() { return *g_opaque; }
name const & get_instance_tk() { return *g_instance; }
name const & get_coercion_tk() { return *g_coercion; }
name const & get_reducible_tk() { return *g_reducible; }
name const & get_class_tk() { return *g_class; }
name const & get_with_tk() { return *g_with; }
name const & get_prev_tk() { return *g_prev; }
name const & get_scoped_tk() { return *g_scoped; }
name const & get_foldr_tk() { return *g_foldr; }
name const & get_foldl_tk() { return *g_foldl; }
name const & get_binder_tk() { return *g_binder; }
name const & get_binders_tk() { return *g_binders; }
name const & get_infix_tk() { return *g_infix; }
name const & get_infixl_tk() { return *g_infixl; }
name const & get_infixr_tk() { return *g_infixr; }
name const & get_postfix_tk() { return *g_postfix; }
name const & get_prefix_tk() { return *g_prefix; }
name const & get_notation_tk() { return *g_notation; }
name const & get_call_tk() { return *g_call; }
name const & get_persistent_tk() { return *g_persistent; }
name const & get_root_tk() { return *g_root; }
}

37
src/frontends/lean/tokens.h
View file

@ -11,6 +11,7 @@ void initialize_tokens();
void finalize_tokens();
name const & get_period_tk();
name const & get_colon_tk();
name const & get_dcolon_tk();
name const & get_lparen_tk();
name const & get_rparen_tk();
name const & get_llevel_curly_tk();
@ -43,8 +44,44 @@ name const & get_decls_tk();
name const & get_hiding_tk();
name const & get_exposing_tk();
name const & get_renaming_tk();
name const & get_extends_tk();
name const & get_as_tk();
name const & get_on_tk();
name const & get_off_tk();
name const & get_none_tk();
name const & get_in_tk();
name const & get_assign_tk();
name const & get_visible_tk();
name const & get_from_tk();
name const & get_using_tk();
name const & get_then_tk();
name const & get_by_tk();
name const & get_proof_tk();
name const & get_qed_tk();
name const & get_end_tk();
name const & get_definition_tk();
name const & get_theorem_tk();
name const & get_axiom_tk();
name const & get_variable_tk();
name const & get_opaque_tk();
name const & get_instance_tk();
name const & get_coercion_tk();
name const & get_reducible_tk();
name const & get_class_tk();
name const & get_with_tk();
name const & get_prev_tk();
name const & get_scoped_tk();
name const & get_foldr_tk();
name const & get_foldl_tk();
name const & get_binder_tk();
name const & get_binders_tk();
name const & get_infix_tk();
name const & get_infixl_tk();
name const & get_infixr_tk();
name const & get_postfix_tk();
name const & get_prefix_tk();
name const & get_notation_tk();
name const & get_call_tk();
name const & get_persistent_tk();
name const & get_root_tk();
}

10
src/frontends/lean/util.cpp
View file

@ -15,12 +15,11 @@ Author: Leonardo de Moura
#include "library/locals.h"
#include "library/explicit.h"
#include "frontends/lean/parser.h"
#include "frontends/lean/tokens.h"
namespace lean {
static name g_persistent("[persistent]");
bool parse_persistent(parser & p, bool & persistent) {
if (p.curr_is_token_or_id(g_persistent)) {
if (p.curr_is_token_or_id(get_persistent_tk())) {
p.next();
persistent = true;
return true;
@ -38,12 +37,11 @@ void check_in_section_or_context(parser const & p) {
if (!in_section_or_context(p.env()))
throw exception(sstream() << "invalid command, it must be used in a section");
}
static name g_root("_root_");
bool is_root_namespace(name const & n) {
return n == g_root;
return n == get_root_tk();
}
name remove_root_prefix(name const & n) {
return n.replace_prefix(g_root, name());
return n.replace_prefix(get_root_tk(), name());
}
// Sort local_names by order of occurrence in the section, and copy the associated parameters to section_ps