diff --git a/src/frontends/lean/frontend.cpp b/src/frontends/lean/frontend.cpp index 76fee8daf..3a3c9cc05 100644 --- a/src/frontends/lean/frontend.cpp +++ b/src/frontends/lean/frontend.cpp @@ -27,7 +27,7 @@ static std::vector g_empty_vector; /** \brief Environment extension object for the Lean default frontend. */ -struct lean_extension : public environment::extension { +struct lean_extension : public environment_extension { typedef std::pair, name> implicit_info; // Remark: only named objects are stored in the dictionary. typedef std::unordered_map operator_table; @@ -46,7 +46,7 @@ struct lean_extension : public environment::extension { expr_to_coercions m_type_coercions; // mapping type -> list (to-type, function) lean_extension const * get_parent() const { - return environment::extension::get_parent(); + return environment_extension::get_parent(); } /** \brief Return the nud operator for the given symbol. */ @@ -206,7 +206,7 @@ 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 & env, io_state & st) { + void add_op(operator_info new_op, expr const & d, bool led, environment const & env, io_state & st) { name const & opn = new_op.get_op_name(); operator_info old_op = find_op(opn, led); if (!old_op) { @@ -236,7 +236,7 @@ struct lean_extension : public environment::extension { remove_bindings(old_op); register_new_op(new_op, d, led); } - env.add_neutral_object(new notation_declaration(new_op, d)); + env->add_neutral_object(new notation_declaration(new_op, d)); } expr mk_explicit_definition_body(expr type, name const & n, unsigned i, unsigned sz) { @@ -252,16 +252,16 @@ struct lean_extension : public environment::extension { } } - void mark_implicit_arguments(name const & n, unsigned sz, bool const * implicit, environment & env) { - if (env.has_children()) + void mark_implicit_arguments(name const & n, unsigned sz, bool const * implicit, environment const & env) { + if (env->has_children()) throw exception(sstream() << "failed to mark implicit arguments, frontend object is read-only"); - object const & obj = env.get_object(n); + object const & obj = env->get_object(n); if (obj.kind() != object_kind::Definition && obj.kind() != object_kind::Postulate && obj.kind() != object_kind::Builtin) throw exception(sstream() << "failed to mark implicit arguments, the object '" << n << "' is not a definition or postulate"); if (has_implicit_arguments(n)) throw exception(sstream() << "the object '" << n << "' already has implicit argument information associated with it"); name explicit_version(n, "explicit"); - if (env.find_object(explicit_version)) + if (env->find_object(explicit_version)) throw exception(sstream() << "failed to mark implicit arguments for '" << n << "', the frontend already has an object named '" << explicit_version << "'"); expr const & type = obj.get_type(); unsigned num_args = 0; @@ -277,9 +277,9 @@ struct lean_extension : public environment::extension { m_implicit_table[n] = mk_pair(v, explicit_version); expr body = mk_explicit_definition_body(type, n, 0, num_args); if (obj.is_axiom() || obj.is_theorem()) { - env.add_theorem(explicit_version, type, body); + env->add_theorem(explicit_version, type, body); } else { - env.add_definition(explicit_version, type, body); + env->add_definition(explicit_version, type, body); } } @@ -326,9 +326,9 @@ struct lean_extension : public environment::extension { return !n.is_atomic() && get_explicit_version(n.get_prefix()) == n; } - void add_coercion(expr const & f, environment & env) { - expr type = env.infer_type(f); - expr norm_type = env.normalize(type); + void add_coercion(expr const & f, environment const & env) { + expr type = env->infer_type(f); + expr norm_type = env->normalize(type); if (!is_arrow(norm_type)) throw exception("invalid coercion declaration, a coercion must have an arrow type (i.e., a non-dependent functional type)"); expr from = abst_domain(norm_type); @@ -341,7 +341,7 @@ struct lean_extension : public environment::extension { m_coercion_set.insert(f); list l = get_coercions(from); insert(m_type_coercions, from, cons(expr_pair(to, f), l)); - env.add_neutral_object(new coercion_declaration(f)); + env->add_neutral_object(new coercion_declaration(f)); } optional get_coercion(expr const & from_type, expr const & to_type) const { @@ -378,47 +378,46 @@ struct lean_extension : public environment::extension { struct lean_extension_initializer { unsigned m_extid; lean_extension_initializer() { - m_extid = environment::register_extension([](){ return std::unique_ptr(new lean_extension()); }); + m_extid = environment_cell::register_extension([](){ return std::unique_ptr(new lean_extension()); }); } }; static lean_extension_initializer g_lean_extension_initializer; -static lean_extension const & to_ext(environment const & env) { - return env.get_extension(g_lean_extension_initializer.m_extid); +static lean_extension const & to_ext(ro_environment const & env) { + return env->get_extension(g_lean_extension_initializer.m_extid); } -static lean_extension & to_ext(environment & env) { - return env.get_extension(g_lean_extension_initializer.m_extid); +static lean_extension & to_ext(environment const & env) { + return env->get_extension(g_lean_extension_initializer.m_extid); } - -bool is_explicit(environment const & env, name const & n) { +bool is_explicit(ro_environment const & env, name const & n) { return to_ext(env).is_explicit(n); } -bool has_implicit_arguments(environment const & env, name const & n) { +bool has_implicit_arguments(ro_environment const & env, name const & n) { return to_ext(env).has_implicit_arguments(n); } -name const & get_explicit_version(environment const & env, name const & n) { +name const & get_explicit_version(ro_environment const & env, name const & n) { return to_ext(env).get_explicit_version(n); } -std::vector const & get_implicit_arguments(environment const & env, name const & n) { +std::vector const & get_implicit_arguments(ro_environment const & env, name const & n) { return to_ext(env).get_implicit_arguments(n); } -bool is_coercion(environment const & env, expr const & f) { +bool is_coercion(ro_environment const & env, expr const & f) { return to_ext(env).is_coercion(f); } -operator_info find_op_for(environment const & env, expr const & n, bool unicode) { +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)) { return r; } else { - optional obj = env.find_object(const_name(n)); + optional obj = env->find_object(const_name(n)); if (obj && obj->is_builtin() && obj->get_name() == const_name(n)) return to_ext(env).find_op_for(obj->get_value(), unicode); else diff --git a/src/frontends/lean/frontend.h b/src/frontends/lean/frontend.h index 03718e773..36d2db6b7 100644 --- a/src/frontends/lean/frontend.h +++ b/src/frontends/lean/frontend.h @@ -27,35 +27,34 @@ public: frontend(); frontend(environment const & env, io_state const & s); - 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(); } + 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(); } - environment & get_environment() { return m_env; } - operator environment &() { 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 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::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(); } + 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 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(); } /*@}*/ /** @@ -199,10 +198,10 @@ public: /*@}*/ }; -bool is_explicit(environment const & env, name const & n); -bool has_implicit_arguments(environment const & env, name const & n); -name const & get_explicit_version(environment const & env, name const & n); -std::vector const & get_implicit_arguments(environment const & env, name const & n); -bool is_coercion(environment const & env, expr const & f); -operator_info find_op_for(environment const & env, expr const & e, bool unicode); +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 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); } diff --git a/src/frontends/lean/notation.cpp b/src/frontends/lean/notation.cpp index 3041414ed..12eda36a4 100644 --- a/src/frontends/lean/notation.cpp +++ b/src/frontends/lean/notation.cpp @@ -20,7 +20,7 @@ void add_alias(frontend & f, name const & n, name const & m) { \brief Initialize builtin notation. */ void init_builtin_notation(frontend & f) { - if (!f.get_environment().mark_builtin_imported("lean_notation")) + if (!f.get_environment()->mark_builtin_imported("lean_notation")) return; f.add_infix("=", 50, mk_homo_eq_fn()); f.mark_implicit_arguments(mk_homo_eq_fn(), 1); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index b3af7ecbe..ec3f945e9 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1373,7 +1373,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, m_frontend.get_state(), s); + proof_state_seq seq = t(m_frontend.get_environment(), m_frontend.get_state(), s); r = seq.pull(); }); if (r) { @@ -1401,9 +1401,9 @@ class parser::imp { // Example: apply_tactic. metavar_env menv = s.get_menv(); buffer ucs; - expr pr_type = type_checker(m_frontend).infer_type(pr, ctx, &menv, &ucs); + expr pr_type = type_checker(m_frontend.get_environment()).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, s.get_menv(), ucs.size(), ucs.data(), m_frontend.get_options()); + elaborator elb(m_frontend.get_environment(), s.get_menv(), ucs.size(), ucs.data(), m_frontend.get_options()); metavar_env new_menv = elb.next(); pr = instantiate_metavars(pr, new_menv); if (has_metavar(pr)) @@ -1602,7 +1602,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, mvar_ctx, mvar_type); + proof_state s = to_proof_state(m_frontend.get_environment(), mvar_ctx, mvar_type); std::pair, pos_info> hint_and_pos = get_tactic_for(mvar); if (hint_and_pos.first) { // metavariable has an associated tactic hint @@ -1746,7 +1746,7 @@ class parser::imp { for (auto b : bindings) { name const & id = std::get<1>(b); if (m_frontend.find_object(id)) - throw already_declared_exception(m_frontend, id); + throw already_declared_exception(m_frontend.get_environment(), id); } for (auto b : bindings) { name const & id = std::get<1>(b); @@ -1771,7 +1771,7 @@ class parser::imp { void parse_eval() { next(); expr v = m_elaborator(parse_expr()); - normalizer norm(m_frontend); + normalizer norm(m_frontend.get_environment()); expr r = norm(v); regular(m_frontend) << r << endl; } @@ -1817,7 +1817,7 @@ class parser::imp { void parse_check() { next(); expr v = m_elaborator(parse_expr()); - expr t = infer_type(v, m_frontend); + 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(); unsigned indent = get_pp_indent(opts); @@ -2001,7 +2001,7 @@ 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())) { + if (!m_frontend.get_environment()->mark_imported(fname.c_str())) { diagnostic(m_frontend) << "Module '" << fname << "' has already been imported" << endl; return; } @@ -2149,7 +2149,7 @@ public: m_frontend(fe), m_scanner(in), m_elaborator(fe), - m_type_inferer(fe), + m_type_inferer(fe.get_environment()), m_use_exceptions(use_exceptions), m_interactive(interactive) { m_script_state = S; diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 4463b9108..8bd277e7f 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -153,7 +153,7 @@ class pp_fn { typedef scoped_map aliases; typedef std::vector> aliases_defs; typedef scoped_set local_names; - environment m_env; + ro_environment m_env; // State aliases m_aliases; aliases_defs m_aliases_defs; @@ -171,8 +171,6 @@ class pp_fn { bool m_extra_lets; //!< introduce extra let-expression to cope with sharing. unsigned m_alias_min_weight; //!< minimal weight for creating an alias - environment const & env() const { return m_env; } - // Create a scope for local definitions struct mk_scope { pp_fn & m_fn; @@ -192,7 +190,7 @@ class pp_fn { typedef std::pair result; bool is_coercion(expr const & e) { - return is_app(e) && num_args(e) == 2 && ::lean::is_coercion(env(), arg(e, 0)); + return is_app(e) && num_args(e) == 2 && ::lean::is_coercion(m_env, arg(e, 0)); } /** @@ -233,7 +231,7 @@ class pp_fn { } bool has_implicit_arguments(name const & n) const { - return ::lean::has_implicit_arguments(env(), n) && m_local_names.find(n) == m_local_names.end(); + return ::lean::has_implicit_arguments(m_env, n) && m_local_names.find(n) == m_local_names.end(); } result pp_constant(expr const & e) { @@ -241,7 +239,7 @@ class pp_fn { if (is_placeholder(e)) { return mk_result(format("_"), 1); } else if (has_implicit_arguments(n)) { - return mk_result(format(get_explicit_version(env(), n)), 1); + return mk_result(format(get_explicit_version(m_env, n)), 1); } else { return mk_result(format(n), 1); } @@ -250,7 +248,7 @@ class pp_fn { result pp_value(expr const & e) { value const & v = to_value(e); if (has_implicit_arguments(v.get_name())) { - return mk_result(format(get_explicit_version(env(), v.get_name())), 1); + return mk_result(format(get_explicit_version(m_env, v.get_name())), 1); } else { return mk_result(v.pp(m_unicode, m_coercion), 1); } @@ -399,7 +397,7 @@ class pp_fn { if (is_constant(e) && m_local_names.find(const_name(e)) != m_local_names.end()) return operator_info(); else - return ::lean::find_op_for(env(), e, m_unicode); + return ::lean::find_op_for(m_env, e, m_unicode); } /** @@ -522,7 +520,7 @@ class pp_fn { } application(expr const & e, pp_fn const & owner, bool show_implicit):m_app(e) { - environment const & env = owner.env(); + ro_environment const & env = owner.m_env; expr const & f = arg(e, 0); if (has_implicit_arguments(owner, f)) { name const & n = is_constant(f) ? const_name(f) : to_value(f).get_name(); @@ -1159,7 +1157,7 @@ class pp_fn { } public: - pp_fn(environment const & env, options const & opts): + pp_fn(ro_environment const & env, options const & opts): m_env(env) { set_options(opts); m_num_steps = 0; @@ -1186,17 +1184,15 @@ public: }; class pp_formatter_cell : public formatter_cell { - environment m_env; - - environment const & env() const { return m_env; } + ro_environment m_env; format pp(expr const & e, options const & opts) { - pp_fn fn(env(), opts); + pp_fn fn(m_env, opts); return fn(e); } format pp(context const & c, expr const & e, bool include_e, options const & opts) { - pp_fn fn(env(), opts); + pp_fn fn(m_env, opts); unsigned indent = get_pp_indent(opts); format r; bool first = true; @@ -1253,9 +1249,9 @@ class pp_formatter_cell : public formatter_cell { } else { lean_assert(is_lambda(v)); std::vector const * implicit_args = nullptr; - if (has_implicit_arguments(env(), n)) - implicit_args = &(get_implicit_arguments(env(), n)); - pp_fn fn(env(), opts); + if (has_implicit_arguments(m_env, n)) + implicit_args = &(get_implicit_arguments(m_env, n)); + pp_fn fn(m_env, opts); format def = fn.pp_definition(v, t, implicit_args); return format{highlight_command(format(kwd)), space(), format(n), def}; } @@ -1270,9 +1266,9 @@ class pp_formatter_cell : public formatter_cell { char const * kwd = obj.keyword(); name const & n = obj.get_name(); format r = format{highlight_command(format(kwd)), space(), format(n)}; - if (has_implicit_arguments(env(), n)) { - pp_fn fn(env(), opts); - r += fn.pp_pi_with_implicit_args(obj.get_type(), get_implicit_arguments(env(), n)); + if (has_implicit_arguments(m_env, n)) { + pp_fn fn(m_env, opts); + r += fn.pp_pi_with_implicit_args(obj.get_type(), get_implicit_arguments(m_env, n)); } else { r += format{space(), colon(), space(), pp(obj.get_type(), opts)}; } @@ -1286,7 +1282,7 @@ class pp_formatter_cell : public formatter_cell { } format pp_definition(object const & obj, options const & opts) { - if (is_explicit(env(), obj.get_name())) { + if (is_explicit(m_env, obj.get_name())) { // Hide implicit arguments when pretty printing the // explicit version on an object. // We do that because otherwise it looks like a recursive definition. @@ -1312,7 +1308,7 @@ class pp_formatter_cell : public formatter_cell { } public: - pp_formatter_cell(environment const & env): + pp_formatter_cell(ro_environment const & env): m_env(env) { } @@ -1363,11 +1359,11 @@ public: lean_unreachable(); // LCOV_EXCL_LINE } - virtual format operator()(environment const & env, options const & opts) { + virtual format operator()(ro_environment const & env, options const & opts) { format r; bool first = true; - std::for_each(env.begin_objects(), - env.end_objects(), + std::for_each(env->begin_objects(), + env->end_objects(), [&](object const & obj) { check_interrupted(); if (first) first = false; else r += line(); @@ -1376,16 +1372,16 @@ public: return r; } - virtual optional get_environment() const { return optional(env()); } + virtual optional get_environment() const { return optional(m_env); } }; -formatter mk_pp_formatter(environment const & env) { +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); + formatter fmt = mk_pp_formatter(fe.get_environment()); bool first = true; std::for_each(fe.begin_objects(), fe.end_objects(), diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h index da683840c..8f652e1da 100644 --- a/src/frontends/lean/pp.h +++ b/src/frontends/lean/pp.h @@ -12,6 +12,6 @@ Author: Leonardo de Moura namespace lean { class frontend; class environment; -formatter mk_pp_formatter(environment const & env); +formatter mk_pp_formatter(ro_environment const & env); std::ostream & operator<<(std::ostream & out, frontend const & fe); } diff --git a/src/frontends/lean/register_module.cpp b/src/frontends/lean/register_module.cpp index 137e5d694..12222e742 100644 --- a/src/frontends/lean/register_module.cpp +++ b/src/frontends/lean/register_module.cpp @@ -16,7 +16,7 @@ Author: Leonardo de Moura namespace lean { /** \see parse_lean_expr */ -static int parse_lean_expr_core(lua_State * L, ro_shared_environment const & env, io_state & st) { +static int parse_lean_expr_core(lua_State * L, rw_shared_environment const & env, io_state & st) { char const * src = luaL_checkstring(L, 1); std::istringstream in(src); script_state S = to_script_state(L); @@ -28,7 +28,7 @@ static int parse_lean_expr_core(lua_State * L, ro_shared_environment const & env } /** \see parse_lean_expr */ -static int parse_lean_expr_core(lua_State * L, ro_shared_environment const & env) { +static int parse_lean_expr_core(lua_State * L, rw_shared_environment const & env) { io_state * io = get_io_state(L); if (io == nullptr) { io_state s(get_global_options(L), mk_pp_formatter(env)); @@ -59,10 +59,10 @@ static int parse_lean_expr(lua_State * L) { */ int nargs = get_nonnil_top(L); if (nargs == 1) { - ro_shared_environment env(L); // get global environment + rw_shared_environment env(L); // get global environment return parse_lean_expr_core(L, env); } else { - ro_shared_environment env(L, 2); + rw_shared_environment env(L, 2); if (nargs == 2) { return parse_lean_expr_core(L, env); } else { @@ -75,7 +75,7 @@ static int parse_lean_expr(lua_State * L) { } /** \see parse_lean_cmds */ -static void parse_lean_cmds_core(lua_State * L, rw_shared_environment & env, io_state & st) { +static void parse_lean_cmds_core(lua_State * L, rw_shared_environment const & env, io_state & st) { char const * src = luaL_checkstring(L, 1); std::istringstream in(src); script_state S = to_script_state(L); @@ -85,7 +85,7 @@ static void parse_lean_cmds_core(lua_State * L, rw_shared_environment & env, io_ } /** \see parse_lean_cmds */ -static void parse_lean_cmds_core(lua_State * L, rw_shared_environment & env) { +static void parse_lean_cmds_core(lua_State * L, rw_shared_environment const & env) { io_state * io = get_io_state(L); if (io == nullptr) { io_state s(get_global_options(L), mk_pp_formatter(env)); diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp index b2da2e1a4..3a33ecbce 100644 --- a/src/kernel/builtin.cpp +++ b/src/kernel/builtin.cpp @@ -204,11 +204,11 @@ MK_CONSTANT(eta_fn, name("Eta")); MK_CONSTANT(imp_antisym_fn, name("ImpAntisym")); MK_CONSTANT(abst_fn, name("Abst")); -void import_basic(environment & env) { - if (!env.mark_builtin_imported("basic")) +void import_basic(environment const & env) { + if (!env->mark_builtin_imported("basic")) return; - env.add_uvar(uvar_name(m_lvl), level() + LEAN_DEFAULT_LEVEL_SEPARATION); - env.add_uvar(uvar_name(u_lvl), m_lvl + LEAN_DEFAULT_LEVEL_SEPARATION); + env->add_uvar(uvar_name(m_lvl), level() + LEAN_DEFAULT_LEVEL_SEPARATION); + env->add_uvar(uvar_name(u_lvl), m_lvl + LEAN_DEFAULT_LEVEL_SEPARATION); expr p1 = Bool >> Bool; expr p2 = Bool >> p1; @@ -231,59 +231,59 @@ void import_basic(environment & env) { expr H1 = Const("H1"); expr H2 = Const("H2"); - env.add_builtin(mk_bool_type()); - env.add_builtin(mk_bool_value(true)); - env.add_builtin(mk_bool_value(false)); - env.add_builtin(mk_if_fn()); + env->add_builtin(mk_bool_type()); + env->add_builtin(mk_bool_value(true)); + env->add_builtin(mk_bool_value(false)); + env->add_builtin(mk_if_fn()); // implies(x, y) := if x y True - env.add_definition(implies_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, bIf(x, y, True))); + env->add_definition(implies_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, bIf(x, y, True))); // iff(x, y) := x = y - env.add_definition(iff_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Eq(x, y))); + env->add_definition(iff_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Eq(x, y))); // not(x) := if x False True - env.add_definition(not_fn_name, p1, Fun({x, Bool}, bIf(x, False, True))); + env->add_definition(not_fn_name, p1, Fun({x, Bool}, bIf(x, False, True))); // or(x, y) := Not(x) => y - env.add_definition(or_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Implies(Not(x), y))); + env->add_definition(or_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Implies(Not(x), y))); // and(x, y) := Not(x => Not(y)) - env.add_definition(and_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Not(Implies(x, Not(y))))); + env->add_definition(and_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Not(Implies(x, Not(y))))); // forall : Pi (A : Type u), (A -> Bool) -> Bool - env.add_definition(forall_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Eq(P, Fun({x, A}, True)))); + env->add_definition(forall_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Eq(P, Fun({x, A}, True)))); // TODO(Leo): introduce epsilon - env.add_definition(exists_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Not(Forall(A, Fun({x, A}, Not(P(x))))))); + env->add_definition(exists_fn_name, q_type, Fun({{A, TypeU}, {P, A_pred}}, Not(Forall(A, Fun({x, A}, Not(P(x))))))); // homogeneous equality - env.add_definition(homo_eq_fn_name, Pi({{A, TypeU}, {x, A}, {y, A}}, Bool), Fun({{A, TypeU}, {x, A}, {y, A}}, Eq(x, y))); + env->add_definition(homo_eq_fn_name, Pi({{A, TypeU}, {x, A}, {y, A}}, Bool), Fun({{A, TypeU}, {x, A}, {y, A}}, Eq(x, y))); // MP : Pi (a b : Bool) (H1 : a => b) (H2 : a), b - env.add_axiom(mp_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, a}}, b)); + env->add_axiom(mp_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, a}}, b)); // Discharge : Pi (a b : Bool) (H : a -> b), a => b - env.add_axiom(discharge_fn_name, Pi({{a, Bool}, {b, Bool}, {H, a >> b}}, Implies(a, b))); + env->add_axiom(discharge_fn_name, Pi({{a, Bool}, {b, Bool}, {H, a >> b}}, Implies(a, b))); // Case : Pi (P : Bool -> Bool) (H1 : P True) (H2 : P False) (a : Bool), P a - env.add_axiom(case_fn_name, Pi({{P, Bool >> Bool}, {H1, P(True)}, {H2, P(False)}, {a, Bool}}, P(a))); + env->add_axiom(case_fn_name, Pi({{P, Bool >> Bool}, {H1, P(True)}, {H2, P(False)}, {a, Bool}}, P(a))); // Refl : Pi (A : Type u) (a : A), a = a - env.add_axiom(refl_fn_name, Pi({{A, TypeU}, {a, A}}, Eq(a, a))); + env->add_axiom(refl_fn_name, Pi({{A, TypeU}, {a, A}}, Eq(a, a))); // TransExt : Pi (A B C: Type u) (a : A) (b : B) (c : C) (H1 : a = b) (H2 : b = c), a = c - env.add_axiom(trans_ext_fn_name, Pi({{A, TypeU}, {B, TypeU}, {C, TypeU}, {a, A}, {b, B}, {c, C}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c))); + env->add_axiom(trans_ext_fn_name, Pi({{A, TypeU}, {B, TypeU}, {C, TypeU}, {a, A}, {b, B}, {c, C}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c))); // Subst : Pi (A : Type u) (a b : A) (P : A -> bool) (H1 : P a) (H2 : a = b), P b - env.add_axiom(subst_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {P, A_pred}, {H1, P(a)}, {H2, Eq(a, b)}}, P(b))); + env->add_axiom(subst_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {P, A_pred}, {H1, P(a)}, {H2, Eq(a, b)}}, P(b))); // Eta : Pi (A : Type u) (B : A -> Type u), f : (Pi x : A, B x), (Fun x : A => f x) = f - env.add_axiom(eta_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}}, Eq(Fun({x, A}, f(x)), f))); + env->add_axiom(eta_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}}, Eq(Fun({x, A}, f(x)), f))); // ImpliesAntisym : Pi (a b : Bool) (H1 : a => b) (H2 : b => a), a = b - env.add_axiom(imp_antisym_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, Implies(b, a)}}, Eq(a, b))); + env->add_axiom(imp_antisym_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, Implies(b, a)}}, Eq(a, b))); // Abst : Pi (A : Type u) (B : A -> Type u), f g : (Pi x : A, B x), H : (Pi x : A, (f x) = (g x)), f = g - env.add_axiom(abst_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {H, Pi(x, A, Eq(f(x), g(x)))}}, Eq(f, g))); + env->add_axiom(abst_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {H, Pi(x, A, Eq(f(x), g(x)))}}, Eq(f, g))); } } diff --git a/src/kernel/builtin.h b/src/kernel/builtin.h index 52898d232..61e283a62 100644 --- a/src/kernel/builtin.h +++ b/src/kernel/builtin.h @@ -188,7 +188,7 @@ inline expr Abst(expr const & A, expr const & B, expr const & f, expr const & g, class environment; /** \brief Initialize the environment with basic builtin declarations and axioms */ -void import_basic(environment & env); +void import_basic(environment const & env); /** \brief Helper macro for defining constants such as bool_type, int_type, int_add, etc. diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 21a0d7a2d..9cdf1f888 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -24,17 +24,17 @@ Author: Leonardo de Moura namespace lean { static name g_builtin_module("builtin_module"); class extension_factory { - std::vector m_makers; - mutex m_makers_mutex; + std::vector m_makers; + mutex m_makers_mutex; public: - unsigned register_extension(environment::mk_extension mk) { + unsigned register_extension(environment_cell::mk_extension mk) { lock_guard lock(m_makers_mutex); unsigned r = m_makers.size(); m_makers.push_back(mk); return r; } - std::unique_ptr mk(unsigned extid) { + std::unique_ptr mk(unsigned extid) { lock_guard lock(m_makers_mutex); return m_makers[extid](); } @@ -47,578 +47,452 @@ static extension_factory & get_extension_factory() { return *g_extension_factory; } -unsigned environment::register_extension(mk_extension mk) { +unsigned environment_cell::register_extension(mk_extension mk) { return get_extension_factory().register_extension(mk); } -/** \brief Implementation of the Lean environment. */ -struct environment::imp { - // Remark: only named objects are stored in the dictionary. - typedef std::unordered_map object_dictionary; - typedef std::tuple constraint; - std::weak_ptr m_this; - // Universe variable management - std::vector m_constraints; - std::vector m_uvars; - // Children environment management - atomic m_num_children; - std::shared_ptr m_parent; - // Object management - std::vector m_objects; - object_dictionary m_object_dictionary; - std::unique_ptr m_type_checker; - std::set m_imported_modules; // set of imported files and builtin modules +environment environment_cell::env() const { + lean_assert(!m_this.expired()); // it is not possible to expire since it is a reference to this object + lean_assert(this == m_this.lock().get()); + return environment(m_this.lock()); +} - std::vector> m_extensions; - friend class extension; +environment environment_cell::parent() const { + lean_assert(has_parent()); + return environment(m_parent); +} - // This mutex is only used to implement threadsafe environment objects - // in the external APIs - shared_mutex m_mutex; +environment environment_cell::mk_child() const { + return environment(m_this.lock(), true); +} - environment env() const { - lean_assert(!m_this.expired()); // it is not possible to expire since it is a reference to this object - lean_assert(this == m_this.lock().get()); - return environment(m_this); +environment_extension & environment_cell::get_extension_core(unsigned extid) { + if (extid >= m_extensions.size()) + m_extensions.resize(extid+1); + if (!m_extensions[extid]) { + std::unique_ptr ext = get_extension_factory().mk(extid); + ext->m_extid = extid; + ext->m_env = this; + m_extensions[extid].swap(ext); } + return *(m_extensions[extid].get()); +} - extension & get_extension_core(unsigned extid) { - if (extid >= m_extensions.size()) - m_extensions.resize(extid+1); - if (!m_extensions[extid]) { - std::unique_ptr ext = get_extension_factory().mk(extid); - ext->m_extid = extid; - ext->m_env = this; - m_extensions[extid].swap(ext); +environment_extension const & environment_cell::get_extension_core(unsigned extid) const { + return const_cast(this)->get_extension_core(extid); +} + +unsigned environment_cell::get_max_weight(expr const & e) { + unsigned w = 0; + auto proc = [&](expr const & c, unsigned) { + if (is_constant(c)) { + optional obj = get_object_core(const_name(c)); + if (obj) + w = std::max(w, obj->get_weight()); } - return *(m_extensions[extid].get()); - } - - unsigned get_max_weight(expr const & e) { - unsigned w = 0; - auto proc = [&](expr const & c, unsigned) { - if (is_constant(c)) { - optional obj = get_object_core(const_name(c)); - if (obj) - w = std::max(w, obj->get_weight()); - } - return true; + return true; }; - for_each_fn visitor(proc); - visitor(e); - return w; - } + for_each_fn visitor(proc); + visitor(e); + return w; +} - /** - \brief Return true iff this environment has children. +/** \brief Throw exception if environment or its ancestors already have an object with the given name. */ +void environment_cell::check_name_core(name const & n) { + if (has_parent()) + m_parent->check_name_core(n); + if (m_object_dictionary.find(n) != m_object_dictionary.end()) + throw already_declared_exception(env(), n); +} - \remark If an environment has children than it cannot be - updated. That is, it is read-only. - */ - bool has_children() const { return m_num_children > 0; } - void inc_children() { m_num_children++; } - void dec_children() { m_num_children--; } +void environment_cell::check_name(name const & n) { + if (has_children()) + throw read_only_environment_exception(env()); + check_name_core(n); +} - /** \brief Return true iff this environment has a parent environment */ - bool has_parent() const { return m_parent != nullptr; } +/** \brief Store new named object inside internal data-structures */ +void environment_cell::register_named_object(object const & new_obj) { + m_objects.push_back(new_obj); + m_object_dictionary.insert(std::make_pair(new_obj.get_name(), new_obj)); +} - /** \brief Throw exception if environment or its ancestors already have an object with the given name. */ - void check_name_core(name const & n) { +/** + \brief Return the object named \c n in the environment or its + ancestors. Return null object if there is no object with the + given name. +*/ +optional environment_cell::get_object_core(name const & n) const { + auto it = m_object_dictionary.find(n); + if (it == m_object_dictionary.end()) { if (has_parent()) - m_parent->check_name_core(n); - if (m_object_dictionary.find(n) != m_object_dictionary.end()) - throw already_declared_exception(env(), n); - } - - void check_name(name const & n) { - if (has_children()) - throw read_only_environment_exception(env()); - check_name_core(n); - } - - /** \brief Store new named object inside internal data-structures */ - void register_named_object(object const & new_obj) { - m_objects.push_back(new_obj); - m_object_dictionary.insert(std::make_pair(new_obj.get_name(), new_obj)); - } - - /** - \brief Return the object named \c n in the environment or its - ancestors. Return null object if there is no object with the - given name. - */ - optional get_object_core(name const & n) const { - auto it = m_object_dictionary.find(n); - if (it == m_object_dictionary.end()) { - if (has_parent()) - return m_parent->get_object_core(n); - else - return none_object(); - } else { - return some_object(it->second); - } - } - - object get_object(name const & n) const { - optional obj = get_object_core(n); - if (obj) { - return *obj; - } else { - throw unknown_object_exception(env(), n); - } - } - - /** - \brief Return true if u >= v + k is implied by constraints - \pre is_uvar(u) && is_uvar(v) - */ - bool is_implied(level const & u, level const & v, int k) { - lean_assert(is_uvar(u) && is_uvar(v)); - if (u == v) - return k <= 0; + return m_parent->get_object_core(n); else - return std::any_of(m_constraints.begin(), m_constraints.end(), - [&](constraint const & c) { return std::get<0>(c) == u && std::get<1>(c) == v && std::get<2>(c) >= k; }); + return none_object(); + } else { + return some_object(it->second); } +} - /** \brief Return true iff l1 >= l2 + k by asserted universe constraints. */ - bool is_ge(level const & l1, level const & l2, int k) { - if (l1 == l2) - return k <= 0; - switch (kind(l2)) { - case level_kind::UVar: - switch (kind(l1)) { - case level_kind::UVar: return is_implied(l1, l2, k); - case level_kind::Lift: return is_ge(lift_of(l1), l2, safe_sub(k, lift_offset(l1))); - case level_kind::Max: return std::any_of(max_begin_levels(l1), max_end_levels(l1), [&](level const & l) { return is_ge(l, l2, k); }); - } - case level_kind::Lift: return is_ge(l1, lift_of(l2), safe_add(k, lift_offset(l2))); - case level_kind::Max: return std::all_of(max_begin_levels(l2), max_end_levels(l2), [&](level const & l) { return is_ge(l1, l, k); }); +object environment_cell::get_object(name const & n) const { + optional obj = get_object_core(n); + if (obj) { + return *obj; + } else { + throw unknown_object_exception(env(), n); + } +} + +/** + \brief Return true if u >= v + k is implied by constraints + \pre is_uvar(u) && is_uvar(v) +*/ +bool environment_cell::is_implied(level const & u, level const & v, int k) const { + lean_assert(is_uvar(u) && is_uvar(v)); + if (u == v) + return k <= 0; + else + return std::any_of(m_constraints.begin(), m_constraints.end(), + [&](constraint const & c) { return std::get<0>(c) == u && std::get<1>(c) == v && std::get<2>(c) >= k; }); +} + +/** \brief Return true iff l1 >= l2 + k by asserted universe constraints. */ +bool environment_cell::is_ge(level const & l1, level const & l2, int k) const { + if (l1 == l2) + return k <= 0; + switch (kind(l2)) { + case level_kind::UVar: + switch (kind(l1)) { + case level_kind::UVar: return is_implied(l1, l2, k); + case level_kind::Lift: return is_ge(lift_of(l1), l2, safe_sub(k, lift_offset(l1))); + case level_kind::Max: return std::any_of(max_begin_levels(l1), max_end_levels(l1), [&](level const & l) { return is_ge(l, l2, k); }); } - lean_unreachable(); // LCOV_EXCL_LINE + case level_kind::Lift: return is_ge(l1, lift_of(l2), safe_add(k, lift_offset(l2))); + case level_kind::Max: return std::all_of(max_begin_levels(l2), max_end_levels(l2), [&](level const & l) { return is_ge(l1, l, k); }); } + lean_unreachable(); // LCOV_EXCL_LINE +} - /** \brief Return true iff l1 >= l2 is implied by asserted universe constraints. */ - bool is_ge(level const & l1, level const & l2) { - if (has_parent()) - return m_parent->is_ge(l1, l2); +/** \brief Return true iff l1 >= l2 is implied by asserted universe constraints. */ +bool environment_cell::is_ge(level const & l1, level const & l2) const { + if (has_parent()) + return m_parent->is_ge(l1, l2); + else + return is_ge(l1, l2, 0); +} + +/** \brief Add a new universe variable */ +level environment_cell::add_uvar_core(name const & n) { + check_name(n); + level r(n); + m_uvars.push_back(r); + return r; +} + +/** + \brief Add basic constraint u >= v + d, and all basic + constraints implied by transitivity. + + \pre is_uvar(u) && is_uvar(v) +*/ +void environment_cell::add_constraint(level const & u, level const & v, int d) { + lean_assert(is_uvar(u) && is_uvar(v)); + if (is_implied(u, v, d)) + return; // redundant + buffer to_add; + for (constraint const & c : m_constraints) { + if (std::get<0>(c) == v) { + level const & l3 = std::get<1>(c); + int u_l3_d = safe_add(d, std::get<2>(c)); + if (!is_implied(u, l3, u_l3_d)) + to_add.emplace_back(u, l3, u_l3_d); + } + } + m_constraints.emplace_back(u, v, d); + for (constraint const & c : to_add) { + m_constraints.push_back(c); + } +} + +/** + \brief Add all basic constraints implied by n >= l + k + + A basic constraint is a constraint of the form u >= v + k + where u and v are universe variables. +*/ +void environment_cell::add_constraints(level const & n, level const & l, int k) { + lean_assert(is_uvar(n)); + switch (kind(l)) { + case level_kind::UVar: add_constraint(n, l, k); return; + case level_kind::Lift: add_constraints(n, lift_of(l), safe_add(k, lift_offset(l))); return; + case level_kind::Max: std::for_each(max_begin_levels(l), max_end_levels(l), [&](level const & l1) { add_constraints(n, l1, k); }); return; + } + lean_unreachable(); // LCOV_EXCL_LINE +} + +/** \brief Add a new universe variable with constraint n >= l */ +level environment_cell::add_uvar(name const & n, level const & l) { + if (has_parent()) + throw kernel_exception(env(), "invalid universe declaration, universe variables can only be declared in top-level environments"); + if (has_children()) + throw read_only_environment_exception(env()); + level r = add_uvar_core(n); + add_constraints(r, l, 0); + register_named_object(mk_uvar_decl(n, l)); + return r; +} + +/** + \brief Return the universe variable with given name. Throw an + exception if the environment and its ancestors do not + contain a universe variable named \c n. +*/ +level environment_cell::get_uvar(name const & n) const { + if (has_parent()) { + return m_parent->get_uvar(n); + } else { + auto it = std::find_if(m_uvars.begin(), m_uvars.end(), [&](level const & l) { return uvar_name(l) == n; }); + if (it == m_uvars.end()) + throw unknown_universe_variable_exception(env(), n); else - return is_ge(l1, l2, 0); + return *it; } +} - /** \brief Add a new universe variable */ - level add_uvar(name const & n) { - check_name(n); - level r(n); - m_uvars.push_back(r); - return r; +/** + \brief Initialize the set of universe variables with bottom +*/ +void environment_cell::init_uvars() { + m_uvars.emplace_back(); +} + +/** + The kernel should *not* accept expressions containing cached types. + Reason: Cached types may introduce unsoundness. + For example, in the environment env, the constant x may have type T. + Now suppose we are trying to add a new definition D that contains x, + and x is associated with a cached type T'. The cached type may allow + us to accept a definition that is type incorrect with respect to env. +*/ +void environment_cell::check_no_cached_type(expr const & e) { + if (find(e, [](expr const & a) { return is_constant(a) && const_type(a); })) + throw kernel_exception(env(), "expression has a constant with a cached type, this is a bug in one of Lean tactics and/or solvers"); +} + +/** + \brief Throw an exception if \c t is not a type or type of \c + v is not convertible to \c t. +*/ +void environment_cell::check_type(name const & n, expr const & t, expr const & v) { + m_type_checker->check_type(t); + expr v_t = m_type_checker->infer_type(v); + if (!m_type_checker->is_convertible(v_t, t)) + throw def_type_mismatch_exception(env(), n, t, v, v_t); +} + +/** \brief Throw exception if it is not a valid new definition */ +void environment_cell::check_new_definition(name const & n, expr const & t, expr const & v) { + check_name(n); + check_type(n, t, v); +} + +/** \brief Add a new builtin value to this environment */ +void environment_cell::add_builtin(expr const & v) { + if (!is_value(v)) + throw invalid_builtin_value_declaration(env(), v); + name const & n = to_value(v).get_name(); + check_name(n); + name const & u = to_value(v).get_unicode_name(); + check_name(u); + register_named_object(mk_builtin(v)); + if (u != n) { + add_definition(u, to_value(v).get_type(), mk_constant(n), false); } +} - /** - \brief Add basic constraint u >= v + d, and all basic - constraints implied by transitivity. +/** \brief Add a new builtin value set to this environment */ +void environment_cell::add_builtin_set(expr const & r) { + if (!is_value(r)) + throw invalid_builtin_value_declaration(env(), r); + check_name(to_value(r).get_name()); + register_named_object(mk_builtin_set(r)); +} - \pre is_uvar(u) && is_uvar(v) - */ - void add_constraint(level const & u, level const & v, int d) { - lean_assert(is_uvar(u) && is_uvar(v)); - if (is_implied(u, v, d)) - return; // redundant - buffer to_add; - for (constraint const & c : m_constraints) { - if (std::get<0>(c) == v) { - level const & l3 = std::get<1>(c); - int u_l3_d = safe_add(d, std::get<2>(c)); - if (!is_implied(u, l3, u_l3_d)) - to_add.emplace_back(u, l3, u_l3_d); - } - } - m_constraints.emplace_back(u, v, d); - for (constraint const & c : to_add) { - m_constraints.push_back(c); - } +/** \brief Add new definition. */ +void environment_cell::add_definition(name const & n, expr const & t, expr const & v, bool opaque) { + check_no_cached_type(t); + check_no_cached_type(v); + check_new_definition(n, t, v); + unsigned w = get_max_weight(v) + 1; + register_named_object(mk_definition(n, t, v, opaque, w)); +} + +/** + \brief Add new definition. + The type of the new definition is the type of \c v. +*/ +void environment_cell::add_definition(name const & n, expr const & v, bool opaque) { + check_no_cached_type(v); + check_name(n); + expr v_t = m_type_checker->infer_type(v); + unsigned w = get_max_weight(v) + 1; + register_named_object(mk_definition(n, v_t, v, opaque, w)); +} + +/** \brief Add new theorem. */ +void environment_cell::add_theorem(name const & n, expr const & t, expr const & v) { + check_no_cached_type(t); + check_no_cached_type(v); + check_new_definition(n, t, v); + register_named_object(mk_theorem(n, t, v)); +} + +/** \brief Add new axiom. */ +void environment_cell::add_axiom(name const & n, expr const & t) { + check_no_cached_type(t); + check_name(n); + m_type_checker->check_type(t); + register_named_object(mk_axiom(n, t)); +} + +/** \brief Add new variable. */ +void environment_cell::add_var(name const & n, expr const & t) { + check_no_cached_type(t); + check_name(n); + m_type_checker->check_type(t); + register_named_object(mk_var_decl(n, t)); +} + +void environment_cell::add_neutral_object(neutral_object_cell * o) { + m_objects.push_back(mk_neutral(o)); +} + +unsigned environment_cell::get_num_objects(bool local) const { + if (local || !has_parent()) { + return m_objects.size(); + } else { + return m_objects.size() + m_parent->get_num_objects(false); } +} - /** - \brief Add all basic constraints implied by n >= l + k - - A basic constraint is a constraint of the form u >= v + k - where u and v are universe variables. - */ - void add_constraints(level const & n, level const & l, int k) { - lean_assert(is_uvar(n)); - switch (kind(l)) { - case level_kind::UVar: add_constraint(n, l, k); return; - case level_kind::Lift: add_constraints(n, lift_of(l), safe_add(k, lift_offset(l))); return; - case level_kind::Max: std::for_each(max_begin_levels(l), max_end_levels(l), [&](level const & l1) { add_constraints(n, l1, k); }); return; - } - lean_unreachable(); // LCOV_EXCL_LINE - } - - /** \brief Add a new universe variable with constraint n >= l */ - level add_uvar(name const & n, level const & l) { - if (has_parent()) - throw kernel_exception(env(), "invalid universe declaration, universe variables can only be declared in top-level environments"); - if (has_children()) - throw read_only_environment_exception(env()); - level r = add_uvar(n); - add_constraints(r, l, 0); - register_named_object(mk_uvar_decl(n, l)); - return r; - } - - /** - \brief Return the universe variable with given name. Throw an - exception if the environment and its ancestors do not - contain a universe variable named \c n. - */ - level get_uvar(name const & n) const { - if (has_parent()) { - return m_parent->get_uvar(n); - } else { - auto it = std::find_if(m_uvars.begin(), m_uvars.end(), [&](level const & l) { return uvar_name(l) == n; }); - if (it == m_uvars.end()) - throw unknown_universe_variable_exception(env(), n); - else - return *it; - } - } - - /** - \brief Initialize the set of universe variables with bottom - */ - void init_uvars() { - m_uvars.emplace_back(); - } - - /** - The kernel should *not* accept expressions containing cached types. - Reason: Cached types may introduce unsoundness. - For example, in the environment env, the constant x may have type T. - Now suppose we are trying to add a new definition D that contains x, - and x is associated with a cached type T'. The cached type may allow - us to accept a definition that is type incorrect with respect to env. - */ - void check_no_cached_type(expr const & e) { - if (find(e, [](expr const & a) { return is_constant(a) && const_type(a); })) - throw kernel_exception(env(), "expression has a constant with a cached type, this is a bug in one of Lean tactics and/or solvers"); - } - - /** - \brief Throw an exception if \c t is not a type or type of \c - v is not convertible to \c t. - */ - void check_type(name const & n, expr const & t, expr const & v) { - m_type_checker->check_type(t); - expr v_t = m_type_checker->infer_type(v); - if (!m_type_checker->is_convertible(v_t, t)) - throw def_type_mismatch_exception(env(), n, t, v, v_t); - } - - /** \brief Throw exception if it is not a valid new definition */ - void check_new_definition(name const & n, expr const & t, expr const & v) { - check_name(n); - check_type(n, t, v); - } - - /** \brief Add a new builtin value to this environment */ - void add_builtin(expr const & v) { - if (!is_value(v)) - throw invalid_builtin_value_declaration(env(), v); - name const & n = to_value(v).get_name(); - check_name(n); - name const & u = to_value(v).get_unicode_name(); - check_name(u); - register_named_object(mk_builtin(v)); - if (u != n) { - add_definition(u, to_value(v).get_type(), mk_constant(n), false); - } - } - - /** \brief Add a new builtin value set to this environment */ - void add_builtin_set(expr const & r) { - if (!is_value(r)) - throw invalid_builtin_value_declaration(env(), r); - check_name(to_value(r).get_name()); - register_named_object(mk_builtin_set(r)); - } - - /** \brief Add new definition. */ - void add_definition(name const & n, expr const & t, expr const & v, bool opaque) { - check_no_cached_type(t); - check_no_cached_type(v); - check_new_definition(n, t, v); - unsigned w = get_max_weight(v) + 1; - register_named_object(mk_definition(n, t, v, opaque, w)); - } - - /** - \brief Add new definition. - The type of the new definition is the type of \c v. - */ - void add_definition(name const & n, expr const & v, bool opaque) { - check_no_cached_type(v); - check_name(n); - expr v_t = m_type_checker->infer_type(v); - unsigned w = get_max_weight(v) + 1; - register_named_object(mk_definition(n, v_t, v, opaque, w)); - } - - /** \brief Add new theorem. */ - void add_theorem(name const & n, expr const & t, expr const & v) { - check_no_cached_type(t); - check_no_cached_type(v); - check_new_definition(n, t, v); - register_named_object(mk_theorem(n, t, v)); - } - - /** \brief Add new axiom. */ - void add_axiom(name const & n, expr const & t) { - check_no_cached_type(t); - check_name(n); - m_type_checker->check_type(t); - register_named_object(mk_axiom(n, t)); - } - - /** \brief Add new variable. */ - void add_var(name const & n, expr const & t) { - check_no_cached_type(t); - check_name(n); - m_type_checker->check_type(t); - register_named_object(mk_var_decl(n, t)); - } - - unsigned get_num_objects(bool local) const { - if (local || !has_parent()) { - return m_objects.size(); - } else { - return m_objects.size() + m_parent->get_num_objects(false); - } - } - - object const & get_object(unsigned i, bool local) const { - if (local || !has_parent()) { - return m_objects[i]; - } else { - unsigned num_parent_objects = m_parent->get_num_objects(false); - if (i >= num_parent_objects) - return m_objects[i - num_parent_objects]; - else - return m_parent->get_object(i, false); - } - } - - expr infer_type(expr const & e, context const & ctx) { - return m_type_checker->infer_type(e, ctx); - } - - expr normalize(expr const & e, context const & ctx) { - return m_type_checker->get_normalizer()(e, ctx); - } - - /** \brief Display universal variable constraints and objects stored in this environment and its parents. */ - void display(std::ostream & out) const { - if (has_parent()) - m_parent->display(out); - for (object const & obj : m_objects) { - if (obj.has_name()) { - out << obj.keyword() << " " << obj.get_name() << "\n"; - } - } - } - - bool already_imported(name const & n) const { - if (m_imported_modules.find(n) != m_imported_modules.end()) - return true; - else if (has_parent()) - return m_parent->already_imported(n); +object const & environment_cell::get_object(unsigned i, bool local) const { + if (local || !has_parent()) { + return m_objects[i]; + } else { + unsigned num_parent_objects = m_parent->get_num_objects(false); + if (i >= num_parent_objects) + return m_objects[i - num_parent_objects]; else - return false; + return m_parent->get_object(i, false); } +} - bool mark_imported_core(name n) { - if (already_imported(n)) { - return false; - } else if (has_children()) { - throw read_only_environment_exception(env()); - } else { - m_imported_modules.insert(n); - return true; +expr environment_cell::infer_type(expr const & e, context const & ctx) const { + return m_type_checker->infer_type(e, ctx); +} + +expr environment_cell::normalize(expr const & e, context const & ctx) const { + return m_type_checker->get_normalizer()(e, ctx); +} + +/** \brief Display universal variable constraints and objects stored in this environment and its parents. */ +void environment_cell::display(std::ostream & out) const { + if (has_parent()) + m_parent->display(out); + for (object const & obj : m_objects) { + if (obj.has_name()) { + out << obj.keyword() << " " << obj.get_name() << "\n"; } } +} - bool mark_imported(char const * fname) { - return mark_imported_core(name(realpath(fname))); - } +bool environment_cell::already_imported(name const & n) const { + if (m_imported_modules.find(n) != m_imported_modules.end()) + return true; + else if (has_parent()) + return m_parent->already_imported(n); + else + return false; +} - bool mark_builtin_imported(char const * id) { - return mark_imported_core(name(g_builtin_module, id)); +bool environment_cell::mark_imported_core(name n) { + if (already_imported(n)) { + return false; + } else if (has_children()) { + throw read_only_environment_exception(env()); + } else { + m_imported_modules.insert(n); + return true; } +} - imp(): - m_num_children(0) { - init_uvars(); - } +bool environment_cell::mark_imported(char const * fname) { + return mark_imported_core(name(realpath(fname))); +} - imp(std::shared_ptr const & parent): - m_num_children(0), - m_parent(parent) { - m_parent->inc_children(); - } +bool environment_cell::mark_builtin_imported(char const * id) { + return mark_imported_core(name(g_builtin_module, id)); +} - ~imp() { - if (m_parent) - m_parent->dec_children(); - } -}; +environment_cell::environment_cell(): + m_num_children(0) { + init_uvars(); +} + +environment_cell::environment_cell(std::shared_ptr const & parent): + m_num_children(0), + m_parent(parent) { + parent->inc_children(); +} + +environment_cell::~environment_cell() { + if (m_parent) + m_parent->dec_children(); +} environment::environment(): - m_ptr(new imp()) { + m_ptr(new environment_cell()) { m_ptr->m_this = m_ptr; m_ptr->m_type_checker.reset(new type_checker(*this)); } // used when creating a new child environment -environment::environment(std::shared_ptr const & parent, bool): - m_ptr(new imp(parent)) { +environment::environment(std::shared_ptr const & parent, bool): + m_ptr(new environment_cell(parent)) { m_ptr->m_this = m_ptr; m_ptr->m_type_checker.reset(new type_checker(*this)); } // used when creating a reference to the parent environment -environment::environment(std::shared_ptr const & ptr): +environment::environment(std::shared_ptr const & ptr): m_ptr(ptr) { } -environment::environment(weak_ref const & r) { +ro_environment::ro_environment(environment const & env): + m_ptr(env.m_ptr) { +} + +ro_environment::ro_environment(weak_ref const & r) { if (r.expired()) throw exception("weak reference to environment object has expired (i.e., the environment has been deleted)"); m_ptr = r.lock(); } -environment::~environment() { -} - -environment environment::mk_child() const { - return environment(m_ptr, true); -} - -bool environment::has_children() const { - return m_ptr->has_children(); -} - -bool environment::has_parent() const { - return m_ptr->has_parent(); -} - -environment environment::parent() const { - lean_assert(has_parent()); - return environment(m_ptr->m_parent); -} - -level environment::add_uvar(name const & n, level const & l) { - return m_ptr->add_uvar(n, l); -} - -bool environment::is_ge(level const & l1, level const & l2) const { - return m_ptr->is_ge(l1, l2); -} - -level environment::get_uvar(name const & n) const { - return m_ptr->get_uvar(n); -} - -void environment::add_builtin(expr const & v) { - return m_ptr->add_builtin(v); -} - -void environment::add_builtin_set(expr const & r) { - return m_ptr->add_builtin_set(r); -} - -void environment::add_definition(name const & n, expr const & t, expr const & v, bool opaque) { - m_ptr->add_definition(n, t, v, opaque); -} - -void environment::add_theorem(name const & n, expr const & t, expr const & v) { - m_ptr->add_theorem(n, t, v); -} - -void environment::add_definition(name const & n, expr const & v, bool opaque) { - m_ptr->add_definition(n, v, opaque); -} - -void environment::add_axiom(name const & n, expr const & t) { - m_ptr->add_axiom(n, t); -} - -void environment::add_var(name const & n, expr const & t) { - m_ptr->add_var(n, t); -} - -void environment::add_neutral_object(neutral_object_cell * o) { - m_ptr->m_objects.push_back(mk_neutral(o)); -} - -object environment::get_object(name const & n) const { - return m_ptr->get_object(n); -} - -optional environment::find_object(name const & n) const { - return m_ptr->get_object_core(n); -} - -unsigned environment::get_num_objects(bool local) const { - return m_ptr->get_num_objects(local); -} - -object const & environment::get_object(unsigned i, bool local) const { - return m_ptr->get_object(i, local); -} - -expr environment::infer_type(expr const & e, context const & ctx) const { - return m_ptr->infer_type(e, ctx); -} - -expr environment::normalize(expr const & e, context const & ctx) const { - return m_ptr->normalize(e, ctx); -} - -void environment::display(std::ostream & out) const { - m_ptr->display(out); -} - -bool environment::mark_imported(char const * fname) { - return m_ptr->mark_imported(fname); -} - -bool environment::mark_builtin_imported(char const * id) { - return m_ptr->mark_builtin_imported(id); -} - -environment::extension const & environment::get_extension_core(unsigned extid) const { - return m_ptr->get_extension_core(extid); -} - -environment::extension & environment::get_extension_core(unsigned extid) { - return m_ptr->get_extension_core(extid); -} - -environment::extension::extension(): +environment_extension::environment_extension(): m_env(nullptr), m_extid(0) { } -environment::extension::~extension() { +environment_extension::~environment_extension() { } -environment::extension const * environment::extension::get_parent_core() const { +environment_extension const * environment_extension::get_parent_core() const { if (m_env == nullptr) return nullptr; - imp * parent = m_env->m_parent.get(); + environment_cell * parent = m_env->m_parent.get(); while (parent) { if (m_extid < parent->m_extensions.size()) { - extension * ext = parent->m_extensions[m_extid].get(); + environment_extension * ext = parent->m_extensions[m_extid].get(); if (ext) return ext; } @@ -627,9 +501,9 @@ environment::extension const * environment::extension::get_parent_core() const { return nullptr; } -read_only_shared_environment::read_only_shared_environment(environment const & env): +read_only_shared_environment::read_only_shared_environment(ro_environment const & env): m_env(env), - m_lock(m_env.m_ptr->m_mutex) { + m_lock(const_cast(m_env.m_ptr.get())->m_mutex) { } read_only_shared_environment::~read_only_shared_environment() {} diff --git a/src/kernel/environment.h b/src/kernel/environment.h index 661cf6531..905febd23 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -7,56 +7,98 @@ Author: Leonardo de Moura #pragma once #include #include +#include +#include +#include +#include "util/lua.h" +#include "util/shared_mutex.h" #include "kernel/context.h" #include "kernel/object.h" #include "kernel/level.h" namespace lean { -/** - \brief Lean environment for defining constants, inductive - datatypes, universe variables, et.c -*/ -class environment { -private: - struct imp; - std::shared_ptr m_ptr; +class environment; +class ro_environment; +class type_checker; +class environment_extension; + +/** \brief Implementation of the Lean environment. */ +struct environment_cell { + friend class environment; + // Remark: only named objects are stored in the dictionary. + typedef std::unordered_map object_dictionary; + typedef std::tuple constraint; + std::weak_ptr m_this; + // Universe variable management + std::vector m_constraints; + std::vector m_uvars; + // Children environment management + atomic m_num_children; + std::shared_ptr m_parent; + // Object management + std::vector m_objects; + object_dictionary m_object_dictionary; + std::unique_ptr m_type_checker; + std::set m_imported_modules; // set of imported files and builtin modules + + std::vector> m_extensions; + friend class environment_extension; + + // This mutex is only used to implement threadsafe environment objects + // in the external APIs + shared_mutex m_mutex; + + environment env() const; + + void inc_children() { m_num_children++; } + void dec_children() { m_num_children--; } + + environment_extension & get_extension_core(unsigned extid); + environment_extension const & get_extension_core(unsigned extid) const; + + unsigned get_max_weight(expr const & e); + void check_name_core(name const & n); + void check_name(name const & n); + + void register_named_object(object const & new_obj); + optional get_object_core(name const & n) const; + + bool is_implied(level const & u, level const & v, int k) const; + bool is_ge(level const & l1, level const & l2, int k) const; + level add_uvar_core(name const & n); + void add_constraint(level const & u, level const & v, int d); + void add_constraints(level const & n, level const & l, int k); + void init_uvars(); + void check_no_cached_type(expr const & e); void check_type(name const & n, expr const & t, expr const & v); - environment(std::shared_ptr const & parent, bool); - explicit environment(std::shared_ptr const & ptr); - friend class read_only_shared_environment; - friend class read_write_shared_environment; + void check_new_definition(name const & n, expr const & t, expr const & v); + + bool already_imported(name const & n) const; + bool mark_imported_core(name n); + + environment_cell(std::shared_ptr const & parent); + public: - typedef std::weak_ptr weak_ref; + environment_cell(); + ~environment_cell(); - environment(); - ~environment(); - environment(weak_ref const & r); + /** \brief Return true iff this environment has children environments. */ + bool has_children() const { return m_num_children > 0; } + /** \brief Return true iff this environment has a parent environment */ + bool has_parent() const { return m_parent != nullptr; } - weak_ref to_weak_ref() const { return weak_ref(m_ptr); } + /** + \brief Return parent environment of this environment. + \pre has_parent() + */ + environment parent() const; - friend bool is_eqp(environment const & env1, environment const & env2) { return env1.m_ptr.get() == env2.m_ptr.get(); } - friend void swap(environment & env1, environment & env2) { env1.m_ptr.swap(env2.m_ptr); } - // ======================================= - // Parent/Child environment management /** \brief Create a child environment. This environment will only allow "read-only" operations until all children environments are deleted. */ environment mk_child() const; - /** \brief Return true iff this environment has children environments. */ - bool has_children() const; - - /** \brief Return true iff this environment has a parent environment. */ - bool has_parent() const; - - /** - \brief Return parent environment of this environment. - \pre has_parent() - */ - environment parent() const; - // ======================================= - // ======================================= // Universe variables /** @@ -143,7 +185,7 @@ public: \brief Find a given object in the environment. Return the null object if there is no object with the given name. */ - optional find_object(name const & n) const; + optional find_object(name const & n) const { return get_object_core(n); } /** \brief Return true iff the environment has an object with the given name */ bool has_object(name const & n) const { return static_cast(find_object(n)); } @@ -169,21 +211,21 @@ public: /** \brief Iterator for Lean environment objects. */ class object_iterator { - environment const & m_env; - unsigned m_idx; - bool m_local; - friend class environment; - object_iterator(environment const & env, unsigned idx, bool local):m_env(env), m_idx(idx), m_local(local) {} + std::shared_ptr m_env; + unsigned m_idx; + bool m_local; + friend class environment_cell; + object_iterator(std::shared_ptr && env, unsigned idx, bool local):m_env(env), m_idx(idx), m_local(local) {} public: object_iterator(object_iterator const & s):m_env(s.m_env), m_idx(s.m_idx), m_local(s.m_local) {} object_iterator & operator++() { ++m_idx; return *this; } object_iterator operator++(int) { object_iterator tmp(*this); operator++(); return tmp; } object_iterator & operator--() { --m_idx; return *this; } object_iterator operator--(int) { object_iterator tmp(*this); operator--(); return tmp; } - bool operator==(object_iterator const & s) const { lean_assert(&m_env == &(s.m_env)); return m_idx == s.m_idx; } + bool operator==(object_iterator const & s) const { lean_assert(m_env.get() == s.m_env.get()); return m_idx == s.m_idx; } bool operator!=(object_iterator const & s) const { return !operator==(s); } - object const & operator*() { return m_env.get_object(m_idx, m_local); } - object const * operator->() { return &(m_env.get_object(m_idx, m_local)); } + object const & operator*() { return m_env->get_object(m_idx, m_local); } + object const * operator->() { return &(m_env->get_object(m_idx, m_local)); } }; /** @@ -193,7 +235,7 @@ public: \remark The objects in this environment and ancestor environments are considered */ - object_iterator begin_objects() const { return object_iterator(*this, 0, false); } + object_iterator begin_objects() const { return object_iterator(m_this.lock(), 0, false); } /** \brief Return an iterator to the end of the sequence of @@ -202,52 +244,26 @@ public: \remark The objects in this environment and ancestor environments are considered */ - object_iterator end_objects() const { return object_iterator(*this, get_num_objects(false), false); } + object_iterator end_objects() const { return object_iterator(m_this.lock(), get_num_objects(false), false); } /** \brief Return an iterator to the beginning of the sequence of objects stored in this environment (objects in ancestor environments are ingored). */ - object_iterator begin_local_objects() const { return object_iterator(*this, 0, true); } + object_iterator begin_local_objects() const { return object_iterator(m_this.lock(), 0, true); } /** \brief Return an iterator to the end of the sequence of objects stored in this environment (objects in ancestor environments are ingored). */ - object_iterator end_local_objects() const { return object_iterator(*this, get_num_objects(true), true); } + object_iterator end_local_objects() const { return object_iterator(m_this.lock(), get_num_objects(true), true); } // ======================================= /** \brief Display universal variable constraints and objects stored in this environment and its parents. */ void display(std::ostream & out) const; - /** - \brief Frontend can store data in environment extensions. - Each extension is associated with a unique token/id. - This token allows the frontend to retrieve/store an extension object - in the environment - */ - class extension { - friend struct imp; - imp * m_env; - unsigned m_extid; // extension id - extension const * get_parent_core() const; - public: - extension(); - virtual ~extension(); - /** - \brief Return a constant reference for a parent extension, - and a nullptr if there is no parent/ancestor, or if the - parent/ancestor has an extension. - */ - template Ext const * get_parent() const { - extension const * ext = get_parent_core(); - lean_assert(!ext || dynamic_cast(ext) != nullptr); - return static_cast(ext); - } - }; - /** \brief Register an environment extension. Every environment object will contain this extension. The funciton mk creates a @@ -259,28 +275,23 @@ public: \see get_extension */ - typedef std::unique_ptr (*mk_extension)(); + typedef std::unique_ptr (*mk_extension)(); static unsigned register_extension(mk_extension mk); -private: - extension const & get_extension_core(unsigned extid) const; - extension & get_extension_core(unsigned extid); - -public: /** \brief Retrieve the extension associated with the token \c extid. The token is the value returned by \c register_extension. */ template Ext const & get_extension(unsigned extid) const { - extension const & ext = get_extension_core(extid); + environment_extension const & ext = get_extension_core(extid); lean_assert(dynamic_cast(&ext) != nullptr); return static_cast(ext); } template Ext & get_extension(unsigned extid) { - extension & ext = get_extension_core(extid); + environment_extension & ext = get_extension_core(extid); lean_assert(dynamic_cast(&ext) != nullptr); return static_cast(ext); } @@ -296,4 +307,66 @@ public: */ bool mark_builtin_imported(char const * id); }; + +/** + \brief Frontend can store data in environment extensions. + Each extension is associated with a unique token/id. + This token allows the frontend to retrieve/store an extension object + in the environment +*/ +class environment_extension { + friend struct environment_cell; + environment_cell * m_env; + unsigned m_extid; // extension id + environment_extension const * get_parent_core() const; +public: + environment_extension(); + virtual ~environment_extension(); + /** + \brief Return a constant reference for a parent extension, + and a nullptr if there is no parent/ancestor, or if the + parent/ancestor has an extension. + */ + template Ext const * get_parent() const { + environment_extension const * ext = get_parent_core(); + lean_assert(!ext || dynamic_cast(ext) != nullptr); + return static_cast(ext); + } +}; + +/** + \brief Reference to environment +*/ +class environment { + friend class ro_environment; + friend class environment_cell; + friend class read_write_shared_environment; + std::shared_ptr m_ptr; + environment(std::shared_ptr const & parent, bool); + environment(std::shared_ptr const & ptr); +public: + environment(); + environment_cell * operator->() const { return m_ptr.get(); } + environment_cell & operator*() const { return *(m_ptr.get()); } +}; + +/** + \brief Read-only reference to environment. +*/ +class ro_environment { + friend class environment_cell; + friend class read_only_shared_environment; + std::shared_ptr m_ptr; + ro_environment(std::shared_ptr const & p):m_ptr(p) {} + friend int push_environment(lua_State * L, ro_environment const & env); + environment cast_to_environment() const { return environment(std::const_pointer_cast(m_ptr)); } +public: + typedef std::weak_ptr weak_ref; + ro_environment(environment const & env); + ro_environment(weak_ref const & env); + explicit operator weak_ref() const { return weak_ref(m_ptr); } + weak_ref to_weak_ref() const { return weak_ref(m_ptr); } + environment_cell const * operator->() const { return m_ptr.get(); } + environment_cell const & operator*() const { return *(m_ptr.get()); } +}; } diff --git a/src/kernel/formatter.cpp b/src/kernel/formatter.cpp index deeb7a529..8044baf34 100644 --- a/src/kernel/formatter.cpp +++ b/src/kernel/formatter.cpp @@ -28,7 +28,7 @@ public: virtual format operator()(object const & obj, options const &) { std::ostringstream s; s << obj; return format(s.str()); } - virtual format operator()(environment const & env, options const &) { + virtual format operator()(ro_environment const & env, options const &) { std::ostringstream s; s << env; return format(s.str()); } }; diff --git a/src/kernel/formatter.h b/src/kernel/formatter.h index 746938b6e..4d78a9dab 100644 --- a/src/kernel/formatter.h +++ b/src/kernel/formatter.h @@ -32,13 +32,13 @@ public: /** \brief Format the given object */ virtual format operator()(object const & obj, options const & opts) = 0; /** \brief Format the given environment */ - virtual format operator()(environment const & env, options const & opts) = 0; + virtual format operator()(ro_environment const & env, options const & opts) = 0; /** \brief Return environment object associated with this formatter. Not every formatter has an associated environment object. */ - virtual optional get_environment() const { return optional(); } + virtual optional get_environment() const { return optional(); } }; /** \brief Smart-pointer for the actual formatter object (aka \c formatter_cell). @@ -51,8 +51,8 @@ public: format operator()(context const & c, options const & opts = options()) const { return (*m_cell)(c, opts); } format operator()(context const & c, expr const & e, bool format_ctx = false, options const & opts = options()) const { return (*m_cell)(c, e, format_ctx, opts); } format operator()(object const & obj, options const & opts = options()) const { return (*m_cell)(obj, opts); } - format operator()(environment const & env, options const & opts = options()) const { return (*m_cell)(env, opts); } - optional get_environment() { return m_cell->get_environment(); } + format operator()(ro_environment const & env, options const & opts = options()) const { return (*m_cell)(env, opts); } + optional get_environment() { return m_cell->get_environment(); } template friend formatter mk_formatter(FCell && fcell); }; diff --git a/src/kernel/kernel_exception.h b/src/kernel/kernel_exception.h index 32dc19754..49f715b27 100644 --- a/src/kernel/kernel_exception.h +++ b/src/kernel/kernel_exception.h @@ -17,12 +17,12 @@ class environment; /** \brief Base class for all kernel exceptions. */ class kernel_exception : public exception { protected: - environment m_env; + ro_environment m_env; public: - kernel_exception(environment const & env):m_env(env) {} - kernel_exception(environment const & env, char const * msg):exception(msg), m_env(env) {} + kernel_exception(ro_environment const & env):m_env(env) {} + kernel_exception(ro_environment const & env, char const * msg):exception(msg), m_env(env) {} virtual ~kernel_exception() noexcept {} - environment const & get_environment() const { return m_env; } + ro_environment const & get_environment() const { return m_env; } /** \brief Return a reference (if available) to the main expression associated with this exception. This information is used to provide better error messages. @@ -38,7 +38,7 @@ class unknown_name_exception : public kernel_exception { protected: name m_name; public: - unknown_name_exception(environment const & env, name const & n):kernel_exception(env), m_name(n) {} + unknown_name_exception(ro_environment const & env, name const & n):kernel_exception(env), m_name(n) {} virtual ~unknown_name_exception() {} name const & get_name() const { return m_name; } virtual format pp(formatter const & fmt, options const & opts) const; @@ -49,7 +49,7 @@ public: /** \brief Exception used to report that a universe variable is not known in a given environment. */ class unknown_universe_variable_exception : public unknown_name_exception { public: - unknown_universe_variable_exception(environment const & env, name const & n):unknown_name_exception(env, n) {} + unknown_universe_variable_exception(ro_environment const & env, name const & n):unknown_name_exception(env, n) {} virtual char const * what() const noexcept { return "unknown universe variable"; } virtual exception * clone() const { return new unknown_universe_variable_exception(m_env, m_name); } virtual void rethrow() const { throw *this; } @@ -58,7 +58,7 @@ public: /** \brief Exception used to report that an object is not known in a given environment. */ class unknown_object_exception : public unknown_name_exception { public: - unknown_object_exception(environment const & env, name const & n):unknown_name_exception(env, n) {} + unknown_object_exception(ro_environment const & env, name const & n):unknown_name_exception(env, n) {} virtual char const * what() const noexcept { return "unknown object"; } virtual exception * clone() const { return new unknown_object_exception(m_env, m_name); } virtual void rethrow() const { throw *this; } @@ -69,7 +69,7 @@ class already_declared_exception : public kernel_exception { protected: name m_name; public: - already_declared_exception(environment const & env, name const & n):kernel_exception(env), m_name(n) {} + already_declared_exception(ro_environment const & env, name const & n):kernel_exception(env), m_name(n) {} virtual ~already_declared_exception() noexcept {} name const & get_name() const { return m_name; } virtual char const * what() const noexcept { return "invalid object declaration, environment already has an object the given name"; } @@ -86,7 +86,7 @@ public: */ class read_only_environment_exception : public kernel_exception { public: - read_only_environment_exception(environment const & env):kernel_exception(env) {} + read_only_environment_exception(ro_environment const & env):kernel_exception(env) {} virtual char const * what() const noexcept { return "environment cannot be updated because it has children environments"; } virtual exception * clone() const { return new read_only_environment_exception(m_env); } virtual void rethrow() const { throw *this; } @@ -95,7 +95,7 @@ public: /** \brief Base class for type checking related exceptions. */ class type_checker_exception : public kernel_exception { public: - type_checker_exception(environment const & env):kernel_exception(env) {} + type_checker_exception(ro_environment const & env):kernel_exception(env) {} virtual exception * clone() const { return new type_checker_exception(m_env); } virtual void rethrow() const { throw *this; } }; @@ -104,7 +104,7 @@ public: class has_no_type_exception : public type_checker_exception { expr m_const; public: - has_no_type_exception(environment const & env, expr const & c):type_checker_exception(env), m_const(c) {} + has_no_type_exception(ro_environment const & env, expr const & c):type_checker_exception(env), m_const(c) {} virtual ~has_no_type_exception() {} virtual optional get_main_expr() const { return some_expr(m_const); } virtual char const * what() const noexcept { return "object does not have a type associated with it"; } @@ -128,7 +128,7 @@ class app_type_mismatch_exception : public type_checker_exception { expr m_app; std::vector m_arg_types; public: - app_type_mismatch_exception(environment const & env, context const & ctx, expr const & app, unsigned num, expr const * arg_types): + app_type_mismatch_exception(ro_environment const & env, context const & ctx, expr const & app, unsigned num, expr const * arg_types): type_checker_exception(env), m_context(ctx), m_app(app), m_arg_types(arg_types, arg_types+num) {} virtual ~app_type_mismatch_exception() {} context const & get_context() const { return m_context; } @@ -153,7 +153,7 @@ class function_expected_exception : public type_checker_exception { context m_context; expr m_expr; public: - function_expected_exception(environment const & env, context const & ctx, expr const & e): + function_expected_exception(ro_environment const & env, context const & ctx, expr const & e): type_checker_exception(env), m_context(ctx), m_expr(e) {} virtual ~function_expected_exception() {} context const & get_context() const { return m_context; } @@ -177,7 +177,7 @@ class type_expected_exception : public type_checker_exception { context m_context; expr m_expr; public: - type_expected_exception(environment const & env, context const & ctx, expr const & e): + type_expected_exception(ro_environment const & env, context const & ctx, expr const & e): type_checker_exception(env), m_context(ctx), m_expr(e) {} virtual ~type_expected_exception() {} context const & get_context() const { return m_context; } @@ -208,9 +208,9 @@ class def_type_mismatch_exception : public type_checker_exception { expr m_value; expr m_value_type; public: - def_type_mismatch_exception(environment const & env, context const & ctx, name const & n, expr const & type, expr const & val, expr const & val_type): + def_type_mismatch_exception(ro_environment const & env, context const & ctx, name const & n, expr const & type, expr const & val, expr const & val_type): type_checker_exception(env), m_context(ctx), m_name(n), m_type(type), m_value(val), m_value_type(val_type) {} - def_type_mismatch_exception(environment const & env, name const & n, expr const & type, expr const & val, expr const & val_type): + def_type_mismatch_exception(ro_environment const & env, name const & n, expr const & type, expr const & val, expr const & val_type): type_checker_exception(env), m_name(n), m_type(type), m_value(val), m_value_type(val_type) {} virtual ~def_type_mismatch_exception() {} name const & get_name() const { return m_name; } @@ -231,7 +231,7 @@ public: class invalid_builtin_value_declaration : public kernel_exception { expr m_expr; public: - invalid_builtin_value_declaration(environment const & env, expr const & e):kernel_exception(env), m_expr(e) {} + invalid_builtin_value_declaration(ro_environment const & env, expr const & e):kernel_exception(env), m_expr(e) {} virtual ~invalid_builtin_value_declaration() {} virtual char const * what() const noexcept { return "invalid builtin value declaration, expression is not a builtin value"; } virtual optional get_main_expr() const { return some_expr(m_expr); } @@ -246,7 +246,7 @@ public: class invalid_builtin_value_reference : public kernel_exception { expr m_expr; public: - invalid_builtin_value_reference(environment const & env, expr const & e):kernel_exception(env), m_expr(e) {} + invalid_builtin_value_reference(ro_environment const & env, expr const & e):kernel_exception(env), m_expr(e) {} virtual ~invalid_builtin_value_reference() {} virtual char const * what() const noexcept { return "invalid builtin value reference, this kind of builtin value was not declared in the environment"; } virtual optional get_main_expr() const { return some_expr(m_expr); } @@ -260,7 +260,7 @@ public: class unexpected_metavar_occurrence : public kernel_exception { expr m_expr; public: - unexpected_metavar_occurrence(environment const & env, expr const & e):kernel_exception(env), m_expr(e) {} + unexpected_metavar_occurrence(ro_environment const & env, expr const & e):kernel_exception(env), m_expr(e) {} virtual ~unexpected_metavar_occurrence() {} virtual char const * what() const noexcept { return "unexpected metavariable occurrence"; } virtual optional get_main_expr() const { return some_expr(m_expr); } diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp index ffe096174..a02776cfc 100644 --- a/src/kernel/normalizer.cpp +++ b/src/kernel/normalizer.cpp @@ -70,13 +70,13 @@ value_stack extend(value_stack const & s, svalue const & v) { return cons(v, s); class normalizer::imp { typedef scoped_map cache; - environment::weak_ref m_env; - context m_ctx; - cache m_cache; - unsigned m_max_depth; - unsigned m_depth; + ro_environment::weak_ref m_env; + context m_ctx; + cache m_cache; + unsigned m_max_depth; + unsigned m_depth; - environment env() const { return environment(m_env); } + ro_environment env() const { return ro_environment(m_env); } /** \brief Auxiliary object for saving the current context. @@ -198,7 +198,7 @@ class normalizer::imp { r = lookup(s, var_idx(a)); break; case expr_kind::Constant: { - object const & obj = env().get_object(const_name(a)); + object const & obj = env()->get_object(const_name(a)); if (obj.is_definition() && !obj.is_opaque()) { r = normalize(obj.get_value(), value_stack(), 0); } else { @@ -290,8 +290,8 @@ class normalizer::imp { } public: - imp(environment const & env, unsigned max_depth): - m_env(env.to_weak_ref()) { + imp(ro_environment const & env, unsigned max_depth): + m_env(env) { m_max_depth = max_depth; m_depth = 0; } @@ -305,14 +305,14 @@ public: void clear() { m_ctx = context(); m_cache.clear(); } }; -normalizer::normalizer(environment const & env, unsigned max_depth):m_ptr(new imp(env, max_depth)) {} -normalizer::normalizer(environment const & env):normalizer(env, std::numeric_limits::max()) {} -normalizer::normalizer(environment const & env, options const & opts):normalizer(env, get_normalizer_max_depth(opts)) {} +normalizer::normalizer(ro_environment const & env, unsigned max_depth):m_ptr(new imp(env, max_depth)) {} +normalizer::normalizer(ro_environment const & env):normalizer(env, std::numeric_limits::max()) {} +normalizer::normalizer(ro_environment const & env, options const & opts):normalizer(env, get_normalizer_max_depth(opts)) {} normalizer::~normalizer() {} expr normalizer::operator()(expr const & e, context const & ctx) { return (*m_ptr)(e, ctx); } void normalizer::clear() { m_ptr->clear(); } -expr normalize(expr const & e, environment const & env, context const & ctx) { +expr normalize(expr const & e, ro_environment const & env, context const & ctx) { return normalizer(env)(e, ctx); } } diff --git a/src/kernel/normalizer.h b/src/kernel/normalizer.h index b7842f3b8..0c745a304 100644 --- a/src/kernel/normalizer.h +++ b/src/kernel/normalizer.h @@ -18,9 +18,9 @@ class normalizer { class imp; std::unique_ptr m_ptr; public: - normalizer(environment const & env); - normalizer(environment const & env, unsigned max_depth); - normalizer(environment const & env, options const & opts); + normalizer(ro_environment const & env); + normalizer(ro_environment const & env, unsigned max_depth); + normalizer(ro_environment const & env, options const & opts); ~normalizer(); expr operator()(expr const & e, context const & ctx = context()); @@ -28,5 +28,5 @@ public: void clear(); }; /** \brief Normalize \c e using the environment \c env and context \c ctx */ -expr normalize(expr const & e, environment const & env, context const & ctx = context()); +expr normalize(expr const & e, ro_environment const & env, context const & ctx = context()); } diff --git a/src/kernel/printer.cpp b/src/kernel/printer.cpp index 92750420c..34f9d7455 100644 --- a/src/kernel/printer.cpp +++ b/src/kernel/printer.cpp @@ -215,9 +215,9 @@ std::ostream & operator<<(std::ostream & out, object const & obj) { return out; } -std::ostream & operator<<(std::ostream & out, environment const & env) { - std::for_each(env.begin_objects(), - env.end_objects(), +std::ostream & operator<<(std::ostream & out, ro_environment const & env) { + std::for_each(env->begin_objects(), + env->end_objects(), [&](object const & obj) { out << obj << "\n"; }); return out; } @@ -225,4 +225,4 @@ std::ostream & operator<<(std::ostream & out, environment const & env) { void print(lean::expr const & a) { std::cout << a << std::endl; } void print(lean::expr const & a, lean::context const & c) { std::cout << mk_pair(a, c) << std::endl; } void print(lean::context const & c) { std::cout << c << std::endl; } -void print(lean::environment const & e) { std::cout << e << std::endl; } +void print(lean::ro_environment const & e) { std::cout << e << std::endl; } diff --git a/src/kernel/printer.h b/src/kernel/printer.h index f13d736b6..0717692c7 100644 --- a/src/kernel/printer.h +++ b/src/kernel/printer.h @@ -11,15 +11,15 @@ Author: Leonardo de Moura #include "kernel/context.h" namespace lean { +class ro_environment; std::ostream & operator<<(std::ostream & out, context const & ctx); std::ostream & operator<<(std::ostream & out, expr const & e); std::ostream & operator<<(std::ostream & out, std::pair const & p); class object; std::ostream & operator<<(std::ostream & out, object const & obj); -class environment; -std::ostream & operator<<(std::ostream & out, environment const & env); +std::ostream & operator<<(std::ostream & out, ro_environment const & env); } void print(lean::expr const & a); void print(lean::expr const & a, lean::context const & c); void print(lean::context const & c); -void print(lean::environment const & e); +void print(lean::ro_environment const & e); diff --git a/src/kernel/threadsafe_environment.h b/src/kernel/threadsafe_environment.h index f49d2d52d..b7c342f36 100644 --- a/src/kernel/threadsafe_environment.h +++ b/src/kernel/threadsafe_environment.h @@ -18,13 +18,14 @@ namespace lean { They are only used for implementing external APIs. */ class read_only_shared_environment { - environment m_env; - shared_lock m_lock; + ro_environment m_env; + shared_lock m_lock; public: - read_only_shared_environment(environment const & env); + read_only_shared_environment(ro_environment const & env); ~read_only_shared_environment(); - operator environment const &() const { return m_env; } - environment const * operator->() const { return &m_env; } + operator ro_environment const &() const { return m_env; } + environment_cell const * operator->() const { return m_env.m_ptr.get(); } + environment_cell const & operator*() const { return *(m_env.m_ptr.get()); } }; /** @@ -36,7 +37,9 @@ class read_write_shared_environment { public: read_write_shared_environment(environment const & env); ~read_write_shared_environment(); - operator environment &() { return m_env; } - environment * operator->() { return &m_env; } + operator environment const &() const { return m_env; } + operator ro_environment() const { return ro_environment(m_env); } + environment_cell * operator->() const { return m_env.m_ptr.get(); } + environment_cell & operator*() const { return *(m_env.m_ptr.get()); } }; } diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 29b2cd76b..83906987d 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -23,7 +23,7 @@ class type_checker::imp { typedef scoped_map cache; typedef buffer unification_constraints; - environment::weak_ref m_env; + ro_environment::weak_ref m_env; cache m_cache; normalizer m_normalizer; context m_ctx; @@ -31,8 +31,8 @@ class type_checker::imp { unsigned m_menv_timestamp; unification_constraints * m_uc; - environment env() const { - return environment(m_env); + ro_environment env() const { + return ro_environment(m_env); } expr normalize(expr const & e, context const & ctx) { @@ -106,7 +106,7 @@ class type_checker::imp { if (const_type(e)) { return save_result(e, *const_type(e), shared); } else { - object const & obj = env().get_object(const_name(e)); + object const & obj = env()->get_object(const_name(e)); if (obj.has_type()) return save_result(e, obj.get_type(), shared); else @@ -208,7 +208,7 @@ class type_checker::imp { case expr_kind::Value: { // Check if the builtin value (or its set) is declared in the environment. name const & n = to_value(e).get_name(); - object obj = env().get_object(n); + object obj = env()->get_object(n); if ((obj.is_builtin() && obj.get_value() == e) || (obj.is_builtin_set() && obj.in_builtin_set(e))) { return save_result(e, to_value(e).get_type(), shared); } else { @@ -227,7 +227,7 @@ class type_checker::imp { expr const * e = &expected; while (true) { if (is_type(*e) && is_type(*g)) { - if (env().is_ge(ty_level(*e), ty_level(*g))) + if (env()->is_ge(ty_level(*e), ty_level(*g))) return true; } @@ -283,8 +283,8 @@ class type_checker::imp { } public: - imp(environment const & env): - m_env(env.to_weak_ref()), + imp(ro_environment const & env): + m_env(env), m_normalizer(env) { m_menv = nullptr; m_menv_timestamp = 0; @@ -327,7 +327,7 @@ public: } }; -type_checker::type_checker(environment const & env):m_ptr(new imp(env)) {} +type_checker::type_checker(ro_environment const & env):m_ptr(new imp(env)) {} type_checker::~type_checker() {} expr type_checker::infer_type(expr const & e, context const & ctx, metavar_env * menv, buffer * uc) { return m_ptr->infer_type(e, ctx, menv, uc); @@ -344,10 +344,10 @@ void type_checker::check_type(expr const & e, context const & ctx) { void type_checker::clear() { m_ptr->clear(); } normalizer & type_checker::get_normalizer() { return m_ptr->get_normalizer(); } -expr infer_type(expr const & e, environment const & env, context const & ctx) { +expr infer_type(expr const & e, ro_environment const & env, context const & ctx) { return type_checker(env).infer_type(e, ctx); } -bool is_convertible(expr const & given, expr const & expected, environment const & env, context const & ctx) { +bool is_convertible(expr const & given, expr const & expected, ro_environment const & env, context const & ctx) { return type_checker(env).is_convertible(given, expected, ctx); } } diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index e6b74a650..fd485c6d7 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -22,7 +22,7 @@ class type_checker { class imp; std::unique_ptr m_ptr; public: - type_checker(environment const & env); + type_checker(ro_environment const & env); ~type_checker(); /** @@ -60,6 +60,6 @@ public: normalizer & get_normalizer(); }; -expr infer_type(expr const & e, environment const & env, context const & ctx = context()); -bool is_convertible(expr const & t1, expr const & t2, environment const & env, context const & ctx = context()); +expr infer_type(expr const & e, ro_environment const & env, context const & ctx = context()); +bool is_convertible(expr const & t1, expr const & t2, ro_environment const & env, context const & ctx = context()); } diff --git a/src/library/all/all.cpp b/src/library/all/all.cpp index 9a97cedd8..4fd71f7e3 100644 --- a/src/library/all/all.cpp +++ b/src/library/all/all.cpp @@ -12,7 +12,7 @@ Author: Leonardo de Moura #include "library/all/all.h" namespace lean { -void import_all(environment & env) { +void import_all(environment const & env) { import_basic(env); hide_builtin(env); import_basic_thms(env); diff --git a/src/library/all/all.h b/src/library/all/all.h index a4f84830d..40a5244ab 100644 --- a/src/library/all/all.h +++ b/src/library/all/all.h @@ -9,7 +9,7 @@ Author: Leonardo de Moura namespace lean { /** \brief Import all builtin libraries and theorems */ -void import_all(environment & env); +void import_all(environment const & env); /** \brief Create top-level environment with all builtin libraries and theorems */ environment mk_toplevel(); } diff --git a/src/library/arith/arith.cpp b/src/library/arith/arith.cpp index 7bb9431c6..965fc69eb 100644 --- a/src/library/arith/arith.cpp +++ b/src/library/arith/arith.cpp @@ -7,7 +7,7 @@ Author: Leonardo de Moura #include "library/arith/arith.h" namespace lean { -void import_arith(environment & env) { +void import_arith(environment const & env) { import_nat(env); import_int(env); import_real(env); diff --git a/src/library/arith/arith.h b/src/library/arith/arith.h index 2e328f772..2ea15f8a4 100644 --- a/src/library/arith/arith.h +++ b/src/library/arith/arith.h @@ -15,5 +15,5 @@ class environment; /** \brief Import all arithmetic related builtin libraries. */ -void import_arith(environment & env); +void import_arith(environment const & env); } diff --git a/src/library/arith/int.cpp b/src/library/arith/int.cpp index 5de8b87dd..f2900a5f1 100644 --- a/src/library/arith/int.cpp +++ b/src/library/arith/int.cpp @@ -144,8 +144,8 @@ MK_BUILTIN(nat_to_int_fn, nat_to_int_value); MK_CONSTANT(nat_sub_fn, name({"Nat", "sub"})); MK_CONSTANT(nat_neg_fn, name({"Nat", "neg"})); -void import_int(environment & env) { - if (!env.mark_builtin_imported("int")) +void import_int(environment const & env) { + if (!env->mark_builtin_imported("int")) return; import_nat(env); expr i_i = Int >> Int; @@ -154,25 +154,25 @@ void import_int(environment & env) { expr x = Const("x"); expr y = Const("y"); - env.add_builtin(Int); - env.add_builtin_set(iVal(0)); - env.add_builtin(mk_int_add_fn()); - env.add_builtin(mk_int_mul_fn()); - env.add_builtin(mk_int_div_fn()); - env.add_builtin(mk_int_le_fn()); - env.add_builtin(mk_nat_to_int_fn()); + env->add_builtin(Int); + env->add_builtin_set(iVal(0)); + env->add_builtin(mk_int_add_fn()); + env->add_builtin(mk_int_mul_fn()); + env->add_builtin(mk_int_div_fn()); + env->add_builtin(mk_int_le_fn()); + env->add_builtin(mk_nat_to_int_fn()); - env.add_definition(int_sub_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iAdd(x, iMul(iVal(-1), y)))); - env.add_definition(int_neg_fn_name, i_i, Fun({x, Int}, iMul(iVal(-1), x))); - env.add_definition(int_mod_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iSub(x, iMul(y, iDiv(x, y))))); - env.add_definition(int_divides_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Eq(iMod(y, x), iVal(0)))); - env.add_definition(int_ge_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, iLe(y, x))); - env.add_definition(int_lt_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Not(iLe(y, x)))); - env.add_definition(int_gt_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Not(iLe(x, y)))); - env.add_definition(int_abs_fn_name, i_i, Fun({x, Int}, iIf(iLe(iVal(0), x), x, iNeg(x)))); + env->add_definition(int_sub_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iAdd(x, iMul(iVal(-1), y)))); + env->add_definition(int_neg_fn_name, i_i, Fun({x, Int}, iMul(iVal(-1), x))); + env->add_definition(int_mod_fn_name, ii_i, Fun({{x, Int}, {y, Int}}, iSub(x, iMul(y, iDiv(x, y))))); + env->add_definition(int_divides_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Eq(iMod(y, x), iVal(0)))); + env->add_definition(int_ge_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, iLe(y, x))); + env->add_definition(int_lt_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Not(iLe(y, x)))); + env->add_definition(int_gt_fn_name, ii_b, Fun({{x, Int}, {y, Int}}, Not(iLe(x, y)))); + env->add_definition(int_abs_fn_name, i_i, Fun({x, Int}, iIf(iLe(iVal(0), x), x, iNeg(x)))); - env.add_definition(nat_sub_fn_name, Nat >> (Nat >> Int), Fun({{x, Nat}, {y, Nat}}, iSub(n2i(x), n2i(y)))); - env.add_definition(nat_neg_fn_name, Nat >> Int, Fun({x, Nat}, iNeg(n2i(x)))); + env->add_definition(nat_sub_fn_name, Nat >> (Nat >> Int), Fun({{x, Nat}, {y, Nat}}, iSub(n2i(x), n2i(y)))); + env->add_definition(nat_neg_fn_name, Nat >> Int, Fun({x, Nat}, iNeg(n2i(x)))); for (auto n : {int_sub_fn_name, int_neg_fn_name, int_mod_fn_name, int_divides_fn_name, int_ge_fn_name, int_lt_fn_name, int_gt_fn_name, int_abs_fn_name, diff --git a/src/library/arith/int.h b/src/library/arith/int.h index a96c1f4a3..ddeef15f9 100644 --- a/src/library/arith/int.h +++ b/src/library/arith/int.h @@ -90,7 +90,7 @@ class environment; \brief Import Integer number library in the given environment (if it has not been imported already). It will also load the natural number library. */ -void import_int(environment & env); +void import_int(environment const & env); void open_int(lua_State * L); } diff --git a/src/library/arith/nat.cpp b/src/library/arith/nat.cpp index 3f0837eaf..3e10f6a8a 100644 --- a/src/library/arith/nat.cpp +++ b/src/library/arith/nat.cpp @@ -109,23 +109,23 @@ MK_CONSTANT(nat_lt_fn, name({"Nat", "lt"})); MK_CONSTANT(nat_gt_fn, name({"Nat", "gt"})); MK_CONSTANT(nat_id_fn, name({"Nat", "id"})); -void import_nat(environment & env) { - if (!env.mark_builtin_imported("nat")) +void import_nat(environment const & env) { + if (!env->mark_builtin_imported("nat")) return; expr nn_b = Nat >> (Nat >> Bool); expr x = Const("x"); expr y = Const("y"); - env.add_builtin(Nat); - env.add_builtin_set(nVal(0)); - env.add_builtin(mk_nat_add_fn()); - env.add_builtin(mk_nat_mul_fn()); - env.add_builtin(mk_nat_le_fn()); + env->add_builtin(Nat); + env->add_builtin_set(nVal(0)); + env->add_builtin(mk_nat_add_fn()); + env->add_builtin(mk_nat_mul_fn()); + env->add_builtin(mk_nat_le_fn()); - env.add_definition(nat_ge_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, nLe(y, x))); - env.add_definition(nat_lt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(y, x)))); - env.add_definition(nat_gt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(x, y)))); - env.add_definition(nat_id_fn_name, Nat >> Nat, Fun({x, Nat}, x)); + env->add_definition(nat_ge_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, nLe(y, x))); + env->add_definition(nat_lt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(y, x)))); + env->add_definition(nat_gt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(x, y)))); + env->add_definition(nat_id_fn_name, Nat >> Nat, Fun({x, Nat}, x)); for (auto n : {nat_ge_fn_name, nat_lt_fn_name, nat_gt_fn_name, nat_id_fn_name}) { set_hidden_flag(env, n); diff --git a/src/library/arith/nat.h b/src/library/arith/nat.h index bd49ce821..a9bfbc221 100644 --- a/src/library/arith/nat.h +++ b/src/library/arith/nat.h @@ -55,7 +55,7 @@ inline expr nIf(expr const & c, expr const & t, expr const & e) { return mk_if(N class environment; /** \brief Import Natural number library in the given environment (if it has not been imported already). */ -void import_nat(environment & env); +void import_nat(environment const & env); void open_nat(lua_State * L); } diff --git a/src/library/arith/real.cpp b/src/library/arith/real.cpp index eaa074b21..5c2b08a8c 100644 --- a/src/library/arith/real.cpp +++ b/src/library/arith/real.cpp @@ -133,8 +133,8 @@ MK_CONSTANT(real_ge_fn, name({"Real", "ge"})); MK_CONSTANT(real_lt_fn, name({"Real", "lt"})); MK_CONSTANT(real_gt_fn, name({"Real", "gt"})); -void import_real(environment & env) { - if (!env.mark_builtin_imported("real")) +void import_real(environment const & env) { + if (!env->mark_builtin_imported("real")) return; expr rr_b = Real >> (Real >> Bool); expr rr_r = Real >> (Real >> Real); @@ -142,19 +142,19 @@ void import_real(environment & env) { expr x = Const("x"); expr y = Const("y"); - env.add_builtin(Real); - env.add_builtin_set(rVal(0)); - env.add_builtin(mk_real_add_fn()); - env.add_builtin(mk_real_mul_fn()); - env.add_builtin(mk_real_div_fn()); - env.add_builtin(mk_real_le_fn()); + env->add_builtin(Real); + env->add_builtin_set(rVal(0)); + env->add_builtin(mk_real_add_fn()); + env->add_builtin(mk_real_mul_fn()); + env->add_builtin(mk_real_div_fn()); + env->add_builtin(mk_real_le_fn()); - env.add_definition(real_sub_fn_name, rr_r, Fun({{x, Real}, {y, Real}}, rAdd(x, rMul(rVal(-1), y)))); - env.add_definition(real_neg_fn_name, r_r, Fun({x, Real}, rMul(rVal(-1), x))); - env.add_definition(real_abs_fn_name, r_r, Fun({x, Real}, rIf(rLe(rVal(0), x), x, rNeg(x)))); - env.add_definition(real_ge_fn_name, rr_b, Fun({{x, Real}, {y, Real}}, rLe(y, x))); - env.add_definition(real_lt_fn_name, rr_b, Fun({{x, Real}, {y, Real}}, Not(rLe(y, x)))); - env.add_definition(real_gt_fn_name, rr_b, Fun({{x, Real}, {y, Real}}, Not(rLe(x, y)))); + env->add_definition(real_sub_fn_name, rr_r, Fun({{x, Real}, {y, Real}}, rAdd(x, rMul(rVal(-1), y)))); + env->add_definition(real_neg_fn_name, r_r, Fun({x, Real}, rMul(rVal(-1), x))); + env->add_definition(real_abs_fn_name, r_r, Fun({x, Real}, rIf(rLe(rVal(0), x), x, rNeg(x)))); + env->add_definition(real_ge_fn_name, rr_b, Fun({{x, Real}, {y, Real}}, rLe(y, x))); + env->add_definition(real_lt_fn_name, rr_b, Fun({{x, Real}, {y, Real}}, Not(rLe(y, x)))); + env->add_definition(real_gt_fn_name, rr_b, Fun({{x, Real}, {y, Real}}, Not(rLe(x, y)))); for (auto n : {real_sub_fn_name, real_neg_fn_name, real_abs_fn_name, real_ge_fn_name, real_lt_fn_name, real_gt_fn_name}) { @@ -176,15 +176,15 @@ public: MK_BUILTIN(int_to_real_fn, int_to_real_value); MK_CONSTANT(nat_to_real_fn, name("nat_to_real")); -void import_int_to_real_coercions(environment & env) { - if (!env.mark_builtin_imported("real_coercions")) +void import_int_to_real_coercions(environment const & env) { + if (!env->mark_builtin_imported("real_coercions")) return; import_int(env); import_real(env); - env.add_builtin(mk_int_to_real_fn()); + env->add_builtin(mk_int_to_real_fn()); expr x = Const("x"); - env.add_definition(nat_to_real_fn_name, Nat >> Real, Fun({x, Nat}, i2r(n2i(x)))); + env->add_definition(nat_to_real_fn_name, Nat >> Real, Fun({x, Nat}, i2r(n2i(x)))); set_hidden_flag(env, nat_to_real_fn_name); } diff --git a/src/library/arith/real.h b/src/library/arith/real.h index 05b255509..b8187096e 100644 --- a/src/library/arith/real.h +++ b/src/library/arith/real.h @@ -67,7 +67,7 @@ inline expr rIf(expr const & c, expr const & t, expr const & e) { return mk_if(R class environment; /** \brief Import (basic) Real number library in the given environment (if it has not been imported already). */ -void import_real(environment & env); +void import_real(environment const & env); /** \brief Coercion from int to real */ expr mk_int_to_real_fn(); @@ -77,7 +77,7 @@ expr mk_nat_to_real_fn(); inline expr n2r(expr const & e) { return mk_app(mk_nat_to_real_fn(), e); } /** \brief Import the coercions \c i2r and \c n2r. The Integer and (basic) Real libraries are also imported. */ -void import_int_to_real_coercions(environment & env); +void import_int_to_real_coercions(environment const & env); void open_real(lua_State * L); } diff --git a/src/library/arith/special_fn.cpp b/src/library/arith/special_fn.cpp index 2d2baef89..a111673ad 100644 --- a/src/library/arith/special_fn.cpp +++ b/src/library/arith/special_fn.cpp @@ -29,34 +29,34 @@ MK_CONSTANT(coth_fn, name("coth")); MK_CONSTANT(sech_fn, name("sech")); MK_CONSTANT(csch_fn, name("csch")); -void import_special_fn(environment & env) { - if (!env.mark_builtin_imported("special_fn")) +void import_special_fn(environment const & env) { + if (!env->mark_builtin_imported("special_fn")) return; import_real(env); expr r_r = Real >> Real; expr x = Const("x"); - env.add_var(exp_fn_name, r_r); - env.add_var(log_fn_name, r_r); + env->add_var(exp_fn_name, r_r); + env->add_var(log_fn_name, r_r); - env.add_var(real_pi_name, Real); - env.add_definition(name("pi"), Real, mk_real_pi()); // alias for pi - env.add_var(sin_fn_name, r_r); - env.add_definition(cos_fn_name, r_r, Fun({x, Real}, Sin(rSub(x, rDiv(mk_real_pi(), rVal(2)))))); - env.add_definition(tan_fn_name, r_r, Fun({x, Real}, rDiv(Sin(x), Cos(x)))); - env.add_definition(cot_fn_name, r_r, Fun({x, Real}, rDiv(Cos(x), Sin(x)))); - env.add_definition(sec_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Cos(x)))); - env.add_definition(csc_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Sin(x)))); + env->add_var(real_pi_name, Real); + env->add_definition(name("pi"), Real, mk_real_pi()); // alias for pi + env->add_var(sin_fn_name, r_r); + env->add_definition(cos_fn_name, r_r, Fun({x, Real}, Sin(rSub(x, rDiv(mk_real_pi(), rVal(2)))))); + env->add_definition(tan_fn_name, r_r, Fun({x, Real}, rDiv(Sin(x), Cos(x)))); + env->add_definition(cot_fn_name, r_r, Fun({x, Real}, rDiv(Cos(x), Sin(x)))); + env->add_definition(sec_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Cos(x)))); + env->add_definition(csc_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Sin(x)))); - env.add_definition(sinh_fn_name, r_r, Fun({x, Real}, rDiv(rSub(rVal(1), Exp(rMul(rVal(-2), x))), + env->add_definition(sinh_fn_name, r_r, Fun({x, Real}, rDiv(rSub(rVal(1), Exp(rMul(rVal(-2), x))), rMul(rVal(2), Exp(rNeg(x)))))); - env.add_definition(cosh_fn_name, r_r, Fun({x, Real}, rDiv(rAdd(rVal(1), Exp(rMul(rVal(-2), x))), + env->add_definition(cosh_fn_name, r_r, Fun({x, Real}, rDiv(rAdd(rVal(1), Exp(rMul(rVal(-2), x))), rMul(rVal(2), Exp(rNeg(x)))))); - env.add_definition(tanh_fn_name, r_r, Fun({x, Real}, rDiv(Sinh(x), Cosh(x)))); - env.add_definition(coth_fn_name, r_r, Fun({x, Real}, rDiv(Cosh(x), Sinh(x)))); - env.add_definition(sech_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Cosh(x)))); - env.add_definition(csch_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Sinh(x)))); + env->add_definition(tanh_fn_name, r_r, Fun({x, Real}, rDiv(Sinh(x), Cosh(x)))); + env->add_definition(coth_fn_name, r_r, Fun({x, Real}, rDiv(Cosh(x), Sinh(x)))); + env->add_definition(sech_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Cosh(x)))); + env->add_definition(csch_fn_name, r_r, Fun({x, Real}, rDiv(rVal(1), Sinh(x)))); for (auto n : {cos_fn_name, tan_fn_name, cot_fn_name, sec_fn_name, csc_fn_name, sinh_fn_name, cosh_fn_name, tanh_fn_name, coth_fn_name, sech_fn_name, csch_fn_name}) { diff --git a/src/library/arith/special_fn.h b/src/library/arith/special_fn.h index 8c2a96c64..ed5b8c852 100644 --- a/src/library/arith/special_fn.h +++ b/src/library/arith/special_fn.h @@ -59,5 +59,5 @@ class environment; \brief Import the special function library (if it has not been imported already). The (basic) Real Number library is also imported. */ -void import_special_fn(environment & env); +void import_special_fn(environment const & env); } diff --git a/src/library/basic_thms.cpp b/src/library/basic_thms.cpp index 1a1861a43..20491fc6a 100644 --- a/src/library/basic_thms.cpp +++ b/src/library/basic_thms.cpp @@ -47,8 +47,8 @@ MK_CONSTANT(domain_inj_fn, name("domain_inj")); MK_CONSTANT(range_inj_fn, name("range_inj")); #endif -void import_basic_thms(environment & env) { - if (!env.mark_builtin_imported("basic_thms")) +void import_basic_thms(environment const & env) { + if (!env->mark_builtin_imported("basic_thms")) return; expr A = Const("A"); expr a = Const("a"); @@ -76,215 +76,215 @@ void import_basic_thms(environment & env) { expr A_arrow_u = A >> TypeU; // Trivial : True - env.add_theorem(trivial_name, True, Refl(Bool, True)); + env->add_theorem(trivial_name, True, Refl(Bool, True)); // True_neq_False : Not(True = False) - env.add_theorem(true_neq_false_name, Not(Eq(True, False)), Trivial); + env->add_theorem(true_neq_false_name, Not(Eq(True, False)), Trivial); // EM : Pi (a : Bool), Or(a, Not(a)) - env.add_theorem(em_fn_name, Pi({a, Bool}, Or(a, Not(a))), - Fun({a, Bool}, Case(Fun({x, Bool}, Or(x, Not(x))), Trivial, Trivial, a))); + env->add_theorem(em_fn_name, Pi({a, Bool}, Or(a, Not(a))), + Fun({a, Bool}, Case(Fun({x, Bool}, Or(x, Not(x))), Trivial, Trivial, a))); // FalseElim : Pi (a : Bool) (H : False), a - env.add_theorem(false_elim_fn_name, Pi({{a, Bool}, {H, False}}, a), - Fun({{a, Bool}, {H, False}}, Case(Fun({x, Bool}, x), Trivial, H, a))); + env->add_theorem(false_elim_fn_name, Pi({{a, Bool}, {H, False}}, a), + Fun({{a, Bool}, {H, False}}, Case(Fun({x, Bool}, x), Trivial, H, a))); // Absurd : Pi (a : Bool) (H1 : a) (H2 : Not a), False - env.add_theorem(absurd_fn_name, Pi({{a, Bool}, {H1, a}, {H2, Not(a)}}, False), - Fun({{a, Bool}, {H1, a}, {H2, Not(a)}}, - MP(a, False, H2, H1))); + env->add_theorem(absurd_fn_name, Pi({{a, Bool}, {H1, a}, {H2, Not(a)}}, False), + Fun({{a, Bool}, {H1, a}, {H2, Not(a)}}, + MP(a, False, H2, H1))); // DoubleNeg : Pi (a : Bool), Eq(Not(Not(a)), a) - env.add_theorem(double_neg_fn_name, Pi({a, Bool}, Eq(Not(Not(a)), a)), - Fun({a, Bool}, Case(Fun({x, Bool}, Eq(Not(Not(x)), x)), Trivial, Trivial, a))); + env->add_theorem(double_neg_fn_name, Pi({a, Bool}, Eq(Not(Not(a)), a)), + Fun({a, Bool}, Case(Fun({x, Bool}, Eq(Not(Not(x)), x)), Trivial, Trivial, a))); // DoubleNegElim : Pi (a : Bool) (P : Bool -> Bool) (H : P (Not (Not a))), (P a) - env.add_theorem(double_neg_elim_fn_name, Pi({{a, Bool}, {P, Bool >> Bool}, {H, P(Not(Not(a)))}}, P(a)), - Fun({{a, Bool}, {P, Bool >> Bool}, {H, P(Not(Not(a)))}}, - Subst(Bool, Not(Not(a)), a, P, H, DoubleNeg(a)))); + env->add_theorem(double_neg_elim_fn_name, Pi({{a, Bool}, {P, Bool >> Bool}, {H, P(Not(Not(a)))}}, P(a)), + Fun({{a, Bool}, {P, Bool >> Bool}, {H, P(Not(Not(a)))}}, + Subst(Bool, Not(Not(a)), a, P, H, DoubleNeg(a)))); // ModusTollens : Pi (a b : Bool) (H1 : a => b) (H2 : Not(b)), Not(a) - env.add_theorem(mt_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, Not(b)}}, Not(a)), - Fun({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, Not(b)}}, - Discharge(a, False, Fun({H, a}, - Absurd(b, MP(a, b, H1, H), H2))))); + env->add_theorem(mt_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, Not(b)}}, Not(a)), + Fun({{a, Bool}, {b, Bool}, {H1, Implies(a, b)}, {H2, Not(b)}}, + Discharge(a, False, Fun({H, a}, + Absurd(b, MP(a, b, H1, H), H2))))); // Contrapositive : Pi (a b : Bool) (H : a => b), (Not(b) => Not(a)) - env.add_theorem(contrapos_fn_name, Pi({{a, Bool}, {b, Bool}, {H, Implies(a, b)}}, Implies(Not(b), Not(a))), - Fun({{a, Bool}, {b, Bool}, {H, Implies(a, b)}}, - Discharge(Not(b), Not(a), Fun({H1, Not(b)}, MT(a, b, H, H1))))); + env->add_theorem(contrapos_fn_name, Pi({{a, Bool}, {b, Bool}, {H, Implies(a, b)}}, Implies(Not(b), Not(a))), + Fun({{a, Bool}, {b, Bool}, {H, Implies(a, b)}}, + Discharge(Not(b), Not(a), Fun({H1, Not(b)}, MT(a, b, H, H1))))); // FalseImpliesAny : Pi (a : Bool), False => a - env.add_theorem(false_imp_any_fn_name, Pi({a, Bool}, Implies(False, a)), - Fun({a, Bool}, Case(Fun({x, Bool}, Implies(False, x)), Trivial, Trivial, a))); + env->add_theorem(false_imp_any_fn_name, Pi({a, Bool}, Implies(False, a)), + Fun({a, Bool}, Case(Fun({x, Bool}, Implies(False, x)), Trivial, Trivial, a))); // AbsurdImpliesAny : Pi (a c : Bool) (H1 : a) (H2 : Not a), c - env.add_theorem(absurd_imp_any_fn_name, Pi({{a, Bool}, {c, Bool}, {H1, a}, {H2, Not(a)}}, c), - Fun({{a, Bool}, {c, Bool}, {H1, a}, {H2, Not(a)}}, - MP(False, c, FalseImpAny(c), Absurd(a, H1, H2)))); + env->add_theorem(absurd_imp_any_fn_name, Pi({{a, Bool}, {c, Bool}, {H1, a}, {H2, Not(a)}}, c), + Fun({{a, Bool}, {c, Bool}, {H1, a}, {H2, Not(a)}}, + MP(False, c, FalseImpAny(c), Absurd(a, H1, H2)))); // EqMP : Pi (a b: Bool) (H1 : a = b) (H2 : a), b - env.add_theorem(eq_mp_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Eq(a, b)}, {H2, a}}, b), - Fun({{a, Bool}, {b, Bool}, {H1, Eq(a, b)}, {H2, a}}, - Subst(Bool, a, b, Fun({x, Bool}, x), H2, H1))); + env->add_theorem(eq_mp_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, Eq(a, b)}, {H2, a}}, b), + Fun({{a, Bool}, {b, Bool}, {H1, Eq(a, b)}, {H2, a}}, + Subst(Bool, a, b, Fun({x, Bool}, x), H2, H1))); // NotImp1 : Pi (a b : Bool) (H : Not(Implies(a, b))), a - env.add_theorem(not_imp1_fn_name, Pi({{a, Bool}, {b, Bool}, {H, Not(Implies(a, b))}}, a), - Fun({{a, Bool}, {b, Bool}, {H, Not(Implies(a, b))}}, - EqMP(Not(Not(a)), a, - DoubleNeg(a), - Discharge(Not(a), False, - Fun({H1, Not(a)}, - Absurd(Implies(a, b), - Discharge(a, b, - Fun({H2, a}, - FalseElim(b, Absurd(a, H2, H1)))), - H)))))); + env->add_theorem(not_imp1_fn_name, Pi({{a, Bool}, {b, Bool}, {H, Not(Implies(a, b))}}, a), + Fun({{a, Bool}, {b, Bool}, {H, Not(Implies(a, b))}}, + EqMP(Not(Not(a)), a, + DoubleNeg(a), + Discharge(Not(a), False, + Fun({H1, Not(a)}, + Absurd(Implies(a, b), + Discharge(a, b, + Fun({H2, a}, + FalseElim(b, Absurd(a, H2, H1)))), + H)))))); // NotImp2 : Pi (a b : Bool) (H : Not(Implies(a, b))), Not(b) - env.add_theorem(not_imp2_fn_name, Pi({{a, Bool}, {b, Bool}, {H, Not(Implies(a, b))}}, Not(b)), - Fun({{a, Bool}, {b, Bool}, {H, Not(Implies(a, b))}}, - Discharge(b, False, - Fun({H1, b}, - Absurd(Implies(a, b), - // a => b - DoubleNegElim(b, Fun({x, Bool}, Implies(a, x)), - // a => Not(Not(b)) - DoubleNegElim(a, Fun({x, Bool}, Implies(x, Not(Not(b)))), - // Not(Not(a)) => Not(Not(b)) - Contrapos(Not(b), Not(a), - Discharge(Not(b), Not(a), - Fun({H2, Not(b)}, - FalseElim(Not(a), Absurd(b, H1, H2))))))), - H))))); + env->add_theorem(not_imp2_fn_name, Pi({{a, Bool}, {b, Bool}, {H, Not(Implies(a, b))}}, Not(b)), + Fun({{a, Bool}, {b, Bool}, {H, Not(Implies(a, b))}}, + Discharge(b, False, + Fun({H1, b}, + Absurd(Implies(a, b), + // a => b + DoubleNegElim(b, Fun({x, Bool}, Implies(a, x)), + // a => Not(Not(b)) + DoubleNegElim(a, Fun({x, Bool}, Implies(x, Not(Not(b)))), + // Not(Not(a)) => Not(Not(b)) + Contrapos(Not(b), Not(a), + Discharge(Not(b), Not(a), + Fun({H2, Not(b)}, + FalseElim(Not(a), Absurd(b, H1, H2))))))), + H))))); // Conj : Pi (a b : Bool) (H1 : a) (H2 : b), And(a, b) - env.add_theorem(conj_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, a}, {H2, b}}, And(a, b)), - Fun({{a, Bool}, {b, Bool}, {H1, a}, {H2, b}}, - Discharge(Implies(a, Not(b)), False, Fun({H, Implies(a, Not(b))}, - Absurd(b, H2, MP(a, Not(b), H, H1)))))); + env->add_theorem(conj_fn_name, Pi({{a, Bool}, {b, Bool}, {H1, a}, {H2, b}}, And(a, b)), + Fun({{a, Bool}, {b, Bool}, {H1, a}, {H2, b}}, + Discharge(Implies(a, Not(b)), False, Fun({H, Implies(a, Not(b))}, + Absurd(b, H2, MP(a, Not(b), H, H1)))))); // Conjunct1 : Pi (a b : Bool) (H : And(a, b)), a - env.add_theorem(conjunct1_fn_name, Pi({{a, Bool}, {b, Bool}, {H, And(a, b)}}, a), - Fun({{a, Bool}, {b, Bool}, {H, And(a, b)}}, - NotImp1(a, Not(b), H))); + env->add_theorem(conjunct1_fn_name, Pi({{a, Bool}, {b, Bool}, {H, And(a, b)}}, a), + Fun({{a, Bool}, {b, Bool}, {H, And(a, b)}}, + NotImp1(a, Not(b), H))); // Conjunct2 : Pi (a b : Bool) (H : And(a, b)), b - env.add_theorem(conjunct2_fn_name, Pi({{a, Bool}, {b, Bool}, {H, And(a, b)}}, b), - Fun({{a, Bool}, {b, Bool}, {H, And(a, b)}}, - EqMP(Not(Not(b)), b, DoubleNeg(b), NotImp2(a, Not(b), H)))); + env->add_theorem(conjunct2_fn_name, Pi({{a, Bool}, {b, Bool}, {H, And(a, b)}}, b), + Fun({{a, Bool}, {b, Bool}, {H, And(a, b)}}, + EqMP(Not(Not(b)), b, DoubleNeg(b), NotImp2(a, Not(b), H)))); // Disj1 : Pi (a b : Bool) (H : a), Or(a, b) - env.add_theorem(disj1_fn_name, Pi({{a, Bool}, {b, Bool}, {H, a}}, Or(a, b)), - Fun({{a, Bool}, {b, Bool}, {H, a}}, - Discharge(Not(a), b, Fun({H1, Not(a)}, - FalseElim(b, Absurd(a, H, H1)))))); + env->add_theorem(disj1_fn_name, Pi({{a, Bool}, {b, Bool}, {H, a}}, Or(a, b)), + Fun({{a, Bool}, {b, Bool}, {H, a}}, + Discharge(Not(a), b, Fun({H1, Not(a)}, + FalseElim(b, Absurd(a, H, H1)))))); // Disj2 : Pi (b a : Bool) (H : b), Or(a, b) - env.add_theorem(disj2_fn_name, Pi({{b, Bool}, {a, Bool}, {H, b}}, Or(a, b)), - Fun({{b, Bool}, {a, Bool}, {H, b}}, - // Not(a) => b - DoubleNegElim(b, Fun({x, Bool}, Implies(Not(a), x)), - // Not(a) => Not(Not(b)) - Contrapos(Not(b), a, - Discharge(Not(b), a, Fun({H1, Not(b)}, - FalseElim(a, Absurd(b, H, H1)))))))); + env->add_theorem(disj2_fn_name, Pi({{b, Bool}, {a, Bool}, {H, b}}, Or(a, b)), + Fun({{b, Bool}, {a, Bool}, {H, b}}, + // Not(a) => b + DoubleNegElim(b, Fun({x, Bool}, Implies(Not(a), x)), + // Not(a) => Not(Not(b)) + Contrapos(Not(b), a, + Discharge(Not(b), a, Fun({H1, Not(b)}, + FalseElim(a, Absurd(b, H, H1)))))))); // DisjCases : Pi (a b c: Bool) (H1 : Or(a, b)) (H2 : a -> c) (H3 : b -> c), c */ - env.add_theorem(disj_cases_fn_name, Pi({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Or(a, b)}, {H2, a >> c}, {H3, b >> c}}, c), - Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Or(a, b)}, {H2, a >> c}, {H3, b >> c}}, - EqMP(Not(Not(c)), c, DoubleNeg(c), - Discharge(Not(c), False, - Fun({H, Not(c)}, - Absurd(c, - MP(b, c, Discharge(b, c, H3), - MP(Not(a), b, H1, - // Not(a) - MT(a, c, Discharge(a, c, H2), H))), - H)))))); + env->add_theorem(disj_cases_fn_name, Pi({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Or(a, b)}, {H2, a >> c}, {H3, b >> c}}, c), + Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, Or(a, b)}, {H2, a >> c}, {H3, b >> c}}, + EqMP(Not(Not(c)), c, DoubleNeg(c), + Discharge(Not(c), False, + Fun({H, Not(c)}, + Absurd(c, + MP(b, c, Discharge(b, c, H3), + MP(Not(a), b, H1, + // Not(a) + MT(a, c, Discharge(a, c, H2), H))), + H)))))); // Symm : Pi (A : Type u) (a b : A) (H : a = b), b = a - env.add_theorem(symm_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {H, Eq(a, b)}}, Eq(b, a)), - Fun({{A, TypeU}, {a, A}, {b, A}, {H, Eq(a, b)}}, - Subst(A, a, b, Fun({x, A}, Eq(x, a)), Refl(A, a), H))); + env->add_theorem(symm_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {H, Eq(a, b)}}, Eq(b, a)), + Fun({{A, TypeU}, {a, A}, {b, A}, {H, Eq(a, b)}}, + Subst(A, a, b, Fun({x, A}, Eq(x, a)), Refl(A, a), H))); // Trans: Pi (A: Type u) (a b c : A) (H1 : a = b) (H2 : b = c), a = c - env.add_theorem(trans_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {c, A}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c)), - Fun({{A, TypeU}, {a, A}, {b, A}, {c, A}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, - Subst(A, b, c, Fun({x, A}, Eq(a, x)), H1, H2))); + env->add_theorem(trans_fn_name, Pi({{A, TypeU}, {a, A}, {b, A}, {c, A}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, Eq(a, c)), + Fun({{A, TypeU}, {a, A}, {b, A}, {c, A}, {H1, Eq(a, b)}, {H2, Eq(b, c)}}, + Subst(A, b, c, Fun({x, A}, Eq(a, x)), H1, H2))); // EqTElim : Pi (a : Bool) (H : a = True), a - env.add_theorem(eqt_elim_fn_name, Pi({{a, Bool}, {H, Eq(a, True)}}, a), - Fun({{a, Bool}, {H, Eq(a, True)}}, - EqMP(True, a, Symm(Bool, a, True, H), Trivial))); + env->add_theorem(eqt_elim_fn_name, Pi({{a, Bool}, {H, Eq(a, True)}}, a), + Fun({{a, Bool}, {H, Eq(a, True)}}, + EqMP(True, a, Symm(Bool, a, True, H), Trivial))); // EqTIntro : Pi (a : Bool) (H : a), a = True - env.add_theorem(eqt_intro_fn_name, Pi({{a, Bool}, {H, a}}, Eq(a, True)), - Fun({{a, Bool}, {H, a}}, - ImpAntisym(a, True, - Discharge(a, True, Fun({H1, a}, Trivial)), - Discharge(True, a, Fun({H2, True}, H))))); + env->add_theorem(eqt_intro_fn_name, Pi({{a, Bool}, {H, a}}, Eq(a, True)), + Fun({{a, Bool}, {H, a}}, + ImpAntisym(a, True, + Discharge(a, True, Fun({H1, a}, Trivial)), + Discharge(True, a, Fun({H2, True}, H))))); - env.add_theorem(name("OrIdempotent"), Pi({a, Bool}, Eq(Or(a, a), a)), - Fun({a, Bool}, Case(Fun({x, Bool}, Eq(Or(x, x), x)), Trivial, Trivial, a))); + env->add_theorem(name("OrIdempotent"), Pi({a, Bool}, Eq(Or(a, a), a)), + Fun({a, Bool}, Case(Fun({x, Bool}, Eq(Or(x, x), x)), Trivial, Trivial, a))); - env.add_theorem(name("OrComm"), Pi({{a, Bool}, {b, Bool}}, Eq(Or(a, b), Or(b, a))), - Fun({{a, Bool}, {b, Bool}}, - Case(Fun({x, Bool}, Eq(Or(x, b), Or(b, x))), - Case(Fun({y, Bool}, Eq(Or(True, y), Or(y, True))), Trivial, Trivial, b), - Case(Fun({y, Bool}, Eq(Or(False, y), Or(y, False))), Trivial, Trivial, b), - a))); + env->add_theorem(name("OrComm"), Pi({{a, Bool}, {b, Bool}}, Eq(Or(a, b), Or(b, a))), + Fun({{a, Bool}, {b, Bool}}, + Case(Fun({x, Bool}, Eq(Or(x, b), Or(b, x))), + Case(Fun({y, Bool}, Eq(Or(True, y), Or(y, True))), Trivial, Trivial, b), + Case(Fun({y, Bool}, Eq(Or(False, y), Or(y, False))), Trivial, Trivial, b), + a))); - env.add_theorem(name("OrAssoc"), Pi({{a, Bool}, {b, Bool}, {c, Bool}}, Eq(Or(Or(a, b), c), Or(a, Or(b, c)))), - Fun({{a, Bool}, {b, Bool}, {c, Bool}}, - Case(Fun({x, Bool}, Eq(Or(Or(x, b), c), Or(x, Or(b, c)))), - Case(Fun({y, Bool}, Eq(Or(Or(True, y), c), Or(True, Or(y, c)))), - Case(Fun({z, Bool}, Eq(Or(Or(True, True), z), Or(True, Or(True, z)))), Trivial, Trivial, c), - Case(Fun({z, Bool}, Eq(Or(Or(True, False), z), Or(True, Or(False, z)))), Trivial, Trivial, c), b), - Case(Fun({y, Bool}, Eq(Or(Or(False, y), c), Or(False, Or(y, c)))), - Case(Fun({z, Bool}, Eq(Or(Or(False, True), z), Or(False, Or(True, z)))), Trivial, Trivial, c), - Case(Fun({z, Bool}, Eq(Or(Or(False, False), z), Or(False, Or(False, z)))), Trivial, Trivial, c), b), a))); + env->add_theorem(name("OrAssoc"), Pi({{a, Bool}, {b, Bool}, {c, Bool}}, Eq(Or(Or(a, b), c), Or(a, Or(b, c)))), + Fun({{a, Bool}, {b, Bool}, {c, Bool}}, + Case(Fun({x, Bool}, Eq(Or(Or(x, b), c), Or(x, Or(b, c)))), + Case(Fun({y, Bool}, Eq(Or(Or(True, y), c), Or(True, Or(y, c)))), + Case(Fun({z, Bool}, Eq(Or(Or(True, True), z), Or(True, Or(True, z)))), Trivial, Trivial, c), + Case(Fun({z, Bool}, Eq(Or(Or(True, False), z), Or(True, Or(False, z)))), Trivial, Trivial, c), b), + Case(Fun({y, Bool}, Eq(Or(Or(False, y), c), Or(False, Or(y, c)))), + Case(Fun({z, Bool}, Eq(Or(Or(False, True), z), Or(False, Or(True, z)))), Trivial, Trivial, c), + Case(Fun({z, Bool}, Eq(Or(Or(False, False), z), Or(False, Or(False, z)))), Trivial, Trivial, c), b), a))); // Congr1 : Pi (A : Type u) (B : A -> Type u) (f g: Pi (x : A) B x) (a : A) (H : f = g), f a = g a - env.add_theorem(congr1_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {H, Eq(f, g)}}, Eq(f(a), g(a))), - Fun({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {H, Eq(f, g)}}, - Subst(piABx, f, g, Fun({h, piABx}, Eq(f(a), h(a))), Refl(B(a), f(a)), H))); + env->add_theorem(congr1_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {H, Eq(f, g)}}, Eq(f(a), g(a))), + Fun({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {H, Eq(f, g)}}, + Subst(piABx, f, g, Fun({h, piABx}, Eq(f(a), h(a))), Refl(B(a), f(a)), H))); // Congr2 : Pi (A : Type u) (B : A -> Type u) (a b : A) (f : Pi (x : A) B x) (H : a = b), f a = f b - env.add_theorem(congr2_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {a, A}, {b, A}, {f, piABx}, {H, Eq(a, b)}}, Eq(f(a), f(b))), - Fun({{A, TypeU}, {B, A_arrow_u}, {a, A}, {b, A}, {f, piABx}, {H, Eq(a, b)}}, - Subst(A, a, b, Fun({x, A}, Eq(f(a), f(x))), Refl(B(a), f(a)), H))); + env->add_theorem(congr2_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {a, A}, {b, A}, {f, piABx}, {H, Eq(a, b)}}, Eq(f(a), f(b))), + Fun({{A, TypeU}, {B, A_arrow_u}, {a, A}, {b, A}, {f, piABx}, {H, Eq(a, b)}}, + Subst(A, a, b, Fun({x, A}, Eq(f(a), f(x))), Refl(B(a), f(a)), H))); // Congr : Pi (A : Type u) (B : A -> Type u) (f g : Pi (x : A) B x) (a b : A) (H1 : f = g) (H2 : a = b), f a = g b - env.add_theorem(congr_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {b, A}, {H1, Eq(f, g)}, {H2, Eq(a, b)}}, Eq(f(a), g(b))), - Fun({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {b, A}, {H1, Eq(f, g)}, {H2, Eq(a, b)}}, - TransExt(B(a), B(b), B(b), f(a), f(b), g(b), - Congr2(A, B, a, b, f, H2), Congr1(A, B, f, g, b, H1)))); + env->add_theorem(congr_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {b, A}, {H1, Eq(f, g)}, {H2, Eq(a, b)}}, Eq(f(a), g(b))), + Fun({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {a, A}, {b, A}, {H1, Eq(f, g)}, {H2, Eq(a, b)}}, + TransExt(B(a), B(b), B(b), f(a), f(b), g(b), + Congr2(A, B, a, b, f, H2), Congr1(A, B, f, g, b, H1)))); // ForallElim : Pi (A : Type u) (P : A -> bool) (H : (forall A P)) (a : A), P a - env.add_theorem(forall_elim_fn_name, Pi({{A, TypeU}, {P, A_pred}, {H, mk_forall(A, P)}, {a, A}}, P(a)), - Fun({{A, TypeU}, {P, A_pred}, {H, mk_forall(A, P)}, {a, A}}, - EqTElim(P(a), Congr1(A, Fun({x, A}, Bool), P, Fun({x, A}, True), a, H)))); + env->add_theorem(forall_elim_fn_name, Pi({{A, TypeU}, {P, A_pred}, {H, mk_forall(A, P)}, {a, A}}, P(a)), + Fun({{A, TypeU}, {P, A_pred}, {H, mk_forall(A, P)}, {a, A}}, + EqTElim(P(a), Congr1(A, Fun({x, A}, Bool), P, Fun({x, A}, True), a, H)))); #if 0 // STOPPED HERE // foralli : Pi (A : Type u) (P : A -> bool) (H : Pi (x : A), P x), (forall A P) - env.add_axiom(foralli_fn_name, Pi({{A, TypeU}, {P, A_pred}, {H, Pi({x, A}, P(x))}}, Forall(A, P))); + env->add_axiom(foralli_fn_name, Pi({{A, TypeU}, {P, A_pred}, {H, Pi({x, A}, P(x))}}, Forall(A, P))); // ext : Pi (A : Type u) (B : A -> Type u) (f g : Pi (x : A) B x) (H : Pi x : A, (f x) = (g x)), f = g - env.add_axiom(ext_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {H, Pi({x, A}, Eq(f(x), g(x)))}}, Eq(f, g))); + env->add_axiom(ext_fn_name, Pi({{A, TypeU}, {B, A_arrow_u}, {f, piABx}, {g, piABx}, {H, Pi({x, A}, Eq(f(x), g(x)))}}, Eq(f, g))); // domain_inj : Pi (A A1: Type u) (B : A -> Type u) (B1 : A1 -> Type u) (H : (Pi (x : A), B x) = (Pi (x : A1), B1 x)), A = A1 expr piA1B1x = Pi({x, A1}, B1(x)); expr A1_arrow_u = A1 >> TypeU; - env.add_axiom(domain_inj_fn_name, Pi({{A, TypeU}, {A1, TypeU}, {B, A_arrow_u}, {B1, A1_arrow_u}, {H, Eq(piABx, piA1B1x)}}, Eq(A, A1))); + env->add_axiom(domain_inj_fn_name, Pi({{A, TypeU}, {A1, TypeU}, {B, A_arrow_u}, {B1, A1_arrow_u}, {H, Eq(piABx, piA1B1x)}}, Eq(A, A1))); // range_inj : Pi (A A1: Type u) (B : A -> Type u) (B1 : A1 -> Type u) (a : A) (a1 : A1) (H : (Pi (x : A), B x) = (Pi (x : A1), B1 x)), (B a) = (B1 a1) - env.add_axiom(range_inj_fn_name, Pi({{A, TypeU}, {A1, TypeU}, {B, A_arrow_u}, {B1, A1_arrow_u}, {a, A}, {a1, A1}, {H, Eq(piABx, piA1B1x)}}, Eq(B(a), B1(a1)))); + env->add_axiom(range_inj_fn_name, Pi({{A, TypeU}, {A1, TypeU}, {B, A_arrow_u}, {B1, A1_arrow_u}, {a, A}, {a1, A1}, {H, Eq(piABx, piA1B1x)}}, Eq(B(a), B1(a1)))); #endif } } diff --git a/src/library/basic_thms.h b/src/library/basic_thms.h index 4f5670d47..c0254cbec 100644 --- a/src/library/basic_thms.h +++ b/src/library/basic_thms.h @@ -123,7 +123,7 @@ expr mk_forall_elim_fn(); inline expr ForallElim(expr const & A, expr const & P, expr const & H, expr const & a) { return mk_app(mk_forall_elim_fn(), A, P, H, a); } /** \brief Add basic theorems to Environment */ -void import_basic_thms(environment & env); +void import_basic_thms(environment const & env); #if 0 expr mk_ext_fn(); diff --git a/src/library/cast/cast.cpp b/src/library/cast/cast.cpp index 7348c3728..808d65d4c 100644 --- a/src/library/cast/cast.cpp +++ b/src/library/cast/cast.cpp @@ -101,8 +101,8 @@ MK_CONSTANT(cast_fn, name("cast")); MK_CONSTANT(dom_inj_fn, name("DomInj")); MK_CONSTANT(ran_inj_fn, name("RanInj")); -void import_cast(environment & env) { - if (!env.mark_builtin_imported("cast")) +void import_cast(environment const & env) { + if (!env->mark_builtin_imported("cast")) return; expr x = Const("x"); expr A = Const("A"); @@ -115,18 +115,18 @@ void import_cast(environment & env) { expr a = Const("a"); expr b = Const("b"); - env.add_builtin(mk_Cast_fn()); + env->add_builtin(mk_Cast_fn()); // Alias for Cast operator. We create the alias to be able to mark // implicit arguments. - env.add_definition(cast_fn_name, Pi({{A, TypeU}, {B, TypeU}}, Eq(A, B) >> (A >> B)), mk_Cast_fn()); + env->add_definition(cast_fn_name, Pi({{A, TypeU}, {B, TypeU}}, Eq(A, B) >> (A >> B)), mk_Cast_fn()); // DomInj : Pi (A A': Type u) (B : A -> Type u) (B' : A' -> Type u) (H : (Pi x : A, B x) = (Pi x : A', B' x)), A = A' - env.add_axiom(dom_inj_fn_name, Pi({{A, TypeU}, {Ap, TypeU}, {B, A >> TypeU}, {Bp, Ap >> TypeU}, {H, Eq(piABx, piApBpx)}}, Eq(A, Ap))); + env->add_axiom(dom_inj_fn_name, Pi({{A, TypeU}, {Ap, TypeU}, {B, A >> TypeU}, {Bp, Ap >> TypeU}, {H, Eq(piABx, piApBpx)}}, Eq(A, Ap))); // RanInj : Pi (A A': Type u) (B : A -> Type u) (B' : A' -> Type u) (H : (Pi x : A, B x) = (Pi x : A', B' x)) (a : A), // B a = B' (cast A A' (DomInj A A' B B' H) a) - env.add_axiom(ran_inj_fn_name, Pi({{A, TypeU}, {Ap, TypeU}, {B, A >> TypeU}, {Bp, Ap >> TypeU}, {H, Eq(piABx, piApBpx)}, {a, A}}, - Eq(B(a), Bp(Cast(A, Ap, DomInj(A, Ap, B, Bp, H), a))))); + env->add_axiom(ran_inj_fn_name, Pi({{A, TypeU}, {Ap, TypeU}, {B, A >> TypeU}, {Bp, Ap >> TypeU}, {H, Eq(piABx, piApBpx)}, {a, A}}, + Eq(B(a), Bp(Cast(A, Ap, DomInj(A, Ap, B, Bp, H), a))))); } } diff --git a/src/library/cast/cast.h b/src/library/cast/cast.h index 03789fe67..0a6612d71 100644 --- a/src/library/cast/cast.h +++ b/src/library/cast/cast.h @@ -41,5 +41,5 @@ inline expr RanInj(expr const & A, expr const & Ap, expr const & B, expr const & class environment; /** \brief Import type "casting" library */ -void import_cast(environment & env); +void import_cast(environment const & env); } diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index c75d49c1f..23a21f7dd 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -120,7 +120,7 @@ class elaborator::imp { } }; - environment const & m_env; + ro_environment m_env; type_inferer m_type_inferer; normalizer m_normalizer; state m_state; @@ -574,7 +574,7 @@ class elaborator::imp { int get_const_weight(expr const & a) { lean_assert(is_constant(a)); - optional obj = m_env.find_object(const_name(a)); + optional obj = m_env->find_object(const_name(a)); if (obj && obj->is_definition() && !obj->is_opaque()) return obj->get_weight(); else @@ -597,11 +597,11 @@ class elaborator::imp { expr unfold(expr const & a) { lean_assert(is_constant(a) || (is_app(a) && is_constant(arg(a, 0)))); if (is_constant(a)) { - lean_assert(m_env.find_object(const_name(a))); - return m_env.find_object(const_name(a))->get_value(); + lean_assert(m_env->find_object(const_name(a))); + return m_env->find_object(const_name(a))->get_value(); } else { - lean_assert(m_env.find_object(const_name(arg(a, 0)))); - return update_app(a, 0, m_env.find_object(const_name(arg(a, 0)))->get_value()); + lean_assert(m_env->find_object(const_name(arg(a, 0)))); + return update_app(a, 0, m_env->find_object(const_name(arg(a, 0)))->get_value()); } } @@ -1134,7 +1134,7 @@ class elaborator::imp { return false; } case expr_kind::Type: - if ((!eq && m_env.is_ge(ty_level(b), ty_level(a))) || (eq && a == b)) { + if ((!eq && m_env->is_ge(ty_level(b), ty_level(a))) || (eq && a == b)) { return true; } else { m_conflict = justification(new unification_failure_justification(c)); @@ -1386,7 +1386,7 @@ class elaborator::imp { } public: - imp(environment const & env, metavar_env const & menv, unsigned num_cnstrs, unification_constraint const * cnstrs, + imp(ro_environment const & env, metavar_env const & menv, unsigned num_cnstrs, unification_constraint const * cnstrs, options const & opts, std::shared_ptr const & p): m_env(env), m_type_inferer(env), @@ -1449,7 +1449,7 @@ public: } }; -elaborator::elaborator(environment const & env, +elaborator::elaborator(ro_environment const & env, metavar_env const & menv, unsigned num_cnstrs, unification_constraint const * cnstrs, @@ -1458,7 +1458,7 @@ elaborator::elaborator(environment const & env, m_ptr(new imp(env, menv, num_cnstrs, cnstrs, opts, p)) { } -elaborator::elaborator(environment const & env, +elaborator::elaborator(ro_environment const & env, metavar_env const & menv, context const & ctx, expr const & lhs, expr const & rhs): elaborator(env, menv, { mk_eq_constraint(ctx, lhs, rhs, justification()) }) { diff --git a/src/library/elaborator/elaborator.h b/src/library/elaborator/elaborator.h index 7150e1692..5e9297509 100644 --- a/src/library/elaborator/elaborator.h +++ b/src/library/elaborator/elaborator.h @@ -36,21 +36,21 @@ public: class imp; std::shared_ptr m_ptr; public: - elaborator(environment const & env, + elaborator(ro_environment const & env, metavar_env const & menv, unsigned num_cnstrs, unification_constraint const * cnstrs, options const & opts = options(), std::shared_ptr const & p = std::shared_ptr()); - elaborator(environment const & env, + elaborator(ro_environment const & env, metavar_env const & menv, std::initializer_list const & cnstrs, options const & opts = options(), std::shared_ptr const & p = std::shared_ptr()): elaborator(env, menv, cnstrs.size(), cnstrs.begin(), opts, p) {} - elaborator(environment const & env, + elaborator(ro_environment const & env, metavar_env const & menv, context const & ctx, expr const & lhs, expr const & rhs); diff --git a/src/library/hidden_defs.cpp b/src/library/hidden_defs.cpp index f90182568..46640af99 100644 --- a/src/library/hidden_defs.cpp +++ b/src/library/hidden_defs.cpp @@ -13,12 +13,12 @@ Author: Leonardo de Moura #include "library/kernel_bindings.h" namespace lean { -struct hidden_defs_extension : public environment::extension { +struct hidden_defs_extension : public environment_extension { typedef std::unordered_map hidden_defs; hidden_defs m_hidden_defs; hidden_defs_extension const * get_parent() const { - return environment::extension::get_parent(); + return environment_extension::get_parent(); } bool is_hidden(name const & n) const { @@ -37,31 +37,31 @@ struct hidden_defs_extension : public environment::extension { struct hidden_defs_extension_initializer { unsigned m_extid; hidden_defs_extension_initializer() { - m_extid = environment::register_extension([](){ return std::unique_ptr(new hidden_defs_extension()); }); + m_extid = environment_cell::register_extension([](){ return std::unique_ptr(new hidden_defs_extension()); }); } }; static hidden_defs_extension_initializer g_hidden_defs_extension_initializer; -static hidden_defs_extension const & to_ext(environment const & env) { - return env.get_extension(g_hidden_defs_extension_initializer.m_extid); +static hidden_defs_extension const & to_ext(ro_environment const & env) { + return env->get_extension(g_hidden_defs_extension_initializer.m_extid); } -static hidden_defs_extension & to_ext(environment & env) { - return env.get_extension(g_hidden_defs_extension_initializer.m_extid); +static hidden_defs_extension & to_ext(environment const & env) { + return env->get_extension(g_hidden_defs_extension_initializer.m_extid); } -bool is_hidden(environment const & env, name const & d) { +bool is_hidden(ro_environment const & env, name const & d) { return to_ext(env).is_hidden(d); } -void set_hidden_flag(environment & env, name const & d, bool flag) { - if (!env.get_object(d).is_definition()) +void set_hidden_flag(environment const & env, name const & d, bool flag) { + if (!env->get_object(d).is_definition()) throw exception(sstream() << "'" << d << "' is not a definition"); to_ext(env).set_hidden_flag(d, flag); } -void hide_builtin(environment & env) { +void hide_builtin(environment const & env) { for (auto c : { mk_implies_fn(), mk_iff_fn(), mk_not_fn(), mk_or_fn(), mk_and_fn(), mk_forall_fn(), mk_exists_fn(), mk_homo_eq_fn() }) set_hidden_flag(env, const_name(c)); diff --git a/src/library/hidden_defs.h b/src/library/hidden_defs.h index 486089f67..588c69a7e 100644 --- a/src/library/hidden_defs.h +++ b/src/library/hidden_defs.h @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include "util/lua.h" namespace lean { class environment; +class ro_environment; class name; /** \brief Return true iff the definition named \c d is hidden in @@ -17,7 +18,7 @@ class name; example, unfold_tactic uses it to decide whether a definition should be unfolded or not. */ -bool is_hidden(environment const & env, name const & d); +bool is_hidden(ro_environment const & env, name const & d); /** \brief Mark the definition named \c d as hidden in the given environment. @@ -25,12 +26,12 @@ bool is_hidden(environment const & env, name const & d); \remark It throws an exception if \c d is not a definition in \c env. */ -void set_hidden_flag(environment & env, name const & d, bool flag = true); +void set_hidden_flag(environment const & env, name const & d, bool flag = true); /** \brief Hide definitions at builtin.cpp. We hide them here because the hidden_defs module is not part of the kernel. */ -void hide_builtin(environment & env); +void hide_builtin(environment const & env); void open_hidden_defs(lua_State * L); } diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 3b176456e..d3283b847 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -851,7 +851,7 @@ static int formatter_call_core(lua_State * L) { static int formatter_call(lua_State * L) { formatter & fmt = to_formatter(L, 1); - optional env = fmt.get_environment(); + optional env = fmt.get_environment(); if (env) { read_only_shared_environment ro_env(*env); return formatter_call_core(L); @@ -927,6 +927,11 @@ static void open_formatter(lua_State * L) { } DECL_UDATA(environment) +int push_environment(lua_State * L, ro_environment const & env) { + // Hack to avoid having environment and ro_environment in the Lua API + // push_environment is a friend of the environment + return push_environment(L, env.cast_to_environment()); +} static environment get_global_environment(lua_State * L); @@ -1142,7 +1147,7 @@ static const struct luaL_Reg environment_m[] = { static char g_set_environment_key; -set_environment::set_environment(lua_State * L, environment & env) { +set_environment::set_environment(lua_State * L, environment const & env) { m_state = L; lua_pushlightuserdata(m_state, static_cast(&g_set_environment_key)); push_environment(m_state, env); diff --git a/src/library/kernel_bindings.h b/src/library/kernel_bindings.h index 6476980f4..1e710ec86 100644 --- a/src/library/kernel_bindings.h +++ b/src/library/kernel_bindings.h @@ -21,6 +21,7 @@ UDATA_DEFS(object) UDATA_DEFS(environment) UDATA_DEFS(justification) UDATA_DEFS(metavar_env) +int push_environment(lua_State * L, ro_environment const & env); int push_optional_expr(lua_State * L, optional const & e); int push_optional_justification(lua_State * L, optional const & j); int push_optional_object(lua_State * L, optional const & o); @@ -49,7 +50,7 @@ void set_global_formatter(lua_State * L, formatter const & fmt); class set_environment { lua_State * m_state; public: - set_environment(lua_State * L, environment & env); + set_environment(lua_State * L, environment const & env); ~set_environment(); }; diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index c774e0db1..acb818182 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -20,7 +20,7 @@ Author: Leonardo de Moura namespace lean { static name g_tmp_mvar_name = name::mk_internal_unique_name(); -static optional apply_tactic(environment const & env, proof_state const & s, +static optional apply_tactic(ro_environment const & env, proof_state const & s, expr const & th, expr const & th_type, bool all) { precision prec = s.get_precision(); if (prec != precision::Precise && prec != precision::Over) { @@ -128,14 +128,14 @@ static optional apply_tactic(environment const & env, proof_state c } tactic apply_tactic(expr const & th, expr const & th_type, bool all) { - return mk_tactic01([=](environment const & env, io_state const &, proof_state const & s) -> optional { + return mk_tactic01([=](ro_environment const & env, io_state const &, proof_state const & s) -> optional { return apply_tactic(env, s, th, th_type, all); }); } tactic apply_tactic(name const & th_name, bool all) { - return mk_tactic01([=](environment const & env, io_state const &, proof_state const & s) -> optional { - optional obj = env.find_object(th_name); + return mk_tactic01([=](ro_environment const & env, io_state const &, proof_state const & s) -> optional { + optional obj = env->find_object(th_name); if (obj && (obj->is_theorem() || obj->is_axiom())) return apply_tactic(env, s, mk_constant(th_name), obj->get_type(), all); else diff --git a/src/library/tactic/boolean_tactics.cpp b/src/library/tactic/boolean_tactics.cpp index b8b98a6a7..092fcd38b 100644 --- a/src/library/tactic/boolean_tactics.cpp +++ b/src/library/tactic/boolean_tactics.cpp @@ -17,7 +17,7 @@ Author: Leonardo de Moura namespace lean { tactic conj_tactic(bool all) { - return mk_tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional { + return mk_tactic01([=](ro_environment const &, io_state const &, proof_state const & s) -> optional { bool found = false; buffer> new_goals_buf; list> proof_info; @@ -58,7 +58,7 @@ tactic conj_tactic(bool all) { } tactic imp_tactic(name const & H_name, bool all) { - return mk_tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional { + return mk_tactic01([=](ro_environment const &, io_state const &, proof_state const & s) -> optional { expr impfn = mk_implies_fn(); bool found = false; list> proof_info; @@ -97,7 +97,7 @@ tactic imp_tactic(name const & H_name, bool all) { } tactic conj_hyp_tactic(bool all) { - return mk_tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional { + return mk_tactic01([=](ro_environment const &, io_state const &, proof_state const & s) -> optional { bool found = false; list> proof_info; // goal name -> expanded hypotheses goals new_goals = map_goals(s, [&](name const & ng, goal const & g) -> optional { @@ -207,13 +207,13 @@ optional disj_hyp_tactic_core(name const & goal_name, name const & } tactic disj_hyp_tactic(name const & goal_name, name const & hyp_name) { - return mk_tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional { + return mk_tactic01([=](ro_environment const &, io_state const &, proof_state const & s) -> optional { return disj_hyp_tactic_core(goal_name, hyp_name, s); }); } tactic disj_hyp_tactic(name const & hyp_name) { - return mk_tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional { + return mk_tactic01([=](ro_environment const &, io_state const &, proof_state const & s) -> optional { for (auto const & p1 : s.get_goals()) { check_interrupted(); goal const & g = p1.second; @@ -227,7 +227,7 @@ tactic disj_hyp_tactic(name const & hyp_name) { } tactic disj_hyp_tactic() { - return mk_tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional { + return mk_tactic01([=](ro_environment const &, io_state const &, proof_state const & s) -> optional { for (auto const & p1 : s.get_goals()) { check_interrupted(); goal const & g = p1.second; @@ -303,7 +303,7 @@ proof_state_seq disj_tactic_core(proof_state const & s, name const & gname) { } tactic disj_tactic(name const & gname) { - return mk_tactic([=](environment const &, io_state const &, proof_state const & s) -> proof_state_seq { + return mk_tactic([=](ro_environment const &, io_state const &, proof_state const & s) -> proof_state_seq { return disj_tactic_core(s, gname); }); } @@ -313,7 +313,7 @@ tactic disj_tactic() { } tactic disj_tactic(unsigned i) { - return mk_tactic([=](environment const &, io_state const &, proof_state const & s) -> proof_state_seq { + return mk_tactic([=](ro_environment const &, io_state const &, proof_state const & s) -> proof_state_seq { if (optional n = s.get_ith_goal_name(i)) return disj_tactic_core(s, *n); else @@ -322,7 +322,7 @@ tactic disj_tactic(unsigned i) { } tactic absurd_tactic() { - return mk_tactic01([](environment const &, io_state const &, proof_state const & s) -> optional { + return mk_tactic01([](ro_environment const &, io_state const &, proof_state const & s) -> optional { list> proofs; goals new_gs = map_goals(s, [&](name const & gname, goal const & g) -> optional { expr const & c = g.get_conclusion(); diff --git a/src/library/tactic/goal.cpp b/src/library/tactic/goal.cpp index f66d069b7..a34a5810c 100644 --- a/src/library/tactic/goal.cpp +++ b/src/library/tactic/goal.cpp @@ -99,7 +99,7 @@ static name mk_unique_name(name_set & s, name const & suggestion) { } } -std::pair to_goal(environment const & env, context const & ctx, expr const & t) { +std::pair to_goal(ro_environment const & env, context const & ctx, expr const & t) { type_inferer inferer(env); if (!inferer.is_proposition(t, ctx)) throw exception("to_goal failed, type is not a proposition"); diff --git a/src/library/tactic/goal.h b/src/library/tactic/goal.h index c1bc0f2af..ab8e625ac 100644 --- a/src/library/tactic/goal.h +++ b/src/library/tactic/goal.h @@ -49,7 +49,7 @@ inline hypotheses add_hypothesis(hypothesis const & h, hypotheses const & hs) { s.t. ctx |- p : T */ class goal_proof_fn { - friend std::pair to_goal(environment const & env, context const & ctx, expr const & t); + friend std::pair to_goal(ro_environment const & env, context const & ctx, expr const & t); std::vector m_constants; goal_proof_fn(std::vector && constants); public: @@ -63,7 +63,7 @@ public: We can use tactics for solving the resultant goal, and the functor \c goal_proof_fn to convert the proof for the goal into the proof term \c ?p. */ -std::pair to_goal(environment const & env, context const & ctx, expr const & t); +std::pair to_goal(ro_environment const & env, context const & ctx, expr const & t); UDATA_DEFS_CORE(hypotheses) UDATA_DEFS(goal) diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp index 8f5994d3e..ec7e5c01a 100644 --- a/src/library/tactic/proof_state.cpp +++ b/src/library/tactic/proof_state.cpp @@ -88,7 +88,7 @@ void proof_state::get_goal_names(name_set & r) const { static name g_main("main"); -proof_state to_proof_state(environment const & env, context const & ctx, expr const & t) { +proof_state to_proof_state(ro_environment const & env, context const & ctx, expr const & t) { auto gfn = to_goal(env, ctx, t); goal g = gfn.first; goal_proof_fn fn = gfn.second; diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h index 206b1b721..9bc36d773 100644 --- a/src/library/tactic/proof_state.h +++ b/src/library/tactic/proof_state.h @@ -96,7 +96,7 @@ public: format pp(formatter const & fmt, options const & opts) const; }; -proof_state to_proof_state(environment const & env, context const & ctx, expr const & t); +proof_state to_proof_state(ro_environment const & env, context const & ctx, expr const & t); inline optional some_proof_state(proof_state const & s, goals const & gs, proof_builder const & p) { return some(proof_state(s, gs, p)); diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index 1777efeea..e76435a22 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -98,7 +98,7 @@ optional to_counterexample(proof_state const & s) { return optional(); } -solve_result tactic::solve(environment const & env, io_state const & io, proof_state const & s1) { +solve_result tactic::solve(ro_environment const & env, io_state const & io, proof_state const & s1) { proof_state_seq r = operator()(env, io, s1); list failures; while (true) { @@ -120,25 +120,25 @@ solve_result tactic::solve(environment const & env, io_state const & io, proof_s } } -solve_result tactic::solve(environment const & env, io_state const & io, context const & ctx, expr const & t) { +solve_result tactic::solve(ro_environment const & env, io_state const & io, context const & ctx, expr const & t) { proof_state s = to_proof_state(env, ctx, t); return solve(env, io, s); } tactic id_tactic() { - return mk_tactic1([](environment const &, io_state const &, proof_state const & s) -> proof_state { + return mk_tactic1([](ro_environment const &, io_state const &, proof_state const & s) -> proof_state { return s; }); } tactic fail_tactic() { - return mk_tactic([](environment const &, io_state const &, proof_state const &) -> proof_state_seq { + return mk_tactic([](ro_environment const &, io_state const &, proof_state const &) -> proof_state_seq { return proof_state_seq(); }); } tactic now_tactic() { - return mk_tactic01([](environment const &, io_state const &, proof_state const & s) -> optional { + return mk_tactic01([](ro_environment const &, io_state const &, proof_state const & s) -> optional { if (!empty(s.get_goals())) return none_proof_state(); else @@ -147,7 +147,7 @@ tactic now_tactic() { } tactic trace_tactic(std::string const & msg) { - return mk_tactic1([=](environment const &, io_state const & io, proof_state const & s) -> proof_state { + return mk_tactic1([=](ro_environment const &, io_state const & io, proof_state const & s) -> proof_state { io.get_diagnostic_channel() << msg << "\n"; io.get_diagnostic_channel().get_stream().flush(); return s; @@ -163,7 +163,7 @@ tactic trace_tactic(char const * msg) { } tactic trace_state_tactic() { - return mk_tactic1([=](environment const &, io_state const & io, proof_state const & s) -> proof_state { + return mk_tactic1([=](ro_environment const &, io_state const & io, proof_state const & s) -> proof_state { options opts = io.get_options(); format fmt = s.pp(io.get_formatter(), opts); io.get_diagnostic_channel() << "Proof state:\n" << mk_pair(fmt, opts) << "\n"; @@ -173,7 +173,7 @@ tactic trace_state_tactic() { } tactic suppress_trace(tactic const & t) { - return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq { + return mk_tactic([=](ro_environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq { io_state new_io(io); std::shared_ptr out(new string_output_channel()); new_io.set_diagnostic_channel(out); @@ -182,7 +182,7 @@ tactic suppress_trace(tactic const & t) { } tactic assumption_tactic() { - return mk_tactic01([](environment const &, io_state const &, proof_state const & s) -> optional { + return mk_tactic01([](ro_environment const &, io_state const &, proof_state const & s) -> optional { list> proofs; goals new_gs = map_goals(s, [&](name const & gname, goal const & g) -> optional { expr const & c = g.get_conclusion(); @@ -209,7 +209,7 @@ tactic assumption_tactic() { } tactic then(tactic const & t1, tactic const & t2) { - return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s1) -> proof_state_seq { + return mk_tactic([=](ro_environment const & env, io_state const & io, proof_state const & s1) -> proof_state_seq { return map_append(t1(env, io, s1), [=](proof_state const & s2) { check_interrupted(); return t2(env, io, s2); @@ -218,13 +218,13 @@ tactic then(tactic const & t1, tactic const & t2) { } tactic orelse(tactic const & t1, tactic const & t2) { - return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq { + return mk_tactic([=](ro_environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq { return orelse(t1(env, io, s), t2(env, io, s), "ORELSE tactical"); }); } tactic using_params(tactic const & t, options const & opts) { - return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq { + return mk_tactic([=](ro_environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq { io_state new_io(io); new_io.set_options(join(opts, io.get_options())); return t(env, new_io, s); @@ -232,31 +232,31 @@ tactic using_params(tactic const & t, options const & opts) { } tactic try_for(tactic const & t, unsigned ms, unsigned check_ms) { - return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq { + return mk_tactic([=](ro_environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq { return timeout(t(env, io, s), ms, check_ms); }); } tactic append(tactic const & t1, tactic const & t2) { - return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq { + return mk_tactic([=](ro_environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq { return append(t1(env, io, s), t2(env, io, s), "APPEND tactical"); }); } tactic interleave(tactic const & t1, tactic const & t2) { - return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq { + return mk_tactic([=](ro_environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq { return interleave(t1(env, io, s), t2(env, io, s), "INTERLEAVE tactical"); }); } tactic par(tactic const & t1, tactic const & t2, unsigned check_ms) { - return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq { + return mk_tactic([=](ro_environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq { return par(t1(env, io, s), t2(env, io, s), check_ms); }); } tactic repeat(tactic const & t) { - return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s1) -> proof_state_seq { + return mk_tactic([=](ro_environment const & env, io_state const & io, proof_state const & s1) -> proof_state_seq { return repeat(s1, [=](proof_state const & s2) { return t(env, io, s2); }, "REPEAT tactical"); @@ -264,7 +264,7 @@ tactic repeat(tactic const & t) { } tactic repeat_at_most(tactic const & t, unsigned k) { - return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s1) -> proof_state_seq { + return mk_tactic([=](ro_environment const & env, io_state const & io, proof_state const & s1) -> proof_state_seq { return repeat_at_most(s1, [=](proof_state const & s2) { return t(env, io, s2); }, k, "REPEAT_AT_MOST tactical"); @@ -272,12 +272,12 @@ tactic repeat_at_most(tactic const & t, unsigned k) { } tactic take(tactic const & t, unsigned k) { - return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq { + return mk_tactic([=](ro_environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq { return take(k, t(env, io, s)); }); } -proof_state_seq focus_core(tactic const & t, name const & gname, environment const & env, io_state const & io, proof_state const & s) { +proof_state_seq focus_core(tactic const & t, name const & gname, ro_environment const & env, io_state const & io, proof_state const & s) { for (auto const & p : s.get_goals()) { if (p.first == gname) { proof_builder pb = mk_proof_builder( @@ -335,13 +335,13 @@ proof_state_seq focus_core(tactic const & t, name const & gname, environment con } tactic focus(tactic const & t, name const & gname) { - return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq { + return mk_tactic([=](ro_environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq { return focus_core(t, gname, env, io, s); }); } tactic focus(tactic const & t, int i) { - return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq { + return mk_tactic([=](ro_environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq { if (optional n = s.get_ith_goal_name(i)) return focus_core(t, *n, env, io, s); else @@ -393,10 +393,10 @@ public: class unfold_all_fn : public unfold_core_fn { protected: - environment m_env; + ro_environment m_env; virtual expr visit_constant(expr const & c, context const &) { - optional obj = m_env.find_object(const_name(c)); + optional obj = m_env->find_object(const_name(c)); if (obj && obj->is_definition() && !obj->is_opaque() && !is_hidden(m_env, const_name(c))) { m_unfolded = true; return obj->get_value(); @@ -406,7 +406,7 @@ protected: } public: - unfold_all_fn(environment const & env):m_env(env) {} + unfold_all_fn(ro_environment const & env):m_env(env) {} }; optional unfold_tactic_core(unfold_core_fn & fn, proof_state const & s) { @@ -423,8 +423,8 @@ optional unfold_tactic_core(unfold_core_fn & fn, proof_state const } tactic unfold_tactic(name const & n) { - return mk_tactic01([=](environment const & env, io_state const &, proof_state const & s) -> optional { - optional obj = env.find_object(n); + return mk_tactic01([=](ro_environment const & env, io_state const &, proof_state const & s) -> optional { + optional obj = env->find_object(n); if (!obj || !obj->is_definition()) return none_proof_state(); // tactic failed unfold_fn fn(n, obj->get_value()); @@ -433,7 +433,7 @@ tactic unfold_tactic(name const & n) { } tactic unfold_tactic() { - return mk_tactic01([=](environment const & env, io_state const &, proof_state const & s) -> optional { + return mk_tactic01([=](ro_environment const & env, io_state const &, proof_state const & s) -> optional { unfold_all_fn fn(env); return unfold_tactic_core(fn, s); }); @@ -462,7 +462,7 @@ public: }; tactic beta_tactic() { - return mk_tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional { + return mk_tactic01([=](ro_environment const &, io_state const &, proof_state const & s) -> optional { beta_fn fn; goals new_gs = map_goals(s, [&](name const &, goal const & g) -> optional { hypotheses new_hs = map(g.get_hypotheses(), [&](hypothesis const & h) { return hypothesis(h.first, fn(h.second)); }); @@ -547,7 +547,7 @@ static void check_ios(io_state * ios) { throw exception("failed to invoke tactic, io_state is not available"); } -static int tactic_call_core(lua_State * L, tactic t, environment env, io_state ios, proof_state s) { +static int tactic_call_core(lua_State * L, tactic t, ro_environment env, io_state ios, proof_state s) { script_state S = to_script_state(L); proof_state_seq seq; S.exec_unprotected([&]() { @@ -625,7 +625,7 @@ static int push_solve_result(lua_State * L, solve_result const & r) { return 1; } -static int tactic_solve_core(lua_State * L, tactic t, environment env, io_state ios, proof_state s) { +static int tactic_solve_core(lua_State * L, tactic t, ro_environment env, io_state ios, proof_state s) { script_state S = to_script_state(L); solve_result result; S.exec_unprotected([&]() { @@ -634,7 +634,7 @@ static int tactic_solve_core(lua_State * L, tactic t, environment env, io_state return push_solve_result(L, result); } -static int tactic_solve_core(lua_State * L, tactic t, environment env, io_state ios, context ctx, expr e) { +static int tactic_solve_core(lua_State * L, tactic t, ro_environment env, io_state ios, context ctx, expr e) { script_state S = to_script_state(L); solve_result result; S.exec_unprotected([&]() { @@ -669,7 +669,7 @@ static int mk_lua_tactic01(lua_State * L) { script_state::weak_ref S = to_script_state(L).to_weak_ref(); luaref ref(L, 1); return push_tactic(L, - mk_tactic01([=](environment const & env, io_state const & ios, proof_state const & s) -> optional { + mk_tactic01([=](ro_environment const & env, io_state const & ios, proof_state const & s) -> optional { script_state S_copy(S); optional r; luaref coref; // Remark: we have to release the reference in a protected block. @@ -713,7 +713,7 @@ static int mk_lua_cond_tactic(lua_State * L, tactic t1, tactic t2) { script_state::weak_ref S = to_script_state(L).to_weak_ref(); luaref ref(L, 1); return push_tactic(L, - mk_tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq { + mk_tactic([=](ro_environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq { return mk_proof_state_seq([=]() { script_state S_copy(S); bool cond = false; diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h index 2971b1ba5..1e44e154b 100644 --- a/src/library/tactic/tactic.h +++ b/src/library/tactic/tactic.h @@ -23,7 +23,7 @@ class tactic_cell { public: tactic_cell():m_rc(0) {} virtual ~tactic_cell() {} - virtual proof_state_seq operator()(environment const & env, io_state const & io, proof_state const & s) const = 0; + virtual proof_state_seq operator()(ro_environment const & env, io_state const & io, proof_state const & s) const = 0; }; template @@ -31,7 +31,7 @@ class tactic_cell_tpl : public tactic_cell { F m_f; public: tactic_cell_tpl(F && f):m_f(f) {} - virtual proof_state_seq operator()(environment const & env, io_state const & io, proof_state const & s) const { + virtual proof_state_seq operator()(ro_environment const & env, io_state const & io, proof_state const & s) const { return m_f(env, io, s); } }; @@ -77,13 +77,13 @@ public: tactic & operator=(tactic const & s); tactic & operator=(tactic && s); - proof_state_seq operator()(environment const & env, io_state const & io, proof_state const & s) const { + proof_state_seq operator()(ro_environment const & env, io_state const & io, proof_state const & s) const { lean_assert(m_ptr); return m_ptr->operator()(env, io, s); } - solve_result solve(environment const & env, io_state const & io, proof_state const & s); - solve_result solve(environment const & env, io_state const & io, context const & ctx, expr const & t); + solve_result solve(ro_environment const & env, io_state const & io, proof_state const & s); + solve_result solve(ro_environment const & env, io_state const & io, context const & ctx, expr const & t); }; inline optional none_tactic() { return optional(); } @@ -95,7 +95,7 @@ inline optional some_tactic(tactic && o) { return optional(std:: The functor must contain the operator: - proof_state_seq operator()(environment const & env, io_state const & io, proof_state const & s) + proof_state_seq operator()(ro_environment const & env, io_state const & io, proof_state const & s) */ template @@ -111,7 +111,7 @@ inline proof_state_seq mk_proof_state_seq(F && f) { The functor f must contain the method: - proof_state operator()(environment const & env, io_state const & io, proof_state const & s) + proof_state operator()(ro_environment const & env, io_state const & io, proof_state const & s) \remark The functor is invoked on demand. @@ -119,7 +119,7 @@ inline proof_state_seq mk_proof_state_seq(F && f) { template tactic mk_tactic1(F && f) { return - mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) { + mk_tactic([=](ro_environment const & env, io_state const & io, proof_state const & s) { return mk_proof_state_seq([=]() { return some(mk_pair(f(env, io, s), proof_state_seq())); }); }); } @@ -129,7 +129,7 @@ tactic mk_tactic1(F && f) { The functor f must contain the method: - optional operator()(environment const & env, io_state const & io, proof_state const & s) + optional operator()(ro_environment const & env, io_state const & io, proof_state const & s) \remark The functor is invoked on demand. @@ -137,7 +137,7 @@ tactic mk_tactic1(F && f) { template tactic mk_tactic01(F && f) { return - mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) { + mk_tactic([=](ro_environment const & env, io_state const & io, proof_state const & s) { return mk_proof_state_seq([=]() { auto r = f(env, io, s); if (r) @@ -263,7 +263,7 @@ inline tactic determ(tactic const & t) { return take(t, 1); } */ template tactic cond(P && p, tactic const & t1, tactic const & t2) { - return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq { + return mk_tactic([=](ro_environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq { return mk_proof_state_seq([=]() { if (p(env, io, s)) { return t1(env, io, s).pull(); diff --git a/src/library/type_inferer.cpp b/src/library/type_inferer.cpp index 2ff9be6f2..8c773b4ee 100644 --- a/src/library/type_inferer.cpp +++ b/src/library/type_inferer.cpp @@ -24,7 +24,7 @@ class type_inferer::imp { typedef scoped_map cache; typedef buffer unification_constraints; - environment m_env; + ro_environment m_env; context m_ctx; metavar_env * m_menv; unsigned m_menv_timestamp; @@ -114,7 +114,7 @@ class type_inferer::imp { if (const_type(e)) { return *const_type(e); } else { - object const & obj = m_env.get_object(const_name(e)); + object const & obj = m_env->get_object(const_name(e)); if (obj.has_type()) return obj.get_type(); else @@ -216,7 +216,7 @@ class type_inferer::imp { } public: - imp(environment const & env): + imp(ro_environment const & env): m_env(env), m_normalizer(env) { m_menv = nullptr; @@ -253,7 +253,7 @@ public: return is_bool(normalize(t, ctx)); } }; -type_inferer::type_inferer(environment const & env):m_ptr(new imp(env)) {} +type_inferer::type_inferer(ro_environment const & env):m_ptr(new imp(env)) {} type_inferer::~type_inferer() {} expr type_inferer::operator()(expr const & e, context const & ctx, metavar_env * menv, buffer * uc) { return m_ptr->operator()(e, ctx, menv, uc); diff --git a/src/library/type_inferer.h b/src/library/type_inferer.h index 84d1a9e77..9464d5bef 100644 --- a/src/library/type_inferer.h +++ b/src/library/type_inferer.h @@ -28,7 +28,7 @@ class type_inferer { class imp; std::unique_ptr m_ptr; public: - type_inferer(environment const & env); + type_inferer(ro_environment const & env); ~type_inferer(); expr operator()(expr const & e, context const & ctx, metavar_env * menv, buffer * uc); diff --git a/src/tests/frontends/lean/frontend.cpp b/src/tests/frontends/lean/frontend.cpp index b079a4cd6..06cb5c8d6 100644 --- a/src/tests/frontends/lean/frontend.cpp +++ b/src/tests/frontends/lean/frontend.cpp @@ -21,7 +21,7 @@ static void tst1() { 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()); + lean_assert(f.get_environment()->has_children()); } static void tst2() { @@ -103,7 +103,7 @@ static void tst6() { std::cout << "=================\n"; frontend f; environment env; - env.add_neutral_object(new alien_cell()); + env->add_neutral_object(new alien_cell()); formatter fmt = mk_pp_formatter(f); std::cout << fmt(env) << "\n"; } diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp index 851b403e3..4025fa2c1 100644 --- a/src/tests/kernel/environment.cpp +++ b/src/tests/kernel/environment.cpp @@ -20,86 +20,86 @@ using namespace lean; static void tst1() { environment env; - level u = env.add_uvar("u", level() + 1); - level w = env.add_uvar("w", u + 1); - lean_assert(!env.has_children()); - lean_assert(!env.has_parent()); + level u = env->add_uvar("u", level() + 1); + level w = env->add_uvar("w", u + 1); + lean_assert(!env->has_children()); + lean_assert(!env->has_parent()); { - environment child = env.mk_child(); - lean_assert(child.is_ge(w, u)); - lean_assert(child.is_ge(w, level() + 2)); - lean_assert(env.is_ge(w, level() + 2)); - lean_assert(env.has_children()); - lean_assert(child.has_parent()); - lean_assert(!env.has_parent()); + environment child = env->mk_child(); + lean_assert(child->is_ge(w, u)); + lean_assert(child->is_ge(w, level() + 2)); + lean_assert(env->is_ge(w, level() + 2)); + lean_assert(env->has_children()); + lean_assert(child->has_parent()); + lean_assert(!env->has_parent()); try { - level o = env.add_uvar("o", w + 1); + level o = env->add_uvar("o", w + 1); lean_unreachable(); } catch (exception const & ex) { std::cout << "expected error: " << ex.what() << "\n"; } } std::cout << "tst1 checkpoint" << std::endl; - level o = env.add_uvar("o", w + 1); - lean_assert(!env.has_children()); + level o = env->add_uvar("o", w + 1); + lean_assert(!env->has_children()); std::cout << env; } static environment mk_child() { environment env; - level u = env.add_uvar("u", level() + 1); - return env.mk_child(); + level u = env->add_uvar("u", level() + 1); + return env->mk_child(); } static void tst2() { environment child = mk_child(); - lean_assert(child.has_parent()); - lean_assert(!child.has_children()); - environment parent = child.parent(); + lean_assert(child->has_parent()); + lean_assert(!child->has_children()); + environment parent = child->parent(); std::cout << parent; - lean_assert(parent.has_children()); - std::cout << "uvar: " << child.get_uvar("u") << "\n"; + lean_assert(parent->has_children()); + std::cout << "uvar: " << child->get_uvar("u") << "\n"; } static void tst3() { std::cout << "tst3\n"; environment env = mk_toplevel(); try { - env.add_definition("a", Int, Const("a")); + env->add_definition("a", Int, Const("a")); lean_unreachable(); } catch (exception const & ex) { std::cout << "expected error: " << ex.what() << "\n"; } - env.add_definition("a", Int, iAdd(iVal(1), iVal(2))); + env->add_definition("a", Int, iAdd(iVal(1), iVal(2))); std::cout << env << "\n"; expr t = iAdd(Const("a"), iVal(1)); std::cout << t << " --> " << normalize(t, env) << "\n"; lean_assert(normalize(t, env) == iVal(4)); - env.add_definition("b", Int, iMul(iVal(2), Const("a"))); + env->add_definition("b", Int, iMul(iVal(2), Const("a"))); std::cout << "b --> " << normalize(Const("b"), env) << "\n"; lean_assert(normalize(Const("b"), env) == iVal(6)); try { - env.add_definition("c", mk_arrow(Int, Int), Const("a")); + env->add_definition("c", mk_arrow(Int, Int), Const("a")); lean_unreachable(); } catch (exception const & ex) { std::cout << "expected error: " << ex.what() << "\n"; } try { - env.add_definition("a", Int, iVal(10)); + env->add_definition("a", Int, iVal(10)); lean_unreachable(); } catch (exception const & ex) { std::cout << "expected error: " << ex.what() << "\n"; } - environment c_env = env.mk_child(); + environment c_env = env->mk_child(); try { - env.add_definition("c", Int, Const("a")); + env->add_definition("c", Int, Const("a")); lean_unreachable(); } catch (exception const & ex) { std::cout << "expected error: " << ex.what() << "\n"; } lean_assert(normalize(Const("b"), env) == iVal(6)); lean_assert(normalize(Const("b"), c_env) == iVal(6)); - c_env.add_definition("c", Int, Const("a")); + c_env->add_definition("c", Int, Const("a")); lean_assert(normalize(Const("c"), c_env) == iVal(3)); try { expr r = normalize(Const("c"), env); @@ -114,11 +114,11 @@ static void tst3() { static void tst4() { std::cout << "tst4\n"; environment env = mk_toplevel(); - env.add_definition("a", Int, iVal(1), true); // add opaque definition + env->add_definition("a", Int, iVal(1), true); // add opaque definition expr t = iAdd(Const("a"), iVal(1)); std::cout << t << " --> " << normalize(t, env) << "\n"; lean_assert(normalize(t, env) == t); - env.add_definition("b", Int, iAdd(Const("a"), iVal(1))); + env->add_definition("b", Int, iAdd(Const("a"), iVal(1))); expr t2 = iSub(Const("b"), iVal(9)); std::cout << t2 << " --> " << normalize(t2, env) << "\n"; lean_assert(normalize(t2, env) == iAdd(iAdd(Const("a"), iVal(1)), iVal(-9))); @@ -126,7 +126,7 @@ static void tst4() { static void tst5() { environment env = mk_toplevel(); - env.add_definition("a", Int, iVal(1), true); // add opaque definition + env->add_definition("a", Int, iVal(1), true); // add opaque definition try { std::cout << infer_type(iAdd(Const("a"), Int), env) << "\n"; lean_unreachable(); @@ -137,9 +137,9 @@ static void tst5() { static void tst6() { environment env = mk_toplevel(); - level u = env.add_uvar("u", level() + 1); - level w = env.add_uvar("w", u + 1); - env.add_var("f", mk_arrow(Type(u), Type(u))); + level u = env->add_uvar("u", level() + 1); + level w = env->add_uvar("w", u + 1); + env->add_var("f", mk_arrow(Type(u), Type(u))); expr t = Const("f")(Int); std::cout << "type of " << t << " is " << infer_type(t, env) << "\n"; try { @@ -164,8 +164,8 @@ static void tst6() { static void tst7() { environment env = mk_toplevel(); - env.add_var("a", Int); - env.add_var("b", Int); + env->add_var("a", Int); + env->add_var("b", Int); expr t = If(Int, True, Const("a"), Const("b")); std::cout << t << " --> " << normalize(t, env) << "\n"; std::cout << infer_type(t, env) << "\n"; @@ -175,36 +175,36 @@ static void tst7() { static void tst8() { environment env; std::cout << "=======================\n"; - env.add_var("a", Type()); - env.add_var("b", Type()); - environment env2 = env.mk_child(); - env2.add_var("c", Type()); - env2.add_var("d", Type()); - env2.add_var("e", Type()); + env->add_var("a", Type()); + env->add_var("b", Type()); + environment env2 = env->mk_child(); + env2->add_var("c", Type()); + env2->add_var("d", Type()); + env2->add_var("e", Type()); unsigned counter = 0; - std::for_each(env2.begin_local_objects(), env2.end_local_objects(), [&](object const & obj) { std::cout << obj.keyword() << " " << obj.get_name() << "\n"; counter++; }); + std::for_each(env2->begin_local_objects(), env2->end_local_objects(), [&](object const & obj) { std::cout << obj.keyword() << " " << obj.get_name() << "\n"; counter++; }); lean_assert(counter == 3); std::cout << "=======================\n"; counter = 0; - std::for_each(env2.begin_objects(), env2.end_objects(), [&](object const & obj) { std::cout << obj.keyword() << " " << obj.get_name() << "\n"; counter++; }); + std::for_each(env2->begin_objects(), env2->end_objects(), [&](object const & obj) { std::cout << obj.keyword() << " " << obj.get_name() << "\n"; counter++; }); lean_assert(counter == 5); - environment env3 = env2.mk_child(); - env3.add_var("f", Type() >> Type()); + environment env3 = env2->mk_child(); + env3->add_var("f", Type() >> Type()); std::cout << "=======================\n"; counter = 0; - std::for_each(env3.begin_objects(), env3.end_objects(), [&](object const & obj) { std::cout << obj.keyword() << " " << obj.get_name() << "\n"; counter++; }); + std::for_each(env3->begin_objects(), env3->end_objects(), [&](object const & obj) { std::cout << obj.keyword() << " " << obj.get_name() << "\n"; counter++; }); lean_assert(counter == 6); } static void tst9() { try { environment env; - env.add_uvar("u1", level()); - env.add_uvar("u2", level()); - env.add_uvar("u1", level("u2")); + env->add_uvar("u1", level()); + env->add_uvar("u2", level()); + env->add_uvar("u1", level("u2")); } catch (already_declared_exception & ex) { std::cout << ex.what() << "\n"; - level l = ex.get_environment().get_uvar(ex.get_name()); + level l = ex.get_environment()->get_uvar(ex.get_name()); std::cout << l << "\n"; } } @@ -212,20 +212,20 @@ static void tst9() { static void tst10() { environment env; import_all(env); - env.add_definition("a", Int, iVal(1)); - lean_assert(env.get_object("a").get_weight() == 1); + env->add_definition("a", Int, iVal(1)); + lean_assert(env->get_object("a").get_weight() == 1); expr a = Const("a"); expr b = Const("b"); expr c = Const("c"); - env.add_definition("b", Int, iAdd(a, a)); - lean_assert(env.get_object("b").get_weight() == 2); - env.add_definition("c", Int, iAdd(a, b)); - lean_assert(env.get_object("c").get_weight() == 3); - env.add_definition("d", Int, iAdd(b, b)); - lean_assert(env.get_object("d").get_weight() == 3); + env->add_definition("b", Int, iAdd(a, a)); + lean_assert(env->get_object("b").get_weight() == 2); + env->add_definition("c", Int, iAdd(a, b)); + lean_assert(env->get_object("c").get_weight() == 3); + env->add_definition("d", Int, iAdd(b, b)); + lean_assert(env->get_object("d").get_weight() == 3); } -struct my_extension : public environment::extension { +struct my_extension : public environment_extension { unsigned m_value1; unsigned m_value2; my_extension():m_value1(0), m_value2(0) {} @@ -234,7 +234,7 @@ struct my_extension : public environment::extension { struct my_extension_reg { unsigned m_extid; my_extension_reg() { - m_extid = environment::register_extension([](){ return std::unique_ptr(new my_extension()); }); + m_extid = environment_cell::register_extension([](){ return std::unique_ptr(new my_extension()); }); } }; @@ -243,14 +243,14 @@ static my_extension_reg R; static void tst11() { unsigned extid = R.m_extid; environment env; - my_extension & ext = env.get_extension(extid); + my_extension & ext = env->get_extension(extid); ext.m_value1 = 10; ext.m_value2 = 20; - my_extension & ext2 = env.get_extension(extid); + my_extension & ext2 = env->get_extension(extid); lean_assert(ext2.m_value1 == 10); lean_assert(ext2.m_value2 == 20); - environment child = env.mk_child(); - my_extension & ext3 = child.get_extension(extid); + environment child = env->mk_child(); + my_extension & ext3 = child->get_extension(extid); lean_assert(ext3.m_value1 == 0); lean_assert(ext3.m_value2 == 0); my_extension const * ext4 = ext3.get_parent(); @@ -263,21 +263,22 @@ static void tst11() { static void tst12() { unsigned extid = R.m_extid; environment env; - environment child = env.mk_child(); - my_extension & ext = child.get_extension(extid); + environment child = env->mk_child(); + my_extension & ext = child->get_extension(extid); lean_assert(ext.m_value1 == 0); lean_assert(ext.m_value2 == 0); lean_assert(ext.get_parent() == nullptr); } static void tst13() { - environment::weak_ref wref; + ro_environment::weak_ref wref; { environment env; - wref = env.to_weak_ref(); + ro_environment roenv(env); + wref = roenv.to_weak_ref(); } try { - environment env2(wref); + ro_environment env2(wref); lean_unreachable(); } catch (exception &) {} } diff --git a/src/tests/kernel/level.cpp b/src/tests/kernel/level.cpp index add0bc104..5b762da66 100644 --- a/src/tests/kernel/level.cpp +++ b/src/tests/kernel/level.cpp @@ -13,13 +13,13 @@ using namespace lean; static void tst0() { environment env; - lean_assert(env.begin_objects() == env.end_objects()); - std::for_each(env.begin_objects(), env.end_objects(), [&](object const & obj) { + lean_assert(env->begin_objects() == env->end_objects()); + std::for_each(env->begin_objects(), env->end_objects(), [&](object const & obj) { std::cout << obj.keyword() << "\n"; }); - level l1 = env.add_uvar(name(name("l1"), "suffix"), level()); - lean_assert(env.begin_objects() != env.end_objects()); - std::for_each(env.begin_objects(), env.end_objects(), [&](object const & obj) { + level l1 = env->add_uvar(name(name("l1"), "suffix"), level()); + lean_assert(env->begin_objects() != env->end_objects()); + std::for_each(env->begin_objects(), env->end_objects(), [&](object const & obj) { std::cout << obj.keyword() << "\n"; }); std::cout << env; @@ -27,23 +27,23 @@ static void tst0() { static void tst1() { environment env; - level l1 = env.add_uvar(name(name("l1"), "suffix"), level()); - level l2 = env.add_uvar("l2", l1 + 10); - level l3 = env.add_uvar("l3", max(l2, l1 + 3)); - level l4 = env.add_uvar("l4", max(l1 + 8, max(l2 + 2, l3 + 20))); + level l1 = env->add_uvar(name(name("l1"), "suffix"), level()); + level l2 = env->add_uvar("l2", l1 + 10); + level l3 = env->add_uvar("l3", max(l2, l1 + 3)); + level l4 = env->add_uvar("l4", max(l1 + 8, max(l2 + 2, l3 + 20))); std::cout << pp(max(l1 + 8, max(l2 + 2, l3 + 20))) << "\n"; std::cout << pp(level()) << "\n"; std::cout << pp(level()+1) << "\n"; std::cout << env; - lean_assert(env.is_ge(l4 + 10, l3 + 30)); - lean_assert(!env.is_ge(l4 + 9, l3 + 30)); + lean_assert(env->is_ge(l4 + 10, l3 + 30)); + lean_assert(!env->is_ge(l4 + 9, l3 + 30)); } static void tst2() { environment env; - level l1 = env.add_uvar("l1", level()); + level l1 = env->add_uvar("l1", level()); try { - level l2 = env.add_uvar("l1", level()); + level l2 = env->add_uvar("l1", level()); lean_unreachable(); } catch (exception & ex) { @@ -53,10 +53,10 @@ static void tst2() { static void tst3() { environment env; - level l1 = env.add_uvar("l1", level()); - level l2 = env.add_uvar("l2", l1 + ((1<<30) + 1024)); + level l1 = env->add_uvar("l1", level()); + level l2 = env->add_uvar("l2", l1 + ((1<<30) + 1024)); try { - level l3 = env.add_uvar("l3", l2 + (1<<30)); + level l3 = env->add_uvar("l3", l2 + (1<<30)); lean_unreachable(); } catch (exception & ex) { @@ -66,36 +66,36 @@ static void tst3() { static void tst4() { environment env; - level l1 = env.add_uvar("l1", level() + 1); - level l2 = env.add_uvar("l2", level() + 1); - level l3 = env.add_uvar("l3", max(l1, l2) + 1); - level l4 = env.add_uvar("l4", l3 + 1); - level l5 = env.add_uvar("l5", l3 + 1); - level l6 = env.add_uvar("l6", max(l4, l5) + 1); - lean_assert(!env.is_ge(l5 + 1, l6)); - lean_assert(env.is_ge(l6, l5)); - lean_assert(env.is_ge(l6, max({l1, l2, l3, l4, l5}))); - lean_assert(env.is_ge(l6, l6)); - lean_assert(!env.is_ge(l5, l4)); - lean_assert(env.is_ge(max({l1, l2, l4, l5}), max({l1, l2, l3, l4, l5}))); - lean_assert(env.is_ge(max({l4, l5}), max({l1, l2, l3}))); - lean_assert(!env.is_ge(max({l1, l2, l5}), max({l1, l2, l3, l4, l5}))); - lean_assert(!env.is_ge(max({l2, l4}), max({l1, l2, l3, l4, l5}))); - lean_assert(env.is_ge(max(l2, l3) + 1, max(l1, l1+1))); - lean_assert(env.is_ge(max(l2, l3) + 1, max(l1+2, l1+1))); - lean_assert(env.is_ge(max(l2, l3) + 1, max(l2+2, l1+1))); - lean_assert(!env.is_ge(max(l4, l5) + 1, max(l2+4, l1+1))); - lean_assert(!env.is_ge(max(l6, l5), max(l2+4, l1+1))); - lean_assert(env.is_ge(max(l6, l5), max(l2+3, l1+1))); - lean_assert(!env.is_ge(max(l6, l5), max(l2, l1+1)+3)); - lean_assert(env.is_ge(max(l6+1, l5), max(l2, l1+1)+3)); + level l1 = env->add_uvar("l1", level() + 1); + level l2 = env->add_uvar("l2", level() + 1); + level l3 = env->add_uvar("l3", max(l1, l2) + 1); + level l4 = env->add_uvar("l4", l3 + 1); + level l5 = env->add_uvar("l5", l3 + 1); + level l6 = env->add_uvar("l6", max(l4, l5) + 1); + lean_assert(!env->is_ge(l5 + 1, l6)); + lean_assert(env->is_ge(l6, l5)); + lean_assert(env->is_ge(l6, max({l1, l2, l3, l4, l5}))); + lean_assert(env->is_ge(l6, l6)); + lean_assert(!env->is_ge(l5, l4)); + lean_assert(env->is_ge(max({l1, l2, l4, l5}), max({l1, l2, l3, l4, l5}))); + lean_assert(env->is_ge(max({l4, l5}), max({l1, l2, l3}))); + lean_assert(!env->is_ge(max({l1, l2, l5}), max({l1, l2, l3, l4, l5}))); + lean_assert(!env->is_ge(max({l2, l4}), max({l1, l2, l3, l4, l5}))); + lean_assert(env->is_ge(max(l2, l3) + 1, max(l1, l1+1))); + lean_assert(env->is_ge(max(l2, l3) + 1, max(l1+2, l1+1))); + lean_assert(env->is_ge(max(l2, l3) + 1, max(l2+2, l1+1))); + lean_assert(!env->is_ge(max(l4, l5) + 1, max(l2+4, l1+1))); + lean_assert(!env->is_ge(max(l6, l5), max(l2+4, l1+1))); + lean_assert(env->is_ge(max(l6, l5), max(l2+3, l1+1))); + lean_assert(!env->is_ge(max(l6, l5), max(l2, l1+1)+3)); + lean_assert(env->is_ge(max(l6+1, l5), max(l2, l1+1)+3)); std::cout << env; } static void tst5() { environment env; - level l1 = env.add_uvar("l1", level() + 1); - level l2 = env.add_uvar("l2", level() + 1); + level l1 = env->add_uvar("l1", level() + 1); + level l2 = env->add_uvar("l2", level() + 1); std::cout << max(l1, l1) << "\n"; lean_assert(max(l1, l1) == l1); lean_assert(max(l1+1, l1+1) == l1+1); diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp index 570a2eb9a..9fe538465 100644 --- a/src/tests/kernel/metavar.cpp +++ b/src/tests/kernel/metavar.cpp @@ -235,11 +235,11 @@ static void tst13() { environment env; metavar_env menv; expr m = menv.mk_metavar(); - env.add_var("N", Type()); + env->add_var("N", Type()); expr N = Const("N"); - env.add_var("f", N >> N); + env->add_var("f", N >> N); expr f = Const("f"); - env.add_var("a", N); + env->add_var("a", N); expr a = Const("a"); expr x = Const("x"); expr F = Fun({x, N}, f(m))(a); @@ -263,13 +263,13 @@ static void tst14() { expr b = Const("b"); expr x = Const("x"); expr y = Const("y"); - env.add_var("h", Pi({N, Type()}, N >> (N >> N))); + env->add_var("h", Pi({N, Type()}, N >> (N >> N))); expr F1 = Fun({{N, Type()}, {a, N}, {f, N >> N}}, (Fun({{x, N}, {y, N}}, Eq(f(m1), y)))(a)); metavar_env menv2 = menv; menv2.assign(m1, h(Var(4), Var(1), Var(3))); normalizer norm(env); - env.add_var("M", Type()); + env->add_var("M", Type()); expr M = Const("M"); std::cout << norm(F1) << "\n"; std::cout << instantiate_metavars(norm(F1), menv2) << "\n"; @@ -295,8 +295,8 @@ static void tst15() { expr y = Const("y"); expr z = Const("z"); expr N = Const("N"); - env.add_var("N", Type()); - env.add_var("f", Type() >> Type()); + env->add_var("N", Type()); + env->add_var("f", Type() >> Type()); expr F = Fun({z, Type()}, Fun({{x, Type()}, {y, Type()}}, f(m1))(N, N)); menv.assign(m1, Var(2)); std::cout << norm(F) << "\n"; @@ -318,7 +318,7 @@ static void tst16() { expr y = Const("y"); expr z = Const("z"); expr N = Const("N"); - env.add_var("N", Type()); + env->add_var("N", Type()); expr F = Fun({z, Type()}, Fun({{x, Type()}, {y, Type()}}, m1)(N, N)); menv.assign(m1, Var(3)); std::cout << norm(F, ctx) << "\n"; @@ -341,7 +341,7 @@ static void tst17() { expr y = Const("y"); expr z = Const("z"); expr N = Const("N"); - env.add_var("N", Type()); + env->add_var("N", Type()); expr F = Fun({z, Type()}, Fun({{x, Type()}, {y, Type()}}, m1)(N, N)); metavar_env menv2 = menv; menv.assign(m1, Var(3)); @@ -377,10 +377,10 @@ static void tst18() { expr z = Const("z"); expr N = Const("N"); expr a = Const("a"); - env.add_var("N", Type()); - env.add_var("a", N); - env.add_var("g", N >> N); - env.add_var("h", N >> (N >> N)); + env->add_var("N", Type()); + env->add_var("a", N); + env->add_var("g", N >> N); + env->add_var("h", N >> (N >> N)); expr F = Fun({z, Type()}, Fun({{f, N >> N}, {y, Type()}}, m1)(Fun({x, N}, g(z, x, m2)), N)); std::cout << norm(F, ctx) << "\n"; metavar_env menv2 = menv; @@ -426,9 +426,9 @@ static void tst20() { expr N = Const("N"); expr a = Const("a"); expr b = Const("b"); - env.add_var("N", Type()); - env.add_var("a", N); - env.add_var("b", N); + env->add_var("N", Type()); + env->add_var("a", N); + env->add_var("b", N); expr F = Fun({{x, N}, {y, N}, {z, N}}, Fun({{x, N}, {y, N}}, m1)(a, b)); std::cout << norm(F) << "\n"; std::cout << norm(F, ctx) << "\n"; @@ -472,9 +472,9 @@ static void tst23() { expr N = Const("N"); expr f = Const("f"); expr a = Const("a"); - env.add_var("N", Type()); - env.add_var("f", N >> (N >> N)); - env.add_var("a", N); + env->add_var("N", Type()); + env->add_var("f", N >> (N >> N)); + env->add_var("a", N); expr x = Const("x"); expr F0 = f(Fun({x, N}, f(_, x))(a), _); expr F1 = replace_placeholders_with_metavars(F0, menv); @@ -510,9 +510,9 @@ static void tst25() { expr N = Const("N"); expr a = Const("a"); expr b = Const("b"); - env.add_var("N", Type()); - env.add_var("a", N); - env.add_var("b", N); + env->add_var("N", Type()); + env->add_var("a", N); + env->add_var("b", N); expr m = menv.mk_metavar(); expr F = m(a, b); std::cout << checker.infer_type(F, context(), &menv, &up) << "\n"; @@ -541,13 +541,13 @@ static void tst26() { expr nil = Const("nil"); expr cons = Const("cons"); expr A = Const("A"); - env.add_var("list", Type() >> Type()); - env.add_var("nil", Pi({A, Type()}, list(A))); - env.add_var("cons", Pi({A, Type()}, A >> (list(A) >> list(A)))); - env.add_var("a", Int); - env.add_var("b", Int); - env.add_var("n", Nat); - env.add_var("m", Nat); + env->add_var("list", Type() >> Type()); + env->add_var("nil", Pi({A, Type()}, list(A))); + env->add_var("cons", Pi({A, Type()}, A >> (list(A) >> list(A)))); + env->add_var("a", Int); + env->add_var("b", Int); + env->add_var("n", Nat); + env->add_var("m", Nat); expr a = Const("a"); expr b = Const("b"); expr n = Const("n"); @@ -585,9 +585,9 @@ static void tst27() { expr b = Const("b"); expr x = Const("x"); expr y = Const("y"); - env.add_var("f", Pi({A, Type()}, A >> (A >> Bool))); - env.add_var("a", Int); - env.add_var("b", Real); + env->add_var("f", Pi({A, Type()}, A >> (A >> Bool))); + env->add_var("a", Int); + env->add_var("b", Real); expr T1 = menv.mk_metavar(); expr T2 = menv.mk_metavar(); expr A1 = menv.mk_metavar(); diff --git a/src/tests/kernel/normalizer.cpp b/src/tests/kernel/normalizer.cpp index 8ee871b06..6059ac699 100644 --- a/src/tests/kernel/normalizer.cpp +++ b/src/tests/kernel/normalizer.cpp @@ -88,10 +88,10 @@ unsigned count(expr const & a) { static void tst_church_numbers() { environment env; - env.add_var("t", Type()); - env.add_var("N", Type()); - env.add_var("z", Const("N")); - env.add_var("s", Const("N")); + env->add_var("t", Type()); + env->add_var("N", Type()); + env->add_var("z", Const("N")); + env->add_var("s", Const("N")); expr N = Const("N"); expr z = Const("z"); expr s = Const("s"); @@ -120,13 +120,13 @@ static void tst_church_numbers() { static void tst1() { environment env; - env.add_var("t", Type()); + env->add_var("t", Type()); expr t = Type(); - env.add_var("f", mk_arrow(t, t)); + env->add_var("f", mk_arrow(t, t)); expr f = Const("f"); - env.add_var("a", t); + env->add_var("a", t); expr a = Const("a"); - env.add_var("b", t); + env->add_var("b", t); expr b = Const("b"); expr x = Var(0); expr y = Var(1); @@ -148,13 +148,13 @@ static void tst1() { static void tst2() { environment env; expr t = Type(); - env.add_var("f", mk_arrow(t, t)); + env->add_var("f", mk_arrow(t, t)); expr f = Const("f"); - env.add_var("a", t); + env->add_var("a", t); expr a = Const("a"); - env.add_var("b", t); + env->add_var("b", t); expr b = Const("b"); - env.add_var("h", mk_arrow(t, t)); + env->add_var("h", mk_arrow(t, t)); expr h = Const("h"); expr x = Var(0); expr y = Var(1); @@ -188,7 +188,7 @@ static void tst2() { static void tst3() { environment env = mk_toplevel(); - env.add_var("a", Bool); + env->add_var("a", Bool); expr t1 = Const("a"); expr t2 = Const("a"); expr e = Eq(t1, t2); @@ -198,7 +198,7 @@ static void tst3() { static void tst4() { environment env; - env.add_var("b", Type()); + env->add_var("b", Type()); expr t1 = mk_let("a", none_expr(), Const("b"), mk_lambda("c", Type(), Var(1)(Var(0)))); std::cout << t1 << " --> " << normalize(t1, env) << "\n"; lean_assert(normalize(t1, env) == mk_lambda("c", Type(), Const("b")(Var(0)))); @@ -215,8 +215,8 @@ static void tst5() { #if !defined(__APPLE__) && defined(LEAN_MULTI_THREAD) expr t = mk_big(18); environment env = mk_toplevel(); - env.add_var("f", Bool >> (Bool >> Bool)); - env.add_var("a", Bool); + env->add_var("f", Bool >> (Bool >> Bool)); + env->add_var("a", Bool); normalizer proc(env); chrono::milliseconds dura(50); interruptible_thread thread([&]() { diff --git a/src/tests/kernel/threads.cpp b/src/tests/kernel/threads.cpp index 0bf7e98ac..c66c670c7 100644 --- a/src/tests/kernel/threads.cpp +++ b/src/tests/kernel/threads.cpp @@ -18,10 +18,10 @@ Author: Leonardo de Moura using namespace lean; expr norm(expr const & e, environment & env) { - env.add_var("a", Int); - env.add_var("b", Int); - env.add_var("f", Int >> (Int >> Int)); - env.add_var("h", Int >> (Int >> Int)); + env->add_var("a", Int); + env->add_var("b", Int); + env->add_var("f", Int >> (Int >> Int)); + env->add_var("h", Int >> (Int >> Int)); return normalize(e, env); } @@ -35,7 +35,7 @@ static void mk(expr const & a) { h = mk_app(h, b); h = max_sharing(h); lean_assert(closed(h)); - environment env2 = env.mk_child(); + environment env2 = env->mk_child(); h = norm(h, env2); h = abstract(h, a); lean_assert(!closed(h)); diff --git a/src/tests/kernel/type_checker.cpp b/src/tests/kernel/type_checker.cpp index 7644bd5e7..1223ef7aa 100644 --- a/src/tests/kernel/type_checker.cpp +++ b/src/tests/kernel/type_checker.cpp @@ -35,8 +35,8 @@ static void tst1() { expr f = mk_pi("_", t0, t0); std::cout << infer_type(f, env) << "\n"; lean_assert(infer_type(f, env) == Type(level()+1)); - level u = env.add_uvar("u", level() + 1); - level v = env.add_uvar("v", level() + 1); + level u = env->add_uvar("u", level() + 1); + level v = env->add_uvar("v", level() + 1); expr g = mk_pi("_", Type(u), Type(v)); std::cout << infer_type(g, env) << "\n"; lean_assert(infer_type(g, env) == Type(max(u+1, v+1))); @@ -58,7 +58,7 @@ static void tst1() { static void tst2() { try{ environment env; - level l1 = env.add_uvar("l1", level() + 1); + level l1 = env->add_uvar("l1", level() + 1); expr t0 = Type(); expr t1 = Type(l1); expr F = @@ -94,7 +94,7 @@ static void tst4() { static void tst5() { environment env = mk_toplevel(); - env.add_var("P", Bool); + env->add_var("P", Bool); expr P = Const("P"); expr H = Const("H"); unsigned n = 4000; @@ -139,8 +139,8 @@ static void tst7() { static void tst8() { environment env = mk_toplevel(); - env.add_var("P", mk_arrow(Int, mk_arrow(Int, Bool))); - env.add_var("x", Int); + env->add_var("P", mk_arrow(Int, mk_arrow(Int, Bool))); + env->add_var("x", Int); expr P = Const("P"); context c; c = extend(c, "P", mk_arrow(Bool, Bool)); @@ -158,8 +158,8 @@ static void tst8() { static void tst9() { environment env = mk_toplevel(); - env.add_var("P", mk_arrow(Int, mk_arrow(Int, Bool))); - env.add_var("x", Int); + env->add_var("P", mk_arrow(Int, mk_arrow(Int, Bool))); + env->add_var("x", Int); expr P = Const("P"); context c; c = extend(c, "P", mk_arrow(Bool, Bool)); @@ -177,8 +177,8 @@ static void tst9() { static void tst10() { environment env = mk_toplevel(); - env.add_var("f", mk_arrow(Int, Int)); - env.add_var("b", Int); + env->add_var("f", mk_arrow(Int, Int)); + env->add_var("b", Int); expr f = Const("f"); expr a = Const("a"); expr b = Const("b"); @@ -187,14 +187,14 @@ static void tst10() { std::cout << t1 << " --> " << normalize(t1, env) << "\n"; expr prop = Eq(t1, t2); expr proof = Refl(Int, t1); - env.add_theorem("simp_eq", prop, proof); - std::cout << env.get_object("simp_eq").get_name() << "\n"; + env->add_theorem("simp_eq", prop, proof); + std::cout << env->get_object("simp_eq").get_name() << "\n"; } static void tst11() { environment env = mk_toplevel(); - env.add_var("f", Int >> (Int >> Int)); - env.add_var("a", Int); + env->add_var("f", Int >> (Int >> Int)); + env->add_var("a", Int); unsigned n = 1000; expr f = Const("f"); expr a = Const("a"); @@ -208,8 +208,8 @@ static void tst11() { t3 = f(t3, t3); } lean_assert(t1 != t2); - env.add_theorem("eqs1", Eq(t1, t2), Refl(Int, t1)); - env.add_theorem("eqs2", Eq(t1, t3), Refl(Int, t1)); + env->add_theorem("eqs1", Eq(t1, t2), Refl(Int, t1)); + env->add_theorem("eqs2", Eq(t1, t3), Refl(Int, t1)); } static expr mk_big(unsigned depth) { @@ -223,8 +223,8 @@ static void tst12() { #if !defined(__APPLE__) && defined(LEAN_MULTI_THREAD) expr t = mk_big(18); environment env = mk_toplevel(); - env.add_var("f", Int >> (Int >> Int)); - env.add_var("a", Int); + env->add_var("f", Int >> (Int >> Int)); + env->add_var("a", Int); type_checker checker(env); chrono::milliseconds dura(100); interruptible_thread thread([&]() { @@ -245,7 +245,7 @@ static void tst12() { static void tst13() { environment env = mk_toplevel(); - env.add_var("f", Type() >> Type()); + env->add_var("f", Type() >> Type()); expr f = Const("f"); std::cout << infer_type(f(Bool), env) << "\n"; std::cout << infer_type(f(Eq(True, False)), env) << "\n"; @@ -256,8 +256,8 @@ static void tst14() { import_all(env); expr f = Const("f"); expr a = Const("a"); - env.add_var("f", Int >> Int); - env.add_var("a", Real); + env->add_var("f", Int >> Int); + env->add_var("a", Real); expr F = f(a); type_checker checker(env); formatter fmt = mk_simple_formatter(); @@ -276,8 +276,8 @@ static void tst15() { expr A = Const("A"); expr vec1 = Const("vec1"); expr vec2 = Const("vec2"); - env.add_var("vec1", Int >> (Type() >> Type())); - env.add_var("vec2", Real >> (Type() >> Type())); + env->add_var("vec1", Int >> (Type() >> Type())); + env->add_var("vec2", Real >> (Type() >> Type())); ctx1 = extend(ctx1, "x", Int, iVal(1)); ctx1 = extend(ctx1, "f", Pi({A, Int}, vec1(A, Int))); ctx2 = extend(ctx2, "x", Real, rVal(2)); diff --git a/src/tests/library/arith.cpp b/src/tests/library/arith.cpp index e0b47f4c2..a4f6b4879 100644 --- a/src/tests/library/arith.cpp +++ b/src/tests/library/arith.cpp @@ -19,7 +19,7 @@ static void tst0() { normalizer norm(env); import_basic(env); import_arith(env); - env.add_var("n", Nat); + env->add_var("n", Nat); expr n = Const("n"); lean_assert_eq(mk_nat_type(), Nat); lean_assert_eq(norm(nMul(nVal(2), nVal(3))), nVal(6)); @@ -27,7 +27,7 @@ static void tst0() { lean_assert_eq(norm(nLe(nVal(5), nVal(3))), False); lean_assert_eq(norm(nLe(nVal(2), nVal(3))), True); lean_assert_eq(norm(nLe(n, nVal(3))), nLe(n, nVal(3))); - env.add_var("x", Real); + env->add_var("x", Real); expr x = Const("x"); lean_assert_eq(mk_real_type(), Real); lean_assert_eq(norm(rMul(rVal(2), rVal(3))), rVal(6)); @@ -36,7 +36,7 @@ static void tst0() { lean_assert_eq(norm(rLe(rVal(5), rVal(3))), False); lean_assert_eq(norm(rLe(rVal(2), rVal(3))), True); lean_assert_eq(norm(rLe(x, rVal(3))), rLe(x, rVal(3))); - env.add_var("i", Int); + env->add_var("i", Int); expr i = Const("i"); lean_assert_eq(norm(i2r(i)), i2r(i)); lean_assert_eq(norm(i2r(iVal(2))), rVal(2)); @@ -109,7 +109,7 @@ static void tst4() { static void tst5() { environment env; import_all(env); - env.add_var(name("a"), Int); + env->add_var(name("a"), Int); expr e = Eq(iVal(3), iVal(4)); std::cout << e << " --> " << normalize(e, env) << "\n"; lean_assert(normalize(e, env) == False); diff --git a/src/tests/library/elaborator/elaborator.cpp b/src/tests/library/elaborator/elaborator.cpp index ba484a4cc..419b4fcc0 100644 --- a/src/tests/library/elaborator/elaborator.cpp +++ b/src/tests/library/elaborator/elaborator.cpp @@ -28,13 +28,13 @@ static void tst1() { expr nil = Const("nil"); expr cons = Const("cons"); expr A = Const("A"); - env.add_var("list", Type() >> Type()); - env.add_var("nil", Pi({A, Type()}, list(A))); - env.add_var("cons", Pi({A, Type()}, A >> (list(A) >> list(A)))); - env.add_var("a", Int); - env.add_var("b", Int); - env.add_var("n", Nat); - env.add_var("m", Nat); + env->add_var("list", Type() >> Type()); + env->add_var("nil", Pi({A, Type()}, list(A))); + env->add_var("cons", Pi({A, Type()}, A >> (list(A) >> list(A)))); + env->add_var("a", Int); + env->add_var("b", Int); + env->add_var("n", Nat); + env->add_var("m", Nat); expr a = Const("a"); expr b = Const("b"); expr n = Const("n"); @@ -81,9 +81,9 @@ static void tst2() { type_checker checker(env); expr A = Const("A"); expr g = Const("g"); - env.add_var("g", Pi({A, Type()}, A >> A)); + env->add_var("g", Pi({A, Type()}, A >> A)); expr a = Const("a"); - env.add_var("a", Int); + env->add_var("a", Int); expr m1 = menv.mk_metavar(); expr m2 = menv.mk_metavar(); expr m3 = menv.mk_metavar(); @@ -122,9 +122,9 @@ static void tst3() { type_checker checker(env); expr A = Const("A"); expr f = Const("f"); - env.add_var("f", Pi({A, Type()}, A >> A)); + env->add_var("f", Pi({A, Type()}, A >> A)); expr a = Const("a"); - env.add_var("a", Int); + env->add_var("a", Int); expr m1 = menv.mk_metavar(); expr m2 = menv.mk_metavar(); expr m3 = menv.mk_metavar(); @@ -164,11 +164,11 @@ static void tst4() { type_checker checker(env); expr A = Const("A"); expr f = Const("f"); - env.add_var("f", Pi({A, Type()}, A >> A)); + env->add_var("f", Pi({A, Type()}, A >> A)); expr a = Const("a"); expr b = Const("b"); - env.add_var("a", Int); - env.add_var("b", Real); + env->add_var("a", Int); + env->add_var("b", Real); expr m1 = menv.mk_metavar(); expr m2 = menv.mk_metavar(); expr m3 = menv.mk_metavar(); @@ -208,11 +208,11 @@ static void tst5() { type_checker checker(env); expr A = Const("A"); expr f = Const("f"); - env.add_var("f", Pi({A, Type()}, A >> (A >> A))); + env->add_var("f", Pi({A, Type()}, A >> (A >> A))); expr a = Const("a"); expr b = Const("b"); - env.add_var("a", Int); - env.add_var("b", Real); + env->add_var("a", Int); + env->add_var("b", Real); expr m1 = menv.mk_metavar(); expr m2 = menv.mk_metavar(); expr m3 = menv.mk_metavar(); @@ -252,11 +252,11 @@ static void tst6() { expr m2 = menv.mk_metavar(); expr m3 = menv.mk_metavar(); expr m4 = menv.mk_metavar(); - env.add_var("f", Int >> (Int >> Int)); - env.add_var("a", Int); - env.add_var("b", Int); - env.add_axiom("H1", Eq(f(a, f(a, b)), a)); - env.add_axiom("H2", Eq(a, b)); + env->add_var("f", Int >> (Int >> Int)); + env->add_var("a", Int); + env->add_var("b", Int); + env->add_axiom("H1", Eq(f(a, f(a, b)), a)); + env->add_axiom("H2", Eq(a, b)); expr V = Subst(m1, m2, m3, m4, H1, H2); expr expected = Eq(f(a, f(b, b)), a); expr given = checker.infer_type(V, context(), &menv, &ucs); @@ -315,10 +315,10 @@ static void tst7() { expr a = Const("a"); expr Nat = Const("N"); expr Real = Const("R"); - env.add_var("N", Type()); - env.add_var("R", Type()); - env.add_var("F", Pi({{A, Type()}, {B, Type()}, {g, A >> B}}, A)); - env.add_var("f", Nat >> Real); + env->add_var("N", Type()); + env->add_var("R", Type()); + env->add_var("F", Pi({{A, Type()}, {B, Type()}, {g, A >> B}}, A)); + env->add_var("f", Nat >> Real); expr f = Const("f"); success(F(_, _, f), F(Nat, Real, f), env); // fails(F(_, Bool, f), env); @@ -334,17 +334,17 @@ static void tst8() { expr c = Const("c"); expr H1 = Const("H1"); expr H2 = Const("H2"); - env.add_var("a", Bool); - env.add_var("b", Bool); - env.add_var("c", Bool); - env.add_axiom("H1", Eq(a, b)); - env.add_axiom("H2", Eq(b, c)); + env->add_var("a", Bool); + env->add_var("b", Bool); + env->add_var("c", Bool); + env->add_axiom("H1", Eq(a, b)); + env->add_axiom("H2", Eq(b, c)); success(Trans(_, _, _, _, H1, H2), Trans(Bool, a, b, c, H1, H2), env); success(Trans(_, _, _, _, Symm(_, _, _, H2), Symm(_, _, _, H1)), Trans(Bool, c, b, a, Symm(Bool, b, c, H2), Symm(Bool, a, b, H1)), env); success(Symm(_, _, _, Trans(_, _ , _ , _ , Symm(_, _, _, H2), Symm(_, _, _, H1))), Symm(Bool, c, a, Trans(Bool, c, b, a, Symm(Bool, b, c, H2), Symm(Bool, a, b, H1))), env); - env.add_axiom("H3", a); + env->add_axiom("H3", a); expr H3 = Const("H3"); success(EqTIntro(_, EqMP(_, _, Symm(_, _, _, Trans(_, _, _, _, Symm(_, _, _, H2), Symm(_, _, _, H1))), H3)), EqTIntro(c, EqMP(a, c, Symm(Bool, c, a, Trans(Bool, c, b, a, Symm(Bool, b, c, H2), Symm(Bool, a, b, H1))), H3)), @@ -356,25 +356,25 @@ static void tst9() { environment env; import_all(env); expr Nat = Const("N"); - env.add_var("N", Type()); - env.add_var("vec", Nat >> Type()); + env->add_var("N", Type()); + env->add_var("vec", Nat >> Type()); expr n = Const("n"); expr vec = Const("vec"); - env.add_var("f", Pi({n, Nat}, vec(n) >> Nat)); + env->add_var("f", Pi({n, Nat}, vec(n) >> Nat)); expr f = Const("f"); expr a = Const("a"); expr b = Const("b"); expr H = Const("H"); expr fact = Const("fact"); - env.add_var("a", Nat); - env.add_var("b", Nat); - env.add_definition("fact", Bool, Eq(a, b)); - env.add_axiom("H", fact); + env->add_var("a", Nat); + env->add_var("b", Nat); + env->add_definition("fact", Bool, Eq(a, b)); + env->add_axiom("H", fact); success(Congr2(_, _, _, _, f, H), Congr2(Nat, Fun({n, Nat}, vec(n) >> Nat), a, b, f, H), env); - env.add_var("g", Pi({n, Nat}, vec(n) >> Nat)); + env->add_var("g", Pi({n, Nat}, vec(n) >> Nat)); expr g = Const("g"); - env.add_axiom("H2", Eq(f, g)); + env->add_axiom("H2", Eq(f, g)); expr H2 = Const("H2"); success(Congr(_, _, _, _, _, _, H2, H), Congr(Nat, Fun({n, Nat}, vec(n) >> Nat), f, g, a, b, H2, H), env); @@ -388,13 +388,13 @@ static void tst10() { environment env; import_all(env); expr Nat = Const("N"); - env.add_var("N", Type()); + env->add_var("N", Type()); expr R = Const("R"); - env.add_var("R", Type()); - env.add_var("a", Nat); + env->add_var("R", Type()); + env->add_var("a", Nat); expr a = Const("a"); expr f = Const("f"); - env.add_var("f", Nat >> ((R >> Nat) >> R)); + env->add_var("f", Nat >> ((R >> Nat) >> R)); expr x = Const("x"); expr y = Const("y"); expr z = Const("z"); @@ -418,9 +418,9 @@ static void tst11() { expr f = Const("f"); expr g = Const("g"); expr Nat = Const("N"); - env.add_var("N", Type()); - env.add_var("f", Pi({{A, Type()}, {a, A}, {b, A}}, A)); - env.add_var("g", Nat >> Nat); + env->add_var("N", Type()); + env->add_var("f", Pi({{A, Type()}, {a, A}, {b, A}}, A)); + env->add_var("g", Nat >> Nat); success(Fun({{a, _}, {b, _}}, g(f(_, a, b))), Fun({{a, Nat}, {b, Nat}}, g(f(Nat, a, b))), env); } @@ -437,11 +437,11 @@ static void tst12() { expr f = Const("f"); expr l = Const("l"); expr a = Const("a"); - env.add_var("N", Type()); - env.add_var("list", Type() >> Type()); - env.add_var("nil", Pi({A, Type()}, lst(A))); - env.add_var("cons", Pi({{A, Type()}, {a, A}, {l, lst(A)}}, lst(A))); - env.add_var("f", lst(N >> N) >> Bool); + env->add_var("N", Type()); + env->add_var("list", Type() >> Type()); + env->add_var("nil", Pi({A, Type()}, lst(A))); + env->add_var("cons", Pi({{A, Type()}, {a, A}, {l, lst(A)}}, lst(A))); + env->add_var("f", lst(N >> N) >> Bool); success(Fun({a, _}, f(cons(_, a, cons(_, a, nil(_))))), Fun({a, N >> N}, f(cons(N >> N, a, cons(N >> N, a, nil(N >> N))))), env); } @@ -454,7 +454,7 @@ static void tst13() { expr A = Const("A"); expr x = Const("x"); expr f = Const("f"); - env.add_var("f", Pi({B, Type()}, B >> B)); + env->add_var("f", Pi({B, Type()}, B >> B)); success(Fun({{A, Type()}, {B, Type()}, {x, _}}, f(B, x)), Fun({{A, Type()}, {B, Type()}, {x, B}}, f(B, x)), env); fails(Fun({{x, _}, {A, Type()}}, f(A, x)), env); @@ -479,8 +479,8 @@ static void tst14() { expr g = Const("g"); expr x = Const("x"); expr y = Const("y"); - env.add_var("N", Type()); - env.add_var("f", Pi({A, Type()}, A >> A)); + env->add_var("N", Type()); + env->add_var("f", Pi({A, Type()}, A >> A)); expr N = Const("N"); success(Fun({g, Pi({A, Type()}, A >> (A >> Bool))}, g(_, True, False)), Fun({g, Pi({A, Type()}, A >> (A >> Bool))}, g(Bool, True, False)), @@ -520,7 +520,7 @@ static void tst15() { expr a = Const("a"); expr b = Const("b"); expr eq = Const("my_eq"); - env.add_var("my_eq", Pi({A, Type()}, A >> (A >> Bool))); + env->add_var("my_eq", Pi({A, Type()}, A >> (A >> Bool))); success(Fun({{A, Type()}, {B, Type()}, {a, _}, {b, B}}, eq(_, a, b)), Fun({{A, Type()}, {B, Type()}, {a, B}, {b, B}}, eq(B, a, b)), env); success(Fun({{A, Type()}, {B, Type()}, {a, _}, {b, A}}, eq(_, a, b)), @@ -545,9 +545,9 @@ static void tst16() { expr c = Const("c"); expr H1 = Const("H1"); expr H2 = Const("H2"); - env.add_var("a", Bool); - env.add_var("b", Bool); - env.add_var("c", Bool); + env->add_var("a", Bool); + env->add_var("b", Bool); + env->add_var("c", Bool); success(Fun({{H1, Eq(a, b)}, {H2, Eq(b, c)}}, Trans(_, _, _, _, H1, H2)), Fun({{H1, Eq(a, b)}, {H2, Eq(b, c)}}, @@ -583,7 +583,7 @@ void tst17() { expr a = Const("a"); expr b = Const("b"); expr eq = Const("my_eq"); - env.add_var("my_eq", Pi({A, Type(level()+1)}, A >> (A >> Bool))); + env->add_var("my_eq", Pi({A, Type(level()+1)}, A >> (A >> Bool))); success(eq(_, Fun({{A, Type()}, {a, _}}, a), Fun({{B, Type()}, {b, B}}, b)), eq(Pi({A, Type()}, A >> A), Fun({{A, Type()}, {a, A}}, a), Fun({{B, Type()}, {b, B}}, b)), env); @@ -597,7 +597,7 @@ void tst18() { expr h = Const("h"); expr f = Const("f"); expr a = Const("a"); - env.add_var("h", Pi({A, Type()}, A) >> Bool); + env->add_var("h", Pi({A, Type()}, A) >> Bool); success(Fun({{f, Pi({A, Type()}, _)}, {a, Bool}}, h(f)), Fun({{f, Pi({A, Type()}, A)}, {a, Bool}}, h(f)), env); @@ -615,10 +615,10 @@ void tst19() { expr g = Const("g"); expr h = Const("h"); expr D = Const("D"); - env.add_var("R", Type() >> Bool); - env.add_var("r", Pi({A, Type()}, R(A))); - env.add_var("h", Pi({A, Type()}, R(A)) >> Bool); - env.add_var("my_eq", Pi({A, Type(level()+1)}, A >> (A >> Bool))); + env->add_var("R", Type() >> Bool); + env->add_var("r", Pi({A, Type()}, R(A))); + env->add_var("h", Pi({A, Type()}, R(A)) >> Bool); + env->add_var("my_eq", Pi({A, Type(level()+1)}, A >> (A >> Bool))); success(Let({{f, Fun({A, Type()}, r(_))}, {g, Fun({A, Type()}, r(_))}, {D, Fun({A, Type()}, eq(_, f(A), g(_)))}}, @@ -636,11 +636,11 @@ void tst20() { metavar_env menv; expr N = Const("N"); expr M = Const("M"); - env.add_var("N", Type()); - env.add_var("M", Type()); - env.add_var("f", N >> (M >> M)); - env.add_var("a", N); - env.add_var("b", M); + env->add_var("N", Type()); + env->add_var("M", Type()); + env->add_var("f", N >> (M >> M)); + env->add_var("a", N); + env->add_var("b", M); expr f = Const("f"); expr x = Const("x"); expr a = Const("a"); @@ -669,10 +669,10 @@ void tst21() { metavar_env menv; expr N = Const("N"); expr M = Const("M"); - env.add_var("N", Type()); - env.add_var("f", N >> (Bool >> N)); - env.add_var("a", N); - env.add_var("b", N); + env->add_var("N", Type()); + env->add_var("f", N >> (Bool >> N)); + env->add_var("a", N); + env->add_var("b", N); expr f = Const("f"); expr x = Const("x"); expr a = Const("a"); @@ -700,10 +700,10 @@ void tst22() { import_all(env); metavar_env menv; expr N = Const("N"); - env.add_var("N", Type()); - env.add_var("f", N >> (Int >> N)); - env.add_var("a", N); - env.add_var("b", N); + env->add_var("N", Type()); + env->add_var("f", N >> (Int >> N)); + env->add_var("a", N); + env->add_var("b", N); expr m1 = menv.mk_metavar(); expr m2 = menv.mk_metavar(); expr m3 = menv.mk_metavar(); @@ -735,8 +735,8 @@ void tst23() { import_all(env); metavar_env menv; expr N = Const("N"); - env.add_var("N", Type()); - env.add_var("f", N >> (N >> N)); + env->add_var("N", Type()); + env->add_var("f", N >> (N >> N)); expr x = Const("x"); expr y = Const("y"); expr f = Const("f"); @@ -765,8 +765,8 @@ void tst24() { import_all(env); metavar_env menv; expr N = Const("N"); - env.add_var("N", Type()); - env.add_var("f", N >> (N >> N)); + env->add_var("N", Type()); + env->add_var("f", N >> (N >> N)); expr f = Const("f"); expr m1 = menv.mk_metavar(); expr l = f(f(m1)); @@ -785,8 +785,8 @@ void tst25() { import_all(env); metavar_env menv; expr N = Const("N"); - env.add_var("N", Type()); - env.add_var("f", N >> (N >> N)); + env->add_var("N", Type()); + env->add_var("f", N >> (N >> N)); expr x = Const("x"); expr y = Const("y"); expr f = Const("f"); @@ -824,9 +824,9 @@ void tst26() { type_checker checker(env); expr A = Const("A"); expr g = Const("g"); - env.add_var("g", Pi({A, TypeU}, A >> A)); + env->add_var("g", Pi({A, TypeU}, A >> A)); expr a = Const("a"); - env.add_var("a", Type(level()+1)); + env->add_var("a", Type(level()+1)); expr m1 = menv.mk_metavar(); expr F = Eq(g(m1, a), a); std::cout << F << "\n"; @@ -857,9 +857,9 @@ void tst27() { expr f = Const("f"); expr a = Const("a"); expr eq = Const("my_eq"); - env.add_var("my_eq", Pi({A, TypeU}, A >> (A >> Bool))); - env.add_var("g", Pi({A, TypeU}, A >> A)); - env.add_var("a", TypeM); + env->add_var("my_eq", Pi({A, TypeU}, A >> (A >> Bool))); + env->add_var("g", Pi({A, TypeU}, A >> A)); + env->add_var("a", TypeM); expr m1 = menv.mk_metavar(); expr m2 = menv.mk_metavar(); expr m3 = menv.mk_metavar(); diff --git a/src/tests/library/formatter.cpp b/src/tests/library/formatter.cpp index 9261d2075..1fe7e9552 100644 --- a/src/tests/library/formatter.cpp +++ b/src/tests/library/formatter.cpp @@ -21,7 +21,7 @@ static void check(format const & f, char const * expected) { static void tst1() { environment env; - env.add_var("N", Type()); + env->add_var("N", Type()); formatter fmt = mk_simple_formatter(); check(fmt(env), "Variable N : Type\n"); expr f = Const("f"); @@ -31,7 +31,7 @@ static void tst1() { expr N = Const("N"); expr F = Fun({x, Pi({x, N}, x >> x)}, Let({y, f(a)}, f(Eq(x, f(y, a))))); check(fmt(F), "fun x : (Pi x : N, (x -> x)), (let y := f a in (f (x == (f y a))))"); - check(fmt(env.get_object("N")), "Variable N : Type"); + check(fmt(env->get_object("N")), "Variable N : Type"); context ctx; ctx = extend(ctx, "x", f(a)); ctx = extend(ctx, "y", f(Var(0), N >> N)); diff --git a/src/tests/library/rewriter/rewriter.cpp b/src/tests/library/rewriter/rewriter.cpp index 5c13888e6..071efb071 100644 --- a/src/tests/library/rewriter/rewriter.cpp +++ b/src/tests/library/rewriter/rewriter.cpp @@ -38,9 +38,9 @@ static void theorem_rewriter1_tst() { expr add_comm_thm_body = Const("ADD_COMM"); environment env = mk_toplevel(); - env.add_var("a", Nat); - env.add_var("b", Nat); - env.add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z + env->add_var("a", Nat); + env->add_var("b", Nat); + env->add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z // Rewriting rewriter add_comm_thm_rewriter = mk_theorem_rewriter(add_comm_thm_type, add_comm_thm_body); @@ -54,7 +54,7 @@ static void theorem_rewriter1_tst() { lean_assert_eq(concl, mk_eq(a_plus_b, b_plus_a)); lean_assert_eq(proof, Const("ADD_COMM")(a, b)); - env.add_theorem("New_theorem1", concl, proof); + env->add_theorem("New_theorem1", concl, proof); } static void theorem_rewriter2_tst() { @@ -70,8 +70,8 @@ static void theorem_rewriter2_tst() { expr add_id_thm_body = Const("ADD_ID"); environment env = mk_toplevel(); - env.add_var("a", Nat); - env.add_axiom("ADD_ID", add_id_thm_type); // ADD_ID : Pi (x : N), x = x + 0 + env->add_var("a", Nat); + env->add_axiom("ADD_ID", add_id_thm_type); // ADD_ID : Pi (x : N), x = x + 0 // Rewriting rewriter add_id_thm_rewriter = mk_theorem_rewriter(add_id_thm_type, add_id_thm_body); @@ -85,7 +85,7 @@ static void theorem_rewriter2_tst() { lean_assert_eq(concl, mk_eq(a_plus_zero, a)); lean_assert_eq(proof, Const("ADD_ID")(a)); - env.add_theorem("New_theorem2", concl, proof); + env->add_theorem("New_theorem2", concl, proof); } static void then_rewriter1_tst() { @@ -108,9 +108,9 @@ static void then_rewriter1_tst() { expr add_id_thm_body = Const("ADD_ID"); environment env = mk_toplevel(); - env.add_var("a", Nat); - env.add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z - env.add_axiom("ADD_ID", add_id_thm_type); // ADD_ID : Pi (x : N), x = x + 0 + env->add_var("a", Nat); + env->add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z + env->add_axiom("ADD_ID", add_id_thm_type); // ADD_ID : Pi (x : N), x = x + 0 // Rewriting rewriter add_comm_thm_rewriter = mk_theorem_rewriter(add_comm_thm_type, add_comm_thm_body); @@ -129,7 +129,7 @@ static void then_rewriter1_tst() { lean_assert(proof == Trans(Nat, zero_plus_a, a_plus_zero, a, Const("ADD_COMM")(zero, a), Const("ADD_ID")(a))); - env.add_theorem("New_theorem3", concl, proof); + env->add_theorem("New_theorem3", concl, proof); } static void then_rewriter2_tst() { @@ -164,10 +164,10 @@ static void then_rewriter2_tst() { expr add_id_thm_body = Const("ADD_ID"); environment env = mk_toplevel(); - env.add_var("a", Nat); - env.add_axiom("ADD_ASSOC", add_assoc_thm_type); // ADD_ASSOC : Pi (x, y, z : N), x + (y + z) = (x + y) + z - env.add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z - env.add_axiom("ADD_ID", add_id_thm_type); // ADD_ID : Pi (x : N), x = x + 0 + env->add_var("a", Nat); + env->add_axiom("ADD_ASSOC", add_assoc_thm_type); // ADD_ASSOC : Pi (x, y, z : N), x + (y + z) = (x + y) + z + env->add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z + env->add_axiom("ADD_ID", add_id_thm_type); // ADD_ID : Pi (x : N), x = x + 0 // Rewriting rewriter add_assoc_thm_rewriter = mk_theorem_rewriter(add_assoc_thm_type, add_assoc_thm_body); @@ -194,7 +194,7 @@ static void then_rewriter2_tst() { Const("ADD_COMM")(zero, a)), Const("ADD_ID")(a))); - env.add_theorem("New_theorem4", concl, proof); + env->add_theorem("New_theorem4", concl, proof); } static void orelse_rewriter1_tst() { @@ -223,9 +223,9 @@ static void orelse_rewriter1_tst() { expr add_id_thm_body = Const("ADD_ID"); environment env = mk_toplevel(); - env.add_var("a", Nat); - env.add_var("b", Nat); - env.add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z + env->add_var("a", Nat); + env->add_var("b", Nat); + env->add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z // Rewriting rewriter add_assoc_thm_rewriter = mk_theorem_rewriter(add_assoc_thm_type, add_assoc_thm_body); @@ -246,7 +246,7 @@ static void orelse_rewriter1_tst() { lean_assert_eq(concl, mk_eq(a_plus_b, b_plus_a)); lean_assert_eq(proof, Const("ADD_COMM")(a, b)); - env.add_theorem("New_theorem5", concl, proof); + env->add_theorem("New_theorem5", concl, proof); } static void orelse_rewriter2_tst() { @@ -270,10 +270,10 @@ static void orelse_rewriter2_tst() { expr add_id_thm_body = Const("ADD_ID"); environment env = mk_toplevel(); - env.add_var("a", Nat); - env.add_var("b", Nat); - env.add_axiom("ADD_ASSOC", add_assoc_thm_type); - env.add_axiom("ADD_ID", add_id_thm_type); + env->add_var("a", Nat); + env->add_var("b", Nat); + env->add_axiom("ADD_ASSOC", add_assoc_thm_type); + env->add_axiom("ADD_ID", add_id_thm_type); // Rewriting rewriter add_assoc_thm_rewriter = mk_theorem_rewriter(add_assoc_thm_type, add_assoc_thm_body); @@ -319,9 +319,9 @@ static void try_rewriter1_tst() { expr add_id_thm_body = Const("ADD_ID"); environment env = mk_toplevel(); - env.add_var("a", Nat); - env.add_var("b", Nat); - env.add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z + env->add_var("a", Nat); + env->add_var("b", Nat); + env->add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z // Rewriting rewriter add_assoc_thm_rewriter = mk_theorem_rewriter(add_assoc_thm_type, add_assoc_thm_body); @@ -341,7 +341,7 @@ static void try_rewriter1_tst() { lean_assert_eq(concl, mk_eq(a_plus_b, a_plus_b)); lean_assert_eq(proof, Const("Refl")(Nat, a_plus_b)); - env.add_theorem("New_theorem6", concl, proof); + env->add_theorem("New_theorem6", concl, proof); } static void try_rewriter2_tst() { @@ -370,9 +370,9 @@ static void try_rewriter2_tst() { expr add_id_thm_body = Const("ADD_ID"); environment env = mk_toplevel(); - env.add_var("a", Nat); - env.add_var("b", Nat); - env.add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z + env->add_var("a", Nat); + env->add_var("b", Nat); + env->add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z // Rewriting rewriter add_assoc_thm_rewriter = mk_theorem_rewriter(add_assoc_thm_type, add_assoc_thm_body); @@ -393,7 +393,7 @@ static void try_rewriter2_tst() { lean_assert_eq(concl, mk_eq(a_plus_b, b_plus_a)); lean_assert_eq(proof, Const("ADD_COMM")(a, b)); - env.add_theorem("try2", concl, proof); + env->add_theorem("try2", concl, proof); } static void app_rewriter1_tst() { @@ -416,13 +416,13 @@ static void app_rewriter1_tst() { expr add_comm_thm_body = Const("ADD_COMM"); environment env = mk_toplevel(); - env.add_var("f1", Nat >> Nat); - env.add_var("f2", Nat >> (Nat >> Nat)); - env.add_var("f3", Nat >> (Nat >> (Nat >> Nat))); - env.add_var("f4", Nat >> (Nat >> (Nat >> (Nat >> Nat)))); - env.add_var("a", Nat); - env.add_var("b", Nat); - env.add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z + env->add_var("f1", Nat >> Nat); + env->add_var("f2", Nat >> (Nat >> Nat)); + env->add_var("f3", Nat >> (Nat >> (Nat >> Nat))); + env->add_var("f4", Nat >> (Nat >> (Nat >> (Nat >> Nat)))); + env->add_var("a", Nat); + env->add_var("b", Nat); + env->add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z // Rewriting rewriter add_comm_thm_rewriter = mk_theorem_rewriter(add_comm_thm_type, add_comm_thm_body); @@ -440,7 +440,7 @@ static void app_rewriter1_tst() { << "Proof = " << proof << std::endl; lean_assert_eq(concl, mk_eq(v, f1(nVal(0)))); lean_assert_eq(proof, Refl(Nat, f1(nVal(0)))); - env.add_theorem("app_rewriter1", concl, proof); + env->add_theorem("app_rewriter1", concl, proof); cout << "====================================================" << std::endl; v = f1(a_plus_b); result = app_try_comm_rewriter(env, ctx, v); @@ -451,7 +451,7 @@ static void app_rewriter1_tst() { lean_assert_eq(concl, mk_eq(v, f1(b_plus_a))); lean_assert_eq(proof, Const("Congr2")(Nat, Fun(name("_"), Nat, Nat), a_plus_b, b_plus_a, f1, Const("ADD_COMM")(a, b))); - env.add_theorem("app_rewriter2", concl, proof); + env->add_theorem("app_rewriter2", concl, proof); cout << "====================================================" << std::endl; v = f4(nVal(0), a_plus_b, nVal(0), b_plus_a); result = app_try_comm_rewriter(env, ctx, v); @@ -471,7 +471,7 @@ static void app_rewriter1_tst() { a_plus_b, b_plus_a, f4(zero), Const("ADD_COMM")(a, b))), Const("ADD_COMM")(b, a))); - env.add_theorem("app_rewriter3", concl, proof); + env->add_theorem("app_rewriter3", concl, proof); } static void repeat_rewriter1_tst() { @@ -506,10 +506,10 @@ static void repeat_rewriter1_tst() { expr add_id_thm_body = Const("ADD_ID"); environment env = mk_toplevel(); - env.add_var("a", Nat); - env.add_axiom("ADD_ASSOC", add_assoc_thm_type); // ADD_ASSOC : Pi (x, y, z : N), x + (y + z) = (x + y) + z - env.add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z - env.add_axiom("ADD_ID", add_id_thm_type); // ADD_ID : Pi (x : N), x = x + 0 + env->add_var("a", Nat); + env->add_axiom("ADD_ASSOC", add_assoc_thm_type); // ADD_ASSOC : Pi (x, y, z : N), x + (y + z) = (x + y) + z + env->add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z + env->add_axiom("ADD_ID", add_id_thm_type); // ADD_ID : Pi (x : N), x = x + 0 // Rewriting rewriter add_assoc_thm_rewriter = mk_theorem_rewriter(add_assoc_thm_type, add_assoc_thm_body); @@ -529,7 +529,7 @@ static void repeat_rewriter1_tst() { cout << " " << concl << " := " << proof << std::endl; lean_assert_eq(concl, mk_eq(zero_plus_a_plus_zero, a)); - env.add_theorem("repeat_thm1", concl, proof); + env->add_theorem("repeat_thm1", concl, proof); } static void repeat_rewriter2_tst() { @@ -564,10 +564,10 @@ static void repeat_rewriter2_tst() { expr add_id_thm_body = Const("ADD_ID"); environment env = mk_toplevel(); - env.add_var("a", Nat); - env.add_axiom("ADD_ASSOC", add_assoc_thm_type); // ADD_ASSOC : Pi (x, y, z : N), x + (y + z) = (x + y) + z - env.add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z - env.add_axiom("ADD_ID", add_id_thm_type); // ADD_ID : Pi (x : N), x = x + 0 + env->add_var("a", Nat); + env->add_axiom("ADD_ASSOC", add_assoc_thm_type); // ADD_ASSOC : Pi (x, y, z : N), x + (y + z) = (x + y) + z + env->add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z + env->add_axiom("ADD_ID", add_id_thm_type); // ADD_ID : Pi (x : N), x = x + 0 // Rewriting rewriter add_assoc_thm_rewriter = mk_theorem_rewriter(add_assoc_thm_type, add_assoc_thm_body); @@ -588,7 +588,7 @@ static void repeat_rewriter2_tst() { cout << " " << concl << " := " << proof << std::endl; lean_assert_eq(concl, mk_eq(zero_plus_a_plus_zero, a)); - env.add_theorem("repeat_thm2", concl, proof); + env->add_theorem("repeat_thm2", concl, proof); } static void depth_rewriter1_tst() { @@ -611,13 +611,13 @@ static void depth_rewriter1_tst() { expr add_comm_thm_body = Const("ADD_COMM"); environment env = mk_toplevel(); - env.add_var("f1", Nat >> Nat); - env.add_var("f2", Nat >> (Nat >> Nat)); - env.add_var("f3", Nat >> (Nat >> (Nat >> Nat))); - env.add_var("f4", Nat >> (Nat >> (Nat >> (Nat >> Nat)))); - env.add_var("a", Nat); - env.add_var("b", Nat); - env.add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z + env->add_var("f1", Nat >> Nat); + env->add_var("f2", Nat >> (Nat >> Nat)); + env->add_var("f3", Nat >> (Nat >> (Nat >> Nat))); + env->add_var("f4", Nat >> (Nat >> (Nat >> (Nat >> Nat)))); + env->add_var("a", Nat); + env->add_var("b", Nat); + env->add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z // Rewriting rewriter add_comm_thm_rewriter = mk_theorem_rewriter(add_comm_thm_type, add_comm_thm_body); @@ -634,7 +634,7 @@ static void depth_rewriter1_tst() { cout << "Concl = " << concl << std::endl << "Proof = " << proof << std::endl; lean_assert_eq(concl, mk_eq(v, nAdd(f3(a, b, nAdd(b, a)), f1(nAdd(b, a))))); - env.add_theorem("depth_rewriter1", concl, proof); + env->add_theorem("depth_rewriter1", concl, proof); cout << "====================================================" << std::endl; } @@ -658,13 +658,13 @@ static void lambda_rewriter1_tst() { expr add_comm_thm_body = Const("ADD_COMM"); environment env = mk_toplevel(); - env.add_var("f1", Nat >> Nat); - env.add_var("f2", Nat >> (Nat >> Nat)); - env.add_var("f3", Nat >> (Nat >> (Nat >> Nat))); - env.add_var("f4", Nat >> (Nat >> (Nat >> (Nat >> Nat)))); - env.add_var("a", Nat); - env.add_var("b", Nat); - env.add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z + env->add_var("f1", Nat >> Nat); + env->add_var("f2", Nat >> (Nat >> Nat)); + env->add_var("f3", Nat >> (Nat >> (Nat >> Nat))); + env->add_var("f4", Nat >> (Nat >> (Nat >> (Nat >> Nat)))); + env->add_var("a", Nat); + env->add_var("b", Nat); + env->add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z // Rewriting rewriter add_comm_thm_rewriter = mk_theorem_rewriter(add_comm_thm_type, add_comm_thm_body); @@ -679,7 +679,7 @@ static void lambda_rewriter1_tst() { cout << "Concl = " << concl << std::endl << "Proof = " << proof << std::endl; lean_assert_eq(concl, mk_eq(v, mk_lambda("x", Nat, nAdd(a, b)))); - env.add_theorem("lambda_rewriter1", concl, proof); + env->add_theorem("lambda_rewriter1", concl, proof); cout << "====================================================" << std::endl; } @@ -703,13 +703,13 @@ static void lambda_rewriter2_tst() { expr add_comm_thm_body = Const("ADD_COMM"); environment env = mk_toplevel(); - env.add_var("f1", Nat >> Nat); - env.add_var("f2", Nat >> (Nat >> Nat)); - env.add_var("f3", Nat >> (Nat >> (Nat >> Nat))); - env.add_var("f4", Nat >> (Nat >> (Nat >> (Nat >> Nat)))); - env.add_var("a", Nat); - env.add_var("b", Nat); - env.add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z + env->add_var("f1", Nat >> Nat); + env->add_var("f2", Nat >> (Nat >> Nat)); + env->add_var("f3", Nat >> (Nat >> (Nat >> Nat))); + env->add_var("f4", Nat >> (Nat >> (Nat >> (Nat >> Nat)))); + env->add_var("a", Nat); + env->add_var("b", Nat); + env->add_axiom("ADD_COMM", add_comm_thm_type); // ADD_COMM : Pi (x, y: N), x + y = y + z // Rewriting rewriter add_comm_thm_rewriter = mk_theorem_rewriter(add_comm_thm_type, add_comm_thm_body); @@ -725,7 +725,7 @@ static void lambda_rewriter2_tst() { cout << "Concl = " << concl << std::endl << "Proof = " << proof << std::endl; lean_assert_eq(concl, mk_eq(v, mk_lambda("x", Nat, nAdd(a, Var(0))))); - env.add_theorem("lambda_rewriter2", concl, proof); + env->add_theorem("lambda_rewriter2", concl, proof); cout << "====================================================" << std::endl; } diff --git a/src/tests/library/tactic/tactic.cpp b/src/tests/library/tactic/tactic.cpp index d24795d5a..46e50d6ed 100644 --- a/src/tests/library/tactic/tactic.cpp +++ b/src/tests/library/tactic/tactic.cpp @@ -18,7 +18,7 @@ Author: Leonardo de Moura using namespace lean; tactic loop_tactic() { - return mk_tactic1([=](environment const &, io_state const &, proof_state const & s) -> proof_state { + return mk_tactic1([=](ro_environment const &, io_state const &, proof_state const & s) -> proof_state { while (true) { check_interrupted(); } @@ -27,21 +27,21 @@ tactic loop_tactic() { } tactic set_tactic(atomic * flag) { - return mk_tactic1([=](environment const &, io_state const &, proof_state const & s) -> proof_state { + return mk_tactic1([=](ro_environment const &, io_state const &, proof_state const & s) -> proof_state { *flag = true; return s; }); } tactic show_opts_tactic() { - return mk_tactic1([=](environment const &, io_state const & io, proof_state const & s) -> proof_state { + return mk_tactic1([=](ro_environment const &, io_state const & io, proof_state const & s) -> proof_state { io.get_diagnostic_channel() << "options: " << io.get_options() << "\n"; io.get_diagnostic_channel().get_stream().flush(); return s; }); } -static void check_failure(tactic t, environment const & env, io_state const & io, context const & ctx, expr const & ty) { +static void check_failure(tactic t, ro_environment const & env, io_state const & io, context const & ctx, expr const & ty) { solve_result r(t.solve(env, io, ctx, ty)); lean_assert(r.kind() == solve_result_kind::Failure); } @@ -50,8 +50,8 @@ static void tst1() { environment env; io_state io(options(), mk_simple_formatter()); import_all(env); - env.add_var("p", Bool); - env.add_var("q", Bool); + env->add_var("p", Bool); + env->add_var("q", Bool); expr p = Const("p"); expr q = Const("q"); context ctx; @@ -95,12 +95,12 @@ static void tst1() { (trace_tactic("hello3.1") || trace_tactic("hello3.2")) << assumption_tactic()).solve(env, io, ctx, q).get_proof() << "\n"; std::cout << "------------------\n"; - std::cout << "proof 2: " << then(cond([](environment const &, io_state const &, proof_state const &) { return true; }, + std::cout << "proof 2: " << then(cond([](ro_environment const &, io_state const &, proof_state const &) { return true; }, trace_tactic("then branch.1") + trace_tactic("then branch.2"), trace_tactic("else branch")), t).solve(env, io, ctx, q).get_proof() << "\n"; - std::cout << "proof 2: " << then(when([](environment const &, io_state const &, proof_state const &) { return true; }, + std::cout << "proof 2: " << then(when([](ro_environment const &, io_state const &, proof_state const &) { return true; }, trace_tactic("when branch.1") + trace_tactic("when branch.2")), t).solve(env, io, ctx, q).get_proof() << "\n"; std::cout << "------------------\n"; @@ -116,10 +116,10 @@ static void tst2() { environment env; io_state io(options(), mk_simple_formatter()); import_all(env); - env.add_var("p", Bool); - env.add_var("q", Bool); - env.add_var("r", Bool); - env.add_var("s", Bool); + env->add_var("p", Bool); + env->add_var("q", Bool); + env->add_var("r", Bool); + env->add_var("s", Bool); expr p = Const("p"); expr q = Const("q"); expr r = Const("r"); @@ -140,7 +140,7 @@ static void tst2() { // Print proof std::cout << pr << "\n"; // Check whether the proof is correct or not. - std::cout << env.infer_type(pr) << "\n"; + std::cout << env->infer_type(pr) << "\n"; } int main() { diff --git a/src/tests/library/type_inferer.cpp b/src/tests/library/type_inferer.cpp index 443fed6be..2a8f925f3 100644 --- a/src/tests/library/type_inferer.cpp +++ b/src/tests/library/type_inferer.cpp @@ -31,7 +31,7 @@ static void tst1() { expr a = Const("a"); expr b = Const("b"); expr A = Const("A"); - env.add_var("f", Int >> (Int >> Int)); + env->add_var("f", Int >> (Int >> Int)); lean_assert(type_of(f(a, a)) == Int); lean_assert(type_of(f(a)) == Int >> Int); lean_assert(is_bool(type_of(And(a, f(a))))); @@ -42,7 +42,7 @@ static void tst1() { lean_assert(type_of(Pi({a, Type()}, Type(level() + 2))) == Type(level() + 3)); lean_assert(type_of(Pi({a, Type(level()+4)}, Type(level() + 2))) == Type(level() + 5)); lean_assert(type_of(Pi({a, Int}, Bool)) == Type()); - env.add_var("g", Pi({A, Type()}, A >> A)); + env->add_var("g", Pi({A, Type()}, A >> A)); lean_assert(type_of(g(Int, a)) == Int); lean_assert(type_of(g(Fun({a, Type()}, a)(Int), a)) == Fun({a, Type()}, a)(Int)); } @@ -82,8 +82,8 @@ static void tst3() { expr A = Const("A"); expr vec1 = Const("vec1"); expr vec2 = Const("vec2"); - env.add_var("vec1", Int >> (Type() >> Type())); - env.add_var("vec2", Real >> (Type() >> Type())); + env->add_var("vec1", Int >> (Type() >> Type())); + env->add_var("vec2", Real >> (Type() >> Type())); ctx1 = extend(ctx1, "x", Int, iVal(1)); ctx1 = extend(ctx1, "f", Pi({A, Int}, vec1(A, Int))); ctx2 = extend(ctx2, "x", Real, rVal(2)); @@ -113,13 +113,13 @@ static void tst4() { expr nil = Const("nil"); expr cons = Const("cons"); expr A = Const("A"); - env.add_var("list", Type() >> Type()); - env.add_var("nil", Pi({A, Type()}, list(A))); - env.add_var("cons", Pi({A, Type()}, A >> (list(A) >> list(A)))); - env.add_var("a", Int); - env.add_var("b", Int); - env.add_var("n", Nat); - env.add_var("m", Nat); + env->add_var("list", Type() >> Type()); + env->add_var("nil", Pi({A, Type()}, list(A))); + env->add_var("cons", Pi({A, Type()}, A >> (list(A) >> list(A)))); + env->add_var("a", Int); + env->add_var("b", Int); + env->add_var("n", Nat); + env->add_var("m", Nat); expr a = Const("a"); expr b = Const("b"); expr n = Const("n");