From 611f29a9545a7c2ff49a30d89dbaf71630661625 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 22 Jun 2014 16:35:00 -0700 Subject: [PATCH] chore(library/elaborator): remove dead code Signed-off-by: Leonardo de Moura --- src/CMakeLists.txt | 3 - src/library/elaborator/CMakeLists.txt | 2 - src/library/elaborator/elaborator.cpp | 2169 ----------------- src/library/elaborator/elaborator.h | 61 - src/library/elaborator/elaborator_exception.h | 26 - .../elaborator/elaborator_justification.cpp | 159 -- .../elaborator/elaborator_justification.h | 190 -- src/library/elaborator/elaborator_plugin.h | 40 - src/tests/library/elaborator/CMakeLists.txt | 4 - src/tests/library/elaborator/elaborator.cpp | 900 ------- 10 files changed, 3554 deletions(-) delete mode 100644 src/library/elaborator/CMakeLists.txt delete mode 100644 src/library/elaborator/elaborator.cpp delete mode 100644 src/library/elaborator/elaborator.h delete mode 100644 src/library/elaborator/elaborator_exception.h delete mode 100644 src/library/elaborator/elaborator_justification.cpp delete mode 100644 src/library/elaborator/elaborator_justification.h delete mode 100644 src/library/elaborator/elaborator_plugin.h delete mode 100644 src/tests/library/elaborator/CMakeLists.txt delete mode 100644 src/tests/library/elaborator/elaborator.cpp diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 724a369e5..e56b56430 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -236,8 +236,6 @@ set(LEAN_LIBS ${LEAN_LIBS} library) # set(LEAN_LIBS ${LEAN_LIBS} rewriter) # add_subdirectory(library/simplifier) # set(LEAN_LIBS ${LEAN_LIBS} simplifier) -# add_subdirectory(library/elaborator) -# set(LEAN_LIBS ${LEAN_LIBS} elaborator) # add_subdirectory(library/tactic) # set(LEAN_LIBS ${LEAN_LIBS} tactic) add_subdirectory(library/error_handling) @@ -262,7 +260,6 @@ add_subdirectory(tests/kernel) add_subdirectory(tests/library) # add_subdirectory(tests/library/rewriter) # add_subdirectory(tests/library/tactic) -# add_subdirectory(tests/library/elaborator) add_subdirectory(tests/frontends/lean) # Include style check diff --git a/src/library/elaborator/CMakeLists.txt b/src/library/elaborator/CMakeLists.txt deleted file mode 100644 index d6854a25c..000000000 --- a/src/library/elaborator/CMakeLists.txt +++ /dev/null @@ -1,2 +0,0 @@ -add_library(elaborator elaborator.cpp elaborator_justification.cpp) -target_link_libraries(elaborator ${LEAN_LIBS}) diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp deleted file mode 100644 index 07b248ccc..000000000 --- a/src/library/elaborator/elaborator.cpp +++ /dev/null @@ -1,2169 +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 -#include -#include -#include "util/list.h" -#include "util/splay_tree.h" -#include "util/interrupt.h" -#include "util/sstream.h" -#include "kernel/for_each_fn.h" -#include "kernel/formatter.h" -#include "kernel/free_vars.h" -#include "kernel/normalizer.h" -#include "kernel/instantiate.h" -#include "kernel/replace_fn.h" -#include "kernel/kernel.h" -#include "kernel/type_checker.h" -#include "kernel/update_expr.h" -#include "library/printer.h" -#include "library/equality.h" -#include "library/elaborator/elaborator.h" -#include "library/elaborator/elaborator_justification.h" - -#ifndef LEAN_ELABORATOR_MAX_STEPS -#define LEAN_ELABORATOR_MAX_STEPS 100000 -#endif - -#ifndef LEAN_ELABORATOR_USE_NORMALIZER -#define LEAN_ELABORATOR_USE_NORMALIZER true -#endif - -#ifndef LEAN_ELABORATOR_INJECTIVITY -#define LEAN_ELABORATOR_INJECTIVITY true -#endif - -namespace lean { -static name g_x_name("x"); - -static name g_elaborator_max_steps {"elaborator", "max_steps"}; -static name g_elaborator_use_normalizer {"elaborator", "use_normalizer"}; -static name g_elaborator_injectivity {"elaborator", "injectivity"}; - -RegisterUnsignedOption(g_elaborator_max_steps, LEAN_ELABORATOR_MAX_STEPS, "(elaborator) maximum number of steps"); -RegisterBoolOption(g_elaborator_use_normalizer, LEAN_ELABORATOR_USE_NORMALIZER, - "(elaborator) invoke normalizer during elaboration"); -RegisterBoolOption(g_elaborator_injectivity, LEAN_ELABORATOR_INJECTIVITY, "(elaborator) reduce unification constrainst of the form f(t1, t2) ≈ f(s1, s2) into t1 ≈ s1 and t2 ≈ s2 even if f-applications are not in head normal form"); - -unsigned get_elaborator_max_steps(options const & opts) { - return opts.get_unsigned(g_elaborator_max_steps, LEAN_ELABORATOR_MAX_STEPS); -} -bool get_elaborator_use_normalizer(options const & opts) { - return opts.get_bool(g_elaborator_use_normalizer, LEAN_ELABORATOR_USE_NORMALIZER); -} -bool get_elaborator_injectivity(options const & opts) { - return opts.get_bool(g_elaborator_injectivity, LEAN_ELABORATOR_INJECTIVITY); -} - -class elaborator::imp { - typedef splay_tree name_set; - typedef list cnstr_list; - typedef list name_list; - typedef list> delayed_cnstr_list; - - struct state { - metavar_env m_menv; - cnstr_list m_active_cnstrs; - delayed_cnstr_list m_delayed_cnstrs; - name_set m_recently_assigned; // recently assigned metavars - state(metavar_env const & menv, unsigned num_cnstrs, unification_constraint const * cnstrs): - m_menv(menv.copy()), - m_active_cnstrs(to_list(cnstrs, cnstrs + num_cnstrs)) { - } - - state(state const & other): - m_menv(other.m_menv.copy()), - m_active_cnstrs(other.m_active_cnstrs), - m_delayed_cnstrs(other.m_delayed_cnstrs), - m_recently_assigned(other.m_recently_assigned) { - } - - state & operator=(state const & other) { - m_menv = other.m_menv.copy(); - m_active_cnstrs = other.m_active_cnstrs; - m_delayed_cnstrs = other.m_delayed_cnstrs; - m_recently_assigned = other.m_recently_assigned; - return *this; - } - }; - - /** - \brief Base class for case splits performed by the elaborator. - */ - struct case_split { - justification m_curr_assumption; // object used to justify current split - state m_prev_state; - std::vector m_failed_justifications; // justifications for failed branches - - case_split(state const & prev_state):m_prev_state(prev_state) {} - virtual ~case_split() {} - - virtual bool next(imp & owner) = 0; - }; - - /** - \brief Case-split object for choice constraints. - */ - struct choice_case_split : public case_split { - unsigned m_idx; - unification_constraint m_choice; - - choice_case_split(unification_constraint const & c, state const & prev_state): - case_split(prev_state), - m_idx(0), - m_choice(c) { - } - - virtual ~choice_case_split() {} - - virtual bool next(imp & owner) { - return owner.next_choice_case(*this); - } - }; - - /** - \brief General purpose case split object - */ - struct generic_case_split : public case_split { - unification_constraint m_constraint; - unsigned m_idx; // current alternative - std::vector m_states; // alternatives - std::vector m_assumptions; // assumption for each alternative - - generic_case_split(unification_constraint const & cnstr, state const & prev_state): - case_split(prev_state), - m_constraint(cnstr), - m_idx(0) { - } - - virtual ~generic_case_split() {} - - virtual bool next(imp & owner) { - return owner.next_generic_case(*this); - } - - void push_back(state const & s, justification const & tr) { - m_states.push_back(s); - m_assumptions.push_back(tr); - } - }; - - struct plugin_case_split : public case_split { - unification_constraint m_constraint; - std::unique_ptr m_alternatives; - - plugin_case_split(unification_constraint const & cnstr, std::unique_ptr & r, state const & prev_state): - case_split(prev_state), - m_constraint(cnstr), - m_alternatives(std::move(r)) { - } - - virtual ~plugin_case_split() {} - - virtual bool next(imp & owner) { - return owner.next_plugin_case(*this); - } - }; - - ro_environment m_env; - type_inferer m_type_inferer; - normalizer m_normalizer; - state m_state; - std::vector> m_case_splits; - std::shared_ptr m_plugin; - unsigned m_next_id; - justification m_conflict; - bool m_first; - level m_U; // universe U used for builtin kernel axioms - unsigned m_num_steps; - - // options - bool m_use_justifications; - bool m_use_normalizer; - bool m_assume_injectivity; - unsigned m_max_steps; - - void set_options(options const & o) { - m_use_justifications = true; - m_use_normalizer = get_elaborator_use_normalizer(o); - m_assume_injectivity = get_elaborator_injectivity(o); - m_max_steps = get_elaborator_max_steps(o); - } - - void check_system() { - check_interrupted(); - if (m_num_steps > m_max_steps) - throw exception(sstream() << "elaborator maximum number of steps (" << m_max_steps << ") exceeded, the maximum number of steps can be increased by setting the option elaborator::max_steps (remark: the elaborator uses higher order unification, which may trigger non-termination"); - m_num_steps++; - } - - justification mk_assumption() { - unsigned id = m_next_id; - m_next_id++; - return mk_assumption_justification(id); - } - - void push_front(cnstr_list & clist, unification_constraint const & c) { - // std::cout << "PUSHING: "; display(std::cout, c); std::cout << "\n"; - clist = cons(c, clist); - } - - /** \brief Add given constraint to active list */ - void push_active(unification_constraint const & c) { - push_front(m_state.m_active_cnstrs, c); - } - - /** \brief Push all contraints in the collection to the active list */ - void push_active(buffer const & cs) { - for (auto const & c : cs) - push_active(c); - } - - void collect_mvars(expr const & e, name_set & r) { - for_each(e, [&](expr const & m, unsigned) { - if (is_metavar(m) && !r.contains(metavar_name(m))) { - r.insert(metavar_name(m)); - for (auto const & entry : metavar_lctx(m)) { - if (entry.is_inst()) - collect_mvars(entry.v(), r); - } - } - return true; - }); - } - - /** \brief Collect metavars in \c c */ - name_list collect_mvars(unification_constraint const & c) { - name_set s; - auto proc = [&](expr const & e) { return collect_mvars(e, s); }; - switch (c.kind()) { - case unification_constraint_kind::Eq: - proc(eq_lhs(c)); proc(eq_rhs(c)); break; - case unification_constraint_kind::Convertible: - proc(convertible_from(c)); proc(convertible_to(c)); break; - case unification_constraint_kind::Max: - proc(max_lhs1(c)); proc(max_lhs2(c)); proc(max_rhs(c)); break; - case unification_constraint_kind::Choice: - lean_unreachable(); // we never delay Choice - break; - } - return s.fold([](name const & n, name_list const & l) { return cons(n, l); }, name_list()); - } - - /** \brief Add given constraint to the delayed list */ - void push_delayed(unification_constraint const & c) { - m_state.m_delayed_cnstrs.emplace_front(c, collect_mvars(c)); - } - - /** \brief Return true iff \c m is an assigned metavariable in the current state */ - bool is_assigned(expr const & m) const { - lean_assert(is_metavar(m)); - return m_state.m_menv->is_assigned(m); - } - - /** \brief Return the substitution (and justification) for an assigned metavariable */ - std::pair get_subst_jst(expr const & m) const { - lean_assert(is_metavar(m)); - lean_assert(is_assigned(m)); - return *(m_state.m_menv->get_subst_jst(m)); - } - - /** - \brief Return true iff \c e contains the metavariable \c m. - The substitutions in the current state are taken into account. - */ - bool has_metavar(expr const & e, expr const & m) const { - return m_state.m_menv->has_metavar(e, m); - } - - static bool has_metavar(expr const & e) { - return ::lean::has_metavar(e); - } - - /** - \brief Return true iff \c e contains an assigned metavariable in - the current state. - */ - bool has_assigned_metavar(expr const & e) const { - return m_state.m_menv->has_assigned_metavar(e); - } - - /** \brief Return true if \c a is of the form (?m ...) */ - static 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 or if \c a is an application where the function is a metavariable */ - static bool is_meta(expr const & a) { - return is_metavar(a) || is_meta_app(a); - } - - /** \brief Return true iff \c a is a metavariable and has a meta context. */ - static 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[...] ...) */ - static bool is_meta_app_with_context(expr const & a) { - return is_meta_app(a) && has_local_context(arg(a, 0)); - } - - /** \brief Return true iff \c a is a proposition */ - bool is_proposition(expr const & a, context const & ctx) { - if ((is_metavar(a)) || - (is_app(a) && is_metavar(arg(a, 0))) || - (is_abstraction(a) && (is_metavar(abst_domain(a)) || is_metavar(abst_body(a))))) { - // Avoid exception at m_type_inferer. - // Throw is expensive in C++. - return false; - } - try { - return m_type_inferer.is_proposition(a, ctx); - } catch (...) { - return false; - } - } - - static 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(i == 0 ? g_x_name : name(g_x_name, i), types[i], r); - } - return r; - } - - /** - \brief Return (f x_{num_vars + first - 1} ... x_first) - */ - expr mk_app_vars(expr const & f, unsigned num_vars, unsigned first = 0) { - buffer args; - args.push_back(f); - unsigned i = num_vars + first; - while (i > first) { - --i; - args.push_back(mk_var(i)); - } - return mk_app(args); - } - - /** - \brief Push a new constraint to the active_cnstrs. - If \c is_eq is true, then a equality constraint is created, otherwise a convertability constraint is created. - */ - void push_new_constraint(cnstr_list & active_cnstrs, bool is_eq, - context const & new_ctx, expr const & new_a, expr const & new_b, justification const & new_jst) { - if (new_a == new_b) - return; // trivial constraint - if (is_eq) - push_front(active_cnstrs, mk_eq_constraint(new_ctx, new_a, new_b, new_jst)); - else - push_front(active_cnstrs, mk_convertible_constraint(new_ctx, new_a, new_b, new_jst)); - } - - /** - \brief Push a new equality constraint new_ctx |- new_a ≈ new_b into the active_cnstrs using - justification \c new_jst. - */ - void push_new_eq_constraint(cnstr_list & active_cnstrs, - context const & new_ctx, expr const & new_a, expr const & new_b, justification const & new_jst) { - push_new_constraint(active_cnstrs, true, new_ctx, new_a, new_b, new_jst); - } - - void push_new_eq_constraint(context const & new_ctx, expr const & new_a, expr const & new_b, justification const & new_jst) { - push_new_eq_constraint(m_state.m_active_cnstrs, new_ctx, new_a, new_b, new_jst); - } - - /** - \brief Auxiliary method for pushing a new constraint to the current active list. - If \c is_eq is true, then a equality constraint is created, otherwise a convertability constraint is created. - */ - void push_new_constraint(bool is_eq, context const & new_ctx, expr const & new_a, expr const & new_b, justification const & new_jst) { - push_new_constraint(m_state.m_active_cnstrs, is_eq, new_ctx, new_a, new_b, new_jst); - } - - /** - \brief Auxiliary method for pushing a new constraint to the current active constraint list. - The new constraint is based on the constraint \c c. The constraint \c c may be a equality or convertability constraint. - The update is justified by \c new_jst. - */ - void push_updated_constraint(unification_constraint const & c, expr const & new_a, expr const & new_b, justification const & new_jst) { - push_new_constraint(m_state.m_active_cnstrs, is_eq(c), get_context(c), new_a, new_b, new_jst); - } - - /** - \brief Auxiliary method for pushing a new constraint to the current active constraint list. - The new constraint is based on the constraint \c c. The constraint \c c may be a equality or convertability constraint. - The flag \c is_lhs says if the left-hand-side or right-hand-side are being updated with \c new_a. - The update is justified by \c new_jst. - */ - void push_updated_constraint(unification_constraint const & c, bool is_lhs, expr const & new_a, justification const & new_jst) { - lean_assert(is_eq(c) || is_convertible(c)); - if (is_eq(c)) { - if (is_lhs) - push_updated_constraint(c, new_a, eq_rhs(c), new_jst); - else - push_updated_constraint(c, eq_lhs(c), new_a, new_jst); - } else { - if (is_lhs) - push_updated_constraint(c, new_a, convertible_to(c), new_jst); - else - push_updated_constraint(c, convertible_from(c), new_a, new_jst); - } - } - - /** - \brief Auxiliary method for pushing a new constraint to the constraint queue. - The new constraint is obtained from \c c by one or more normalization steps that produce \c new_a and \c new_b - */ - void push_normalized_constraint(unification_constraint const & c, expr const & new_a, expr const & new_b) { - push_updated_constraint(c, new_a, new_b, justification(new normalize_justification(c))); - } - - justification mk_failure_justification(unification_constraint const & c) { - return justification(new unification_failure_justification(c, m_state.m_menv.copy())); - } - - /** - \brief Assign \c v to \c m with justification \c tr in the current state. - */ - bool assign(expr const & m, expr const & v, unification_constraint const & c, bool is_lhs) { - lean_assert(is_metavar(m)); - if (instantiate_metavars(!is_lhs, v, c)) // make sure v does not have assigned metavars - return true; - context const & ctx = get_context(c); - justification jst(new assignment_justification(c)); - metavar_env const & menv = m_state.m_menv; - if (!menv->assign(m, v, jst)) { - m_conflict = mk_failure_justification(c); - return false; - } - if (menv->has_type(m)) { - buffer ucs; - expr tv = m_type_inferer(v, ctx, menv, ucs); - push_active(ucs); - justification new_jst(new typeof_mvar_justification(ctx, m, menv->get_type(m), tv, jst)); - push_active(mk_eq_constraint(ctx, tv, menv->get_type(m), new_jst)); - } - m_state.m_recently_assigned.insert(metavar_name(m)); - return true; - } - - bool process(unification_constraint const & c) { - switch (c.kind()) { - case unification_constraint_kind::Eq: return process_eq(c); - case unification_constraint_kind::Convertible: return process_convertible(c); - case unification_constraint_kind::Max: return process_max(c); - case unification_constraint_kind::Choice: return process_choice(c); - } - lean_unreachable(); // LCOV_EXCL_LINE - return true; - } - - bool process_eq(unification_constraint const & c) { - return process_eq_convertible(get_context(c), eq_lhs(c), eq_rhs(c), c); - } - - bool process_convertible(unification_constraint const & c) { - return process_eq_convertible(get_context(c), convertible_from(c), convertible_to(c), c); - } - - /** - Process ctx |- a ≈ b and ctx |- 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 { Processed, Failed, Continue }; - status process_metavar(unification_constraint const & c, expr const & a, expr const & b, bool is_lhs) { - context const & ctx = get_context(c); - lean_assert(!(is_metavar(a) && is_assigned(a))); - lean_assert(!(is_metavar(b) && is_assigned(b))); - if (is_metavar(a)) { - if (!has_local_context(a)) { - // Case 2 - if (has_metavar(b, a)) { - m_conflict = mk_failure_justification(c); - return Failed; - } else if (is_eq(c) || is_proposition(b, ctx)) { - // At this point, we only assign metavariables if the constraint is an equational constraint, - // or b is a proposition. - // It is important to handle propositions since we don't want to normalize them. - // The normalization process destroys the structure of the proposition. - return assign(a, b, c, is_lhs) ? Processed : Failed; - } - } else { - if (!is_metavar(b) && has_metavar(b, a)) { - m_conflict = mk_failure_justification(c); - return Failed; - } - local_entry const & me = head(metavar_lctx(a)); - if (me.is_lift()) { - // Case 3 - // a is of the form ?m[lift:s:n] - unsigned s = me.s(); - unsigned n = me.n(); - // Let ctx be of the form - // [ce_{m-1}, ..., ce_{s+n}, ce_{s+n-1}, ..., ce_s, ce_{s-1}, ..., ce_0] - // Then, we reduce - // [ce_{m-1}, ..., ce_{s+n}, ce_{s+n-1}, ..., ce_s, ce_{s-1}, ..., ce_0] |- ?m[lift:s:n] ≈ b - // to - // [ce_{m-1}, ..., ce_{s+n}, lower(ce_{s-1}, n, n), ..., lower(ce_0, s + n - 1, n)] |- ?m ≈ lower(b, s + n, n) - // - // Remark: we have to check if the lower operations are applicable using the operation has_free_var. - // - if (!has_free_var(b, s, s + n, m_state.m_menv)) { - optional new_ctx = ctx.remove(s, n, m_state.m_menv); // method remove will lower the entries ce_0, ..., ce_{s-1} - if (!new_ctx) - return Continue; // rule is not applicable because we cannot lower the entries. - justification new_jst(new normalize_justification(c)); - expr new_a = pop_meta_context(a); - expr new_b = lower_free_vars(b, s + n, n, m_state.m_menv); - if (!is_lhs) - swap(new_a, new_b); - push_new_constraint(is_eq(c), *new_ctx, new_a, new_b, new_jst); - return Processed; - } - } - } - } - - if (is_app(a) && is_metavar(arg(a, 0)) && is_assigned(arg(a, 0))) { - // Case 4 - auto s_j = get_subst_jst(arg(a, 0)); - justification new_jst(new substitution_justification(c, s_j.second)); - expr new_f = s_j.first; - expr new_a = update_app(a, 0, new_f); - if (m_state.m_menv->beta_reduce_metavar_application()) - new_a = head_beta_reduce(new_a); - push_updated_constraint(c, is_lhs, new_a, new_jst); - return Processed; - } - return Continue; - } - - bool check_metavar_lift(unification_constraint const & c, expr const & a, expr const & b) { - if (is_metavar(a) && has_local_context(a) && !has_metavar(b)) { - lean_assert(!is_assigned(a)); - local_entry const & me = head(metavar_lctx(a)); - if (me.is_lift()) { - // a is of the form ?m[lift:s:n] - unsigned s = me.s(); - unsigned n = me.n(); - if (has_free_var(b, s, s + n, m_state.m_menv)) { - // Failure, there is no way to unify - // ?m[lift:s:n, ...] with a term that contains variables in [s, s+n] - - // In older commits, this check was being done inside of process_metavar. - // This was incorrect. This check must be performed AFTER b is normalized. - m_conflict = mk_failure_justification(c); - return false; - } - } - } - return true; - } - - justification mk_subst_justification(unification_constraint const & c, buffer const & subst_justifications) { - if (subst_justifications.size() == 1) { - return justification(new substitution_justification(c, subst_justifications[0])); - } else { - return justification(new multi_substitution_justification(c, subst_justifications.size(), subst_justifications.data())); - } - } - - /** - \brief Instantiate the assigned metavariables in \c a, and store the justifications - in \c jsts. - */ - expr instantiate_metavars(expr const & a, buffer & jsts) { - lean_assert(has_assigned_metavar(a)); - return m_state.m_menv->instantiate_metavars(a, jsts); - } - - /** - \brief Return true iff \c a contains instantiated variables. If this is the case, - then constraint \c c is updated with a new \c a s.t. all metavariables of \c a - are instantiated. - - \remark if \c is_lhs is true, then we are considering the left-hand-side of the constraint \c c. - */ - bool instantiate_metavars(bool is_lhs, expr const & a, unification_constraint const & c) { - lean_assert(is_eq(c) || is_convertible(c)); - lean_assert(!is_eq(c) || !is_lhs || is_eqp(eq_lhs(c), a)); - lean_assert(!is_eq(c) || is_lhs || is_eqp(eq_rhs(c), a)); - lean_assert(!is_convertible(c) || !is_lhs || is_eqp(convertible_from(c), a)); - lean_assert(!is_convertible(c) || is_lhs || is_eqp(convertible_to(c), a)); - if (has_assigned_metavar(a)) { - buffer jsts; - expr new_a = instantiate_metavars(a, jsts); - justification new_jst = mk_subst_justification(c, jsts); - push_updated_constraint(c, is_lhs, new_a, new_jst); - return true; - } else { - return false; - } - } - - /** \brief Unfold let-expression */ - void process_let(expr & a) { - if (is_let(a)) - a = instantiate(let_body(a), let_value(a), m_state.m_menv); - } - - /** \brief Replace variables by their definition if the context contains it. */ - void process_var(context const & ctx, expr & a) { - if (is_var(a)) { - auto e = find(ctx, var_idx(a)); - if (e && e->get_body()) - a = lift_free_vars(*(e->get_body()), var_idx(a) + 1, m_state.m_menv); - } - } - - expr normalize(context const & ctx, expr const & a) { - return m_normalizer(a, ctx, m_state.m_menv); - } - - void process_app(context const & ctx, expr & a) { - if (is_app(a)) { - expr f = arg(a, 0); - if (is_value(f) && m_use_normalizer) { - // if f is a semantic attachment, we keep normalizing children from - // left to right until the semantic attachment is applicable - buffer new_args; - new_args.append(num_args(a), &(arg(a, 0))); - bool modified = false; - expr r; - for (unsigned i = 1; i < new_args.size(); i++) { - expr const & curr = new_args[i]; - expr new_curr = normalize(ctx, curr); - if (curr != new_curr) { - modified = true; - new_args[i] = new_curr; - if (optional r = to_value(f).normalize(new_args.size(), new_args.data())) { - a = *r; - return; - } - } - } - if (optional r = to_value(f).normalize(new_args.size(), new_args.data())) { - a = *r; - return; - } - if (modified) { - a = mk_app(new_args); - return; - } - } else { - process_let(f); - process_var(ctx, f); - f = head_beta_reduce(f); - a = update_app(a, 0, f); - a = head_beta_reduce(a); - } - } - } - - void process_proj(context const & ctx, expr & a) { - if (is_proj(a)) { - expr const & arg = proj_arg(a); - expr new_arg = arg; - if (m_use_normalizer) - new_arg = normalize(ctx, arg); - if (is_dep_pair(new_arg)) { - if (proj_first(a)) - a = pair_first(new_arg); - else - a = pair_second(new_arg); - } else { - a = update_proj(a, new_arg); - } - } - } - - expr normalize_step(context const & ctx, expr const & a) { - expr new_a = a; - process_let(new_a); - process_var(ctx, new_a); - process_app(ctx, new_a); - process_proj(ctx, new_a); - return new_a; - } - - int get_const_weight(expr const & a) { - lean_assert(is_constant(a)); - optional obj = m_env->find_object(const_name(a)); - if (should_unfold(obj)) - return obj->get_weight(); - else - return -1; - } - - /** - \brief Return a number >= 0 if \c a is a defined constant or the application of a defined constant. - In this case, the value is the weight of the definition. - */ - int get_unfolding_weight(expr const & a) { - if (is_constant(a)) - return get_const_weight(a); - else if (is_app(a) && is_constant(arg(a, 0))) - return get_const_weight(arg(a, 0)); - else - return -1; - } - - expr unfold(expr const & a) { - lean_assert(is_constant(a) || (is_app(a) && is_constant(arg(a, 0)))); - if (is_constant(a)) { - lean_assert(m_env->find_object(const_name(a))); - return m_env->find_object(const_name(a))->get_value(); - } else { - lean_assert(m_env->find_object(const_name(arg(a, 0)))); - return update_app(a, 0, m_env->find_object(const_name(arg(a, 0)))->get_value()); - } - } - - bool normalize_head(expr a, expr b, unification_constraint const & c) { - context const & ctx = get_context(c); - bool modified = false; - while (true) { - check_system(); - expr new_a = normalize_step(ctx, a); - expr new_b = normalize_step(ctx, b); - if (new_a == a && new_b == b) { - if (is_meta(a) || is_meta(b)) - break; // we do not unfold if one of the arguments is a metavar or metavar_app - int w_a = get_unfolding_weight(a); - int w_b = get_unfolding_weight(b); - if (w_a >= 0 || w_b >= 0) { - if (w_a >= w_b) - new_a = unfold(a); - if (w_b >= w_a) - new_b = unfold(b); - if (new_a == a && new_b == b) - break; - } else { - break; - } - } - modified = true; - a = new_a; - b = new_b; - if (a == b) { - return true; - } - } - if (modified) { - push_normalized_constraint(c, a, b); - return true; - } else { - return false; - } - } - - /** \brief Return true iff the variable with id \c vidx has a body/definition in the context \c ctx. */ - static bool has_body(context const & ctx, unsigned vidx) { - auto e = find(ctx, vidx); - return e && e->get_body(); - } - - /** - \brief Return true iff \c a may be an actual lower bound for a convertibility constraint. - That is, if the result is false, it means the convertability constraint is essentially - an equality constraint. - */ - bool is_actual_lower(expr const & a) { - return is_type(a) || is_metavar(a) || is_bool(a) || (is_pi(a) && is_actual_lower(abst_body(a))); - } - - /** - \brief Return true iff \c a may be an actual upper bound for a convertibility constraint. - That is, if the result is false, it means the convertability constraint is essentially - an equality constraint. - */ - bool is_actual_upper(expr const & a) { - return is_type(a) || is_metavar(a) || (is_pi(a) && is_actual_upper(abst_body(a))); - } - - optional try_get_type(context const & ctx, expr const & e) { - try { - return some_expr(m_type_inferer(e, ctx)); - } catch (...) { - return none_expr(); - } - } - - /** - \brief Return true iff all arguments of the application \c a are variables that do - not have a definition in \c ctx. - */ - static bool are_args_vars(context const & ctx, expr const & a) { - lean_assert(is_app(a)); - for (unsigned i = 1; i < num_args(a); i++) { - if (!is_var(arg(a, i))) - return false; - if (has_body(ctx, var_idx(arg(a, i)))) - return false; - } - return true; - } - - /** - \brief are_args_vars(a) && all variables are distinct - */ - static bool are_args_distinct_vars(context const & ctx, expr const & a) { - if (!are_args_vars(ctx, a)) - return false; - buffer found; - for (unsigned i = 1; i < num_args(a); i++) { - unsigned vidx = var_idx(arg(a, i)); - if (vidx >= found.size()) - found.resize(vidx+1, false); - if (found[vidx]) - return false; - found[vidx] = true; - } - return true; - } - - /** - \brief See \c process_simple_ho_match (case 1) - */ - bool is_simple_ho_match_closed(context const & ctx, expr const & a, expr const & b, bool is_lhs, unification_constraint const & c) { - return is_meta_app(a) && are_args_vars(ctx, a) && closed(b) && - (is_eq(c) || (is_lhs && !is_actual_upper(b)) || (!is_lhs && !is_actual_lower(b))); - } - - /** - \brief See \c process_simple_ho_match (case 2) - */ - bool is_simple_ho_match_app(context const & ctx, expr const & a, expr const & b, bool is_lhs, unification_constraint const & c) { - if (is_meta_app(a) && are_args_distinct_vars(ctx, a) && is_app(b) && !is_meta_app(b) && - num_args(a) == num_args(b) && - (is_eq(c) || (is_lhs && !is_actual_upper(b)) || (!is_lhs && !is_actual_lower(b)))) { - // check if a and b have the same arguments - for (unsigned i = 1; i < num_args(a); i++) { - if (arg(a, i) != arg(b, i)) - return false; - } - // a is of the form (?m x1 ... xn) AND b is of the form (f x1 ... xn) - // f should not contain any xi - bool failed = false; - for_each(arg(b, 0), [&](expr const & e, unsigned offset) { - if (failed) - return false; // abort search - if (is_var(e)) { - unsigned vidx = var_idx(e); - if (vidx >= offset) { - vidx -= offset; - for (unsigned i = 1; i < num_args(a); i++) { - if (var_idx(arg(a, i)) == vidx) { - failed = true; - return false; - } - } - } - } - return true; // continue search - }); - return !failed; - } else { - return false; - } - } - - /** - \brief Return true iff ctx |- a ≈ b is a "simple" higher-order matching constraint. By simple, we mean - - 1) a constraint of the form - ctx |- (?m x1 ... xn) ≈ c where c is closed - The constraint is solved by assigning ?m to (fun x1 ... xn, c). - The arguments may contain duplicate occurrences of variables. - - The following case is INCORRECT, and restricts the set of solutions that can be found. - IT WAS DISABLED. - 2) a constraint of the form - ctx |- (?m x1 ... xn) ≈ (f x1 ... xn) where f does not contain x1 ... xn, and x1 ... xn are distinct - The constraint is solved by assigning ?m to f OR ?m to (fun x1 ... xn, f x1 ... xn) - */ - bool process_simple_ho_match(context const & ctx, expr const & a, expr const & b, bool is_lhs, unification_constraint const & c) { - // Solve constraint of the form - // ctx |- (?m x) ≈ c - // using imitation - bool eq_closed = is_simple_ho_match_closed(ctx, a, b, is_lhs, c); - bool eq_app = is_simple_ho_match_app(ctx, a, b, is_lhs, c); - if (eq_closed || eq_app) { - expr m = arg(a, 0); - buffer types; - for (unsigned i = 1; i < num_args(a); i++) { - optional d = try_get_type(ctx, arg(a, i)); - if (d) - types.push_back(*d); - else - return false; - } - if (eq_closed) { - justification new_jst(new destruct_justification(c)); - expr s = mk_lambda(types, b); - push_new_eq_constraint(ctx, m, s, new_jst); - return true; - } else { - return false; - #if 0 - // This code was disabled because it removes valid solutions. - // For example, when this piece of code is enabled, we can't - // solve - // theorem or_imp (p q : Bool) : (p ∨ q) ↔ (¬ p → q) - // := subst (symm (imp_or (¬ p) q)) (not_not_eq p) - // TODO(Leo): delete this piece of code - lean_assert(eq_app); - expr f = arg(b, 0); - std::unique_ptr new_cs(new generic_case_split(c, m_state)); - { - // eta-expanded version: m = fun x1 ... xn, f x1 ... xn - unsigned n = types.size(); - expr s = mk_lambda(types, mk_app_vars(lift_free_vars(f, 0, n), n)); - state new_state(m_state); - justification new_assumption = mk_assumption(); - push_new_eq_constraint(new_state.m_active_cnstrs, ctx, m, s, new_assumption); - new_cs->push_back(new_state, new_assumption); - } - { - // m = f - state new_state(m_state); - justification new_assumption = mk_assumption(); - push_new_eq_constraint(new_state.m_active_cnstrs, ctx, m, f, new_assumption); - new_cs->push_back(new_state, new_assumption); - } - // add case split - bool r = new_cs->next(*this); - lean_assert(r); - m_case_splits.push_back(std::move(new_cs)); - return r; - #endif - } - } else { - return false; - } - } - - /** - \brief Auxiliary method for \c process_meta_app. Add new case-splits to new_cs - */ - void process_meta_app_core(std::unique_ptr & new_cs, expr const & a, expr const & b, bool is_lhs, - unification_constraint const & c) { - lean_assert(is_meta_app(a)); - context const & ctx = get_context(c); - metavar_env & menv = m_state.m_menv; - expr f_a = arg(a, 0); - lean_assert(is_metavar(f_a)); - unsigned num_a = num_args(a); - buffer arg_types; - buffer ucs; - for (unsigned i = 1; i < num_a; i++) { - arg_types.push_back(m_type_inferer(arg(a, i), ctx, menv, ucs)); - push_active(ucs); - } - // Add imitation - state new_state(m_state); - justification new_assumption = mk_assumption(); - expr imitation; - // Auxiliary function for creating the term - // (h[lift:0:num_a-1] #0 ... #(num_a-1)) - auto mk_app_h_vars = [&](expr const & h) { - lean_assert(is_metavar(h)); - return mk_app_vars(add_lift(h, 0, num_a - 1), num_a - 1); - }; - lean_assert(arg_types.size() == num_a - 1); - 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_1) ... (x_{num_a} : T_{num_a}), f_b (h_1 x_1 ... x_{num_a}) ... (h_{num_b} x_1 ... x_{num_a}) - // New constraints (h_i a_1 ... a_{num_a}) ≈ arg(b, i) - buffer imitation_args; // arguments for the imitation - imitation_args.push_back(lift_free_vars(f_b, 0, num_a - 1, new_state.m_menv)); - for (unsigned i = 1; i < num_b; i++) { - expr h_i = new_state.m_menv->mk_metavar(ctx); - imitation_args.push_back(mk_app_h_vars(h_i)); - push_new_eq_constraint(new_state.m_active_cnstrs, ctx, update_app(a, 0, h_i), arg(b, i), new_assumption); - } - imitation = mk_lambda(arg_types, mk_app(imitation_args)); - } else if (is_abstraction(b)) { - // Imitation for lambdas, Pis, and Sigmas - // Assign f_a <- fun (x_1 : T_1) ... (x_{num_a} : T_{num_a}), - // fun (x_b : (?h_1 x_1 ... x_{num_a})), (?h_2 x_1 ... x_{num_a} x_b) - // New constraints (h_1 a_1 ... a_{num_a}) ≈ abst_domain(b) - // (h_2 a_1 ... a_{num_a} x_b) ≈ abst_body(b) - expr h_1 = new_state.m_menv->mk_metavar(ctx); - context new_ctx = extend(ctx, abst_name(b), abst_domain(b)); - expr h_2 = new_state.m_menv->mk_metavar(extend(ctx, abst_name(b), abst_domain(b))); - push_new_eq_constraint(new_state.m_active_cnstrs, ctx, update_app(a, 0, h_1), abst_domain(b), new_assumption); - if (is_arrow(b)) { - push_new_eq_constraint(new_state.m_active_cnstrs, new_ctx, - update_app(lift_free_vars(a, 1), 0, h_2), abst_body(b), new_assumption); - imitation = mk_lambda(arg_types, update_abstraction(b, mk_app_h_vars(h_1), mk_app_vars(add_lift(h_2, 1, num_a - 1), num_a - 1, 1))); - } else { - push_new_eq_constraint(new_state.m_active_cnstrs, new_ctx, - mk_app(update_app(lift_free_vars(a, 1), 0, h_2), mk_var(0)), abst_body(b), new_assumption); - imitation = mk_lambda(arg_types, update_abstraction(b, mk_app_h_vars(h_1), mk_app_vars(add_lift(h_2, 1, num_a - 1), num_a))); - } - } else if (is_heq(b)) { - // Imitation for heterogeneous equality - expr h_1 = new_state.m_menv->mk_metavar(ctx); - expr h_2 = new_state.m_menv->mk_metavar(ctx); - push_new_eq_constraint(new_state.m_active_cnstrs, ctx, update_app(a, 0, h_1), heq_lhs(b), new_assumption); - push_new_eq_constraint(new_state.m_active_cnstrs, ctx, update_app(a, 0, h_2), heq_rhs(b), new_assumption); - imitation = mk_lambda(arg_types, mk_heq(mk_app_h_vars(h_1), mk_app_h_vars(h_2))); - } else if (is_dep_pair(b)) { - // Imitation for dependent pairs - expr h_f = new_state.m_menv->mk_metavar(ctx); - expr h_s = new_state.m_menv->mk_metavar(ctx); - expr h_t = new_state.m_menv->mk_metavar(ctx); - push_new_eq_constraint(new_state.m_active_cnstrs, ctx, update_app(a, 0, h_f), pair_first(b), new_assumption); - push_new_eq_constraint(new_state.m_active_cnstrs, ctx, update_app(a, 0, h_s), pair_second(b), new_assumption); - push_new_eq_constraint(new_state.m_active_cnstrs, ctx, update_app(a, 0, h_t), pair_type(b), new_assumption); - imitation = mk_lambda(arg_types, mk_pair(mk_app_h_vars(h_f), mk_app_h_vars(h_s), mk_app_h_vars(h_t))); - } else if (is_proj(b)) { - // Imitation for pair-projection - expr h_a = new_state.m_menv->mk_metavar(ctx); - push_new_eq_constraint(new_state.m_active_cnstrs, ctx, update_app(a, 0, h_a), proj_arg(b), new_assumption); - imitation = mk_lambda(arg_types, mk_proj(proj_first(b), mk_app_h_vars(h_a))); - } else { - // "Dumb imitation" aka the constant function - // Assign f_a <- fun (x_1 : T_1) ... (x_{num_a} : T_{num_a}), b - imitation = mk_lambda(arg_types, lift_free_vars(b, 0, num_a - 1, new_state.m_menv)); - } - push_new_eq_constraint(new_state.m_active_cnstrs, ctx, f_a, imitation, new_assumption); - new_cs->push_back(new_state, new_assumption); - // 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 - state new_state(m_state); - justification new_assumption = mk_assumption(); - expr proj = mk_lambda(arg_types, mk_var(num_a - i - 1)); - expr new_a = arg(a, i); - expr new_b = b; - if (!is_lhs) - swap(new_a, new_b); - push_new_constraint(new_state.m_active_cnstrs, is_eq(c), ctx, new_a, new_b, new_assumption); - push_new_eq_constraint(new_state.m_active_cnstrs, ctx, f_a, proj, new_assumption); - new_cs->push_back(new_state, new_assumption); - } - } - - /** - \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(expr const & a, expr const & b, bool is_lhs, unification_constraint const & c, - bool flex_flex = false, bool local_ctx = false) { - if (!is_meta_app(a)) - return false; - if (!local_ctx && has_local_context(arg(a, 0))) - return false; - if (!flex_flex) { - if (is_meta_app(b)) - return false; - if (is_abstraction(b) && is_meta_app(abst_domain(b)) && is_meta_app(abst_body(b))) - return false; - } - if (!(is_eq(c) || (is_lhs && !is_actual_upper(b)) || (!is_lhs && !is_actual_lower(b)))) - return false; - std::unique_ptr new_cs(new generic_case_split(c, m_state)); - process_meta_app_core(new_cs, a, b, is_lhs, c); - if (flex_flex && is_meta_app(b)) - process_meta_app_core(new_cs, b, a, !is_lhs, c); - bool r = new_cs->next(*this); - lean_assert(r); - m_case_splits.push_back(std::move(new_cs)); - return r; - } - - /** \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 Return true if \c a is of the form ?m[lift:s:n, ...] */ - bool is_metavar_lift(expr const & a) const { - return is_metavar(a) && has_local_context(a) && head(metavar_lctx(a)).is_lift(); - } - - /** - \brief Collect possible solutions for ?m given a constraint of the form - ctx |- ?m[lctx] ≈ b - where b is a Constant, Type, Value or Variable. - - We only need the local context \c lctx and \c b for computing the set of possible solutions. - The result is stored in \c solutions. - - We may have more than one solution. Here is an example: - - ?m[inst:3:b, lift:1:1, inst:2:b] ≈ b - - The possible solutions is the set of solutions for - 1- ?m[lift:1:1, inst:2:b] ≈ #3 - 2- ?m[lift:1:1, inst:2:b] ≈ b - - The solutions for constraints 1 and 2 are the solutions for - 1.1- ?m[inst:2:b] ≈ #2 - 2.1- ?m[inst:2:b] ≈ b - - And 1.1 has two possible solutions - 1.1.1 ?m ≈ #3 - 1.1.2 ?m ≈ b - - And 2.1 has also two possible solutions - 2.1.1 ?m ≈ #2 - 2.1.2 ?m ≈ b - - Thus, the resulting set of solutions is {#3, b, #2} - */ - void collect_metavar_solutions(local_context const & lctx, expr const & b, buffer & solutions) { - lean_assert(is_constant(b) || is_type(b) || is_value(b) || is_var(b)); - if (lctx) { - local_entry const & e = head(lctx); - if (e.is_inst()) { - if (e.v() == b || has_metavar(e.v())) { - // There is an extra possible solution #{e.s()} - // If e.v() has metavariables, then it may become equal to b. - collect_metavar_solutions(tail(lctx), mk_var(e.s()), solutions); - } - if (is_var(b) && var_idx(b) >= e.s()) { - collect_metavar_solutions(tail(lctx), mk_var(var_idx(b) + 1), solutions); - } else { - collect_metavar_solutions(tail(lctx), b, solutions); - } - } else { - lean_assert(e.is_lift()); - if (is_var(b) && var_idx(b) >= e.s() + e.n()) { - collect_metavar_solutions(tail(lctx), mk_var(var_idx(b) - e.n()), solutions); - } else { - collect_metavar_solutions(tail(lctx), b, solutions); - } - } - } else { - lean_assert(length(lctx) == 0); - if (std::find(solutions.begin(), solutions.end(), b) == solutions.end()) - solutions.push_back(b); // insert new solution - } - } - - /** - \brief Return true if the local context contains a metavariable. - */ - bool local_context_has_metavar(local_context const & lctx) { - for (auto const & e : lctx) { - if (e.is_inst() && has_metavar(e.v())) - return true; - } - return false; - } - - /** - \brief Solve a constraint of the form - ctx |- a ≈ b - where - a is of the form ?m[...] i.e., metavariable with a non-empty local context. - b is an abstraction - - We solve the constraint by assigning a to an abstraction with fresh metavariables. - */ - void imitate_abstraction(expr const & a, expr const & b, unification_constraint const & c) { - lean_assert(is_metavar(a)); - lean_assert(is_abstraction(b)); - lean_assert(!is_assigned(a)); - lean_assert(has_local_context(a)); - // imitate - push_active(c); - // a <- (fun x : ?h1, ?h2), or (Pi x : ?h1, ?h2), or (Sigma x : ?h1, ?h2) - // ?h1 is in the same context where 'a' was defined - // ?h2 is in the context of 'a' + domain of b - expr m = mk_metavar(metavar_name(a)); - context ctx_m = m_state.m_menv->get_context(m); - expr h_1 = m_state.m_menv->mk_metavar(ctx_m); - expr h_2 = m_state.m_menv->mk_metavar(extend(ctx_m, abst_name(b), abst_domain(b))); - expr imitation = update_abstraction(b, h_1, h_2); - justification new_jst(new imitation_justification(c)); - push_new_constraint(true, ctx_m, m, imitation, new_jst); - } - - /** - \brief Similar to imitate_abstraction, but b is an application, where the function - is a Variable, Constant or Value. - */ - void imitate_application(expr const & a, expr const & b, unification_constraint const & c) { - lean_assert(is_metavar(a)); - lean_assert(is_app(b) && (is_var(arg(b, 0)) || is_constant(arg(b, 0)) || is_value(arg(b, 0)))); - lean_assert(!is_assigned(a)); - lean_assert(has_local_context(a)); - // Create a fresh meta variable for each argument of b. - // The new metavariables have the same context of a. - expr m = mk_metavar(metavar_name(a)); - context ctx_m = m_state.m_menv->get_context(m); - expr f_b = arg(b, 0); - buffer new_args; - new_args.push_back(expr()); // save space. - unsigned num = num_args(b); - for (unsigned i = 1; i < num; i++) - new_args.push_back(m_state.m_menv->mk_metavar(ctx_m)); - // We may have many different imitations. - local_context lctx = metavar_lctx(a); - buffer solutions; - collect_metavar_solutions(lctx, f_b, solutions); - lean_assert(solutions.size() >= 1); - if (solutions.size() == 1) { - new_args[0] = solutions[0]; - expr imitation = mk_app(new_args); - justification new_jst(new imitation_justification(c)); - push_active(c); - push_new_constraint(true, ctx_m, m, imitation, new_jst); - } else { - // More than one solution. We must create a case-split. - std::unique_ptr new_cs(new generic_case_split(c, m_state)); - for (auto s : solutions) { - new_args[0] = s; - expr imitation = mk_app(new_args); - state new_state(m_state); - justification new_assumption = mk_assumption(); - push_front(new_state.m_active_cnstrs, c); - push_new_eq_constraint(new_state.m_active_cnstrs, ctx_m, m, imitation, new_assumption); - new_cs->push_back(new_state, new_assumption); - } - lean_verify(new_cs->next(*this)); - m_case_splits.push_back(std::move(new_cs)); - } - } - /** - \brief Solve a constraint of the form - ctx |- a ≈ b - where - a is of the form ?m[...] i.e., metavariable with a non-empty local context. - b is a pair projection. - - We solve the constraint by assigning a to an abstraction with fresh metavariables. - */ - - void imitate_proj(expr const & a, expr const & b, unification_constraint const & c) { - lean_assert(is_metavar(a)); - lean_assert(is_proj(b)); - lean_assert(!is_assigned(a)); - lean_assert(has_local_context(a)); - // imitate - push_active(c); - // a <- (proj1/2 ?h_1) - // ?h_1 is in the same context where 'a' was defined - expr m = mk_metavar(metavar_name(a)); - context ctx_m = m_state.m_menv->get_context(m); - expr h_1 = m_state.m_menv->mk_metavar(ctx_m); - expr imitation = update_proj(b, h_1); - justification new_jst(new imitation_justification(c)); - push_new_constraint(true, ctx_m, m, imitation, new_jst); - } - - /** - \brief Solve a constraint of the form - ctx |- a ≈ b - where - a is of the form ?m[...] i.e., metavariable with a non-empty local context. - b is a dependent pair - - We solve the constraint by assigning a to an abstraction with fresh metavariables. - */ - - void imitate_pair(expr const & a, expr const & b, unification_constraint const & c) { - lean_assert(is_metavar(a)); - lean_assert(is_dep_pair(b)); - lean_assert(!is_assigned(a)); - lean_assert(has_local_context(a)); - // imitate - push_active(c); - // a <- (pair ?h_1 ?h_2 ?h_3) - // ?h_i are in the same context where 'a' was defined - expr m = mk_metavar(metavar_name(a)); - context ctx_m = m_state.m_menv->get_context(m); - expr h_1 = m_state.m_menv->mk_metavar(ctx_m); - expr h_2 = m_state.m_menv->mk_metavar(ctx_m); - expr h_3 = m_state.m_menv->mk_metavar(ctx_m); - expr imitation = mk_pair(h_1, h_2, h_3); - justification new_jst(new imitation_justification(c)); - push_new_constraint(true, ctx_m, m, imitation, new_jst); - } - - /** - \brief Solve a constraint of the form - ctx |- a ≈ b - where - a is of the form ?m[...] i.e., metavariable with a non-empty local context. - b is a heterogeneous equality - - We solve the constraint by assigning a to an abstraction with fresh metavariables. - */ - void imitate_heq(expr const & a, expr const & b, unification_constraint const & c) { - lean_assert(is_metavar(a)); - lean_assert(is_heq(b)); - lean_assert(!is_assigned(a)); - lean_assert(has_local_context(a)); - // imitate - push_active(c); - // a <- ?h_1 == ?h_2 - // ?h_i are in the same context where 'a' was defined - expr m = mk_metavar(metavar_name(a)); - context ctx_m = m_state.m_menv->get_context(m); - expr h_1 = m_state.m_menv->mk_metavar(ctx_m); - expr h_2 = m_state.m_menv->mk_metavar(ctx_m); - expr imitation = mk_heq(h_1, h_2); - justification new_jst(new imitation_justification(c)); - push_new_constraint(true, ctx_m, m, imitation, new_jst); - } - - /** - \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 (for constants, variables, values and Type) - Case 2) imitate b - */ - bool process_metavar_inst(expr const & a, expr const & b, bool is_lhs, unification_constraint const & c) { - // This method is miss some cases. In particular the local context of \c a contains metavariables. - // - // (f#2 #1) ≈ ?M2[i:1 ?M1] - // - // A possible solution for this constraint is: - // ?M2 ≈ #1 - // ?M1 ≈ f#2 #1 - // - // TODO(Leo): consider the following alternative design: We do NOT use approximations, since it is quite - // hard to understand what happened when they do not work. Instead, we rely on user provided plugins - // for handling the nasty cases. - // - // TODO(Leo): another possible design is to inform the user where approximation was used. - if (is_metavar_inst(a) && (is_eq(c) || (is_lhs && !is_actual_upper(b)) || (!is_lhs && !is_actual_lower(b)))) { - lean_assert(!is_assigned(a)); - if (is_constant(b) || is_type(b) || is_value(b) || is_var(b)) { - local_context lctx = metavar_lctx(a); - buffer solutions; - collect_metavar_solutions(lctx, b, solutions); - lean_assert(solutions.size() >= 1); - bool keep_c = local_context_has_metavar(metavar_lctx(a)); - expr m = mk_metavar(metavar_name(a)); - context ctx_m = m_state.m_menv->get_context(m); - if (solutions.size() == 1) { - justification new_jst(new destruct_justification(c)); - if (keep_c) - push_active(c); - push_new_eq_constraint(ctx_m, m, solutions[0], new_jst); - return true; - } else { - // More than one solution. We must create a case-split. - std::unique_ptr new_cs(new generic_case_split(c, m_state)); - for (auto s : solutions) { - state new_state(m_state); - justification new_assumption = mk_assumption(); - if (keep_c) - push_front(new_state.m_active_cnstrs, c); - push_new_eq_constraint(new_state.m_active_cnstrs, ctx_m, m, s, new_assumption); - new_cs->push_back(new_state, new_assumption); - } - bool r = new_cs->next(*this); - lean_assert(r); - m_case_splits.push_back(std::move(new_cs)); - return r; - } - } else if (is_abstraction(b)) { - imitate_abstraction(a, b, c); - return true; - } else if (is_app(b) && (is_var(arg(b, 0)) || is_constant(arg(b, 0)) || is_value(arg(b, 0)))) { - imitate_application(a, b, c); - return true; - } else if (is_proj(b)) { - imitate_proj(a, b, c); - return true; - } else if (is_heq(b)) { - imitate_heq(a, b, c); - return true; - } else if (is_dep_pair(b)) { - imitate_pair(a, b, c); - return true; - } - } - return false; - } - - /** - \brief Process a constraint of the form ctx |- ?m[lift, ...] ≈ b where \c b is an abstraction. - That is, \c b is a Pi or Lambda. In both cases, ?m must have the same kind. - We just add a new assignment that forces ?m to have the corresponding kind. - - Remark: we can expand this method and support application and equality - */ - bool process_metavar_lift_abstraction(expr const & a, expr const & b, unification_constraint const & c) { - if (is_metavar_lift(a) && is_abstraction(b)) { - imitate_abstraction(a, b, c); - return true; - } else { - return false; - } - } - - /** - \brief Return true iff c is a constraint of the form ctx |- a << ?m, where \c a is Type or Bool - */ - bool is_lower(unification_constraint const & c) { - return - is_convertible(c) && - (is_metavar(convertible_to(c)) || is_meta_app(convertible_to(c))) && - (is_bool(convertible_from(c)) || is_type(convertible_from(c))); - } - - /** \brief Process constraint of the form ctx |- a << ?m, where \c a is Type or Bool */ - bool process_lower(expr const & a, expr const & b, unification_constraint const & c) { - if (is_lower(c)) { - // Remark: in principle, there are infinite number of choices. - // We approximate and only consider the most useful ones. - justification new_jst(new destruct_justification(c)); - if (is_bool(a)) { - expr choices[3] = { Bool, Type(), TypeU }; - push_active(mk_choice_constraint(get_context(c), b, 3, choices, new_jst)); - return true; - } else if (m_env->is_ge(ty_level(a), m_U)) { - expr choices[2] = { a, Type(ty_level(a) + 1) }; - push_active(mk_choice_constraint(get_context(c), b, 2, choices, new_jst)); - return true; - } else { - expr choices[4] = { a, Type(ty_level(a) + 1), TypeU }; - push_active(mk_choice_constraint(get_context(c), b, 4, choices, new_jst)); - return true; - } - } else { - return false; - } - } - - /** - \brief Return true if the current queue contains a constraint that satisfies the predicate p - */ - template - bool has_constraint(P p) { - for (auto const & c : m_state.m_active_cnstrs) { - if (p(c)) - return true; - } - for (auto const & c : m_state.m_delayed_cnstrs) { - if (p(c.first)) - return true; - } - return false; - } - - /** - \brief Return true iff the current queue has a max constraint of the form ctx |- max(L1, L2) ≈ a. - - \pre is_metavar(a) - */ - bool has_max_constraint(expr const & a) { - lean_assert(is_metavar(a)); - return has_constraint([&](unification_constraint const & c) { return is_max(c) && max_rhs(c) == a; }); - } - - - /** - \brief Return true iff the current queue has a constraint that is a lower bound for \c a. - \pre is_metavar(a) - */ - bool has_lower(expr const & a) { - lean_assert(is_metavar(a)); - return has_constraint([&](unification_constraint const & c) { return is_lower(c) && convertible_to(c) == a; }); - } - - /** \brief Process constraint of the form ctx |- ?m << b, where \c a is Type */ - bool process_upper(expr const & a, expr const & b, unification_constraint const & c) { - if (is_convertible(c) && is_metavar(a) && is_type(b) && !has_max_constraint(a) && !has_lower(a)) { - // Remark: in principle, there are infinite number of choices. - // We approximate and only consider the most useful ones. - // - // Remark: we only consider \c a if the queue does not have a constraint - // of the form ctx |- max(L1, L2) ≈ a. - // If it does, we don't need to guess. We wait \c a to be assigned - // and just check if the upper bound is satisfied. - // - // Remark: we also give preference to lower bounds - justification new_jst(new destruct_justification(c)); - if (b == Type()) { - expr choices[2] = { Type(), Bool }; - push_active(mk_choice_constraint(get_context(c), a, 2, choices, new_jst)); - return true; - } else if (b == TypeU) { - expr choices[4] = { TypeU, Type(level() + 1), Type(), Bool }; - push_active(mk_choice_constraint(get_context(c), a, 4, choices, new_jst)); - return true; - } else { - level const & lvl = ty_level(b); - lean_assert(!lvl.is_bottom()); - if (is_lift(lvl)) { - // If b is (Type L + k) - // make choices == { Type(L + k), Type(L + k - 1), ..., Type(L), Type, Bool } - buffer choices; - unsigned k = lift_offset(lvl); - level L = lift_of(lvl); - lean_assert(k > 0); - while (k > 0) { - choices.push_back(mk_type(L + k)); - k--; - } - choices.push_back(mk_type(L)); - if (!L.is_bottom()) - choices.push_back(Type()); - choices.push_back(Bool); - push_active(mk_choice_constraint(get_context(c), a, choices.size(), choices.data(), new_jst)); - return true; - } else if (is_uvar(lvl)) { - expr choices[4] = { Type(level() + 1), Type(), b, Bool }; - push_active(mk_choice_constraint(get_context(c), a, 4, choices, new_jst)); - return true; - } else { - lean_assert(is_max(lvl)); - // TODO(Leo) - return false; - } - } - } else { - return false; - } - } - - bool process_assigned_metavar(unification_constraint const & c, expr const & a, bool is_lhs) { - if (is_metavar(a) && is_assigned(a)) { - auto s_j = get_subst_jst(a); - justification new_jst(new substitution_justification(c, s_j.second)); - push_updated_constraint(c, is_lhs, s_j.first, new_jst); - return true; - } else { - return false; - } - } - - /** - \brief Resolve constraints of the form - - ctx |- ?m << Pi(x : A, B) (param is_lhs is true) - and - ctx |- Pi(x : A, B) << ?m (param is_lhs is false) - - where ?m is not assigned and does not have a local context. - - We replace - ctx | ?m << Pi(x : A, B) - with - ctx |- ?m ≈ Pi(x : A, ?m1) - ctx, x : A |- ?m1 << B - */ - void process_metavar_conv_pi(unification_constraint const & c, expr const & m, expr const & pi, bool is_lhs) { - lean_assert(!is_eq(c)); - lean_assert(is_metavar(m) && !has_local_context(m)); - lean_assert(!is_assigned(m)); - lean_assert(is_pi(pi)); - lean_assert(is_lhs || is_eqp(convertible_to(c), m)); - lean_assert(!is_lhs || is_eqp(convertible_from(c), m)); - context ctx = get_context(c); - context new_ctx = extend(ctx, abst_name(pi), abst_domain(pi)); - expr m1 = m_state.m_menv->mk_metavar(new_ctx); - justification new_jst(new destruct_justification(c)); - - // Add ctx, x : A |- ?m1 << B when is_lhs ≈ true, - // and ctx, x : A |- B << ?m1 when is_lhs ≈ false - expr lhs = m1; - expr rhs = abst_body(pi); - if (!is_lhs) - swap(lhs, rhs); - push_new_constraint(false, new_ctx, lhs, rhs, new_jst); - - // Add ctx |- ?m ≈ Pi(x : A, ?m1) - push_new_eq_constraint(ctx, m, update_abstraction(pi, abst_domain(pi), m1), new_jst); - } - - /** - \brief Return true iff \c a has not metavar and no free - variable that is assigned to a term containing metavariables in - ctx. - */ - bool has_no_metavar(context const & ctx, expr const & a) { - if (has_metavar(a)) - return false; - bool found = false; - for_each(a, [&](expr const & e, unsigned offset) { - if (found) return false; // stop the search - if (is_var(e)) { - unsigned vidx = var_idx(e); - if (vidx >= offset) { - vidx -= offset; - auto entry = find(ctx, vidx); - if (entry && entry->get_body() && has_metavar(*entry->get_body())) { - found = true; - return false; - } - } - } - return true; - }); - return !found; - } - - bool process_eq_convertible(context const & ctx, expr const & a, expr const & b, unification_constraint const & c) { - bool eq = is_eq(c); - if (a == b) - return true; - if (has_no_metavar(ctx, a) && has_no_metavar(ctx, b)) { - if (m_type_inferer.is_convertible(a, b, ctx)) { - return true; - } else { - m_conflict = mk_failure_justification(c); - return false; - } - } - - if (process_assigned_metavar(c, a, true) || process_assigned_metavar(c, b, false)) - return true; - - if (m_assume_injectivity && is_app(a) && is_app(b) && num_args(a) == num_args(b) && arg(a, 0) == arg(b, 0) && !is_metavar(arg(a, 0)) - // BIG (temporary) HACK - && !(is_constant(arg(a, 0)) && const_name(arg(a, 0)) == "carrier")) { - // If m_assume_injectivity is true, we apply the following rule - // ctx |- (f a1 a2) ≈ (f b1 b2) - // ==> - // ctx |- a1 ≈ b1 - // ctx |- a2 ≈ b2 - justification new_jst(new destruct_justification(c)); - for (unsigned i = 1; i < num_args(a); i++) - push_new_eq_constraint(ctx, arg(a, i), arg(b, i), new_jst); - return true; - } - - status r; - r = process_metavar(c, a, b, true); - if (r != Continue) { return r == Processed; } - r = process_metavar(c, b, a, false); - if (r != Continue) { return r == Processed; } - - if (is_equality(a) && is_equality(b)) { - expr_pair p1 = get_equality_args(a); - expr_pair p2 = get_equality_args(b); - justification new_jst(new destruct_justification(c)); - if (is_eq(a) && is_eq(b)) - push_new_eq_constraint(ctx, arg(a, 1), arg(b, 1), new_jst); - push_new_eq_constraint(ctx, p1.first, p2.first, new_jst); - push_new_eq_constraint(ctx, p1.second, p2.second, new_jst); - return true; - } - - if (a.kind() == b.kind()) { - switch (a.kind()) { - case expr_kind::Pi: { - justification new_jst(new destruct_justification(c)); - push_new_eq_constraint(ctx, abst_domain(a), abst_domain(b), new_jst); - context new_ctx = extend(ctx, abst_name(a), abst_domain(a)); - push_new_constraint(eq, new_ctx, abst_body(a), abst_body(b), new_jst); - return true; - } - case expr_kind::Lambda: case expr_kind::Sigma: { - justification new_jst(new destruct_justification(c)); - push_new_eq_constraint(ctx, abst_domain(a), abst_domain(b), new_jst); - context new_ctx = extend(ctx, abst_name(a), abst_domain(a)); - push_new_eq_constraint(new_ctx, abst_body(a), abst_body(b), new_jst); - return true; - } - default: - break; - } - } - - if (!eq) { - // Try to assign convertability constraints. - if (is_metavar(a) && !is_assigned(a) && !has_local_context(a)) { - if (is_pi(b)) { - process_metavar_conv_pi(c, a, b, true); - return true; - } else if (!is_type(b) && !is_meta(b)) { - // We can assign a <- b at this point IF b is not (Type lvl) or Metavariable - lean_assert(!has_metavar(b, a)); - return assign(a, b, c, true); - } - } - - if (is_metavar(b) && !is_assigned(b) && !has_local_context(b)) { - if (is_pi(a)) { - process_metavar_conv_pi(c, b, a, false); - return true; - } else if (!is_type(a) && !is_meta(a) && a != Bool) { - // We can assign b <- a at this point IF a is not (Type lvl) or Metavariable or Bool. - lean_assert(!has_metavar(a, b)); - return assign(b, a, c, false); - } - } - } - - if (!is_meta_app(a) && !is_meta_app(b) && normalize_head(a, b, c)) { return true; } - - if (!check_metavar_lift(c, a, b) || !check_metavar_lift(c, b, a)) { return false; } - - if (process_simple_ho_match(ctx, a, b, true, c) || - process_simple_ho_match(ctx, b, a, false, c)) - return true; - - if (!eq && is_bool(a) && is_type(b)) - return true; - - if ((is_proj(a) && instantiate_metavars(true, a, c)) || - (is_proj(b) && instantiate_metavars(false, b, c))) { - return true; - } - - if (a.kind() == b.kind()) { - switch (a.kind()) { - case expr_kind::Constant: case expr_kind::Var: case expr_kind::Value: - if (a == b) { - return true; - } else { - m_conflict = mk_failure_justification(c); - return false; - } - case expr_kind::Type: - if ((!eq && m_env->is_ge(ty_level(b), ty_level(a))) || (eq && a == b)) { - return true; - } else { - m_conflict = mk_failure_justification(c); - return false; - } - case expr_kind::HEq: { - justification new_jst(new destruct_justification(c)); - push_new_eq_constraint(ctx, heq_lhs(a), heq_lhs(b), new_jst); - push_new_eq_constraint(ctx, heq_rhs(a), heq_rhs(b), new_jst); - return true; - } - case expr_kind::Proj: - if (proj_first(a) != proj_first(b)) { - m_conflict = mk_failure_justification(c); - return false; - } else { - justification new_jst(new destruct_justification(c)); - push_new_eq_constraint(ctx, proj_arg(a), proj_arg(b), new_jst); - return true; - } - case expr_kind::Pair: { - justification new_jst(new destruct_justification(c)); - push_new_eq_constraint(ctx, pair_first(a), pair_first(b), new_jst); - push_new_eq_constraint(ctx, pair_second(a), pair_second(b), new_jst); - push_new_eq_constraint(ctx, pair_type(a), pair_type(b), new_jst); - return true; - } - case expr_kind::App: - if (!is_meta_app(a) && !is_meta_app(b)) { - if (num_args(a) == num_args(b)) { - justification new_jst(new destruct_justification(c)); - for (unsigned i = 0; i < num_args(a); i++) - push_new_eq_constraint(ctx, arg(a, i), arg(b, i), new_jst); - return true; - } else { - m_conflict = mk_failure_justification(c); - return false; - } - } - break; - case expr_kind::Let: - lean_unreachable(); // LCOV_EXCL_LINE - return true; - case expr_kind::Pi: case expr_kind::Lambda: - case expr_kind::Sigma: case expr_kind::MetaVar: - break; - } - } - - if (instantiate_metavars(true, a, c) || - instantiate_metavars(false, b, c)) { - return true; - } - - // If 'a' and 'b' have different kinds, and 'a' and 'b' are not metavariables, - // and 'a' and 'b' are not applications where the function contains metavariables, - // then it is not possible to unify 'a' and 'b'. - // We need the last condition because if 'a'/'b' are applications containing metavariables, - // then they can be reduced when the metavariable is assigned - // Here is an example: - // |- (?m Type) << Type - // If ?m is assigned to the identity function (fun x, x), then the constraint can be solved. - if (a.kind() != b.kind() && !is_metavar(a) && !is_metavar(b) && - !(is_app(a) && has_metavar(arg(a, 0))) && !(is_app(b) && has_metavar(arg(b, 0)))) { - // std::cout << "CONFLICT: "; display(std::cout, c); std::cout << "\n"; - m_conflict = mk_failure_justification(c); - return false; - } - - push_delayed(c); - return true; - } - - bool process_max(unification_constraint const & c) { - expr lhs1 = max_lhs1(c); - expr lhs2 = max_lhs2(c); - expr const & rhs = max_rhs(c); - buffer jsts; - bool modified = false; - expr new_lhs1 = lhs1; - expr new_lhs2 = lhs2; - expr new_rhs = rhs; - if (has_assigned_metavar(lhs1)) { - new_lhs1 = instantiate_metavars(lhs1, jsts); - modified = true; - } - if (has_assigned_metavar(lhs2)) { - new_lhs2 = instantiate_metavars(lhs2, jsts); - modified = true; - } - if (has_assigned_metavar(rhs)) { - new_rhs = instantiate_metavars(rhs, jsts); - modified = true; - } - if (modified) { - justification new_jst = mk_subst_justification(c, jsts); - push_active(mk_max_constraint(get_context(c), new_lhs1, new_lhs2, new_rhs, new_jst)); - return true; - } - if (is_bool(lhs2)) { - justification new_jst(new normalize_justification(c)); - push_new_eq_constraint(get_context(c), lhs2, rhs, new_jst); - return true; - } - if (!is_metavar(lhs1) && !is_type(lhs1)) { - new_lhs1 = normalize(get_context(c), lhs1); - modified = (lhs1 != new_lhs1); - } - if (!is_metavar(lhs2) && !is_type(lhs2)) { - new_lhs2 = normalize(get_context(c), lhs2); - modified = (lhs2 != new_lhs2); - } - if (!is_metavar(rhs) && !is_type(rhs)) { - new_rhs = normalize(get_context(c), rhs); - modified = (rhs != new_rhs); - } - if (modified) { - justification new_jst(new normalize_justification(c)); - push_active(mk_max_constraint(get_context(c), new_lhs1, new_lhs2, new_rhs, new_jst)); - return true; - } - if (is_bool(lhs1)) - lhs1 = Type(); - if (is_type(lhs1) && is_type(lhs2)) { - justification new_jst(new normalize_justification(c)); - expr new_lhs = mk_type(max(ty_level(lhs1), ty_level(lhs2))); - push_new_eq_constraint(get_context(c), new_lhs, rhs, new_jst); - return true; - } - if (lhs1 == rhs) { - // ctx |- max(lhs1, lhs2) ≈ rhs - // ==> IF lhs1 = rhs - // ctx |- lhs2 << rhs - justification new_jst(new normalize_justification(c)); - push_active(mk_convertible_constraint(get_context(c), lhs2, rhs, new_jst)); - return true; - } else if (lhs2 == rhs && is_type(lhs2)) { - // ctx |- max(lhs1, lhs2) ≈ rhs IF lhs2 is a Type - // ==> IF lhs1 = rhs - // ctx |- lhs2 << rhs - - // Remark: this rule is not applicable when lhs2 == Bool. - // Recall that max is actually a constraint generated for a Pi(x : A, B) - // where lhs1 and lhs2 represent the types of A and B. - // If lhs2 == Bool, the type of Pi(x : A, B) is Bool, and the type - // of A (lhs1) can be as big as we want - justification new_jst(new normalize_justification(c)); - push_active(mk_convertible_constraint(get_context(c), lhs1, rhs, new_jst)); - return true; - } - - if ((!has_metavar(lhs1) && !is_type(lhs1)) || - (!has_metavar(lhs2) && !is_type(lhs2))) { - m_conflict = mk_failure_justification(c); - return false; - } - // std::cout << "Postponed: "; display(std::cout, c); - push_delayed(c); - return true; - } - - bool process_choice(unification_constraint const & c) { - std::unique_ptr new_cs(new choice_case_split(c, m_state)); - bool r = new_cs->next(*this); - lean_assert(r); - m_case_splits.push_back(std::move(new_cs)); - return r; - } - - void resolve_conflict() { - lean_assert(m_conflict); - - // std::cout << "Resolve conflict, num case_splits: " << m_case_splits.size() << "\n"; - // formatter fmt = mk_simple_formatter(); - // std::cout << m_conflict.pp(fmt, options(), nullptr, true) << "\n"; - - while (!m_case_splits.empty()) { - std::unique_ptr & d = m_case_splits.back(); - // std::cout << "Assumption " << d->m_curr_assumption.pp(fmt, options(), nullptr, true) << "\n"; - if (depends_on(m_conflict, d->m_curr_assumption)) { - d->m_failed_justifications.push_back(m_conflict); - if (d->next(*this)) { - m_conflict = justification(); - return; - } - } - m_case_splits.pop_back(); - } - throw elaborator_exception(m_conflict); - } - - bool next_choice_case(choice_case_split & s) { - unification_constraint & choice = s.m_choice; - unsigned idx = s.m_idx; - if (idx < choice_size(choice)) { - s.m_idx++; - s.m_curr_assumption = mk_assumption(); - m_state = s.m_prev_state; - push_new_eq_constraint(get_context(choice), choice_mvar(choice), choice_ith(choice, idx), s.m_curr_assumption); - return true; - } else { - m_conflict = justification(new unification_failure_by_cases_justification(choice, s.m_failed_justifications.size(), - s.m_failed_justifications.data(), - s.m_prev_state.m_menv)); - return false; - } - } - - bool next_generic_case(generic_case_split & s) { - unsigned idx = s.m_idx; - unsigned sz = s.m_states.size(); - if (idx < sz) { - s.m_idx++; - s.m_curr_assumption = s.m_assumptions[sz - idx - 1]; - m_state = s.m_states[sz - idx - 1]; - return true; - } else { - m_conflict = justification(new unification_failure_by_cases_justification(s.m_constraint, s.m_failed_justifications.size(), - s.m_failed_justifications.data(), - s.m_prev_state.m_menv)); - return false; - } - } - - bool next_plugin_case(plugin_case_split & s) { - try { - s.m_curr_assumption = mk_assumption(); - std::pair> r = s.m_alternatives->next(s.m_curr_assumption); - m_state.m_active_cnstrs = s.m_prev_state.m_active_cnstrs; - m_state.m_delayed_cnstrs = s.m_prev_state.m_delayed_cnstrs; - m_state.m_recently_assigned = s.m_prev_state.m_recently_assigned; - m_state.m_menv = r.first; - for (auto c : r.second) { - push_active(c); - } - return true; - } catch (exception & ex) { - m_conflict = justification(new unification_failure_by_cases_justification(s.m_constraint, s.m_failed_justifications.size(), - s.m_failed_justifications.data(), - s.m_prev_state.m_menv)); - return false; - } - } - - bool process_delayed() { - name_set const & recently_assigned = m_state.m_recently_assigned; - m_state.m_delayed_cnstrs = - filter(m_state.m_delayed_cnstrs, - [&](std::pair const & p) { - bool found = false; - for (auto const & m : p.second) { - if (recently_assigned.contains(m)) { - found = true; - break; - } - } - if (found) { - push_active(p.first); - return false; - } else { - return true; - } - }); - - m_state.m_recently_assigned = name_set(); // reset - lean_assert(m_state.m_recently_assigned.empty()); - if (!empty(m_state.m_active_cnstrs)) - return true; - // second pass trying to apply process_meta_app - m_state.m_delayed_cnstrs = - remove_last(m_state.m_delayed_cnstrs, - [&](std::pair const & p) { - unification_constraint const & c = p.first; - if (is_eq(c) || is_convertible(c)) { - expr const & a = is_eq(c) ? eq_lhs(c) : convertible_from(c); - expr const & b = is_eq(c) ? eq_rhs(c) : convertible_to(c); - if ((process_meta_app(a, b, true, c) || process_meta_app(b, a, false, c))) { - // std::cout << "META_APP: "; display(std::cout, c); std::cout << "\n"; - return true; - } - } - return false; - }); - if (!empty(m_state.m_active_cnstrs)) - return true; - // final pass trying expensive constraints - m_state.m_delayed_cnstrs = - remove_last(m_state.m_delayed_cnstrs, - [&](std::pair const & p) { - unification_constraint const & c = p.first; - if (is_eq(c) || is_convertible(c)) { - // std::cout << "EXPENSIVE: "; display(std::cout, c); std::cout << "\n"; - expr const & a = is_eq(c) ? eq_lhs(c) : convertible_from(c); - expr const & b = is_eq(c) ? eq_rhs(c) : convertible_to(c); - if (process_lower(a, b, c) || - process_upper(a, b, c) || - process_metavar_inst(a, b, true, c) || - process_metavar_inst(b, a, false, c) || - process_metavar_lift_abstraction(a, b, c) || - process_metavar_lift_abstraction(b, a, c) || - process_meta_app(a, b, true, c, false, true) || - process_meta_app(b, a, false, c, false, true) || - process_meta_app(a, b, true, c, true)) { - return true; - } - } - return false; - }); - if (!empty(m_state.m_active_cnstrs)) - return true; - // "approximated mode" - // change convertability into equality constraint - m_state.m_delayed_cnstrs = - remove_last(m_state.m_delayed_cnstrs, - [&](std::pair const & p) { - if (is_convertible(p.first)) { - unification_constraint const & c = p.first; - // std::cout << "CONVERTABILITY: "; display(std::cout, c); std::cout << "\n"; - push_new_eq_constraint(get_context(c), convertible_from(c), convertible_to(c), get_justification(c)); - return true; - } - return false; - }); - return !empty(m_state.m_active_cnstrs); - } - -public: - imp(ro_environment const & env, metavar_env const & menv, unsigned num_cnstrs, unification_constraint const * cnstrs, - options const & opts, std::shared_ptr const & p): - m_env(env), - m_type_inferer(env), - m_normalizer(env), - m_state(menv, num_cnstrs, cnstrs), - m_plugin(p) { - set_options(opts); - m_next_id = 0; - m_first = true; - m_U = m_env->get_uvar("U"); - m_num_steps = 0; - // display(std::cout); - } - - metavar_env next() { - m_num_steps = 0; - check_system(); - if (m_conflict) - throw elaborator_exception(m_conflict); - if (!m_case_splits.empty()) { - buffer assumptions; - for (std::unique_ptr const & cs : m_case_splits) - assumptions.push_back(cs->m_curr_assumption); - m_conflict = justification(new next_solution_justification(assumptions.size(), assumptions.data())); - resolve_conflict(); - } else if (m_first) { - m_first = false; - } else { - // this is not the first run, and there are no case-splits - m_conflict = justification(new next_solution_justification(0, nullptr)); - throw elaborator_exception(m_conflict); - } - while (true) { - check_system(); - cnstr_list & active_cnstrs = m_state.m_active_cnstrs; - if (!empty(active_cnstrs)) { - unification_constraint c = head(active_cnstrs); - m_state.m_active_cnstrs = tail(active_cnstrs); - // std::cout << "Processing, depth: " << m_case_splits.size() << " "; display(std::cout, c); - if (!process(c)) { - resolve_conflict(); - } - } else if (!empty(m_state.m_delayed_cnstrs)) { - // std::cout << "PROCESSING DELAYED\n"; display(std::cout); std::cout << "\n\n"; - if (!process_delayed()) { - // std::cout << "FAILED to solve\n"; - // display(std::cout); - return m_state.m_menv; - } - } else { - return m_state.m_menv; - } - } - } - - void display(std::ostream & out, unification_constraint const & c) const { - formatter fmt = mk_simple_formatter(); - out << c.pp(fmt, options(), nullptr, false) << "\n"; - } - - void display(std::ostream & out) const { - m_state.m_menv->for_each_subst([&](name const & m, expr const & e) { - out << m << " <- " << e << "\n"; - }); - for (auto c : m_state.m_active_cnstrs) - display(out, c); - out << "Delayed constraints:\n"; - for (auto c : m_state.m_delayed_cnstrs) - display(out, c.first); - } -}; - -elaborator::elaborator(ro_environment const & env, - metavar_env const & menv, - unsigned num_cnstrs, - unification_constraint const * cnstrs, - options const & opts, - std::shared_ptr const & p): - m_ptr(new imp(env, menv, num_cnstrs, cnstrs, opts, p)) { -} - -elaborator::elaborator(ro_environment const & env, - metavar_env const & menv, - context const & ctx, expr const & lhs, expr const & rhs): - elaborator(env, menv, { mk_eq_constraint(ctx, lhs, rhs, justification()) }) { -} - -elaborator::~elaborator() { -} - -metavar_env elaborator::next() { - return m_ptr->next(); -} -} diff --git a/src/library/elaborator/elaborator.h b/src/library/elaborator/elaborator.h deleted file mode 100644 index 5e9297509..000000000 --- a/src/library/elaborator/elaborator.h +++ /dev/null @@ -1,61 +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 "util/sexpr/options.h" -#include "kernel/expr.h" -#include "kernel/environment.h" -#include "kernel/metavar.h" -#include "kernel/unification_constraint.h" -#include "library/elaborator/elaborator_plugin.h" -#include "library/elaborator/elaborator_exception.h" - -namespace lean { -/** - \brief Elaborator fills "holes" in Lean using unification based - method. This is essentially a generalizationof the ML type inference - algorithm. - - Each hole is represented using a metavariable. This object is - responsible for solving the easy "holes" and invoking external - plugins for filling the other ones. It is also responsible for - managing the search space (i.e., managing the backtracking search). - - The elaborator can be customized using plugins that are invoked - whenever the elaborator does not know how to solve a unification - constraint. - - The result is a sequence of substitutions. Each substitution - represents a different way of filling the holes. -*/ -class elaborator { -public: - class imp; - std::shared_ptr m_ptr; -public: - elaborator(ro_environment const & env, - metavar_env const & menv, - unsigned num_cnstrs, - unification_constraint const * cnstrs, - options const & opts = options(), - std::shared_ptr const & p = std::shared_ptr()); - - elaborator(ro_environment const & env, - metavar_env const & menv, - std::initializer_list const & cnstrs, - options const & opts = options(), - std::shared_ptr const & p = std::shared_ptr()): - elaborator(env, menv, cnstrs.size(), cnstrs.begin(), opts, p) {} - - elaborator(ro_environment const & env, - metavar_env const & menv, - context const & ctx, expr const & lhs, expr const & rhs); - - ~elaborator(); - - metavar_env next(); -}; -} diff --git a/src/library/elaborator/elaborator_exception.h b/src/library/elaborator/elaborator_exception.h deleted file mode 100644 index 7f847eee5..000000000 --- a/src/library/elaborator/elaborator_exception.h +++ /dev/null @@ -1,26 +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 "util/exception.h" -#include "kernel/justification.h" - -namespace lean { -/** - \brief Elaborator and related components store the reason for - failure in justification objects. -*/ -class elaborator_exception : public exception { - justification m_justification; -public: - elaborator_exception(justification const & j):m_justification(j) {} - virtual ~elaborator_exception() {} - virtual char const * what() const noexcept { return "elaborator exception"; } - justification const & get_justification() const { return m_justification; } - virtual exception * clone() const { return new elaborator_exception(m_justification); } - virtual void rethrow() const { throw *this; } -}; -} diff --git a/src/library/elaborator/elaborator_justification.cpp b/src/library/elaborator/elaborator_justification.cpp deleted file mode 100644 index e1e701045..000000000 --- a/src/library/elaborator/elaborator_justification.cpp +++ /dev/null @@ -1,159 +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 "library/elaborator/elaborator_justification.h" - -namespace lean { -// ------------------------- -// Propagation justification -// ------------------------- -propagation_justification::propagation_justification(unification_constraint const & c): - m_constraint(c) { -} -propagation_justification::~propagation_justification() { -} -void propagation_justification::get_children(buffer & r) const { - push_back(r, m_constraint.get_justification()); -} -optional propagation_justification::get_main_expr() const { - return none_expr(); -} -format propagation_justification::pp_header(formatter const & fmt, options const & opts, optional const & menv) const { - format r; - r += format(get_prop_name()); - r += compose(line(), get_constraint().pp(fmt, opts, nullptr, false, menv)); - return r; -} - -// ------------------------- -// Unification failure (by cases) -// ------------------------- -unification_failure_by_cases_justification::unification_failure_by_cases_justification( - unification_constraint const & c, unsigned num, justification const * cs, metavar_env const & menv): - unification_failure_justification(c, menv), - m_cases(cs, cs + num) { -} -unification_failure_by_cases_justification::~unification_failure_by_cases_justification() { -} -void unification_failure_by_cases_justification::get_children(buffer & r) const { - push_back(r, get_constraint().get_justification()); - append(r, m_cases); -} - -// ------------------------- -// Substitution justification -// ------------------------- -substitution_justification::substitution_justification(unification_constraint const & c, justification const & t): - propagation_justification(c), - m_assignment_justification(t) { -} -substitution_justification::~substitution_justification() { -} -void substitution_justification::get_children(buffer & r) const { - propagation_justification::get_children(r); - push_back(r, m_assignment_justification); -} - -multi_substitution_justification::multi_substitution_justification(unification_constraint const & c, unsigned num, justification const * ts): - propagation_justification(c), - m_assignment_justifications(ts, ts + num) { -} -multi_substitution_justification::~multi_substitution_justification() { -} -void multi_substitution_justification::get_children(buffer & r) const { - propagation_justification::get_children(r); - append(r, m_assignment_justifications); -} - -// ------------------------- -// typeof metavar justification -// ------------------------- -typeof_mvar_justification::typeof_mvar_justification(context const & ctx, expr const & m, expr const & tm, expr const & t, justification const & tr): - m_context(ctx), - m_mvar(m), - m_typeof_mvar(tm), - m_type(t), - m_justification(tr) { -} -typeof_mvar_justification::~typeof_mvar_justification() { -} -format typeof_mvar_justification::pp_header(formatter const & fmt, options const & opts, optional const & menv) const { - format r; - unsigned indent = get_pp_indent(opts); - r += format("Propagate type,"); - { - format body; - body += fmt(m_context, m_mvar, false, opts); - body += space(); - body += colon(); - body += nest(indent, compose(line(), fmt(m_context, instantiate_metavars(menv, m_typeof_mvar), false, opts))); - r += nest(indent, compose(line(), body)); - } - return group(r); -} -void typeof_mvar_justification::get_children(buffer & r) const { - push_back(r, m_justification); -} - -// ------------------------- -// Next solution justification -// ------------------------- -next_solution_justification::next_solution_justification(unsigned num, justification const * as): - m_assumptions(as, as + num) { -} -next_solution_justification::~next_solution_justification() { -} -format next_solution_justification::pp_header(formatter const &, options const &, optional const &) const { - return format("next solution"); -} -void next_solution_justification::get_children(buffer & r) const { - append(r, m_assumptions); -} -optional next_solution_justification::get_main_expr() const { - return none_expr(); -} - -bool is_derived_constraint(unification_constraint const & uc) { - auto j = uc.get_justification(); - return j && dynamic_cast(j.raw()); -} - -unification_constraint get_non_derived_constraint(unification_constraint const & uc) { - auto j = uc.get_justification(); - auto jcell = j.raw(); - if (auto pcell = dynamic_cast(jcell)) { - return get_non_derived_constraint(pcell->get_constraint()); - } else { - return uc.updt_justification(remove_detail(j)); - } -} - -justification remove_detail(justification const & j) { - auto jcell = j.raw(); - if (auto fc_cell = dynamic_cast(jcell)) { - auto uc = fc_cell->get_constraint(); - if (is_derived_constraint(uc)) { - // we usually don't care about internal case-splits - unification_constraint const & new_uc = get_non_derived_constraint(uc); - return justification(new unification_failure_justification(new_uc, fc_cell->get_menv())); - } else { - buffer new_js; - for (auto const & j : fc_cell->get_cases()) - new_js.push_back(remove_detail(j)); - return justification(new unification_failure_by_cases_justification(uc, new_js.size(), new_js.data(), fc_cell->get_menv())); - } - } else if (auto f_cell = dynamic_cast(jcell)) { - unification_constraint const & new_uc = get_non_derived_constraint(f_cell->get_constraint()); - return justification(new unification_failure_justification(new_uc, f_cell->get_menv())); - } else if (auto p_cell = dynamic_cast(jcell)) { - return remove_detail(p_cell->get_constraint().get_justification()); - } else if (auto t_cell = dynamic_cast(jcell)) { - return remove_detail(t_cell->get_justification()); - } else { - return j; - } -} -} diff --git a/src/library/elaborator/elaborator_justification.h b/src/library/elaborator/elaborator_justification.h deleted file mode 100644 index 31609bbe0..000000000 --- a/src/library/elaborator/elaborator_justification.h +++ /dev/null @@ -1,190 +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 "kernel/justification.h" -#include "kernel/unification_constraint.h" -#include "kernel/metavar.h" - -namespace lean { -/** - \brief Base class for justifying propagations and failures -*/ -class propagation_justification : public justification_cell { - unification_constraint m_constraint; -protected: - /** \brief Auxiliary method used by pp_header to label a propagation step, subclasses must redefine it. */ - virtual char const * get_prop_name() const = 0; -public: - propagation_justification(unification_constraint const & c); - virtual ~propagation_justification(); - virtual void get_children(buffer & r) const; - virtual optional get_main_expr() const; - virtual format pp_header(formatter const &, options const &, optional const &) const; - unification_constraint const & get_constraint() const { return m_constraint; } -}; - -/** - \brief Justification object used to mark that a particular unification constraint could not be solved. -*/ -class unification_failure_justification : public propagation_justification { -protected: - // We store the menv at the time of failure. We use it to produce less cryptic error messages. - metavar_env m_menv; - virtual char const * get_prop_name() const { return "Failed to solve"; } -public: - unification_failure_justification(unification_constraint const & c, metavar_env const & menv): - propagation_justification(c), m_menv(menv) {} - virtual format pp_header(formatter const & fmt, options const & opts, optional const &) const { - return propagation_justification::pp_header(fmt, opts, optional(m_menv)); - } - virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children, - optional const &) const { - return propagation_justification::pp(fmt, opts, p, display_children, optional(m_menv)); - } - metavar_env get_menv() const { return m_menv; } -}; - -/** - \brief Justification object created for justifying that a constraint that - generated a case-split does not have a solution. Each case-split - corresponds to a different way of solving the constraint. -*/ -class unification_failure_by_cases_justification : public unification_failure_justification { - std::vector m_cases; // why each case failed -public: - unification_failure_by_cases_justification(unification_constraint const & c, unsigned num, justification const * cs, metavar_env const & menv); - virtual ~unification_failure_by_cases_justification(); - virtual void get_children(buffer & r) const; - std::vector const & get_cases() const { return m_cases; } -}; - -/** - \brief Justification object used to justify a metavar assignment. -*/ -class assignment_justification : public propagation_justification { -protected: - virtual char const * get_prop_name() const { return "Assignment"; } -public: - assignment_justification(unification_constraint const & c):propagation_justification(c) {} -}; - -/** - \brief Justification object used to justify simple structural steps when processing unification - constraints. For example, given the constraint - - ctx |- (f a) == (f b) - - where \c f is a variable, we must have - - ctx |- a == b - - The justification for the latter is a destruct justification based on the former. -*/ -class destruct_justification : public propagation_justification { -protected: - virtual char const * get_prop_name() const { return "Destruct/Decompose"; } -public: - destruct_justification(unification_constraint const & c):propagation_justification(c) {} -}; - -/** - \brief Justification object used to justify a normalization step such as. - - ctx |- (fun x : T, x) a == b - ==> - ctx |- a == b -*/ -class normalize_justification : public propagation_justification { -protected: - virtual char const * get_prop_name() const { return "Normalize"; } -public: - normalize_justification(unification_constraint const & c):propagation_justification(c) {} -}; - -/** - \brief Justification object used to justify an imitation step. - An imitation step is used when solving constraints such as: - - ctx |- ?m[lift:s:n, ...] == Pi (x : A), B x - - In this case, ?m must be a Pi. We make progress, by adding the constraint - ctx |- ?m == Pi (x : ?M1), (?M2 x) - - where ?M1 and ?M2 are fresh metavariables. -*/ -class imitation_justification : public propagation_justification { -protected: - virtual char const * get_prop_name() const { return "Imitation"; } -public: - imitation_justification(unification_constraint const & c):propagation_justification(c) {} -}; - -/** - \brief Justification object used to justify a new constraint obtained by substitution. -*/ -class substitution_justification : public propagation_justification { - justification m_assignment_justification; -protected: - virtual char const * get_prop_name() const { return "Substitution"; } -public: - substitution_justification(unification_constraint const & c, justification const & t); - virtual ~substitution_justification(); - virtual void get_children(buffer & r) const; -}; - -/** - \brief Justification object used to justify a new constraint obtained by multiple substitution. -*/ -class multi_substitution_justification : public propagation_justification { - std::vector m_assignment_justifications; -protected: - virtual char const * get_prop_name() const { return "Substitution"; } -public: - multi_substitution_justification(unification_constraint const & c, unsigned num, justification const * ts); - virtual ~multi_substitution_justification(); - virtual void get_children(buffer & r) const; -}; - -/** - \brief Justification object used to justify a typeof(m) == t constraint generated when - we assign a metavariable \c m. -*/ -class typeof_mvar_justification : public justification_cell { - context m_context; - expr m_mvar; - expr m_typeof_mvar; - expr m_type; - justification m_justification; -public: - typeof_mvar_justification(context const & ctx, expr const & m, expr const & mt, expr const & t, justification const & tr); - virtual ~typeof_mvar_justification(); - virtual format pp_header(formatter const &, options const &, optional const & menv) const; - virtual void get_children(buffer & r) const; - justification const & get_justification() const { return m_justification; } -}; - -/** - \brief Justification object used to justify that we are moving to the next solution. -*/ -class next_solution_justification : public justification_cell { - std::vector m_assumptions; // Set of assumptions used to derive last solution -public: - next_solution_justification(unsigned num, justification const * as); - virtual ~next_solution_justification(); - virtual format pp_header(formatter const &, options const &, optional const & menv) const; - virtual void get_children(buffer & r) const; - virtual optional get_main_expr() const; -}; - -/** - \brief Create a new justification object where we eliminate - intermediate steps and assignment justifications. This function - produces a new justification object that is better for - pretty printing. -*/ -justification remove_detail(justification const & j); -}; diff --git a/src/library/elaborator/elaborator_plugin.h b/src/library/elaborator/elaborator_plugin.h deleted file mode 100644 index 427971e3b..000000000 --- a/src/library/elaborator/elaborator_plugin.h +++ /dev/null @@ -1,40 +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 "kernel/environment.h" -#include "kernel/context.h" -#include "kernel/unification_constraint.h" - -namespace lean { -class elaborator_plugin { -public: - virtual ~elaborator_plugin() {} - - /** \brief The plugin produces a "result" object that can generates the sequence of possible solutions. */ - class result { - public: - virtual ~result() {} - /** - \brief Return the next possible solution. An elaborator_exception is throw in case of failure. - - Each result is represented by a pair: the new metavariable - environment and a new list of constraints to be solved. - */ - virtual std::pair> next(justification const & assumption) = 0; - /** \brief Interrupt the computation for the next solution. */ - }; - - /** - \brief Ask plugin to solve the constraint \c cnstr in the given - environment and metavar environment. - */ - virtual std::unique_ptr operator()(environment const & env, metavar_env const & menv, unification_constraint const & cnstr) = 0; -}; -} diff --git a/src/tests/library/elaborator/CMakeLists.txt b/src/tests/library/elaborator/CMakeLists.txt deleted file mode 100644 index d1ec53c04..000000000 --- a/src/tests/library/elaborator/CMakeLists.txt +++ /dev/null @@ -1,4 +0,0 @@ -add_executable(elaborator_tst elaborator.cpp) -target_link_libraries(elaborator_tst ${EXTRA_LIBS}) -add_test(elaborator_tst ${CMAKE_CURRENT_BINARY_DIR}/elaborator_tst) -set_tests_properties(elaborator_tst PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_BINARY_DIR}/shell") diff --git a/src/tests/library/elaborator/elaborator.cpp b/src/tests/library/elaborator/elaborator.cpp deleted file mode 100644 index 71e7d74d8..000000000 --- a/src/tests/library/elaborator/elaborator.cpp +++ /dev/null @@ -1,900 +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/type_checker.h" -#include "kernel/abstract.h" -#include "kernel/kernel_exception.h" -#include "kernel/normalizer.h" -#include "kernel/instantiate.h" -#include "kernel/kernel.h" -#include "library/io_state_stream.h" -#include "library/placeholder.h" -#include "library/printer.h" -#include "library/arith/arith.h" -#include "library/elaborator/elaborator.h" -#include "frontends/lean/frontend.h" -#include "frontends/lua/register_modules.h" -using namespace lean; - -static void tst1() { - environment env; - init_test_frontend(env); - metavar_env menv; - buffer ucs; - type_checker checker(env); - expr list = Const("list"); - expr nil = Const("nil"); - expr cons = Const("cons"); - expr A = Const("A"); - env->add_var("list", Type() >> Type()); - env->add_var("nil", Pi({A, Type()}, list(A))); - env->add_var("cons", Pi({A, Type()}, A >> (list(A) >> list(A)))); - env->add_var("a", Int); - env->add_var("b", Int); - env->add_var("n", Nat); - env->add_var("m", Nat); - expr a = Const("a"); - expr b = Const("b"); - expr n = Const("n"); - expr m = Const("m"); - expr m1 = menv->mk_metavar(); - expr m2 = menv->mk_metavar(); - expr m3 = menv->mk_metavar(); - expr A1 = menv->mk_metavar(); - expr A2 = menv->mk_metavar(); - expr A3 = menv->mk_metavar(); - expr A4 = menv->mk_metavar(); - expr F = cons(A1, m1(a), cons(A2, m2(n), cons(A3, m3(b), nil(A4)))); - std::cout << F << "\n"; - std::cout << checker.check(F, context(), menv, ucs) << "\n"; - expr int_id = Fun({a, Int}, a); - expr nat_id = Fun({a, Nat}, a); - ucs.push_back(mk_choice_constraint(context(), m1, { int_id, mk_int_to_real_fn() }, justification())); - ucs.push_back(mk_choice_constraint(context(), m2, { nat_id, mk_nat_to_int_fn(), mk_nat_to_real_fn() }, justification())); - ucs.push_back(mk_choice_constraint(context(), m3, { int_id, mk_int_to_real_fn() }, justification())); - elaborator elb(env, menv, ucs.size(), ucs.data()); - elb.next(); -} - -static void tst2() { - /* - Solve elaboration problem for - - g : Pi (A : Type), A -> A - a : Int - Axiom H : g _ a <= 0 - - The following elaboration problem is created - - ?m1 (g ?m2 (?m3 a)) (?m4 a) - - ?m1 in { Nat::Le, Int::Le, Real::Le } - ?m3 in { Id, int2real } - ?m4 in { Id, nat2int, nat2real } - */ - environment env; - init_test_frontend(env); - metavar_env menv; - buffer ucs; - type_checker checker(env); - expr A = Const("A"); - expr g = Const("g"); - env->add_var("g", Pi({A, Type()}, A >> A)); - expr a = Const("a"); - env->add_var("a", Int); - expr m1 = menv->mk_metavar(); - expr m2 = menv->mk_metavar(); - expr m3 = menv->mk_metavar(); - expr m4 = menv->mk_metavar(); - expr int_id = Fun({a, Int}, a); - expr nat_id = Fun({a, Nat}, a); - expr F = m1(g(m2, m3(a)), m4(nVal(0))); - std::cout << F << "\n"; - std::cout << checker.check(F, context(), menv, ucs) << "\n"; - ucs.push_back(mk_choice_constraint(context(), m1, { mk_Nat_le_fn(), mk_Int_le_fn(), mk_Real_le_fn() }, justification())); - ucs.push_back(mk_choice_constraint(context(), m3, { int_id, mk_int_to_real_fn() }, justification())); - ucs.push_back(mk_choice_constraint(context(), m4, { nat_id, mk_nat_to_int_fn(), mk_nat_to_real_fn() }, justification())); - elaborator elb(env, menv, ucs.size(), ucs.data()); - elb.next(); -} - -static void tst3() { - /* - Solve elaboration problem for - - a : Int - (fun x, (f x) > 10) a - - The following elaboration problem is created - - (fun x : ?m1, ?m2 (f ?m3 x) (?m4 10)) (?m5 a) - - ?m2 in { Nat::Le, Int::Le, Real::Le } - ?m4 in { Id, nat2int, nat2real } - ?m5 in { Id, int2real } - */ - environment env; - init_test_frontend(env); - metavar_env menv; - buffer ucs; - type_checker checker(env); - expr A = Const("A"); - expr f = Const("f"); - env->add_var("f", Pi({A, Type()}, A >> A)); - expr a = Const("a"); - env->add_var("a", Int); - expr m1 = menv->mk_metavar(); - expr m2 = menv->mk_metavar(); - expr m3 = menv->mk_metavar(); - expr m4 = menv->mk_metavar(); - expr m5 = menv->mk_metavar(); - expr int_id = Fun({a, Int}, a); - expr nat_id = Fun({a, Nat}, a); - expr x = Const("x"); - expr F = Fun({x, m1}, m2(f(m3, x), m4(nVal(10))))(m5(a)); - std::cout << F << "\n"; - std::cout << checker.check(F, context(), menv, ucs) << "\n"; - ucs.push_back(mk_choice_constraint(context(), m2, { mk_Nat_le_fn(), mk_Int_le_fn(), mk_Real_le_fn() }, justification())); - ucs.push_back(mk_choice_constraint(context(), m4, { nat_id, mk_nat_to_int_fn(), mk_nat_to_real_fn() }, justification())); - ucs.push_back(mk_choice_constraint(context(), m5, { int_id, mk_int_to_real_fn() }, justification())); - elaborator elb(env, menv, ucs.size(), ucs.data()); - elb.next(); -} - -static void tst4() { - /* - Variable f {A : Type} (a : A) : A - Variable a : Int - Variable b : Real - (fun x y, (f x) > (f y)) a b - - The following elaboration problem is created - - (fun (x : ?m1) (y : ?m2), ?m3 (f ?m4 x) (f ?m5 y)) (?m6 a) b - - ?m3 in { Nat::Le, Int::Le, Real::Le } - ?m6 in { Id, int2real } - */ - environment env; - init_test_frontend(env); - metavar_env menv; - buffer ucs; - type_checker checker(env); - expr A = Const("A"); - expr f = Const("f"); - env->add_var("f", Pi({A, Type()}, A >> A)); - expr a = Const("a"); - expr b = Const("b"); - env->add_var("a", Int); - env->add_var("b", Real); - expr m1 = menv->mk_metavar(); - expr m2 = menv->mk_metavar(); - expr m3 = menv->mk_metavar(); - expr m4 = menv->mk_metavar(); - expr m5 = menv->mk_metavar(); - expr m6 = menv->mk_metavar(); - expr x = Const("x"); - expr y = Const("y"); - expr int_id = Fun({a, Int}, a); - expr F = Fun({{x, m1}, {y, m2}}, m3(f(m4, x), f(m5, y)))(m6(a), b); - std::cout << F << "\n"; - std::cout << checker.check(F, context(), menv, ucs) << "\n"; - ucs.push_back(mk_choice_constraint(context(), m3, { mk_Nat_le_fn(), mk_Int_le_fn(), mk_Real_le_fn() }, justification())); - ucs.push_back(mk_choice_constraint(context(), m6, { int_id, mk_int_to_real_fn() }, justification())); - elaborator elb(env, menv, ucs.size(), ucs.data()); - elb.next(); -} - -static void tst5() { - /* - - Variable f {A : Type} (a b : A) : Bool - Variable a : Int - Variable b : Real - (fun x y, f x y) a b - - The following elaboration problem is created - - (fun (x : ?m1) (y : ?m2), (f ?m3 x y)) (?m4 a) b - - ?m4 in { Id, int2real } - */ - environment env; - init_test_frontend(env); - metavar_env menv; - buffer ucs; - type_checker checker(env); - expr A = Const("A"); - expr f = Const("f"); - env->add_var("f", Pi({A, Type()}, A >> (A >> A))); - expr a = Const("a"); - expr b = Const("b"); - env->add_var("a", Int); - env->add_var("b", Real); - expr m1 = menv->mk_metavar(); - expr m2 = menv->mk_metavar(); - expr m3 = menv->mk_metavar(); - expr m4 = menv->mk_metavar(); - expr x = Const("x"); - expr y = Const("y"); - expr int_id = Fun({a, Int}, a); - expr F = Fun({{x, m1}, {y, m2}}, f(m3, x, y))(m4(a), b); - std::cout << F << "\n"; - std::cout << checker.check(F, context(), menv, ucs) << "\n"; - ucs.push_back(mk_choice_constraint(context(), m4, { int_id, mk_int_to_real_fn() }, justification())); - elaborator elb(env, menv, ucs.size(), ucs.data()); - elb.next(); -} - -static void tst6() { - /* - Subst : Π (A : Type U) (a b : A) (P : A → Bool), (P a) → (a = b) → (P b) - f : Int -> Int -> Int - a : Int - b : Int - H1 : (f a (f a b)) == a - H2 : a = b - Theorem T : (f a (f b b)) == a := Subst _ _ _ _ H1 H2 - */ - environment env; - init_test_frontend(env); - metavar_env menv; - buffer ucs; - type_checker checker(env); - expr f = Const("f"); - expr a = Const("a"); - expr b = Const("b"); - expr H1 = Const("H1"); - expr H2 = Const("H2"); - expr m1 = menv->mk_metavar(); - expr m2 = menv->mk_metavar(); - expr m3 = menv->mk_metavar(); - expr m4 = menv->mk_metavar(); - env->add_var("f", Int >> (Int >> Int)); - env->add_var("a", Int); - env->add_var("b", Int); - env->add_axiom("H1", mk_eq(Int, f(a, f(a, b)), a)); - env->add_axiom("H2", mk_eq(Int, a, b)); - expr V = mk_subst_th(m1, m2, m3, m4, H1, H2); - expr expected = mk_eq(Int, f(a, f(b, b)), a); - expr given = checker.check(V, context(), menv, ucs); - ucs.push_back(mk_eq_constraint(context(), expected, given, justification())); - elaborator elb(env, menv, ucs.size(), ucs.data()); - metavar_env s = elb.next(); - std::cout << s->instantiate_metavars(V) << "\n"; -} - -#define _ mk_placeholder() - -static expr elaborate(expr const & e, environment const & env) { - metavar_env menv; - buffer ucs; - type_checker checker(env); - expr e2 = replace_placeholders_with_metavars(e, menv); - checker.check(e2, context(), menv, ucs); - elaborator elb(env, menv, ucs.size(), ucs.data()); - metavar_env s = elb.next(); - return s->instantiate_metavars(e2); -} - -// Check elaborator success -static void success(expr const & e, expr const & expected, environment const & env) { - std::cout << "\n" << e << "\n\n"; - expr r = elaborate(e, env); - std::cout << "\n" << e << "\n------>\n" << r << "\n"; - lean_assert_eq(r, expected); -} - -// Check elaborator failure -static void fails(expr const & e, environment const & env) { - try { - expr new_e = elaborate(e, env); - std::cout << "new_e: " << new_e << std::endl; - lean_unreachable(); - } catch (exception &) { - } -} - -// Check elaborator partial success (i.e., result still contain some metavariables */ -static void unsolved(expr const & e, environment const & env) { - expr r = elaborate(e, env); - std::cout << "\n" << e << "\n------>\n" << r << "\n"; - lean_assert(has_metavar(r)); -} - -static void tst7() { - std::cout << "\nTST 7\n"; - environment env; - init_test_frontend(env); - expr A = Const("A"); - expr B = Const("B"); - expr F = Const("F"); - expr g = Const("g"); - expr a = Const("a"); - expr Nat = Const("N"); - expr Real = Const("R"); - env->add_var("N", Type()); - env->add_var("R", Type()); - env->add_var("F", Pi({{A, Type()}, {B, Type()}, {g, A >> B}}, A)); - env->add_var("f", Nat >> Real); - expr f = Const("f"); - success(F(_, _, f), F(Nat, Real, f), env); - // fails(F(_, Bool, f), env); - success(F(_, _, Fun({a, Nat}, a)), F(Nat, Nat, Fun({a, Nat}, a)), env); -} - -static void tst8() { - std::cout << "\nTST 8\n"; - environment env; - init_test_frontend(env); - expr a = Const("a"); - expr b = Const("b"); - expr c = Const("c"); - expr H1 = Const("H1"); - expr H2 = Const("H2"); - env->add_var("a", Bool); - env->add_var("b", Bool); - env->add_var("c", Bool); - env->add_axiom("H1", mk_eq(Bool, a, b)); - env->add_axiom("H2", mk_eq(Bool, b, c)); - success(mk_trans_th(_, _, _, _, H1, H2), mk_trans_th(Bool, a, b, c, H1, H2), env); - success(mk_trans_th(_, _, _, _, mk_symm_th(_, _, _, H2), mk_symm_th(_, _, _, H1)), - mk_trans_th(Bool, c, b, a, mk_symm_th(Bool, b, c, H2), mk_symm_th(Bool, a, b, H1)), env); - success(mk_symm_th(_, _, _, mk_trans_th(_, _ , _ , _ , mk_symm_th(_, _, _, H2), mk_symm_th(_, _, _, H1))), - mk_symm_th(Bool, c, a, mk_trans_th(Bool, c, b, a, mk_symm_th(Bool, b, c, H2), mk_symm_th(Bool, a, b, H1))), env); - env->add_axiom("H3", a); - expr H3 = Const("H3"); - success(mk_eqt_intro_th(_, mk_eqmp_th(_, _, mk_symm_th(_, _, _, mk_trans_th(_, _, _, _, mk_symm_th(_, _, _, H2), mk_symm_th(_, _, _, H1))), H3)), - mk_eqt_intro_th(c, mk_eqmp_th(a, c, mk_symm_th(Bool, c, a, mk_trans_th(Bool, c, b, a, mk_symm_th(Bool, b, c, H2), mk_symm_th(Bool, a, b, H1))), H3)), - env); -} - -static void tst9() { - std::cout << "\nTST 9\n"; - environment env; - init_test_frontend(env); - expr Nat = Const("N"); - env->add_var("N", Type()); - env->add_var("vec", Nat >> Type()); - expr n = Const("n"); - expr vec = Const("vec"); - std::cout << "step1\n"; - expr z = Const("z"); - env->add_var("z", Nat); - env->add_var("f", Pi({n, Nat}, vec(z) >> Nat)); - std::cout << "step2\n"; - expr f = Const("f"); - expr a = Const("a"); - expr b = Const("b"); - expr H = Const("H"); - expr fact = Const("fact"); - env->add_var("a", Nat); - env->add_var("b", Nat); - env->add_definition("fact", Bool, mk_eq(Nat, a, b)); - env->add_axiom("H", fact); - success(mk_congr2_th(_, _, _, _, f, H), - mk_congr2_th(Nat, vec(z) >> Nat, a, b, f, H), env); - env->add_var("g", Pi({n, Nat}, vec(z) >> Nat)); - expr g = Const("g"); - env->add_axiom("H2", mk_eq(Pi({n, Nat}, vec(z) >> Nat), f, g)); - expr H2 = Const("H2"); - success(mk_congr_th(_, _, _, _, _, _, H2, H), - mk_congr_th(Nat, vec(z) >> Nat, f, g, a, b, H2, H), env); - success(mk_congr_th(_, _, _, _, _, _, mk_refl_th(_, f), H), - mk_congr_th(Nat, vec(z) >> Nat, f, f, a, b, mk_refl_th(Pi({n, Nat}, vec(z) >> Nat), f), H), env); - success(mk_refl_th(_, a), mk_refl_th(Nat, a), env); -} - -static void tst10() { - std::cout << "\nTST 10\n"; - environment env; - init_test_frontend(env); - expr Nat = Const("N"); - env->add_var("N", Type()); - expr R = Const("R"); - env->add_var("R", Type()); - env->add_var("a", Nat); - expr a = Const("a"); - expr f = Const("f"); - env->add_var("f", Nat >> ((R >> Nat) >> R)); - expr x = Const("x"); - expr y = Const("y"); - expr z = Const("z"); - success(Fun({{x, _}, {y, _}}, f(x, y)), - Fun({{x, Nat}, {y, R >> Nat}}, f(x, y)), env); - success(Fun({{x, _}, {y, _}, {z, _}}, mk_eq(_, f(x, y), f(x, z))), - Fun({{x, Nat}, {y, R >> Nat}, {z, R >> Nat}}, mk_eq(R, f(x, y), f(x, z))), env); - expr A = Const("A"); - success(Fun({{A, Type()}, {x, _}, {y, _}, {z, _}}, mk_eq(_, f(x, y), f(x, z))), - Fun({{A, Type()}, {x, Nat}, {y, R >> Nat}, {z, R >> Nat}}, mk_eq(R, f(x, y), f(x, z))), env); -} - -static void tst11() { - std::cout << "\nTST 11\n"; - environment env; - init_test_frontend(env); - expr A = Const("A"); - expr B = Const("B"); - expr a = Const("a"); - expr b = Const("b"); - expr f = Const("f"); - expr g = Const("g"); - expr Nat = Const("N"); - env->add_var("N", Type()); - env->add_var("f", Pi({{A, Type()}, {a, A}, {b, A}}, A)); - env->add_var("g", Nat >> Nat); - success(Fun({{a, _}, {b, _}}, g(f(_, a, b))), - Fun({{a, Nat}, {b, Nat}}, g(f(Nat, a, b))), env); -} - -static void tst12() { - std::cout << "\nTST 12\n"; - environment env; - init_test_frontend(env); - expr lst = Const("list"); - expr nil = Const("nil"); - expr cons = Const("cons"); - expr N = Const("N"); - expr A = Const("A"); - expr f = Const("f"); - expr l = Const("l"); - expr a = Const("a"); - env->add_var("N", Type()); - env->add_var("list", Type() >> Type()); - env->add_var("nil", Pi({A, Type()}, lst(A))); - env->add_var("cons", Pi({{A, Type()}, {a, A}, {l, lst(A)}}, lst(A))); - env->add_var("f", lst(N >> N) >> Bool); - success(Fun({a, _}, f(cons(_, a, cons(_, a, nil(_))))), - Fun({a, N >> N}, f(cons(N >> N, a, cons(N >> N, a, nil(N >> N))))), env); -} - -static void tst13() { - std::cout << "\nTST 13\n"; - environment env; - init_test_frontend(env); - expr B = Const("B"); - expr A = Const("A"); - expr x = Const("x"); - expr f = Const("f"); - env->add_var("f", Pi({B, Type()}, B >> B)); - success(Fun({{A, Type()}, {B, Type()}, {x, _}}, f(B, x)), - Fun({{A, Type()}, {B, Type()}, {x, B}}, f(B, x)), env); - fails(Fun({{x, _}, {A, Type()}}, f(A, x)), env); - success(Fun({{A, Type()}, {x, _}}, f(A, x)), - Fun({{A, Type()}, {x, A}}, f(A, x)), env); - success(Fun({{A, Type()}, {B, Type()}, {x, _}}, f(A, x)), - Fun({{A, Type()}, {B, Type()}, {x, A}}, f(A, x)), env); - success(Fun({{A, Type()}, {B, Type()}, {x, _}}, mk_eq(_, f(B, x), f(_, x))), - Fun({{A, Type()}, {B, Type()}, {x, B}}, mk_eq(B, f(B, x), f(B, x))), env); - success(Fun({{A, Type()}, {B, Type()}, {x, _}}, mk_eq(B, f(B, x), f(_, x))), - Fun({{A, Type()}, {B, Type()}, {x, B}}, mk_eq(B, f(B, x), f(B, x))), env); - unsolved(Fun({{A, _}, {B, _}, {x, _}}, mk_eq(_, f(B, x), f(_, x))), env); -} - -static void tst14() { - std::cout << "\nTST 14\n"; - environment env; - init_test_frontend(env); - expr A = Const("A"); - expr B = Const("B"); - expr f = Const("f"); - expr g = Const("g"); - expr x = Const("x"); - expr y = Const("y"); - env->add_var("N", Type()); - env->add_var("f", Pi({A, Type()}, A >> A)); - expr N = Const("N"); - success(Fun({g, Pi({A, Type()}, A >> (A >> Bool))}, g(_, True, False)), - Fun({g, Pi({A, Type()}, A >> (A >> Bool))}, g(Bool, True, False)), - env); - success(Fun({g, Pi({A, TypeU}, A >> (A >> Bool))}, g(_, Bool, Bool)), - Fun({g, Pi({A, TypeU}, A >> (A >> Bool))}, g(Type(), Bool, Bool)), - env); - success(Fun({g, Pi({A, TypeU}, A >> (A >> Bool))}, g(_, Bool, N)), - Fun({g, Pi({A, TypeU}, A >> (A >> Bool))}, g(Type(), Bool, N)), - env); -} - -static void tst15() { - std::cout << "\nTST 15\n"; - environment env; - init_test_frontend(env); - expr A = Const("A"); - expr B = Const("B"); - expr C = Const("C"); - expr a = Const("a"); - expr b = Const("b"); - expr eq = Const("my_eq"); - env->add_var("my_eq", Pi({A, Type()}, A >> (A >> Bool))); - success(Fun({{A, Type()}, {B, Type()}, {a, _}, {b, B}}, eq(_, a, b)), - Fun({{A, Type()}, {B, Type()}, {a, B}, {b, B}}, eq(B, a, b)), env); - success(Fun({{A, Type()}, {B, Type()}, {a, _}, {b, A}}, eq(_, a, b)), - Fun({{A, Type()}, {B, Type()}, {a, A}, {b, A}}, eq(A, a, b)), env); - success(Fun({{A, Type()}, {B, Type()}, {a, A}, {b, _}}, eq(_, a, b)), - Fun({{A, Type()}, {B, Type()}, {a, A}, {b, A}}, eq(A, a, b)), env); - success(Fun({{A, Type()}, {B, Type()}, {a, B}, {b, _}}, eq(_, a, b)), - Fun({{A, Type()}, {B, Type()}, {a, B}, {b, B}}, eq(B, a, b)), env); - success(Fun({{A, Type()}, {B, Type()}, {a, B}, {b, _}, {C, Type()}}, eq(_, a, b)), - Fun({{A, Type()}, {B, Type()}, {a, B}, {b, B}, {C, Type()}}, eq(B, a, b)), env); - fails(Fun({{A, Type()}, {B, Type()}, {a, _}, {b, _}, {C, Type()}}, eq(C, a, b)), env); - success(Fun({{A, Type()}, {B, Type()}, {a, _}, {b, _}, {C, Type()}}, eq(B, a, b)), - Fun({{A, Type()}, {B, Type()}, {a, B}, {b, B}, {C, Type()}}, eq(B, a, b)), env); -} - -static void tst16() { - std::cout << "\nTST 16\n"; - environment env; - init_test_frontend(env); - expr a = Const("a"); - expr b = Const("b"); - expr c = Const("c"); - expr H1 = Const("H1"); - expr H2 = Const("H2"); - env->add_var("a", Bool); - env->add_var("b", Bool); - env->add_var("c", Bool); - success(Fun({{H1, mk_eq(_, a, b)}, {H2, mk_eq(_, b, c)}}, - mk_trans_th(_, _, _, _, H1, H2)), - Fun({{H1, mk_eq(Bool, a, b)}, {H2, mk_eq(Bool, b, c)}}, - mk_trans_th(Bool, a, b, c, H1, H2)), - env); - expr H3 = Const("H3"); - success(Fun({{H1, mk_eq(Bool, a, b)}, {H2, mk_eq(Bool, b, c)}, {H3, a}}, - mk_eqt_intro_th(_, mk_eqmp_th(_, _, mk_symm_th(_, _, _, mk_trans_th(_, _, _, _, mk_symm_th(_, _, _, H2), mk_symm_th(_, _, _, H1))), H3))), - Fun({{H1, mk_eq(Bool, a, b)}, {H2, mk_eq(Bool, b, c)}, {H3, a}}, - mk_eqt_intro_th(c, mk_eqmp_th(a, c, mk_symm_th(Bool, c, a, mk_trans_th(Bool, c, b, a, mk_symm_th(Bool, b, c, H2), mk_symm_th(Bool, a, b, H1))), H3))), - env); - environment env2; - init_test_frontend(env2); - success(Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, mk_eq(_, a, b)}, {H2, mk_eq(_, b, c)}, {H3, a}}, - mk_eqt_intro_th(_, mk_eqmp_th(_, _, mk_symm_th(_, _, _, mk_trans_th(_, _, _, _, mk_symm_th(_, _, _, H2), mk_symm_th(_, _, _, H1))), H3))), - Fun({{a, Bool}, {b, Bool}, {c, Bool}, {H1, mk_eq(Bool, a, b)}, {H2, mk_eq(Bool, b, c)}, {H3, a}}, - mk_eqt_intro_th(c, mk_eqmp_th(a, c, mk_symm_th(Bool, c, a, mk_trans_th(Bool, c, b, a, mk_symm_th(Bool, b, c, H2), mk_symm_th(Bool, a, b, H1))), H3))), - env2); - expr A = Const("A"); - success(Fun({{A, Type()}, {a, A}, {b, A}, {c, A}, {H1, mk_eq(_, a, b)}, {H2, mk_eq(_, b, c)}}, - mk_symm_th(_, _, _, mk_trans_th(_, _, _, _, mk_symm_th(_, _, _, H2), mk_symm_th(_, _, _, H1)))), - Fun({{A, Type()}, {a, A}, {b, A}, {c, A}, {H1, mk_eq(A, a, b)}, {H2, mk_eq(A, b, c)}}, - mk_symm_th(A, c, a, mk_trans_th(A, c, b, a, mk_symm_th(A, b, c, H2), mk_symm_th(A, a, b, H1)))), - env2); -} - -void tst17() { - std::cout << "\nTST 17\n"; - environment env; - init_test_frontend(env); - expr A = Const("A"); - expr B = Const("B"); - expr a = Const("a"); - expr b = Const("b"); - expr eq = Const("my_eq"); - env->add_var("my_eq", Pi({A, Type(level()+1)}, A >> (A >> Bool))); - success(eq(_, Fun({{A, Type()}, {a, _}}, a), Fun({{B, Type()}, {b, B}}, b)), - eq(Pi({A, Type()}, A >> A), Fun({{A, Type()}, {a, A}}, a), Fun({{B, Type()}, {b, B}}, b)), - env); -} - -void tst18() { - std::cout << "\nTST 18\n"; - environment env; - init_test_frontend(env); - expr A = Const("A"); - expr h = Const("h"); - expr f = Const("f"); - expr a = Const("a"); - env->add_var("h", Pi({A, Type()}, A) >> Bool); - success(Fun({{f, Pi({A, Type()}, _)}, {a, Bool}}, h(f)), - Fun({{f, Pi({A, Type()}, A)}, {a, Bool}}, h(f)), - env); -} - -void tst19() { - std::cout << "\nTST 19\n"; - environment env; - init_test_frontend(env); - expr R = Const("R"); - expr A = Const("A"); - expr r = Const("r"); - expr eq = Const("my_eq"); - expr f = Const("f"); - expr g = Const("g"); - expr h = Const("h"); - expr D = Const("D"); - env->add_var("R", Type() >> Bool); - env->add_var("r", Pi({A, Type()}, R(A))); - env->add_var("h", Pi({A, Type()}, R(A)) >> Bool); - env->add_var("my_eq", Pi({A, Type(level()+1)}, A >> (A >> Bool))); - success(Let({{f, Fun({A, Type()}, r(_))}, - {g, Fun({A, Type()}, r(_))}, - {D, Fun({A, Type()}, eq(_, f(A), g(_)))}}, - h(f)), - Let({{f, Fun({A, Type()}, r(A))}, - {g, Fun({A, Type()}, r(A))}, - {D, Fun({A, Type()}, eq(R(A), f(A), g(A)))}}, - h(f)), - env); -} - -void tst20() { - std::cout << "\nTST 20\n"; - environment env; - init_test_frontend(env); - metavar_env menv; - expr N = Const("N1"); - expr M = Const("M1"); - env->add_var("N1", Type()); - env->add_var("M1", 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 = menv->mk_metavar(); - expr l = m1(b, a); - expr r = f(b, f(a, b)); - elaborator elb(env, menv, context(), l, r); - while (true) { - try { - auto sol = elb.next(); - std::cout << m1 << " -> " << *(sol->get_subst(m1)) << "\n"; - std::cout << sol->instantiate_metavars(l) << "\n"; - lean_assert(sol->instantiate_metavars(l) == r); - std::cout << "--------------\n"; - } catch (elaborator_exception & ex) { - break; - } - } -} - -void tst21() { - std::cout << "\nTST 21\n"; - environment env; - init_test_frontend(env); - metavar_env menv; - expr N = Const("N"); - expr M = Const("M"); - env->add_var("N", Type()); - env->add_var("f", N >> (Bool >> N)); - env->add_var("a", N); - env->add_var("b", N); - expr f = Const("f"); - expr x = Const("x"); - expr a = Const("a"); - expr b = Const("b"); - expr m1 = menv->mk_metavar(); - expr l = m1(b, a); - expr r = Fun({x, N}, f(x, mk_eq(_, a, b))); - elaborator elb(env, menv, context(), l, r); - while (true) { - try { - auto sol = elb.next(); - std::cout << m1 << " -> " << *(sol->get_subst(m1)) << "\n"; - std::cout << sol->instantiate_metavars(l) << "\n"; - lean_assert(sol->instantiate_metavars(l) == r); - std::cout << "--------------\n"; - } catch (elaborator_exception & ex) { - break; - } - } -} - -void tst22() { - std::cout << "\nTST 22\n"; - environment env; - init_test_frontend(env); - metavar_env menv; - expr N = Const("N"); - env->add_var("N", Type()); - env->add_var("f", N >> (Int >> N)); - env->add_var("a", N); - env->add_var("b", N); - expr m1 = menv->mk_metavar(); - expr m2 = menv->mk_metavar(); - expr m3 = menv->mk_metavar(); - expr t1 = menv->get_type(m1); - expr t2 = menv->get_type(m2); - expr f = Const("f"); - expr a = Const("a"); - expr b = Const("b"); - expr l = f(m1(a), mk_Int_add(m3, mk_Int_add(iVal(1), iVal(1)))); - expr r = f(m2(b), mk_Int_add(iVal(1), iVal(2))); - elaborator elb(env, menv, context(), l, r); - while (true) { - try { - auto sol = elb.next(); - std::cout << m3 << " -> " << *(sol->get_subst(m3)) << "\n"; - lean_assert(*(sol->get_subst(m3)) == iVal(1)); - std::cout << sol->instantiate_metavars(l) << "\n"; - std::cout << sol->instantiate_metavars(r) << "\n"; - std::cout << "--------------\n"; - } catch (elaborator_exception & ex) { - break; - } - } -} - -void tst23() { - std::cout << "\nTST 23\n"; - environment env; - init_test_frontend(env); - metavar_env menv; - 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 = menv->mk_metavar(); - expr m2 = menv->mk_metavar(); - expr l = Fun({{x, N}, {y, N}}, mk_eq(_, y, f(x, m1))); - expr r = Fun({{x, N}, {y, N}}, mk_eq(_, m2, f(m1, x))); - elaborator elb(env, menv, context(), l, r); - while (true) { - try { - auto sol = elb.next(); - std::cout << m1 << " -> " << *(sol->get_subst(m1)) << "\n"; - std::cout << sol->instantiate_metavars(l) << "\n"; - lean_assert_eq(sol->instantiate_metavars(l), - sol->instantiate_metavars(r)); - std::cout << "--------------\n"; - } catch (elaborator_exception & ex) { - break; - } - } -} - -void tst24() { - std::cout << "\nTST 24\n"; - environment env; - init_test_frontend(env); - metavar_env menv; - expr N = Const("N"); - env->add_var("N", Type()); - env->add_var("f", N >> (N >> N)); - expr f = Const("f"); - expr m1 = menv->mk_metavar(); - expr l = f(f(m1)); - expr r = f(m1); - elaborator elb(env, menv, context(), l, r); - try { - elb.next(); - lean_unreachable(); - } catch (elaborator_exception & ex) { - } -} - -void tst25() { - std::cout << "\nTST 25\n"; - environment env; - init_test_frontend(env); - metavar_env menv; - 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 = menv->mk_metavar(); - expr l = Fun({x, N}, Fun({y, N}, f(m1, y))(x)); - expr r = Fun({x, N}, f(x, x)); - elaborator elb(env, menv, context(), l, r); - while (true) { - try { - auto sol = elb.next(); - std::cout << m1 << " -> " << *(sol->get_subst(m1)) << "\n"; - std::cout << sol->instantiate_metavars(l) << "\n"; - lean_assert_eq(beta_reduce(sol->instantiate_metavars(l)), - beta_reduce(sol->instantiate_metavars(r))); - std::cout << "--------------\n"; - } catch (elaborator_exception & ex) { - break; - } - } -} - -void tst26() { - std::cout << "\nTST 26\n"; - /* - Solve elaboration problem for - - g : Pi (A : Type U), A -> A - a : Type 1 - Axiom H : g _ a = a - */ - environment env; - init_test_frontend(env); - env->add_uvar_cnstr("U", level() + 2); - metavar_env menv; - buffer ucs; - type_checker checker(env); - expr A = Const("A"); - expr g = Const("g"); - env->add_var("g", Pi({A, TypeU}, A >> A)); - expr a = Const("a"); - env->add_var("a", Type(level()+1)); - expr m1 = menv->mk_metavar(); - expr m2 = menv->mk_metavar(); - expr F = mk_eq(m2, g(m1, a), a); - std::cout << F << "\n"; - std::cout << checker.check(F, context(), menv, ucs) << "\n"; - elaborator elb(env, menv, ucs.size(), ucs.data()); - metavar_env s = elb.next(); - std::cout << s->instantiate_metavars(F) << "\n"; - lean_assert_eq(s->instantiate_metavars(F), mk_eq(Type(level()+1), g(Type(level()+1), a), a)); -} - -void tst27() { - std::cout << "\nTST 27\n"; - /* - Solve elaboration problem for - - g : Pi (A : Type U), A -> A - eq : Pi (A : Type U), A -> A -> Bool - a : Type M - fun f : _, eq _ ((g _ f) a) a - */ - environment env; - init_test_frontend(env); - metavar_env menv; - buffer ucs; - type_checker checker(env); - expr A = Const("A"); - expr g = Const("g"); - expr f = Const("f"); - expr a = Const("a"); - expr eq = Const("my_eq"); - env->add_var("my_eq", Pi({A, TypeU}, A >> (A >> Bool))); - env->add_var("g", Pi({A, TypeU}, A >> A)); - env->add_var("a", Type()); - expr m1 = menv->mk_metavar(); - expr m2 = menv->mk_metavar(); - expr m3 = menv->mk_metavar(); - expr F = Fun({f, m1}, eq(m2, g(m3, f)(a), a)); - std::cout << F << "\n"; - std::cout << checker.check(F, context(), menv, ucs) << "\n"; - elaborator elb(env, menv, ucs.size(), ucs.data()); - metavar_env s = elb.next(); - std::cout << s->instantiate_metavars(F) << "\n"; - lean_assert_eq(s->instantiate_metavars(F), - Fun({f, Type() >> Type()}, eq(Type(), g(Type() >> Type(), f)(a), a))); -} - -int main() { - save_stack_info(); - register_modules(); - tst1(); - tst2(); - tst3(); - tst4(); - tst5(); - tst6(); - tst7(); - tst8(); - tst9(); - tst10(); - tst11(); - tst12(); - tst13(); - tst14(); - tst15(); - tst16(); - tst17(); - tst18(); - tst19(); - tst20(); - tst21(); - tst22(); - tst23(); - tst24(); - tst25(); - tst26(); - tst27(); - return has_violations() ? 1 : 0; -}