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

refactor(frontends/lean): remove frontend class, it is not needed anymore

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-18 14:37:55 -08:00
parent 2aaa9a5273
commit 97b872a05c
14 changed files with 630 additions and 698 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

189
src/frontends/lean/frontend.cpp
View file

@ -26,6 +26,15 @@ Author: Leonardo de Moura
#include "frontends/lean/pp.h"
namespace lean {
/**
\brief Import all definitions and notation.
*/
void init_frontend(environment const & env, io_state & ios) {
ios.set_formatter(mk_pp_formatter(env));
import_all(env);
init_builtin_notation(env, ios);
}
static std::vector<bool> g_empty_vector;
/**
\brief Environment extension object for the Lean default frontend.
@ -160,23 +169,23 @@ struct lean_extension : public environment_extension {
l = cons(op, l);
}
void check_precedence(name const & n, unsigned prec, io_state & st) const {
void check_precedence(name const & n, unsigned prec, io_state const & ios) const {
auto old_prec = get_lbp(n);
if (old_prec && *old_prec != prec)
diagnostic(st) << "The precedence of '" << n << "' changed from " << *old_prec << " to " << prec << ".\n";
diagnostic(ios) << "The precedence of '" << n << "' changed from " << *old_prec << " to " << prec << ".\n";
}
/** \brief Register the new operator in the tables for parsing and pretty printing. */
void register_new_op(operator_info new_op, expr const & d, bool led, io_state & st) {
void register_new_op(operator_info new_op, expr const & d, bool led, io_state const & ios) {
new_op.add_expr(d);
insert_op(new_op, led);
insert_expr_to_operator_entry(d, new_op);
auto parts = new_op.get_op_name_parts();
auto prec = new_op.get_precedence();
if (led)
check_precedence(head(parts), prec, st);
check_precedence(head(parts), prec, ios);
for (name const & part : tail(parts)) {
check_precedence(part, prec, st);
check_precedence(part, prec, ios);
m_other_lbp[part] = prec;
}
}
@ -246,11 +255,11 @@ struct lean_extension : public environment_extension {
2) It is a real conflict, and report the issue in the
diagnostic channel, and override the existing operator (aka notation).
*/
void add_op(operator_info new_op, expr const & d, bool led, environment const & env, io_state & st) {
void add_op(operator_info new_op, expr const & d, bool led, environment const & env, io_state const & ios) {
name const & opn = new_op.get_op_name();
operator_info old_op = find_op(opn, led);
if (!old_op) {
register_new_op(new_op, d, led, st);
register_new_op(new_op, d, led, ios);
} else if (old_op == new_op) {
if (compatible_denotations(old_op, d)) {
// overload
@ -261,20 +270,20 @@ struct lean_extension : public environment_extension {
// we must copy the operator because it was defined in
// a parent frontend.
new_op = old_op.copy();
register_new_op(new_op, d, led, st);
register_new_op(new_op, d, led, ios);
}
} else {
diagnostic(st) << "The denotation(s) for the existing notation:\n " << old_op
<< "\nhave been replaced with the new denotation:\n " << d
<< "\nbecause they conflict on how implicit arguments are used.\n";
diagnostic(ios) << "The denotation(s) for the existing notation:\n " << old_op
<< "\nhave been replaced with the new denotation:\n " << d
<< "\nbecause they conflict on how implicit arguments are used.\n";
remove_bindings(old_op);
register_new_op(new_op, d, led, st);
register_new_op(new_op, d, led, ios);
}
} else {
diagnostic(st) << "Notation has been redefined, the existing notation:\n " << old_op
<< "\nhas been replaced with:\n " << new_op << "\nbecause they conflict with each other.\n";
diagnostic(ios) << "Notation has been redefined, the existing notation:\n " << old_op
<< "\nhas been replaced with:\n " << new_op << "\nbecause they conflict with each other.\n";
remove_bindings(old_op);
register_new_op(new_op, d, led, st);
register_new_op(new_op, d, led, ios);
}
env->add_neutral_object(new notation_declaration(new_op, d));
}
@ -432,26 +441,33 @@ static lean_extension & to_ext(environment const & env) {
return env->get_extension<lean_extension>(g_lean_extension_initializer.m_extid);
}
bool is_explicit(ro_environment const & env, name const & n) {
return to_ext(env).is_explicit(n);
void add_infix(environment const & env, io_state const & ios, name const & opn, unsigned p, expr const & d) {
to_ext(env).add_op(infix(opn, p), d, true, env, ios);
}
bool has_implicit_arguments(ro_environment const & env, name const & n) {
return to_ext(env).has_implicit_arguments(n);
void add_infixl(environment const & env, io_state const & ios, name const & opn, unsigned p, expr const & d) {
to_ext(env).add_op(infixl(opn, p), d, true, env, ios);
}
name const & get_explicit_version(ro_environment const & env, name const & n) {
return to_ext(env).get_explicit_version(n);
void add_infixr(environment const & env, io_state const & ios, name const & opn, unsigned p, expr const & d) {
to_ext(env).add_op(infixr(opn, p), d, true, env, ios);
}
std::vector<bool> const & get_implicit_arguments(ro_environment const & env, name const & n) {
return to_ext(env).get_implicit_arguments(n);
void add_prefix(environment const & env, io_state const & ios, name const & opn, unsigned p, expr const & d) {
to_ext(env).add_op(prefix(opn, p), d, false, env, ios);
}
bool is_coercion(ro_environment const & env, expr const & f) {
return to_ext(env).is_coercion(f);
void add_postfix(environment const & env, io_state const & ios, name const & opn, unsigned p, expr const & d) {
to_ext(env).add_op(postfix(opn, p), d, true, env, ios);
}
void add_mixfixl(environment const & env, io_state const & ios, unsigned sz, name const * opns, unsigned p, expr const & d) {
to_ext(env).add_op(mixfixl(sz, opns, p), d, false, env, ios);
}
void add_mixfixr(environment const & env, io_state const & ios, unsigned sz, name const * opns, unsigned p, expr const & d) {
to_ext(env).add_op(mixfixr(sz, opns, p), d, true, env, ios);
}
void add_mixfixc(environment const & env, io_state const & ios, unsigned sz, name const * opns, unsigned p, expr const & d) {
to_ext(env).add_op(mixfixc(sz, opns, p), d, false, env, ios);
}
void add_mixfixo(environment const & env, io_state const & ios, unsigned sz, name const * opns, unsigned p, expr const & d) {
to_ext(env).add_op(mixfixo(sz, opns, p), d, true, env, ios);
}
operator_info find_op_for(ro_environment const & env, expr const & n, bool unicode) {
operator_info r = to_ext(env).find_op_for(n, unicode);
if (r || !is_constant(n)) {
@ -464,110 +480,69 @@ operator_info find_op_for(ro_environment const & env, expr const & n, bool unico
return r;
}
}
frontend::frontend() {
m_state.set_formatter(mk_pp_formatter(m_env));
import_all(m_env);
init_builtin_notation(*this);
operator_info find_nud(ro_environment const & env, name const & n) {
return to_ext(env).find_nud(n);
}
frontend::frontend(environment const & env, io_state const & s):m_env(env), m_state(s) {
import_all(m_env);
init_builtin_notation(*this);
operator_info find_led(ro_environment const & env, name const & n) {
return to_ext(env).find_led(n);
}
void frontend::add_infix(name const & opn, unsigned p, expr const & d) {
to_ext(m_env).add_op(infix(opn, p), d, true, m_env, m_state);
optional<unsigned> get_lbp(ro_environment const & env, name const & n) {
return to_ext(env).get_lbp(n);
}
void frontend::add_infixl(name const & opn, unsigned p, expr const & d) {
to_ext(m_env).add_op(infixl(opn, p), d, true, m_env, m_state);
void mark_implicit_arguments(environment const & env, name const & n, unsigned sz, bool const * implicit) {
to_ext(env).mark_implicit_arguments(n, sz, implicit, env);
}
void frontend::add_infixr(name const & opn, unsigned p, expr const & d) {
to_ext(m_env).add_op(infixr(opn, p), d, true, m_env, m_state);
}
void frontend::add_prefix(name const & opn, unsigned p, expr const & d) {
to_ext(m_env).add_op(prefix(opn, p), d, false, m_env, m_state);
}
void frontend::add_postfix(name const & opn, unsigned p, expr const & d) {
to_ext(m_env).add_op(postfix(opn, p), d, true, m_env, m_state);
}
void frontend::add_mixfixl(unsigned sz, name const * opns, unsigned p, expr const & d) {
to_ext(m_env).add_op(mixfixl(sz, opns, p), d, false, m_env, m_state);
}
void frontend::add_mixfixr(unsigned sz, name const * opns, unsigned p, expr const & d) {
to_ext(m_env).add_op(mixfixr(sz, opns, p), d, true, m_env, m_state);
}
void frontend::add_mixfixc(unsigned sz, name const * opns, unsigned p, expr const & d) {
to_ext(m_env).add_op(mixfixc(sz, opns, p), d, false, m_env, m_state);
}
void frontend::add_mixfixo(unsigned sz, name const * opns, unsigned p, expr const & d) {
to_ext(m_env).add_op(mixfixo(sz, opns, p), d, true, m_env, m_state);
}
operator_info frontend::find_op_for(expr const & n, bool unicode) const {
return ::lean::find_op_for(m_env, n, unicode);
}
operator_info frontend::find_nud(name const & n) const {
return to_ext(m_env).find_nud(n);
}
operator_info frontend::find_led(name const & n) const {
return to_ext(m_env).find_led(n);
}
optional<unsigned> frontend::get_lbp(name const & n) const {
return to_ext(m_env).get_lbp(n);
}
void frontend::mark_implicit_arguments(name const & n, unsigned sz, bool const * implicit) {
to_ext(m_env).mark_implicit_arguments(n, sz, implicit, m_env);
}
void frontend::mark_implicit_arguments(name const & n, unsigned prefix_sz) {
void mark_implicit_arguments(environment const & env, name const & n, unsigned prefix_sz) {
buffer<bool> implicit; implicit.resize(prefix_sz, true);
mark_implicit_arguments(n, implicit.size(), implicit.data());
mark_implicit_arguments(env, n, implicit.size(), implicit.data());
}
void frontend::mark_implicit_arguments(expr const & n, unsigned prefix_sz) {
void mark_implicit_arguments(environment const & env, expr const & n, unsigned prefix_sz) {
if (is_constant(n)) {
mark_implicit_arguments(const_name(n), prefix_sz);
mark_implicit_arguments(env, const_name(n), prefix_sz);
} else {
lean_assert(is_value(n));
mark_implicit_arguments(to_value(n).get_name(), prefix_sz);
mark_implicit_arguments(env, to_value(n).get_name(), prefix_sz);
}
}
void frontend::mark_implicit_arguments(name const & n, std::initializer_list<bool> const & l) {
mark_implicit_arguments(n, l.size(), l.begin());
void mark_implicit_arguments(environment const & env, name const & n, std::initializer_list<bool> const & l) {
mark_implicit_arguments(env, n, l.size(), l.begin());
}
void frontend::mark_implicit_arguments(expr const & n, std::initializer_list<bool> const & l) {
void mark_implicit_arguments(environment const & env, expr const & n, std::initializer_list<bool> const & l) {
if (is_constant(n)) {
mark_implicit_arguments(const_name(n), l);
mark_implicit_arguments(env, const_name(n), l);
} else {
lean_assert(is_value(n));
mark_implicit_arguments(to_value(n).get_name(), l);
mark_implicit_arguments(env, to_value(n).get_name(), l);
}
}
bool frontend::has_implicit_arguments(name const & n) const {
return to_ext(m_env).has_implicit_arguments(n);
bool has_implicit_arguments(ro_environment const & env, name const & n) {
return to_ext(env).has_implicit_arguments(n);
}
std::vector<bool> const & frontend::get_implicit_arguments(name const & n) const {
return to_ext(m_env).get_implicit_arguments(n);
std::vector<bool> const & get_implicit_arguments(ro_environment const & env, name const & n) {
return to_ext(env).get_implicit_arguments(n);
}
std::vector<bool> const & frontend::get_implicit_arguments(expr const & n) const {
std::vector<bool> const & get_implicit_arguments(ro_environment const & env, expr const & n) {
if (is_constant(n))
return get_implicit_arguments(const_name(n));
return get_implicit_arguments(env, const_name(n));
else
return g_empty_vector;
}
name const & frontend::get_explicit_version(name const & n) const {
return to_ext(m_env).get_explicit_version(n);
name const & get_explicit_version(ro_environment const & env, name const & n) {
return to_ext(env).get_explicit_version(n);
}
bool frontend::is_explicit(name const & n) const {
return to_ext(m_env).is_explicit(n);
bool is_explicit(ro_environment const & env, name const & n) {
return to_ext(env).is_explicit(n);
}
void frontend::add_coercion(expr const & f) {
to_ext(m_env).add_coercion(f, m_env);
void add_coercion(environment const & env, expr const & f) {
to_ext(env).add_coercion(f, env);
}
optional<expr> frontend::get_coercion(expr const & from_type, expr const & to_type) const {
return to_ext(m_env).get_coercion(from_type, to_type);
optional<expr> get_coercion(ro_environment const & env, expr const & from_type, expr const & to_type) {
return to_ext(env).get_coercion(from_type, to_type);
}
list<expr_pair> frontend::get_coercions(expr const & from_type) const {
return to_ext(m_env).get_coercions(from_type);
list<expr_pair> get_coercions(ro_environment const & env, expr const & from_type) {
return to_ext(env).get_coercions(from_type);
}
bool frontend::is_coercion(expr const & f) const {
return to_ext(m_env).is_coercion(f);
bool is_coercion(ro_environment const & env, expr const & f) {
return to_ext(env).is_coercion(f);
}
}

333
src/frontends/lean/frontend.h
View file

@ -14,197 +14,148 @@ Author: Leonardo de Moura
namespace lean {
/**
\brief Wrapper for environment/state that provides additional objects
that are specific to the Lean frontend.
This wrapper provides APIs for accessing/using the Lean frontend
extension data in the environment.
\brief Import all definitions and notation.
*/
class frontend {
environment m_env;
io_state m_state;
public:
frontend();
frontend(environment const & env, io_state const & s);
void init_frontend(environment const & env, io_state & ios);
frontend mk_child() const { return frontend(m_env->mk_child(), m_state); }
bool has_children() const { return m_env->has_children(); }
bool has_parent() const { return m_env->has_parent(); }
environment const & get_environment() const { return m_env; }
operator environment const &() const { return get_environment(); }
operator ro_environment() const { return ro_environment(m_env); }
/**
@name Environment API
*/
/*@{*/
level add_uvar(name const & n, level const & l) { return m_env->add_uvar(n, l); }
level add_uvar(name const & n) { return m_env->add_uvar(n); }
level get_uvar(name const & n) const { return m_env->get_uvar(n); }
void add_definition(name const & n, expr const & t, expr const & v, bool opaque = false) { m_env->add_definition(n, t, v, opaque); }
void add_theorem(name const & n, expr const & t, expr const & v) { m_env->add_theorem(n, t, v); }
void add_definition(name const & n, expr const & v, bool opaque = false) { m_env->add_definition(n, v, opaque); }
void add_axiom(name const & n, expr const & t) { m_env->add_axiom(n, t); }
void add_var(name const & n, expr const & t) { m_env->add_var(n, t); }
object get_object(name const & n) const { return m_env->get_object(n); }
optional<object> find_object(name const & n) const { return m_env->find_object(n); }
bool has_object(name const & n) const { return m_env->has_object(n); }
typedef environment_cell::object_iterator object_iterator;
object_iterator begin_objects() const { return m_env->begin_objects(); }
object_iterator end_objects() const { return m_env->end_objects(); }
object_iterator begin_local_objects() const { return m_env->begin_local_objects(); }
object_iterator end_local_objects() const { return m_env->end_local_objects(); }
/*@}*/
/**
@name Notation for parsing and pretty printing.
*/
/*@{*/
void add_infix(name const & opn, unsigned precedence, expr const & d);
void add_infixl(name const & opn, unsigned precedence, expr const & d);
void add_infixr(name const & opn, unsigned precedence, expr const & d);
void add_prefix(name const & opn, unsigned precedence, expr const & d);
void add_postfix(name const & opn, unsigned precedence, expr const & d);
void add_mixfixl(unsigned sz, name const * opns, unsigned precedence, expr const & d);
void add_mixfixr(unsigned sz, name const * opns, unsigned precedence, expr const & d);
void add_mixfixc(unsigned sz, name const * opns, unsigned precedence, expr const & d);
void add_mixfixo(unsigned sz, name const * opns, unsigned precedence, expr const & d);
void add_mixfixl(std::initializer_list<name> const & l, unsigned p, expr const & d) { add_mixfixl(l.size(), l.begin(), p, d); }
void add_mixfixr(std::initializer_list<name> const & l, unsigned p, expr const & d) { add_mixfixr(l.size(), l.begin(), p, d); }
void add_mixfixc(std::initializer_list<name> const & l, unsigned p, expr const & d) { add_mixfixc(l.size(), l.begin(), p, d); }
void add_mixfixo(std::initializer_list<name> const & l, unsigned p, expr const & d) { add_mixfixo(l.size(), l.begin(), p, d); }
/**
\brief Return the operator (if one exists) associated with the
given expression.
\remark If an operator is not associated with \c e, then
return the null operator.
\remark This is used for pretty printing.
\remark If unicode is false, then only operators containing
safe ASCII chars are considered.
*/
operator_info find_op_for(expr const & e, bool unicode) const;
/**
\brief Return the operator (if one exists) that can appear at
the beginning of a language construct.
\remark If there isn't a nud operator starting with \c n, then
return the null operator.
\remark This is used for parsing.
*/
operator_info find_nud(name const & n) const;
/**
\brief Return the operator (if one exists) that can appear
inside of a language construct.
\remark If there isn't a led operator starting with \c n, then
return the null operator.
\remark This is used for parsing.
*/
operator_info find_led(name const & n) const;
/** \brief Return the precedence (aka binding power) of the given name. */
optional<unsigned> get_lbp(name const & n) const;
/*@}*/
/**
@name Implicit arguments.
*/
/**
\brief Mark the given arguments of \c n as implicit.
The bit-vector array specify the position of the implicit arguments.
*/
void mark_implicit_arguments(name const & n, unsigned sz, bool const * mask);
void mark_implicit_arguments(name const & n, std::initializer_list<bool> const & l);
void mark_implicit_arguments(expr const & n, std::initializer_list<bool> const & l);
/**
\brief Syntax sugar for mark_implicit_arguments(n, {true, ..., true}), with prefix_sz true's.
*/
void mark_implicit_arguments(name const & n, unsigned prefix_sz);
void mark_implicit_arguments(expr const & n, unsigned prefix_sz);
/** \brief Return true iff \c n has implicit arguments */
bool has_implicit_arguments(name const & n) const;
/** \brief Return the position of the arguments that are implicit. */
std::vector<bool> const & get_implicit_arguments(name const & n) const;
/**
\brief Return the position of the arguments that are implicit.
\remark If \c n is not a constant, then return the empty vector.
*/
std::vector<bool> const & get_implicit_arguments(expr const & n) const;
/**
\brief This frontend associates an definition with each
definition (or postulate) that has implicit arguments. The
additional definition has explicit arguments, and it is called
n::explicit. The explicit version can be used when the Lean
frontend can't figure out the value for the implicit
arguments.
*/
name const & get_explicit_version(name const & n) const;
/**
\brief Return true iff \c n is the name of the "explicit"
version of an object with implicit arguments
*/
bool is_explicit(name const & n) const;
/*@}*/
/**
@name Coercions
We support a very basic form of coercion. It is an expression
with type T1 -> T2. This expression can be used to convert
an expression of type T1 into an expression of type T2 whenever
T2 is expected, but T1 was provided.
*/
/**
\brief Add a new coercion to the frontend.
It throws an exception if f does not have type T1 -> T2, or if there is already a
coercion from T1 to T2.
*/
void add_coercion(expr const & f);
/**
\brief Return a coercion from given_type to expected_type if it exists.
*/
optional<expr> get_coercion(expr const & from_type, expr const & to_type) const;
/**
\brief Return the list of coercions for the given type.
The result is a list of pairs (to_type, function).
*/
list<expr_pair> get_coercions(expr const & from_type) const;
/**
\brief Return true iff the given expression is a coercion. That is, it was added using
\c add_coercion.
*/
bool is_coercion(expr const & f) const;
/*@}*/
/**
@name State management.
*/
/*@{*/
io_state const & get_state() const { return m_state; }
operator io_state const &() const { return m_state; }
io_state & get_state() { return m_state; }
operator io_state &() { return m_state; }
options get_options() const { return m_state.get_options(); }
void set_options(options const & opts) { return m_state.set_options(opts); }
template<typename T> void set_option(name const & n, T const & v) { m_state.set_option(n, v); }
void set_regular_channel(std::shared_ptr<output_channel> const & out) { m_state.set_regular_channel(out); }
void set_diagnostic_channel(std::shared_ptr<output_channel> const & out) { m_state.set_diagnostic_channel(out); }
/*@}*/
};
bool is_explicit(ro_environment const & env, name const & n);
bool has_implicit_arguments(ro_environment const & env, name const & n);
name const & get_explicit_version(ro_environment const & env, name const & n);
std::vector<bool> const & get_implicit_arguments(ro_environment const & env, name const & n);
bool is_coercion(ro_environment const & env, expr const & f);
operator_info find_op_for(ro_environment const & env, expr const & e, bool unicode);
/**
@name Notation for parsing and pretty printing.
*/
/*@{*/
void add_infix(environment const & env, io_state const & ios, name const & opn, unsigned p, expr const & d);
void add_infixl(environment const & env, io_state const & ios, name const & opn, unsigned p, expr const & d);
void add_infixr(environment const & env, io_state const & ios, name const & opn, unsigned p, expr const & d);
void add_prefix(environment const & env, io_state const & ios, name const & opn, unsigned p, expr const & d);
void add_postfix(environment const & env, io_state const & ios, name const & opn, unsigned p, expr const & d);
void add_mixfixl(environment const & env, io_state const & ios, unsigned sz, name const * opns, unsigned precedence, expr const & d);
void add_mixfixr(environment const & env, io_state const & ios, unsigned sz, name const * opns, unsigned precedence, expr const & d);
void add_mixfixc(environment const & env, io_state const & ios, unsigned sz, name const * opns, unsigned precedence, expr const & d);
void add_mixfixo(environment const & env, io_state const & ios, unsigned sz, name const * opns, unsigned precedence, expr const & d);
inline void add_mixfixl(environment const & env, io_state const & ios, std::initializer_list<name> const & l, unsigned p, expr const & d) {
add_mixfixl(env, ios, l.size(), l.begin(), p, d);
}
inline void add_mixfixr(environment const & env, io_state const & ios, std::initializer_list<name> const & l, unsigned p, expr const & d) {
add_mixfixr(env, ios, l.size(), l.begin(), p, d);
}
inline void add_mixfixc(environment const & env, io_state const & ios, std::initializer_list<name> const & l, unsigned p, expr const & d) {
add_mixfixc(env, ios, l.size(), l.begin(), p, d);
}
inline void add_mixfixo(environment const & env, io_state const & ios, std::initializer_list<name> const & l, unsigned p, expr const & d) {
add_mixfixo(env, ios, l.size(), l.begin(), p, d);
}
/**
\brief Return the operator (if one exists) that can appear at
the beginning of a language construct.
\remark If there isn't a nud operator starting with \c n, then
return the null operator.
\remark This is used for parsing.
*/
operator_info find_nud(ro_environment const & env, name const & n);
/**
\brief Return the operator (if one exists) that can appear
inside of a language construct.
\remark If there isn't a led operator starting with \c n, then
return the null operator.
\remark This is used for parsing.
*/
operator_info find_led(ro_environment const & env, name const & n);
/**
\brief Return the precedence (aka binding power) of the given name.
*/
optional<unsigned> get_lbp(ro_environment const & env, name const & n);
/**
\brief Return the operator (if one exists) associated with the
given expression.
\remark If an operator is not associated with \c e, then
return the null operator.
\remark This is used for pretty printing.
\remark If unicode is false, then only operators containing
safe ASCII chars are considered.
*/
operator_info find_op_for(ro_environment const & env, expr const & e, bool unicode);
/*@}*/
/**
@name Implicit arguments.
*/
/*@{*/
/**
\brief Mark the given arguments of \c n as implicit.
The bit-vector array specify the position of the implicit arguments.
*/
void mark_implicit_arguments(environment const & env, name const & n, unsigned sz, bool const * implicit);
void mark_implicit_arguments(environment const & env, name const & n, std::initializer_list<bool> const & l);
void mark_implicit_arguments(environment const & env, expr const & n, std::initializer_list<bool> const & l);
/**
\brief Syntax sugar for mark_implicit_arguments(n, {true, ..., true}), with prefix_sz true's.
*/
void mark_implicit_arguments(environment const & env, name const & n, unsigned prefix_sz);
void mark_implicit_arguments(environment const & env, expr const & n, unsigned prefix_sz);
/**
\brief Return true iff \c n has implicit arguments
*/
bool has_implicit_arguments(ro_environment const & env, name const & n);
/**
\brief Return the position of the arguments that are implicit.
*/
std::vector<bool> const & get_implicit_arguments(ro_environment const & env, name const & n);
/**
\brief Return the position of the arguments that are implicit.
\remark If \c n is not a constant, then return the empty vector.
*/
std::vector<bool> const & get_implicit_arguments(ro_environment const & env, expr const & n);
/**
\brief This frontend associates an definition with each
definition (or postulate) that has implicit arguments. The
additional definition has explicit arguments, and it is called
n::explicit. The explicit version can be used when the Lean
frontend can't figure out the value for the implicit
arguments.
*/
name const & get_explicit_version(ro_environment const & env, name const & n);
/**
\brief Return true iff \c n is the name of the "explicit"
version of an object with implicit arguments
*/
bool is_explicit(ro_environment const & env, name const & n);
/*@}*/
/**
@name Coercions
We support a very basic form of coercion. It is an expression
with type T1 -> T2. This expression can be used to convert
an expression of type T1 into an expression of type T2 whenever
T2 is expected, but T1 was provided.
*/
/*@{*/
/**
\brief Add a new coercion to the frontend.
It throws an exception if f does not have type T1 -> T2, or if there is already a
coercion from T1 to T2.
*/
void add_coercion(environment const & env, expr const & f);
/**
\brief Return true iff the given expression is a coercion. That is, it was added using
\c add_coercion.
*/
bool is_coercion(ro_environment const & env, expr const & f);
/**
\brief Return a coercion from given_type to expected_type if it exists.
*/
optional<expr> get_coercion(ro_environment const & env, expr const & from_type, expr const & to_type);
/**
\brief Return the list of coercions for the given type.
The result is a list of pairs (to_type, function).
*/
list<expr_pair> get_coercions(ro_environment const & env, expr const & from_type);
/*@}*/
}

18
src/frontends/lean/frontend_elaborator.cpp
View file

@ -125,7 +125,6 @@ inline justification mk_overload_justification(context const & ctx, expr const &
\brief Actual implementation of the frontend_elaborator.
*/
class frontend_elaborator::imp {
frontend const & m_frontend;
environment const & m_env;
type_checker m_type_checker;
type_inferer m_type_inferer;
@ -150,6 +149,8 @@ class frontend_elaborator::imp {
return ::lean::instantiate(e, v, m_ref.m_menv);
}
environment const & env() const { return m_ref.m_env; }
virtual expr visit_constant(expr const & e, context const & ctx) {
if (is_placeholder(e)) {
expr m = m_ref.m_menv->mk_metavar(ctx, visit(const_type(e), ctx));
@ -243,7 +244,7 @@ class frontend_elaborator::imp {
if (!has_metavar(expected) && !has_metavar(*given)) {
if (m_ref.m_type_checker.is_convertible(*given, expected, ctx)) {
// compatible
} else if (m_ref.m_frontend.get_coercion(*given, expected)) {
} else if (get_coercion(env(), *given, expected)) {
// compatible if using coercion
num_coercions++;
} else {
@ -334,7 +335,7 @@ class frontend_elaborator::imp {
args[0] = mk_overload_mvar(f_choices, ctx, e);
for (unsigned i = 1; i < args.size(); i++) {
if (arg_types[i]) {
list<expr_pair> coercions = m_ref.m_frontend.get_coercions(*(arg_types[i]));
list<expr_pair> coercions = get_coercions(env(), *(arg_types[i]));
if (coercions)
args[i] = add_coercion_mvar_app(coercions, args[i], *(arg_types[i]), ctx, arg(e, i));
}
@ -358,7 +359,7 @@ class frontend_elaborator::imp {
expr new_a = args[i];
optional<expr> new_a_t = arg_types[i];
if (new_a_t) {
list<expr_pair> coercions = m_ref.m_frontend.get_coercions(*new_a_t);
list<expr_pair> coercions = get_coercions(env(), *new_a_t);
if (coercions) {
if (!f_t) {
new_a = add_coercion_mvar_app(coercions, new_a, *new_a_t, ctx, a);
@ -390,7 +391,7 @@ class frontend_elaborator::imp {
if (new_t) {
optional<expr> new_v_t = get_type(new_v, ctx);
if (new_v_t && *new_t != *new_v_t) {
list<expr_pair> coercions = m_ref.m_frontend.get_coercions(*new_v_t);
list<expr_pair> coercions = get_coercions(env(), *new_v_t);
if (coercions) {
new_v = add_coercion_mvar_app(coercions, new_v, *new_v_t, ctx, v);
}
@ -427,9 +428,8 @@ class frontend_elaborator::imp {
}
public:
imp(frontend const & fe):
m_frontend(fe),
m_env(fe.get_environment()),
imp(environment const & env):
m_env(env),
m_type_checker(m_env),
m_type_inferer(m_env),
m_normalizer(m_env) {
@ -503,7 +503,7 @@ public:
}
};
frontend_elaborator::frontend_elaborator(frontend const & fe):m_ptr(new imp(fe)) {}
frontend_elaborator::frontend_elaborator(environment const & env):m_ptr(new imp(env)) {}
frontend_elaborator::~frontend_elaborator() {}
expr frontend_elaborator::operator()(expr const & e) { return m_ptr->elaborate(e); }
std::tuple<expr, expr, metavar_env> frontend_elaborator::operator()(name const & n, expr const & t, expr const & e) {

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

@ -23,7 +23,7 @@ class frontend_elaborator {
std::shared_ptr<imp> m_ptr;
static void print(imp * ptr);
public:
explicit frontend_elaborator(frontend const & fe);
explicit frontend_elaborator(environment const & env);
~frontend_elaborator();
/**

194
src/frontends/lean/notation.cpp
View file

@ -11,117 +11,117 @@ Author: Leonardo de Moura
#include "frontends/lean/frontend.h"
namespace lean {
void add_alias(frontend & f, name const & n, name const & m) {
object const & obj = f.get_object(n);
f.add_definition(m, obj.get_type(), mk_constant(n));
void add_alias(environment const & env, name const & n, name const & m) {
object const & obj = env->get_object(n);
env->add_definition(m, obj.get_type(), mk_constant(n));
}
/**
\brief Initialize builtin notation.
*/
void init_builtin_notation(frontend & f) {
if (!f.get_environment()->mark_builtin_imported("lean_notation"))
void init_builtin_notation(environment const & env, io_state & ios) {
if (!env->mark_builtin_imported("lean_notation"))
return;
f.add_infix("=", 50, mk_homo_eq_fn());
f.mark_implicit_arguments(mk_homo_eq_fn(), 1);
f.mark_implicit_arguments(mk_if_fn(), 1);
add_infix(env, ios, "=", 50, mk_homo_eq_fn());
mark_implicit_arguments(env, mk_homo_eq_fn(), 1);
mark_implicit_arguments(env, mk_if_fn(), 1);
f.add_prefix("\u00ac", 40, mk_not_fn()); // "¬"
f.add_infixr("&&", 35, mk_and_fn()); // "&&"
f.add_infixr("/\\", 35, mk_and_fn()); // "/\"
f.add_infixr("\u2227", 35, mk_and_fn()); // "∧"
f.add_infixr("||", 30, mk_or_fn()); // "||"
f.add_infixr("\\/", 30, mk_or_fn()); // "\/"
f.add_infixr("\u2228", 30, mk_or_fn()); // "∨"
f.add_infixr("=>", 25, mk_implies_fn()); // "=>"
f.add_infixr("\u21D2", 25, mk_implies_fn()); // "⇒"
f.add_infixr("<=>", 25, mk_iff_fn()); // "<=>"
f.add_infixr("\u21D4", 25, mk_iff_fn()); // "⇔"
add_prefix(env, ios, "\u00ac", 40, mk_not_fn()); // "¬"
add_infixr(env, ios, "&&", 35, mk_and_fn()); // "&&"
add_infixr(env, ios, "/\\", 35, mk_and_fn()); // "/\"
add_infixr(env, ios, "\u2227", 35, mk_and_fn()); // "∧"
add_infixr(env, ios, "||", 30, mk_or_fn()); // "||"
add_infixr(env, ios, "\\/", 30, mk_or_fn()); // "\/"
add_infixr(env, ios, "\u2228", 30, mk_or_fn()); // "∨"
add_infixr(env, ios, "=>", 25, mk_implies_fn()); // "=>"
add_infixr(env, ios, "\u21D2", 25, mk_implies_fn()); // "⇒"
add_infixr(env, ios, "<=>", 25, mk_iff_fn()); // "<=>"
add_infixr(env, ios, "\u21D4", 25, mk_iff_fn()); // "⇔"
f.add_infixl("+", 65, mk_nat_add_fn());
f.add_infixl("-", 65, mk_nat_sub_fn());
f.add_prefix("-", 75, mk_nat_neg_fn());
f.add_infixl("*", 70, mk_nat_mul_fn());
f.add_infix("<=", 50, mk_nat_le_fn());
f.add_infix("\u2264", 50, mk_nat_le_fn()); // ≤
f.add_infix(">=", 50, mk_nat_ge_fn());
f.add_infix("\u2265", 50, mk_nat_ge_fn()); // ≥
f.add_infix("<", 50, mk_nat_lt_fn());
f.add_infix(">", 50, mk_nat_gt_fn());
f.add_mixfixc({"|", "|"}, 55, mk_nat_id_fn()); // absolute value for naturals is the identity function
add_infixl(env, ios, "+", 65, mk_nat_add_fn());
add_infixl(env, ios, "-", 65, mk_nat_sub_fn());
add_prefix(env, ios, "-", 75, mk_nat_neg_fn());
add_infixl(env, ios, "*", 70, mk_nat_mul_fn());
add_infix(env, ios, "<=", 50, mk_nat_le_fn());
add_infix(env, ios, "\u2264", 50, mk_nat_le_fn()); // ≤
add_infix(env, ios, ">=", 50, mk_nat_ge_fn());
add_infix(env, ios, "\u2265", 50, mk_nat_ge_fn()); // ≥
add_infix(env, ios, "<", 50, mk_nat_lt_fn());
add_infix(env, ios, ">", 50, mk_nat_gt_fn());
add_mixfixc(env, ios, {"|", "|"}, 55, mk_nat_id_fn()); // absolute value for naturals is the identity function
f.add_infixl("+", 65, mk_int_add_fn());
f.add_infixl("-", 65, mk_int_sub_fn());
f.add_prefix("-", 75, mk_int_neg_fn());
f.add_infixl("*", 70, mk_int_mul_fn());
f.add_infixl("div", 70, mk_int_div_fn());
f.add_infixl("mod", 70, mk_int_mod_fn());
f.add_infix("|", 50, mk_int_divides_fn());
f.add_mixfixc({"|", "|"}, 55, mk_int_abs_fn());
f.add_infix("<=", 50, mk_int_le_fn());
f.add_infix("\u2264", 50, mk_int_le_fn()); // ≤
f.add_infix(">=", 50, mk_int_ge_fn());
f.add_infix("\u2265", 50, mk_int_ge_fn()); // ≥
f.add_infix("<", 50, mk_int_lt_fn());
f.add_infix(">", 50, mk_int_gt_fn());
add_infixl(env, ios, "+", 65, mk_int_add_fn());
add_infixl(env, ios, "-", 65, mk_int_sub_fn());
add_prefix(env, ios, "-", 75, mk_int_neg_fn());
add_infixl(env, ios, "*", 70, mk_int_mul_fn());
add_infixl(env, ios, "div", 70, mk_int_div_fn());
add_infixl(env, ios, "mod", 70, mk_int_mod_fn());
add_infix(env, ios, "|", 50, mk_int_divides_fn());
add_mixfixc(env, ios, {"|", "|"}, 55, mk_int_abs_fn());
add_infix(env, ios, "<=", 50, mk_int_le_fn());
add_infix(env, ios, "\u2264", 50, mk_int_le_fn()); // ≤
add_infix(env, ios, ">=", 50, mk_int_ge_fn());
add_infix(env, ios, "\u2265", 50, mk_int_ge_fn()); // ≥
add_infix(env, ios, "<", 50, mk_int_lt_fn());
add_infix(env, ios, ">", 50, mk_int_gt_fn());
f.add_infixl("+", 65, mk_real_add_fn());
f.add_infixl("-", 65, mk_real_sub_fn());
f.add_prefix("-", 75, mk_real_neg_fn());
f.add_infixl("*", 70, mk_real_mul_fn());
f.add_infixl("/", 70, mk_real_div_fn());
f.add_mixfixc({"|", "|"}, 55, mk_real_abs_fn());
f.add_infix("<=", 50, mk_real_le_fn());
f.add_infix("\u2264", 50, mk_real_le_fn()); // ≤
f.add_infix(">=", 50, mk_real_ge_fn());
f.add_infix("\u2265", 50, mk_real_ge_fn()); // ≥
f.add_infix("<", 50, mk_real_lt_fn());
f.add_infix(">", 50, mk_real_gt_fn());
add_infixl(env, ios, "+", 65, mk_real_add_fn());
add_infixl(env, ios, "-", 65, mk_real_sub_fn());
add_prefix(env, ios, "-", 75, mk_real_neg_fn());
add_infixl(env, ios, "*", 70, mk_real_mul_fn());
add_infixl(env, ios, "/", 70, mk_real_div_fn());
add_mixfixc(env, ios, {"|", "|"}, 55, mk_real_abs_fn());
add_infix(env, ios, "<=", 50, mk_real_le_fn());
add_infix(env, ios, "\u2264", 50, mk_real_le_fn()); // ≤
add_infix(env, ios, ">=", 50, mk_real_ge_fn());
add_infix(env, ios, "\u2265", 50, mk_real_ge_fn()); // ≥
add_infix(env, ios, "<", 50, mk_real_lt_fn());
add_infix(env, ios, ">", 50, mk_real_gt_fn());
f.add_coercion(mk_nat_to_int_fn());
f.add_coercion(mk_int_to_real_fn());
f.add_coercion(mk_nat_to_real_fn());
add_coercion(env, mk_nat_to_int_fn());
add_coercion(env, mk_int_to_real_fn());
add_coercion(env, mk_nat_to_real_fn());
// implicit arguments for builtin axioms
f.mark_implicit_arguments(mk_cast_fn(), 2);
f.mark_implicit_arguments(mk_mp_fn(), 2);
f.mark_implicit_arguments(mk_discharge_fn(), 2);
f.mark_implicit_arguments(mk_refl_fn(), 1);
f.mark_implicit_arguments(mk_subst_fn(), 4);
add_alias(f, "Subst", "SubstP");
f.mark_implicit_arguments("SubstP", 3);
f.mark_implicit_arguments(mk_trans_ext_fn(), 6);
f.mark_implicit_arguments(mk_eta_fn(), 2);
f.mark_implicit_arguments(mk_abst_fn(), 4);
f.mark_implicit_arguments(mk_imp_antisym_fn(), 2);
f.mark_implicit_arguments(mk_dom_inj_fn(), 4);
f.mark_implicit_arguments(mk_ran_inj_fn(), 4);
mark_implicit_arguments(env, mk_cast_fn(), 2);
mark_implicit_arguments(env, mk_mp_fn(), 2);
mark_implicit_arguments(env, mk_discharge_fn(), 2);
mark_implicit_arguments(env, mk_refl_fn(), 1);
mark_implicit_arguments(env, mk_subst_fn(), 4);
add_alias(env, "Subst", "SubstP");
mark_implicit_arguments(env, "SubstP", 3);
mark_implicit_arguments(env, mk_trans_ext_fn(), 6);
mark_implicit_arguments(env, mk_eta_fn(), 2);
mark_implicit_arguments(env, mk_abst_fn(), 4);
mark_implicit_arguments(env, mk_imp_antisym_fn(), 2);
mark_implicit_arguments(env, mk_dom_inj_fn(), 4);
mark_implicit_arguments(env, mk_ran_inj_fn(), 4);
// implicit arguments for basic theorems
f.mark_implicit_arguments(mk_absurd_fn(), 1);
f.mark_implicit_arguments(mk_double_neg_elim_fn(), 1);
f.mark_implicit_arguments(mk_mt_fn(), 2);
f.mark_implicit_arguments(mk_contrapos_fn(), 2);
f.mark_implicit_arguments(mk_eq_mp_fn(), 2);
f.mark_implicit_arguments(mk_not_imp1_fn(), 2);
f.mark_implicit_arguments(mk_not_imp2_fn(), 2);
f.mark_implicit_arguments(mk_conj_fn(), 2);
f.mark_implicit_arguments(mk_conjunct1_fn(), 2);
f.mark_implicit_arguments(mk_conjunct2_fn(), 2);
f.mark_implicit_arguments(mk_disj1_fn(), 1);
f.mark_implicit_arguments(mk_disj2_fn(), 1);
f.mark_implicit_arguments(mk_disj_cases_fn(), 3);
f.mark_implicit_arguments(mk_refute_fn(), 1);
f.mark_implicit_arguments(mk_symm_fn(), 3);
f.mark_implicit_arguments(mk_trans_fn(), 4);
f.mark_implicit_arguments(mk_eqt_elim_fn(), 1);
f.mark_implicit_arguments(mk_eqt_intro_fn(), 1);
f.mark_implicit_arguments(mk_congr1_fn(), 4);
f.mark_implicit_arguments(mk_congr2_fn(), 4);
f.mark_implicit_arguments(mk_congr_fn(), 6);
f.mark_implicit_arguments(mk_forall_elim_fn(), 2);
f.mark_implicit_arguments(mk_forall_intro_fn(), 2);
f.mark_implicit_arguments(mk_exists_elim_fn(), 3);
f.mark_implicit_arguments(mk_exists_intro_fn(), 2);
mark_implicit_arguments(env, mk_absurd_fn(), 1);
mark_implicit_arguments(env, mk_double_neg_elim_fn(), 1);
mark_implicit_arguments(env, mk_mt_fn(), 2);
mark_implicit_arguments(env, mk_contrapos_fn(), 2);
mark_implicit_arguments(env, mk_eq_mp_fn(), 2);
mark_implicit_arguments(env, mk_not_imp1_fn(), 2);
mark_implicit_arguments(env, mk_not_imp2_fn(), 2);
mark_implicit_arguments(env, mk_conj_fn(), 2);
mark_implicit_arguments(env, mk_conjunct1_fn(), 2);
mark_implicit_arguments(env, mk_conjunct2_fn(), 2);
mark_implicit_arguments(env, mk_disj1_fn(), 1);
mark_implicit_arguments(env, mk_disj2_fn(), 1);
mark_implicit_arguments(env, mk_disj_cases_fn(), 3);
mark_implicit_arguments(env, mk_refute_fn(), 1);
mark_implicit_arguments(env, mk_symm_fn(), 3);
mark_implicit_arguments(env, mk_trans_fn(), 4);
mark_implicit_arguments(env, mk_eqt_elim_fn(), 1);
mark_implicit_arguments(env, mk_eqt_intro_fn(), 1);
mark_implicit_arguments(env, mk_congr1_fn(), 4);
mark_implicit_arguments(env, mk_congr2_fn(), 4);
mark_implicit_arguments(env, mk_congr_fn(), 6);
mark_implicit_arguments(env, mk_forall_elim_fn(), 2);
mark_implicit_arguments(env, mk_forall_intro_fn(), 2);
mark_implicit_arguments(env, mk_exists_elim_fn(), 3);
mark_implicit_arguments(env, mk_exists_intro_fn(), 2);
}
}

5
src/frontends/lean/notation.h
View file

@ -8,6 +8,7 @@ Author: Leonardo de Moura
namespace lean {
constexpr unsigned g_eq_precedence = 50;
constexpr unsigned g_arrow_precedence = 25;
class frontend;
void init_builtin_notation(frontend & fe);
class environment;
class io_state;
void init_builtin_notation(environment const & env, io_state & st);
}

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

@ -135,13 +135,15 @@ static name g_unused = name::mk_internal_unique_name();
operators.
*/
class parser::imp {
friend class parser;
typedef scoped_map<name, unsigned, name_hash, name_eq> local_decls;
typedef name_map<expr> builtins;
typedef std::pair<unsigned, unsigned> pos_info;
typedef expr_map<pos_info> expr_pos_info;
typedef expr_map<tactic> tactic_hints; // a mapping from placeholder to tactic
typedef buffer<std::tuple<pos_info, name, expr, bool>> bindings_buffer;
frontend & m_frontend;
environment m_env;
io_state m_io_state;
scanner m_scanner;
frontend_elaborator m_elaborator;
type_inferer m_type_inferer;
@ -181,8 +183,8 @@ class parser::imp {
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_frontend.get_state());
set_environment set2(L, m_frontend.get_environment());
set_io_state set1(L, m_io_state);
set_environment set2(L, m_env);
return f(L);
});
}
@ -190,8 +192,8 @@ class parser::imp {
template<typename F>
void code_with_callbacks(F && f) {
m_script_state->apply([&](lua_State * L) {
set_io_state set1(L, m_frontend.get_state());
set_environment set2(L, m_frontend.get_environment());
set_io_state set1(L, m_io_state);
set_environment set2(L, m_env);
m_script_state->exec_unprotected([&]() {
f();
});
@ -319,10 +321,10 @@ class parser::imp {
/*@{*/
void display_error_pos(unsigned line, unsigned pos) {
regular(m_frontend) << "Error (line: " << line;
regular(m_io_state) << "Error (line: " << line;
if (pos != static_cast<unsigned>(-1))
regular(m_frontend) << ", pos: " << pos;
regular(m_frontend) << ")";
regular(m_io_state) << ", pos: " << pos;
regular(m_io_state) << ")";
}
void display_error_pos(pos_info const & p) { display_error_pos(p.first, p.second); }
@ -341,7 +343,7 @@ class parser::imp {
void display_error(char const * msg, unsigned line, unsigned pos) {
display_error_pos(line, pos);
regular(m_frontend) << " " << msg << endl;
regular(m_io_state) << " " << msg << endl;
}
void display_error(char const * msg) {
@ -354,7 +356,7 @@ class parser::imp {
display_error_pos(some_expr(m_elaborator.get_original(*main_expr)));
else
display_error_pos(main_expr);
regular(m_frontend) << " " << ex << endl;
regular(m_io_state) << " " << ex << endl;
}
struct lean_pos_info_provider : public pos_info_provider {
@ -370,25 +372,25 @@ class parser::imp {
};
void display_error(elaborator_exception const & ex) {
formatter fmt = m_frontend.get_state().get_formatter();
options opts = m_frontend.get_state().get_options();
formatter fmt = m_io_state.get_formatter();
options opts = m_io_state.get_options();
lean_pos_info_provider pos_provider(*this);
regular(m_frontend) << mk_pair(ex.get_justification().pp(fmt, opts, &pos_provider, true), opts) << endl;
regular(m_io_state) << mk_pair(ex.get_justification().pp(fmt, opts, &pos_provider, true), opts) << endl;
}
void 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_frontend) << " executing script," << ex.get_msg() << endl;
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_frontend) << " executing external script (" << ex.get_filename() << ":" << ex.get_line() << ")," << ex.get_msg() << endl;
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_frontend) << " executing script, but could not decode position information, " << ex.what() << endl;
regular(m_io_state) << " executing script, but could not decode position information, " << ex.what() << endl;
break;
}
}
@ -446,7 +448,7 @@ class parser::imp {
throw;
} catch (interrupted & ex) {
if (m_verbose)
regular(m_frontend) << "!!!Interrupted!!!" << endl;
regular(m_io_state) << "!!!Interrupted!!!" << endl;
reset_interrupt();
sync();
if (m_use_exceptions)
@ -508,7 +510,7 @@ class parser::imp {
return parse_level_max();
} else {
next();
return m_frontend.get_uvar(id);
return m_env->get_uvar(id);
}
}
@ -586,7 +588,7 @@ class parser::imp {
\brief Return the size of the implicit vector associated with the given denotation.
*/
unsigned get_implicit_vector_size(expr const & d) {
return m_frontend.get_implicit_arguments(d).size();
return get_implicit_arguments(m_env, d).size();
}
/**
@ -597,7 +599,7 @@ class parser::imp {
std::vector<bool> const * r = nullptr;
unsigned m = std::numeric_limits<unsigned>::max();
for (expr const & d : ds) {
std::vector<bool> const & v = m_frontend.get_implicit_arguments(d);
std::vector<bool> const & v = get_implicit_arguments(m_env, d);
unsigned s = v.size();
if (s == 0) {
return v;
@ -803,12 +805,12 @@ class parser::imp {
to check if \c id is a builtin symbol. If it is not throws an error.
*/
expr get_name_ref(name const & id, pos_info const & p) {
optional<object> obj = m_frontend.find_object(id);
optional<object> obj = m_env->find_object(id);
if (obj) {
object_kind k = obj->kind();
if (k == object_kind::Definition || k == object_kind::Postulate || k == object_kind::Builtin) {
if (m_frontend.has_implicit_arguments(obj->get_name())) {
std::vector<bool> const & imp_args = m_frontend.get_implicit_arguments(obj->get_name());
if (has_implicit_arguments(m_env, obj->get_name())) {
std::vector<bool> const & imp_args = get_implicit_arguments(m_env, obj->get_name());
buffer<expr> args;
pos_info p = pos();
expr f = (k == object_kind::Builtin) ? obj->get_value() : mk_constant(obj->get_name());
@ -850,7 +852,7 @@ class parser::imp {
if (it != m_local_decls.end()) {
return save(mk_var(m_num_local_decls - it->second - 1), p);
} else {
operator_info op = m_frontend.find_nud(id);
operator_info op = find_nud(m_env, id);
if (op) {
switch (op.get_fixity()) {
case fixity::Prefix: return parse_prefix(op);
@ -882,7 +884,7 @@ class parser::imp {
if (it != m_local_decls.end()) {
return save(mk_app(left, save(mk_var(m_num_local_decls - it->second - 1), p)), p2);
} else {
operator_info op = m_frontend.find_led(id);
operator_info op = find_led(m_env, id);
if (op) {
switch (op.get_fixity()) {
case fixity::Infix: return parse_infix(left, op);
@ -1205,7 +1207,7 @@ class parser::imp {
return ::lean::apply_tactic(pr, pr_type);
} else {
name n = check_identifier_next("invalid apply command, identifier, '(' expr ')', or 'script-block' expected");
optional<object> o = m_frontend.find_object(n);
optional<object> o = m_env->find_object(n);
if (o && (o->is_theorem() || o->is_axiom())) {
return ::lean::apply_tactic(n);
} else {
@ -1306,7 +1308,7 @@ class parser::imp {
if (it != m_local_decls.end()) {
return app_lbp;
} else {
optional<unsigned> prec = m_frontend.get_lbp(id);
optional<unsigned> prec = get_lbp(m_env, id);
if (prec)
return *prec;
else
@ -1352,11 +1354,11 @@ class parser::imp {
found = true;
}
if (found)
m_frontend.mark_implicit_arguments(n, imp_args.size(), imp_args.data());
mark_implicit_arguments(m_env, n, imp_args.size(), imp_args.data());
}
void display_proof_state(proof_state s) {
regular(m_frontend) << "Proof state:\n" << s << endl;
regular(m_io_state) << "Proof state:\n" << s << endl;
}
void display_proof_state_if_interactive(proof_state s) {
@ -1375,7 +1377,7 @@ class parser::imp {
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_frontend.get_environment(), m_frontend.get_state(), s);
proof_state_seq seq = t(m_env, m_io_state, s);
r = seq.pull();
});
if (r) {
@ -1403,9 +1405,9 @@ class parser::imp {
// Example: apply_tactic.
metavar_env menv = s.get_menv().copy();
buffer<unification_constraint> ucs;
expr pr_type = type_checker(m_frontend.get_environment()).infer_type(pr, ctx, menv, ucs);
expr pr_type = type_checker(m_env).infer_type(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_frontend.get_environment(), menv, ucs.size(), ucs.data(), m_frontend.get_options());
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))
@ -1604,7 +1606,7 @@ class parser::imp {
context mvar_ctx(to_list(new_entries.begin(), new_entries.end()));
if (!m_type_inferer.is_proposition(mvar_type, mvar_ctx))
throw exception("failed to synthesize metavar, its type is not a proposition");
proof_state s = to_proof_state(m_frontend.get_environment(), mvar_ctx, mvar_type);
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
@ -1669,13 +1671,13 @@ class parser::imp {
if (has_metavar(val))
throw exception("invalid definition, value still contains metavariables after elaboration");
if (is_definition) {
m_frontend.add_definition(id, type, val);
m_env->add_definition(id, type, val);
if (m_verbose)
regular(m_frontend) << " Defined: " << id << endl;
regular(m_io_state) << " Defined: " << id << endl;
} else {
m_frontend.add_theorem(id, type, val);
m_env->add_theorem(id, type, val);
if (m_verbose)
regular(m_frontend) << " Proved: " << id << endl;
regular(m_io_state) << " Proved: " << id << endl;
}
register_implicit_arguments(id, bindings);
}
@ -1719,11 +1721,11 @@ class parser::imp {
type = m_elaborator(mk_abstraction(false, bindings, type_body));
}
if (is_var)
m_frontend.add_var(id, type);
m_env->add_var(id, type);
else
m_frontend.add_axiom(id, type);
m_env->add_axiom(id, type);
if (m_verbose)
regular(m_frontend) << " Assumed: " << id << endl;
regular(m_io_state) << " Assumed: " << id << endl;
register_implicit_arguments(id, bindings);
}
@ -1747,15 +1749,15 @@ class parser::imp {
parse_simple_bindings(bindings, false, false);
for (auto b : bindings) {
name const & id = std::get<1>(b);
if (m_frontend.find_object(id))
throw already_declared_exception(m_frontend.get_environment(), id);
if (m_env->find_object(id))
throw already_declared_exception(m_env, id);
}
for (auto b : bindings) {
name const & id = std::get<1>(b);
expr const & type = std::get<2>(b);
m_frontend.add_var(id, type);
m_env->add_var(id, type);
if (m_verbose)
regular(m_frontend) << " Assumed: " << id << endl;
regular(m_io_state) << " Assumed: " << id << endl;
}
}
@ -1773,9 +1775,9 @@ class parser::imp {
void parse_eval() {
next();
expr v = m_elaborator(parse_expr());
normalizer norm(m_frontend.get_environment());
normalizer norm(m_env);
expr r = norm(v);
regular(m_frontend) << r << endl;
regular(m_io_state) << r << endl;
}
/** \brief Parse
@ -1791,27 +1793,27 @@ class parser::imp {
if (opt_id == g_env_kwd) {
if (curr_is_nat()) {
unsigned i = parse_unsigned("invalid argument, value does not fit in a machine integer");
auto end = m_frontend.end_objects();
auto beg = m_frontend.begin_objects();
auto end = m_env->end_objects();
auto beg = m_env->begin_objects();
auto it = end;
while (it != beg && i != 0) {
--i;
--it;
}
for (; it != end; ++it) {
regular(m_frontend) << *it << endl;
regular(m_io_state) << *it << endl;
}
} else {
regular(m_frontend) << m_frontend << endl;
regular(m_io_state) << m_env << endl;
}
} else if (opt_id == g_options_kwd) {
regular(m_frontend) << pp(m_frontend.get_state().get_options()) << endl;
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());
regular(m_frontend) << v << endl;
regular(m_io_state) << v << endl;
}
}
@ -1819,12 +1821,12 @@ class parser::imp {
void parse_check() {
next();
expr v = m_elaborator(parse_expr());
expr t = infer_type(v, m_frontend.get_environment());
formatter fmt = m_frontend.get_state().get_formatter();
options opts = m_frontend.get_state().get_options();
expr t = infer_type(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_frontend) << mk_pair(r, opts) << endl;
regular(m_io_state) << mk_pair(r, opts) << endl;
}
/** \brief Return the (optional) precedence of a user-defined operator. */
@ -1855,9 +1857,9 @@ class parser::imp {
name name_id = check_identifier_next("invalid operator definition, identifier expected");
expr d = mk_constant(name_id);
switch (fx) {
case fixity::Infix: m_frontend.add_infix(op_id, prec, d); break;
case fixity::Infixl: m_frontend.add_infixl(op_id, prec, d); break;
case fixity::Infixr: m_frontend.add_infixr(op_id, prec, d); break;
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
}
}
@ -1898,29 +1900,29 @@ class parser::imp {
if (parts.size() == 1) {
if (first_placeholder && prev_placeholder) {
// infix: _ ID _
m_frontend.add_infix(parts[0], prec, d);
add_infix(m_env, m_io_state, parts[0], prec, d);
} else if (first_placeholder) {
// postfix: _ ID
m_frontend.add_postfix(parts[0], prec, d);
add_postfix(m_env, m_io_state, parts[0], prec, d);
} else if (prev_placeholder) {
// prefix: ID _
m_frontend.add_prefix(parts[0], prec, d);
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 _
m_frontend.add_mixfixo(parts.size(), parts.data(), prec, d);
add_mixfixo(m_env, m_io_state, parts.size(), parts.data(), prec, d);
} else if (first_placeholder) {
// mixfixr: _ ID ... ID
m_frontend.add_mixfixr(parts.size(), parts.data(), prec, d);
add_mixfixr(m_env, m_io_state, parts.size(), parts.data(), prec, d);
} else if (prev_placeholder) {
// mixfixl: ID _ ... ID _
m_frontend.add_mixfixl(parts.size(), parts.data(), prec, d);
add_mixfixl(m_env, m_io_state, parts.size(), parts.data(), prec, d);
} else {
// mixfixc: ID _ ... _ ID
m_frontend.add_mixfixc(parts.size(), parts.data(), prec, d);
add_mixfixc(m_env, m_io_state, parts.size(), parts.data(), prec, d);
}
}
return;
@ -1941,7 +1943,7 @@ class parser::imp {
void parse_echo() {
next();
std::string msg = check_string_next("invalid echo command, string expected");
regular(m_frontend) << msg << endl;
regular(m_io_state) << msg << endl;
}
/** Parse 'Set' [id] [value] */
@ -1966,9 +1968,9 @@ class parser::imp {
if (k != BoolOption)
throw parser_error(sstream() << "invalid option value, given option is not Boolean", pos());
if (curr_name() == "true")
m_frontend.set_option(id, true);
m_io_state.set_option(id, true);
else if (curr_name() == "false")
m_frontend.set_option(id, false);
m_io_state.set_option(id, false);
else
throw parser_error("invalid Boolean option value, 'true' or 'false' expected", pos());
next();
@ -1976,25 +1978,25 @@ class parser::imp {
case scanner::token::StringVal:
if (k != StringOption)
throw parser_error("invalid option value, given option is not a string", pos());
m_frontend.set_option(id, curr_string());
m_io_state.set_option(id, curr_string());
next();
break;
case scanner::token::NatVal:
if (k != IntOption && k != UnsignedOption)
throw parser_error("invalid option value, given option is not an integer", pos());
m_frontend.set_option(id, parse_unsigned("invalid option value, value does not fit in a machine integer"));
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_frontend.set_option(id, parse_double());
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_frontend) << " Set: " << id << endl;
regular(m_io_state) << " Set: " << id << endl;
}
void parse_import() {
@ -2003,14 +2005,14 @@ class parser::imp {
std::ifstream in(fname);
if (!in.is_open())
throw parser_error(sstream() << "invalid import command, failed to open file '" << fname << "'", m_last_cmd_pos);
if (!m_frontend.get_environment()->mark_imported(fname.c_str())) {
diagnostic(m_frontend) << "Module '" << fname << "' has already been imported" << endl;
if (!m_env->mark_imported(fname.c_str())) {
diagnostic(m_io_state) << "Module '" << fname << "' has already been imported" << endl;
return;
}
try {
if (m_verbose)
regular(m_frontend) << "Importing file '" << fname << "'" << endl;
parser import_parser(m_frontend, in, m_script_state, true /* use exceptions */, false /* not interactive */);
regular(m_io_state) << "Importing file '" << fname << "'" << endl;
parser import_parser(m_env, m_io_state, in, m_script_state, true /* use exceptions */, false /* not interactive */);
import_parser();
} catch (interrupted &) {
throw;
@ -2025,17 +2027,17 @@ class parser::imp {
name opt_id = curr_name();
next();
if (opt_id == g_options_kwd) {
regular(m_frontend) << "Available options:" << endl;
regular(m_io_state) << "Available options:" << endl;
for (auto p : get_option_declarations()) {
auto opt = p.second;
regular(m_frontend) << " " << opt.get_name() << " (" << opt.kind() << ") "
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_frontend) << "Available commands:" << endl
regular(m_io_state) << "Available commands:" << 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
@ -2055,7 +2057,7 @@ class parser::imp {
<< " 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_frontend) << "Type Ctrl-D to exit" << endl;
regular(m_io_state) << "Type Ctrl-D to exit" << endl;
#endif
}
}
@ -2064,9 +2066,9 @@ class parser::imp {
void parse_coercion() {
next();
expr coercion = parse_expr();
m_frontend.add_coercion(coercion);
add_coercion(m_env, coercion);
if (m_verbose)
regular(m_frontend) << " Coercion " << coercion << endl;
regular(m_io_state) << " Coercion " << coercion << endl;
}
/** \brief Parse a Lean command. */
@ -2122,8 +2124,8 @@ class parser::imp {
/*@}*/
void updt_options() {
m_verbose = get_parser_verbose(m_frontend.get_state().get_options());
m_show_errors = get_parser_show_errors(m_frontend.get_state().get_options());
m_verbose = get_parser_verbose(m_io_state.get_options());
m_show_errors = get_parser_show_errors(m_io_state.get_options());
}
/**
@ -2147,11 +2149,12 @@ class parser::imp {
void parse_script_expr() { return parse_script(true); }
public:
imp(frontend & fe, std::istream & in, script_state * S, bool use_exceptions, bool interactive):
m_frontend(fe),
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(fe),
m_type_inferer(fe.get_environment()),
m_elaborator(env),
m_type_inferer(env),
m_use_exceptions(use_exceptions),
m_interactive(interactive) {
m_script_state = S;
@ -2162,21 +2165,21 @@ public:
scan();
}
static void show_prompt(bool interactive, frontend & fe) {
static void show_prompt(bool interactive, io_state const & ios) {
if (interactive) {
regular(fe) << "# ";
regular(fe).flush();
regular(ios) << "# ";
regular(ios).flush();
}
}
void show_prompt() {
show_prompt(m_interactive, m_frontend);
show_prompt(m_interactive, m_io_state);
}
void show_tactic_prompt() {
if (m_interactive) {
regular(m_frontend) << "## ";
regular(m_frontend).flush();
regular(m_io_state) << "## ";
regular(m_io_state).flush();
}
}
@ -2216,9 +2219,14 @@ public:
}
};
parser::parser(frontend & fe, std::istream & in, script_state * S, bool use_exceptions, bool interactive) {
parser::imp::show_prompt(interactive, fe);
m_ptr.reset(new imp(fe, in, S, use_exceptions, interactive));
parser::parser(environment const & env, io_state const & ios, std::istream & in, script_state * S, bool use_exceptions, bool interactive) {
parser::imp::show_prompt(interactive, ios);
m_ptr.reset(new imp(env, ios, in, S, use_exceptions, interactive));
}
parser::parser(environment const & env, std::istream & in, script_state * S, bool use_exceptions, bool interactive):
parser(env, io_state(), in, S, use_exceptions, interactive) {
m_ptr->m_io_state.set_formatter(mk_pp_formatter(m_ptr->m_env));
}
parser::~parser() {
@ -2232,7 +2240,15 @@ expr parser::parse_expr() {
return m_ptr->parse_expr_main();
}
shell::shell(frontend & fe, script_state * S):m_frontend(fe), m_script_state(S) {
io_state parser::get_io_state() const {
return m_ptr->m_io_state;
}
shell::shell(environment const & env, io_state const & ios, script_state * S):m_env(env), m_io_state(ios), m_script_state(S) {
}
shell::shell(environment const & env, script_state * S):m_env(env), m_io_state(), m_script_state(S) {
m_io_state.set_formatter(mk_pp_formatter(m_env));
}
shell::~shell() {
@ -2248,37 +2264,29 @@ bool shell::operator()() {
add_history(input);
std::istringstream strm(input);
{
parser p(m_frontend, strm, m_script_state, false, false);
parser p(m_env, m_io_state, strm, m_script_state, false, false);
if (!p())
errors = true;
}
free(input);
}
#else
parser p(m_frontend, std::cin, m_script_state, false, true);
parser p(m_env, m_io_state, std::cin, m_script_state, false, true);
return p();
#endif
}
bool parse_commands(frontend & fe, std::istream & in, script_state * S, bool use_exceptions, bool interactive) {
return parser(fe, in, S, use_exceptions, interactive)();
}
bool parse_commands(environment const & env, io_state & st, std::istream & in, script_state * S, bool use_exceptions, bool interactive) {
frontend f(env, st);
bool r = parse_commands(f, in, S, use_exceptions, interactive);
st = f.get_state();
bool parse_commands(environment const & env, io_state & ios, std::istream & in, script_state * S, bool use_exceptions, bool interactive) {
parser p(env, ios, in, S, use_exceptions, interactive);
bool r = p();
ios = p.get_io_state();
return r;
}
expr parse_expr(frontend & fe, std::istream & in, script_state * S, bool use_exceptions) {
return parser(fe, in, S, use_exceptions).parse_expr();
}
expr parse_expr(environment const & env, io_state & st, std::istream & in, script_state * S, bool use_exceptions) {
frontend f(env, st);
expr r = parse_expr(f, in, S, use_exceptions);
st = f.get_state();
expr parse_expr(environment const & env, io_state & ios, std::istream & in, script_state * S, bool use_exceptions) {
parser p(env, ios, in, S, use_exceptions);
expr r = p.parse_expr();
ios = p.get_io_state();
return r;
}
}

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

@ -6,18 +6,18 @@ Author: Leonardo de Moura
*/
#pragma once
#include <iostream>
#include "kernel/environment.h"
#include "library/io_state.h"
namespace lean {
class script_state;
class frontend;
class io_state;
class environment;
/** \brief Functional object for parsing commands and expressions */
class parser {
class imp;
std::unique_ptr<imp> m_ptr;
public:
parser(frontend & fe, std::istream & in, script_state * S, bool use_exceptions = true, bool interactive = false);
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);
~parser();
/** \brief Parse a sequence of commands */
@ -25,21 +25,24 @@ public:
/** \brief Parse a single expression */
expr parse_expr();
io_state get_io_state() const;
};
/** \brief Implements the Read Eval Print loop */
class shell {
frontend & m_frontend;
script_state * m_script_state;
environment m_env;
io_state m_io_state;
script_state * m_script_state;
public:
shell(frontend & fe, script_state * S);
shell(environment const & env, io_state const & st, script_state * S);
shell(environment const & env, script_state * S);
~shell();
bool operator()();
io_state get_io_state() const { return m_io_state; }
};
bool parse_commands(frontend & fe, std::istream & in, script_state * S = nullptr, bool use_exceptions = true, bool interactive = false);
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(frontend & fe, std::istream & in, script_state * S = nullptr, bool use_exceptions = true);
expr parse_expr(environment const & env, io_state & st, std::istream & in, script_state * S = nullptr, bool use_exceptions = true);
}

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

@ -1377,17 +1377,4 @@ public:
formatter mk_pp_formatter(ro_environment const & env) {
return mk_formatter(pp_formatter_cell(env));
}
std::ostream & operator<<(std::ostream & out, frontend const & fe) {
options const & opts = fe.get_state().get_options();
formatter fmt = mk_pp_formatter(fe.get_environment());
bool first = true;
std::for_each(fe.begin_objects(),
fe.end_objects(),
[&](object const & obj) {
if (first) first = false; else out << "\n";
out << mk_pair(fmt(obj, opts), opts);
});
return out;
}
}

6
src/frontends/lean/register_module.cpp
View file

@ -125,8 +125,10 @@ static int parse_lean_cmds(lua_State * L) {
}
static int mk_environment(lua_State * L) {
frontend f;
return push_environment(L, f.get_environment());
environment env;
io_state ios;
init_frontend(env, ios);
return push_environment(L, env);
}
static int mk_lean_formatter(lua_State * L) {

17
src/shell/lean.cpp
View file

@ -16,6 +16,7 @@ Author: Leonardo de Moura
#include "util/script_state.h"
#include "util/thread.h"
#include "kernel/printer.h"
#include "kernel/environment.h"
#include "library/io_state.h"
#include "library/kernel_bindings.h"
#include "frontends/lean/parser.h"
@ -26,12 +27,13 @@ Author: Leonardo de Moura
#include "githash.h" // NOLINT
using lean::shell;
using lean::frontend;
using lean::parser;
using lean::script_state;
using lean::unreachable_reached;
using lean::invoke_debugger;
using lean::notify_assertion_violation;
using lean::environment;
using lean::io_state;
enum class input_kind { Unspecified, Lean, Lua };
@ -133,9 +135,11 @@ int main(int argc, char ** argv) {
#else
std::cout << "Type Ctrl-D or 'Exit.' to exit or 'Help.' for help."<< std::endl;
#endif
frontend f;
environment env;
io_state ios;
init_frontend(env, ios);
script_state S;
shell sh(f, &S);
shell sh(env, &S);
return sh() ? 0 : 1;
} else {
lean_assert(default_k == input_kind::Lua);
@ -143,7 +147,9 @@ int main(int argc, char ** argv) {
S.dostring(g_lua_repl);
}
} else {
frontend f;
environment env;
io_state ios;
init_frontend(env, ios);
script_state S;
bool ok = true;
for (int i = optind; i < argc; i++) {
@ -162,8 +168,7 @@ int main(int argc, char ** argv) {
std::cerr << "Failed to open file '" << argv[i] << "'\n";
return 1;
}
parser p(f, in, &S, false, false);
if (!p())
if (!parse_commands(env, ios, in, &S, false, false))
ok = false;
} else if (k == input_kind::Lua) {
try {

123
src/tests/frontends/lean/frontend.cpp
View file

@ -17,11 +17,11 @@ Author: Leonardo de Moura
using namespace lean;
static void tst1() {
frontend f;
f.add_uvar("tst");
frontend c = f.mk_child();
lean_assert(c.get_uvar("tst") == f.get_uvar("tst"));
lean_assert(f.get_environment()->has_children());
environment env; io_state ios; init_frontend(env, ios);
env->add_uvar("tst");
environment c = env->mk_child();
lean_assert(c->get_uvar("tst") == env->get_uvar("tst"));
lean_assert(env->has_children());
}
static void tst2() {
@ -53,14 +53,14 @@ static void tst2() {
}
static void tst3() {
frontend f;
environment env;
std::cout << "====================\n";
std::cout << f << "\n";
std::cout << env << "\n";
}
static void tst4() {
frontend f;
formatter fmt = mk_pp_formatter(f);
environment env; io_state ios; init_frontend(env, ios);
formatter fmt = mk_pp_formatter(env);
context c;
c = extend(c, "x", Bool);
c = extend(c, "y", Bool);
@ -73,18 +73,18 @@ static void tst4() {
static void tst5() {
std::cout << "=================\n";
frontend f;
formatter fmt = mk_pp_formatter(f);
f.add_var("A", Type());
f.add_var("x", Const("A"));
optional<object> obj = f.find_object("x");
environment env; io_state ios; init_frontend(env, ios);
formatter fmt = mk_pp_formatter(env);
env->add_var("A", Type());
env->add_var("x", Const("A"));
optional<object> obj = env->find_object("x");
lean_assert(obj);
lean_assert(obj->get_name() == "x");
std::cout << fmt(*obj) << "\n";
optional<object> obj2 = f.find_object("y");
optional<object> obj2 = env->find_object("y");
lean_assert(!obj2);
try {
f.get_object("y");
env->get_object("y");
lean_unreachable();
} catch (unknown_name_exception & ex) {
std::cout << ex.what() << " " << ex.get_name() << "\n";
@ -101,61 +101,60 @@ public:
static void tst6() {
std::cout << "=================\n";
frontend f;
environment env;
environment env; io_state ios; init_frontend(env, ios);
env->add_neutral_object(new alien_cell());
formatter fmt = mk_pp_formatter(f);
formatter fmt = mk_pp_formatter(env);
std::cout << fmt(env) << "\n";
}
static void tst7() {
frontend f;
formatter fmt = mk_pp_formatter(f);
environment env; io_state ios; init_frontend(env, ios);
formatter fmt = mk_pp_formatter(env);
std::cout << fmt(And(Const("x"), Const("y"))) << "\n";
}
static void tst8() {
frontend fe;
formatter fmt = mk_pp_formatter(fe);
fe.add_infixl("<-$->", 10, mk_refl_fn());
std::cout << fmt(*(fe.find_object("Trivial"))) << "\n";
environment env; io_state ios; init_frontend(env, ios);
formatter fmt = mk_pp_formatter(env);
add_infixl(env, ios, "<-$->", 10, mk_refl_fn());
std::cout << fmt(*(env->find_object("Trivial"))) << "\n";
}
static void tst9() {
frontend f;
lean_assert(!f.has_children());
environment env; io_state ios; init_frontend(env, ios);
lean_assert(!env->has_children());
{
frontend c = f.mk_child();
lean_assert(f.has_children());
environment c = env->mk_child();
lean_assert(env->has_children());
}
lean_assert(!f.has_children());
f.add_uvar("l", level()+1);
lean_assert(f.get_uvar("l") == level("l"));
try { f.get_uvar("l2"); lean_unreachable(); }
lean_assert(!env->has_children());
env->add_uvar("l", level()+1);
lean_assert(env->get_uvar("l") == level("l"));
try { env->get_uvar("l2"); lean_unreachable(); }
catch (exception &) {}
f.add_definition("x", Bool, True);
object const & obj = f.get_object("x");
env->add_definition("x", Bool, True);
object const & obj = env->get_object("x");
lean_assert(obj.get_name() == "x");
lean_assert(is_bool(obj.get_type()));
lean_assert(obj.get_value() == True);
try { f.get_object("y"); lean_unreachable(); }
try { env->get_object("y"); lean_unreachable(); }
catch (exception &) {}
lean_assert(!f.find_object("y"));
f.add_definition("y", False);
lean_assert(is_bool(f.find_object("y")->get_type()));
lean_assert(f.has_object("y"));
lean_assert(!f.has_object("z"));
lean_assert(!env->find_object("y"));
env->add_definition("y", False);
lean_assert(is_bool(env->find_object("y")->get_type()));
lean_assert(env->has_object("y"));
lean_assert(!env->has_object("z"));
bool found = false;
std::for_each(f.begin_objects(), f.end_objects(), [&](object const & obj) { if (obj.has_name() && obj.get_name() == "y") found = true; });
std::for_each(env->begin_objects(), env->end_objects(), [&](object const & obj) { if (obj.has_name() && obj.get_name() == "y") found = true; });
lean_assert(found);
f.add_postfix("!", 10, Const("factorial"));
add_postfix(env, ios, "!", 10, Const("factorial"));
name parts[] = {"if", "then", "else"};
f.add_mixfixl(3, parts, 10, Const("if"));
add_mixfixl(env, ios, 3, parts, 10, Const("if"));
}
static void tst10() {
frontend f;
formatter fmt = mk_pp_formatter(f);
environment env; io_state ios; init_frontend(env, ios);
formatter fmt = mk_pp_formatter(env);
expr x = Const("xxxxxxxxxxxx");
expr y = Const("y");
expr z = Const("foo");
@ -165,39 +164,39 @@ static void tst10() {
}
static void tst11() {
frontend f;
environment env; io_state ios; init_frontend(env, ios);
expr A = Const("A");
f.add_var("g", Pi({A, Type()}, A >> (A >> A)));
lean_assert(!f.has_implicit_arguments("g"));
f.mark_implicit_arguments("g", {true, false, false});
lean_assert(f.has_implicit_arguments("g"))
name gexp = f.get_explicit_version("g");
lean_assert(f.find_object(gexp));
lean_assert(f.find_object("g")->get_type() == f.find_object(gexp)->get_type());
lean_assert(f.get_implicit_arguments("g") == std::vector<bool>({true})); // the trailing "false" marks are removed
env->add_var("g", Pi({A, Type()}, A >> (A >> A)));
lean_assert(!has_implicit_arguments(env, "g"));
mark_implicit_arguments(env, "g", {true, false, false});
lean_assert(has_implicit_arguments(env, "g"))
name gexp = get_explicit_version(env, "g");
lean_assert(env->find_object(gexp));
lean_assert(env->find_object("g")->get_type() == env->find_object(gexp)->get_type());
lean_assert(get_implicit_arguments(env, "g") == std::vector<bool>({true})); // the trailing "false" marks are removed
try {
f.mark_implicit_arguments("g", {true, false, false});
mark_implicit_arguments(env, "g", {true, false, false});
lean_unreachable();
} catch (exception & ex) {
std::cout << "Expected error: " << ex.what() << std::endl;
}
f.add_var("s", Pi({A, Type()}, A >> (A >> A)));
env->add_var("s", Pi({A, Type()}, A >> (A >> A)));
try {
f.mark_implicit_arguments("s", {true, true, true, true});
mark_implicit_arguments(env, "s", {true, true, true, true});
lean_unreachable();
} catch (exception & ex) {
std::cout << "Expected error: " << ex.what() << std::endl;
}
f.add_var(name{"h", "explicit"}, Pi({A, Type()}, A >> (A >> A)));
f.add_var("h", Pi({A, Type()}, A >> (A >> A)));
env->add_var(name{"h", "explicit"}, Pi({A, Type()}, A >> (A >> A)));
env->add_var("h", Pi({A, Type()}, A >> (A >> A)));
try {
f.mark_implicit_arguments("h", {true, false, false});
mark_implicit_arguments(env, "h", {true, false, false});
lean_unreachable();
} catch (exception & ex) {
std::cout << "Expected error: " << ex.what() << std::endl;
}
try {
f.mark_implicit_arguments("u", {true, false});
mark_implicit_arguments(env, "u", {true, false});
lean_unreachable();
} catch (exception & ex) {
std::cout << "Expected error: " << ex.what() << std::endl;

111
src/tests/frontends/lean/parser.cpp
View file

@ -17,13 +17,14 @@ Author: Leonardo de Moura
#include "frontends/lean/pp.h"
using namespace lean;
static void parse(frontend & fe, char const * str) {
frontend child = fe.mk_child();
static void parse(environment const & env, io_state const & ios, char const * str) {
environment child = env->mk_child();
io_state ios_copy = ios;
std::istringstream in(str);
if (parse_commands(child, in)) {
formatter fmt = mk_pp_formatter(child);
std::for_each(child.begin_local_objects(),
child.end_local_objects(),
if (parse_commands(child, ios_copy, in)) {
formatter fmt = mk_pp_formatter(env);
std::for_each(child->begin_local_objects(),
child->end_local_objects(),
[&](object const & obj) {
std::cout << fmt(obj) << "\n";
std::cout << obj << "\n";
@ -31,9 +32,9 @@ static void parse(frontend & fe, char const * str) {
}
}
static void parse_error(frontend & fe, char const * str) {
static void parse_error(environment const & env, io_state const & ios, char const * str) {
try {
parse(fe, str);
parse(env, ios, str);
lean_unreachable();
} catch (exception & ex) {
std::cout << "expected error: " << ex.what() << "\n";
@ -41,20 +42,20 @@ static void parse_error(frontend & fe, char const * str) {
}
static void tst1() {
frontend fe;
parse(fe, "Variable x : Bool Variable y : Bool Axiom H : x && y || x => x");
parse(fe, "Eval true && true");
parse(fe, "Show true && false Eval true && false");
parse(fe, "Infixl 35 & : and Show true & false & false Eval true & false");
parse(fe, "Notation 100 if _ then _ fi : implies Show if true then false fi");
parse(fe, "Show Pi (A : Type), A -> A");
parse(fe, "Check Pi (A : Type), A -> A");
environment env; io_state ios; init_frontend(env, ios);
parse(env, ios, "Variable x : Bool Variable y : Bool Axiom H : x && y || x => x");
parse(env, ios, "Eval true && true");
parse(env, ios, "Show true && false Eval true && false");
parse(env, ios, "Infixl 35 & : and Show true & false & false Eval true & false");
parse(env, ios, "Notation 100 if _ then _ fi : implies Show if true then false fi");
parse(env, ios, "Show Pi (A : Type), A -> A");
parse(env, ios, "Check Pi (A : Type), A -> A");
}
static void check(frontend & fe, char const * str, expr const & expected) {
static void check(environment const & env, io_state & ios, char const * str, expr const & expected) {
std::istringstream in(str);
try {
expr got = parse_expr(fe, in);
expr got = parse_expr(env, ios, in);
lean_assert(expected == got);
} catch (exception &) {
lean_unreachable();
@ -62,47 +63,47 @@ static void check(frontend & fe, char const * str, expr const & expected) {
}
static void tst2() {
frontend fe;
fe.add_var("x", Bool);
fe.add_var("y", Bool);
fe.add_var("z", Bool);
environment env; io_state ios; init_frontend(env, ios);
env->add_var("x", Bool);
env->add_var("y", Bool);
env->add_var("z", Bool);
expr x = Const("x"); expr y = Const("y"); expr z = Const("z");
check(fe, "x && y", And(x, y));
check(fe, "x && y || z", Or(And(x, y), z));
check(fe, "x || y && z", Or(x, And(y, z)));
check(fe, "x || y || x && z", Or(x, Or(y, And(x, z))));
check(fe, "x || y || x && z => x && y", Implies(Or(x, Or(y, And(x, z))), And(x, y)));
check(fe, "x ∨ y ∨ x ∧ z ⇒ x ∧ y", Implies(Or(x, Or(y, And(x, z))), And(x, y)));
check(fe, "x⇒y⇒z⇒x", Implies(x, Implies(y, Implies(z, x))));
check(fe, "x=>y=>z=>x", Implies(x, Implies(y, Implies(z, x))));
check(fe, "x=>(y=>z)=>x", Implies(x, Implies(Implies(y, z), x)));
check(env, ios, "x && y", And(x, y));
check(env, ios, "x && y || z", Or(And(x, y), z));
check(env, ios, "x || y && z", Or(x, And(y, z)));
check(env, ios, "x || y || x && z", Or(x, Or(y, And(x, z))));
check(env, ios, "x || y || x && z => x && y", Implies(Or(x, Or(y, And(x, z))), And(x, y)));
check(env, ios, "x ∨ y ∨ x ∧ z ⇒ x ∧ y", Implies(Or(x, Or(y, And(x, z))), And(x, y)));
check(env, ios, "x⇒y⇒z⇒x", Implies(x, Implies(y, Implies(z, x))));
check(env, ios, "x=>y=>z=>x", Implies(x, Implies(y, Implies(z, x))));
check(env, ios, "x=>(y=>z)=>x", Implies(x, Implies(Implies(y, z), x)));
}
static void tst3() {
frontend fe;
parse(fe, "Help");
parse(fe, "Help Options");
parse_error(fe, "Help Echo");
check(fe, "10.3", mk_real_value(mpq(103, 10)));
parse(fe, "Variable f : Real -> Real. Check f 10.3.");
parse(fe, "Variable g : Type 1 -> Type. Check g Type");
parse_error(fe, "Check fun .");
parse_error(fe, "Definition foo .");
parse_error(fe, "Check a");
parse_error(fe, "Check U");
parse(fe, "Variable h : Real -> Real -> Real. Notation 10 [ _ ; _ ] : h. Check [ 10.3 ; 20.1 ].");
parse_error(fe, "Variable h : Real -> Real -> Real. Notation 10 [ _ ; _ ] : h. Check [ 10.3 | 20.1 ].");
parse_error(fe, "Set pp::indent true");
parse(fe, "Set pp::indent 10");
parse_error(fe, "Set pp::colors foo");
parse_error(fe, "Set pp::colors \"foo\"");
parse(fe, "Set pp::colors true");
parse_error(fe, "Notation 10 : Int::add");
parse_error(fe, "Notation 10 _ : Int::add");
parse(fe, "Notation 10 _ ++ _ : Int::add. Eval 10 ++ 20.");
parse(fe, "Notation 10 _ -- : Int::neg. Eval 10 --");
parse(fe, "Notation 30 -- _ : Int::neg. Eval -- 10");
parse_error(fe, "10 + 30");
environment env; io_state ios; init_frontend(env, ios);
parse(env, ios, "Help");
parse(env, ios, "Help Options");
parse_error(env, ios, "Help Echo");
check(env, ios, "10.3", mk_real_value(mpq(103, 10)));
parse(env, ios, "Variable f : Real -> Real. Check f 10.3.");
parse(env, ios, "Variable g : Type 1 -> Type. Check g Type");
parse_error(env, ios, "Check fun .");
parse_error(env, ios, "Definition foo .");
parse_error(env, ios, "Check a");
parse_error(env, ios, "Check U");
parse(env, ios, "Variable h : Real -> Real -> Real. Notation 10 [ _ ; _ ] : h. Check [ 10.3 ; 20.1 ].");
parse_error(env, ios, "Variable h : Real -> Real -> Real. Notation 10 [ _ ; _ ] : h. Check [ 10.3 | 20.1 ].");
parse_error(env, ios, "Set pp::indent true");
parse(env, ios, "Set pp::indent 10");
parse_error(env, ios, "Set pp::colors foo");
parse_error(env, ios, "Set pp::colors \"foo\"");
parse(env, ios, "Set pp::colors true");
parse_error(env, ios, "Notation 10 : Int::add");
parse_error(env, ios, "Notation 10 _ : Int::add");
parse(env, ios, "Notation 10 _ ++ _ : Int::add. Eval 10 ++ 20.");
parse(env, ios, "Notation 10 _ -- : Int::neg. Eval 10 --");
parse(env, ios, "Notation 30 -- _ : Int::neg. Eval -- 10");
parse_error(env, ios, "10 + 30");
}
int main() {

54
src/tests/frontends/lean/pp.cpp
View file

@ -22,8 +22,8 @@ static expr mk_shared_expr(unsigned depth) {
}
static void tst1() {
frontend f;
formatter fmt = mk_pp_formatter(f);
environment env; io_state ios; init_frontend(env, ios);
formatter fmt = mk_pp_formatter(env);
std::cout << "Basic printer\n";
std::cout << mk_shared_expr(10) << std::endl;
std::cout << "----------------------------\nPretty printer\n";
@ -31,19 +31,19 @@ static void tst1() {
}
static void tst2() {
frontend f;
formatter fmt = mk_pp_formatter(f);
environment env; io_state ios; init_frontend(env, ios);
formatter fmt = mk_pp_formatter(env);
expr a = Const("a");
expr t = Fun({a, Type()}, mk_shared_expr(10));
expr g = Const("g");
std::cout << fmt(g(t, t, t)) << std::endl;
formatter fmt2 = mk_pp_formatter(f);
formatter fmt2 = mk_pp_formatter(env);
std::cout << fmt2(g(t, t, t), options({"lean", "pp", "alias_min_weight"}, 100)) << std::endl;
}
static void tst3() {
frontend f;
formatter fmt = mk_pp_formatter(f);
environment env; io_state ios; init_frontend(env, ios);
formatter fmt = mk_pp_formatter(env);
expr g = Const("g");
expr a = Const("\u03BA");
expr b = Const("\u03C1");
@ -58,28 +58,28 @@ static void tst3() {
}
static void tst4() {
frontend f;
io_state const & s1 = f.get_state();
io_state s2 = f.get_state();
environment env; io_state ios; init_frontend(env, ios);
io_state const & s1 = ios;
io_state s2 = ios;
regular(s1) << And(Const("a"), Const("b")) << "\n";
regular(f) << And(Const("a"), Const("b")) << "\n";
diagnostic(f) << And(Const("a"), Const("b")) << "\n";
f.set_option(name{"lean", "pp", "notation"}, false);
regular(f) << And(Const("a"), Const("b")) << "\n";
regular(ios) << And(Const("a"), Const("b")) << "\n";
diagnostic(ios) << And(Const("a"), Const("b")) << "\n";
ios.set_option(name{"lean", "pp", "notation"}, false);
regular(ios) << And(Const("a"), Const("b")) << "\n";
regular(s1) << And(Const("a"), Const("b")) << "\n";
regular(s2) << And(Const("a"), Const("b")) << "\n";
}
static void tst5() {
frontend f;
environment env; io_state ios; init_frontend(env, ios);
std::shared_ptr<string_output_channel> out(new string_output_channel());
f.set_regular_channel(out);
f.set_option(name{"pp", "unicode"}, true);
f.set_option(name{"lean", "pp", "notation"}, true);
regular(f) << And(Const("a"), Const("b"));
ios.set_regular_channel(out);
ios.set_option(name{"pp", "unicode"}, true);
ios.set_option(name{"lean", "pp", "notation"}, true);
regular(ios) << And(Const("a"), Const("b"));
lean_assert(out->str() == "a ∧ b");
f.set_option(name{"lean", "pp", "notation"}, false);
regular(f) << " " << And(Const("a"), Const("b"));
ios.set_option(name{"lean", "pp", "notation"}, false);
regular(ios) << " " << And(Const("a"), Const("b"));
lean_assert(out->str() == "a ∧ b and a b");
}
@ -91,14 +91,14 @@ static expr mk_deep(unsigned depth) {
}
static void tst6() {
frontend f;
environment env; io_state ios; init_frontend(env, ios);
std::shared_ptr<string_output_channel> out(new string_output_channel());
f.set_regular_channel(out);
ios.set_regular_channel(out);
expr t = mk_deep(10);
f.set_option(name{"lean", "pp", "max_depth"}, 5);
f.set_option(name{"pp", "colors"}, false);
f.set_option(name{"pp", "unicode"}, false);
regular(f) << t;
ios.set_option(name{"lean", "pp", "max_depth"}, 5);
ios.set_option(name{"pp", "colors"}, false);
ios.set_option(name{"pp", "unicode"}, false);
regular(ios) << t;
lean_assert(out->str() == "f (f (f (f (f (...)))))");
}