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

refactor(parser): use 'scope objects' for creating local scopes and setting m_type_use_placeholder flag

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-16 09:24:41 -07:00
parent cb49e3719e
commit 775e10186d
3 changed files with 79 additions and 60 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -62,18 +62,6 @@ static void parse_univ_params(parser & p, buffer<name> & ps) {
}
}
struct local_scope_if_not_section {
parser & m_p;
local_scope_if_not_section(parser & p):m_p(p) {
if (!in_section(p.env()))
p.push_local_scope();
}
~local_scope_if_not_section() {
if (!in_section(m_p.env()))
m_p.pop_local_scope();
}
};
static void update_parameters(buffer<name> & ls_buffer, name_set const & found, parser const & p) {
unsigned old_sz = ls_buffer.size();
found.for_each([&](name const & n) {
@ -91,9 +79,11 @@ environment variable_cmd_core(parser & p, bool is_axiom, binder_info const & bi)
buffer<name> ls_buffer;
if (p.curr_is_token(g_llevel_curly) && in_section(p.env()))
throw parser_error("invalid declaration, axioms/parameters occurring in sections cannot be universe polymorphic", p.pos());
local_scope_if_not_section scope(p);
optional<parser::local_scope> scope1;
if (!in_section(p.env()))
scope1.emplace(p);
parse_univ_params(p, ls_buffer);
p.set_type_use_placeholder(false);
parser::param_universe_scope scope2(p);
expr type;
if (!p.curr_is_token(g_colon)) {
buffer<parameter> ps;
@ -201,24 +191,28 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque) {
expr type, value;
level_param_names ls;
{
parser::local_scope scope(p);
parser::local_scope scope1(p);
parse_univ_params(p, ls_buffer);
p.set_type_use_placeholder(false);
if (!p.curr_is_token(g_colon)) {
buffer<parameter> ps;
auto lenv = p.parse_binders(ps);
p.check_token_next(g_colon, "invalid declaration, ':' expected");
type = p.parse_scoped_expr(ps, lenv);
optional<local_environment> lenv;
{
parser::param_universe_scope scope2(p);
lenv = p.parse_binders(ps);
p.check_token_next(g_colon, "invalid declaration, ':' expected");
type = p.parse_scoped_expr(ps, *lenv);
}
p.check_token_next(g_assign, "invalid declaration, ':=' expected");
p.set_type_use_placeholder(true);
value = p.parse_scoped_expr(ps, lenv);
value = p.parse_scoped_expr(ps, *lenv);
type = p.pi_abstract(ps, type);
value = p.lambda_abstract(ps, value);
} else {
p.next();
type = p.parse_expr();
{
parser::param_universe_scope scope2(p);
type = p.parse_expr();
}
p.check_token_next(g_assign, "invalid declaration, ':=' expected");
p.set_type_use_placeholder(true);
value = p.parse_expr();
}
update_parameters(ls_buffer, collect_univ_params(value, collect_univ_params(type)), p);

65
src/frontends/lean/parser.cpp
View file

@ -39,6 +39,23 @@ RegisterBoolOption(g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS, "(lean
bool get_parser_show_errors(options const & opts) { return opts.get_bool(g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS); }
// ==========================================
parser::local_scope::local_scope(parser & p):
m_p(p), m_env(p.env()) {
p.push_local_scope();
}
parser::local_scope::~local_scope() {
m_p.pop_local_scope();
m_p.m_env = m_env;
}
parser::param_universe_scope::param_universe_scope(parser & p):m_p(p), m_old(m_p.m_type_use_placeholder) {
m_p.m_type_use_placeholder = false;
}
parser::param_universe_scope::~param_universe_scope() {
m_p.m_type_use_placeholder = m_old;
}
parser::parser(environment const & env, io_state const & ios,
std::istream & strm, char const * strm_name,
script_state * ss, bool use_exceptions,
@ -255,12 +272,14 @@ expr parser::mk_app(expr fn, expr arg, pos_info const & p) {
}
void parser::push_local_scope() {
m_local_level_decls.push();
if (m_type_use_placeholder)
m_local_level_decls.push();
m_local_decls.push();
}
void parser::pop_local_scope() {
m_local_level_decls.pop();
if (m_type_use_placeholder)
m_local_level_decls.pop();
m_local_decls.pop();
}
@ -530,21 +549,8 @@ void parser::parse_binders_core(buffer<parameter> & r) {
parse_binder_block(r, binder_info());
} else if (curr_is_token(g_lparen)) {
next();
if (curr_is_token(g_infix) || curr_is_token(g_infixl)) {
next();
m_env = infixl_cmd_core(*this, false);
} else if (curr_is_token(g_infixr)) {
next();
m_env = infixr_cmd_core(*this, false);
} else if (curr_is_token(g_postfix)) {
next();
m_env = postfix_cmd_core(*this, false);
} else if (curr_is_token(g_notation)) {
next();
m_env = notation_cmd_core(*this, false);
} else {
if (!parse_local_notation_decl())
parse_binder_block(r, binder_info());
}
check_token_next(g_rparen, "invalid binder, ')' expected");
} else if (curr_is_token(g_lcurly)) {
next();
@ -570,6 +576,28 @@ local_environment parser::parse_binders(buffer<parameter> & r) {
return local_environment(m_env);
}
bool parser::parse_local_notation_decl() {
if (curr_is_token(g_infix) || curr_is_token(g_infixl)) {
next();
m_env = infixl_cmd_core(*this, false);
return true;
} else if (curr_is_token(g_infixr)) {
next();
m_env = infixr_cmd_core(*this, false);
return true;
} else if (curr_is_token(g_postfix)) {
next();
m_env = postfix_cmd_core(*this, false);
return true;
} else if (curr_is_token(g_notation)) {
next();
m_env = notation_cmd_core(*this, false);
return true;
} else {
return false;
}
}
expr parser::parse_notation(parse_table t, expr * left) {
lean_assert(curr() == scanner::token_kind::Keyword);
auto p = pos();
@ -777,11 +805,11 @@ expr parser::parse_expr(unsigned rbp) {
}
expr parser::parse_scoped_expr(unsigned num_params, parameter const * ps, local_environment const & lenv, unsigned rbp) {
flet<environment> let(m_env, lenv.m_env);
if (num_params == 0) {
return parse_expr(rbp);
} else {
local_expr_decls::mk_scope scope(m_local_decls);
local_scope scope(*this);
m_env = lenv;
for (unsigned i = 0; i < num_params; i++)
add_local(ps[i].m_local);
return parse_expr(rbp);
@ -814,7 +842,6 @@ tactic parser::parse_tactic(unsigned /* rbp */) {
void parser::parse_command() {
lean_assert(curr() == scanner::token_kind::CommandKeyword);
flet<bool> save1(m_type_use_placeholder, m_type_use_placeholder);
m_last_cmd_pos = pos();
name const & cmd_name = get_token_info().value();
if (auto it = cmds().find(cmd_name)) {

34
src/frontends/lean/parser.h
View file

@ -43,11 +43,7 @@ struct parser_error : public exception {
struct interrupt_parser {};
typedef local_decls<parameter> local_expr_decls;
typedef local_decls<level> local_level_decls;
class local_environment {
friend parser;
environment m_env;
local_environment(environment const & env):m_env(env) {}
};
typedef environment local_environment;
class parser {
environment m_env;
@ -124,6 +120,12 @@ class parser {
void parse_binders_core(buffer<parameter> & r);
expr mk_app(expr fn, expr arg, pos_info const & p);
friend environment section_cmd(parser & p);
friend environment end_scoped_cmd(parser & p);
void push_local_scope();
void pop_local_scope();
public:
parser(environment const & env, io_state const & ios,
std::istream & strm, char const * str_name,
@ -185,6 +187,8 @@ public:
unsigned get_small_nat();
unsigned parse_small_nat();
bool parse_local_notation_decl();
level parse_level(unsigned rbp = 0);
parameter parse_binder();
@ -206,9 +210,7 @@ public:
tactic parse_tactic(unsigned rbp = 0);
void push_local_scope();
void pop_local_scope();
struct local_scope { parser & m_p; local_scope(parser & p):m_p(p) { p.push_local_scope(); } ~local_scope() { m_p.pop_local_scope(); } };
struct local_scope { parser & m_p; environment m_env; local_scope(parser & p); ~local_scope(); };
void add_local_level(name const & n, level const & l);
void add_local_expr(name const & n, expr const & e, binder_info const & bi = binder_info());
void add_local(expr const & t);
@ -219,17 +221,13 @@ public:
/** \brief Return the local parameter named \c n */
optional<parameter> get_local(name const & n) const;
/**
\brief Specify how the method mk_Type behaves. When <tt>set_type_use_placeholder(true)</tt>, then
it returns <tt>'Type.{_}'</tt>, where '_' is placeholder that instructs the Lean elaborator to
automalically infer a universe level expression for '_'. When <tt>set_type_use_placeholder(false)</tt>,
then it returns <tt>'Type.{l}'</tt>, where \c l is a fresh universe level parameter.
The new parameter is automatically added to \c m_local_level_decls.
\remark When the parse is created the flag is set to false.
\remark Before parsing a command, the parser automatically "caches" the current value, and
restores it after the command is parsed (or aborted).
\brief By default, \c mk_Type returns <tt>Type.{_}</tt> where '_' is a new placeholder.
This scope object allows us to temporarily change this behavior.
In any scope containing this object, \c mk_Type returns <tt>Type.{l}</tt>, where
\c l is a fresh universe level parameter.
The new parameter is automatically added to \c m_local_level_decls.
*/
void set_type_use_placeholder(bool f) { m_type_use_placeholder = f; }
struct param_universe_scope { parser & m_p; bool m_old; param_universe_scope(parser &); ~param_universe_scope(); };
expr mk_Type();
expr elaborate(expr const & e, level_param_names const &);