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

refactor(frontends/lean/parser): break parser in smaller chunks

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-02 06:46:28 -08:00
parent 7d18e9b32e
commit 5540fc861a
14 changed files with 3206 additions and 2895 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/frontends/lean/CMakeLists.txt
View file

@ -1,4 +1,7 @@
add_library(lean_frontend frontend.cpp operator_info.cpp scanner.cpp parser.cpp pp.cpp
frontend_elaborator.cpp register_module.cpp environment_scope.cpp coercion.cpp
shell.cpp)
add_library(lean_frontend frontend.cpp operator_info.cpp scanner.cpp
parser.cpp parser_imp.cpp parser_expr.cpp parser_error.cpp
parser_imp.cpp parser_cmds.cpp parser_level.cpp parser_tactic.cpp
parser_macros.cpp pp.cpp frontend_elaborator.cpp register_module.cpp
environment_scope.cpp coercion.cpp shell.cpp)
target_link_libraries(lean_frontend ${LEAN_LIBS})

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

File diff suppressed because it is too large Load diff

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

@ -12,12 +12,11 @@ Author: Leonardo de Moura
namespace lean {
class script_state;
class parser_imp;
/** \brief Functional object for parsing commands and expressions */
class parser {
public:
class imp;
private:
std::unique_ptr<imp> m_ptr;
std::unique_ptr<parser_imp> m_ptr;
public:
parser(environment const & env, io_state const & st, std::istream & in, script_state * S, bool use_exceptions = true, bool interactive = false);
parser(environment const & env, std::istream & in, script_state * S, bool use_exceptions = true, bool interactive = false);
@ -34,6 +33,5 @@ public:
bool parse_commands(environment const & env, io_state & st, std::istream & in, script_state * S = nullptr, bool use_exceptions = true, bool interactive = false);
expr parse_expr(environment const & env, io_state & st, std::istream & in, script_state * S = nullptr, bool use_exceptions = true);
void open_macros(lua_State * L);
}

819
src/frontends/lean/parser_cmds.cpp Normal file
View file

@ -0,0 +1,819 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <limits>
#include <utility>
#include <string>
#include "util/sstream.h"
#include "util/lean_path.h"
#include "util/sexpr/option_declarations.h"
#include "kernel/find_fn.h"
#include "kernel/kernel_exception.h"
#include "kernel/normalizer.h"
#include "kernel/type_checker.h"
#include "library/placeholder.h"
#include "frontends/lean/parser_imp.h"
#include "frontends/lean/frontend.h"
#include "frontends/lean/pp.h"
#include "frontends/lean/environment_scope.h"
namespace lean {
// ==========================================
// Builtin commands
static name g_alias_kwd("Alias");
static name g_definition_kwd("Definition");
static name g_variable_kwd("Variable");
static name g_variables_kwd("Variables");
static name g_theorem_kwd("Theorem");
static name g_axiom_kwd("Axiom");
static name g_universe_kwd("Universe");
static name g_eval_kwd("Eval");
static name g_show_kwd("Show");
static name g_check_kwd("Check");
static name g_infix_kwd("Infix");
static name g_infixl_kwd("Infixl");
static name g_infixr_kwd("Infixr");
static name g_notation_kwd("Notation");
static name g_echo_kwd("Echo");
static name g_set_option_kwd("SetOption");
static name g_set_opaque_kwd("SetOpaque");
static name g_options_kwd("Options");
static name g_env_kwd("Environment");
static name g_import_kwd("Import");
static name g_help_kwd("Help");
static name g_coercion_kwd("Coercion");
static name g_exit_kwd("Exit");
static name g_push_kwd("Push");
static name g_pop_kwd("Pop");
static name g_scope_kwd("Scope");
static name g_end_scope_kwd("EndScope");
static name g_builtin_kwd("Builtin");
static name g_namespace_kwd("Namespace");
static name g_end_namespace_kwd("EndNamespace");
/** \brief Table/List with all builtin command keywords */
static list<name> g_command_keywords = {g_definition_kwd, g_variable_kwd, g_variables_kwd, g_theorem_kwd, g_axiom_kwd, g_universe_kwd, g_eval_kwd,
g_show_kwd, g_check_kwd, g_infix_kwd, g_infixl_kwd, g_infixr_kwd, g_notation_kwd, g_echo_kwd,
g_set_option_kwd, g_set_opaque_kwd, g_env_kwd, g_options_kwd, g_import_kwd, g_help_kwd, g_coercion_kwd,
g_exit_kwd, g_push_kwd, g_pop_kwd, g_scope_kwd, g_end_scope_kwd, g_alias_kwd, g_builtin_kwd,
g_namespace_kwd, g_end_namespace_kwd};
// ==========================================
list<name> const & parser_imp::get_command_keywords() {
return g_command_keywords;
}
/**
\brief Register implicit arguments for the definition or
postulate named \c n. The fourth element in the tuple parameters
is a flag indiciating whether the argument is implicit or not.
*/
void parser_imp::register_implicit_arguments(name const & n, parameter_buffer & parameters) {
bool found = false;
buffer<bool> imp_args;
for (unsigned i = 0; i < parameters.size(); i++) {
imp_args.push_back(parameters[i].m_implicit);
if (imp_args.back())
found = true;
}
if (found)
mark_implicit_arguments(m_env, n, imp_args.size(), imp_args.data());
}
/** \brief Throw an exception if \c e contains a metavariable */
void parser_imp::check_no_metavar(expr const & e, metavar_env const & menv, char const * msg) {
auto m = find(e, [](expr const & e) -> bool { return is_metavar(e); });
if (m) {
auto p = get_metavar_ctx_and_type(*m, menv);
throw metavar_not_synthesized_exception(p.second, *m, p.first, msg);
}
}
void parser_imp::check_no_metavar(std::pair<expr, metavar_env> const & p, char const * msg) {
check_no_metavar(p.first, p.second, msg);
}
/**
\brief Return a fully qualified name (i.e., include current namespace)
*/
name parser_imp::mk_full_name(name const & n) {
return m_namespace_prefixes.back() + n;
}
/** \brief Auxiliary method used for parsing definitions and theorems. */
void parser_imp::parse_def_core(bool is_definition) {
next();
expr pre_type, pre_val;
name id = check_identifier_next("invalid definition, identifier expected");
parameter_buffer parameters;
if (curr_is_colon()) {
next();
pre_type = parse_expr();
if (!is_definition && curr_is_period()) {
pre_val = save(mk_placeholder(), pos());
} else {
check_assign_next("invalid definition, ':=' expected");
pre_val = parse_expr();
}
} else if (is_definition && curr_is_assign()) {
auto p = pos();
next();
pre_type = save(mk_placeholder(), p);
pre_val = parse_expr();
} else {
mk_scope scope(*this);
parse_definition_parameters(parameters);
expr type_body;
if (curr_is_colon()) {
next();
type_body = parse_expr();
} else {
auto p = pos();
type_body = save(mk_placeholder(), p);
}
pre_type = mk_abstraction(false, parameters, type_body);
if (!is_definition && curr_is_period()) {
pre_val = mk_abstraction(true, parameters, mk_placeholder());
} else {
check_assign_next("invalid definition, ':=' expected");
expr val_body = parse_expr();
pre_val = mk_abstraction(true, parameters, val_body);
}
}
auto r = m_elaborator(id, pre_type, pre_val);
expr type = std::get<0>(r);
expr val = std::get<1>(r);
metavar_env menv = std::get<2>(r);
check_no_metavar(type, menv, "invalid definition, type still contains metavariables after elaboration");
if (has_metavar(val)) {
val = apply_tactics(val, menv);
} else {
check_no_metavar(val, menv, "invalid definition, value still contains metavariables after elaboration");
}
lean_assert(!has_metavar(val));
name full_id = mk_full_name(id);
if (is_definition) {
m_env->add_definition(full_id, type, val);
if (m_verbose)
regular(m_io_state) << " Defined: " << full_id << endl;
} else {
m_env->add_theorem(full_id, type, val);
if (m_verbose)
regular(m_io_state) << " Proved: " << full_id << endl;
}
register_implicit_arguments(full_id, parameters);
}
/**
\brief Parse a Definition. It has one of the following two forms:
1) 'Definition' ID ':' expr ':=' expr
2) 'Definition' ID parameters ':' expr ':=' expr
*/
void parser_imp::parse_definition() {
parse_def_core(true);
}
/**
\brief Parse a Theorem. It has one of the following two forms:
1) 'Theorem' ID ':' expr ':=' expr
2) 'Theorem' ID parameters ':' expr ':=' expr
*/
void parser_imp::parse_theorem() {
parse_def_core(false);
}
/** \brief Auxiliary method for parsing Variable and axiom declarations. */
void parser_imp::parse_variable_core(bool is_var) {
next();
name id = check_identifier_next("invalid variable/axiom declaration, identifier expected");
parameter_buffer parameters;
expr type;
if (curr_is_colon()) {
next();
auto p = m_elaborator(parse_expr());
check_no_metavar(p, "invalid declaration, type still contains metavariables after elaboration");
type = p.first;
} else {
mk_scope scope(*this);
parse_var_decl_parameters(parameters);
check_colon_next("invalid variable/axiom declaration, ':' expected");
expr type_body = parse_expr();
auto p = m_elaborator(mk_abstraction(false, parameters, type_body));
check_no_metavar(p, "invalid declaration, type still contains metavariables after elaboration");
type = p.first;
}
name full_id = mk_full_name(id);
if (is_var)
m_env->add_var(full_id, type);
else
m_env->add_axiom(full_id, type);
if (m_verbose)
regular(m_io_state) << " Assumed: " << full_id << endl;
register_implicit_arguments(full_id, parameters);
}
/** \brief Parse one of the two forms:
1) 'Variable' ID ':' type
2) 'Variable' ID parameters ':' type
*/
void parser_imp::parse_variable() {
parse_variable_core(true);
}
/** \brief Parse the form:
'Variables' ID+ ':' type
*/
void parser_imp::parse_variables() {
next();
mk_scope scope(*this);
parameter_buffer parameters;
parse_simple_parameters(parameters, false, false);
for (auto p : parameters) {
name full_id = mk_full_name(p.m_name);
if (m_env->find_object(full_id))
throw already_declared_exception(m_env, full_id);
}
for (auto p : parameters) {
name full_id = mk_full_name(p.m_name);
expr const & type = p.m_type;
m_env->add_var(full_id, type);
if (m_verbose)
regular(m_io_state) << " Assumed: " << full_id << endl;
}
}
/** \brief Parse one of the two forms:
1) 'Axiom' ID ':' type
2) 'Axiom' ID parameters ':' type
*/
void parser_imp::parse_axiom() {
parse_variable_core(false);
}
/** \brief Parse 'Eval' expr */
void parser_imp::parse_eval() {
next();
expr v = m_elaborator(parse_expr()).first;
normalizer norm(m_env);
expr r = norm(v, context(), true);
regular(m_io_state) << r << endl;
}
/** \brief Return true iff \c obj is an object that should be ignored by the Show command */
bool parser_imp::is_hidden_object(object const & obj) const {
return (obj.is_definition() && is_explicit(m_env, obj.get_name())) || !supported_by_pp(obj);
}
/** \brief Parse
'Show' expr
'Show' Environment [num]
'Show' Environment all
'Show' Options
*/
void parser_imp::parse_show() {
next();
if (curr() == scanner::token::CommandId) {
name opt_id = curr_name();
next();
if (opt_id == g_env_kwd) {
buffer<object> to_display;
bool all = false;
unsigned end = m_env->get_num_objects(false);
unsigned i;
if (curr_is_nat()) {
i = parse_unsigned("invalid argument, value does not fit in a machine integer");
} else if (curr_is_identifier() && curr_name() == "all") {
next();
i = std::numeric_limits<unsigned>::max();
all = true;
} else {
i = std::numeric_limits<unsigned>::max();
}
unsigned it = end;
unsigned num_imports = 0;
while (it != 0 && i != 0) {
--it;
auto obj = m_env->get_object(it, false);
if (is_begin_import(obj)) {
lean_assert(num_imports > 0);
num_imports--;
if (num_imports == 0)
to_display.push_back(obj);
} else if (is_begin_builtin_import(obj)) {
lean_assert(num_imports > 0);
num_imports--;
} else if (is_end_import(obj)) {
num_imports++;
} else if (is_hidden_object(obj)) {
// skip
} else if (num_imports == 0 || all) {
to_display.push_back(obj);
--i;
}
}
std::reverse(to_display.begin(), to_display.end());
for (auto obj : to_display) {
if (is_begin_import(obj)) {
regular(m_io_state) << "Import \"" << *get_imported_module(obj) << "\"" << endl;
} else {
regular(m_io_state) << obj << endl;
}
}
} else if (opt_id == g_options_kwd) {
regular(m_io_state) << pp(m_io_state.get_options()) << endl;
} else {
throw parser_error("invalid Show command, expression, 'Options' or 'Environment' expected", m_last_cmd_pos);
}
} else {
expr v = m_elaborator(parse_expr()).first;
regular(m_io_state) << v << endl;
}
}
/** \brief Parse 'Check' expr */
void parser_imp::parse_check() {
next();
auto p = m_elaborator(parse_expr());
check_no_metavar(p, "invalid expression, it still contains metavariables after elaboration");
expr v = p.first;
expr t = type_check(v, m_env);
formatter fmt = m_io_state.get_formatter();
options opts = m_io_state.get_options();
unsigned indent = get_pp_indent(opts);
format r = group(format{fmt(v, opts), space(), colon(), nest(indent, compose(line(), fmt(t, opts)))});
regular(m_io_state) << mk_pair(r, opts) << endl;
}
/** \brief Return the (optional) precedence of a user-defined operator. */
unsigned parser_imp::parse_precedence() {
if (curr_is_nat()) {
return parse_unsigned("invalid operator definition, precedence does not fit in a machine integer");
} else {
return 0;
}
}
/** \brief Throw an error if the current token is not an identifier. If it is, move to next token. */
name parser_imp::parse_op_id() {
return check_identifier_next("invalid operator definition, identifier expected");
}
/**
\brief Parse prefix/postfix/infix/infixl/infixr user operator
definitions. These definitions have the form:
- fixity [Num] ID ':' ID
*/
void parser_imp::parse_op(fixity fx) {
next();
unsigned prec = parse_precedence();
name op_id = parse_op_id();
check_colon_next("invalid operator definition, ':' expected");
auto name_pos = pos();
name name_id = check_identifier_next("invalid operator definition, identifier expected");
expr d = get_name_ref(name_id, name_pos, false);
switch (fx) {
case fixity::Infix: add_infix(m_env, m_io_state, op_id, prec, d); break;
case fixity::Infixl: add_infixl(m_env, m_io_state, op_id, prec, d); break;
case fixity::Infixr: add_infixr(m_env, m_io_state, op_id, prec, d); break;
default: lean_unreachable(); // LCOV_EXCL_LINE
}
}
/**
\brief Parse notation declaration unified format
'Notation' [Num] parts ':' ID
*/
void parser_imp::parse_notation_decl() {
auto p = pos();
next();
unsigned prec = parse_precedence();
bool first = true;
bool prev_placeholder = false;
bool first_placeholder = false;
buffer<name> parts;
while (true) {
if (first) {
if (curr_is_placeholder()) {
prev_placeholder = true;
first_placeholder = true;
next();
} else {
parts.push_back(check_identifier_next("invalid notation declaration, identifier or '_' expected"));
prev_placeholder = false;
first_placeholder = false;
}
first = false;
} else {
if (curr_is_colon()) {
next();
if (parts.size() == 0) {
throw parser_error("invalid notation declaration, it must have at least one identifier", p);
}
auto id_pos = pos();
name name_id = check_identifier_next("invalid notation declaration, identifier expected");
expr d = get_name_ref(name_id, id_pos, false);
if (parts.size() == 1) {
if (first_placeholder && prev_placeholder) {
// infix: _ ID _
add_infix(m_env, m_io_state, parts[0], prec, d);
} else if (first_placeholder) {
// postfix: _ ID
add_postfix(m_env, m_io_state, parts[0], prec, d);
} else if (prev_placeholder) {
// prefix: ID _
add_prefix(m_env, m_io_state, parts[0], prec, d);
} else {
throw parser_error("invalid notation declaration, at least one placeholder expected", p);
}
} else {
if (first_placeholder && prev_placeholder) {
// mixfixo: _ ID ... ID _
add_mixfixo(m_env, m_io_state, parts.size(), parts.data(), prec, d);
} else if (first_placeholder) {
// mixfixr: _ ID ... ID
add_mixfixr(m_env, m_io_state, parts.size(), parts.data(), prec, d);
} else if (prev_placeholder) {
// mixfixl: ID _ ... ID _
add_mixfixl(m_env, m_io_state, parts.size(), parts.data(), prec, d);
} else {
// mixfixc: ID _ ... _ ID
add_mixfixc(m_env, m_io_state, parts.size(), parts.data(), prec, d);
}
}
return;
} else {
if (prev_placeholder) {
parts.push_back(check_identifier_next("invalid notation declaration, identifier or ':' expected"));
prev_placeholder = false;
} else {
check_placeholder_next("invalid notation declaration, '_' or ':' expected");
prev_placeholder = true;
}
}
}
}
}
/** Parse 'Echo' [string] */
void parser_imp::parse_echo() {
next();
std::string msg = check_string_next("invalid echo command, string expected");
regular(m_io_state) << msg << endl;
}
/** Parse 'SetOption' [id] [value] */
void parser_imp::parse_set_option() {
next();
auto id_pos = pos();
name id = check_identifier_next("invalid set options, identifier (i.e., option name) expected");
auto decl_it = get_option_declarations().find(id);
if (decl_it == get_option_declarations().end()) {
// add "lean" prefix
name lean_id = name("lean") + id;
decl_it = get_option_declarations().find(lean_id);
if (decl_it == get_option_declarations().end()) {
throw parser_error(sstream() << "unknown option '" << id << "', type 'Help Options.' for list of available options", id_pos);
} else {
id = lean_id;
}
}
option_kind k = decl_it->second.kind();
switch (curr()) {
case scanner::token::Id:
if (k != BoolOption)
throw parser_error(sstream() << "invalid option value, given option is not Boolean", pos());
if (curr_name() == "true")
m_io_state.set_option(id, true);
else if (curr_name() == "false")
m_io_state.set_option(id, false);
else
throw parser_error("invalid Boolean option value, 'true' or 'false' expected", pos());
next();
break;
case scanner::token::StringVal:
if (k != StringOption)
throw parser_error("invalid option value, given option is not a string", pos());
m_io_state.set_option(id, curr_string());
next();
break;
case scanner::token::IntVal:
if (k != IntOption && k != UnsignedOption)
throw parser_error("invalid option value, given option is not an integer", pos());
m_io_state.set_option(id, parse_unsigned("invalid option value, value does not fit in a machine integer"));
break;
case scanner::token::DecimalVal:
if (k != DoubleOption)
throw parser_error("invalid option value, given option is not floating point value", pos());
m_io_state.set_option(id, parse_double());
break;
default:
throw parser_error("invalid option value, 'true', 'false', string, integer or decimal value expected", pos());
}
updt_options();
if (m_verbose)
regular(m_io_state) << " Set: " << id << endl;
}
/** Parse 'SetOpaque' [id] [true/false] */
void parser_imp::parse_set_opaque() {
next();
name id;
if (curr() == scanner::token::Forall) {
id = "forall";
} else if (curr() == scanner::token::Exists) {
id = "exists";
} else {
check_identifier("invalid set opaque, identifier expected");
id = curr_name();
}
next();
name full_id = mk_full_name(id);
auto val_pos = pos();
name val = check_identifier_next("invalid opaque flag, true/false expected");
if (val == "true")
m_env->set_opaque(full_id, true);
else if (val == "false")
m_env->set_opaque(full_id, false);
else
throw parser_error("invalid opaque flag, true/false expected", val_pos);
}
optional<std::string> parser_imp::find_lua_file(std::string const & fname) {
try {
return some(find_file(fname, {".lua"}));
} catch (...) {
return optional<std::string>();
}
}
void parser_imp::parse_import() {
next();
std::string fname;
if (curr_is_identifier()) {
fname = name_to_file(curr_name());
next();
} else {
fname = check_string_next("invalid import command, string (i.e., file name) or identifier expected");
}
bool r = false;
if (auto lua_fname = find_lua_file(fname)) {
if (!m_script_state)
throw parser_error(sstream() << "failed to import Lua file '" << *lua_fname << "', parser does not have an intepreter",
m_last_cmd_pos);
r = m_script_state->import_explicit(lua_fname->c_str());
} else {
r = m_env->import(fname, m_io_state);
}
if (m_verbose && r) {
regular(m_io_state) << " Imported '" << fname << "'" << endl;
}
}
void parser_imp::parse_help() {
next();
if (curr() == scanner::token::CommandId) {
name opt_id = curr_name();
next();
if (opt_id == g_options_kwd) {
regular(m_io_state) << "Available options:" << endl;
for (auto p : get_option_declarations()) {
auto opt = p.second;
regular(m_io_state) << " " << opt.get_name() << " (" << opt.kind() << ") "
<< opt.get_description() << " (default: " << opt.get_default_value() << ")" << endl;
}
} else {
throw parser_error("invalid help command", m_last_cmd_pos);
}
} else {
regular(m_io_state) << "Available commands:" << endl
<< " Alias [id] : [expr] define an alias for the given expression" << endl
<< " Axiom [id] : [type] assert/postulate a new axiom" << endl
<< " Check [expr] type check the given expression" << endl
<< " Definition [id] : [type] := [expr] define a new element" << endl
<< " Echo [string] display the given string" << endl
<< " EndScope end the current scope and import its objects into the parent scope" << endl
<< " Eval [expr] evaluate the given expression" << endl
<< " Exit exit" << endl
<< " Help display this message" << endl
<< " Help Options display available options" << endl
<< " Help Notation describe commands for defining infix, mixfix, postfix operators" << endl
<< " Import [string] load the given file" << endl
<< " Push create a scope (it is just an alias for the command Scope)" << endl
<< " Pop discard the current scope" << endl
<< " Scope create a scope" << endl
<< " SetOption [id] [value] set option [id] with value [value]" << endl
<< " Show [expr] pretty print the given expression" << endl
<< " Show Options show current the set of assigned options" << endl
<< " Show Environment show objects in the environment, if [Num] provided, then show only the last [Num] objects" << endl
<< " Show Environment [num] show the last num objects in the environment" << endl
<< " Theorem [id] : [type] := [expr] define a new theorem" << endl
<< " Variable [id] : [type] declare/postulate an element of the given type" << endl
<< " Universe [id] [level] declare a new universe variable that is >= the given level" << endl;
#if !defined(LEAN_WINDOWS)
regular(m_io_state) << "Type Ctrl-D to exit" << endl;
#endif
}
}
/** \brief Parse 'Coercion' expr */
void parser_imp::parse_coercion() {
next();
expr coercion = parse_expr();
add_coercion(m_env, coercion);
if (m_verbose)
regular(m_io_state) << " Coercion " << coercion << endl;
}
void parser_imp::reset_env(environment env) {
m_env = env;
m_elaborator.reset(env);
m_io_state.set_formatter(mk_pp_formatter(env));
}
void parser_imp::parse_scope() {
next();
reset_env(m_env->mk_child());
}
void parser_imp::parse_pop() {
next();
if (!m_env->has_parent())
throw parser_error("main scope cannot be removed", m_last_cmd_pos);
reset_env(m_env->parent());
}
void parser_imp::parse_end_scope() {
next();
if (!m_env->has_parent())
throw parser_error("main scope cannot be removed", m_last_cmd_pos);
auto new_objects = export_local_objects(m_env);
reset_env(m_env->parent());
for (auto const & obj : new_objects) {
if (obj.is_theorem())
m_env->add_theorem(obj.get_name(), obj.get_type(), obj.get_value());
else
m_env->add_definition(obj.get_name(), obj.get_type(), obj.get_value(), obj.is_opaque());
}
}
void parser_imp::parse_cmd_macro(name cmd_id, pos_info const & p) {
lean_assert(m_cmd_macros && m_cmd_macros->find(cmd_id) != m_cmd_macros->end());
next();
auto m = m_cmd_macros->find(cmd_id)->second;
macro_arg_stack args;
parse_macro(m.m_arg_kinds, m.m_fn, m.m_precedence, args, p);
}
void parser_imp::parse_universe() {
next();
name id = check_identifier_next("invalid universe declaration, identifier expected");
check_colon_next("invalid universe declaration, ':' expected");
level lvl = parse_level();
m_env->add_uvar(id, lvl);
}
void parser_imp::parse_alias() {
next();
name id = check_identifier_next("invalid alias declaration, identifier expected");
check_colon_next("invalid alias declaration, ':' expected");
expr e = parse_expr();
add_alias(m_env, id, e);
}
void parser_imp::parse_builtin() {
next();
auto id_pos = pos();
name id = check_identifier_next("invalid builtin declaration, identifier expected");
name full_id = mk_full_name(id);
auto d = get_builtin(full_id);
if (!d)
throw parser_error(sstream() << "unknown builtin '" << full_id << "'", id_pos);
expr b = d->first;
if (d->second) {
m_env->add_builtin_set(b);
return;
}
parameter_buffer parameters;
expr type;
if (curr_is_colon()) {
next();
auto p = m_elaborator(parse_expr());
check_no_metavar(p, "invalid builtin declaration, type still contains metavariables after elaboration");
type = p.first;
} else {
mk_scope scope(*this);
parse_var_decl_parameters(parameters);
check_colon_next("invalid builtin declaration, ':' expected");
expr type_body = parse_expr();
auto p = m_elaborator(mk_abstraction(false, parameters, type_body));
check_no_metavar(p, "invalid declaration, type still contains metavariables after elaboration");
type = p.first;
}
if (to_value(b).get_type() != type) {
diagnostic(m_io_state) << "Error, builtin expected type: " << to_value(b).get_type() << ", given: " << type << "\n";
throw parser_error(sstream() << "given type does not match builtin type", id_pos);
}
m_env->add_builtin(d->first);
if (m_verbose)
regular(m_io_state) << " Added: " << full_id << endl;
register_implicit_arguments(full_id, parameters);
}
void parser_imp::parse_namespace() {
next();
name id = check_identifier_next("invalid namespace declaration, identifier expected");
m_namespace_prefixes.push_back(m_namespace_prefixes.back() + id);
}
void parser_imp::parse_end_namespace() {
next();
if (m_namespace_prefixes.size() <= 1)
throw parser_error("invalid end namespace command, there are no open namespaces", m_last_cmd_pos);
m_namespace_prefixes.pop_back();
}
/** \brief Parse a Lean command. */
bool parser_imp::parse_command() {
m_elaborator.clear();
m_expr_pos_info.clear();
m_tactic_hints.clear();
m_last_cmd_pos = pos();
name const & cmd_id = curr_name();
if (cmd_id == g_definition_kwd) {
parse_definition();
} else if (cmd_id == g_variable_kwd) {
parse_variable();
} else if (cmd_id == g_variables_kwd) {
parse_variables();
} else if (cmd_id == g_theorem_kwd) {
parse_theorem();
} else if (cmd_id == g_axiom_kwd) {
parse_axiom();
} else if (cmd_id == g_eval_kwd) {
parse_eval();
} else if (cmd_id == g_show_kwd) {
parse_show();
} else if (cmd_id == g_check_kwd) {
parse_check();
} else if (cmd_id == g_infix_kwd) {
parse_op(fixity::Infix);
} else if (cmd_id == g_infixl_kwd) {
parse_op(fixity::Infixl);
} else if (cmd_id == g_infixr_kwd) {
parse_op(fixity::Infixr);
} else if (cmd_id == g_notation_kwd) {
parse_notation_decl();
} else if (cmd_id == g_echo_kwd) {
parse_echo();
} else if (cmd_id == g_set_option_kwd) {
parse_set_option();
} else if (cmd_id == g_set_opaque_kwd) {
parse_set_opaque();
} else if (cmd_id == g_import_kwd) {
parse_import();
} else if (cmd_id == g_help_kwd) {
parse_help();
} else if (cmd_id == g_coercion_kwd) {
parse_coercion();
} else if (cmd_id == g_exit_kwd) {
next();
return false;
} else if (cmd_id == g_push_kwd || cmd_id == g_scope_kwd) {
parse_scope();
} else if (cmd_id == g_pop_kwd) {
parse_pop();
} else if (cmd_id == g_end_scope_kwd) {
parse_end_scope();
} else if (cmd_id == g_universe_kwd) {
parse_universe();
} else if (cmd_id == g_alias_kwd) {
parse_alias();
} else if (cmd_id == g_builtin_kwd) {
parse_builtin();
} else if (cmd_id == g_namespace_kwd) {
parse_namespace();
} else if (cmd_id == g_end_namespace_kwd) {
parse_end_namespace();
} else if (m_cmd_macros && m_cmd_macros->find(cmd_id) != m_cmd_macros->end()) {
parse_cmd_macro(cmd_id, m_last_cmd_pos);
} else {
next();
throw parser_error(sstream() << "invalid command '" << cmd_id << "'", m_last_cmd_pos);
}
return true;
}
}

164
src/frontends/lean/parser_error.cpp Normal file
View file

@ -0,0 +1,164 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <utility>
#include "kernel/kernel_exception.h"
#include "frontends/lean/parser_imp.h"
namespace lean {
void parser_imp::display_error_pos(unsigned line, unsigned pos) {
regular(m_io_state) << "Error (line: " << line;
if (pos != static_cast<unsigned>(-1))
regular(m_io_state) << ", pos: " << pos;
regular(m_io_state) << ")";
}
void parser_imp::display_error_pos(pos_info const & p) { display_error_pos(p.first, p.second); }
void parser_imp::display_error_pos(optional<expr> const & e) {
if (e) {
auto it = m_expr_pos_info.find(*e);
if (it == m_expr_pos_info.end())
return display_error_pos(m_last_cmd_pos);
else
return display_error_pos(it->second);
} else {
return display_error_pos(m_last_cmd_pos);
}
}
void parser_imp::display_error(char const * msg, unsigned line, unsigned pos) {
display_error_pos(line, pos);
regular(m_io_state) << " " << msg << endl;
}
void parser_imp::display_error(char const * msg) {
display_error(msg, m_scanner.get_line(), m_scanner.get_pos());
}
void parser_imp::display_error(kernel_exception const & ex) {
optional<expr> main_expr = ex.get_main_expr();
if (main_expr)
display_error_pos(some_expr(m_elaborator.get_original(*main_expr)));
else
display_error_pos(main_expr);
regular(m_io_state) << " " << ex << endl;
}
void parser_imp::display_error(metavar_not_synthesized_exception const & ex) {
display_error_pos(some_expr(m_elaborator.get_original(ex.m_mvar)));
regular(m_io_state) << " " << ex.what() << ", metavariable: " << ex.m_mvar << ", type:\n";
formatter fmt = m_io_state.get_formatter();
options opts = m_io_state.get_options();
regular(m_io_state) << mk_pair(fmt(ex.m_mvar_ctx, ex.m_mvar_type, true, opts), opts) << "\n";
}
std::pair<unsigned, unsigned> parser_imp::lean_pos_info_provider::get_pos_info(expr const & e) const {
expr const & o = m_ref.m_elaborator.get_original(e);
auto it = m_ref.m_expr_pos_info.find(o);
if (it == m_ref.m_expr_pos_info.end())
throw exception("position is not available"); // information is not available
return it->second;
}
void parser_imp::display_error(elaborator_exception const & ex) {
formatter fmt = m_io_state.get_formatter();
options opts = m_io_state.get_options();
lean_pos_info_provider pos_provider(*this);
regular(m_io_state) << mk_pair(ex.get_justification().pp(fmt, opts, &pos_provider, true), opts) << endl;
}
void parser_imp::display_error(script_exception const & ex) {
switch (ex.get_source()) {
case script_exception::source::String:
display_error_pos(ex.get_line() + m_last_script_pos.first - 1, static_cast<unsigned>(-1));
regular(m_io_state) << " executing script," << ex.get_msg() << endl;
break;
case script_exception::source::File:
display_error_pos(m_last_script_pos);
regular(m_io_state) << " executing external script (" << ex.get_filename() << ":" << ex.get_line() << ")," << ex.get_msg() << endl;
break;
case script_exception::source::Unknown:
display_error_pos(m_last_script_pos);
regular(m_io_state) << " executing script, exact error position is not available, " << ex.what() << endl;
break;
}
}
void parser_imp::display_error(tactic_cmd_error const & ex) {
display_error(ex.what(), ex.m_pos.first, ex.m_pos.second);
display_proof_state(ex.m_state);
}
/**
\brief Execute the given function \c f, and handle exceptions occurring
when executing \c f.
The parameter \c s is an error synchronization procedure.
*/
void parser_imp::protected_call(std::function<void()> && f, std::function<void()> && sync) {
try {
f();
} catch (tactic_cmd_error & ex) {
m_found_errors = true;
if (m_show_errors)
display_error(ex);
sync();
if (m_use_exceptions)
throw;
} catch (parser_error & ex) {
m_found_errors = true;
if (m_show_errors)
display_error(ex.what(), ex.m_pos.first, ex.m_pos.second);
sync();
if (m_use_exceptions) {
throw parser_exception(ex.what(), ex.m_pos.first, ex.m_pos.second);
}
} catch (kernel_exception & ex) {
m_found_errors = true;
if (m_show_errors)
display_error(ex);
sync();
if (m_use_exceptions)
throw;
} catch (elaborator_exception & ex) {
m_found_errors = true;
if (m_show_errors)
display_error(ex);
sync();
if (m_use_exceptions)
throw;
} catch (metavar_not_synthesized_exception & ex) {
m_found_errors = true;
if (m_show_errors)
display_error(ex);
sync();
if (m_use_exceptions)
throw;
} catch (script_exception & ex) {
m_found_errors = true;
reset_interrupt();
if (m_show_errors)
display_error(ex);
sync();
if (m_use_exceptions)
throw;
} catch (interrupted & ex) {
if (m_verbose)
regular(m_io_state) << "!!!Interrupted!!!" << endl;
reset_interrupt();
sync();
if (m_use_exceptions)
throw;
} catch (exception & ex) {
m_found_errors = true;
if (m_show_errors)
display_error(ex.what());
sync();
if (m_use_exceptions)
throw;
}
}
}

1001
src/frontends/lean/parser_expr.cpp Normal file
View file

File diff suppressed because it is too large Load diff

204
src/frontends/lean/parser_imp.cpp Normal file
View file

@ -0,0 +1,204 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <utility>
#include <string>
#include <vector>
#include "frontends/lean/parser_imp.h"
#include "frontends/lean/parser_macros.h"
#ifndef LEAN_DEFAULT_PARSER_SHOW_ERRORS
#define LEAN_DEFAULT_PARSER_SHOW_ERRORS true
#endif
#ifndef LEAN_DEFAULT_PARSER_VERBOSE
#define LEAN_DEFAULT_PARSER_VERBOSE true
#endif
namespace lean {
// ==========================================
// Parser configuration options
static name g_parser_verbose {"lean", "parser", "verbose"};
static name g_parser_show_errors {"lean", "parser", "show_errors"};
RegisterBoolOption(g_parser_verbose, LEAN_DEFAULT_PARSER_VERBOSE, "(lean parser) disable/enable parser verbose messages");
RegisterBoolOption(g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS, "(lean parser) display error messages in the regular output channel");
bool get_parser_verbose(options const & opts) { return opts.get_bool(g_parser_verbose, LEAN_DEFAULT_PARSER_VERBOSE); }
bool get_parser_show_errors(options const & opts) { return opts.get_bool(g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS); }
// ==========================================
parser_imp::mk_scope::mk_scope(parser_imp & fn):
m_fn(fn),
m_scope(fn.m_local_decls),
m_old_num_local_decls(fn.m_num_local_decls) {
}
parser_imp::mk_scope::~mk_scope() {
m_fn.m_num_local_decls = m_old_num_local_decls;
}
pos_info parser_imp::pos_of(expr const & e, pos_info default_pos) {
auto it = m_expr_pos_info.find(e);
if (it == m_expr_pos_info.end())
return default_pos;
else
return it->second;
}
void parser_imp::check_next(scanner::token t, char const * msg) {
if (curr() == t)
next();
else
throw parser_error(msg, pos());
}
/**
\brief Throws a parser error if the current token is not a
string. If it is, move to the next token.
*/
std::string parser_imp::check_string_next(char const * msg) {
if (curr() != scanner::token::StringVal)
throw parser_error(msg, pos());
std::string r = curr_string();
next();
return r;
}
unsigned parser_imp::parse_unsigned(char const * msg) {
lean_assert(curr_is_nat());
mpz pval = curr_num().get_numerator();
if (!pval.is_unsigned_int()) {
throw parser_error(msg, pos());
} else {
unsigned r = pval.get_unsigned_int();
next();
return r;
}
}
double parser_imp::parse_double() {
return 0.0;
}
[[ noreturn ]] void parser_imp::not_implemented_yet() {
// TODO(Leo)
throw parser_error("not implemented yet", pos());
}
void parser_imp::updt_options() {
m_verbose = get_parser_verbose(m_io_state.get_options());
m_show_errors = get_parser_show_errors(m_io_state.get_options());
}
/**
\brief Parse a block of Lua code. If as_expr is true, then
it appends the string "return " in front of the script.
*/
void parser_imp::parse_script(bool as_expr) {
m_last_script_pos = mk_pair(m_scanner.get_script_block_line(), m_scanner.get_script_block_pos());
if (!m_script_state)
throw exception("failed to execute Lua script, parser does not have a Lua interpreter");
std::string script_code = m_scanner.get_str_val();
if (as_expr) {
script_code = "return " + script_code;
}
next();
using_script([&](lua_State * L) {
dostring(L, script_code.c_str());
});
}
void parser_imp::parse_script_expr() { return parse_script(true); }
parser_imp::parser_imp(environment const & env, io_state const & st, std::istream & in,
script_state * S, bool use_exceptions, bool interactive):
m_env(env),
m_io_state(st),
m_scanner(in),
m_elaborator(env),
m_use_exceptions(use_exceptions),
m_interactive(interactive),
m_script_state(S),
m_set_parser(m_script_state, this) {
m_namespace_prefixes.push_back(name());
m_check_identifiers = true;
updt_options();
m_found_errors = false;
m_num_local_decls = 0;
m_scanner.set_command_keywords(get_command_keywords());
if (m_script_state) {
m_script_state->apply([&](lua_State * L) {
m_expr_macros = &get_expr_macros(L);
m_tactic_macros = &get_tactic_macros(L);
m_cmd_macros = &get_cmd_macros(L);
for (auto const & p : *m_cmd_macros) {
m_scanner.add_command_keyword(p.first);
}
});
} else {
m_expr_macros = nullptr;
m_tactic_macros = nullptr;
m_cmd_macros = nullptr;
}
scan();
}
void parser_imp::show_prompt(bool interactive, io_state const & ios) {
if (interactive) {
regular(ios) << "# ";
regular(ios).flush();
}
}
void parser_imp::show_prompt() {
show_prompt(m_interactive, m_io_state);
}
void parser_imp::show_tactic_prompt() {
if (m_interactive) {
regular(m_io_state) << "## ";
regular(m_io_state).flush();
}
}
/** \brief Parse a sequence of commands. This method also perform error management. */
bool parser_imp::parse_commands() {
bool done = false;
while (!done) {
protected_call([&]() {
check_interrupted();
switch (curr()) {
case scanner::token::CommandId: if (!parse_command()) done = true; break;
case scanner::token::ScriptBlock: parse_script(); break;
case scanner::token::Period: show_prompt(); next(); break;
case scanner::token::Eof: done = true; break;
default:
throw parser_error("Command expected", pos());
}
}, [&]() {
// Keep consuming tokens until we find a Command or End-of-file
show_prompt();
while (curr() != scanner::token::CommandId && curr() != scanner::token::Eof && curr() != scanner::token::Period)
next();
if (curr_is_period())
next();
});
}
return !m_found_errors;
}
/** \brief Parse an expression. */
expr parser_imp::parse_expr_main() {
try {
auto p = m_elaborator(parse_expr());
check_no_metavar(p, "invalid expression, it still contains metavariables after elaboration");
return p.first;
} catch (parser_error & ex) {
throw parser_exception(ex.what(), ex.m_pos.first, ex.m_pos.second);
}
}
};

432
src/frontends/lean/parser_imp.h Normal file
View file

@ -0,0 +1,432 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <utility>
#include <string>
#include <vector>
#include "util/name_map.h"
#include "util/scoped_map.h"
#include "util/script_exception.h"
#include "util/script_state.h"
#include "kernel/expr_maps.h"
#include "kernel/io_state.h"
#include "kernel/environment.h"
#include "library/kernel_bindings.h"
#include "library/tactic/tactic.h"
#include "library/elaborator/elaborator_exception.h"
#include "frontends/lean/scanner.h"
#include "frontends/lean/parser_types.h"
#include "frontends/lean/parser_error.h"
#include "frontends/lean/operator_info.h"
#include "frontends/lean/frontend_elaborator.h"
namespace lean {
class parser_imp;
bool get_parser_verbose(options const & opts);
bool get_parser_show_errors(options const & opts);
/** \brief Auxiliary object that stores a reference to the parser object inside the Lua State */
struct set_parser {
script_state * m_state;
parser_imp * m_prev;
set_parser(script_state * S, parser_imp * ptr);
~set_parser();
};
/**
\brief Actual implementation for the default Lean parser
\remark It is an instance of a Pratt parser
(http://en.wikipedia.org/wiki/Pratt_parser) described in the paper
"Top down operator precedence". This algorithm is super simple,
and it is easy to support user-defined infix/prefix/postfix/mixfix
operators.
*/
class parser_imp {
friend class parser;
friend int mk_cmd_macro(lua_State * L);
typedef scoped_map<name, unsigned, name_hash, name_eq> local_decls;
typedef name_map<expr> builtins;
typedef expr_map<pos_info> expr_pos_info;
typedef expr_map<tactic> tactic_hints; // a mapping from placeholder to tactic
environment m_env;
io_state m_io_state;
scanner m_scanner;
frontend_elaborator m_elaborator;
macros const * m_expr_macros;
macros const * m_cmd_macros;
macros const * m_tactic_macros;
scanner::token m_curr;
bool m_use_exceptions;
bool m_interactive;
bool m_found_errors;
local_decls m_local_decls;
unsigned m_num_local_decls;
expr_pos_info m_expr_pos_info;
pos_info m_last_cmd_pos;
pos_info m_last_script_pos;
tactic_hints m_tactic_hints;
std::vector<name> m_namespace_prefixes;
// If true then return error when parsing identifiers and it is not local or global.
// We set this flag off when parsing tactics. The apply_tac may reference
// a hypothesis in the proof state. This hypothesis is not visible until we
// execute the tactic.
bool m_check_identifiers;
script_state * m_script_state;
set_parser m_set_parser;
bool m_verbose;
bool m_show_errors;
template<typename F>
typename std::result_of<F(lua_State * L)>::type using_script(F && f) {
return m_script_state->apply([&](lua_State * L) {
set_io_state set1(L, m_io_state);
set_environment set2(L, m_env);
return f(L);
});
}
template<typename F>
void code_with_callbacks(F && f) {
m_script_state->apply([&](lua_State * L) {
set_io_state set1(L, m_io_state);
set_environment set2(L, m_env);
m_script_state->exec_unprotected([&]() {
f();
});
});
}
/**
\brief Auxiliar struct for creating/destroying a new scope for
local declarations.
*/
struct mk_scope {
parser_imp & m_fn;
local_decls::mk_scope m_scope;
unsigned m_old_num_local_decls;
mk_scope(parser_imp & fn);
~mk_scope();
};
public:
/** \brief Return the current position information */
pos_info pos() const { return mk_pair(m_scanner.get_line(), m_scanner.get_pos()); }
/** \brief Return the position associated with \c e. If there is none, then return \c default_pos. */
pos_info pos_of(expr const & e, pos_info default_pos);
/** \brief Associate position \c p with \c e and return \c e */
expr save(expr const & e, pos_info p) { m_expr_pos_info[e] = p; return e; }
/** \brief Read the next token. */
void scan() { m_curr = m_scanner.scan(); }
/** \brief Return the current token */
scanner::token curr() const { return m_curr; }
/** \brief Read the next token if the current one is not End-of-file. */
void next() { if (m_curr != scanner::token::Eof) scan(); }
/** \brief Return the name associated with the current token. */
name const & curr_name() const { return m_scanner.get_name_val(); }
/** \brief Return the numeral associated with the current token. */
mpq const & curr_num() const { return m_scanner.get_num_val(); }
/** \brief Return the string associated with the current token. */
std::string const & curr_string() const { return m_scanner.get_str_val(); }
/**
\brief Check if the current token is \c t, and move to the
next one. If the current token is not \c t, it throws a parser error.
*/
void check_next(scanner::token t, char const * msg);
/** \brief Return true iff the current token is an identifier */
bool curr_is_identifier() const { return curr() == scanner::token::Id; }
/** \brief Return true iff the current token is a '_" */
bool curr_is_placeholder() const { return curr() == scanner::token::Placeholder; }
/** \brief Return true iff the current token is a natural number */
bool curr_is_nat() const { return curr() == scanner::token::IntVal && m_scanner.get_num_val() >= 0; }
/** \brief Return true iff the current token is a '(' */
bool curr_is_lparen() const { return curr() == scanner::token::LeftParen; }
/** \brief Return true iff the current token is a '{' */
bool curr_is_lcurly() const { return curr() == scanner::token::LeftCurlyBracket; }
/** \brief Return true iff the current token is a ':' */
bool curr_is_colon() const { return curr() == scanner::token::Colon; }
/** \brief Return true iff the current token is a ',' */
bool curr_is_comma() const { return curr() == scanner::token::Comma; }
/** \brief Return true iff the current token is a ':=' */
bool curr_is_assign() const { return curr() == scanner::token::Assign; }
/** \brief Return true iff the current token is an 'in' token */
bool curr_is_in() const { return curr() == scanner::token::In; }
/** \brief Return true iff the current token is '.' */
bool curr_is_period() const { return curr() == scanner::token::Period; }
/** \brief Throws a parser error if the current token is not an identifier. */
void check_identifier(char const * msg) { if (!curr_is_identifier()) throw parser_error(msg, pos()); }
/**
\brief Throws a parser error if the current token is not an
identifier. If it is, move to the next token.
*/
name check_identifier_next(char const * msg) { check_identifier(msg); name r = curr_name(); next(); return r; }
/** \brief Throws a parser error if the current token is not '_'. If it is, move to the next token. */
void check_placeholder_next(char const * msg) { check_next(scanner::token::Placeholder, msg); }
/** \brief Throws a parser error if the current token is not ':'. If it is, move to the next token. */
void check_colon_next(char const * msg) { check_next(scanner::token::Colon, msg); }
/** \brief Throws a parser error if the current token is not ','. If it is, move to the next token. */
void check_comma_next(char const * msg) { check_next(scanner::token::Comma, msg); }
/** \brief Throws a parser error if the current token is not ')'. If it is, move to the next token. */
void check_rparen_next(char const * msg) { check_next(scanner::token::RightParen, msg); }
/** \brief Throws a parser error if the current token is not '}'. If it is, move to the next token. */
void check_rcurly_next(char const * msg) { check_next(scanner::token::RightCurlyBracket, msg); }
/** \brief Throws a parser error if the current token is not ':='. If it is, move to the next token. */
void check_assign_next(char const * msg) { check_next(scanner::token::Assign, msg); }
/** \brief Throws a parser error if the current token is not '.'. If it is, move to the next token. */
void check_period_next(char const * msg) { check_next(scanner::token::Period, msg); }
std::string check_string_next(char const * msg);
/**
@name Error handling
*/
/*@{*/
private:
void display_error_pos(unsigned line, unsigned pos);
void display_error_pos(pos_info const & p);
void display_error_pos(optional<expr> const & e);
void display_error(char const * msg, unsigned line, unsigned pos);
void display_error(char const * msg);
void display_error(kernel_exception const & ex);
void display_error(metavar_not_synthesized_exception const & ex);
struct lean_pos_info_provider : public pos_info_provider {
parser_imp const & m_ref;
lean_pos_info_provider(parser_imp const & r):m_ref(r) {}
virtual std::pair<unsigned, unsigned> get_pos_info(expr const & e) const;
};
void display_error(elaborator_exception const & ex);
void display_error(script_exception const & ex);
void display_error(tactic_cmd_error const & ex);
public:
void protected_call(std::function<void()> && f, std::function<void()> && sync);
/*@}*/
public:
unsigned parse_unsigned(char const * msg);
double parse_double();
private:
[[ noreturn ]] void not_implemented_yet();
void updt_options();
void parse_script(bool as_expr = false);
void parse_script_expr();
/**
@name Parse Universe levels
*/
/*@{*/
private:
level parse_level_max();
level parse_level_nud_id();
level parse_level_nud_int();
level parse_level_lparen();
level parse_level_nud();
level parse_level_led_plus(level const & left);
level parse_level_led_cup(level const & left);
level parse_level_led(level const & left);
unsigned curr_level_lbp();
public:
/** \brief Parse a universe level */
level parse_level(unsigned rbp = 0);
/*@}*/
/**
@name Parse Expressions
*/
/*@{*/
private:
unsigned get_implicit_vector_size(expr const & d);
std::vector<bool> const & get_smallest_implicit_vector(list<expr> const & ds);
unsigned get_smallest_implicit_vector_size(list<expr> const & ds);
expr mk_fun(operator_info const & op, pos_info const & pos);
expr mk_application(operator_info const & op, pos_info const & pos, unsigned num_args, expr const * args);
expr mk_application(operator_info const & op, pos_info const & pos, std::initializer_list<expr> const & l);
expr mk_application(operator_info const & op, pos_info const & pos, expr const & arg);
expr mk_application(operator_info const & op, pos_info const & pos, buffer<expr> const & args);
expr parse_prefix(operator_info const & op);
expr parse_postfix(expr const & left, operator_info const & op);
expr parse_infix(expr const & left, operator_info const & op);
expr parse_infixl(expr const & left, operator_info const & op);
expr parse_infixr(expr const & left, operator_info const & op);
void check_op_part(name const & op_part);
void parse_mixfix_args(list<name> const & ops, unsigned prec, buffer<expr> & args);
expr parse_mixfixl(operator_info const & op);
expr parse_mixfixr(expr const & left, operator_info const & op);
expr parse_mixfixo(expr const & left, operator_info const & op);
expr parse_mixfixc(operator_info const & op);
void propagate_position(expr const & e, pos_info p);
bool is_curr_begin_expr() const;
bool is_curr_begin_tactic() const;
typedef buffer<std::pair<macro_arg_kind, void*>> macro_arg_stack;
struct macro_result {
optional<expr> m_expr;
optional<tactic> m_tactic;
macro_result(expr const & e):m_expr(e) {}
macro_result(tactic const & t):m_tactic(t) {}
macro_result() {}
};
macro_result parse_macro(list<macro_arg_kind> const & arg_kinds, luaref const & fn, unsigned prec, macro_arg_stack & args,
pos_info const & p);
expr parse_expr_macro(name const & id, pos_info const & p);
expr parse_led_id(expr const & left);
expr parse_eq(expr const & left);
expr parse_arrow(expr const & left);
expr parse_lparen();
void parse_names(buffer<std::pair<pos_info, name>> & result);
void register_binding(name const & n);
void parse_simple_parameters(parameter_buffer & result, bool implicit_decl, bool suppress_type);
expr mk_abstraction(bool is_lambda, parameter_buffer const & parameters, expr const & body);
expr parse_abstraction(bool is_lambda);
expr parse_lambda();
expr parse_pi();
expr parse_quantifier(bool is_forall);
expr parse_forall();
expr parse_exists();
expr parse_let();
expr parse_type(bool level_expected);
tactic parse_tactic_macro(name tac_id, pos_info const & p);
expr parse_show_expr();
expr parse_nud_id();
expr parse_nud();
expr parse_led(expr const & left);
expr mk_app_left(expr const & left, expr const & arg);
unsigned curr_lbp();
expr parse_nat_int();
expr parse_decimal();
expr parse_string();
expr parse_by_expr();
public:
/**
\brief Try to find an object (Definition or Postulate) named \c
id in the frontend/environment. If there isn't one, then tries
to check if \c id is a builtin symbol. If it is not throws an error.
If \c implicit_args is true, then we also parse explicit arguments until
we have a placeholder forall implicit ones.
*/
expr get_name_ref(name const & id, pos_info const & p, bool implicit_args = true);
/**
\brief Parse a sequence of <tt>'(' ID ... ID ':' expr ')'</tt>.
This is used when parsing lambda, Pi, forall/exists expressions and
definitions.
\remark If implicit_decls is true, then we allow declarations
with curly braces. These declarations are used to tag implicit
arguments. Such as:
<code> Definition f {A : Type} (a b : A) : A := ... </code>
\see parse_simple_parameters
*/
void parse_parameters(parameter_buffer & result, bool implicit_decls, bool suppress_type);
/** \brief Parse parameters for expressions such as: lambda, pi, forall, exists */
void parse_expr_parameters(parameter_buffer & result);
void parse_var_decl_parameters(parameter_buffer & result);
void parse_definition_parameters(parameter_buffer & result);
/** \brief Parse a tactic expression, it can be
1) A Lua Script Block expression that returns a tactic
2) '(' expr ')' where expr is a proof term
3) identifier that is the name of a tactic or proof term.
*/
tactic parse_tactic_expr();
/** \brief Parse \c _ a hole that must be filled by the elaborator. */
expr parse_placeholder();
/** \brief Parse an expression */
expr parse_expr(unsigned rbp = 0);
/*@}*/
/**
@name Tactics
*/
/*@{*/
private:
/** \brief Return true iff the current token is a tactic command */
bool curr_is_tactic_cmd() const;
void display_proof_state(proof_state s);
void display_proof_state_if_interactive(proof_state s);
typedef std::vector<proof_state_seq> proof_state_seq_stack;
std::pair<proof_state, proof_state_seq> apply_tactic(proof_state const & s, tactic const & t, pos_info const & p);
expr mk_proof_for(proof_state const & s, pos_info const & p, context const & ctx, expr const & expected_type);
void back_cmd(/* inout */ proof_state_seq_stack & stack, /* inout */ proof_state & s);
void tactic_cmd(/* inout */ proof_state_seq_stack & stack, /* inout */ proof_state & s);
expr done_cmd(proof_state const & s, context const & ctx, expr const & expected_type);
expr parse_tactic_cmds(proof_state s, context const & ctx, expr const & expected_type);
std::pair<optional<tactic>, pos_info> get_tactic_for(expr const & mvar);
std::pair<expr, context> get_metavar_ctx_and_type(expr const & mvar, metavar_env const & menv);
expr apply_tactics(expr const & val, metavar_env & menv);
/*@}*/
private:
/**
@name Parse Commands
*/
/*@{*/
static list<name> const & get_command_keywords();
void register_implicit_arguments(name const & n, parameter_buffer & parameters);
void check_no_metavar(expr const & e, metavar_env const & menv, char const * msg);
void check_no_metavar(std::pair<expr, metavar_env> const & p, char const * msg);
name mk_full_name(name const & n);
void parse_def_core(bool is_definition);
void parse_definition();
void parse_theorem();
void parse_variable_core(bool is_var);
void parse_variable();
void parse_variables();
void parse_axiom();
void parse_eval();
bool is_hidden_object(object const & obj) const;
void parse_show();
void parse_check();
unsigned parse_precedence();
name parse_op_id();
void parse_op(fixity fx);
void parse_notation_decl();
void parse_echo();
void parse_set_option();
void parse_set_opaque();
optional<std::string> find_lua_file(std::string const & fname);
void parse_import();
void parse_help();
void parse_coercion();
void reset_env(environment env);
void parse_scope();
void parse_pop();
void parse_end_scope();
void parse_cmd_macro(name cmd_id, pos_info const & p);
void parse_universe();
void parse_alias();
void parse_builtin();
void parse_namespace();
void parse_end_namespace();
bool parse_command();
/*@}*/
public:
parser_imp(environment const & env, io_state const & st, std::istream & in, script_state * S, bool use_exceptions, bool interactive);
static void show_prompt(bool interactive, io_state const & ios);
void show_prompt();
void show_tactic_prompt();
/** \brief Parse a sequence of commands. This method also perform error management. */
bool parse_commands();
/** \brief Parse an expression. */
expr parse_expr_main();
};
}

118
src/frontends/lean/parser_level.cpp Normal file
View file

@ -0,0 +1,118 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "frontends/lean/parser_imp.h"
namespace lean {
// ==========================================
// Support for parsing levels
static name g_max_name("max");
static name g_cup_name("\u2294");
static name g_plus_name("+");
static unsigned g_level_plus_prec = 10;
static unsigned g_level_cup_prec = 5;
// ==========================================
/*
Parse Universe levels
*/
level parser_imp::parse_level_max() {
auto p = pos();
next();
buffer<level> lvls;
while (curr_is_identifier() || curr_is_nat()) {
lvls.push_back(parse_level());
}
if (lvls.size() < 2)
throw parser_error("invalid level expression, max must have at least two arguments", p);
level r = lvls[0];
for (unsigned i = 1; i < lvls.size(); i++)
r = max(r, lvls[i]);
return r;
}
level parser_imp::parse_level_nud_id() {
name id = curr_name();
if (id == g_max_name) {
return parse_level_max();
} else {
next();
return m_env->get_uvar(id);
}
}
level parser_imp::parse_level_nud_int() {
auto p = pos();
mpz val = curr_num().get_numerator();
next();
if (val < 0)
throw parser_error("invalid level expression, value is negative", p);
if (!val.is_unsigned_int())
throw parser_error("invalid level expression, value does not fit in a machine integer", p);
return level() + val.get_unsigned_int();
}
level parser_imp::parse_level_lparen() {
next();
level r = parse_level();
check_rparen_next("invalid level expression, ')' expected");
return r;
}
level parser_imp::parse_level_nud() {
switch (curr()) {
case scanner::token::Id: return parse_level_nud_id();
case scanner::token::IntVal: return parse_level_nud_int();
case scanner::token::LeftParen: return parse_level_lparen();
default:
throw parser_error("invalid level expression", pos());
}
}
level parser_imp::parse_level_led_plus(level const & left) {
auto p = pos();
next();
level right = parse_level(g_level_plus_prec);
if (!is_lift(right) || !lift_of(right).is_bottom())
throw parser_error("invalid level expression, right hand side of '+' (aka universe lift operator) must be a numeral", p);
return left + lift_offset(right);
}
level parser_imp::parse_level_led_cup(level const & left) {
next();
level right = parse_level(g_level_cup_prec);
return max(left, right);
}
level parser_imp::parse_level_led(level const & left) {
switch (curr()) {
case scanner::token::Id:
if (curr_name() == g_plus_name) return parse_level_led_plus(left);
else if (curr_name() == g_cup_name) return parse_level_led_cup(left);
default:
throw parser_error("invalid level expression", pos());
}
}
unsigned parser_imp::curr_level_lbp() {
switch (curr()) {
case scanner::token::Id: {
name const & id = curr_name();
if (id == g_plus_name) return g_level_plus_prec;
else if (id == g_cup_name) return g_level_cup_prec;
else return 0;
}
default: return 0;
}
}
level parser_imp::parse_level(unsigned rbp) {
level left = parse_level_nud();
while (rbp < curr_level_lbp()) {
left = parse_level_led(left);
}
return left;
}
}

140
src/frontends/lean/parser_macros.cpp Normal file
View file

@ -0,0 +1,140 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "frontends/lean/parser_imp.h"
#include "frontends/lean/notation.h"
namespace lean {
static char g_set_parser_key;
/** \brief Return a reference to the parser object */
parser_imp * get_parser(lua_State * L) {
lua_pushlightuserdata(L, static_cast<void *>(&g_set_parser_key));
lua_gettable(L, LUA_REGISTRYINDEX);
if (lua_islightuserdata(L, -1)) {
auto r = static_cast<parser_imp*>(lua_touserdata(L, -1));
lua_pop(L, 1);
return r;
}
lua_pop(L, 1);
return nullptr;
}
set_parser::set_parser(script_state * S, parser_imp * ptr) {
m_state = S;
if (m_state) {
m_state->apply([&](lua_State * L) {
m_prev = get_parser(L);
lua_pushlightuserdata(L, static_cast<void *>(&g_set_parser_key));
lua_pushlightuserdata(L, ptr);
lua_settable(L, LUA_REGISTRYINDEX);
});
}
}
set_parser::~set_parser() {
if (m_state) {
m_state->apply([&](lua_State * L) {
lua_pushlightuserdata(L, static_cast<void *>(&g_set_parser_key));
lua_pushlightuserdata(L, m_prev);
lua_settable(L, LUA_REGISTRYINDEX);
});
}
}
static char g_parser_expr_macros_key;
static char g_parser_tactic_macros_key;
static char g_parser_cmd_macros_key;
DECL_UDATA(macros)
macros & get_macros(lua_State * L, char * key) {
lua_pushlightuserdata(L, static_cast<void *>(key));
lua_gettable(L, LUA_REGISTRYINDEX);
if (lua_isnil(L, -1)) {
lua_pop(L, 1);
lua_pushlightuserdata(L, static_cast<void *>(key));
push_macros(L, macros());
lua_settable(L, LUA_REGISTRYINDEX);
lua_pushlightuserdata(L, static_cast<void *>(key));
lua_gettable(L, LUA_REGISTRYINDEX);
}
lean_assert(is_macros(L, -1));
macros & r = to_macros(L, -1);
lua_pop(L, 1);
return r;
}
macros & get_expr_macros(lua_State * L) { return get_macros(L, &g_parser_expr_macros_key); }
macros & get_tactic_macros(lua_State * L) { return get_macros(L, &g_parser_tactic_macros_key); }
macros & get_cmd_macros(lua_State * L) { return get_macros(L, &g_parser_cmd_macros_key); }
void mk_macro(lua_State * L, macros & mtable) {
int nargs = lua_gettop(L);
name macro_name = to_name_ext(L, 1);
unsigned prec = nargs == 4 ? lua_tointeger(L, 4) : g_app_precedence;
luaL_checktype(L, 3, LUA_TFUNCTION); // user-fun
buffer<macro_arg_kind> arg_kind_buffer;
int n = objlen(L, 2);
for (int i = 1; i <= n; i++) {
lua_rawgeti(L, 2, i);
arg_kind_buffer.push_back(static_cast<macro_arg_kind>(luaL_checkinteger(L, -1)));
lua_pop(L, 1);
}
list<macro_arg_kind> arg_kinds = to_list(arg_kind_buffer.begin(), arg_kind_buffer.end());
mtable.insert(mk_pair(macro_name, macro(arg_kinds, luaref(L, 3), prec)));
}
int mk_macro(lua_State * L) {
mk_macro(L, get_expr_macros(L));
return 0;
}
int mk_cmd_macro(lua_State * L) {
mk_macro(L, get_cmd_macros(L));
name macro_name = to_name_ext(L, 1);
parser_imp * ptr = get_parser(L);
if (!ptr)
throw exception("invalid cmd_macro, it is not in the context of a Lean parser");
// Make sure macro_name is a CommandId.
ptr->m_scanner.add_command_keyword(macro_name);
if (ptr->m_curr == scanner::token::Id && ptr->curr_name() == macro_name) {
ptr->m_curr = scanner::token::CommandId;
}
return 0;
}
int mk_tactic_macro(lua_State * L) {
mk_macro(L, get_tactic_macros(L));
return 0;
}
static const struct luaL_Reg macros_m[] = {
{"__gc", macros_gc}, // never throws
{0, 0}
};
void open_macros(lua_State * L) {
luaL_newmetatable(L, macros_mt);
lua_pushvalue(L, -1);
lua_setfield(L, -2, "__index");
setfuncs(L, macros_m, 0);
SET_GLOBAL_FUN(macros_pred, "is_macros");
SET_GLOBAL_FUN(mk_macro, "macro");
SET_GLOBAL_FUN(mk_cmd_macro, "cmd_macro");
SET_GLOBAL_FUN(mk_tactic_macro, "tactic_macro");
lua_newtable(L);
SET_ENUM("Expr", macro_arg_kind::Expr);
SET_ENUM("Exprs", macro_arg_kind::Exprs);
SET_ENUM("Parameters", macro_arg_kind::Parameters);
SET_ENUM("Id", macro_arg_kind::Id);
SET_ENUM("String", macro_arg_kind::String);
SET_ENUM("Int", macro_arg_kind::Int);
SET_ENUM("Comma", macro_arg_kind::Comma);
SET_ENUM("Assign", macro_arg_kind::Assign);
SET_ENUM("Tactic", macro_arg_kind::Tactic);
SET_ENUM("Tactics", macro_arg_kind::Tactics);
lua_setglobal(L, "macro_arg");
}
}

14
src/frontends/lean/parser_macros.h Normal file
View file

@ -0,0 +1,14 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "util/lua.h"
#include "frontends/lean/parser_types.h"
namespace lean {
macros & get_expr_macros(lua_State * L);
macros & get_tactic_macros(lua_State * L);
macros & get_cmd_macros(lua_State * L);
}

290
src/frontends/lean/parser_tactic.cpp Normal file
View file

@ -0,0 +1,290 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <utility>
#include <algorithm>
#include "kernel/for_each_fn.h"
#include "kernel/type_checker.h"
#include "kernel/type_checker_justification.h"
#include "kernel/unification_constraint.h"
#include "library/expr_lt.h"
#include "library/elaborator/elaborator.h"
#include "frontends/lean/parser_imp.h"
namespace lean {
static name g_apply("apply");
static name g_done("done");
static name g_back("back");
static name g_abort("abort");
static name g_assumption("assumption");
static list<name> g_tactic_cmds = { g_apply, g_done, g_back, g_abort, g_assumption };
bool parser_imp::curr_is_tactic_cmd() const {
return curr_is_identifier() && std::find(g_tactic_cmds.begin(), g_tactic_cmds.end(), curr_name()) != g_tactic_cmds.end();
}
void parser_imp::display_proof_state(proof_state s) {
regular(m_io_state) << "Proof state:\n" << s << endl;
}
void parser_imp::display_proof_state_if_interactive(proof_state s) {
if (m_interactive)
display_proof_state(s);
}
/**
\brief Apply tactic \c t to state \c s.
When \c t succeeds, it returns the head and tail of the output state sequence.
Throws an exception if the tactic fails, and use \c p to sign the error position.
*/
std::pair<proof_state, proof_state_seq> parser_imp::apply_tactic(proof_state const & s, tactic const & t, pos_info const & p) {
proof_state_seq::maybe_pair r;
code_with_callbacks([&]() {
// t may have call-backs we should set ios in the script_state
proof_state_seq seq = t(m_env, m_io_state, s);
r = seq.pull();
});
if (r) {
return mk_pair(r->first, r->second);
} else {
throw tactic_cmd_error("tactic failed", p, s);
}
}
/**
\brief Try to create a proof for the input state \c s.
It basically applies the proof_builder if \c s does not contain
any goals left. The position information is used to throw an exception
if \c s is not a final state.
The resultant proof must have type \c expected_type in the context \c ctx.
*/
expr parser_imp::mk_proof_for(proof_state const & s, pos_info const & p, context const & ctx, expr const & expected_type) {
if (s.is_proof_final_state()) {
assignment a(s.get_menv().copy());
proof_map m;
expr pr = s.get_proof_builder()(m, a);
if (has_metavar(pr)) {
// Some tactics generate metavariables that can only be instantiated by type inference elaboration.
// Example: apply_tactic.
metavar_env menv = s.get_menv().copy();
buffer<unification_constraint> ucs;
expr pr_type = type_checker(m_env).check(pr, ctx, menv, ucs);
ucs.push_back(mk_convertible_constraint(ctx, pr_type, expected_type, mk_type_match_justification(ctx, expected_type, pr)));
elaborator elb(m_env, menv, ucs.size(), ucs.data(), m_io_state.get_options());
metavar_env new_menv = elb.next();
pr = new_menv->instantiate_metavars(pr);
if (has_metavar(pr))
throw exception("synthesized proof object has unsolved metavars");
}
return pr;
} else {
throw tactic_cmd_error("invalid 'done' command, proof cannot be produced from this state", p, s);
}
}
/**
\brief Execute the \c back (backtrack) tactic command. It
succeeds if the stack \c stack contains proof states. When it
succeeds, \c s is updated with the next state in the state
sequence on the top of \c stack. The new state is also removed
from the stack.
*/
void parser_imp::back_cmd(/* inout */ proof_state_seq_stack & stack, /* inout */ proof_state & s) {
auto p = pos();
next();
while (!stack.empty()) {
check_interrupted();
lazy_list<proof_state> seq = stack.back();
stack.pop_back();
proof_state_seq::maybe_pair r;
code_with_callbacks([&]() {
r = seq.pull();
});
if (r) {
stack.push_back(r->second);
s = r->first;
return;
}
}
throw tactic_cmd_error("failed to backtrack", p, s);
}
/**
\brief Execute the tactic.
This command just applies the tactic to the input state \c s.
If it succeeds, \c s is assigned to the head of the output
state sequence produced by the tactic. The rest/tail of the
output state sequence is stored on the top of the stack \c
stack.
*/
void parser_imp::tactic_cmd(/* inout */ proof_state_seq_stack & stack, /* inout */ proof_state & s) {
auto tac_pos = pos();
tactic t = parse_tactic_expr();
auto r = apply_tactic(s, t, tac_pos);
s = r.first;
stack.push_back(r.second);
}
/**
\brief Execute the \c done tactic command. It succeeds if
a proof for \c s can be built.
*/
expr parser_imp::done_cmd(proof_state const & s, context const & ctx, expr const & expected_type) {
auto p = pos();
next();
return mk_proof_for(s, p, ctx, expected_type);
}
/**
\brief Parse tactic command sequence for solving input state \c s.
The proof for \c s must have type \c expected_type in the context \c ctx.
*/
expr parser_imp::parse_tactic_cmds(proof_state s, context const & ctx, expr const & expected_type) {
proof_state_seq_stack stack;
optional<expr> pr;
enum class status { Continue, Done, Eof, Abort };
status st = status::Continue;
while (st == status::Continue) {
protected_call(
[&]() {
auto p = pos();
check_interrupted();
name id;
switch (curr()) {
case scanner::token::Period:
display_proof_state_if_interactive(s);
show_tactic_prompt();
next();
break;
case scanner::token::Eof:
st = status::Eof;
break;
case scanner::token::Id:
id = curr_name();
if (id == g_back) {
back_cmd(stack, s);
} else if (id == g_done) {
pr = done_cmd(s, ctx, expected_type);
if (pr)
st = status::Done;
} else if (id == g_abort) {
next();
st = status::Abort;
} else {
tactic_cmd(stack, s);
}
break;
case scanner::token::ScriptBlock:
tactic_cmd(stack, s);
break;
case scanner::token::CommandId:
st = status::Abort;
break;
default:
next();
throw tactic_cmd_error("invalid tactic command, identifier expected", p, s);
}
},
[&]() {
// Keep consuming tokens until we find a Command or End-of-file or Tactic command
show_tactic_prompt();
while (curr() != scanner::token::CommandId && curr() != scanner::token::Eof &&
curr() != scanner::token::Period && !curr_is_tactic_cmd())
next();
if (curr_is_period())
next();
});
}
switch (st) {
case status::Done: return *pr;
case status::Eof: throw tactic_cmd_error("invalid tactic command, unexpected end of file", pos(), s);
case status::Abort: throw tactic_cmd_error("failed to prove theorem, proof has been aborted", pos(), s);
default: lean_unreachable(); // LCOV_EXCL_LINE
}
}
/**
\brief Return a 'hint' tactic (if it exists) for the given metavariable.
If the metavariable is not associated with any hint, then return the
null tactic. The method also returns the position of the hint.
*/
std::pair<optional<tactic>, pos_info> parser_imp::get_tactic_for(expr const & mvar) {
expr placeholder = m_elaborator.get_original(mvar);
auto it = m_tactic_hints.find(placeholder);
if (it != m_tactic_hints.end()) {
return mk_pair(some_tactic(it->second), pos_of(placeholder, pos()));
} else {
return mk_pair(none_tactic(), pos_of(placeholder, pos()));
}
}
std::pair<expr, context> parser_imp::get_metavar_ctx_and_type(expr const & mvar, metavar_env const & menv) {
expr mvar_type = menv->instantiate_metavars(menv->get_type(mvar));
buffer<context_entry> new_entries;
for (auto e : menv->get_context(mvar)) {
optional<expr> d = e.get_domain();
optional<expr> b = e.get_body();
if (d) d = menv->instantiate_metavars(*d);
if (b) b = menv->instantiate_metavars(*b);
if (d)
new_entries.emplace_back(e.get_name(), *d, b);
else
new_entries.emplace_back(e.get_name(), d, *b);
}
context mvar_ctx(new_entries.size(), new_entries.data());
return mk_pair(mvar_type, mvar_ctx);
}
/**
\brief Try to fill the 'holes' in \c val using tactics.
The metavar_env \c menv contains the definition of the metavariables occurring in \c val.
If a 'hole' is associated with a "hint tactic" ('show-by' and 'by' constructs),
then this will be the tactic used to "fill" the hole. Otherwise,
a tactic command sequence is expected in the input stream being parsed.
*/
expr parser_imp::apply_tactics(expr const & val, metavar_env & menv) {
buffer<expr> mvars;
for_each(val, [&](expr const & e, unsigned) {
if (is_metavar(e)) {
mvars.push_back(e);
}
return true;
});
std::sort(mvars.begin(), mvars.end(), [](expr const & e1, expr const & e2) { return is_lt(e1, e2, false); });
for (auto mvar : mvars) {
auto p = get_metavar_ctx_and_type(mvar, menv);
expr mvar_type = p.first;
context mvar_ctx = p.second;
if (has_metavar(mvar_type))
throw metavar_not_synthesized_exception(mvar_ctx, mvar, mvar_type,
"failed to synthesize metavar, its type contains metavariables");
try {
proof_state s = to_proof_state(m_env, mvar_ctx, mvar_type);
std::pair<optional<tactic>, pos_info> hint_and_pos = get_tactic_for(mvar);
if (hint_and_pos.first) {
// metavariable has an associated tactic hint
s = apply_tactic(s, *(hint_and_pos.first), hint_and_pos.second).first;
menv->assign(mvar, mk_proof_for(s, hint_and_pos.second, mvar_ctx, mvar_type));
} else {
if (curr_is_period()) {
display_proof_state_if_interactive(s);
show_tactic_prompt();
next();
}
expr mvar_val = parse_tactic_cmds(s, mvar_ctx, mvar_type);
menv->assign(mvar, mvar_val);
}
} catch (type_is_not_proposition_exception &) {
throw metavar_not_synthesized_exception(mvar_ctx, mvar, mvar_type, "failed to synthesize metavar, its type is not a proposition");
}
}
return menv->instantiate_metavars(val);
}
}

12
src/frontends/lean/parser_types.h
View file

@ -8,6 +8,9 @@ Author: Leonardo de Moura
#include <utility>
#include "util/name.h"
#include "util/buffer.h"
#include "util/list.h"
#include "util/luaref.h"
#include "util/name_map.h"
#include "kernel/expr.h"
namespace lean {
@ -22,4 +25,13 @@ struct parameter {
parameter():m_pos(0, 0), m_implicit(false) {}
};
typedef buffer<parameter> parameter_buffer;
enum class macro_arg_kind { Expr, Exprs, Parameters, Id, Int, String, Comma, Assign, Tactic, Tactics };
struct macro {
list<macro_arg_kind> m_arg_kinds;
luaref m_fn;
unsigned m_precedence;
macro(list<macro_arg_kind> const & as, luaref const & fn, unsigned prec):m_arg_kinds(as), m_fn(fn), m_precedence(prec) {}
};
typedef name_map<macro> macros;
}

1
src/frontends/lean/shell.cpp
View file

@ -12,6 +12,7 @@ Author: Leonardo de Moura
#include <unistd.h>
#include <algorithm>
#endif
#include <string>
#include "frontends/lean/shell.h"
#include "frontends/lean/pp.h"