diff --git a/src/api/exception.cpp b/src/api/exception.cpp index 1b510392f1..01cd5d1f44 100644 --- a/src/api/exception.cpp +++ b/src/api/exception.cpp @@ -6,7 +6,6 @@ Author: Leonardo de Moura */ #include "kernel/kernel_exception.h" #include "kernel/type_checker.h" -#include "library/unifier.h" #include "library/print.h" #include "library/error_handling.h" #include "api/exception.h" @@ -73,10 +72,6 @@ lean_exception_kind lean_exception_get_kind(lean_exception e) { return LEAN_KERNEL_EXCEPTION; if (dynamic_cast(ex)) return LEAN_INTERRUPTED; - if (dynamic_cast(ex)) - return LEAN_UNIFIER_EXCEPTION; - // if (dynamic_cast(ex)) - // return LEAN_TACTIC_EXCEPTION; if (dynamic_cast(ex)) return LEAN_PARSER_EXCEPTION; return LEAN_OTHER_EXCEPTION; diff --git a/src/api/lean_exception.h b/src/api/lean_exception.h index 906806110a..cbae92ddfb 100644 --- a/src/api/lean_exception.h +++ b/src/api/lean_exception.h @@ -49,8 +49,6 @@ typedef enum { LEAN_OUT_OF_MEMORY, // out of memory exception LEAN_INTERRUPTED, // execution was interrupted by user request LEAN_KERNEL_EXCEPTION, // type checking error - LEAN_UNIFIER_EXCEPTION, // unification exception - LEAN_TACTIC_EXCEPTION, // tactic exception LEAN_PARSER_EXCEPTION, // parser exception LEAN_OTHER_EXCEPTION // other (TODO) lean exceptions } lean_exception_kind; diff --git a/src/frontends/lean/server.cpp b/src/frontends/lean/server.cpp index c02d7b847b..39b792b523 100644 --- a/src/frontends/lean/server.cpp +++ b/src/frontends/lean/server.cpp @@ -15,7 +15,6 @@ Author: Leonardo de Moura #include "util/bitap_fuzzy_search.h" #include "kernel/instantiate.h" #include "library/aliases.h" -#include "library/unifier.h" #include "library/protected.h" #include "library/reducible.h" #include "library/projection.h" diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index bd25c2573a..b7ee8e451c 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -19,7 +19,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp # Legacy -- The following files will be eventually deleted normalize.cpp justification.cpp constraint.cpp metavar.cpp choice.cpp locals.cpp - unifier.cpp class_instance_resolution.cpp old_type_context.cpp + class_instance_resolution.cpp old_type_context.cpp legacy_type_context.cpp old_type_checker.cpp old_converter.cpp old_default_converter.cpp old_util.cpp old_local_context.cpp choice_iterator.cpp old_tmp_type_context.cpp diff --git a/src/library/error_handling.cpp b/src/library/error_handling.cpp index 9196e749cf..67be1283e4 100644 --- a/src/library/error_handling.cpp +++ b/src/library/error_handling.cpp @@ -10,7 +10,6 @@ Author: Leonardo de Moura #include "kernel/ext_exception.h" #include "kernel/for_each_fn.h" #include "library/io_state_stream.h" -#include "library/unifier.h" #include "library/exception.h" #include "library/flycheck.h" #include "library/pp_options.h" @@ -129,14 +128,6 @@ static void display_error_warning(bool is_error, io_state_stream const & ios, po ios << " " << ex << endl; } -static void display_error_warning(bool is_error, io_state_stream const & ios, pos_info_provider const * p, unifier_exception const & ex) { - formatter fmt = ios.get_formatter(); - options opts = ios.get_options(); - auto j = ex.get_justification(); - display_error_warning_pos(is_error, ios, p, j.get_main_expr()); - ios << " " << mk_pair(j.pp(fmt, p, ex.get_substitution()), opts) << endl; -} - static void display_error_warning(bool is_error, io_state_stream const & ios, pos_info_provider const * p, formatted_exception const & ex) { display_error_warning_pos(is_error, ios, p, ex.get_main_expr()); ios << " " << ex << endl; @@ -148,8 +139,6 @@ static void display_error_warning(bool is_error, io_state_stream const & ios, po display_error_warning(is_error, ios, p, *k_ex); } else if (auto f_ex = dynamic_cast(&ex)) { display_error_warning(is_error, ios, p, *f_ex); - } else if (auto e_ex = dynamic_cast(&ex)) { - display_error_warning(is_error, ios, p, *e_ex); } else if (p) { display_error_warning_pos(is_error, ios, p->get_file_name(), p->get_some_pos().first, p->get_some_pos().second); ios << " " << ex.what() << endl; diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index 1724eaf371..b34f64a718 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -6,7 +6,6 @@ Author: Leonardo de Moura */ #include "library/trace.h" #include "library/constants.h" -#include "library/unifier.h" #include "library/kernel_serializer.h" #include "library/typed_expr.h" #include "library/choice.h" @@ -93,7 +92,6 @@ void initialize_library_module() { initialize_placeholder(); initialize_idx_metavar(); initialize_io_state(); - initialize_unifier(); initialize_kernel_serializer(); initialize_typed_expr(); initialize_choice(); @@ -171,7 +169,6 @@ void finalize_library_module() { finalize_choice(); finalize_typed_expr(); finalize_kernel_serializer(); - finalize_unifier(); finalize_io_state(); finalize_idx_metavar(); finalize_placeholder(); diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp deleted file mode 100644 index 60802a810d..0000000000 --- a/src/library/unifier.cpp +++ /dev/null @@ -1,2864 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include -#include -#include -#include "util/interrupt.h" -#include "util/lazy_list_fn.h" -#include "util/sstream.h" -#include "util/lbool.h" -#include "util/flet.h" -#include "util/fresh_name.h" -#include "util/sexpr/option_declarations.h" -#include "kernel/for_each_fn.h" -#include "kernel/abstract.h" -#include "kernel/instantiate.h" -#include "kernel/kernel_exception.h" -#include "kernel/error_msgs.h" -#include "library/trace.h" -#include "library/util.h" -#include "library/locals.h" -#include "library/module.h" -#include "library/unifier.h" -#include "library/reducible.h" -#include "library/print.h" -#include "library/expr_lt.h" -#include "library/projection.h" -#include "library/old_type_checker.h" - -#ifndef LEAN_DEFAULT_UNIFIER_MAX_STEPS -#define LEAN_DEFAULT_UNIFIER_MAX_STEPS 20000 -#endif - -#ifndef LEAN_DEFAULT_UNIFIER_EXPENSIVE_CLASSES -#define LEAN_DEFAULT_UNIFIER_EXPENSIVE_CLASSES false -#endif - -#ifndef LEAN_DEFAULT_UNIFIER_CONSERVATIVE -#define LEAN_DEFAULT_UNIFIER_CONSERVATIVE false -#endif - -#ifndef LEAN_DEFAULT_UNIFIER_NONCHRONOLOGICAL -#define LEAN_DEFAULT_UNIFIER_NONCHRONOLOGICAL true -#endif - -#ifndef LEAN_DEFAULT_UNIFIER_NORMALIZER_MAX_STEPS -#define LEAN_DEFAULT_UNIFIER_NORMALIZER_MAX_STEPS 512 -#endif - -namespace lean { -static name * g_unifier_max_steps = nullptr; -static name * g_unifier_expensive_classes = nullptr; -static name * g_unifier_conservative = nullptr; -static name * g_unifier_nonchronological = nullptr; -static name * g_unifier_normalizer_max_steps = nullptr; - -unsigned get_unifier_max_steps(options const & opts) { - return opts.get_unsigned(*g_unifier_max_steps, LEAN_DEFAULT_UNIFIER_MAX_STEPS); -} - -unsigned get_unifier_normalizer_max_steps(options const & opts) { - return opts.get_unsigned(*g_unifier_normalizer_max_steps, LEAN_DEFAULT_UNIFIER_NORMALIZER_MAX_STEPS); -} - -bool get_unifier_expensive_classes(options const & opts) { - return opts.get_bool(*g_unifier_expensive_classes, LEAN_DEFAULT_UNIFIER_EXPENSIVE_CLASSES); -} - -bool get_unifier_conservative(options const & opts) { - return opts.get_bool(*g_unifier_conservative, LEAN_DEFAULT_UNIFIER_CONSERVATIVE); -} - -bool get_unifier_nonchronological(options const & opts) { - return opts.get_bool(*g_unifier_nonchronological, LEAN_DEFAULT_UNIFIER_NONCHRONOLOGICAL); -} - -unifier_config::unifier_config(bool use_exceptions, bool discard): - m_use_exceptions(use_exceptions), - m_max_steps(LEAN_DEFAULT_UNIFIER_MAX_STEPS), - m_normalizer_max_steps(LEAN_DEFAULT_UNIFIER_NORMALIZER_MAX_STEPS), - m_expensive_classes(LEAN_DEFAULT_UNIFIER_EXPENSIVE_CLASSES), - m_discard(discard), - m_nonchronological(LEAN_DEFAULT_UNIFIER_NONCHRONOLOGICAL) { - m_kind = unifier_kind::Liberal; - m_pattern = false; - m_ignore_context_check = false; -} - -unifier_config::unifier_config(options const & o, bool use_exceptions, bool discard): - m_use_exceptions(use_exceptions), - m_max_steps(get_unifier_max_steps(o)), - m_normalizer_max_steps(get_unifier_normalizer_max_steps(o)), - m_expensive_classes(get_unifier_expensive_classes(o)), - m_discard(discard), - m_nonchronological(get_unifier_nonchronological(o)) { - if (get_unifier_conservative(o)) - m_kind = unifier_kind::Conservative; - else - m_kind = unifier_kind::Liberal; - m_pattern = false; - m_ignore_context_check = false; -} - -// If \c e is a metavariable ?m or a term of the form (?m l_1 ... l_n) where -// l_1 ... l_n are distinct local variables, then return ?m, and store l_1 ... l_n in args. -// Otherwise return none. -optional is_simple_meta(expr const & e, buffer & args) { - expr const & m = get_app_args(e, args); - if (!is_metavar(m)) - return none_expr(); - for (auto it = args.begin(); it != args.end(); it++) { - if (!is_local(*it) || contains_local(*it, args.begin(), it)) - return none_expr(); - } - return some_expr(m); -} - -bool is_simple_meta(expr const & e) { - buffer args; - return (bool)is_simple_meta(e, args); // NOLINT -} - -// Return true if all local constants in \c e are in locals -bool context_check(expr const & e, buffer const & locals) { - bool failed = false; - for_each(e, [&](expr const & e, unsigned) { - if (failed) - return false; - if (is_local(e)) { - if (!contains_local(e, locals)) - failed = true; - return false; // do not visit type - } - if (is_metavar(e)) - return false; // do not visit type - return has_local(e); - }); - return !failed; -} - -enum class occurs_check_status { Ok, Maybe, FailCircular, FailLocal }; - -// Return -// - l_undef if \c e contains a metavariable application that contains -// a local constant not in locals -// - l_true if \c e does not contain the metavariable \c m, and all local -// constants are in \c e are in \c locals. -// - l_false if \c e contains \c m or it contains a local constant \c l -// not in locals that is not in a metavariable application. -occurs_check_status occurs_context_check(substitution & s, expr const & e, expr const & m, buffer const & locals, expr & bad_local) { - expr root = e; - occurs_check_status r = occurs_check_status::Ok; - for_each(e, [&](expr const & e, unsigned) { - if (r == occurs_check_status::FailLocal || r == occurs_check_status::FailCircular) { - return false; - } else if (is_local(e)) { - if (!contains_local(e, locals)) { - // right-hand-side contains variable that is not in the scope - // of metavariable. - bad_local = e; - r = occurs_check_status::FailLocal; - } - return false; // do not visit type - } else if (is_meta(e)) { - if (r == occurs_check_status::Ok) { - if (!context_check(e, locals)) - r = occurs_check_status::Maybe; - if (s.occurs(m, e)) - r = occurs_check_status::Maybe; - } - if (mlocal_name(get_app_fn(e)) == mlocal_name(m)) - r = occurs_check_status::FailCircular; - return false; // do not visit children - } else { - // we only need to continue exploring e if it contains - // metavariables and/or local constants. - return has_expr_metavar(e) || has_local(e); - } - }); - if (r != occurs_check_status::Ok) - return r; - for (expr const & local : locals) { - if (s.occurs(m, mlocal_type(local))) - return occurs_check_status::Maybe; - } - return r; -} - -occurs_check_status occurs_context_check(substitution & s, expr const & e, expr const & m, buffer const & locals) { - expr bad_local; - return occurs_context_check(s, e, m, locals, bad_local); -} - -unify_status unify_simple_core(substitution & s, expr const & lhs, expr const & rhs, justification const & j) { - lean_assert(is_meta(lhs)); - buffer args; - auto m = is_simple_meta(lhs, args); - if (!m || is_meta(rhs)) { - return unify_status::Unsupported; - } else { - switch (occurs_context_check(s, rhs, *m, args)) { - case occurs_check_status::FailLocal: - case occurs_check_status::FailCircular: - return unify_status::Failed; - case occurs_check_status::Maybe: - return unify_status::Unsupported; - case occurs_check_status::Ok: { - s.assign(*m, args, rhs, j); - return unify_status::Solved; - }} - } - lean_unreachable(); // LCOV_EXCL_LINE -} - -unify_status unify_simple(substitution & s, expr const & lhs, expr const & rhs, justification const & j) { - if (lhs == rhs) - return unify_status::Solved; - else if (!has_metavar(lhs) && !has_metavar(rhs)) - return unify_status::Failed; - else if (is_meta(lhs)) - return unify_simple_core(s, lhs, rhs, j); - else if (is_meta(rhs)) - return unify_simple_core(s, rhs, lhs, j); - else - return unify_status::Unsupported; -} - -// Return true if m occurs in e -bool occurs_meta(level const & m, level const & e) { - lean_assert(is_meta(m)); - bool contains = false; - for_each(e, [&](level const & l) { - if (contains) - return false; - if (l == m) { - contains = true; - return false; - } - return has_meta(l); - }); - return contains; -} - -unify_status unify_simple_core(substitution & s, level const & lhs, level const & rhs, justification const & j) { - lean_assert(is_meta(lhs)); - bool contains = occurs_meta(lhs, rhs); - if (contains) { - if (is_succ(rhs)) - return unify_status::Failed; - else - return unify_status::Unsupported; - } - s.assign(meta_id(lhs), rhs, j); - return unify_status::Solved; -} - -unify_status unify_simple(substitution & s, level const & lhs, level const & rhs, justification const & j) { - if (lhs == rhs) - return unify_status::Solved; - else if (!has_meta(lhs) && !has_meta(rhs)) - return unify_status::Failed; - else if (is_meta(lhs)) - return unify_simple_core(s, lhs, rhs, j); - else if (is_meta(rhs)) - return unify_simple_core(s, rhs, lhs, j); - else if (is_succ(lhs) && is_succ(rhs)) - return unify_simple(s, succ_of(lhs), succ_of(rhs), j); - else - return unify_status::Unsupported; -} - -unify_status unify_simple(substitution & s, constraint const & c) { - if (is_eq_cnstr(c)) - return unify_simple(s, cnstr_lhs_expr(c), cnstr_rhs_expr(c), c.get_justification()); - else if (is_level_eq_cnstr(c)) - return unify_simple(s, cnstr_lhs_level(c), cnstr_rhs_level(c), c.get_justification()); - else - return unify_status::Unsupported; -} - -static constraint * g_dont_care_cnstr = nullptr; -static unsigned g_group_size = 1u << 28; -constexpr unsigned g_num_groups = 9; -static unsigned g_cnstr_group_first_index[g_num_groups] = { 0, g_group_size, 2*g_group_size, 3*g_group_size, 4*g_group_size, 5*g_group_size, 6*g_group_size, 7*g_group_size, 8*g_group_size}; -static unsigned get_group_first_index(cnstr_group g) { - return g_cnstr_group_first_index[static_cast(g)]; -} - -static unsigned get_group_last_index(cnstr_group g) { - unsigned idx = static_cast(g); - lean_assert(idx < g_num_groups); - if (idx == g_num_groups - 1) { - lean_assert(g == cnstr_group::MaxDelayed); - return std::numeric_limits::max() - g_group_size; - } else { - lean_assert(idx < g_num_groups - 1); - return g_cnstr_group_first_index[idx+1] - 1; - } -} - -static cnstr_group to_cnstr_group(unsigned cidx) { - for (unsigned i = 1; i < g_num_groups; i++) { - if (cidx < g_cnstr_group_first_index[i]) - return static_cast(i); - } - return cnstr_group::MaxDelayed; -} - -/** \brief Convert choice constraint delay factor to cnstr_group */ -cnstr_group get_choice_cnstr_group(constraint const & c) { - lean_assert(is_choice_cnstr(c)); - unsigned f = cnstr_delay_factor(c); - if (f > static_cast(cnstr_group::MaxDelayed)) { - return cnstr_group::MaxDelayed; - } else { - return static_cast(f); - } -} - -/** \brief Auxiliary functional object for implementing simultaneous higher-order unification */ -struct unifier_fn { - typedef pair cnstr; // constraint + idx - struct cnstr_cmp { - int operator()(cnstr const & c1, cnstr const & c2) const { - return c1.second < c2.second ? -1 : (c1.second == c2.second ? 0 : 1); - } - }; - typedef rb_tree cnstr_set; - typedef rb_tree cnstr_idx_set; - typedef name_map name_to_cnstrs; - typedef name_map owned_map; - typedef rb_map, expr_quick_cmp> expr_map; - typedef std::shared_ptr type_checker_ptr; - environment m_env; - substitution m_subst; - constraints m_postponed; // constraints that will not be solved - owned_map m_owned_map; // mapping from metavariable name m to constraint idx - expr_map m_type_map; // auxiliary map for storing the type of the expr in choice constraints - type_checker_ptr m_tc; - type_checker_ptr m_flex_rigid_tc; // type checker used when solving flex rigid constraints. By default, - // only the definitions from the main module are treated as transparent. - unifier_config m_config; - unsigned m_num_steps; - bool m_first; //!< True if we still have to generate the first solution. - unsigned m_next_assumption_idx; //!< Next assumption index. - unsigned m_next_cidx; //!< Next constraint index. - /** - \brief "Queue" of constraints to be solved. - - We implement it using a red-black-tree because: - 1- Our red-black-trees support a O(1) copy operation. So, it is cheap to create a snapshot - whenever we create a backtracking point. - - 2- We can easily remove any constraint from the queue in O(n log n). We do that when - a metavariable \c m is assigned, and we want to instantiate it in all constraints that - contains it. - */ - cnstr_set m_cnstrs; - /** - \brief The following map is an index. The map a metavariable name \c m to the set of constraint indices that contain \c m. - We use these indices whenever a metavariable \c m is assigned. - When the metavariable is assigned, we used this index to remove constraints that contains \c m from \c m_cnstrs, - instantiate \c m, and reprocess them. - - \remark \c m_mvar_occs is for regular metavariables. - */ - name_to_cnstrs m_mvar_occs; - - /** - \brief Base class for the case-splits created by the unifier. - - We have three different kinds of case splits: - 1- unifier plugin - 2- choice constraints - 3- higher-order unification - */ - struct case_split { - unsigned m_assumption_idx; // idx of the current assumption - justification m_jst; - justification m_failed_justifications; // justifications for failed branches - // snapshot of unifier's state - substitution m_subst; - constraints m_postponed; - cnstr_set m_cnstrs; - expr_map m_type_map; - name_to_cnstrs m_mvar_occs; - owned_map m_owned_map; - - /** \brief Save unifier's state */ - case_split(unifier_fn & u, justification const & j): - m_assumption_idx(u.m_next_assumption_idx), m_jst(j), m_subst(u.m_subst), - m_postponed(u.m_postponed), m_cnstrs(u.m_cnstrs), m_type_map(u.m_type_map), - m_mvar_occs(u.m_mvar_occs), m_owned_map(u.m_owned_map) { - u.m_next_assumption_idx++; - } - - /** \brief Restore unifier's state with saved values, and update m_assumption_idx and m_failed_justifications. */ - void restore_state(unifier_fn & u) { - lean_assert(u.in_conflict()); - u.m_subst = m_subst; - u.m_postponed = m_postponed; - u.m_cnstrs = m_cnstrs; - u.m_mvar_occs = m_mvar_occs; - u.m_owned_map = m_owned_map; - u.m_type_map = m_type_map; - m_assumption_idx = u.m_next_assumption_idx; - m_failed_justifications = mk_composite1(m_failed_justifications, *u.m_conflict); - u.m_next_assumption_idx++; - u.m_conflict = optional(); - } - justification get_jst() const { return m_jst; } - virtual ~case_split() {} - virtual bool next(unifier_fn & u) = 0; - }; - typedef std::vector> case_split_stack; - - struct lazy_constraints_case_split : public case_split { - lazy_list m_tail; - lazy_constraints_case_split(unifier_fn & u, justification const & j, lazy_list const & tail): - case_split(u, j), m_tail(tail) {} - virtual bool next(unifier_fn & u) { return u.next_lazy_constraints_case_split(*this); } - }; - - struct simple_case_split : public case_split { - list m_tail; - simple_case_split(unifier_fn & u, justification const & j, list const & tail):case_split(u, j), m_tail(tail) {} - virtual bool next(unifier_fn & u) { return u.next_simple_case_split(*this); } - }; - - struct delta_unfold_case_split : public case_split { - bool m_done; - constraint m_cnstr; - delta_unfold_case_split(unifier_fn & u, justification const & j, constraint const & c): - case_split(u, j), m_done(false), m_cnstr(c) {} - virtual bool next(unifier_fn & u) { return u.next_delta_unfold_case_split(*this); } - }; - - case_split_stack m_case_splits; - optional m_conflict; //!< if different from none, then there is a conflict. - - unifier_fn(environment const & env, unsigned num_cs, constraint const * cs, - substitution const & s, - unifier_config const & cfg): - m_env(env), m_subst(s), - m_config(cfg), m_num_steps(0) { - switch (m_config.m_kind) { - case unifier_kind::Cheap: - m_tc = mk_opaque_type_checker(env); - m_flex_rigid_tc = m_tc; - break; - case unifier_kind::Conservative: - m_tc = mk_type_checker(env, UnfoldReducible); - m_flex_rigid_tc = m_tc; - break; - case unifier_kind::Liberal: - m_tc = mk_type_checker(env); - m_flex_rigid_tc = mk_type_checker(env, UnfoldReducible); - break; - default: - lean_unreachable(); - } - m_next_assumption_idx = 0; - m_next_cidx = 0; - m_first = true; - process_input_constraints(num_cs, cs); - } - - void process_input_constraints(unsigned num_cs, constraint const * cs) { - // Input choice constraints may have ownership over a metavariable. - // So, we must first process them, to make sure the ownership table is initialized before - // we solve the remaining constraints - for (unsigned i = 0; i < num_cs; i++) { - if (cs[i].kind() == constraint_kind::Choice) - preprocess_choice_constraint(cs[i]); - } - for (unsigned i = 0; i < num_cs; i++) { - if (cs[i].kind() != constraint_kind::Choice) - process_constraint(cs[i]); - } - } - - void check_system() { - ::lean::check_system("unifier"); - } - - void check_full() { - check_system(); - if (m_num_steps > m_config.m_max_steps) - throw exception(sstream() << "unifier maximum number of steps (" << m_config.m_max_steps << ") exceeded, " << - "the maximum number of steps can be increased by setting the option unifier.max_steps " << - "(remark: the unifier uses higher order unification and unification-hints, " << - "which may trigger non-termination"); - m_num_steps++; - } - - bool in_conflict() const { return (bool)m_conflict; } // NOLINT - void set_conflict(justification const & j) { m_conflict = j; } - void update_conflict(justification const & j) { m_conflict = j; } - void reset_conflict() { m_conflict = optional(); lean_assert(!in_conflict()); } - - expr mk_local_for(expr const & b) { - return mk_local(mk_fresh_name(), binding_name(b), binding_domain(b), binding_info(b)); - } - - /** - \brief Update occurrence index with entry m -> cidx, where \c m is the name of a metavariable, - and \c cidx is the index of a constraint that contains \c m. - */ - void add_mvar_occ(name const & m, unsigned cidx) { - cnstr_idx_set s; - auto it = m_mvar_occs.find(m); - if (it) - s = *it; - if (!s.contains(cidx)) { - s.insert(cidx); - m_mvar_occs.insert(m, s); - } - } - - void add_meta_occ(expr const & m, unsigned cidx) { - lean_assert(is_meta(m)); - add_mvar_occ(mlocal_name(get_app_fn(m)), cidx); - } - - /** \brief For each metavariable m in e add an entry m -> cidx at m_mvar_occs. - Return true if at least one entry was added. - */ - bool add_meta_occs(expr const & e, unsigned cidx) { - bool added = false; - if (has_expr_metavar(e)) { - for_each(e, [&](expr const & e, unsigned) { - if (is_meta(e)) { - add_meta_occ(e, cidx); - added = true; - return false; - } - if (is_local(e)) - return false; - return has_expr_metavar(e); - }); - } - return added; - } - - /** \brief Add constraint to the constraint queue. - - \remark We use FIFO policy for all but MaxDelayed group. - */ - unsigned add_cnstr(constraint const & c, cnstr_group g) { - unsigned cidx; - if (g == cnstr_group::MaxDelayed) { - // MaxDelayed is a stack - cidx = get_group_last_index(g) - m_next_cidx; - /* Make sure there is at least one free space between any two MAX_DELAYED constraints. - We want to put constraints containing the variable owned by a MAX_DELAYED constraint c - after it and before the next MAX_DELAYED constraint c. */ - m_next_cidx += 2; - } else { - cidx = m_next_cidx + get_group_first_index(g); - m_next_cidx++; - } - m_cnstrs.insert(cnstr(c, cidx)); - return cidx; - } - - /** \brief Add constraint \c to the constraint queue, but - make sure it occurs AFTER the the constraint with index \c cidx. - - \remark We used this method to make sure \c c is going to be - processed after the constraint \c cidx. */ - unsigned add_cnstr_after(constraint const & c, unsigned cidx) { - cnstr_group g = to_cnstr_group(cidx); - unsigned new_cidx; - if (g == cnstr_group::MaxDelayed) { - // See add_cnstr - new_cidx = cidx + 1; - } else { - new_cidx = m_next_cidx + get_group_first_index(g); - m_next_cidx++; - } - m_cnstrs.insert(cnstr(c, new_cidx)); - return new_cidx; - } - - /** \brief Check if \c t1 and \c t2 are definitionally equal, if they are not, set a conflict with justification \c j - */ - bool is_def_eq(expr const & t1, expr const & t2, justification const & j) { - try { - auto dcs = m_tc->is_def_eq(t1, t2, j); - if (!dcs.first) { - lean_trace("unifier", tout() << "conflict: " << t1 << " =?= " << t2 << "\n";); - set_conflict(j); - return false; - } else { - return process_constraints(dcs.second); - } - } catch (exception&) { - set_conflict(j); - return false; - } - } - - /** \brief Process the given constraints. Return true iff no conflict was detected. */ - bool process_constraints(constraint_seq const & cs) { - return cs.all_of([&](constraint const & c) { return process_constraint(c); }); - } - - bool process_constraints(buffer const & cs) { - for (auto const & c : cs) { - if (!process_constraint(c)) - return false; - } - return true; - } - - - /** \brief Process constraints in \c cs, and append justification \c j to them. */ - bool process_constraints(constraint_seq const & cs, justification const & j) { - return cs.all_of([&](constraint const & c) { - return process_constraint(update_justification(c, mk_composite1(c.get_justification(), j))); - }); - } - - template - bool process_constraints(Constraints const & cs, justification const & j) { - for (auto const & c : cs) { - if (!process_constraint(update_justification(c, mk_composite1(c.get_justification(), j)))) - return false; - } - return true; - } - - /** \brief Put \c e in weak head normal form. - - \remark Constraints generated in the process are stored in \c cs. - */ - expr whnf(expr const & e, constraint_seq & cs) { - return m_tc->whnf(e, cs); - } - - /** \brief Infer \c e type. - - \remark Return none if an exception was throw when inferring the type. - \remark Constraints generated in the process are stored in \c cs. - */ - optional infer(expr const & e, constraint_seq & cs) { - try { - return some_expr(m_tc->infer(e, cs)); - } catch (exception &) { - return none_expr(); - } - } - - expr whnf(expr const & e, justification const & j, buffer & cs) { - constraint_seq _cs; - expr r = whnf(e, _cs); - to_buffer(_cs, j, cs); - return r; - } - - expr flex_rigid_whnf(expr const & e, justification const & j, buffer & cs) { - constraint_seq _cs; - expr r = m_flex_rigid_tc->whnf(e, _cs); - to_buffer(_cs, j, cs); - return r; - } - - justification mk_assign_justification(expr const & m, expr const & m_type, expr const & v_type, justification const & j) { - auto r = j.get_main_expr(); - if (!r) r = m; - justification new_j = mk_justification(r, [=](formatter const & fmt, substitution const & subst, bool) { - substitution s(subst); - format r; - expr _m = s.instantiate(m); - if (is_meta(_m)) { - r = format("type error in placeholder assignment"); - } else { - r = format("type error in placeholder assigned to"); - r += pp_indent_expr(fmt, _m); - } - format expected_fmt, given_fmt; - std::tie(expected_fmt, given_fmt) = pp_until_different(fmt, m_type, v_type); - r += compose(line(), format("placeholder has type")); - r += given_fmt; - r += compose(line(), format("but is expected to have type")); - r += expected_fmt; - r += compose(line(), format("the assignment was attempted when processing")); - r += nest(2*get_pp_indent(fmt.get_options()), compose(line(), j.pp(fmt, nullptr, subst, false))); - return r; - }); - return mk_composite1(new_j, j); - } - - /** - \brief Given lhs of the form (m args), assign (m args) := rhs with justification j. - The type of lhs and rhs are inferred, and is_def_eq is invoked. - - Any other constraint that contains \c m is revisited - */ - bool assign(expr const & lhs, expr const & m, buffer const & args, expr const & rhs, justification const & j) { - lean_assert(is_metavar(m)); - lean_assert(!in_conflict()); - m_subst.assign(m, args, rhs, j); - constraint_seq cs; - auto lhs_type = infer(lhs, cs); - auto rhs_type = infer(rhs, cs); - if (lhs_type && rhs_type) { - if (!process_constraints(cs, j)) - return false; - justification new_j = mk_assign_justification(m, *lhs_type, *rhs_type, j); - if (!is_def_eq(*lhs_type, *rhs_type, new_j)) - return false; - } else { - set_conflict(j); - return false; - } - auto it = m_mvar_occs.find(mlocal_name(m)); - if (it) { - cnstr_idx_set s = *it; - m_mvar_occs.erase(mlocal_name(m)); - s.for_each([&](unsigned cidx) { - process_constraint_cidx(cidx); - }); - return !in_conflict(); - } else { - return true; - } - } - - /** - \brief Assign \c v to universe metavariable \c m with justification \c j. - Any constraint that contains \c m is revisted. - */ - bool assign(level const & m, level const & v, justification const & j) { - lean_assert(is_meta(m)); - m_subst.assign(m, v, j); - return true; - } - - justification mk_invalid_local_ctx_justification(expr const & lhs, expr const & rhs, justification const & j, - expr const & bad_local) { - justification new_j = mk_justification(get_app_fn(lhs), [=](formatter const & fmt, substitution const & subst, bool) { - format r = format("invalid local context when tried to assign"); - r += pp_indent_expr(fmt, rhs); - buffer locals; - auto m = get_app_args(lhs, locals); - r += line() + format("containing '") + fmt(bad_local) + format("', to placeholder '") + fmt(m) + format("'"); - if (locals.empty()) { - r += format(", in the empty local context"); - } else { - r += format(", in the local context"); - format aux; - bool first = true; - for (expr const l : locals) { - if (first) first = false; else aux += space(); - aux += fmt(l); - } - r += nest(get_pp_indent(fmt.get_options()), compose(line(), aux)); - } - r += compose(line(), format("the assignment was attempted when processing")); - r += nest(2*get_pp_indent(fmt.get_options()), compose(line(), j.pp(fmt, nullptr, subst, false))); - return r; - }); - return mk_composite1(new_j, j); - } - - enum status { Solved, Failed, Continue }; - - struct interrupt_normalizer {}; - - /** - \brief Process constraints of the form lhs =?= rhs where lhs is of the form ?m or (?m l_1 .... l_n), - where all \c l_i are distinct local variables. In this case, the method returns Solved, if the method assign succeeds. - The method returns \c Failed if \c rhs contains ?m, or it contains a local constant not in {l_1, ..., l_n}. - Otherwise, it returns \c Continue. - */ - status process_metavar_eq(expr const & lhs, expr const & rhs, justification const & j) { - if (!is_meta(lhs)) - return Continue; - buffer locals; - auto m = is_simple_meta(lhs, locals); - if (!m || is_meta(rhs)) - return Continue; - expr bad_local; - occurs_check_status status; - if (m_config.m_ignore_context_check) - status = occurs_check_status::Ok; - else - status = occurs_context_check(m_subst, rhs, *m, locals, bad_local); - if (status == occurs_check_status::FailLocal || status == occurs_check_status::FailCircular) { - // Try to normalize rhs - // Example: ?M := f (pr1 (pair 0 ?M)) - try { - // unsigned counter = 0; - constraint_seq cs; - /* - auto is_target_fn = [&](expr const & e) { - if ((status == occurs_check_status::FailLocal && occurs(bad_local, e)) || - (status == occurs_check_status::FailCircular && occurs(*m, e))) { - counter++; - if (counter > m_config.m_normalizer_max_steps) - throw interrupt_normalizer(); - return true; - } else { - return false; - } - }; - */ - expr rhs_n = rhs; // normalize(*m_tc, rhs, is_target_fn, cs); - if (rhs != rhs_n && process_constraints(cs)) - return process_metavar_eq(lhs, rhs_n, j); - } catch (interrupt_normalizer &) { - // exceeded maximum number of steps - } - } - switch (status) { - case occurs_check_status::FailLocal: - set_conflict(mk_invalid_local_ctx_justification(lhs, rhs, j, bad_local)); - return Failed; - case occurs_check_status::FailCircular: - set_conflict(j); - return Failed; - case occurs_check_status::Maybe: - return Continue; - case occurs_check_status::Ok: - lean_assert(!m_subst.is_assigned(*m)); - if (assign(lhs, *m, locals, rhs, j)) { - return Solved; - } else { - return Failed; - } - } - lean_unreachable(); // LCOV_EXCL_LINE - } - - /** \brief Return true if type of \c e is Type. - \remark constraints are discarded */ - bool is_type(expr const & e) { - constraint_seq cs; - optional t = infer(e, cs); - if (!t) - return false; - t = whnf(*t, cs); - return is_sort(*t); - } - - optional is_delta(expr const & e) { - return m_tc->is_delta(e); - } - - /** \brief Return true if lhs and rhs are of the form (f ...) where f can be expanded */ - bool is_eq_deltas(expr const & lhs, expr const & rhs) { - auto lhs_d = is_delta(lhs); - auto rhs_d = is_delta(rhs); - return lhs_d && rhs_d && is_eqp(*lhs_d, *rhs_d); - } - - /** \brief Return true if the constraint is of the form (f ...) =?= (f ...), where f can be expanded. */ - bool is_delta_cnstr(constraint const & c) { - return is_eq_cnstr(c) && is_eq_deltas(cnstr_lhs_expr(c), cnstr_rhs_expr(c)); - } - - pair instantiate_metavars(constraint const & c) { - if (is_eq_cnstr(c)) { - auto lhs_jst = m_subst.instantiate_metavars(cnstr_lhs_expr(c)); - auto rhs_jst = m_subst.instantiate_metavars(cnstr_rhs_expr(c)); - expr lhs = lhs_jst.first; - expr rhs = rhs_jst.first; - if (lhs != cnstr_lhs_expr(c) || rhs != cnstr_rhs_expr(c)) { - return mk_pair(mk_eq_cnstr(lhs, rhs, - mk_composite1(mk_composite1(c.get_justification(), lhs_jst.second), rhs_jst.second)), - true); - } - } else if (is_level_eq_cnstr(c)) { - auto lhs_jst = m_subst.instantiate_metavars(cnstr_lhs_level(c)); - auto rhs_jst = m_subst.instantiate_metavars(cnstr_rhs_level(c)); - level lhs = lhs_jst.first; - level rhs = rhs_jst.first; - if (lhs != cnstr_lhs_level(c) || rhs != cnstr_rhs_level(c)) { - return mk_pair(mk_level_eq_cnstr(lhs, rhs, - mk_composite1(mk_composite1(c.get_justification(), lhs_jst.second), rhs_jst.second)), - true); - } - } - return mk_pair(c, false); - } - - status process_eq_constraint_core(constraint const & c) { - expr const & lhs = cnstr_lhs_expr(c); - expr const & rhs = cnstr_rhs_expr(c); - justification const & jst = c.get_justification(); - - if (lhs == rhs) - return Solved; // trivial constraint - - // Update justification using the justification of the instantiated metavariables - if (!has_metavar(lhs) && !has_metavar(rhs)) { - return is_def_eq(lhs, rhs, jst) ? Solved : Failed; - } - - // Handle higher-order pattern matching. - status st = process_metavar_eq(lhs, rhs, jst); - if (st != Continue) return st; - st = process_metavar_eq(rhs, lhs, jst); - if (st != Continue) return st; - - return Continue; - } - - expr instantiate_meta(expr e, justification & j) { - while (true) { - if (auto p = m_subst.expand_metavar_app(e)) { - // The following check_system is defensive programming. - // If the unifier is correct, and no loops are introduced in the substituion, - // then this loop should always terminate. - // Anyway, we may have bugs, and we should interrupt the loop if all resources are being consumed. - check_system(); - e = p->first; - j = mk_composite1(j, p->second); - } else { - return e; - } - } - } - - expr instantiate_meta_args(expr const & e, justification & j) { - if (!is_app(e)) - return e; - buffer args; - bool modified = false; - expr const & f = get_app_rev_args(e, args); - unsigned i = args.size(); - while (i > 0) { - --i; - expr new_arg = instantiate_meta(args[i], j); - if (new_arg != args[i]) { - modified = true; - args[i] = new_arg; - } - } - if (!modified) - return e; - return mk_rev_app(f, args.size(), args.data()); - } - - status instantiate_eq_cnstr(constraint const & c) { - justification j = c.get_justification(); - expr lhs = instantiate_meta(cnstr_lhs_expr(c), j); - expr rhs = instantiate_meta(cnstr_rhs_expr(c), j); - if (lhs != cnstr_lhs_expr(c) || rhs != cnstr_rhs_expr(c)) - return is_def_eq(lhs, rhs, j) ? Solved : Failed; - lhs = instantiate_meta_args(lhs, j); - rhs = instantiate_meta_args(rhs, j); - if (lhs != cnstr_lhs_expr(c) || rhs != cnstr_rhs_expr(c)) - return is_def_eq(lhs, rhs, j) ? Solved : Failed; - return Continue; - } - - /** \brief Return a delay factor if e is of the form (?m ...) and ?m is a metavariable owned by - a choice constraint. The delay factor is the delay of the choice constraint. - Return none otherwise. */ - optional is_owned(expr const & e) { - expr const & m = get_app_fn(e); - if (!is_metavar(m)) - return optional(); - if (auto it = m_owned_map.find(mlocal_name(m))) - return optional(*it); - else - return optional(); - } - - /** \brief Applies previous method to the left and right hand sides of the equality constraint */ - optional is_owned(constraint const & c) { - if (auto d = is_owned(cnstr_lhs_expr(c))) - return d; - else - return is_owned(cnstr_rhs_expr(c)); - } - - static status to_status(bool b) { return b ? Solved : Failed; } - - status reduce_both_proj_and_check(expr const & lhs, expr const & rhs, justification const & j) { - lean_assert(is_projection_app(lhs)); - lean_assert(is_projection_app(rhs)); - constraint_seq new_cs; - expr new_lhs = whnf(lhs, new_cs); - expr new_rhs = whnf(rhs, new_cs); - if (lhs != new_lhs || rhs != new_rhs) - return to_status(is_def_eq(new_lhs, new_rhs, j) && process_constraints(new_cs)); - if (const_name(get_app_fn(lhs)) != const_name(get_app_fn(rhs))) { - // Two projection applications - // pr_1 ... =?= pr_2 ... - // where pr_1 != pr_2 and both are not stuck - set_conflict(j); - return Failed; - } else { - return Continue; - } - } - - status reduce_proj_and_check(expr const & lhs, expr const & rhs, justification const & j) { - lean_assert(is_projection_app(lhs)); - lean_assert(!is_projection_app(rhs)); - { - // First try to reduce projection - constraint_seq new_cs; - expr new_lhs = whnf(lhs, new_cs); - if (lhs != new_lhs) - return to_status(is_def_eq(new_lhs, rhs, j) && process_constraints(new_cs)); - } - { - constraint_seq new_cs; - expr new_rhs = whnf(rhs, new_cs); - if (rhs != new_rhs) - return to_status(is_def_eq(lhs, new_rhs, j) && process_constraints(new_cs)); - } - return Continue; - } - - /** \brief Process an equality constraints. */ - bool process_eq_constraint(constraint const & c) { - lean_assert(is_eq_cnstr(c)); - // instantiate assigned metavariables - status st = instantiate_eq_cnstr(c); - if (st != Continue) return st == Solved; - - if (auto d = is_owned(c)) { - // Metavariable in the constraint is owned by choice constraint. - // So, we postpone this constraint. - add_cnstr_after(c, *d); - return true; - } - - st = process_eq_constraint_core(c); - if (st != Continue) return st == Solved; - - expr const & lhs = cnstr_lhs_expr(c); - expr const & rhs = cnstr_rhs_expr(c); - bool is_proj_lhs = is_projection_app(lhs); - bool is_proj_rhs = is_projection_app(rhs); - bool is_proj_stuck_lhs = is_proj_lhs && m_tc->is_stuck(lhs); - bool is_proj_stuck_rhs = is_proj_rhs && m_tc->is_stuck(rhs); - - if (is_proj_lhs && is_proj_rhs && !is_proj_stuck_lhs && !is_proj_stuck_rhs) { - if (const_name(get_app_fn(lhs)) == const_name(get_app_fn(rhs))) { - return process_same_projection_projection(c); - } else { - st = reduce_both_proj_and_check(lhs, rhs, c.get_justification()); - if (st != Continue) return st == Solved; - } - } else if (is_proj_lhs && !is_proj_stuck_lhs && !is_proj_rhs && !is_meta(rhs)) { - st = reduce_proj_and_check(lhs, rhs, c.get_justification()); - if (st != Continue) return st == Solved; - } else if (is_proj_rhs && !is_proj_stuck_rhs && !is_proj_lhs && !is_meta(lhs)) { - st = reduce_proj_and_check(rhs, lhs, c.get_justification()); - if (st != Continue) return st == Solved; - } - - if (is_eq_deltas(lhs, rhs)) { - // we need to create a backtracking point for this one - add_cnstr(c, cnstr_group::Basic); - return true; - } else if (is_meta(lhs) && is_meta(rhs)) { - // flex-flex constraints are delayed the most. - unsigned cidx = add_cnstr(c, cnstr_group::FlexFlex); - add_meta_occ(lhs, cidx); - add_meta_occ(rhs, cidx); - return true; - } else if (m_tc->may_reduce_later(lhs) || - m_tc->may_reduce_later(rhs)) { - unsigned cidx = add_cnstr(c, cnstr_group::PluginDelayed); - add_meta_occs(lhs, cidx); - add_meta_occs(rhs, cidx); - if (is_proj_lhs && is_proj_rhs) - return preprocess_projection_projection(c); - else - return true; - } else if (is_meta(lhs)) { - // flex-rigid constraints are delayed. - unsigned cidx = add_cnstr(c, cnstr_group::FlexRigid); - add_meta_occ(lhs, cidx); - return true; - } else if (is_meta(rhs)) { - // flex-rigid constraints are delayed. - unsigned cidx = add_cnstr(c, cnstr_group::FlexRigid); - add_meta_occ(rhs, cidx); - return true; - } else { - // this constraints require the unifier plugin to be solved - add_cnstr(c, cnstr_group::Basic); - return true; - } - } - - /** - \brief Process a universe level constraints of the form ?m =?= rhs. It fails if rhs contains \c ?m and - is definitely bigger than \c ?m. - - TODO(Leo): we should improve this method in the future. It is doing only very basic things. - */ - status process_metavar_eq(level const & lhs, level const & rhs, justification const & j) { - if (!is_meta(lhs)) - return Continue; - bool contains = occurs_meta(lhs, rhs); - if (contains) { - if (is_succ(rhs)) { - set_conflict(j); - return Failed; - } else { - return Continue; - } - } - lean_assert(!m_subst.is_assigned(lhs)); - if (assign(lhs, rhs, j)) { - return Solved; - } else { - set_conflict(j); - return Failed; - } - } - - /** \brief Process a universe level contraints. */ - bool process_level_eq_constraint(constraint const & c) { - lean_assert(is_level_eq_cnstr(c)); - // instantiate assigned metavariables - constraint new_c = instantiate_metavars(c).first; - level lhs = cnstr_lhs_level(new_c); - level rhs = cnstr_rhs_level(new_c); - justification jst = new_c.get_justification(); - - // normalize lhs and rhs - lhs = normalize(lhs); - rhs = normalize(rhs); - // eliminate outermost succs - while (is_succ(lhs) && is_succ(rhs)) { - lhs = succ_of(lhs); - rhs = succ_of(rhs); - } - - if (lhs == rhs) - return true; // trivial constraint - - if (!has_meta(lhs) && !has_meta(rhs)) { - set_conflict(jst); - return false; // trivial failure - } - - status st = process_metavar_eq(lhs, rhs, jst); - if (st != Continue) return st == Solved; - st = process_metavar_eq(rhs, lhs, jst); - if (st != Continue) return st == Solved; - - if (lhs != cnstr_lhs_level(new_c) || rhs != cnstr_rhs_level(new_c)) - new_c = mk_level_eq_cnstr(lhs, rhs, new_c.get_justification()); - - add_cnstr(new_c, cnstr_group::FlexRigid); - return true; - } - - bool preprocess_choice_constraint(constraint c) { - if (!cnstr_on_demand(c)) { - unsigned cidx = add_cnstr(c, get_choice_cnstr_group(c)); - if (cnstr_is_owner(c)) { - expr m = get_app_fn(cnstr_expr(c)); - lean_assert(is_metavar(m)); - m_owned_map.insert(mlocal_name(m), cidx); - } - return true; - } else { - expr m = cnstr_expr(c); - // choice constraints that are marked as "on demand" - // are only processed when all metavariables in the - // type of m have been instantiated. - expr type; - justification jst; - if (auto it = m_type_map.find(m)) { - // Type of m is already cached in m_type_map - type = it->first; - jst = it->second; - } else { - // Type of m is not cached yet, we - // should infer it, process generated - // constraints and save the result in - // m_type_map. - constraint_seq cs; - optional t = infer(m, cs); - if (!t) { - set_conflict(c.get_justification()); - return false; - } - if (!process_constraints(cs, c.get_justification())) - return false; - type = *t; - m_type_map.insert(m, mk_pair(type, justification())); - } - // Try to instantiate metavariables in type - pair type_jst = m_subst.instantiate_metavars(type); - if (type_jst.first != type) { - // Type was modified by instantiation, - // we update the constraint justification, - // and store the new type in m_type_map - jst = mk_composite1(jst, type_jst.second); - type = type_jst.first; - c = update_justification(c, mk_composite1(c.get_justification(), jst)); - m_type_map.insert(m, mk_pair(type, jst)); - } - unsigned cidx = add_cnstr(c, cnstr_group::ClassInstance); - if (!add_meta_occs(type, cidx)) { - // type does not contain metavariables... - // so this "on demand" constraint is ready to be solved - m_cnstrs.erase(cnstr(c, cidx)); - add_cnstr(c, cnstr_group::Basic); - m_type_map.erase(m); - } - return true; - } - } - - /** - \brief Process the given constraint \c c. "Easy" constraints are solved, and the remaining ones - are added to the constraint queue m_cnstrs. By "easy", see the methods - #process_eq_constraint and #process_level_eq_constraint. - */ - bool process_constraint(constraint const & c) { - if (in_conflict()) - return false; - check_full(); - lean_trace("unifier", tout() << "process: " << c << "\n";); - switch (c.kind()) { - case constraint_kind::Choice: - return preprocess_choice_constraint(c); - case constraint_kind::Eq: - return process_eq_constraint(c); - case constraint_kind::LevelEq: - return process_level_eq_constraint(c); - } - lean_unreachable(); // LCOV_EXCL_LINE - } - - /** - \brief Process constraint with index \c cidx. The constraint is removed - from the constraint queue, and the method #process_constraint is invoked. - */ - bool process_constraint_cidx(unsigned cidx) { - if (in_conflict()) - return false; - cnstr c(*g_dont_care_cnstr, cidx); - if (auto it = m_cnstrs.find(c)) { - constraint c2 = it->first; - m_cnstrs.erase(c); - return process_constraint(c2); - } - return true; - } - - void add_case_split(std::unique_ptr && cs) { - m_case_splits.push_back(std::move(cs)); - } - - // This method is used only for debugging purposes. - void display(std::ostream & out, justification const & j, unsigned indent = 0) { - for (unsigned i = 0; i < indent; i++) - out << " "; - out << j.pp(mk_print_formatter_factory()(m_env, options(), m_tc->get_type_context()), nullptr, m_subst) << "\n"; - if (j.is_composite()) { - display(out, composite_child1(j), indent+2); - display(out, composite_child2(j), indent+2); - } - } - - void pop_case_split() { - m_case_splits.pop_back(); - } - - bool resolve_conflict() { - lean_assert(in_conflict()); - while (!m_case_splits.empty()) { - check_system(); - justification conflict = *m_conflict; - std::unique_ptr & d = m_case_splits.back(); - if (!m_config.m_nonchronological || depends_on(conflict, d->m_assumption_idx)) { - d->m_failed_justifications = mk_composite1(d->m_failed_justifications, conflict); - if (d->next(*this)) { - reset_conflict(); - return true; - } - } else { - pop_case_split(); - } - } - return false; - } - - bool next_lazy_constraints_case_split(lazy_constraints_case_split & cs) { - auto r = cs.m_tail.pull(); - if (r) { - cs.restore_state(*this); - lean_assert(!in_conflict()); - cs.m_tail = r->second; - return process_constraints(r->first, mk_composite1(cs.get_jst(), mk_assumption_justification(cs.m_assumption_idx))); - } else { - // update conflict - update_conflict(mk_composite1(*m_conflict, cs.m_failed_justifications)); - pop_case_split(); - return false; - } - } - - bool process_lazy_constraints(lazy_list const & l, justification const & j) { - auto r = l.pull(); - if (r) { - if (r->second.is_nil()) { - // there is only one alternative - return process_constraints(r->first, j); - } else { - justification a = mk_assumption_justification(m_next_assumption_idx); - add_case_split(std::unique_ptr(new lazy_constraints_case_split(*this, j, r->second))); - return process_constraints(r->first, mk_composite1(j, a)); - } - } else { - set_conflict(j); - return false; - } - } - - /** \brief Given a constraint of the form - f a_1 ... a_n =?= f b_1 ... b_n - Return singleton stream with the possible solution - a_i =?= b_i - If c is not of the expected form, then return the empty stream. - */ - lazy_list process_const_const_cnstr(constraint const & c) { - if (!is_eq_cnstr(c)) - return lazy_list(); - expr const & lhs = cnstr_lhs_expr(c); - expr const & rhs = cnstr_rhs_expr(c); - expr const & f_lhs = get_app_fn(lhs); - expr const & f_rhs = get_app_fn(rhs); - if (!is_constant(f_lhs) || !is_constant(f_rhs) || const_name(f_lhs) != const_name(f_rhs)) - return lazy_list(); - justification const & j = c.get_justification(); - constraint_seq cs; - auto fcs = m_tc->is_def_eq(f_lhs, f_rhs, j); - if (!fcs.first) - return lazy_list(); - cs = fcs.second; - buffer args_lhs, args_rhs; - get_app_args(lhs, args_lhs); - get_app_args(rhs, args_rhs); - if (args_lhs.size() != args_rhs.size()) - return lazy_list(); - for (unsigned i = 0; i < args_lhs.size(); i++) { - auto acs = m_tc->is_def_eq(args_lhs[i], args_rhs[i], j); - if (!acs.first) - return lazy_list(); - cs = acs.second + cs; - } - return lazy_list(cs.to_list()); - } - - /** Return true iff t is a projection application */ - bool is_projection_app(expr const & t) { - expr const & f = get_app_fn(t); - return is_constant(f) && is_projection(m_env, const_name(f)); - } - - // See #preprocess_projection_projection - bool is_preprocess_projection_projection_target(projection_info const * info, buffer const & args) { - if (!info->m_inst_implicit) - return false; - if (args.size() < info->m_nparams+1) - return false; - unsigned sidx = info->m_nparams; - if (!has_expr_metavar(args[sidx])) - return false; - for (unsigned i = 0; i < info->m_nparams; i++) - if (has_expr_metavar(args[i])) - return true; - // all parameters do not have metavariables, thus type class resolution will be triggered - // to synthesize the args[sidx] - return false; - } - - /** - For constraints of the form - pr_1 A_1 s_1 a_1 =?= pr_2 A_2 s_2 a_2 - where pr is a projection, A_{1,2} are parameters, s_{1,2} the structure, and a_{1,2} arguments. - If s_1/A_1 or s_2/A_2 contain metavariables, we add the constraint - infer_type(pr_1 A_1 s_1) =?= infer_type(pr_2 A_2 s_2) - when pr_{1,2} is the projection of a class. The new constraint may force some of the meta-variables occurring - in the parameters to be assigned, and then this assignment will trigger type class resolution at s_{1,2} - - \remark Note that whenever we use this step we may be missing solutions. - This should only happen in very unusual circumstances. We may add an option to disable this - step in the future. This step is essential for processing the algebraic hierarchy. - */ - bool preprocess_projection_projection(constraint const & c) { - expr const & lhs = cnstr_lhs_expr(c); - expr const & rhs = cnstr_rhs_expr(c); - lean_assert(is_projection_app(lhs) && is_projection_app(rhs)); - buffer lhs_args, rhs_args; - expr const & f_lhs = get_app_args(lhs, lhs_args); - expr const & f_rhs = get_app_args(rhs, rhs_args); - projection_info const * info_lhs = get_projection_info(m_env, const_name(f_lhs)); - projection_info const * info_rhs = get_projection_info(m_env, const_name(f_rhs)); - lean_assert(info_lhs); - lean_assert(info_rhs); - if (!is_preprocess_projection_projection_target(info_lhs, lhs_args) && - !is_preprocess_projection_projection_target(info_rhs, rhs_args)) - return true; // do nothing, preprocessing step will not help - unsigned l_nparams = info_lhs->m_nparams; - unsigned r_nparams = info_rhs->m_nparams; - if (lhs_args.size() - l_nparams != rhs_args.size() - r_nparams) - return true; // the number of arguments to the projection data do not match. - expr new_lhs_app = mk_app(f_lhs, l_nparams+1, lhs_args.data()); - expr new_rhs_app = mk_app(f_rhs, r_nparams+1, rhs_args.data()); - constraint_seq cs; - auto t1 = infer(new_lhs_app, cs); - auto t2 = infer(new_rhs_app, cs); - if (!t1 || !t2) - return true; // failed to infer types - if (!process_constraints(cs)) - return false; - return is_def_eq(*t1, *t2, c.get_justification()); - } - - /** \brief Return true iff lhs and rhs are of the form (pr ...) where pr is a projection */ - bool is_same_projection_projection(expr const & lhs, expr const & rhs) { - expr const & f_lhs = get_app_fn(lhs); - expr const & f_rhs = get_app_fn(rhs); - return - is_constant(f_lhs) && is_constant(f_rhs) && - const_name(f_lhs) == const_name(f_rhs) && - is_projection(m_env, const_name(f_lhs)); - } - - /** \brief Return true iff c is of the form (pr ...) =?= (pr ...) where pr is a projection. */ - bool is_same_projection_projection(constraint const & c) { - lean_assert(is_eq_cnstr(c)); - return is_same_projection_projection(cnstr_lhs_expr(c), cnstr_rhs_expr(c)); - } - - /** - \brief Reduce constraint - pr a_1 ... a_n =?= pr b_1 ... b_n - into - a_1 =?= b_1, ..., a_n =?= b_n - where pr is a projection - - \remark This step is only performed at process_next. - Moreover, we only do it when the "major premise" of both projections is not a constructor. - */ - bool process_same_projection_projection(constraint const & c) { - lean_assert(is_same_projection_projection(c)); - buffer lhs_args, rhs_args; - expr const & f_lhs = get_app_args(cnstr_lhs_expr(c), lhs_args); - expr const & f_rhs = get_app_args(cnstr_rhs_expr(c), rhs_args); - justification const & j = c.get_justification(); - return process_levels(const_levels(f_lhs), const_levels(f_rhs), j) && process_args(lhs_args, rhs_args, j); - } - - /** \brief Return true iff c is of the form (pr_1 ...) =?= (pr_2 ...) where pr_1 and pr_2 are projections. */ - bool is_projection_projection(constraint const & c) { - return is_projection_app(cnstr_lhs_expr(c)) && is_projection_app(cnstr_rhs_expr(c)); - } - - /** - \brief Postpone constraints of the form - pr_1 a_1 ... a_n =?= pr_2 b_1 ... b_m - when pr_1 and pr_2 are projections and pr_1 != pr_2 - - If the constraint cannot be postponed anymore, we just fail. - - \remark This step is only performed at process_next. - */ - bool process_projection_projection(constraint const & c, unsigned cidx) { - lean_assert(is_projection_projection(c)); - // postpone constraint - if (cidx < get_group_first_index(cnstr_group::ClassInstance)) { - // pospone constraint - unsigned cidx = add_cnstr(c, cnstr_group::Epilogue); - add_meta_occs(cnstr_lhs_expr(c), cidx); - add_meta_occs(cnstr_rhs_expr(c), cidx); - return true; - } else { - set_conflict(c.get_justification()); - return false; - } - } - - /** \brief Return true iff c is of the form (pr ...) =?= t, where - pr is a stuck projection. */ - bool is_projection_lhs(constraint const & c) { - lean_assert(is_eq_cnstr(c)); - return is_projection_app(cnstr_lhs_expr(c)) && m_tc->is_stuck(cnstr_lhs_expr(c)); - } - - /** \brief Return true iff c is of the form t =?= (pr ...), where - pr is a stuck projection. */ - bool is_projection_rhs(constraint const & c) { - lean_assert(is_eq_cnstr(c)); - return is_projection_app(cnstr_rhs_expr(c)) && m_tc->is_stuck(cnstr_rhs_expr(c)); - } - - /** \brief Process constraints of the form - (pr_i ... M ..) =?= t - If the "major premise" M of (pr_i ... M ...) is stuck, we reduce the constraint above into - M =?= (mk ?M_1 ... ?M_k) - (?M_i ...) =?= t - where ?M_i's are fresh metavariables - - If M is not stuck, the procedure signs a conflict - - \remark This step is only performed at process_next. - */ - bool process_projection_eq(expr const & lhs, expr const & rhs, justification const & j) { - lean_assert(is_projection_app(lhs)); - buffer pr_args; - expr const & pr = get_app_args(lhs, pr_args); - projection_info const * info = get_projection_info(m_env, const_name(pr)); - unsigned nparams = info->m_nparams; - unsigned mkidx = nparams; - if (pr_args.size() < nparams+1) { - set_conflict(j); - return false; - } - auto stuck_it = m_tc->is_stuck(pr_args[mkidx]); - if (!stuck_it) { - // TODO(Lean): normalize, and try is_stuck again? - // We don't do it because it seems there is very little gain, and it may negatively affect performance. - return false; - } - expr meta = *stuck_it; - lean_assert(is_meta(meta)); - buffer meta_args; - expr const & mvar = get_app_args(meta, meta_args); - expr const & mvar_type = mlocal_type(mvar); - constraint_seq cs; - expr mk = mk_app(mk_constant(info->m_constructor, const_levels(pr)), nparams, pr_args.data()); - auto it = infer(mk, cs); - if (!it) { - set_conflict(j); - return false; - } - // Remark: this is another example where it would be really nice if every - // unification constraint had a context associated with it. - expr mk_type = whnf(*it, cs); - optional mk_i; - unsigned i = 0; - while (is_pi(mk_type)) { - expr new_mvar = mk_app(mk_aux_metavar_for(mvar_type), meta_args); - mk = mk_app(mk, new_mvar); - if (info->m_i == i) - mk_i = new_mvar; - i++; - mk_type = whnf(instantiate(binding_body(mk_type), new_mvar), cs); - } - if (!mk_i) { - set_conflict(j); - return false; - } - expr Mi = mk_app(*mk_i, pr_args.size() - mkidx - 1, pr_args.data() + mkidx + 1); - cs += mk_eq_cnstr(meta, mk, j); - cs += mk_eq_cnstr(Mi, rhs, j); - return process_constraints(cs); - } - - bool process_plugin_constraint(constraint const & c) { - lean_assert(!is_choice_cnstr(c)); - lazy_list alts; - alts = append(alts, process_const_const_cnstr(c)); - return process_lazy_constraints(alts, c.get_justification()); - } - - bool process_choice_constraint(constraint const & c) { - lean_assert(is_choice_cnstr(c)); - expr const & m = cnstr_expr(c); - choice_fn const & fn = cnstr_choice_fn(c); - if (cnstr_is_owner(c)) { - // choice will have a chance to assign m, so - // we remove the "barrier" that was preventing m from being assigned. - m_owned_map.erase(mlocal_name(get_app_fn(m))); - } - expr m_type; - - constraint_seq cs; - if (auto type = infer(m, cs)) { - m_type = *type; - if (!process_constraints(cs)) - return false; - } else { - set_conflict(c.get_justification()); - return false; - } - auto m_type_jst = m_subst.instantiate_metavars(m_type); - lazy_list alts = fn(m, m_type_jst.first, m_subst); - return process_lazy_constraints(alts, mk_composite1(c.get_justification(), m_type_jst.second)); - } - - bool next_simple_case_split(simple_case_split & cs) { - if (!is_nil(cs.m_tail)) { - cs.restore_state(*this); - lean_assert(!in_conflict()); - constraints c = head(cs.m_tail); - cs.m_tail = tail(cs.m_tail); - return process_constraints(c, mk_composite1(cs.get_jst(), mk_assumption_justification(cs.m_assumption_idx))); - } else { - // update conflict - update_conflict(mk_composite1(*m_conflict, cs.m_failed_justifications)); - pop_case_split(); - return false; - } - } - - bool unfold_delta(constraint const & c, justification const & extra_j) { - expr const & lhs = cnstr_lhs_expr(c); - expr const & rhs = cnstr_rhs_expr(c); - buffer lhs_args, rhs_args; - justification j = c.get_justification(); - expr lhs_fn = get_app_rev_args(lhs, lhs_args); - expr rhs_fn = get_app_rev_args(rhs, rhs_args); - declaration d = *m_env.find(const_name(lhs_fn)); - expr lhs_fn_val = instantiate_value_univ_params(d, const_levels(lhs_fn)); - expr rhs_fn_val = instantiate_value_univ_params(d, const_levels(rhs_fn)); - expr t = apply_beta(lhs_fn_val, lhs_args.size(), lhs_args.data()); - expr s = apply_beta(rhs_fn_val, rhs_args.size(), rhs_args.data()); - auto dcs = m_tc->is_def_eq(t, s, j); - if (dcs.first) { - constraints cnstrs = dcs.second.to_list(); - return process_constraints(cnstrs, extra_j); - } else { - set_conflict(j); - return false; - } - } - - bool next_delta_unfold_case_split(delta_unfold_case_split & cs) { - if (!cs.m_done) { - cs.restore_state(*this); - cs.m_done = true; - constraint const & c = cs.m_cnstr; - justification j = mk_composite1(cs.get_jst(), mk_assumption_justification(cs.m_assumption_idx)); - return unfold_delta(c, j); - } else { - // update conflict - update_conflict(mk_composite1(*m_conflict, cs.m_failed_justifications)); - pop_case_split(); - return false; - } - } - - // Make sure the two lists of levels are definitionally equal. - bool process_levels(levels lhs_lvls, levels rhs_lvls, justification const & j) { - while (!is_nil(lhs_lvls)) { - if (is_nil(rhs_lvls)) - return false; - level lhs = head(lhs_lvls); - level rhs = head(rhs_lvls); - if (!process_constraint(mk_level_eq_cnstr(lhs, rhs, j))) - return false; - lhs_lvls = tail(lhs_lvls); - rhs_lvls = tail(rhs_lvls); - } - return is_nil(rhs_lvls); - } - - // Make sure the two buffers of arguments are definitionally equal - bool process_args(buffer const & lhs_args, buffer const & rhs_args, justification const & j) { - if (lhs_args.size() != rhs_args.size()) - return false; - unsigned i = lhs_args.size(); - while (i > 0) { - --i; - if (!is_def_eq(lhs_args[i], rhs_args[i], j)) - return false; - } - return true; - } - - // Return true if we should case-split on a delta constraint where \c lhs is the left-hand-side - bool split_delta(expr const & lhs) { - expr lhs_fn = get_app_fn(lhs); - lean_assert(is_constant(lhs_fn)); - declaration d = *m_env.find(const_name(lhs_fn)); - return (m_config.m_kind == unifier_kind::Liberal && (module::is_definition(m_env, d.get_name()) || is_reducible(m_env, d.get_name()))); - } - - /** - \brief Solve constraints of the form (f a_1 ... a_n) =?= (f b_1 ... b_n) where f can be expanded. - We consider two possible solutions: - 1) a_1 =?= b_1, ..., a_n =?= b_n - 2) t =?= s, where t and s are the terms we get after expanding f - */ - bool process_delta(constraint const & c) { - lean_assert(is_delta_cnstr(c)); - expr const & lhs = cnstr_lhs_expr(c); - expr const & rhs = cnstr_rhs_expr(c); - buffer lhs_args, rhs_args; - justification j = c.get_justification(); - expr lhs_fn = get_app_rev_args(lhs, lhs_args); - expr rhs_fn = get_app_rev_args(rhs, rhs_args); - declaration d = *m_env.find(const_name(lhs_fn)); - levels lhs_lvls = const_levels(lhs_fn); - levels rhs_lvls = const_levels(rhs_fn); - if (length(lhs_lvls) != length(rhs_lvls) || - d.get_num_univ_params() != length(lhs_lvls)) { - // the constraint is not well-formed, this can happen when users are abusing the API - set_conflict(j); - return false; - } - - if (lhs_args.size() != rhs_args.size()) - return unfold_delta(c, justification()); - - justification a; - if (split_delta(lhs)) { - // add case_split for t =?= s - a = mk_assumption_justification(m_next_assumption_idx); - add_case_split(std::unique_ptr(new delta_unfold_case_split(*this, j, c))); - } - - // process first case - justification new_j = mk_composite1(j, a); - return process_levels(lhs_lvls, rhs_lvls, new_j) && process_args(lhs_args, rhs_args, new_j); - } - - /** \brief Return true iff \c c is a flex-rigid constraint. */ - static bool is_flex_rigid(constraint const & c) { - if (!is_eq_cnstr(c)) - return false; - bool is_lhs_meta = is_meta(cnstr_lhs_expr(c)); - bool is_rhs_meta = is_meta(cnstr_rhs_expr(c)); - return is_lhs_meta != is_rhs_meta; - } - - /** \brief Return true iff \c c is a flex-flex constraint */ - static bool is_flex_flex(constraint const & c) { - return is_eq_cnstr(c) && is_meta(cnstr_lhs_expr(c)) && is_meta(cnstr_rhs_expr(c)); - } - - /** \brief Append the auxiliary constraints \c aux to each alternative in \c alts */ - void append_auxiliary_constraints(buffer & alts, list const & aux) { - if (is_nil(aux)) - return; - for (constraints & cs : alts) - cs = append(aux, cs); - } - - /** \see ensure_sufficient_args */ - expr ensure_sufficient_args_core(expr mtype, unsigned nargs, unsigned i, constraint_seq & cs) { - if (i == nargs) - return mtype; - mtype = m_tc->ensure_pi(mtype, cs); - expr local = mk_local_for(mtype); - expr body = instantiate(binding_body(mtype), local); - return Pi(local, ensure_sufficient_args_core(body, nargs, i+1, cs)); - } - - /** \brief Make sure mtype is a Pi of size at least nargs. - If it is not, we use ensure_pi and (potentially) add new constaints to enforce it. - */ - expr ensure_sufficient_args(expr const & mtype, unsigned nargs, constraint_seq & cs) { - expr t = mtype; - unsigned num = 0; - while (is_pi(t)) { - num++; - t = binding_body(t); - } - if (num >= nargs) - return mtype; - return ensure_sufficient_args_core(mtype, nargs, 0, cs); - } - - /** \brief Auxiliary functional object for implementing process_flex_rigid_core */ - class flex_rigid_core_fn { - unifier_fn & u; - expr const & lhs; - buffer margs; - expr const & m; - expr const & rhs; - justification j; - buffer & alts; // result: alternatives - bool imitation_only; // if true, then only imitation step is used - - optional _has_meta_args; - - bool cheap() const { return u.m_config.m_kind == unifier_kind::Cheap; } - bool pattern() const { return u.m_config.m_pattern; } - - old_type_checker & tc() { - return *u.m_tc; - } - - old_type_checker & restricted_tc() { - return *u.m_flex_rigid_tc; - } - - /** \brief Return true if margs contains an expression \c e s.t. is_meta(e) */ - bool has_meta_args() { - if (!_has_meta_args) { - _has_meta_args = std::any_of(margs.begin(), margs.end(), - [](expr const & e) { return is_meta(e); }); - } - return *_has_meta_args; - } - - /** - \brief Given t - Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), B[x_1, ..., x_n] - return - fun (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), v[x_1, ... x_n] - - \remark v has free variables. - */ - expr mk_lambda_for(unsigned i, expr const & t, expr const & v) { - if (i < margs.size()) { - return mk_lambda(binding_name(t), binding_domain(t), mk_lambda_for(i+1, binding_body(t), v), binding_info(t)); - } else { - return v; - } - } - - expr mk_lambda_for(expr const & t, expr const & v) { - return mk_lambda_for(0, t, v); - } - - /** \brief Return true if \c local occurs once in the buffer \c es. */ - bool local_occurs_once(expr const & local, buffer const & es) { - bool found = false; - for (expr const & e : es) { - if (is_local(e) && mlocal_name(e) == mlocal_name(local)) { - if (found) - return false; - found = true; - } - } - return true; - } - - /** \brief Make sure mtype is a Pi of size at least margs.size(). */ - expr ensure_sufficient_args(expr const & mtype, constraint_seq & cs) { - return u.ensure_sufficient_args(mtype, margs.size(), cs); - } - - /** - \brief Given - m := a metavariable ?m - rhs := sort, constant - Then solve (?m a_1 ... a_k) =?= rhs, by returning the constraint - ?m =?= fun (x1 ... x_k), rhs - */ - void mk_simple_imitation() { - lean_assert(is_metavar(m)); - lean_assert(is_sort(rhs) || is_constant(rhs)); - expr const & mtype = mlocal_type(m); - constraint_seq cs; - expr new_mtype = ensure_sufficient_args(mtype, cs); - cs = cs + mk_eq_cnstr(m, mk_lambda_for(new_mtype, rhs), j); - alts.push_back(cs.to_list()); - } - - bool restricted_is_def_eq(expr const & marg, expr const & rhs, justification const & j, constraint_seq & cs) { - try { - if (restricted_tc().is_def_eq(marg, rhs, j, cs)) { - return true; - } else { - return false; - } - } catch (exception & ex) { - return false; - } - } - - /** - Given, - m := a metavariable ?m - margs := [a_1 ... a_k] - We say a unification problem (?m a_1 ... a_k) =?= rhs uses "simple nonlocal i-th projection" when - - 1) rhs is not a local constant - 2) is_def_eq(a_i, rhs) does not fail - - In this case, we add - a_i =?= rhs - ?m =?= fun x_1 ... x_k, x_i - to alts as a possible solution. - */ - void mk_simple_nonlocal_projection(unsigned i) { - expr const & mtype = mlocal_type(m); - unsigned vidx = margs.size() - i - 1; - expr const & marg = margs[i]; - constraint_seq cs; - auto new_mtype = ensure_sufficient_args(mtype, cs); - // Remark: we should not use mk_eq_cnstr(marg, rhs, j) since is_def_eq may be able to reduce them. - // The unifier assumes the eq constraints are reduced. - if (tc().is_def_eq_types(marg, rhs, j, cs) && - restricted_is_def_eq(marg, rhs, j, cs)) { - expr v = mk_lambda_for(new_mtype, mk_var(vidx)); - cs = cs + mk_eq_cnstr(m, v, j); - alts.push_back(cs.to_list()); - } - } - - /** - Given, - m := a metavariable ?m - margs := [a_1 ... a_k] - We say a unification problem (?m a_1 ... a_k) =?= rhs uses "simple projections" when - - If (rhs and a_i are *not* local constants) OR (rhs is a local constant and a_i is a metavariable application), - then we add the constraints - a_i =?= rhs - ?m =?= fun x_1 ... x_k, x_i - to alts as a possible solution. - - If rhs is a local constant and a_i == rhs, then we add the constraint - ?m =?= fun x_1 ... x_k, x_i - to alts as a possible solution when a_i is the same local constant or a metavariable application - */ - void mk_simple_projections() { - lean_assert(is_metavar(m)); - lean_assert(!is_meta(rhs)); - expr const & mtype = mlocal_type(m); - unsigned i = margs.size(); - while (i > 0) { - unsigned vidx = margs.size() - i; - --i; - expr const & marg = margs[i]; - if ((!is_local(marg) && !is_local(rhs)) || (is_meta(marg) && is_local(rhs))) { - // if rhs is not local, then we only add projections for the nonlocal arguments of lhs - mk_simple_nonlocal_projection(i); - if (cheap()) - return; - } else if (is_local(marg) && is_local(rhs) && mlocal_name(marg) == mlocal_name(rhs)) { - // if the argument is local, and rhs is equal to it, then we also add a projection - constraint_seq cs; - auto new_mtype = ensure_sufficient_args(mtype, cs); - expr v = mk_lambda_for(new_mtype, mk_var(vidx)); - cs = cs + mk_eq_cnstr(m, v, j); - alts.push_back(cs.to_list()); - if (cheap()) - return; - } - } - } - - void mk_app_projections() { - lean_assert(is_metavar(m)); - lean_assert(is_app(rhs)); - if (!pattern() && !cheap()) { - expr const & f = get_app_fn(rhs); - lean_assert(is_constant(f) || is_local(f)); - if (is_local(f)) { - unsigned i = margs.size(); - while (i > 0) { - --i; - if (!(is_local(margs[i]) && mlocal_name(margs[i]) == mlocal_name(f))) - mk_simple_nonlocal_projection(i); - } - } else { - mk_simple_projections(); - } - } - } - - /** \brief Create the local context \c locals for the imitation step. - */ - void mk_local_context(buffer & locals, constraint_seq & cs) { - expr mtype = mlocal_type(m); - unsigned nargs = margs.size(); - mtype = ensure_sufficient_args(mtype, cs); - expr it = mtype; - for (unsigned i = 0; i < nargs; i++) { - expr d = instantiate_rev(binding_domain(it), locals.size(), locals.data()); - auto d_jst = u.m_subst.instantiate_metavars(d); - d = d_jst.first; - j = mk_composite1(j, d_jst.second); - name n; - if (is_local(margs[i]) && local_occurs_once(margs[i], margs)) { - n = mlocal_name(margs[i]); - } else { - n = mk_fresh_name(); - } - expr local = mk_local(n, binding_name(it), d, binding_info(it)); - locals.push_back(local); - it = binding_body(it); - } - } - - expr mk_imitation_arg(expr const & arg, expr const & type, buffer const & locals, - constraint_seq & cs) { - // The following optimization is broken. It does not really work when we have dependent - // types. The problem is that the type of arg may depend on other arguments, - // and constraints are not generated to enforce it. - // - // Here is a minimal counterexample - // ?M A B a b H B b =?= heq.type_eq A B a b H - // with this optimization the imitation is - // - // ?M := fun (A B a b H B' b'), heq.type_eq A (?M1 A B a b H B' b') a (?M2 A B a b H B' b') H - // - // This imitation is only correct if - // typeof(H) is (heq A a (?M1 A B a b H B' b') (?M2 A B a b H B' b')) - // - // Adding an extra constraint is problematic since typeof(H) may contain local constants, - // and these local constants may have been "renamed" by mk_local_context above - // - // For now, we simply comment the optimization. - // - - // Broken optimization - // if (!has_meta_args() && is_local(arg) && contains_local(arg, locals)) { - // return arg; - // } - - // The following code is not affected by the problem above because we - // attach the type \c type to the new metavariables being created. - - // std::cout << "type: " << type << "\n"; - if (context_check(type, locals)) { - expr maux = mk_metavar(mk_fresh_name(), Pi(locals, type)); - // std::cout << " >> " << maux << " : " << mlocal_type(maux) << "\n"; - cs = mk_eq_cnstr(mk_app(maux, margs), arg, j) + cs; - return mk_app(maux, locals); - } else { - expr maux_type = mk_metavar(mk_fresh_name(), Pi(locals, mk_sort(mk_meta_univ(mk_fresh_name())))); - expr maux = mk_metavar(mk_fresh_name(), Pi(locals, mk_app(maux_type, locals))); - cs = mk_eq_cnstr(mk_app(maux, margs), arg, j) + cs; - return mk_app(maux, locals); - } - } - - void mk_app_imitation_core(expr const & f, buffer const & locals, constraint_seq & cs) { - buffer rargs; - get_app_args(rhs, rargs); - buffer sargs; - try { - expr f_type = tc().infer(f, cs); - for (expr const & rarg : rargs) { - f_type = tc().ensure_pi(f_type, cs); - expr d_type = binding_domain(f_type); - expr sarg = mk_imitation_arg(rarg, d_type, locals, cs); - sargs.push_back(sarg); - f_type = instantiate(binding_body(f_type), sarg); - } - } catch (exception&) {} - expr v = Fun(locals, mk_app(f, sargs)); - cs += mk_eq_cnstr(m, v, j); - alts.push_back(cs.to_list()); - } - - /** - \brief Given - m := a metavariable ?m - margs := [a_1 ... a_k] - rhs := (f b_1 ... b_n) - Then create the constraints - (?m_1 a_1 ... a_k) =?= b_1 - ... - (?m_n a_1 ... a_k) =?= b_n - ?m =?= fun (x_1 ... x_k), g (?m_1 x_1 ... x_k) ... (?m_n x_1 ... x_k) - - If f is a constant (or a macro), then g is f. - If f is a local constant, then we consider each a_i that is equal to f. - - Remark: we try to minimize the number of constraints (?m_i a_1 ... a_k) =?= b_i by detecting "easy" cases - that can be solved immediately. See \c mk_imitation_arg - */ - void mk_app_imitation() { - lean_assert(is_metavar(m)); - lean_assert(is_app(rhs)); - buffer locals; - constraint_seq cs; - flet let(j, j); // save j value - mk_local_context(locals, cs); - lean_assert(margs.size() == locals.size()); - expr const & f = get_app_fn(rhs); - lean_assert(is_constant(f) || is_macro(f) || is_local(f)); - if (is_local(f)) { - unsigned i = margs.size(); - while (i > 0) { - --i; - if (is_local(margs[i]) && mlocal_name(margs[i]) == mlocal_name(f)) { - constraint_seq new_cs = cs; - mk_app_imitation_core(locals[i], locals, new_cs); - } - } - } else { - lean_assert(is_constant(f) || is_macro(f)); - mk_app_imitation_core(f, locals, cs); - } - } - - /** - \brief Given - m := a metavariable ?m - margs := [a_1 ... a_k] - rhs := (fun/Pi (y : A), B y) - Then create the constraints - (?m_1 a_1 ... a_k) =?= A - (?m_2 a_1 ... a_k l) =?= B l - ?m =?= fun (x_1 ... x_k), fun/Pi (y : ?m_1 x_1 ... x_k), ?m_2 x_1 ... x_k y - where l is a fresh local constant. - */ - void mk_bindings_imitation() { - lean_assert(is_metavar(m)); - lean_assert(is_binding(rhs)); - constraint_seq cs; - buffer locals; - flet let(j, j); // save j value - mk_local_context(locals, cs); - lean_assert(margs.size() == locals.size()); - try { - // create a scope to make sure no constraints "leak" into the current state - expr rhs_A = binding_domain(rhs); - expr A_type = tc().infer(rhs_A, cs); - expr A = mk_imitation_arg(rhs_A, A_type, locals, cs); - expr local = mk_local(mk_fresh_name(), binding_name(rhs), A, binding_info(rhs)); - locals.push_back(local); - margs.push_back(local); - expr rhs_B = instantiate(binding_body(rhs), local); - expr B_type = tc().infer(rhs_B, cs); - expr B = mk_imitation_arg(rhs_B, B_type, locals, cs); - expr binding = is_pi(rhs) ? Pi(local, B) : Fun(local, B); - locals.pop_back(); - expr v = Fun(locals, binding); - cs += mk_eq_cnstr(m, v, j); - alts.push_back(cs.to_list()); - } catch (exception&) {} - margs.pop_back(); - } - - public: - flex_rigid_core_fn(unifier_fn & _u, expr const & _lhs, expr const & _rhs, - justification const & _j, buffer & _alts, - bool _imitation_only): - u(_u), lhs(_lhs), m(get_app_args(lhs, margs)), rhs(_rhs), j(_j), alts(_alts), - imitation_only(_imitation_only) {} - - void operator()() { - switch (rhs.kind()) { - case expr_kind::Var: case expr_kind::Meta: - lean_unreachable(); // LCOV_EXCL_LINE - case expr_kind::Local: - mk_simple_projections(); - break; - case expr_kind::Sort: case expr_kind::Constant: - if (!pattern() && !cheap() && !imitation_only) - mk_simple_projections(); - mk_simple_imitation(); - break; - case expr_kind::Pi: case expr_kind::Lambda: - if (!pattern() && !cheap() && !imitation_only) - mk_simple_projections(); - mk_bindings_imitation(); - break; - case expr_kind::Let: - case expr_kind::Macro: - lean_unreachable(); // LCOV_EXCL_LINE - case expr_kind::App: - if (!imitation_only) - mk_app_projections(); - mk_app_imitation(); - break; - } - } - }; - - void process_flex_rigid_core(expr const & lhs, expr const & rhs, justification const & j, - buffer & alts, bool imitation_only) { - flex_rigid_core_fn(*this, lhs, rhs, j, alts, imitation_only)(); - } - - /** \brief When lhs is an application (f ...), make sure that if any argument that is reducible to a - local constant is replaced with a local constant. - - \remark We store auxiliary constraints created in the reductions in \c aux. We return the new - "reduce" application. - */ - expr expose_local_args(expr const & lhs, justification const & j, buffer & aux) { - buffer margs; - expr m = get_app_args(lhs, margs); - bool modified = false; - for (expr & marg : margs) { - // Make sure that if marg is reducible to a local constant, then it is replaced with it. - if (!is_local(marg)) { - expr new_marg = whnf(marg, j, aux); - if (is_local(new_marg)) { - marg = new_marg; - modified = true; - } - } - } - return modified ? mk_app(m, margs) : lhs; - } - - optional expand_rhs(expr const & rhs) { - buffer args; - expr const & f = get_app_rev_args(rhs, args); - lean_assert(!is_local(f) && !is_constant(f) && !is_var(f) && !is_metavar(f)); - if (is_lambda(f)) { - return some_expr(apply_beta(f, args.size(), args.data())); - } else if (is_macro(f)) { - if (optional new_f = m_tc->expand_macro(f)) - return some_expr(mk_rev_app(*new_f, args.size(), args.data())); - } - return none_expr(); - } - - /** \brief When solving flex-rigid constraints lhs =?= rhs (lhs is of the form ?M a_1 ... a_n), - we consider an additional case-split where rhs is put in weak-head-normal-form when - - 1- At least one a_i is not a local constant - 2- rhs contains a local constant that is not equal to any a_i. - */ - bool use_flex_rigid_whnf_split(expr const & lhs, expr const & rhs) { - lean_assert(is_meta(lhs)); - if (m_config.m_kind != unifier_kind::Liberal) - return false; - buffer locals; - expr const * it = &lhs; - while (is_app(*it)) { - expr const & arg = app_arg(*it); - if (!is_local(arg)) - return true; // lhs contains non-local constant - locals.push_back(arg); - it = &(app_fn(*it)); - } - if (!context_check(rhs, locals)) - return true; // rhs contains local constant that is not in locals - return false; - } - - /** \brief Process a flex rigid constraint */ - bool process_flex_rigid(expr lhs, expr const & rhs, justification const & j) { - lean_assert(is_meta(lhs)); - lean_assert(!is_meta(rhs)); - if (is_app(rhs)) { - expr const & f = get_app_fn(rhs); - if (!is_local(f) && !is_constant(f)) { - if (auto new_rhs = expand_rhs(rhs)) { - lean_assert(*new_rhs != rhs); - return is_def_eq(lhs, *new_rhs, j); - } else { - return false; - } - } - } else if (is_macro(rhs)) { - if (auto new_rhs = expand_rhs(rhs)) { - lean_assert(*new_rhs != rhs); - return is_def_eq(lhs, *new_rhs, j); - } else { - return false; - } - } - - buffer aux; - lhs = expose_local_args(lhs, j, aux); - buffer alts; - process_flex_rigid_core(lhs, rhs, j, alts, false); - append_auxiliary_constraints(alts, to_list(aux.begin(), aux.end())); - if (use_flex_rigid_whnf_split(lhs, rhs)) { - expr rhs_whnf = flex_rigid_whnf(rhs, j, aux); - if (rhs_whnf != rhs) { - if (is_meta(rhs_whnf)) { - // it become a flex-flex constraint - alts.push_back(constraints(mk_eq_cnstr(lhs, rhs_whnf, j))); - } else { - buffer alts2; - process_flex_rigid_core(lhs, rhs_whnf, j, alts2, true); - append_auxiliary_constraints(alts2, to_list(aux.begin(), aux.end())); - alts.append(alts2); - } - } - } - - // std::cout << "FlexRigid\n"; - // for (auto cs : alts) { - // std::cout << " alternative\n"; - // for (auto c : cs) { - // std::cout << " >> " << c << "\n"; - // } - // } - - if (alts.empty()) { - set_conflict(j); - return false; - } else if (alts.size() == 1) { - // we don't need to create a backtracking point - return process_constraints(alts[0], justification()); - } else { - justification a = mk_assumption_justification(m_next_assumption_idx); - add_case_split(std::unique_ptr(new simple_case_split(*this, j, to_list(alts.begin() + 1, alts.end())))); - return process_constraints(alts[0], a); - } - } - - /** \brief Process a flex rigid constraint */ - bool process_flex_rigid(constraint const & c) { - lean_assert(is_flex_rigid(c)); - expr lhs = cnstr_lhs_expr(c); - expr rhs = cnstr_rhs_expr(c); - if (is_meta(lhs)) - return process_flex_rigid(lhs, rhs, c.get_justification()); - else - return process_flex_rigid(rhs, lhs, c.get_justification()); - } - - void postpone(constraint const & c) { - m_postponed = cons(c, m_postponed); - } - - void discard(constraint const & c) { - if (!m_config.m_discard) - postpone(c); - } - - // Auxiliary method used in process_flex_flex_approx - bool assign_flex_approx(expr const & m, expr const & v, justification const & j, constraint_seq & cs) { - lean_assert(m_config.m_discard); - buffer args; - expr const & fn = get_app_args(m, args); - lean_assert(is_metavar(fn)); - expr type = mlocal_type(fn); - type = ensure_sufficient_args(type, args.size(), cs); - buffer locals; - for (expr const & a : args) { - expr local = is_local(a) ? a : mk_local_for(type); - locals.push_back(local); - type = instantiate(binding_body(type), local); - } - return assign(m, fn, locals, v, j); - } - - bool process_flex_flex_approx(constraint const & c) { - lean_assert(m_config.m_discard); - // Try to solve constraint - // ?M_1 t_1 ... t_n =?= ?M_2 s_1 ... s_m - // by creating a fresh metavariable ?M using common local constants. - // If can't build approximate solution, then discard constraint. - expr const & lhs = cnstr_lhs_expr(c); - expr const & rhs = cnstr_rhs_expr(c); - buffer lhs_args, rhs_args; - get_app_args(lhs, lhs_args); - get_app_args(rhs, rhs_args); - buffer shared_locals; - unsigned sz = std::min(lhs_args.size(), rhs_args.size()); - unsigned i = 0; - for (; i < sz; i++) { - if (!is_local(lhs_args[i]) || !is_local(rhs_args[i]) || - mlocal_name(lhs_args[i]) != mlocal_name(rhs_args[i])) - break; - shared_locals.push_back(lhs_args[i]); - } - constraint_seq cs; - if (optional lhs_type = infer(lhs, cs)) { - expr new_type = Pi(shared_locals, *lhs_type); - if (!has_local(new_type)) { - expr new_mvar = mk_metavar(mk_fresh_name(), new_type); - expr new_val = mk_app(new_mvar, shared_locals); - justification const & j = c.get_justification(); - return - assign_flex_approx(lhs, new_val, j, cs) && - assign_flex_approx(rhs, new_val, j, cs) && - process_constraints(cs, c.get_justification()); - } - } - // Failed to generate approximate solution. - // TODO(Leo): generate an error, or just ingore? - // we are currently just ignoring... - return true; - } - - - bool process_flex_flex(constraint const & c) { - expr const & lhs = cnstr_lhs_expr(c); - expr const & rhs = cnstr_rhs_expr(c); - // We ignore almost all flex-flex constraints. - // We just handle flex_flex "first-order" case - // ?M_1 l_1 ... l_k =?= ?M_2 l_1 ... l_k - // ?M_1 l_1 ... l_k =?= ?M_2 l_1 ... l_k ... l_n - // ?M_1 l_1 ... l_k ... l_n =?= ?M_2 l_1 ... l_k - if (!is_simple_meta(lhs) || !is_simple_meta(rhs)) { - if (m_config.m_discard) { - return process_flex_flex_approx(c); - } else { - discard(c); - return true; - } - } - buffer lhs_args, rhs_args; - expr ml = get_app_args(lhs, lhs_args); - expr mr = get_app_args(rhs, rhs_args); - if (mlocal_name(ml) == mlocal_name(mr)) { - discard(c); - return true; - } - unsigned min_sz = std::min(lhs_args.size(), rhs_args.size()); - lean_assert(!m_subst.is_assigned(ml)); - lean_assert(!m_subst.is_assigned(mr)); - unsigned i = 0; - for (; i < min_sz; i++) - if (mlocal_name(lhs_args[i]) != mlocal_name(rhs_args[i])) - break; - if (i == min_sz) { - if (lhs_args.size() >= rhs_args.size()) { - return assign(lhs, ml, lhs_args, rhs, c.get_justification()); - } else { - return assign(rhs, mr, rhs_args, lhs, c.get_justification()); - } - } else { - discard(c); - return true; - } - } - - /** \brief Return true iff \c rhs is of the form max(l_1 ... lhs ... l_k) , - such that l_i's do not contain lhs. - - If the result is true, then all l_i's are stored in rest. - */ - static bool generalized_check_meta(level const & m, level const & rhs, bool & found_m, buffer & rest) { - lean_assert(is_meta(m)); - if (is_max(rhs)) { - return - generalized_check_meta(m, max_lhs(rhs), found_m, rest) && - generalized_check_meta(m, max_rhs(rhs), found_m, rest); - } else if (m == rhs) { - found_m = true; - return true; - } else if (occurs_meta(m, rhs)) { - return false; - } else { - rest.push_back(rhs); - return true; - } - } - - status process_l_eq_max_core(level const & lhs, level const & rhs, justification const & jst) { - lean_assert(is_meta(lhs)); - buffer rest; - bool found_lhs = false; - if (generalized_check_meta(lhs, rhs, found_lhs, rest)) { - level r; - if (found_lhs) { - // rhs is of the form max(rest, lhs) - // Solution is lhs := max(rest, ?u) where ?u is fresh metavariable - r = mk_meta_univ(mk_fresh_name()); - rest.push_back(r); - unsigned i = rest.size(); - while (i > 0) { - --i; - r = mk_max(rest[i], r); - } - r = normalize(r); - } else { - // lhs does not occur in rhs - r = rhs; - } - - if (assign(lhs, r, jst)) { - return Solved; - } else { - set_conflict(jst); - return Failed; - } - } else { - return Continue; - } - } - - /** \brief Return solved iff \c c is a constraint of the form - lhs =?= max(rest, lhs) - and is successfully solved. - */ - status process_l_eq_max(constraint const & c) { - lean_assert(is_level_eq_cnstr(c)); - level lhs = cnstr_lhs_level(c); - level rhs = cnstr_rhs_level(c); - justification jst = c.get_justification(); - if (is_meta(lhs)) - return process_l_eq_max_core(lhs, rhs, jst); - else if (is_meta(rhs)) - return process_l_eq_max_core(rhs, lhs, jst); - else - return Continue; - } - - /** Auxiliary method for process_succ_eq_max */ - status process_succ_eq_max_core(level const & lhs, level const & rhs, justification const & jst) { - if (!is_succ(lhs) || !is_max(rhs)) - return Continue; - level m = rhs; - while (is_max(m)) { - level m1 = max_lhs(m); - level m2 = max_rhs(m); - if (is_geq(lhs, m1)) { - m = m2; - } else if (is_geq(lhs, m2)) { - m = m1; - } else { - return Continue; - } - } - if (!is_meta(m)) - return Continue; - if (occurs(m, lhs)) - return Continue; - if (assign(m, lhs, jst)) { - return Solved; - } else { - set_conflict(jst); - return Failed; - } - } - - /** \brief Return Solved iff \c c is a constraint of the form - succ^k_1 a =?= max(succ^k_2 b, ?m) - where k_1 >= k_2 and a == b or b == zero - - and is successfully solved by assigning ?m := succ^k_1 a - */ - status process_succ_eq_max(constraint const & c) { - lean_assert(is_level_eq_cnstr(c)); - level lhs = cnstr_lhs_level(c); - level rhs = cnstr_rhs_level(c); - justification jst = c.get_justification(); - status st = process_succ_eq_max_core(lhs, rhs, jst); - if (st != Continue) return st; - return process_succ_eq_max_core(rhs, lhs, jst); - } - - /** - \brief Process the following constraints - 1. (max l1 l2) =?= 0 OR - solution: l1 =?= 0, l2 =?= 0 - 2. (imax l1 l2) =?= 0 - solution: l2 =?= 0 - */ - status try_level_eq_zero(level const & lhs, level const & rhs, justification const & j) { - if (!is_zero(rhs)) - return Continue; - if (is_max(lhs)) { - if (process_constraint(mk_level_eq_cnstr(max_lhs(lhs), rhs, j)) && - process_constraint(mk_level_eq_cnstr(max_rhs(lhs), rhs, j))) - return Solved; - else - return Failed; - } else if (is_imax(lhs)) { - return process_constraint(mk_level_eq_cnstr(imax_rhs(lhs), rhs, j)) ? Solved : Failed; - } else { - return Continue; - } - } - - status try_level_eq_zero(constraint const & c) { - lean_assert(is_level_eq_cnstr(c)); - level const & lhs = cnstr_lhs_level(c); - level const & rhs = cnstr_rhs_level(c); - justification const & j = c.get_justification(); - status st = try_level_eq_zero(lhs, rhs, j); - if (st != Continue) return st; - return try_level_eq_zero(rhs, lhs, j); - } - - /** \brief Try to solve constraints of the form - (?m1 =?= max ?m2 ?m3) - (?m1 =?= max ?m2 ?m3) - by assigning ?m1 =?= ?m2 and ?m1 =?= ?m3 - - \remark we may miss solutions. - */ - status try_merge_max_core(level const & lhs, level const & rhs, justification const & j) { - level m1 = lhs; - level m2, m3; - if (is_max(rhs)) { - m2 = max_lhs(rhs); - m3 = max_rhs(rhs); - } else if (is_imax(rhs)) { - m2 = imax_lhs(rhs); - m3 = imax_rhs(rhs); - } else { - return Continue; - } - if (process_constraint(mk_level_eq_cnstr(m1, m2, j)) && - process_constraint(mk_level_eq_cnstr(m1, m3, j))) - return Solved; - else - return Failed; - } - - /** \see try_merge_max_core */ - status try_merge_max(constraint const & c) { - lean_assert(is_level_eq_cnstr(c)); - level const & lhs = cnstr_lhs_level(c); - level const & rhs = cnstr_rhs_level(c); - justification const & j = c.get_justification(); - status st = try_merge_max_core(lhs, rhs, j); - if (st != Continue) return st; - return try_merge_max_core(rhs, lhs, j); - } - - - static void get_max_args(level const & m, buffer & args) { - if (is_max(m)) { - get_max_args(max_lhs(m), args); - get_max_args(max_rhs(m), args); - } else { - args.push_back(m); - } - } - - static level mk_max_args(buffer const & args) { - lean_assert(!args.empty()); - level r = args[0]; - for (unsigned i = 1; i < args.size(); i++) - r = mk_max(r, args[i]); - return r; - } - - /** - Given a constraint of the form (or commutative variants) - max u t =?= max u v - reduce it to t =?= v - - \remark we may miss solutions since this is an approximation - - see issue #777 - */ - status try_max_max_cancel(constraint const & c) { - lean_assert(is_level_eq_cnstr(c)); - level const & lhs = cnstr_lhs_level(c); - level const & rhs = cnstr_rhs_level(c); - justification const & j = c.get_justification(); - if (is_max(lhs) && is_max(rhs)) { - buffer lhs_args, rhs_args; - get_max_args(lhs, lhs_args); - get_max_args(rhs, rhs_args); - for (level const & l : lhs_args) { - if (std::find(rhs_args.begin(), rhs_args.end(), l) != rhs_args.end()) { - lhs_args.erase_elem(l); - rhs_args.erase_elem(l); - constraint new_c = mk_level_eq_cnstr(mk_max_args(lhs_args), mk_max_args(rhs_args), j); - if (process_constraint(new_c)) - return Solved; - else - return Continue; - } - } - } - return Continue; - } - - void cut_search() { - m_case_splits.clear(); - } - - /** \brief Process the next constraint in the constraint queue m_cnstrs */ - bool process_next() { - lean_assert(!m_cnstrs.empty()); - auto const * p = m_cnstrs.min(); - constraint c = p->first; - unsigned cidx = p->second; - if (cidx >= get_group_first_index(cnstr_group::ClassInstance) && - is_choice_cnstr(c) && cnstr_on_demand(c)) { - // we postpone class-instance constraints whose type still contains metavariables - m_cnstrs.erase_min(); - postpone(c); - return true; - } - if (cidx >= get_group_first_index(cnstr_group::Checkpoint) && - cidx < get_group_first_index(cnstr_group::FlexFlex)) { - cut_search(); - } - lean_trace("unifier", tout() << "process_next: " << cidx << " " << static_cast(to_cnstr_group(cidx)) << " " << c << "\n";); - m_cnstrs.erase_min(); - if (is_choice_cnstr(c)) { - return process_choice_constraint(c); - } else { - auto r = instantiate_metavars(c); - c = r.first; - bool modified = r.second; - if (is_level_eq_cnstr(c)) { - if (modified) { - return process_constraint(c); - } - status st = process_l_eq_max(c); - if (st != Continue) return st == Solved; - st = process_succ_eq_max(c); - if (st != Continue) return st == Solved; - if (m_config.m_discard) { - // we only try try_level_eq_zero, try_max_max_cancel and try_merge_max when we are discarding - // constraints that cannot be solved. - st = try_level_eq_zero(c); - if (st != Continue) { - return st == Solved; - } - if (cidx < get_group_first_index(cnstr_group::FlexFlex)) { - add_cnstr(c, cnstr_group::FlexFlex); - return true; - } - st = try_max_max_cancel(c); - if (st != Continue) { - return st == Solved; - } - st = try_merge_max(c); - if (st != Continue) { - return st == Solved; - } - return process_plugin_constraint(c); - } else { - discard(c); - return true; - } - } else { - lean_assert(is_eq_cnstr(c)); - if (is_delta_cnstr(c) && (!modified || has_expr_metavar_relaxed(cnstr_lhs_expr(c)) || has_expr_metavar_relaxed(cnstr_rhs_expr(c)))) { - return process_delta(c); - } else if (modified) { - return is_def_eq(cnstr_lhs_expr(c), cnstr_rhs_expr(c), c.get_justification()); - } else if (auto d = is_owned(c)) { - // Metavariable in the constraint is owned by choice constraint. - // choice constraint was postponed... since c was not modifed - // So, we should postpone this one too. - add_cnstr_after(c, *d); - return true; - } else if (is_flex_rigid(c)) { - return process_flex_rigid(c); - } else if (is_flex_flex(c)) { - return process_flex_flex(c); - } else if (is_same_projection_projection(c)) { - return process_same_projection_projection(c); - } else if (is_projection_projection(c)) { - return process_projection_projection(c, cidx); - } else if (is_projection_lhs(c)) { - return process_projection_eq(cnstr_lhs_expr(c), cnstr_rhs_expr(c), c.get_justification()); - } else if (is_projection_rhs(c)) { - return process_projection_eq(cnstr_rhs_expr(c), cnstr_lhs_expr(c), c.get_justification()); - } else { - return process_plugin_constraint(c); - } - } - } - } - - /** \brief Return true if unifier may be able to produce more solutions */ - bool more_solutions() const { - return !in_conflict() || !m_case_splits.empty(); - } - - typedef optional> next_result; - - next_result failure() { - lean_assert(in_conflict()); - if (m_config.m_use_exceptions) - throw unifier_exception(*m_conflict, m_subst); - else - return next_result(); - } - - /** \brief Produce the next solution */ - next_result next() { - if (!more_solutions()) - return failure(); - if (!m_first && !m_case_splits.empty()) { - justification all_assumptions; - for (auto const & cs : m_case_splits) - all_assumptions = mk_composite1(all_assumptions, mk_assumption_justification(cs->m_assumption_idx)); - set_conflict(all_assumptions); - if (!resolve_conflict()) - return failure(); - } else if (m_first) { - m_first = false; - } else { - // This is not the first run, and there are no case-splits. - // We don't throw an exception since there are no more solutions. - return next_result(); - } - - while (true) { - if (!in_conflict()) { - if (m_cnstrs.empty()) - break; - process_next(); - } - if (in_conflict() && !resolve_conflict()) - return failure(); - } - lean_assert(!in_conflict()); - lean_assert(m_cnstrs.empty()); - substitution s = m_subst; - s.forget_justifications(); - return next_result(mk_pair(s, m_postponed)); - } -}; - -unify_result_seq unify(std::shared_ptr u) { - if (!u->more_solutions()) { - u->failure(); // make sure exception is thrown if u->m_use_exception is true - return unify_result_seq(); - } else { - return mk_lazy_list>([=]() { - auto s = u->next(); - if (s) - return some(mk_pair(*s, unify(u))); - else - return unify_result_seq::maybe_pair(); - }); - } -} - -unify_result_seq unify(environment const & env, unsigned num_cs, constraint const * cs, - substitution const & s, unifier_config const & cfg) { - return unify(std::make_shared(env, num_cs, cs, s, cfg)); -} - -unify_result_seq unify(environment const & env, expr const & lhs, expr const & rhs, - substitution const & s, unifier_config const & cfg) { - substitution new_s = s; - expr _lhs = new_s.instantiate(lhs); - expr _rhs = new_s.instantiate(rhs); - auto u = std::make_shared(env, 0, nullptr, new_s, cfg); - constraint_seq cs; - if (!u->m_tc->is_def_eq(_lhs, _rhs, justification(), cs) || !u->process_constraints(cs)) { - return unify_result_seq(); - } else { - return unify(u); - } -} - -void initialize_unifier() { - register_trace_class(name{"unifier"}); - g_unifier_max_steps = new name{"unifier", "max_steps"}; - g_unifier_normalizer_max_steps = new name{"unifier", "normalizer_max_steps"}; - g_unifier_expensive_classes = new name{"unifier", "expensive_classes"}; - g_unifier_conservative = new name{"unifier", "conservative"}; - g_unifier_nonchronological = new name{"unifier", "nonchronological"}; - - register_unsigned_option(*g_unifier_max_steps, LEAN_DEFAULT_UNIFIER_MAX_STEPS, "(unifier) maximum number of steps"); - register_unsigned_option(*g_unifier_normalizer_max_steps, LEAN_DEFAULT_UNIFIER_NORMALIZER_MAX_STEPS, "(unifier) maximum number of steps the normalization procedure may perform when invoked by the unifier"); - register_bool_option(*g_unifier_expensive_classes, LEAN_DEFAULT_UNIFIER_EXPENSIVE_CLASSES, - "(unifier) use \"full\" higher-order unification when solving class instances"); - register_bool_option(*g_unifier_conservative, LEAN_DEFAULT_UNIFIER_CONSERVATIVE, - "(unifier) unfolds only constants marked as reducible, avoid expensive case-splits (it is faster but less complete)"); - register_bool_option(*g_unifier_nonchronological, LEAN_DEFAULT_UNIFIER_NONCHRONOLOGICAL, - "(unifier) enable/disable nonchronological backtracking in the unifier (this option is only available for debugging and benchmarking purposes, and running experiments)"); - - g_dont_care_cnstr = new constraint(mk_eq_cnstr(expr(), expr(), justification())); -} - -void finalize_unifier() { - delete g_dont_care_cnstr; - delete g_unifier_max_steps; - delete g_unifier_normalizer_max_steps; - delete g_unifier_expensive_classes; - delete g_unifier_conservative; - delete g_unifier_nonchronological; -} -} diff --git a/src/library/unifier.h b/src/library/unifier.h deleted file mode 100644 index c8b20802c8..0000000000 --- a/src/library/unifier.h +++ /dev/null @@ -1,121 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -#include -#include "util/lazy_list.h" -#include "util/sexpr/options.h" -#include "kernel/environment.h" -#include "library/metavar.h" -#include "library/constraint.h" - -namespace lean { -unsigned get_unifier_max_steps(options const & opts); - -bool is_simple_meta(expr const & e); -expr mk_aux_metavar_for(expr const & t); - -enum class unify_status { Solved, Failed, Unsupported }; -/** - \brief Handle the easy-cases: first-order unification, higher-order patterns, identical terms, and terms without metavariables. - - This function assumes that all assigned metavariables have been substituted. -*/ -unify_status unify_simple(substitution & s, expr const & lhs, expr const & rhs, justification const & j); -unify_status unify_simple(substitution & s, level const & lhs, level const & rhs, justification const & j); -unify_status unify_simple(substitution & s, constraint const & c); - -enum class unifier_kind { Cheap, Conservative, Liberal }; - -struct unifier_config { - bool m_use_exceptions; - unsigned m_max_steps; - unsigned m_normalizer_max_steps; - bool m_expensive_classes; - // If m_discard is true, then constraints that cannot be solved are discarded (or incomplete methods are used) - // If m_discard is false, unify returns the set of constraints that could not be handled. - bool m_discard; - // If m_mind == Conservative, then the following restrictions are imposed: - // - All constants that are not at least marked as Semireducible are treated as - // opaque. - // - Disables case-split on delta-delta constraints. - // - Disables reduction case-split on flex-rigid constraints. - // - // If m_kind == Cheap is true, then expensive case-analysis is not performed (e.g., delta). - // It is more restrictive than VeryConservative - // - // Default is Liberal - unifier_kind m_kind; - // If m_pattern is true, then we restrict the number of cases splits on - // flex-rigid constraints that are *not* in the higher-order pattern case. - bool m_pattern; - // If m_ignore_context_check == true, then occurs-check is skipped. - // Default is m_ignore_context_check == false - bool m_ignore_context_check; - // If m_nonchronological is true, then nonchronological backtracking is used in the unifier. - // Default is true - bool m_nonchronological; - unifier_config(bool use_exceptions = false, bool discard = false); - explicit unifier_config(options const & o, bool use_exceptions = false, bool discard = false); -}; - -/** \brief The unification procedures produce a lazy list of pair substitution + constraints that could not be solved. */ -typedef lazy_list> unify_result_seq; - -unify_result_seq unify(environment const & env, unsigned num_cs, constraint const * cs, - substitution const & s = substitution(), unifier_config const & c = unifier_config()); -unify_result_seq unify(environment const & env, expr const & lhs, expr const & rhs, - substitution const & s = substitution(), unifier_config const & c = unifier_config()); - -/** - The unifier divides the constraints in 9 groups: Simple, Basic, FlexRigid, PluginDelayed, DelayedChoice, ClassInstance, - Epilogue, FlexFlex, MaxDelayed - - 1) Simple: constraints that never create case-splits. Example: pattern matching constraints (?M l_1 ... l_n) =?= t. - The are not even inserted in the constraint priority queue. - - 2) Basic: contains user choice constraints used to model coercions and overloaded constraints, and constraints - that cannot be solved, and the unification plugin must be invoked. - - 3) FlexRigid constraints (?M t_1 ... t_n) =?= t, where t_n is not an introduction application - - 4) PluginDelayed: contraints delayed by the unifier_plugin. Examples: (elim ... (?m ...)) and (?m ... (intro ...)), - where elim is an eliminator/recursor and intro is an introduction/constructor. - This constraints are delayed because after ?m is assigned we may be able to reduce them. - - 5) DelayedChoice: for delayed choice constraints (we use this group for the maximally delayed coercions constraints). - - 6) ClassInstance: for delayed choice constraints (we use this group for class-instance). - - 7) Epilogue: constraints that must be solved before FlexFlex are discarded/postponed. - - 8) Checkpoint: unifier performs a prolog-like cut for any constraint in this group. - - 9) FlexFlex: (?m1 ...) =?= (?m2 ...) we don't try to solve this constraint, we delay them and hope the other - ones instantiate ?m1 or ?m2. If this kind of constraint is the next to be processed in the queue, then - we simply discard it (or save it and return to the caller as residue). - - 10) MaxDelayed: maximally delayed constraint group -*/ -enum class cnstr_group { Basic = 0, FlexRigid, PluginDelayed, DelayedChoice, ClassInstance, - Epilogue, Checkpoint, FlexFlex, MaxDelayed }; -inline unsigned to_delay_factor(cnstr_group g) { return static_cast(g); } - -class unifier_exception : public exception { - justification m_jst; - substitution m_subst; -public: - unifier_exception(justification const & j, substitution const & s):exception("unifier exception"), m_jst(j), m_subst(s) {} - virtual throwable * clone() const { return new unifier_exception(m_jst, m_subst); } - virtual void rethrow() const { throw *this; } - justification const & get_justification() const { return m_jst; } - substitution const & get_substitution() const { return m_subst; } -}; - -void initialize_unifier(); -void finalize_unifier(); -}