chore: remove io_state & abstract_type_context
This commit is contained in:
Sebastian Ullrich
Leonardo de Moura
parent
4278480ea3
commit
74c2d1dca9
13 changed files with 4 additions and 544 deletions
|
|
@ -1,4 +1,4 @@
|
|||
add_library(library OBJECT expr_lt.cpp io_state.cpp
|
||||
add_library(library OBJECT expr_lt.cpp
|
||||
bin_app.cpp constants.cpp max_sharing.cpp
|
||||
module.cpp sorry.cpp replace_visitor.cpp num.cpp
|
||||
class.cpp util.cpp print.cpp annotation.cpp
|
||||
|
|
@ -6,5 +6,4 @@ add_library(library OBJECT expr_lt.cpp io_state.cpp
|
|||
pp_options.cpp projection.cpp
|
||||
aux_recursors.cpp trace.cpp
|
||||
profiling.cpp time_task.cpp
|
||||
formatter.cpp
|
||||
abstract_type_context.cpp)
|
||||
formatter.cpp)
|
||||
|
|
|
|||
|
|
@ -1,15 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include "kernel/abstract.h"
|
||||
#include "library/abstract_type_context.h"
|
||||
|
||||
namespace lean {
|
||||
push_local_fn::~push_local_fn() {
|
||||
for (unsigned i = 0; i < m_counter; i++)
|
||||
m_ctx.pop_local();
|
||||
}
|
||||
}
|
||||
|
|
@ -1,47 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include "kernel/expr.h"
|
||||
|
||||
namespace lean {
|
||||
class abstract_type_context {
|
||||
options m_options;
|
||||
public:
|
||||
abstract_type_context(options const & opts):m_options(opts) {}
|
||||
abstract_type_context() {}
|
||||
options const & get_options() const { return m_options; }
|
||||
virtual ~abstract_type_context() {}
|
||||
virtual environment const & env() const { lean_unreachable(); }
|
||||
virtual expr whnf(expr const &) { lean_unreachable(); }
|
||||
virtual name next_name() { lean_unreachable(); }
|
||||
virtual expr relaxed_whnf(expr const &) { lean_unreachable(); }
|
||||
virtual bool is_def_eq(expr const &, expr const &) { lean_unreachable(); }
|
||||
virtual bool relaxed_is_def_eq(expr const &, expr const &) { lean_unreachable(); }
|
||||
virtual expr infer(expr const &) { lean_unreachable(); }
|
||||
/** \brief Simular to \c infer, but also performs type checking.
|
||||
\remark Default implementation just invokes \c infer. */
|
||||
virtual expr check(expr const &) { lean_unreachable(); }
|
||||
virtual optional<expr> is_stuck(expr const &) { lean_unreachable(); }
|
||||
virtual optional<name> get_local_pp_name(expr const &) { lean_unreachable(); }
|
||||
virtual expr push_local(name const &, expr const &, binder_info) { lean_unreachable(); }
|
||||
virtual void pop_local() { lean_unreachable(); }
|
||||
|
||||
expr check(expr const &, bool) { lean_unreachable(); }
|
||||
};
|
||||
|
||||
class push_local_fn {
|
||||
abstract_type_context & m_ctx;
|
||||
unsigned m_counter;
|
||||
public:
|
||||
push_local_fn(abstract_type_context & ctx):m_ctx(ctx), m_counter(0) {}
|
||||
~push_local_fn();
|
||||
expr operator()(name const & pp_name, expr const & type, binder_info bi = mk_binder_info()) {
|
||||
m_counter++;
|
||||
return m_ctx.push_local(pp_name, type, bi);
|
||||
}
|
||||
};
|
||||
}
|
||||
|
|
@ -5,19 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include <utility>
|
||||
#include "util/option_declarations.h"
|
||||
#include "library/formatter.h"
|
||||
|
||||
#ifndef LEAN_DEFAULT_FORMATTER_HIDE_FULL_TERMS
|
||||
#define LEAN_DEFAULT_FORMATTER_HIDE_FULL_TERMS false
|
||||
#endif
|
||||
|
||||
namespace lean {
|
||||
static name * g_formatter_hide_full = nullptr;
|
||||
|
||||
name const & get_formatter_hide_full_terms_name() { return *g_formatter_hide_full; }
|
||||
bool get_formatter_hide_full_terms(options const & opts) { return opts.get_bool(*g_formatter_hide_full, LEAN_DEFAULT_FORMATTER_HIDE_FULL_TERMS); }
|
||||
|
||||
static std::function<void(std::ostream &, expr const & e)> * g_print = nullptr;
|
||||
|
||||
void set_print_fn(std::function<void(std::ostream &, expr const &)> const & fn) {
|
||||
|
|
@ -37,14 +27,9 @@ std::ostream & operator<<(std::ostream & out, expr const & e) {
|
|||
void print(lean::expr const & a) { std::cout << a << std::endl; }
|
||||
|
||||
void initialize_formatter() {
|
||||
g_formatter_hide_full = new name{"formatter", "hide_full_terms"};
|
||||
mark_persistent(g_formatter_hide_full->raw());
|
||||
register_bool_option(*g_formatter_hide_full, LEAN_DEFAULT_FORMATTER_HIDE_FULL_TERMS,
|
||||
"(formatter) replace terms which do not contain metavariables with `...`");
|
||||
}
|
||||
|
||||
void finalize_formatter() {
|
||||
delete g_formatter_hide_full;
|
||||
delete g_print;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -7,31 +7,11 @@ Author: Leonardo de Moura
|
|||
#pragma once
|
||||
#include <memory>
|
||||
#include <utility>
|
||||
#include "kernel/expr.h"
|
||||
#include "util/options.h"
|
||||
#include "util/format.h"
|
||||
#include "library/abstract_type_context.h"
|
||||
|
||||
namespace lean {
|
||||
name const & get_formatter_hide_full_terms_name();
|
||||
bool get_formatter_hide_full_terms(options const & opts);
|
||||
|
||||
class formatter {
|
||||
std::function<format(expr const &, options const &)> m_fn;
|
||||
options m_options;
|
||||
public:
|
||||
formatter(options const & o, std::function<format(expr const &, options const &)> const & fn):m_fn(fn), m_options(o) {}
|
||||
format operator()(expr const & e) const { return m_fn(e, m_options); }
|
||||
options const & get_options() const { return m_options; }
|
||||
formatter update_options(options const & o) const { return formatter(o, m_fn); }
|
||||
formatter update_option_if_undef(name const & n, bool v) const { return formatter(m_options.update_if_undef(n, v), m_fn); }
|
||||
};
|
||||
|
||||
typedef std::function<formatter(environment const &, options const &, abstract_type_context &)> formatter_factory;
|
||||
|
||||
std::ostream & operator<<(std::ostream & out, expr const & e);
|
||||
|
||||
typedef std::function<format(formatter const &)> pp_fn;
|
||||
|
||||
void set_print_fn(std::function<void(std::ostream &, expr const &)> const & fn);
|
||||
|
||||
void initialize_formatter();
|
||||
|
|
|
|||
|
|
@ -10,7 +10,6 @@ Author: Leonardo de Moura
|
|||
#include "library/num.h"
|
||||
#include "library/annotation.h"
|
||||
#include "library/protected.h"
|
||||
#include "library/io_state.h"
|
||||
#include "library/print.h"
|
||||
#include "library/util.h"
|
||||
#include "library/pp_options.h"
|
||||
|
|
@ -35,7 +34,6 @@ void finalize_library_core_module() {
|
|||
|
||||
void initialize_library_module() {
|
||||
initialize_print();
|
||||
initialize_io_state();
|
||||
initialize_num();
|
||||
initialize_annotation();
|
||||
initialize_class();
|
||||
|
|
@ -51,7 +49,6 @@ void finalize_library_module() {
|
|||
finalize_class();
|
||||
finalize_annotation();
|
||||
finalize_num();
|
||||
finalize_io_state();
|
||||
finalize_print();
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,105 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include <string>
|
||||
#include "kernel/kernel_exception.h"
|
||||
#include "library/print.h"
|
||||
#include "library/io_state.h"
|
||||
|
||||
namespace lean {
|
||||
static io_state * g_dummy_ios = nullptr;
|
||||
|
||||
io_state const & get_dummy_ios() {
|
||||
return *g_dummy_ios;
|
||||
}
|
||||
|
||||
io_state::io_state():io_state(mk_print_formatter_factory()) {}
|
||||
|
||||
io_state::io_state(formatter_factory const & fmtf):
|
||||
m_formatter_factory(fmtf),
|
||||
m_regular_channel(std::make_shared<stdout_channel>()),
|
||||
m_diagnostic_channel(std::make_shared<stderr_channel>()) {
|
||||
}
|
||||
|
||||
io_state::io_state(options const & opts, formatter_factory const & fmtf):
|
||||
m_options(opts),
|
||||
m_formatter_factory(fmtf),
|
||||
m_regular_channel(std::make_shared<stdout_channel>()),
|
||||
m_diagnostic_channel(std::make_shared<stderr_channel>()) {
|
||||
}
|
||||
io_state::io_state(io_state const & ios, std::shared_ptr<output_channel> const & r, std::shared_ptr<output_channel> const & d):
|
||||
m_options(ios.m_options),
|
||||
m_formatter_factory(ios.m_formatter_factory),
|
||||
m_regular_channel(r),
|
||||
m_diagnostic_channel(d) {
|
||||
}
|
||||
io_state::io_state(io_state const & ios, options const & o):
|
||||
m_options(o),
|
||||
m_formatter_factory(ios.m_formatter_factory),
|
||||
m_regular_channel(ios.m_regular_channel),
|
||||
m_diagnostic_channel(ios.m_diagnostic_channel) {
|
||||
}
|
||||
|
||||
io_state::~io_state() {}
|
||||
|
||||
void io_state::set_regular_channel(std::shared_ptr<output_channel> const & out) {
|
||||
if (out)
|
||||
m_regular_channel = out;
|
||||
}
|
||||
|
||||
void io_state::set_diagnostic_channel(std::shared_ptr<output_channel> const & out) {
|
||||
if (out)
|
||||
m_diagnostic_channel = out;
|
||||
}
|
||||
|
||||
void io_state::set_options(options const & opts) {
|
||||
m_options = opts;
|
||||
}
|
||||
|
||||
void io_state::set_formatter_factory(formatter_factory const & f) {
|
||||
m_formatter_factory = f;
|
||||
}
|
||||
|
||||
LEAN_THREAD_PTR(io_state, g_ios);
|
||||
|
||||
io_state const & get_global_ios() {
|
||||
if (g_ios)
|
||||
return *g_ios;
|
||||
else
|
||||
return get_dummy_ios();
|
||||
}
|
||||
|
||||
scope_global_ios::scope_global_ios(io_state const & ios) {
|
||||
m_old_ios = g_ios;
|
||||
g_ios = const_cast<io_state*>(&ios);
|
||||
}
|
||||
|
||||
scope_global_ios::~scope_global_ios() {
|
||||
g_ios = m_old_ios;
|
||||
}
|
||||
|
||||
char const * formatted_exception::what() const noexcept {
|
||||
if (!m_what_buffer) {
|
||||
options const & opts = get_global_ios().get_options();
|
||||
std::ostringstream out;
|
||||
out << mk_pair(m_fmt, opts);
|
||||
const_cast<formatted_exception*>(this)->m_what_buffer = out.str();
|
||||
}
|
||||
return m_what_buffer->c_str();
|
||||
}
|
||||
|
||||
options const & get_options_from_ios(io_state const & ios) {
|
||||
return ios.get_options();
|
||||
}
|
||||
|
||||
void initialize_io_state() {
|
||||
g_dummy_ios = new io_state(mk_print_formatter_factory());
|
||||
}
|
||||
|
||||
void finalize_io_state() {
|
||||
delete g_dummy_ios;
|
||||
}
|
||||
}
|
||||
|
|
@ -1,86 +0,0 @@
|
|||
/*
|
||||
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include <string>
|
||||
#include "util/output_channel.h"
|
||||
#include "util/options.h"
|
||||
#include "util/exception_with_pos.h"
|
||||
#include "kernel/expr.h"
|
||||
#include "library/formatter.h"
|
||||
|
||||
namespace lean {
|
||||
/**
|
||||
\brief State provided to internal lean procedures that need to:
|
||||
1- Access user defined options
|
||||
2- Produce verbosity messages
|
||||
3- Output results
|
||||
4- Produce formatted output
|
||||
*/
|
||||
class io_state {
|
||||
options m_options;
|
||||
formatter_factory m_formatter_factory;
|
||||
std::shared_ptr<output_channel> m_regular_channel;
|
||||
std::shared_ptr<output_channel> m_diagnostic_channel;
|
||||
public:
|
||||
io_state();
|
||||
io_state(formatter_factory const & fmtf);
|
||||
io_state(options const & opts, formatter_factory const & fmtf);
|
||||
io_state(io_state const & ios, std::shared_ptr<output_channel> const & r, std::shared_ptr<output_channel> const & d);
|
||||
io_state(io_state const & ios, options const & o);
|
||||
~io_state();
|
||||
|
||||
options const & get_options() const { return m_options; }
|
||||
formatter_factory const & get_formatter_factory() const { return m_formatter_factory; }
|
||||
std::shared_ptr<output_channel> const & get_regular_channel_ptr() const { return m_regular_channel; }
|
||||
std::shared_ptr<output_channel> const & get_diagnostic_channel_ptr() const { return m_diagnostic_channel; }
|
||||
output_channel & get_regular_channel() const { return *m_regular_channel; }
|
||||
output_channel & get_diagnostic_channel() const { return *m_diagnostic_channel; }
|
||||
std::ostream & get_regular_stream() const { return m_regular_channel->get_stream(); }
|
||||
std::ostream & get_diagnostic_stream() const { return m_diagnostic_channel->get_stream(); }
|
||||
|
||||
void set_regular_channel(std::shared_ptr<output_channel> const & out);
|
||||
void set_diagnostic_channel(std::shared_ptr<output_channel> const & out);
|
||||
void set_options(options const & opts);
|
||||
void set_formatter_factory(formatter_factory const & f);
|
||||
template<typename T> void set_option(name const & n, T const & v) {
|
||||
set_options(get_options().update(n, v));
|
||||
}
|
||||
};
|
||||
|
||||
/** \brief Return a dummy io_state that is meant to be used in contexts that require an io_state, but it is not really used */
|
||||
io_state const & get_dummy_ios();
|
||||
|
||||
/** \brief Return reference to thread local io_state object. */
|
||||
io_state const & get_global_ios();
|
||||
|
||||
/** \brief Formatted exceptions where the format object must be eagerly constructed.
|
||||
This is slightly different from ext_exception where the format object is built on demand. */
|
||||
class formatted_exception : public exception_with_pos {
|
||||
protected:
|
||||
optional<pos_info> m_pos;
|
||||
format m_fmt;
|
||||
optional<std::string> m_what_buffer;
|
||||
public:
|
||||
explicit formatted_exception(format const & fmt):m_fmt(fmt) {}
|
||||
formatted_exception(optional<pos_info> const & p, format const & fmt):m_pos(p), m_fmt(fmt) {}
|
||||
virtual char const * what() const noexcept override;
|
||||
virtual optional<pos_info> get_pos() const override { return m_pos; }
|
||||
virtual format pp() const { return m_fmt; }
|
||||
};
|
||||
|
||||
struct scope_global_ios {
|
||||
io_state * m_old_ios;
|
||||
public:
|
||||
scope_global_ios(io_state const & ios);
|
||||
~scope_global_ios();
|
||||
};
|
||||
|
||||
options const & get_options_from_ios(io_state const & ios);
|
||||
|
||||
void initialize_io_state();
|
||||
void finalize_io_state();
|
||||
}
|
||||
|
|
@ -11,7 +11,6 @@ Authors: Leonardo de Moura, Gabriel Ebner, Sebastian Ullrich
|
|||
#include <vector>
|
||||
#include <lean/serializer.h>
|
||||
#include <lean/optional.h>
|
||||
#include "library/io_state.h"
|
||||
#include "kernel/environment.h"
|
||||
|
||||
namespace lean {
|
||||
|
|
|
|||
|
|
@ -296,17 +296,6 @@ struct print_expr_fn {
|
|||
}
|
||||
};
|
||||
|
||||
formatter_factory mk_print_formatter_factory() {
|
||||
return [](environment const &, options const & o, abstract_type_context &) { // NOLINT
|
||||
return formatter(o, [=](expr const & e, options const &) {
|
||||
std::ostringstream s;
|
||||
print_expr_fn pr(s);
|
||||
pr(e);
|
||||
return format(s.str());
|
||||
});
|
||||
};
|
||||
}
|
||||
|
||||
void init_default_print_fn() {
|
||||
set_print_fn([](std::ostream & out, expr const & e) {
|
||||
print_expr_fn pr(out);
|
||||
|
|
|
|||
|
|
@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include "kernel/expr.h"
|
||||
#include "library/formatter.h"
|
||||
|
||||
namespace lean {
|
||||
|
|
@ -21,12 +22,6 @@ name pick_unused_name(expr const & t, name const & s);
|
|||
pair<expr, expr> binding_body_fresh(expr const & b, bool preserve_type = false);
|
||||
pair<expr, expr> let_body_fresh(expr const & b, bool preserve_type = false);
|
||||
|
||||
/** \brief Create a simple formatter object based on operator for "print" procedure.
|
||||
|
||||
\remark The print procedure is only used for debugging purposes.
|
||||
*/
|
||||
formatter_factory mk_print_formatter_factory();
|
||||
|
||||
/** \brief Use simple formatter as the default print function */
|
||||
void init_default_print_fn();
|
||||
|
||||
|
|
|
|||
|
|
@ -65,13 +65,6 @@ optional<expr_pair> is_auto_param(expr const & e) {
|
|||
}
|
||||
}
|
||||
|
||||
level get_level(abstract_type_context & ctx, expr const & A) {
|
||||
expr S = ctx.relaxed_whnf(ctx.infer(A));
|
||||
if (!is_sort(S))
|
||||
throw exception("invalid expression, sort expected");
|
||||
return sort_level(S);
|
||||
}
|
||||
|
||||
name mk_fresh_lp_name(names const & lp_names) {
|
||||
name l("l");
|
||||
int i = 1;
|
||||
|
|
@ -324,20 +317,6 @@ expr instantiate_lparam(expr const & e, name const & p, level const & l) {
|
|||
return instantiate_lparams(e, names(p), levels(l));
|
||||
}
|
||||
|
||||
unsigned get_expect_num_args(abstract_type_context & ctx, expr e) {
|
||||
push_local_fn push_local(ctx);
|
||||
unsigned r = 0;
|
||||
while (true) {
|
||||
e = ctx.whnf(e);
|
||||
if (!is_pi(e))
|
||||
return r;
|
||||
// TODO(Leo): try to avoid the following instantiate.
|
||||
expr local = push_local(binding_name(e), binding_domain(e), binding_info(e));
|
||||
e = instantiate(binding_body(e), local);
|
||||
r++;
|
||||
}
|
||||
}
|
||||
|
||||
expr to_telescope(bool pi, local_ctx & lctx, name_generator & ngen, expr e, buffer<expr> & telescope, optional<binder_info> const & binfo) {
|
||||
while ((pi && is_pi(e)) || (!pi && is_lambda(e))) {
|
||||
expr local;
|
||||
|
|
@ -413,20 +392,6 @@ expr mk_and(expr const & a, expr const & b) {
|
|||
return mk_app(*g_and, a, b);
|
||||
}
|
||||
|
||||
expr mk_and_intro(abstract_type_context & ctx, expr const & Ha, expr const & Hb) {
|
||||
return mk_app(*g_and_intro, ctx.infer(Ha), ctx.infer(Hb), Ha, Hb);
|
||||
}
|
||||
|
||||
expr mk_and_left(abstract_type_context & ctx, expr const & H) {
|
||||
expr a_and_b = ctx.whnf(ctx.infer(H));
|
||||
return mk_app(*g_and_left, app_arg(app_fn(a_and_b)), app_arg(a_and_b), H);
|
||||
}
|
||||
|
||||
expr mk_and_right(abstract_type_context & ctx, expr const & H) {
|
||||
expr a_and_b = ctx.whnf(ctx.infer(H));
|
||||
return mk_app(*g_and_right, app_arg(app_fn(a_and_b)), app_arg(a_and_b), H);
|
||||
}
|
||||
|
||||
expr mk_unit(level const & l) {
|
||||
return mk_constant(get_punit_name(), {l});
|
||||
}
|
||||
|
|
@ -446,34 +411,6 @@ expr mk_unit_mk() {
|
|||
return *g_unit_mk;
|
||||
}
|
||||
|
||||
expr mk_pprod(abstract_type_context & ctx, expr const & A, expr const & B) {
|
||||
level l1 = get_level(ctx, A);
|
||||
level l2 = get_level(ctx, B);
|
||||
return mk_app(mk_constant(get_pprod_name(), {l1, l2}), A, B);
|
||||
}
|
||||
|
||||
expr mk_pprod_mk(abstract_type_context & ctx, expr const & a, expr const & b) {
|
||||
expr A = ctx.infer(a);
|
||||
expr B = ctx.infer(b);
|
||||
level l1 = get_level(ctx, A);
|
||||
level l2 = get_level(ctx, B);
|
||||
return mk_app(mk_constant(get_pprod_mk_name(), {l1, l2}), A, B, a, b);
|
||||
}
|
||||
|
||||
expr mk_pprod_fst(abstract_type_context & ctx, expr const & p) {
|
||||
expr AxB = ctx.whnf(ctx.infer(p));
|
||||
expr const & A = app_arg(app_fn(AxB));
|
||||
expr const & B = app_arg(AxB);
|
||||
return mk_app(mk_constant(get_pprod_fst_name(), const_levels(get_app_fn(AxB))), A, B, p);
|
||||
}
|
||||
|
||||
expr mk_pprod_snd(abstract_type_context & ctx, expr const & p) {
|
||||
expr AxB = ctx.whnf(ctx.infer(p));
|
||||
expr const & A = app_arg(app_fn(AxB));
|
||||
expr const & B = app_arg(AxB);
|
||||
return mk_app(mk_constant(get_pprod_snd_name(), const_levels(get_app_fn(AxB))), A, B, p);
|
||||
}
|
||||
|
||||
static expr * g_nat = nullptr;
|
||||
static expr * g_nat_zero = nullptr;
|
||||
static expr * g_nat_one = nullptr;
|
||||
|
|
@ -543,19 +480,6 @@ static void finalize_char() {
|
|||
expr mk_unit(level const & l, bool prop) { return prop ? mk_true() : mk_unit(l); }
|
||||
expr mk_unit_mk(level const & l, bool prop) { return prop ? mk_true_intro() : mk_unit_mk(l); }
|
||||
|
||||
expr mk_pprod(abstract_type_context & ctx, expr const & a, expr const & b, bool prop) {
|
||||
return prop ? mk_and(a, b) : mk_pprod(ctx, a, b);
|
||||
}
|
||||
expr mk_pprod_mk(abstract_type_context & ctx, expr const & a, expr const & b, bool prop) {
|
||||
return prop ? mk_and_intro(ctx, a, b) : mk_pprod_mk(ctx, a, b);
|
||||
}
|
||||
expr mk_pprod_fst(abstract_type_context & ctx, expr const & p, bool prop) {
|
||||
return prop ? mk_and_left(ctx, p) : mk_pprod_fst(ctx, p);
|
||||
}
|
||||
expr mk_pprod_snd(abstract_type_context & ctx, expr const & p, bool prop) {
|
||||
return prop ? mk_and_right(ctx, p) : mk_pprod_snd(ctx, p);
|
||||
}
|
||||
|
||||
bool is_ite(expr const & e) {
|
||||
return is_app_of(e, get_ite_name(), 5);
|
||||
}
|
||||
|
|
@ -593,85 +517,6 @@ expr mk_propext(expr const & lhs, expr const & rhs, expr const & iff_pr) {
|
|||
return mk_app(mk_constant(get_propext_name()), lhs, rhs, iff_pr);
|
||||
}
|
||||
|
||||
expr mk_eq(abstract_type_context & ctx, expr const & lhs, expr const & rhs) {
|
||||
expr A = ctx.whnf(ctx.infer(lhs));
|
||||
level lvl = get_level(ctx, A);
|
||||
return mk_app(mk_constant(get_eq_name(), {lvl}), A, lhs, rhs);
|
||||
}
|
||||
|
||||
expr mk_eq_refl(abstract_type_context & ctx, expr const & a) {
|
||||
expr A = ctx.whnf(ctx.infer(a));
|
||||
level lvl = get_level(ctx, A);
|
||||
return mk_app(mk_constant(get_eq_refl_name(), {lvl}), A, a);
|
||||
}
|
||||
|
||||
expr mk_eq_symm(abstract_type_context & ctx, expr const & H) {
|
||||
if (is_app_of(H, get_eq_refl_name()))
|
||||
return H;
|
||||
expr p = ctx.whnf(ctx.infer(H));
|
||||
lean_assert(is_eq(p));
|
||||
expr lhs = app_arg(app_fn(p));
|
||||
expr rhs = app_arg(p);
|
||||
expr A = ctx.infer(lhs);
|
||||
level lvl = get_level(ctx, A);
|
||||
return mk_app(mk_constant(get_eq_symm_name(), {lvl}), A, lhs, rhs, H);
|
||||
}
|
||||
|
||||
expr mk_eq_trans(abstract_type_context & ctx, expr const & H1, expr const & H2) {
|
||||
if (is_app_of(H1, get_eq_refl_name()))
|
||||
return H2;
|
||||
if (is_app_of(H2, get_eq_refl_name()))
|
||||
return H1;
|
||||
expr p1 = ctx.whnf(ctx.infer(H1));
|
||||
expr p2 = ctx.whnf(ctx.infer(H2));
|
||||
lean_assert(is_eq(p1) && is_eq(p2));
|
||||
expr lhs1 = app_arg(app_fn(p1));
|
||||
expr rhs1 = app_arg(p1);
|
||||
expr rhs2 = app_arg(p2);
|
||||
expr A = ctx.infer(lhs1);
|
||||
level lvl = get_level(ctx, A);
|
||||
return mk_app({mk_constant(get_eq_trans_name(), {lvl}), A, lhs1, rhs1, rhs2, H1, H2});
|
||||
}
|
||||
|
||||
expr mk_eq_subst(abstract_type_context & ctx, expr const & motive,
|
||||
expr const & x, expr const & y, expr const & xeqy, expr const & h) {
|
||||
expr A = ctx.infer(x);
|
||||
level l1 = get_level(ctx, A);
|
||||
expr r = mk_constant(get_eq_subst_name(), {l1});
|
||||
return mk_app({r, A, x, y, motive, xeqy, h});
|
||||
}
|
||||
|
||||
expr mk_eq_subst(abstract_type_context & ctx, expr const & motive, expr const & xeqy, expr const & h) {
|
||||
expr xeqy_type = ctx.whnf(ctx.infer(xeqy));
|
||||
return mk_eq_subst(ctx, motive, app_arg(app_fn(xeqy_type)), app_arg(xeqy_type), xeqy, h);
|
||||
}
|
||||
|
||||
expr mk_congr_arg(abstract_type_context & ctx, expr const & f, expr const & H) {
|
||||
expr eq = ctx.relaxed_whnf(ctx.infer(H));
|
||||
expr pi = ctx.relaxed_whnf(ctx.infer(f));
|
||||
expr A, B, lhs, rhs;
|
||||
lean_verify(is_eq(eq, A, lhs, rhs));
|
||||
lean_assert(is_arrow(pi));
|
||||
B = binding_body(pi);
|
||||
level lvl_1 = get_level(ctx, A);
|
||||
level lvl_2 = get_level(ctx, B);
|
||||
return ::lean::mk_app({mk_constant(get_congr_arg_name(), {lvl_1, lvl_2}), A, B, lhs, rhs, f, H});
|
||||
}
|
||||
|
||||
expr mk_subsingleton_elim(abstract_type_context & ctx, expr const & h, expr const & x, expr const & y) {
|
||||
expr A = ctx.infer(x);
|
||||
level l = get_level(ctx, A);
|
||||
expr r = mk_constant(get_subsingleton_elim_name(), {l});
|
||||
return mk_app({r, A, h, x, y});
|
||||
}
|
||||
|
||||
expr mk_heq(abstract_type_context & ctx, expr const & lhs, expr const & rhs) {
|
||||
expr A = ctx.whnf(ctx.infer(lhs));
|
||||
expr B = ctx.whnf(ctx.infer(rhs));
|
||||
level lvl = get_level(ctx, A);
|
||||
return mk_app(mk_constant(get_heq_name(), {lvl}), A, lhs, B, rhs);
|
||||
}
|
||||
|
||||
bool is_eq_ndrec_core(expr const & e) {
|
||||
expr const & fn = get_app_fn(e);
|
||||
return is_constant(fn) && const_name(fn) == get_eq_ndrec_name();
|
||||
|
|
@ -720,14 +565,6 @@ bool is_eq_a_a(expr const & e) {
|
|||
return lhs == rhs;
|
||||
}
|
||||
|
||||
bool is_eq_a_a(abstract_type_context & ctx, expr const & e) {
|
||||
if (!is_eq(e))
|
||||
return false;
|
||||
expr lhs = app_arg(app_fn(e));
|
||||
expr rhs = app_arg(e);
|
||||
return ctx.is_def_eq(lhs, rhs);
|
||||
}
|
||||
|
||||
bool is_heq(expr const & e) {
|
||||
return is_app_of(e, get_heq_name(), 4);
|
||||
}
|
||||
|
|
@ -749,15 +586,6 @@ bool is_heq(expr const & e, expr & lhs, expr & rhs) {
|
|||
return is_heq(e, A, lhs, B, rhs);
|
||||
}
|
||||
|
||||
expr mk_cast(abstract_type_context & ctx, expr const & H, expr const & e) {
|
||||
expr type = ctx.relaxed_whnf(ctx.infer(H));
|
||||
expr A, B;
|
||||
if (!is_eq(type, A, B))
|
||||
throw exception("cast failed, equality proof expected");
|
||||
level lvl = get_level(ctx, A);
|
||||
return mk_app(mk_constant(get_cast_name(), {lvl}), A, B, H, e);
|
||||
}
|
||||
|
||||
expr mk_false() {
|
||||
return mk_constant(get_false_name());
|
||||
}
|
||||
|
|
@ -774,11 +602,6 @@ bool is_empty(expr const & e) {
|
|||
return is_constant(e) && const_name(e) == get_empty_name();
|
||||
}
|
||||
|
||||
expr mk_false_rec(abstract_type_context & ctx, expr const & f, expr const & t) {
|
||||
level t_lvl = get_level(ctx, t);
|
||||
return mk_app(mk_constant(get_false_rec_name(), {t_lvl}), t, f);
|
||||
}
|
||||
|
||||
bool is_or(expr const & e) {
|
||||
return is_app_of(e, get_or_name(), 2);
|
||||
}
|
||||
|
|
@ -823,12 +646,6 @@ expr mk_not(expr const & e) {
|
|||
return mk_app(mk_constant(get_not_name()), e);
|
||||
}
|
||||
|
||||
expr mk_absurd(abstract_type_context & ctx, expr const & t, expr const & e, expr const & not_e) {
|
||||
level t_lvl = get_level(ctx, t);
|
||||
expr e_type = ctx.infer(e);
|
||||
return mk_app(mk_constant(get_absurd_name(), {t_lvl}), e_type, t, e, not_e);
|
||||
}
|
||||
|
||||
bool is_exists(expr const & e, expr & A, expr & p) {
|
||||
if (is_app_of(e, get_exists_name(), 2)) {
|
||||
A = app_arg(app_fn(e));
|
||||
|
|
|
|||
|
|
@ -8,7 +8,6 @@ Author: Leonardo de Moura
|
|||
#include <string>
|
||||
#include "kernel/environment.h"
|
||||
#include "library/expr_pair.h"
|
||||
#include "library/abstract_type_context.h"
|
||||
|
||||
namespace lean {
|
||||
/* If \c n is not in \c env, then return \c. Otherwise, find the first j >= idx s.t.
|
||||
|
|
@ -26,11 +25,6 @@ optional<expr> is_optional_param(expr const & e);
|
|||
|
||||
optional<expr_pair> is_auto_param(expr const & e);
|
||||
|
||||
/** \brief Return the universe level of the type of \c A.
|
||||
Throws an exception if the (relaxed) whnf of the type
|
||||
of A is not a sort. */
|
||||
level get_level(abstract_type_context & ctx, expr const & A);
|
||||
|
||||
/** brief Return a name that does not appear in `lp_names`. */
|
||||
name mk_fresh_lp_name(names const & lp_names);
|
||||
|
||||
|
|
@ -130,12 +124,6 @@ unsigned get_constructor_idx(environment const & env, name const & n);
|
|||
\pre inductive::is_intro_rule(env, ctor_name) */
|
||||
name get_constructor_inductive_type(environment const & env, name const & ctor_name);
|
||||
|
||||
/** \brief Given an expression \c e, return the number of arguments expected arguments.
|
||||
|
||||
\remark This function counts the number of nested Pi's in \c e. Weak-head-normal-forms are computed for the type of \c e.
|
||||
\remark The type and whnf are computed using \c tc. */
|
||||
unsigned get_expect_num_args(abstract_type_context & ctx, expr e);
|
||||
|
||||
/** \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> */
|
||||
level get_datatype_level(expr const & ind_type);
|
||||
|
|
@ -161,28 +149,15 @@ expr mk_true_intro();
|
|||
bool is_and(expr const & e, expr & arg1, expr & arg2);
|
||||
bool is_and(expr const & e);
|
||||
expr mk_and(expr const & a, expr const & b);
|
||||
expr mk_and_intro(abstract_type_context & ctx, expr const & Ha, expr const & Hb);
|
||||
expr mk_and_elim_left(abstract_type_context & ctx, expr const & H);
|
||||
expr mk_and_elim_right(abstract_type_context & ctx, expr const & H);
|
||||
|
||||
expr mk_unit(level const & l);
|
||||
expr mk_unit_mk(level const & l);
|
||||
expr mk_unit();
|
||||
expr mk_unit_mk();
|
||||
|
||||
expr mk_pprod(abstract_type_context & ctx, expr const & A, expr const & B);
|
||||
expr mk_pprod_mk(abstract_type_context & ctx, expr const & a, expr const & b);
|
||||
expr mk_pprod_fst(abstract_type_context & ctx, expr const & p);
|
||||
expr mk_pprod_snd(abstract_type_context & ctx, expr const & p);
|
||||
|
||||
expr mk_unit(level const & l, bool prop);
|
||||
expr mk_unit_mk(level const & l, bool prop);
|
||||
|
||||
expr mk_pprod(abstract_type_context & ctx, expr const & a, expr const & b, bool prop);
|
||||
expr mk_pprod_mk(abstract_type_context & ctx, expr const & a, expr const & b, bool prop);
|
||||
expr mk_pprod_fst(abstract_type_context & ctx, expr const & p, bool prop);
|
||||
expr mk_pprod_snd(abstract_type_context & ctx, expr const & p, bool prop);
|
||||
|
||||
expr mk_nat_type();
|
||||
bool is_nat_type(expr const & e);
|
||||
expr mk_nat_zero();
|
||||
|
|
@ -206,19 +181,6 @@ expr mk_iff_refl(expr const & a);
|
|||
|
||||
expr mk_propext(expr const & lhs, expr const & rhs, expr const & iff_pr);
|
||||
|
||||
expr mk_eq(abstract_type_context & ctx, expr const & lhs, expr const & rhs);
|
||||
expr mk_eq_refl(abstract_type_context & ctx, expr const & a);
|
||||
expr mk_eq_symm(abstract_type_context & ctx, expr const & H);
|
||||
expr mk_eq_trans(abstract_type_context & ctx, expr const & H1, expr const & H2);
|
||||
expr mk_eq_subst(abstract_type_context & ctx, expr const & motive,
|
||||
expr const & x, expr const & y, expr const & xeqy, expr const & h);
|
||||
expr mk_eq_subst(abstract_type_context & ctx, expr const & motive, expr const & xeqy, expr const & h);
|
||||
|
||||
expr mk_congr_arg(abstract_type_context & ctx, expr const & f, expr const & H);
|
||||
|
||||
/** \brief Create an proof for x = y using subsingleton.elim (in standard mode) */
|
||||
expr mk_subsingleton_elim(abstract_type_context & ctx, expr const & h, expr const & x, expr const & y);
|
||||
|
||||
/** \brief Return true iff \c e is a term of the form (eq.rec ....) */
|
||||
bool is_eq_rec_core(expr const & e);
|
||||
/** \brief Return true iff \c e is a term of the form (eq.rec ....) */
|
||||
|
|
@ -231,23 +193,16 @@ bool is_eq(expr const & e, expr & lhs, expr & rhs);
|
|||
bool is_eq(expr const & e, expr & A, expr & lhs, expr & rhs);
|
||||
/** \brief Return true iff \c e is of the form (eq A a a) */
|
||||
bool is_eq_a_a(expr const & e);
|
||||
/** \brief Return true iff \c e is of the form (eq A a a') where \c a and \c a' are definitionally equal */
|
||||
bool is_eq_a_a(abstract_type_context & ctx, expr const & e);
|
||||
|
||||
expr mk_heq(abstract_type_context & ctx, expr const & lhs, expr const & rhs);
|
||||
bool is_heq(expr const & e);
|
||||
bool is_heq(expr const & e, expr & lhs, expr & rhs);
|
||||
bool is_heq(expr const & e, expr & A, expr & lhs, expr & B, expr & rhs);
|
||||
|
||||
expr mk_cast(abstract_type_context & ctx, expr const & H, expr const & e);
|
||||
|
||||
expr mk_false();
|
||||
expr mk_empty();
|
||||
|
||||
bool is_false(expr const & e);
|
||||
bool is_empty(expr const & e);
|
||||
/** \brief Return an element of type t given an element \c f : false */
|
||||
expr mk_false_rec(abstract_type_context & ctx, expr const & f, expr const & t);
|
||||
|
||||
bool is_or(expr const & e);
|
||||
bool is_or(expr const & e, expr & A, expr & B);
|
||||
|
|
@ -260,9 +215,6 @@ inline bool is_not(expr const & e) { expr a; return is_not(e, a); }
|
|||
bool is_not_or_ne(expr const & e, expr & a);
|
||||
expr mk_not(expr const & e);
|
||||
|
||||
/** \brief Create the term <tt>absurd e not_e : t</tt>. */
|
||||
expr mk_absurd(abstract_type_context & ctx, expr const & t, expr const & e, expr const & not_e);
|
||||
|
||||
/** \brief Returns none if \c e is not an application with at least two arguments.
|
||||
Otherwise it returns <tt>app_fn(app_fn(e))</tt>. */
|
||||
optional<expr> get_binary_op(expr const & e);
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue