diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 0ef9997296..fb0e18d2c2 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -16,4 +16,5 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp relation_manager.cpp export.cpp user_recursors.cpp idx_metavar.cpp composition_manager.cpp tc_multigraph.cpp noncomputable.cpp aux_recursors.cpp norm_num.cpp decl_stats.cpp meng_paulson.cpp - norm_num.cpp class_instance_resolution.cpp type_context.cpp) + norm_num.cpp class_instance_resolution.cpp type_context.cpp + tmp_type_context.cpp) diff --git a/src/library/tmp_type_context.cpp b/src/library/tmp_type_context.cpp new file mode 100644 index 0000000000..b525903de1 --- /dev/null +++ b/src/library/tmp_type_context.cpp @@ -0,0 +1,155 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "library/tmp_type_context.h" +#include "library/idx_metavar.h" + +namespace lean { +static name * g_prefix = nullptr; + +tmp_type_context::tmp_type_context(environment const & env, io_state const & ios, reducible_behavior b): + type_context(env, ios) { + switch (b) { + case UnfoldReducible: m_opaque_pred = mk_not_reducible_pred(env); break; + case UnfoldQuasireducible: m_opaque_pred = mk_not_quasireducible_pred(env); break; + case UnfoldSemireducible: m_opaque_pred = mk_irreducible_pred(env); break; + } + m_next_local_idx = 0; +} + +tmp_type_context::~tmp_type_context() { +} + +void tmp_type_context::clear() { + m_next_local_idx = 0; + m_uassignment.clear(); + m_eassignment.clear(); + m_trail.clear(); + m_scopes.clear(); +} + +void tmp_type_context::set_next_uvar_idx(unsigned next_idx) { + lean_assert(m_uassignment.empty()); + lean_assert(m_scopes.empty()); + m_uassignment.resize(next_idx); +} + +void tmp_type_context::set_next_mvar_idx(unsigned next_idx) { + lean_assert(m_eassignment.empty()); + lean_assert(m_scopes.empty()); + m_eassignment.resize(next_idx); +} + +expr tmp_type_context::mk_tmp_local(expr const & type, binder_info const & bi) { + unsigned idx = m_next_local_idx; + m_next_local_idx++; + name n(*g_prefix, idx); + return lean::mk_local(n, n, type, bi); +} + +bool tmp_type_context::is_tmp_local(expr const & e) const { + if (!is_local(e)) + return false; + name const & n = mlocal_name(e); + return !n.is_atomic() && n.get_prefix() == *g_prefix; +} + +bool tmp_type_context::is_uvar(level const & l) const { + return is_idx_metauniv(l); +} + +bool tmp_type_context::is_mvar(expr const & e) const { + return is_idx_metavar(e); +} + +optional tmp_type_context::get_assignment(level const & u) const { + unsigned idx = to_meta_idx(u); + // if the following assetion is violated, we have two options: + // 1- We should create the meta-variable using mk_uvar + // 2- We create using mk_idx_metauniv, and notify this object using + // set_next_uvar_idx + lean_assert(idx < m_uassignment.size()); + return m_uassignment[idx]; +} + +optional tmp_type_context::get_assignment(expr const & m) const { + unsigned idx = to_meta_idx(m); + // if the following assetion is violated, we have two options: + // 1- We should create the meta-variable using mk_mvar + // 2- We create using mk_idx_metavar, and notify this object using + // set_next_mvar_idx + lean_assert(idx < m_eassignment.size()); + return m_eassignment[idx]; +} + +void tmp_type_context::update_assignment(level const & u, level const & v) { + unsigned idx = to_meta_idx(u); + lean_assert(idx < m_uassignment.size()); // see comments above + lean_assert(!m_uassignment[idx]); + m_uassignment[idx] = v; + if (!m_scopes.empty()) + m_trail.emplace_back(trail_kind::Level, idx); +} + +void tmp_type_context::update_assignment(expr const & m, expr const & v) { + unsigned idx = to_meta_idx(m); + lean_assert(idx < m_eassignment.size()); // see comments above + // Remark: type class resolution may update an already assigned meta-variable with a + // definitionally equal, but the new assignment is "nicer", i.e., it has not been + // accidentally unfolded by the unifier. + // We only add the entry to the trail if it was not assigned before. + bool was_assigned = static_cast(m_eassignment[idx]); + m_eassignment[idx] = v; + if (!m_scopes.empty() && !was_assigned) + m_trail.emplace_back(trail_kind::Expr, idx); +} + +level tmp_type_context::mk_uvar() { + unsigned idx = m_uassignment.size(); + m_uassignment.push_back(none_level()); + return mk_idx_metauniv(idx); +} + +expr tmp_type_context::mk_mvar(expr const & type) { + unsigned idx = m_eassignment.size(); + m_eassignment.push_back(none_expr()); + return mk_idx_metavar(idx, type); +} + +void tmp_type_context::push() { + m_scopes.push_back(scope()); + scope & s = m_scopes.back(); + s.m_old_next_local_idx = m_next_local_idx; + s.m_uassignment_sz = m_uassignment.size(); + s.m_eassignment_sz = m_eassignment.size(); + s.m_trail_sz = m_trail.size(); +} + +void tmp_type_context::pop() { + lean_assert(!m_scopes.empty()); + scope const & s = m_scopes.back(); + m_next_local_idx = s.m_old_next_local_idx; + unsigned old_sz = s.m_trail_sz; + unsigned i = m_trail.size(); + while (i > old_sz) { + --i; + pair const & p = m_trail.back(); + switch (p.first) { + case trail_kind::Level: m_uassignment[p.second] = none_level(); break; + case trail_kind::Expr: m_eassignment[p.second] = none_expr(); break; + } + m_trail.pop_back(); + } + lean_assert(m_trail.size() == old_sz); + m_uassignment.resize(s.m_uassignment_sz); + m_eassignment.resize(s.m_eassignment_sz); +} + +void tmp_type_context::commit() { + lean_assert(!m_scopes.empty()); + m_scopes.pop_back(); +} +} diff --git a/src/library/tmp_type_context.h b/src/library/tmp_type_context.h new file mode 100644 index 0000000000..3dc210bfac --- /dev/null +++ b/src/library/tmp_type_context.h @@ -0,0 +1,84 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include "library/type_context.h" +#include "library/reducible.h" + +namespace lean { +/** \brief Type context for solving matching and simple unification problems. + It only supports meta-variables created with the module idx_metavar.h. + Internally, it stores the meta-variable assignments in an array. + So, it is assuming the metavariables have small indices. + + The assignment and backtracking stack can be reset using the clear method. + + \remark By default, this object assumes that non-reducible constants are opaque. + We can change that by providing a different reducible_behavior value when + creating the object. + + \remark The default implementations for infer_local(e) and + infer_metavar(e) just return mlocal_type(e). They must be + redefined if we want to use this class in modules that store the type + of local constants and meta-variables in a different place. + + \remark The local context is set using the method set_context from type_context. +*/ +class tmp_type_context : public type_context { + unsigned m_next_local_idx; + name_predicate m_opaque_pred; + std::vector> m_uassignment; + std::vector> m_eassignment; + enum class trail_kind { Level, Expr }; + std::vector> m_trail; // undo stack + struct scope { + unsigned m_old_next_local_idx; + unsigned m_uassignment_sz; + unsigned m_eassignment_sz; + unsigned m_trail_sz; + }; + std::vector m_scopes; +public: + tmp_type_context(environment const & env, io_state const & ios, reducible_behavior b = UnfoldReducible); + virtual ~tmp_type_context(); + + /** \brief Reset the state: backtracking stack, indices and assignment. */ + void clear(); + + /** \remark The following methods are useful when indexed meta-variables have been created outside + of this module. + \pre This method should only be invoked if not meta-variable has been created. + Use the method clear() to ensure this condition holds */ + void set_next_uvar_idx(unsigned next_idx); + + /** \remark The following methods are useful when indexed meta-variables have been created outside + of this module. + \pre This method should only be invoked if not meta-variable has been created. + Use the method clear() to ensure this condition holds */ + void set_next_mvar_idx(unsigned next_idx); + + virtual bool is_extra_opaque(name const & n) const { return m_opaque_pred(n); } + virtual expr mk_tmp_local(expr const & type, binder_info const & bi = binder_info()); + virtual bool is_tmp_local(expr const & e) const; + virtual bool is_uvar(level const & l) const; + virtual bool is_mvar(expr const & e) const; + virtual optional get_assignment(level const & u) const; + virtual optional get_assignment(expr const & m) const; + virtual void update_assignment(level const & u, level const & v); + virtual void update_assignment(expr const & m, expr const & v); + + virtual expr infer_local(expr const & e) const { return mlocal_type(e); } + virtual expr infer_metavar(expr const & e) const { return mlocal_type(e); } + + virtual level mk_uvar(); + virtual expr mk_mvar(expr const &); + + virtual void push(); + virtual void pop(); + virtual void commit(); +}; +}