diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 627699b4d4..f7e68fe645 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -1,5 +1,5 @@ add_library(library basic_thms.cpp deep_copy.cpp max_sharing.cpp context_to_lambda.cpp state.cpp update_expr.cpp reduce.cpp - type_inferer.cpp placeholder.cpp ho_unifier.cpp expr_lt.cpp) + type_inferer.cpp placeholder.cpp expr_lt.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/library/ho_unifier.cpp b/src/library/ho_unifier.cpp deleted file mode 100644 index 2f9fe1c0ac..0000000000 --- a/src/library/ho_unifier.cpp +++ /dev/null @@ -1,704 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include "util/pvector.h" -#include "util/pdeque.h" -#include "util/exception.h" -#include "util/sexpr/options.h" -#include "kernel/environment.h" -#include "kernel/free_vars.h" -#include "kernel/instantiate.h" -#include "kernel/normalizer.h" -#include "kernel/printer.h" -#include "library/type_inferer.h" -#include "library/reduce.h" -#include "library/update_expr.h" -#include "library/ho_unifier.h" - -#ifndef LEAN_LIBRARY_HO_UNIFIER_MAX_SOLUTIONS -#define LEAN_LIBRARY_HO_UNIFIER_MAX_SOLUTIONS std::numeric_limits::max() -#endif - -#ifndef LEAN_LIBRARY_HO_UNIFIER_REMOVE_DUPLICATES -#define LEAN_LIBRARY_HO_UNIFIER_REMOVE_DUPLICATES true -#endif - -#ifndef LEAN_LIBRARY_HO_UNIFIER_USE_NORMALIZER -#define LEAN_LIBRARY_HO_UNIFIER_USE_NORMALIZER true -#endif - -#ifndef LEAN_LIBRARY_HO_UNIFIER_USE_BETA -#define LEAN_LIBRARY_HO_UNIFIER_USE_BETA true -#endif - -namespace lean { -static name g_library_ho_unifier_max_solutions {"library", "ho_unifier", "max_solutions"}; -static name g_library_ho_unifier_remove_duplicates {"library", "ho_unifier", "remove_duplicates"}; -static name g_library_ho_unifier_use_normalizer {"library", "ho_unifier", "use_normalizer"}; -static name g_library_ho_unifier_use_beta {"library", "ho_unifier", "use_beta"}; - -RegisterUnsignedOption(g_library_ho_unifier_max_solutions, LEAN_LIBRARY_HO_UNIFIER_MAX_SOLUTIONS, - "maximum number of solutions for each invocation of the higher-order unifier"); -RegisterBoolOption(g_library_ho_unifier_remove_duplicates, LEAN_LIBRARY_HO_UNIFIER_REMOVE_DUPLICATES, - "remove duplicate solutions in the higher-order unification module"); -RegisterBoolOption(g_library_ho_unifier_use_normalizer, LEAN_LIBRARY_HO_UNIFIER_USE_NORMALIZER, - "use normalizer in the higher-order unification module"); -RegisterBoolOption(g_library_ho_unifier_use_beta, LEAN_LIBRARY_HO_UNIFIER_USE_BETA, - "use beta-reduction in the higher-order unification module"); - -unsigned get_ho_unifier_max_solutions(options const & opts) { - return opts.get_unsigned(g_library_ho_unifier_max_solutions, LEAN_LIBRARY_HO_UNIFIER_MAX_SOLUTIONS); -} - -bool get_ho_unifier_remove_duplicates(options const & opts) { - return opts.get_bool(g_library_ho_unifier_remove_duplicates, LEAN_LIBRARY_HO_UNIFIER_REMOVE_DUPLICATES); -} - -bool get_ho_unifier_use_normalizer(options const & opts) { - return opts.get_bool(g_library_ho_unifier_use_normalizer, LEAN_LIBRARY_HO_UNIFIER_USE_NORMALIZER); -} - -bool get_ho_unifier_use_beta(options const & opts) { - return opts.get_bool(g_library_ho_unifier_use_beta, LEAN_LIBRARY_HO_UNIFIER_USE_BETA); -} - -static name g_x_name("x"); -class ho_unifier::imp { - typedef std::tuple constraint; - typedef pdeque cqueue; // constraint queue - struct state { - unsigned m_id; - substitution m_subst; - cqueue m_queue; - state(unsigned id, substitution const & subst, cqueue const & q): - m_id(id), m_subst(subst), m_queue(q) {} - }; - typedef std::vector state_stack; - - environment m_env; - normalizer m_normalizer; - type_inferer m_type_inferer; - state_stack m_state_stack; - unsigned m_delayed; - unsigned m_next_state_id; - bool m_used_aux_vars; - volatile bool m_interrupted; - // options - unsigned m_max_solutions; - bool m_remove_duplicates; - bool m_use_normalizer; - bool m_use_beta; - - static substitution & subst_of(state & s) { return s.m_subst; } - static cqueue & queue_of(state & s) { return s.m_queue; } - - state mk_state(substitution const & s, cqueue const & q) { - unsigned id = m_next_state_id; - m_next_state_id++; - return state(id, s, q); - } - - void reset_delayed() { - m_delayed = 0; - } - - /** - \brief Add a constraint to the state in the top of the state_stack - */ - void add_constraint(context const & ctx, expr const & l, expr const & r) { - lean_assert(!m_state_stack.empty()); - state & s = m_state_stack.back(); - queue_of(s).push_front(constraint(ctx, l, r)); - reset_delayed(); - } - - /** - \brief Add a constraint to the state in the top of the state_stack, - but put the constraint in the end of the queue, and increase the m_delayed counter. - */ - void postpone_constraint(context const & ctx, expr const & l, expr const & r) { - lean_assert(!m_state_stack.empty()); - state & s = m_state_stack.back(); - queue_of(s).push_back(constraint(ctx, l, r)); - m_delayed++; - } - - void init(context const & ctx, expr const & l, expr const & r, substitution const & subst) { - m_next_state_id = 0; - m_used_aux_vars = false; - m_state_stack.clear(); - m_state_stack.push_back(mk_state(subst, cqueue())); - add_constraint(ctx, l, r); - } - - /** - \brief Return true iff \c r already contains the solution (s, rs). - - \remark We only check if \c rs is empty. - - \remark \c ini_s is the initial substitution set. \c s is an extension of \c ini_s - */ - bool contains_solution(list const & r, substitution const & /* s */, residue const & rs, substitution const & /* ini_s */ ) { - return - empty(rs) && - std::any_of(r.begin(), r.end(), [&](result const & prev) { - if (!empty(prev.second)) - return false; - // TODO(Leo) metavar - // substitution const & prev_s = prev.first; - // if (s != prev_s) - // return false; - // return true; - return false; - }); - } - - /** - \brief Cleanup the result (remove auxiliary metavariables created by higher-order matching) - - \remark \c ini_s is the initial substitution set. \c s is an extension of \c ini_s - */ - substitution cleanup_subst(substitution const & s, substitution const & /* ini_s */) { -#if 0 // TODO(Leo) metavar - metavar_env new_s; - for (unsigned i = 0; i < ini_s.size(); i++) { - new_s.mk_metavar(s.get_type(i), s.get_context(i)); - expr subst = s.get_subst(i); - if (subst) { - if (m_use_beta && !ini_s.is_assigned(i)) { - // beta-reduce the substitution in order to simplify expressions built using - // higher-order matching - subst = beta_reduce(subst); - } - new_s.assign(i, subst); - } - } - return new_s; -#else - return s; -#endif - } - - /** - \brief Store a result (s, rs) into r. - If m_remove_duplicates is true, then we check if r does not already contains the solution (s, rs). - In the current implementation, we only perform the check when rs is empty. - - \remark \c ini_s is the initial substitution set. \c s is an extension of \c ini_s - */ - list save_result(list const & r, substitution s, residue const & rs, substitution const & ini_s) { - if (empty(rs) && m_used_aux_vars) { - // We only do the cleanup when we don't have a residue. - // If we have a residue, we can only remove auxiliary metavariables that do not occur in rs - s = cleanup_subst(s, ini_s); - } - - if (m_remove_duplicates && contains_solution(r, s, rs, ini_s)) { - return r; - } else { - return cons(result(s, rs), r); - } - } - - /** - Process a == b when: - 1- \c a is an assigned metavariable - 2- \c a is a unassigned metavariable without a metavariable context. - 3- \c a is a unassigned metavariable of the form ?m[lift:s:n, ...], and \c b does not have - a free variable in the range [s, s+n). - 4- \c a is an application of the form (?m ...) where ?m is an assigned metavariable. - */ - enum status { Solved, Failed, Continue }; - status process_metavar(expr & a, expr & b, substitution & s) { - if (is_metavar(a)) { - if (s.is_assigned(a)) { - // Case 1 - a = s.get_subst(a); - } else if (!has_local_context(a)) { - // Case 2 - if (has_metavar(b, a, s)) { - return Failed; - } else { - s.assign(a, b); - reset_delayed(); - return Solved; - } - } else { - local_entry const & me = head(metavar_lctx(a)); - if (me.is_lift() && !has_free_var(b, me.s(), me.s() + me.n())) { - // Case 3 - b = lower_free_vars(b, me.s() + me.n(), me.n()); - a = pop_meta_context(a); - } - } - } - - if (is_app(a) && is_metavar(arg(a, 0)) && s.is_assigned(arg(a, 0))) { - // Case 4 - a = update_app(a, 0, s.get_subst(arg(a, 0))); - } - return Continue; - } - - /** \brief Unfold let-expression */ - void process_let(expr & a) { - if (is_let(a)) - a = instantiate(let_body(a), let_value(a)); - } - - /** \brief Unfold constants */ - void process_constant(expr & a) { - if (is_constant(a)) { - object const & obj = m_env.find_object(const_name(a)); - if (obj && obj.is_definition() && !obj.is_opaque()) - a = obj.get_value(); - } - } - - /** \brief Replace variables by their definition if the context contains it. */ - void process_var(context const & ctx, expr & a) { - if (is_var(a)) { - try { - context_entry const & e = lookup(ctx, var_idx(a)); - if (e.get_body()) - a = e.get_body(); - } catch (exception&) { - } - } - } - - /** \brief Applies simple unfolding steps */ - void process_simple(context const & ctx, expr & a) { - process_let(a); - process_constant(a); - process_var(ctx, a); - } - - /** \brief Process the application's function using \c process_simple */ - void process_app_function(context const & ctx, expr & a) { - if (is_app(a)) { - expr f = arg(a, 0); - process_simple(ctx, f); - a = update_app(a, 0, f); - } - } - - /** \brief Creates a subproblem based on the application arguments */ - bool process_app_args(context const & ctx, expr const & a, expr const & b, unsigned start) { - lean_assert(is_app(a) && is_app(b)); - if (num_args(a) != num_args(b)) { - return false; - } else { - for (unsigned i = start; i < num_args(a); i++) { - add_constraint(ctx, arg(a, i), arg(b, i)); - } - return true; - } - } - - /** - Process a constraint ctx |- a = b, where \c a and \c b - are applications and the function is the same. - That is, arg(a, 0) == arg(b, 0) - - \pre is_app(a) && is_app(b) && arg(a, 0) == arg(b, 0) - */ - bool process_easy_app(context const & ctx, expr const & a, expr const & b) { - lean_assert(is_app(a) && is_app(b) && arg(a, 0) == arg(b, 0)); - return process_app_args(ctx, a, b, 1); - } - - /** \brief Return true if \c a is of the form (?m ...) */ - bool is_meta_app(expr const & a) { - return is_app(a) && is_metavar(arg(a, 0)); - } - - /** \brief Return true iff \c a is a metavariable and has a meta context. */ - bool is_metavar_with_context(expr const & a) { - return is_metavar(a) && has_local_context(a); - } - - /** \brief Return true if \c a is of the form (?m[...] ...) */ - bool is_meta_app_with_context(expr const & a) { - return is_meta_app(a) && has_local_context(arg(a, 0)); - } - - expr mk_lambda(name const & n, expr const & d, expr const & b) { - return ::lean::mk_lambda(n, d, b); - } - - /** - \brief Create the term (fun (x_0 : types[0]) ... (x_{n-1} : types[n-1]) body) - */ - expr mk_lambda(buffer const & types, expr const & body) { - expr r = body; - unsigned i = types.size(); - while (i > 0) { - --i; - r = mk_lambda(name(g_x_name, i), types[i], r); - } - return r; - } - - /** - \brief Return (f x_{num_vars - 1} ... x_0) - */ - expr mk_app_vars(expr const & f, unsigned num_vars) { - buffer args; - args.push_back(f); - unsigned i = num_vars; - while (i > 0) { - --i; - args.push_back(mk_var(i)); - } - return mk_app(args.size(), args.data()); - } - - /** - \brief Process a constraint ctx |- a = b where \c a is of the form (?m ...). - We perform a "case split" using "projection" or "imitation". See Huet&Lang's paper on higher order matching - for further details. - */ - bool process_meta_app(context const & /* ctx */, expr const & /* a */, expr const & /* b */) { - return true; -#if 0 - lean_assert(is_meta_app(a)); - lean_assert(!has_local_context(arg(a, 0))); - lean_assert(!is_meta_app(b)); - m_used_aux_vars = true; - expr f_a = arg(a, 0); - lean_assert(is_metavar(f_a)); - state top_state = m_state_stack.back(); - cqueue q = queue_of(top_state); - substitution s = subst_of(top_state); - name const & mname = metavar_name(f_a); - unsigned num_a = num_args(a); - // unification_constraints_wrapper ucw; - buffer arg_types; - for (unsigned i = 1; i < num_a; i++) { - arg_types.push_back(m_type_inferer(arg(a, i), ctx, &s, &ucw)); - } - // Clear m_type_infer cache since we don't want a reference to s inside of m_type_infer - m_type_inferer.clear(); - if (ucw.failed()) - return false; - m_state_stack.pop_back(); - // Add projections - for (unsigned i = 1; i < num_a; i++) { - // Assign f_a <- fun (x_1 : T_0) ... (x_{num_a-1} : T_{num_a-1}), x_i - cqueue new_q = q; - new_q.push_front(constraint(ctx, arg(a, i), b)); - substitution new_s = s; - expr proj = mk_lambda(arg_types, mk_var(num_a - i - 1)); - new_s.assign(mname, proj); - m_state_stack.push_back(mk_state(new_s, new_q)); - } - // Add imitation - substitution new_s = s; - cqueue new_q = q; - if (is_app(b)) { - // Imitation for applications - expr f_b = arg(b, 0); - unsigned num_b = num_args(b); - // Assign f_a <- fun (x_1 : T_0) ... (x_{num_a-1} : T_{num_a-1}), f_b (h_1 x_1 ... x_{num_a-1}) ... (h_{num_b-1} x_1 ... x_{num_a-1}) - // New constraints (h_i a_1 ... a_{num_a-1}) == arg(b, i) - buffer imitation_args; // arguments for the imitation - imitation_args.push_back(f_b); - for (unsigned i = 1; i < num_b; i++) { - expr h_i; // = new_s.mk_metavar(ctx); - imitation_args.push_back(mk_app_vars(h_i, num_a - 1)); - new_q.push_front(constraint(ctx, update_app(a, 0, h_i), arg(b, i))); - } - expr imitation = mk_lambda(arg_types, mk_app(imitation_args.size(), imitation_args.data())); - new_s.assign(mname, imitation); - } else if (is_eq(b)) { - // Imitation for equality - // Assign f_a <- fun (x_1 : T_0) ... (x_{num_a-1} : T_{num_a-1}), (h_1 x_1 ... x_{num_a-1}) = (h_2 x_1 ... x_{num_a-1}) - // New constraints (h_1 a_1 ... a_{num_a-1}) == eq_lhs(b) - // (h_2 a_1 ... a_{num_a-1}) == eq_rhs(b) - expr h_1; // = new_s.mk_metavar(ctx); - expr h_2; // = new_s.mk_metavar(ctx); - expr imitation = mk_lambda(arg_types, mk_eq(mk_app_vars(h_1, num_a - 1), mk_app_vars(h_2, num_a - 1))); - new_s.assign(mname, imitation); - new_q.push_front(constraint(ctx, update_app(a, 0, h_1), eq_lhs(b))); - new_q.push_front(constraint(ctx, update_app(a, 0, h_2), eq_rhs(b))); - } else if (is_abstraction(b)) { - // Imitation for lambdas and Pis - // Assign f_a <- fun (x_1 : T_0) ... (x_{num_a-1} : T_{num_a-1}), - // fun (x_b : (?h_1 x_1 ... x_{num_a-1})), (?h_2 x_1 ... x_{num_a-1} x_b) - // New constraints (h_1 a_1 ... a_{num_a-1}) == abst_domain(b) - // (h_2 a_1 ... a_{num_a-1} x_b) == abst_body(b) - expr h_1; // = new_s.mk_metavar(ctx); - expr h_2; // = new_s.mk_metavar(ctx); - expr imitation = mk_lambda(arg_types, update_abstraction(b, mk_app_vars(h_1, num_a - 1), mk_app_vars(h_2, num_a))); - new_s.assign(mname, imitation); - new_q.push_front(constraint(ctx, update_app(a, 0, h_1), abst_domain(b))); - new_q.push_front(constraint(extend(ctx, abst_name(b), abst_domain(b)), mk_app(update_app(a, 0, h_2), Var(0)), abst_body(b))); - } else { - // "Dumb imitation" aka the constant function - // Assign f_a <- fun (x_1 : T_0) ... (x_{num_a-1} : T_{num_a-1}), b - expr imitation = mk_lambda(arg_types, lift_free_vars(b, 0, num_a - 1)); - new_s.assign(mname, imitation); - } - m_state_stack.push_back(mk_state(new_s, new_q)); - reset_delayed(); - return true; -#endif - } - - /** \brief Return true if \c a is of the form ?m[inst:i t, ...] */ - bool is_metavar_inst(expr const & a) const { - return is_metavar(a) && has_local_context(a) && head(metavar_lctx(a)).is_inst(); - } - - /** - \brief Process a constraint ctx |- a = b where \c a is of the form ?m[(inst:i t), ...]. - We perform a "case split", - Case 1) ?m == #i and t == b - Case 2) imitate b - */ - void process_metavar_inst(context const & ctx, expr const & a, expr const & b) { - lean_assert(is_metavar_inst(a)); - lean_assert(!is_metavar_inst(b)); - lean_assert(!is_meta_app(b)); - m_used_aux_vars = true; - local_context lctx = metavar_lctx(a); - name const & mname = metavar_name(a); - unsigned i = head(lctx).s(); - expr t = head(lctx).v(); - state top_state = m_state_stack.back(); - cqueue q = queue_of(top_state); - substitution s = subst_of(top_state); - m_state_stack.pop_back(); - { - // Case 1 - substitution new_s = s; - new_s.assign(mname, mk_var(i)); - cqueue new_q = q; - new_q.push_front(constraint(ctx, t, b)); - m_state_stack.push_back(mk_state(new_s, new_q)); - } - { - // Case 2 - substitution new_s = s; - cqueue new_q = q; - if (is_app(b)) { - // Imitation for applications b == f(s_1, ..., s_k) - // mname <- f(?h_1, ..., ?h_k) - expr f_b = arg(b, 0); - unsigned num_b = num_args(b); - buffer imitation; - imitation.push_back(f_b); - for (unsigned i = 1; i < num_b; i++) - imitation.push_back(expr()); // new_s.mk_metavar(ctx)); - new_s.assign(mname, mk_app(imitation.size(), imitation.data())); - } else if (is_eq(b)) { - // Imitation for equality b == Eq(s1, s2) - // mname <- Eq(?h_1, ?h_2) - expr h_1; // = new_s.mk_metavar(ctx); - expr h_2; // = new_s.mk_metavar(ctx); - new_s.assign(mname, mk_eq(h_1, h_2)); - } else if (is_abstraction(b)) { - // Lambdas and Pis - // Imitation for Lambdas and Pis, b == Fun(x:T) B - // mname <- Fun (x:?h_1) ?h_2 x) - expr h_1; // = new_s.mk_metavar(ctx); - expr h_2; // = new_s.mk_metavar(ctx); - new_s.assign(mname, update_abstraction(b, h_1, mk_app(h_2, Var(0)))); - } else { - new_q.push_front(constraint(ctx, pop_meta_context(a), lift_free_vars(b, i, 1))); - } - m_state_stack.push_back(mk_state(new_s, new_q)); - reset_delayed(); - } - } - - /** - \brief Process the constraint \c c. Return true if the constraint was processed or postponed, and false - if it failed to solve the constraint. - */ - bool process(constraint const & c, substitution & s) { - context ctx = std::get<0>(c); - expr const & old_a = std::get<1>(c); - expr const & old_b = std::get<2>(c); - expr a = old_a; - expr b = old_b; - if (a == b) { - reset_delayed(); - return true; - } - if (is_app(a) && is_app(b) && arg(a, 0) == arg(b, 0)) - return process_easy_app(ctx, a, b); - status r; - r = process_metavar(a, b, s); - if (r != Continue) { return r == Solved; } - r = process_metavar(b, a, s); - if (r != Continue) { return r == Solved; } - process_simple(ctx, a); - process_simple(ctx, b); - process_app_function(ctx, a); - process_app_function(ctx, b); - if ((is_app(a) && !is_eqp(a, old_a)) || (is_app(b) && !is_eqp(b, old_b))) { - // some progress was made - add_constraint(ctx, a, b); - return true; - } - if (m_use_beta) { - a = head_beta_reduce(a); - b = head_beta_reduce(b); - } - if (is_metavar_inst(a) && (!is_metavar_inst(b) && !is_meta_app(b))) { - process_metavar_inst(ctx, a, b); - return true; - } - if (is_metavar_inst(b) && (!is_metavar_inst(a) && !is_meta_app(a))) { - process_metavar_inst(ctx, b, a); - return true; - } - if (is_metavar_with_context(a) || is_metavar_with_context(b) || - is_meta_app_with_context(a) || is_meta_app_with_context(b)) { - // a or b is a metavariable that has a metavariable context associated with it. - // postpone - postpone_constraint(ctx, a, b); - return true; - } - if (!is_app(a) && !is_app(b)) { - if (a.kind() != b.kind()) - return false; - switch (a.kind()) { - case expr_kind::Constant: case expr_kind::Var: case expr_kind::Value: case expr_kind::Type: - return a == b; - case expr_kind::Eq: - add_constraint(ctx, eq_lhs(a), eq_lhs(b)); - add_constraint(ctx, eq_rhs(a), eq_rhs(b)); - return true; - case expr_kind::Lambda: case expr_kind::Pi: - add_constraint(ctx, abst_domain(a), abst_domain(b)); - add_constraint(extend(ctx, abst_name(a), abst_domain(a)), abst_body(a), abst_body(b)); - return true; - case expr_kind::Let: case expr_kind::MetaVar: case expr_kind::App: - lean_unreachable(); - } - } - - if (is_meta_app(a)) { - if (is_meta_app(b)) { - postpone_constraint(ctx, a, b); - return true; - } else { - return process_meta_app(ctx, a, b); - return true; - } - } else if (is_meta_app(b)) { - lean_assert(!is_meta_app(b)); - return process_meta_app(ctx, b, a); - } - - if (m_use_normalizer) { - if (!is_eqp(a, old_a) || !is_eqp(b, old_b)) { - // some progress was made - add_constraint(ctx, a, b); - return true; - } - - expr norm_a; // = m_normalizer(a, ctx, &s); - expr norm_b; // = m_normalizer(b, ctx, &s); - if (norm_a.kind() != norm_b.kind()) - return false; - if (is_app(norm_a)) { - return process_app_args(ctx, norm_a, norm_b, 0); - } else if (a == norm_a && b == norm_b) { - return false; - } else { - // some progress was made - add_constraint(ctx, norm_a, norm_b); - return true; - } - } else { - if (a.kind() != b.kind()) - return false; - if (is_app(a)) { - return process_app_args(ctx, a, b, 0); - } else if (!is_eqp(a, old_a) || !is_eqp(b, old_b)) { - // some progress was made - add_constraint(ctx, a, b); - return true; - } else { - return false; - } - } - } - -public: - imp(environment const & env, options const & opts): - m_env(env), - m_normalizer(env, opts), - m_type_inferer(env) { - m_interrupted = false; - m_delayed = 0; - m_max_solutions = get_ho_unifier_max_solutions(opts); - m_remove_duplicates = get_ho_unifier_remove_duplicates(opts); - m_use_normalizer = get_ho_unifier_use_normalizer(opts); - m_use_beta = get_ho_unifier_use_beta(opts); - } - - list unify(context const & ctx, expr const & a, expr const & b, substitution const & subst) { - init(ctx, a, b, subst); - list r; - unsigned num_solutions = 0; - while (!m_state_stack.empty()) { - check_interrupted(m_interrupted); - if (num_solutions > m_max_solutions) - return r; - state & top_state = m_state_stack.back(); - cqueue & cq = queue_of(top_state); - unsigned cq_size = cq.size(); - if (cq.empty()) { - // no constraints left to be solved - r = save_result(r, subst_of(top_state), residue(), subst); - num_solutions++; - m_state_stack.pop_back(); - } else { - // try cq_sz times to find a constraint that can be processed - constraint c = cq.front(); - // std::cout << "solving (" << top_state.m_id << ") " << std::get<1>(c) << " === " << std::get<2>(c) << "\n"; - cq.pop_front(); - if (!process(c, subst_of(top_state))) { - // state can't be solved - reset_delayed(); - m_state_stack.pop_back(); - } - if (m_delayed > cq_size) { - // None of the constraints could be processed. - // So, we save the remaining constraints as a residue - residue rs; - for (auto c : cq) - rs = cons(c, rs); - r = save_result(r, subst_of(top_state), rs, subst); - num_solutions++; - reset_delayed(); - m_state_stack.pop_back(); - } - } - } - return r; - } - - void set_interrupt(bool flag) { - m_interrupted = flag; - m_normalizer.set_interrupt(flag); - m_type_inferer.set_interrupt(flag); - } -}; - -ho_unifier::ho_unifier(environment const & env, options const & opts):m_ptr(new imp(env, opts)) {} -ho_unifier::~ho_unifier() {} -void ho_unifier::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); } -list ho_unifier::operator()(context const & ctx, expr const & l, expr const & r, substitution const & subst) { - return m_ptr->unify(ctx, l, r, subst); -} -} diff --git a/src/library/ho_unifier.h b/src/library/ho_unifier.h deleted file mode 100644 index 6c649f4441..0000000000 --- a/src/library/ho_unifier.h +++ /dev/null @@ -1,43 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -#include -#include "util/list.h" -#include "util/sexpr/options.h" -#include "kernel/metavar.h" - -namespace lean { -/** \brief Functional object for (incomplete) higher-order unification */ -class ho_unifier { - class imp; - std::unique_ptr m_ptr; -public: - ho_unifier(environment const & env, options const & opts = options()); - ~ho_unifier(); - - typedef list> residue; - typedef std::pair result; - - /** - \brief Try to unify \c l and \c r in the context \c ctx using the input substitution \c menv. - By unification, we mean we have to find an assignment for the unassigned metavariables in - \c l and \c r s.t. \c l and \c r become definitionally equal. - The unifier may produce a residue: a set of unification problems - that could not be solved, and were postponed. The unifier postpones unification problems of the form - (?M1 ...) == (?M2 ...) where \c M1 and \c M2 are unassigned metavariables. - The result is a list of pairs: substitution (in the form of \c metavar_env) and residue. - Each pair is a possible solution. The resultant \c metavar_env may contain new metavariables. - The empty list represents failure. - */ - list operator()(context const & ctx, expr const & l, expr const & r, substitution const & menv); - - void set_interrupt(bool flag); - void interrupt() { set_interrupt(true); } - void reset_interrupt() { set_interrupt(false); } -}; -} diff --git a/src/tests/library/CMakeLists.txt b/src/tests/library/CMakeLists.txt index 8563b3d20e..49577ff779 100644 --- a/src/tests/library/CMakeLists.txt +++ b/src/tests/library/CMakeLists.txt @@ -1,9 +1,6 @@ add_executable(type_inferer type_inferer.cpp) target_link_libraries(type_inferer ${EXTRA_LIBS}) add_test(type_inferer ${CMAKE_CURRENT_BINARY_DIR}/type_inferer) -add_executable(ho_unifier ho_unifier.cpp) -target_link_libraries(ho_unifier ${EXTRA_LIBS}) -add_test(ho_unifier ${CMAKE_CURRENT_BINARY_DIR}/ho_unifier) add_executable(formatter formatter.cpp) target_link_libraries(formatter ${EXTRA_LIBS}) add_test(formatter ${CMAKE_CURRENT_BINARY_DIR}/formatter) diff --git a/src/tests/library/ho_unifier.cpp b/src/tests/library/ho_unifier.cpp deleted file mode 100644 index 75eee89618..0000000000 --- a/src/tests/library/ho_unifier.cpp +++ /dev/null @@ -1,172 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "util/test.h" -#include "kernel/environment.h" -#include "kernel/builtin.h" -#include "kernel/abstract.h" -#include "kernel/printer.h" -#include "library/ho_unifier.h" -#include "library/reduce.h" -#include "library/arith/arith.h" -using namespace lean; - -void tst1() { - environment env; - substitution subst; - ho_unifier unify(env); - expr N = Const("N"); - expr M = Const("M"); - env.add_var("N", Type()); - env.add_var("M", Type()); - env.add_var("f", N >> (M >> M)); - env.add_var("a", N); - env.add_var("b", M); - expr f = Const("f"); - expr x = Const("x"); - expr a = Const("a"); - expr b = Const("b"); - expr m1; // = subst.mk_metavar(); - expr l = m1(b, a); - expr r = f(b, f(a, b)); - for (auto sol : unify(context(), l, r, subst)) { - std::cout << m1 << " -> " << beta_reduce(sol.first.get_subst(m1)) << "\n"; - std::cout << beta_reduce(instantiate_metavars(l, sol.first)) << "\n"; - lean_assert(beta_reduce(instantiate_metavars(l, sol.first)) == r); - std::cout << "--------------\n"; - } -} - -void tst2() { - environment env; - import_basic(env); - substitution subst; - ho_unifier unify(env); - expr N = Const("N"); - expr M = Const("M"); - env.add_var("N", Type()); - env.add_var("f", N >> (Bool >> N)); - env.add_var("a", N); - env.add_var("b", N); - expr f = Const("f"); - expr x = Const("x"); - expr a = Const("a"); - expr b = Const("b"); - expr m1; // = subst.mk_metavar(); - expr l = m1(b, a); - expr r = Fun({x, N}, f(x, Eq(a, b))); - for (auto sol : unify(context(), l, r, subst)) { - std::cout << m1 << " -> " << beta_reduce(sol.first.get_subst(m1)) << "\n"; - std::cout << beta_reduce(instantiate_metavars(l, sol.first)) << "\n"; - lean_assert(beta_reduce(instantiate_metavars(l, sol.first)) == r); - std::cout << "--------------\n"; - } -} - -void tst3() { - environment env; - import_basic(env); - import_arith(env); - substitution subst; - ho_unifier unify(env); - expr N = Const("N"); - env.add_var("N", Type()); - env.add_var("f", N >> (Int >> N)); - env.add_var("a", N); - env.add_var("b", N); - expr m1; // = subst.mk_metavar(); - expr m2; // = subst.mk_metavar(); - expr m3; // = subst.mk_metavar(); - expr t1; // = metavar_type(m1); - expr t2; // = metavar_type(m2); - expr f = Const("f"); - expr a = Const("a"); - expr b = Const("b"); - expr l = f(m1(a), iAdd(m3, iAdd(iVal(1), iVal(1)))); - expr r = f(m2(b), iAdd(iVal(1), iVal(2))); - for (auto sol : unify(context(), l, r, subst)) { - std::cout << m3 << " -> " << sol.first.get_subst(m3) << "\n"; - lean_assert(sol.first.get_subst(m3) == iVal(1)); - lean_assert(length(sol.second) == 1); - for (auto c : sol.second) { - std::cout << std::get<1>(c) << " == " << std::get<2>(c) << "\n"; - } - } -} - -void tst4() { - environment env; - substitution subst; - ho_unifier unify(env); - expr N = Const("N"); - env.add_var("N", Type()); - env.add_var("f", N >> (N >> N)); - expr x = Const("x"); - expr y = Const("y"); - expr f = Const("f"); - expr m1; // = subst.mk_metavar(); - expr m2; // = subst.mk_metavar(); - expr l = Fun({{x, N}, {y, N}}, Eq(y, f(x, m1))); - expr r = Fun({{x, N}, {y, N}}, Eq(m2, f(m1, x))); - auto sols = unify(context(), l, r, subst); - lean_assert(length(sols) == 1); - for (auto sol : sols) { - std::cout << m1 << " -> " << sol.first.get_subst(m1) << "\n"; - std::cout << m2 << " -> " << sol.first.get_subst(m2) << "\n"; - lean_assert(empty(sol.second)); - lean_assert(beta_reduce(instantiate_metavars(l, sol.first)) == - beta_reduce(instantiate_metavars(r, sol.first))); - } -} - -void tst5() { - environment env; - substitution subst; - ho_unifier unify(env); - expr N = Const("N"); - env.add_var("N", Type()); - env.add_var("f", N >> (N >> N)); - expr f = Const("f"); - expr m1; // = subst.mk_metavar(); - expr l = f(f(m1)); - expr r = f(m1); - auto sols = unify(context(), l, r, subst); - lean_assert(length(sols) == 0); -} - -void tst6() { - environment env; - substitution subst; - ho_unifier unify(env); - expr N = Const("N"); - env.add_var("N", Type()); - env.add_var("f", N >> (N >> N)); - expr x = Const("x"); - expr y = Const("y"); - expr f = Const("f"); - expr m1; // = subst.mk_metavar(); - expr l = Fun({x, N}, Fun({y, N}, f(m1, y))(x)); - expr r = Fun({x, N}, f(x, x)); - auto sols = unify(context(), l, r, subst); - lean_assert(length(sols) == 2); - for (auto sol : sols) { - std::cout << m1 << " -> " << sol.first.get_subst(m1) << "\n"; - std::cout << instantiate_metavars(l, sol.first) << "\n"; - lean_assert(empty(sol.second)); - lean_assert(beta_reduce(instantiate_metavars(l, sol.first)) == - beta_reduce(instantiate_metavars(r, sol.first))); - } -} - -int main() { - tst1(); - tst2(); - tst3(); - tst4(); - tst5(); - tst6(); - return has_violations() ? 1 : 0; -}