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

refactor(library): add compile_equations function, generic_exception, and cleanup elaborator_exception

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-15 11:04:55 -08:00
parent 5a9cd9eed4
commit 8939351903
15 changed files with 298 additions and 64 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -821,10 +821,10 @@ expr const & elaborator::get_equation_fn(expr const & eq) const {
while (is_lambda(it))
it = binding_body(it);
if (!is_equation(it))
throw_elaborator_exception(env(), "ill-formed equation", eq);
throw_elaborator_exception("ill-formed equation", eq);
expr const & fn = get_app_fn(equation_lhs(it));
if (!is_local(fn))
throw_elaborator_exception(env(), "ill-formed equation", eq);
throw_elaborator_exception("ill-formed equation", eq);
return fn;
}
@ -911,11 +911,8 @@ static expr assign_equation_lhs_metas(type_checker & tc, expr const & eqns) {
} else {
name x("x");
buffer<expr> locals;
while (is_lambda(eq)) {
expr local = mk_local(tc.mk_fresh_name(), binding_name(eq), binding_domain(eq), binding_info(eq));
locals.push_back(local);
eq = instantiate(binding_body(eq), local);
}
name_generator ngen = tc.mk_ngen();
eq = fun_to_telescope(ngen, eq, locals, optional<binder_info>());
lean_assert(num_fns <= locals.size());
lean_assert(is_equation(eq));
unsigned idx = 1;
@ -955,25 +952,22 @@ static expr assign_equation_lhs_metas(type_checker & tc, expr const & eqns) {
}
}
if (is_wf_equations(eqns)) {
return mk_equations(num_fns, new_eqs.size(), new_eqs.data(), equations_wf_rel(eqns), equations_wf_proof(eqns));
} else {
return mk_equations(num_fns, new_eqs.size(), new_eqs.data());
}
return update_equations(eqns, new_eqs);
}
static constraint mk_equations_cnstr(environment const & env, io_state const & ios, expr const & m, expr const & eqns,
bool relax) {
justification j = mk_failed_to_synthesize_jst(env, m);
auto choice_fn = [=](expr const & , expr const &, substitution const & s,
auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s,
name_generator const & ngen) {
substitution new_s = s;
expr new_eqns = substitution(s).instantiate_all(eqns);
type_checker_ptr tc = mk_type_checker(env, ngen, relax);
new_eqns = assign_equation_lhs_metas(*tc, new_eqns);
regular(env, ios) << "Equations:\n" << new_eqns << "\n\n";
// TODO(Leo): invoke equations compiler
return lazy_list<constraints>(constraints());
expr val = compile_equations(*tc, ios, new_eqns, meta, meta_type, relax);
justification j = mk_justification("equation compilation", some_expr(eqns));
constraint c = mk_eq_cnstr(meta, val, j, relax);
return lazy_list<constraints>(c);
};
bool owner = true;
return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::MaxDelayed), owner, j, relax);
@ -988,7 +982,7 @@ expr elaborator::visit_equations(expr const & eqns, constraint_seq & cs) {
to_equations(eqns, eqs);
if (eqs.empty())
throw_elaborator_exception(env(), "invalid empty set of recursive equations", eqns);
throw_elaborator_exception("invalid empty set of recursive equations", eqns);
if (is_wf_equations(eqns)) {
new_R = visit(equations_wf_rel(eqns), cs);
@ -1069,21 +1063,21 @@ expr elaborator::visit_equation(expr const & eq, constraint_seq & cs) {
expr elaborator::visit_inaccessible(expr const & e, constraint_seq & cs) {
if (!m_in_equation_lhs)
throw_elaborator_exception(env(), "invalid occurrence of 'inaccessible' annotation, it must only occur in the "
throw_elaborator_exception("invalid occurrence of 'inaccessible' annotation, it must only occur in the "
"left-hand-side of recursive equations", e);
return mk_inaccessible(visit(get_annotation_arg(e), cs));
}
expr elaborator::visit_decreasing(expr const & e, constraint_seq & cs) {
if (!m_equation_lhs)
throw_elaborator_exception(env(), "invalid occurrence of 'decreasing' annotation, it must only occur in "
throw_elaborator_exception("invalid occurrence of 'decreasing' annotation, it must only occur in "
"the right-hand-side of recursive equations", e);
if (!m_equation_R)
throw_elaborator_exception(env(), "invalid occurrence of 'decreasing' annotation, it can only be used when "
throw_elaborator_exception("invalid occurrence of 'decreasing' annotation, it can only be used when "
"recursive equations are being defined by well-founded recursion", e);
expr const & lhs_fn = get_app_fn(*m_equation_lhs);
if (get_app_fn(decreasing_app(e)) != lhs_fn)
throw_elaborator_exception(env(), "invalid occurrence of 'decreasing' annotation, expression must be an "
throw_elaborator_exception("invalid occurrence of 'decreasing' annotation, expression must be an "
"application of the recursive function being defined", e);
expr dec_app = visit(decreasing_app(e), cs);
expr dec_proof = visit(decreasing_proof(e), cs);
@ -1096,7 +1090,7 @@ expr elaborator::visit_decreasing(expr const & e, constraint_seq & cs) {
get_app_args(*m_equation_lhs, old_args);
get_app_args(dec_app, new_args);
if (new_args.size() != old_args.size() || new_args.size() != ts.size())
throw_elaborator_exception(env(), "invalid recursive application, mistmatch in the number of arguments", e);
throw_elaborator_exception("invalid recursive application, mistmatch in the number of arguments", e);
expr old_tuple = mk_sigma_mk(tc, ts, old_args, cs);
expr new_tuple = mk_sigma_mk(tc, ts, new_args, cs);
expr expected_dec_proof_type = mk_app(mk_app(*m_equation_R, new_tuple, e.get_tag()), old_tuple, e.get_tag());
@ -1554,13 +1548,13 @@ std::tuple<expr, expr, level_param_names> elaborator::operator()(
}
// Auxiliary procedure for #translate
static expr translate_local_name(environment const & env, list<expr> const & ctx, name const & local_name,
static expr translate_local_name(list<expr> const & ctx, name const & local_name,
expr const & src) {
for (expr const & local : ctx) {
if (local_pp_name(local) == local_name)
return copy(local);
}
throw_elaborator_exception(env, sstream() << "unknown identifier '" << local_name << "'", src);
throw_elaborator_exception(sstream() << "unknown identifier '" << local_name << "'", src);
}
/** \brief Translated local constants (and undefined constants) occurring in \c e into
@ -1573,13 +1567,13 @@ static expr translate(environment const & env, list<expr> const & ctx, expr cons
return some_expr(e); // ignore placeholders
} else if (is_constant(e)) {
if (!env.find(const_name(e))) {
expr new_e = copy_tag(e, translate_local_name(env, ctx, const_name(e), e));
expr new_e = copy_tag(e, translate_local_name(ctx, const_name(e), e));
return some_expr(new_e);
} else {
return none_expr();
}
} else if (is_local(e)) {
expr new_e = copy_tag(e, translate_local_name(env, ctx, local_pp_name(e), e));
expr new_e = copy_tag(e, translate_local_name(ctx, local_pp_name(e), e));
return some_expr(new_e);
} else {
return none_expr();

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

@ -4,23 +4,23 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "kernel/kernel_exception.h"
#include "library/generic_exception.h"
#include "frontends/lean/elaborator_exception.h"
namespace lean {
[[ noreturn ]] void throw_elaborator_exception(environment const & env, char const * msg, expr const & m) {
throw_kernel_exception(env, msg, m);
[[ noreturn ]] void throw_elaborator_exception(char const * msg, expr const & m) {
throw_generic_exception(msg, m);
}
[[ noreturn ]] void throw_elaborator_exception(environment const & env, sstream const & strm, expr const & m) {
throw_kernel_exception(env, strm, m);
[[ noreturn ]] void throw_elaborator_exception(sstream const & strm, expr const & m) {
throw_generic_exception(strm, m);
}
[[ noreturn ]] void throw_elaborator_exception(environment const & env, char const * msg, expr const & m, pp_fn const & fn) {
throw_kernel_exception(env, msg, m, fn);
[[ noreturn ]] void throw_elaborator_exception(char const * msg, expr const & m, pp_fn const & fn) {
throw_generic_exception(msg, m, fn);
}
[[ noreturn ]] void throw_elaborator_exception(environment const & env, expr const & m, pp_fn const & fn) {
throw_kernel_exception(env, m, fn);
[[ noreturn ]] void throw_elaborator_exception(expr const & m, pp_fn const & fn) {
throw_generic_exception(m, fn);
}
}

8
src/frontends/lean/elaborator_exception.h
View file

@ -9,8 +9,8 @@ Author: Leonardo de Moura
#include "kernel/formatter.h"
namespace lean {
[[ noreturn ]] void throw_elaborator_exception(environment const & env, char const * msg, expr const & m);
[[ noreturn ]] void throw_elaborator_exception(environment const & env, sstream const & strm, expr const & m);
[[ noreturn ]] void throw_elaborator_exception(environment const & env, char const * msg, expr const & m, pp_fn const & fn);
[[ noreturn ]] void throw_elaborator_exception(environment const & env, expr const & m, pp_fn const & fn);
[[ noreturn ]] void throw_elaborator_exception(char const * msg, expr const & m);
[[ noreturn ]] void throw_elaborator_exception(sstream const & strm, expr const & m);
[[ noreturn ]] void throw_elaborator_exception(char const * msg, expr const & m, pp_fn const & fn);
[[ noreturn ]] void throw_elaborator_exception(expr const & m, pp_fn const & fn);
}

4
src/frontends/lean/placeholder_elaborator.cpp
View file

@ -154,7 +154,7 @@ struct placeholder_elaborator : public choice_iterator {
choice_iterator(), m_C(C), m_ctx(ctx), m_meta(meta), m_meta_type(meta_type),
m_local_instances(local_insts), m_instances(instances), m_jst(j), m_depth(depth) {
if (m_depth > m_C->get_max_depth()) {
throw_elaborator_exception(C->env(), "maximum class-instance resolution depth has been reached "
throw_elaborator_exception("maximum class-instance resolution depth has been reached "
"(the limit can be increased by setting option 'elaborator.instance_max_depth') "
"(the class-instance resolution trace can be visualized by setting option 'elaborator.trace_instances')",
C->get_main_meta());
@ -363,7 +363,7 @@ constraint mk_placeholder_root_cnstr(std::shared_ptr<placeholder_context> const
cnstrs = p.second;
expr next_solution = subst.instantiate(new_meta);
if (solution) {
throw_elaborator_exception(env, m, [=](formatter const & fmt) {
throw_elaborator_exception(m, [=](formatter const & fmt) {
format r = format("ambiguous class-instance resolution, "
"there is more than one solution");
r += pp_indent_expr(fmt, *solution);

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

@ -360,7 +360,7 @@ struct structure_cmd_fn {
return optional<unsigned>(i);
} else {
expr prev_ftype = mlocal_type(m_fields[i]);
throw_elaborator_exception(m_env, parent, [=](formatter const & fmt) {
throw_elaborator_exception(parent, [=](formatter const & fmt) {
format r = format("invalid 'structure' header, field '");
r += format(fname);
r += format("' from '");
@ -400,8 +400,7 @@ struct structure_cmd_fn {
expr intro_type = inductive::intro_rule_type(intro);
intro_type = instantiate_univ_params(intro_type, lparams, const_levels(parent_fn));
if (nparams != args.size()) {
throw_elaborator_exception(m_env,
sstream() << "invalid 'structure' header, number of argument "
throw_elaborator_exception(sstream() << "invalid 'structure' header, number of argument "
"mismatch for parent structure '" << parent_name << "'",
parent);
}
@ -419,8 +418,7 @@ struct structure_cmd_fn {
fmap.push_back(*fidx);
field = m_fields[*fidx];
if (local_info(field) != binding_info(intro_type)) {
throw_elaborator_exception(m_env,
sstream() << "invalid 'structure' header, field '" << fname <<
throw_elaborator_exception(sstream() << "invalid 'structure' header, field '" << fname <<
"' has already been declared with a different binder annotation",
parent);
}
@ -479,7 +477,7 @@ struct structure_cmd_fn {
[&](expr const & inherited_field) {
return local_pp_name(inherited_field) == local_pp_name(new_field);
}) != m_fields.end()) {
throw_elaborator_exception(m_env, sstream() << "field '" << local_pp_name(new_field) <<
throw_elaborator_exception(sstream() << "field '" << local_pp_name(new_field) <<
"' has been declared in parent structure",
new_field);
}

15
src/library/CMakeLists.txt
View file

@ -4,12 +4,13 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
normalize.cpp shared_environment.cpp module.cpp coercion.cpp
private.cpp placeholder.cpp aliases.cpp level_names.cpp
update_declaration.cpp choice.cpp scoped_ext.cpp locals.cpp
standard_kernel.cpp sorry.cpp replace_visitor.cpp
unifier.cpp unifier_plugin.cpp inductive_unifier_plugin.cpp
explicit.cpp num.cpp string.cpp head_map.cpp match.cpp
definition_cache.cpp declaration_index.cpp class.cpp util.cpp
print.cpp annotation.cpp typed_expr.cpp let.cpp type_util.cpp
protected.cpp metavar_closure.cpp reducible.cpp init_module.cpp
fingerprint.cpp flycheck.cpp hott_kernel.cpp local_context.cpp)
standard_kernel.cpp sorry.cpp replace_visitor.cpp unifier.cpp
unifier_plugin.cpp inductive_unifier_plugin.cpp explicit.cpp num.cpp
string.cpp head_map.cpp match.cpp definition_cache.cpp
declaration_index.cpp class.cpp util.cpp print.cpp annotation.cpp
typed_expr.cpp let.cpp type_util.cpp protected.cpp
metavar_closure.cpp reducible.cpp init_module.cpp
generic_exception.cpp fingerprint.cpp flycheck.cpp hott_kernel.cpp
local_context.cpp)
target_link_libraries(library ${LEAN_LIBS})

116
src/library/definitional/equations.cpp
View file

@ -6,8 +6,15 @@ Author: Leonardo de Moura
*/
#include <string>
#include "kernel/expr.h"
#include "kernel/type_checker.h"
#include "kernel/abstract.h"
#include "kernel/error_msgs.h"
#include "library/generic_exception.h"
#include "library/kernel_serializer.h"
#include "library/io_state_stream.h"
#include "library/annotation.h"
#include "library/util.h"
#include "library/tactic/inversion_tactic.h"
namespace lean {
static name * g_equations_name = nullptr;
@ -142,6 +149,17 @@ expr mk_equations(unsigned num_fns, unsigned num_eqs, expr const * eqs, expr con
return mk_macro(def, args.size(), args.data());
}
expr update_equations(expr const & eqns, buffer<expr> const & new_eqs) {
lean_assert(is_equations(eqns));
lean_assert(!new_eqs.empty());
if (is_wf_equations(eqns)) {
return mk_equations(equations_num_fns(eqns), new_eqs.size(), new_eqs.data(),
equations_wf_rel(eqns), equations_wf_proof(eqns));
} else {
return mk_equations(equations_num_fns(eqns), new_eqs.size(), new_eqs.data());
}
}
expr mk_inaccessible(expr const & e) { return mk_annotation(*g_inaccessible_name, e); }
bool is_inaccessible(expr const & e) { return is_annotation(e, *g_inaccessible_name); }
@ -195,4 +213,102 @@ void finalize_equations() {
delete g_decreasing_name;
delete g_inaccessible_name;
}
class equation_compiler_fn {
type_checker & m_tc;
io_state const & m_ios;
expr m_meta;
expr m_meta_type;
bool m_relax;
environment const & env() const { return m_tc.env(); }
struct validate_exception {
expr m_expr;
validate_exception(expr const & e):m_expr(e) {}
};
[[ noreturn ]] void throw_error(char const * msg, expr const & src) { throw_generic_exception(msg, src); }
[[ noreturn ]] void throw_error(expr const & src, pp_fn const & fn) { throw_generic_exception(src, fn); }
// --------------------------------
// Pattern validation/normalization
// --------------------------------
expr validate_lhs_arg(expr arg) {
if (is_inaccessible(arg))
return arg;
if (is_local(arg))
return arg;
expr new_arg = m_tc.whnf(arg).first;
if (is_local(new_arg))
return new_arg;
buffer<expr> arg_args;
expr const & fn = get_app_args(new_arg, arg_args);
if (!is_constant(fn) || !inductive::is_intro_rule(env(), const_name(fn)))
throw validate_exception(arg);
for (expr & arg_arg : arg_args)
arg_arg = validate_lhs_arg(arg_arg);
return mk_app(fn, arg_args);
}
expr validate_lhs(expr const & lhs) {
buffer<expr> args;
expr fn = get_app_args(lhs, args);
for (expr & arg : args) {
try {
arg = validate_lhs_arg(arg);
} catch (validate_exception & ex) {
expr problem_expr = ex.m_expr;
throw_error(lhs, [=](formatter const & fmt) {
format r("invalid argument, it is not a constructor, variable, "
"nor it is marked as an inaccessible pattern");
r += pp_indent_expr(fmt, problem_expr);
r += compose(line(), format("in the following equation left-hand-side"));
r += pp_indent_expr(fmt, lhs);
return r;
});
}
}
return mk_app(fn, args);
}
expr validate_patterns_core(expr eq) {
buffer<expr> args;
name_generator ngen = m_tc.mk_ngen();
eq = fun_to_telescope(ngen, eq, args, optional<binder_info>());
lean_assert(is_equation(eq));
expr new_lhs = validate_lhs(equation_lhs(eq));
return Fun(args, mk_equation(new_lhs, equation_rhs(eq)));
}
expr validate_patterns(expr const & eqns) {
lean_assert(is_equations(eqns));
buffer<expr> eqs;
buffer<expr> new_eqs;
to_equations(eqns, eqs);
for (expr const & eq : eqs) {
new_eqs.push_back(validate_patterns_core(eq));
}
return update_equations(eqns, new_eqs);
}
public:
equation_compiler_fn(type_checker & tc, io_state const & ios, expr const & meta, expr const & meta_type, bool relax):
m_tc(tc), m_ios(ios), m_meta(meta), m_meta_type(meta_type), m_relax(relax) {
}
expr operator()(expr eqns) {
proof_state ps = to_proof_state(m_meta, m_meta_type, m_tc.mk_ngen(), m_relax);
eqns = validate_patterns(eqns);
regular(env(), m_ios) << "Equations:\n" << eqns << "\n";
regular(env(), m_ios) << ps.pp(env(), m_ios) << "\n\n";
return eqns;
}
};
expr compile_equations(type_checker & tc, io_state const & ios, expr const & eqns,
expr const & meta, expr const & meta_type, bool relax) {
return equation_compiler_fn(tc, ios, meta, meta_type, relax)(eqns);
}
}

7
src/library/definitional/equations.h
View file

@ -8,6 +8,9 @@ Author: Leonardo de Moura
#include "kernel/expr.h"
namespace lean {
class type_checker;
class io_state;
bool is_equation(expr const & e);
expr const & equation_lhs(expr const & e);
expr const & equation_rhs(expr const & e);
@ -29,10 +32,14 @@ expr const & equations_wf_proof(expr const & e);
expr const & equations_wf_rel(expr const & e);
expr mk_equations(unsigned num_fns, unsigned num_eqs, expr const * eqs);
expr mk_equations(unsigned num_fns, unsigned num_eqs, expr const * eqs, expr const & R, expr const & Hwf);
expr update_equations(expr const & eqns, buffer<expr> const & new_eqs);
expr mk_inaccessible(expr const & e);
bool is_inaccessible(expr const & e);
expr compile_equations(type_checker & tc, io_state const & ios, expr const & eqns,
expr const & meta, expr const & meta_type, bool relax);
void initialize_equations();
void finalize_equations();
}

10
src/library/error_handling/error_handling.cpp
View file

@ -13,8 +13,9 @@ Author: Leonardo de Moura
#include "library/io_state_stream.h"
#include "library/unifier.h"
#include "library/parser_nested_exception.h"
#include "library/error_handling/error_handling.h"
#include "library/generic_exception.h"
#include "library/flycheck.h"
#include "library/error_handling/error_handling.h"
namespace lean {
void display_pos(io_state_stream const & ios, char const * strm_name, unsigned line, unsigned pos) {
@ -74,6 +75,11 @@ static void display_error(io_state_stream const & ios, pos_info_provider const *
ios << " " << ex << endl;
}
static void display_error(io_state_stream const & ios, pos_info_provider const * p, generic_exception const & ex) {
display_error_pos(ios, p, ex.get_main_expr());
ios << " " << ex << endl;
}
static void display_error(io_state_stream const & ios, pos_info_provider const * p, unifier_exception const & ex) {
formatter fmt = ios.get_formatter();
options opts = ios.get_options();
@ -142,6 +148,8 @@ void display_error(io_state_stream const & ios, pos_info_provider const * p, exc
flycheck_error err(ios);
if (auto k_ex = dynamic_cast<kernel_exception const *>(&ex)) {
display_error(ios, p, *k_ex);
} else if (auto g_ex = dynamic_cast<generic_exception const *>(&ex)) {
display_error(ios, p, *g_ex);
} else if (auto e_ex = dynamic_cast<unifier_exception const *>(&ex)) {
display_error(ios, p, *e_ex);
} else if (auto ls_ex = dynamic_cast<script_nested_exception const *>(&ex)) {

44
src/library/generic_exception.cpp Normal file
View file

@ -0,0 +1,44 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <string>
#include "library/generic_exception.h"
namespace lean {
[[ noreturn ]] void throw_generic_exception(char const * msg, optional<expr> const & m) {
std::string msg_str = msg;
throw generic_exception(msg, m, [=](formatter const &) { return format(msg_str); });
}
[[ noreturn ]] void throw_generic_exception(sstream const & strm, optional<expr> const & m) {
throw_generic_exception(strm.str().c_str(), m);
}
[[ noreturn ]] void throw_generic_exception(char const * msg, expr const & m) {
throw_generic_exception(msg, some_expr(m));
}
[[ noreturn ]] void throw_generic_exception(sstream const & strm, expr const & m) {
throw_generic_exception(strm, some_expr(m));
}
[[ noreturn ]] void throw_generic_exception(char const * msg, optional<expr> const & m, pp_fn const & fn) {
throw generic_exception(msg, m, fn);
}
[[ noreturn ]] void throw_generic_exception(char const * msg, expr const & m, pp_fn const & fn) {
throw_generic_exception(msg, some_expr(m), fn);
}
[[ noreturn ]] void throw_generic_exception(optional<expr> const & m, pp_fn const & fn) {
throw generic_exception(m, fn);
}
[[ noreturn ]] void throw_generic_exception(expr const & m, pp_fn const & fn) {
throw_generic_exception(some_expr(m), fn);
}
}

38
src/library/generic_exception.h Normal file
View file

@ -0,0 +1,38 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <string>
#include "util/sstream.h"
#include "kernel/expr.h"
#include "kernel/formatter.h"
namespace lean {
class generic_exception : public exception {
protected:
optional<expr> m_main_expr;
pp_fn m_pp_fn;
public:
generic_exception(char const * msg, optional<expr> const & m, pp_fn const & fn):
exception(msg), m_main_expr(m), m_pp_fn(fn) {}
generic_exception(optional<expr> const & m, pp_fn const & fn):
exception(), m_main_expr(m), m_pp_fn(fn) {}
virtual ~generic_exception() noexcept {}
virtual optional<expr> get_main_expr() const { return m_main_expr; }
virtual format pp(formatter const & fmt) const { return m_pp_fn(fmt); }
virtual exception * clone() const { return new generic_exception(m_msg.c_str(), m_main_expr, m_pp_fn); }
virtual void rethrow() const { throw *this; }
};
[[ noreturn ]] void throw_generic_exception(char const * msg, optional<expr> const & m);
[[ noreturn ]] void throw_generic_exception(sstream const & strm, optional<expr> const & m);
[[ noreturn ]] void throw_generic_exception(char const * msg, expr const & m);
[[ noreturn ]] void throw_generic_exception(sstream const & strm, expr const & m);
[[ noreturn ]] void throw_generic_exception(char const * msg, optional<expr> const & m, pp_fn const & fn);
[[ noreturn ]] void throw_generic_exception(char const * msg, expr const & m, pp_fn const & fn);
[[ noreturn ]] void throw_generic_exception(optional<expr> const & m, pp_fn const & fn);
[[ noreturn ]] void throw_generic_exception(expr const & m, pp_fn const & fn);
}

10
src/library/io_state_stream.cpp
View file

@ -4,8 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "library/io_state_stream.h"
#include "kernel/kernel_exception.h"
#include "library/io_state_stream.h"
#include "library/generic_exception.h"
namespace lean {
io_state_stream const & operator<<(io_state_stream const & out, endl_class) {
out.get_stream() << std::endl;
@ -24,6 +26,12 @@ io_state_stream const & operator<<(io_state_stream const & out, kernel_exception
return out;
}
io_state_stream const & operator<<(io_state_stream const & out, generic_exception const & ex) {
options const & opts = out.get_options();
out.get_stream() << mk_pair(ex.pp(out.get_formatter()), opts);
return out;
}
io_state_stream const & operator<<(io_state_stream const & out, format const & f) {
options const & opts = out.get_options();
out.get_stream() << mk_pair(f, opts);

2
src/library/io_state_stream.h
View file

@ -37,10 +37,12 @@ struct endl_class { endl_class() {} };
const endl_class endl;
class kernel_exception;
class generic_exception;
io_state_stream const & operator<<(io_state_stream const & out, endl_class);
io_state_stream const & operator<<(io_state_stream const & out, expr const & e);
io_state_stream const & operator<<(io_state_stream const & out, kernel_exception const & ex);
io_state_stream const & operator<<(io_state_stream const & out, generic_exception const & ex);
io_state_stream const & operator<<(io_state_stream const & out, format const & f);
template<typename T> io_state_stream const & operator<<(io_state_stream const & out, T const & t) {
out.get_stream() << t;

22
src/library/util.cpp
View file

@ -110,17 +110,27 @@ expr instantiate_univ_param (expr const & e, name const & p, level const & l) {
return instantiate_univ_params(e, to_list(p), to_list(l));
}
expr to_telescope(name_generator & ngen, expr type, buffer<expr> & telescope, optional<binder_info> const & binfo) {
while (is_pi(type)) {
expr to_telescope(bool pi, name_generator & ngen, expr e, buffer<expr> & telescope,
optional<binder_info> const & binfo) {
while ((pi && is_pi(e)) || (!pi && is_lambda(e))) {
expr local;
if (binfo)
local = mk_local(ngen.next(), binding_name(type), binding_domain(type), *binfo);
local = mk_local(ngen.next(), binding_name(e), binding_domain(e), *binfo);
else
local = mk_local(ngen.next(), binding_name(type), binding_domain(type), binding_info(type));
local = mk_local(ngen.next(), binding_name(e), binding_domain(e), binding_info(e));
telescope.push_back(local);
type = instantiate(binding_body(type), local);
e = instantiate(binding_body(e), local);
}
return type;
return e;
}
expr to_telescope(name_generator & ngen, expr const & type, buffer<expr> & telescope, optional<binder_info> const & binfo) {
return to_telescope(true, ngen, type, telescope, binfo);
}
expr fun_to_telescope(name_generator & ngen, expr const & e, buffer<expr> & telescope,
optional<binder_info> const & binfo) {
return to_telescope(false, ngen, e, telescope, binfo);
}
expr to_telescope(type_checker & tc, expr type, buffer<expr> & telescope, optional<binder_info> const & binfo,

12
src/library/util.h
View file

@ -36,12 +36,12 @@ bool is_reflexive_datatype(type_checker & tc, name const & n);
*/
bool is_inductive_predicate(environment const & env, name const & n);
/** \brief "Consume" Pi-type \c type. This method creates local constants based on the domain of \c type
/** \brief "Consume" Pi-type \c type. This procedure creates local constants based on the domain of \c type
and store them in telescope. If \c binfo is provided, then the local constants are annoted with the given
binder_info, otherwise the procedure uses the one attached in the domain.
The procedure returns the "body" of type.
*/
expr to_telescope(name_generator & ngen, expr type, buffer<expr> & telescope,
expr to_telescope(name_generator & ngen, expr const & type, buffer<expr> & telescope,
optional<binder_info> const & binfo = optional<binder_info>());
/** \brief Similar to previous procedure, but puts \c type in whnf */
expr to_telescope(type_checker & tc, expr type, buffer<expr> & telescope,
@ -53,6 +53,14 @@ expr to_telescope(type_checker & tc, expr type, buffer<expr> & telescope,
*/
expr to_telescope(type_checker & tc, expr type, buffer<expr> & telescope, optional<binder_info> const & binfo,
constraint_seq & cs);
/** \brief "Consume" fun/lambda. This procedure creates local constants based on the arguments of \c e
and store them in telescope. If \c binfo is provided, then the local constants are annoted with the given
binder_info, otherwise the procedure uses the one attached to the arguments.
The procedure returns the "body" of function.
*/
expr fun_to_telescope(name_generator & ngen, expr const & e, buffer<expr> & telescope, optional<binder_info> const & binfo);
/** \brief Return the universe where inductive datatype resides
\pre \c ind_type is of the form <tt>Pi (a_1 : A_1) (a_2 : A_2[a_1]) ..., Type.{lvl}</tt>
*/