feat(library/tmp_type_context): add temporary type_context

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)

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<level> 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<expr> 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<bool>(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<trail_kind, unsigned> 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();
+}
+}

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 <vector>
+#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<optional<level>>      m_uassignment;
+    std::vector<optional<expr>>       m_eassignment;
+    enum class trail_kind { Level, Expr };
+    std::vector<pair<trail_kind, unsigned>> 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<scope>                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<level> get_assignment(level const & u) const;
+    virtual optional<expr> 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();
+};
+}