From c66dbf202bc49b1bdd5c04ee4785a2cb406b2c81 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 19 Sep 2016 17:13:30 -0700 Subject: [PATCH] chore(library/equations_compiler): remove old equation compiler --- src/frontends/lean/CMakeLists.txt | 8 +- src/library/equations_compiler/CMakeLists.txt | 4 +- .../equations_compiler/old_compiler.cpp | 1539 ----------------- src/library/equations_compiler/old_compiler.h | 12 - src/library/equations_compiler/old_goal.cpp | 182 -- src/library/equations_compiler/old_goal.h | 113 -- .../equations_compiler/old_inversion.cpp | 1102 ------------ .../equations_compiler/old_inversion.h | 62 - 8 files changed, 2 insertions(+), 3020 deletions(-) delete mode 100644 src/library/equations_compiler/old_compiler.cpp delete mode 100644 src/library/equations_compiler/old_compiler.h delete mode 100644 src/library/equations_compiler/old_goal.cpp delete mode 100644 src/library/equations_compiler/old_goal.h delete mode 100644 src/library/equations_compiler/old_inversion.cpp delete mode 100644 src/library/equations_compiler/old_inversion.h diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index 7d7403ff61..fc0c5b06be 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -9,10 +9,4 @@ type_util.cpp local_ref_info.cpp decl_attributes.cpp nested_declaration.cpp opt_cmd.cpp prenum.cpp print_cmd.cpp elaborator.cpp match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp # LEGACY -old_attributes.cpp -# begin_end_annotation.cpp tactic_hint.cpp -# info_tactic.cpp -# parse_tactic_location.cpp parse_rewrite_tactic.cpp builtin_tactics.cpp -# parse_with_options_tactic.cpp -#parse_with_attributes_tactic.cpp -) +old_attributes.cpp) diff --git a/src/library/equations_compiler/CMakeLists.txt b/src/library/equations_compiler/CMakeLists.txt index c380277d8b..db6c6d1598 100644 --- a/src/library/equations_compiler/CMakeLists.txt +++ b/src/library/equations_compiler/CMakeLists.txt @@ -1,6 +1,4 @@ add_library(equations_compiler OBJECT equations.cpp util.cpp pack_domain.cpp structural_rec.cpp unbounded_rec.cpp - elim_match.cpp compiler.cpp init_module.cpp -#LEGACY - old_compiler.cpp old_goal.cpp old_inversion.cpp) + elim_match.cpp compiler.cpp init_module.cpp) diff --git a/src/library/equations_compiler/old_compiler.cpp b/src/library/equations_compiler/old_compiler.cpp deleted file mode 100644 index cdeba1fa1b..0000000000 --- a/src/library/equations_compiler/old_compiler.cpp +++ /dev/null @@ -1,1539 +0,0 @@ -/* -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include "util/sstream.h" -#include "util/list_fn.h" -#include "util/fresh_name.h" -#include "kernel/expr.h" -#include "kernel/type_checker.h" -#include "kernel/abstract.h" -#include "kernel/instantiate.h" -#include "kernel/error_msgs.h" -#include "kernel/for_each_fn.h" -#include "kernel/find_fn.h" -#include "kernel/replace_fn.h" -#include "library/exception.h" -#include "library/kernel_serializer.h" -#include "library/io_state_stream.h" -#include "library/annotation.h" -#include "library/util.h" -#include "library/old_util.h" -#include "library/locals.h" -#include "library/constants.h" -#include "library/normalize.h" -#include "library/pp_options.h" -#include "library/equations_compiler/equations.h" -#include "library/equations_compiler/old_inversion.h" - -namespace lean { -class equation_compiler_fn { - old_type_checker & m_tc; - io_state const & m_ios; - expr m_meta; - expr m_meta_type; - buffer m_global_context; - // The additional context is used to store inductive datatype parameters that occur as arguments in recursive equations. - // For example, suppose the user writes - // - // definition append : Π (A : Type), list A → list A → list A, - // append A nil l := l, - // append A (h :: t) l := h :: (append t l) - // - // instead of - // - // definition append (A : Type) : list A → list A → list A, - // append nil l := l, - // append (h :: t) l := h :: (append t l) - // - // In this case, we move the parameter (A : Type) to m_additional_context and simplify the recursive equations. - // The simplification is necessary when we are translating the recursive applications into a brec_on recursor. - buffer m_additional_context; - buffer m_fns; // functions being defined - - environment const & env() const { return m_tc.env(); } - io_state const & ios() const { return m_ios; } - io_state_stream out() const { return regular(env(), ios(), m_tc.get_type_context()); } - expr whnf(expr const & e) { return m_tc.whnf(e).first; } - expr infer_type(expr const & e) { return m_tc.infer(e).first; } - bool is_def_eq(expr const & e1, expr const & e2) { return m_tc.is_def_eq(e1, e2).first; } - bool is_proof_irrelevant() const { return m_tc.env().prop_proof_irrel(); } - - optional is_constructor(expr const & e) const { - if (!is_constant(e)) - return optional(); - return inductive::is_intro_rule(env(), const_name(e)); - } - - expr to_telescope(expr const & e, buffer & tele) { - return ::lean::to_telescope(e, tele, optional()); - } - - expr fun_to_telescope(expr const & e, buffer & tele) { - return ::lean::fun_to_telescope(e, tele, optional()); - } - - // Similar to to_telescope, but uses normalization - expr to_telescope_ext(expr const & e, buffer & tele) { - return ::lean::to_telescope(m_tc, e, tele, optional()); - } - - [[ noreturn ]] static void throw_error(char const * msg, expr const & src) { throw generic_exception(src, msg); } - [[ noreturn ]] static void throw_error(sstream const & ss, expr const & src) { throw generic_exception(src, ss); } - [[ noreturn ]] static void throw_error(expr const & src, pp_fn const & fn) { throw generic_exception(src, fn); } - [[ noreturn ]] void throw_error(sstream const & ss) const { throw generic_exception(m_meta, ss); } - [[ noreturn ]] void throw_error(expr const & src, sstream const & ss) const { throw generic_exception(src, ss); } - - void check_limitations(expr const & eqns) const { - if (is_wf_equations(eqns) && equations_num_fns(eqns) != 1) - throw_error("mutually recursive equations do not support well-founded recursion yet", eqns); - } - -#ifdef LEAN_DEBUG - static bool disjoint(list const & l1, list const & l2) { - for (expr const & e1 : l1) { - for (expr const & e2 : l2) { - lean_assert(mlocal_name(e1) != mlocal_name(e2)); - } - } - return true; - } - - // Return true iff all names in s1 are names of local constants in s2. - static bool contained(list> const & s1, list const & s2) { - return std::all_of(s1.begin(), s1.end(), [&](optional const & n) { - return - !n || - std::any_of(s2.begin(), s2.end(), [&](expr const & e) { - return mlocal_name(e) == *n; - }); - }); - } -#endif - - struct eqn { - // The local context for an equation is of additional - // local constants occurring in m_patterns and m_rhs - // which are not in m_global_context or - // in the function containing the equation. - // Remark: each function/program contains its own m_context. - // So, the variables occurring in m_patterns and m_rhs - // are in m_global_context, m_context, or m_local_context, - // or is one of the functions being defined. - // We say an equation is in "compiled" form - // if m_local_context and m_patterns are empty. - list m_local_context; - list m_patterns; // patterns to be processed - expr m_rhs; // right-hand-side - eqn(list const & c, list const & p, expr const & r): - m_local_context(c), m_patterns(p), m_rhs(r) {} - eqn(eqn const & e, list const & c, list const & p): - eqn(c, p, e.m_rhs) {} - }; - - // Data-structure used to store for compiling pattern matching. - // We create a program object for each function being defined - struct program { - expr m_fn; // function being defined - list m_context; // local constants - list> m_var_stack; // variables that must be matched with the patterns it is a "subset" of m_context. - list m_eqns; // equations - expr m_type; // result type - - // Due to dependent pattern matching some elements in m_var_stack are "none", and are skipped - // during dependent pattern matching. - - // The goal of the compiler is to process all variables in m_var_stack - program(expr const & fn, list const & ctx, list> const & s, list const & e, expr const & t): - m_fn(fn), m_context(ctx), m_var_stack(s), m_eqns(e), m_type(t) { - lean_assert(contained(m_var_stack, m_context)); - } - program(program const & p, list const & ctx, list> const & new_s, list const & new_e): - program(p.m_fn, ctx, new_s, new_e, p.m_type) {} - program(program const & p, list> const & new_s, list const & new_e): - program(p.m_fn, p.m_context, new_s, new_e, p.m_type) {} - program(program const & p, list const & ctx): - program(p.m_fn, ctx, p.m_var_stack, p.m_eqns, p.m_type) {} - program(program const & p, list const & new_e): - program(p, p.m_var_stack, new_e) {} - program() {} - expr const & get_var(name const & n) const { - for (expr const & v : m_context) { - if (mlocal_name(v) == n) - return v; - } - lean_unreachable(); - } - }; - - // Auxiliary fields for producing error messages - buffer m_init_prgs; - unsigned m_prg_idx; // current program index being compiled - -#ifdef LEAN_DEBUG - // For debugging purposes: checks whether all local constants occurring in \c e - // are in local_ctx or m_global_context - bool check_ctx(expr const & e, list const & context, list const & local_context) const { - for_each(e, [&](expr const & e, unsigned) { - if (is_local(e)) { - if (!(contains_local(e, local_context) || - contains_local(e, context) || - contains_local(e, m_additional_context) || - contains_local(e, m_global_context) || - contains_local(e, m_fns))) { - lean_unreachable(); - } - return false; // do not visit type - } - if (is_metavar(e)) - return false; // do not visit type - return true; - }); - return true; - } - - // For debugging purposes: check if the program is well-formed - bool check_program(program const & s) const { - unsigned sz = length(s.m_var_stack); - lean_assert(contained(s.m_var_stack, s.m_context)); - for (eqn const & e : s.m_eqns) { - // the number of patterns in each equation is equal to the variable stack size - if (length(e.m_patterns) != sz) { - lean_unreachable(); - return false; - } - check_ctx(e.m_rhs, s.m_context, e.m_local_context); - for (expr const & p : e.m_patterns) - check_ctx(p, s.m_context, e.m_local_context); - lean_assert(disjoint(e.m_local_context, s.m_context)); - } - return true; - } -#endif - - // Initialize m_fns (the vector of functions to be compiled) - void initialize_fns(expr const & eqns) { - lean_assert(is_equations(eqns)); - unsigned num_fns = equations_num_fns(eqns); - buffer eqs; - to_equations(eqns, eqs); - expr eq = eqs[0]; - for (unsigned i = 0; i < num_fns; i++) { - expr fn = mk_local(mk_fresh_name(), binding_name(eq), binding_domain(eq), binder_info()); - m_fns.push_back(fn); - eq = instantiate(binding_body(eq), fn); - } - } - - // Store in \c arities the number of arguments of each function being defined. - // This procedure also makes sure that two different equations for the same function - // contain the same number of arguments in the left-hand-side. - // Remark: after executing this procedure the arity of m_fns[i] is stored in arities[i] - // if there is at least one equation for m_fns[i]. - void initialize_arities(expr const & eqns, buffer> & arities) { - lean_assert(arities.empty()); - buffer eqs; - to_equations(eqns, eqs); - lean_assert(!eqs.empty()); - arities.resize(m_fns.size()); - for (expr eq : eqs) { - if (is_lambda_equation(eq)) { - for (expr const & fn : m_fns) - eq = instantiate(binding_body(eq), fn); - while (is_lambda(eq)) - eq = binding_body(eq); - lean_assert(is_equation(eq)); - expr const & lhs = equation_lhs(eq); - buffer lhs_args; - expr const & lhs_fn = get_app_args(lhs, lhs_args); - if (!is_local(lhs_fn)) - throw_error(sstream() << "invalid equation, " - << "left-hand-side is not one of the functions being defined", eq); - unsigned i = 0; - for (; i < m_fns.size(); i++) { - if (lhs_fn == m_fns[i]) { - if (arities[i] && *arities[i] != lhs_args.size()) - throw_error(sstream() << "invalid equation for '" << lhs_fn << "' " - << "left-hand-side of different equations have different number of arguments", eq); - arities[i] = lhs_args.size(); - } - } - } - } - } - - // Initialize the variable stack for each function that needs - // to be compiled. - // This method assumes m_fns has been already initialized. - // This method also initialized the buffer prg, but the eqns - // field of each program is not initialized by it. - // - // See initialize_arities for an explanation for \c arities. - void initialize_var_stack(buffer & prgs, buffer> const & arities) { - lean_assert(!m_fns.empty()); - lean_assert(prgs.empty()); - for (unsigned i = 0; i < m_fns.size(); i++) { - expr const & fn = m_fns[i]; - buffer args; - expr r_type = to_telescope(mlocal_type(fn), args); - for (expr & arg : args) - arg = update_mlocal(arg, whnf(mlocal_type(arg))); - if (arities[i]) { - unsigned arity = *arities[i]; - if (args.size() > arity) { - r_type = Pi(args.size() - arity, args.data() + arity, r_type); - args.shrink(arity); - } - } - list ctx = to_list(args); - list> vstack = map2>(ctx, [](expr const & e) { - return optional(mlocal_name(e)); - }); - prgs.push_back(program(fn, ctx, vstack, list(), r_type)); - } - } - - struct validate_exception { - expr m_expr; - validate_exception(expr const & e):m_expr(e) {} - }; - - void check_in_local_ctx(expr const & e, buffer const & local_ctx) { - if (!contains_local(e, local_ctx)) - throw_error(e, sstream() << "invalid equation, variable '" << e - << "' has the same name of a variable in an outer-scope (solution: rename this variable)"); - } - - // Validate/normalize the given pattern. - // It stores in reachable_vars any variable that does not occur - // in inaccessible terms. - expr validate_pattern(expr pat, buffer const & local_ctx, name_set & reachable_vars) { - if (is_inaccessible(pat)) - return pat; - if (is_local(pat)) { - reachable_vars.insert(mlocal_name(pat)); - check_in_local_ctx(pat, local_ctx); - return pat; - } - expr new_pat = whnf(pat); - if (is_local(new_pat)) { - reachable_vars.insert(mlocal_name(new_pat)); - check_in_local_ctx(new_pat, local_ctx); - return new_pat; - } - buffer pat_args; - expr const & fn = get_app_args(new_pat, pat_args); - if (auto in = is_constructor(fn)) { - unsigned num_params = *inductive::get_num_params(env(), *in); - for (unsigned i = num_params; i < pat_args.size(); i++) - pat_args[i] = validate_pattern(pat_args[i], local_ctx, reachable_vars); - return mk_app(fn, pat_args, pat.get_tag()); - } else { - throw validate_exception(pat); - } - } - - // Validate/normalize the patterns associated with the given lhs. - // The lhs is only used to report errors. - // It stores in reachable_vars any variable that does not occur - // in inaccessible terms. - void validate_patterns(expr const & lhs, buffer const & local_ctx, buffer & patterns, name_set & reachable_vars) { - for (expr & pat : patterns) { - try { - pat = validate_pattern(pat, local_ctx, reachable_vars); - } catch (validate_exception & ex) { - expr problem_expr = ex.m_expr; - throw_error(lhs, [=](formatter const & fmt) { - format r("invalid argument, it is not a constructor, variable, " - "nor it is marked as an inaccessible pattern"); - r += pp_indent_expr(fmt, problem_expr); - r += compose(line(), format("in the following equation left-hand-side")); - r += pp_indent_expr(fmt, lhs); - return r; - }); - } - } - } - - // Create initial program state for each function being defined. - void initialize(expr const & eqns, buffer & prg) { - lean_assert(is_equations(eqns)); - buffer> arities; - initialize_fns(eqns); - initialize_arities(eqns, arities); - initialize_var_stack(prg, arities); - buffer eqs; - to_equations(eqns, eqs); - buffer> res_eqns; - res_eqns.resize(m_fns.size()); - for (expr eq : eqs) { - if (is_lambda_no_equation(eq)) - continue; // skip marker - for (expr const & fn : m_fns) - eq = instantiate(binding_body(eq), fn); - buffer local_ctx; - eq = fun_to_telescope(eq, local_ctx); - expr const & lhs = equation_lhs(eq); - expr const & rhs = equation_rhs(eq); - buffer patterns; - expr const & fn = get_app_args(lhs, patterns); - name_set reachable_vars; - validate_patterns(lhs, local_ctx, patterns, reachable_vars); - for (expr const & v : local_ctx) { - // every variable in the local_ctx must be "reachable". - if (!reachable_vars.contains(mlocal_name(v))) { - throw_error(lhs, [=](formatter const & fmt) { - options o = fmt.get_options().update_if_undef(get_pp_implicit_name(), true); - formatter new_fmt = fmt.update_options(o); - format r("invalid equation left-hand-side, variable '"); - r += format(local_pp_name(v)); - r += format("' only occurs in inaccessible terms in the following equation left-hand-side"); - r += pp_indent_expr(new_fmt, lhs); - return r; - }); - } - } - for (unsigned i = 0; i < m_fns.size(); i++) { - if (mlocal_name(fn) == mlocal_name(m_fns[i])) { - if (patterns.size() != length(prg[i].m_var_stack)) - throw_error("ill-formed equation, number of provided arguments does not match function type", eq); - res_eqns[i].push_back(eqn(to_list(local_ctx), to_list(patterns), rhs)); - } - } - } - for (unsigned i = 0; i < m_fns.size(); i++) { - prg[i].m_eqns = to_list(res_eqns[i]); - lean_assert(check_program(prg[i])); - } - } - - // For debugging purposes: display the context at m_ios - template - void display_ctx(Ctx const & ctx) const { - bool first = true; - for (expr const & e : ctx) { - out() << (first ? "" : ", ") << local_pp_name(e) << " : " << mlocal_type(e); - first = false; - } - } - - // For debugging purposes: dump prg in m_ios - void display(program const & prg) const { - display_ctx(prg.m_context); - out() << " ;;"; - for (optional const & v : prg.m_var_stack) { - if (v) - out() << " " << local_pp_name(prg.get_var(*v)); - else - out() << " "; - } - out() << " |- " << prg.m_type << "\n"; - out() << "\n"; - for (eqn const & e : prg.m_eqns) { - out() << "> "; - display_ctx(e.m_local_context); - out() << " |-"; - for (expr const & p : e.m_patterns) { - if (is_atomic(p)) - out() << " " << p; - else - out() << " (" << p << ")"; - } - out() << " := " << e.m_rhs << "\n"; - } - } - - // Return true iff the next pattern in all equations is a variable or an inaccessible term - bool is_variable_transition(program const & p) const { - for (eqn const & e : p.m_eqns) { - lean_assert(e.m_patterns); - if (!is_local(head(e.m_patterns)) && !is_inaccessible(head(e.m_patterns))) - return false; - } - return true; - } - - // Return true iff the next pattern in all equations is a constructor. - bool is_constructor_transition(program const & p) const { - for (eqn const & e : p.m_eqns) { - lean_assert(e.m_patterns); - if (!is_constructor(get_app_fn(head(e.m_patterns)))) - return false; - } - return true; - } - - /** Return true if there are no equations, and the next variable is an inductive datatype. - In this case, it is worth trying the cases tactic, since this may be a conflicting state. */ - bool is_no_equation_constructor_transition(program const & p) { - lean_assert(p.m_var_stack); - if (!p.m_eqns && head(p.m_var_stack)) { - expr const & x = p.get_var(*head(p.m_var_stack)); - expr const & I = get_app_fn(mlocal_type(x)); - return is_constant(I) && inductive::is_inductive_decl(env(), const_name(I)); - } else { - return false; - } - } - - // Return true iff the next pattern of every equation is a constructor or variable, - // and there are at least one equation where it is a variable and another where it is a - // constructor. - bool is_complete_transition(program const & p) const { - bool has_variable = false; - bool has_constructor = false; - for (eqn const & e : p.m_eqns) { - lean_assert(e.m_patterns); - expr const & p = head(e.m_patterns); - if (is_local(p)) - has_variable = true; - else if (is_constructor(get_app_fn(p))) - has_constructor = true; - else - return false; - } - return has_variable && has_constructor; - } - - // Remove variable from local context - static list remove(list const & local_ctx, expr const & l) { - if (!local_ctx) - return local_ctx; - else if (mlocal_name(head(local_ctx)) == mlocal_name(l)) - return tail(local_ctx); - else - return cons(head(local_ctx), remove(tail(local_ctx), l)); - } - - static expr replace(expr const & e, buffer const & from_buffer, buffer const & to_buffer) { - lean_assert(from_buffer.size() == to_buffer.size()); - return instantiate_rev(abstract_locals(e, from_buffer.size(), from_buffer.data()), - to_buffer.size(), to_buffer.data()); - } - - eqn replace(eqn const & e, expr const & from, expr const & to) { - buffer from_buffer; from_buffer.push_back(from); - buffer to_buffer; to_buffer.push_back(to); - buffer new_ctx; - for (expr const & l : e.m_local_context) { - expr new_l = replace(l, from_buffer, to_buffer); - if (new_l != l) { - from_buffer.push_back(l); - to_buffer.push_back(new_l); - } - new_ctx.push_back(new_l); - } - list new_patterns = map(e.m_patterns, [&](expr const & p) { return replace(p, from_buffer, to_buffer); }); - expr new_rhs = replace(e.m_rhs, from_buffer, to_buffer); - return eqn(to_list(new_ctx), new_patterns, new_rhs); - } - - expr compile_skip(program const & prg) { - lean_assert(!head(prg.m_var_stack)); - auto new_stack = tail(prg.m_var_stack); - buffer new_eqs; - for (eqn const & e : prg.m_eqns) { - auto new_patterns = tail(e.m_patterns); - new_eqs.emplace_back(e.m_local_context, new_patterns, e.m_rhs); - } - return compile_core(program(prg, new_stack, to_list(new_eqs))); - } - - expr compile_variable(program const & prg) { - // The next pattern of every equation is a variable (or inaccessible term). - // Thus, we just rename them with the variable on - // the top of the variable stack. - // Remark: if the pattern is an inaccessible term, we just ignore it. - expr x = prg.get_var(*head(prg.m_var_stack)); - auto new_stack = tail(prg.m_var_stack); - buffer new_eqs; - for (eqn const & e : prg.m_eqns) { - expr p = head(e.m_patterns); - if (is_inaccessible(p)) { - new_eqs.emplace_back(e.m_local_context, tail(e.m_patterns), e.m_rhs); - } else { - lean_assert(is_local(p)); - if (contains_local(p, e.m_local_context)) { - list new_local_ctx = remove(e.m_local_context, p); - new_eqs.push_back(replace(eqn(e, new_local_ctx, tail(e.m_patterns)), p, x)); - } else { - new_eqs.emplace_back(eqn(e, e.m_local_context, tail(e.m_patterns))); - } - } - } - return compile_core(program(prg, new_stack, to_list(new_eqs))); - } - - class implementation : public inversion::implementation { - eqn m_eqn; - public: - implementation(eqn const & e):m_eqn(e) {} - - eqn const & get_eqn() const { return m_eqn; } - - virtual name const & get_constructor_name() const { - return const_name(get_app_fn(head(m_eqn.m_patterns))); - } - - virtual void update_exprs(std::function const & fn) { - m_eqn.m_local_context = map(m_eqn.m_local_context, fn); - m_eqn.m_patterns = map(m_eqn.m_patterns, fn); - m_eqn.m_rhs = fn(m_eqn.m_rhs); - } - }; - - // Wrap the equations from \c p as an "implementation_list" for the inversion package. - inversion::implementation_list to_implementation_list(program const & p) { - return map2(p.m_eqns, [&](eqn const & e) { - return std::shared_ptr(new implementation(e)); - }); - } - - // Convert program into a goal. We need that to be able to invoke the inversion package. - old_goal to_goal(program const & p) { - buffer hyps; - to_buffer(p.m_context, hyps); - expr new_type = p.m_type; - expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(hyps, new_type)), hyps); - return old_goal(new_meta, new_type); - } - - // Convert goal and implementation_list back into a program. - // - nvars is the number of new variables in the variable stack. - program to_program(expr const & fn, old_goal const & g, unsigned nvars, list> const & new_var_stack, - inversion::implementation_list const & imps) { - buffer new_context; - g.get_hyps(new_context); - expr new_type = g.get_type(); - buffer new_equations; - for (inversion::implementation_ptr const & imp : imps) { - eqn e = static_cast(imp.get())->get_eqn(); - buffer pat_args; - get_app_args(head(e.m_patterns), pat_args); - lean_assert(pat_args.size() >= nvars); - list new_pats = to_list(pat_args.end() - nvars, pat_args.end(), tail(e.m_patterns)); - new_equations.push_back(eqn(e.m_local_context, new_pats, e.m_rhs)); - } - return program(fn, to_list(new_context), new_var_stack, to_list(new_equations), new_type); - } - - /** \brief Compile constructor transition. - \remark if fail_if_subgoals is true, then it returns none if there are subgoals. - */ - optional compile_constructor_core(program const & p, bool fail_if_subgoals) { - expr h = p.get_var(*head(p.m_var_stack)); - old_goal g = to_goal(p); - auto imps = to_implementation_list(p); - bool clear_elim = false; - if (auto r = apply(env(), ios(), m_tc, g, h, imps, clear_elim)) { - substitution subst = r->m_subst; - list> args = r->m_args; - list rn_maps = r->m_renames; - list imps_list = r->m_implementation_lists; - if (fail_if_subgoals && r->m_goals) - return none_expr(); - for (old_goal const & new_g : r->m_goals) { - list> new_vars = map2>(head(args), - [](expr const & a) { - if (is_local(a)) - return optional(mlocal_name(a)); - else - return optional(); - }); - rename_map const & rn = head(rn_maps); - list> new_var_stack = map(tail(p.m_var_stack), - [&](optional const & n) -> optional { - if (n) - return optional(rn.find(*n)); - else - return n; - }); - list> new_case_stack = append(new_vars, new_var_stack); - program new_p = to_program(p.m_fn, new_g, length(new_vars), new_case_stack, head(imps_list)); - args = tail(args); - imps_list = tail(imps_list); - rn_maps = tail(rn_maps); - expr t = compile_core(new_p); - assign(subst, new_g, t); - } - expr t = subst.instantiate_all(g.get_meta()); - return some_expr(t); - } else { - throw_error(sstream() << "pattern matching failed"); - } - } - - expr compile_constructor(program const & p) { - bool fail_if_subgoals = false; - return *compile_constructor_core(p, fail_if_subgoals); - } - - expr compile_no_equations(program const & p) { - lean_assert(head(p.m_var_stack)); - expr const & x = p.get_var(*head(p.m_var_stack)); - expr const & I = get_app_fn(mlocal_type(x)); - lean_assert(is_constant(I) && inductive::is_inductive_decl(env(), const_name(I))); - /* If the head variable is a recursive datatype, then we want to fail if subgoals are generated. - Reason: avoid non-termination. */ - bool fail_if_subgoals = is_recursive_datatype(env(), const_name(I)); - if (auto r = compile_constructor_core(p, fail_if_subgoals)) - return *r; - else - return compile_variable(p); - } - - expr mk_constructor(name const & n, levels const & ls, buffer const & params, buffer & args) { - expr c = mk_app(mk_constant(n, ls), params); - expr t = infer_type(c); - to_telescope_ext(t, args); - return mk_app(c, args); - } - - expr compile_complete(program const & prg) { - // The next pattern of every equation is a constructor or variable. - // We split the equations where the next pattern is a variable into cases. - // That is, we are reducing this case to the compile_constructor case. - buffer new_eqns; - for (eqn const & e : prg.m_eqns) { - expr const & p = head(e.m_patterns); - if (is_local(p)) { - list rest_ctx = remove(e.m_local_context, p); - expr x = prg.get_var(*head(prg.m_var_stack)); - expr x_type = whnf(mlocal_type(x)); - buffer I_args; - expr const & I = get_app_args(x_type, I_args); - name const & I_name = const_name(I); - levels const & I_ls = const_levels(I); - unsigned nparams = *inductive::get_num_params(env(), I_name); - buffer I_params; - I_params.append(nparams, I_args.data()); - buffer constructor_names; - get_intro_rule_names(env(), I_name, constructor_names); - for (name const & c_name : constructor_names) { - buffer new_args; - expr c = mk_constructor(c_name, I_ls, I_params, new_args); - list new_ctx = to_list(new_args.begin(), new_args.end(), rest_ctx); - list new_patterns = cons(c, tail(e.m_patterns)); - new_eqns.push_back(replace(eqn(e, new_ctx, new_patterns), p, c)); - } - } else { - new_eqns.push_back(e); - } - } - return compile_core(program(prg, to_list(new_eqns))); - } - - [[ noreturn ]] void throw_non_exhaustive() { - program prg = m_init_prgs[m_prg_idx]; - throw_error(m_meta, [=](formatter const & _fmt) { - options opts = _fmt.get_options().update_if_undef(get_pp_implicit_name(), true); - opts = opts.update_if_undef(get_pp_purify_locals_name(), false); - formatter fmt = _fmt.update_options(opts); - format r = format("invalid non-exhaustive set of equations, " - "left-hand-side(s) after elaboration:"); - for (eqn const & e : prg.m_eqns) { - expr lhs = prg.m_fn; - for (expr const & p : e.m_patterns) lhs = mk_app(lhs, p); - r += pp_indent_expr(fmt, lhs); - r += line(); - } - return r; - }); - } - - expr compile_core(program const & p) { - lean_assert(check_program(p)); - // out() << "compile_core step\n"; - // display(p); - // out() << "------------------\n"; - if (p.m_var_stack) { - if (!head(p.m_var_stack)) { - return compile_skip(p); - } else if (is_no_equation_constructor_transition(p)) { - return compile_no_equations(p); - } else if (is_variable_transition(p)) { - return compile_variable(p); - } else if (is_constructor_transition(p)) { - return compile_constructor(p); - } else if (is_complete_transition(p)) { - return compile_complete(p); - } else { - // In some equations the next pattern is an inaccessible term, - // and in others it is a constructor. - throw_error(sstream() << "invalid equations for '" << local_pp_name(p.m_fn) - << "', inconsistent use of inaccessible term annotation, " - << "in some equations a pattern is a constructor, and in another it is an inaccessible term"); - } - } else { - if (p.m_eqns) { - // variable stack is empty - expr r = head(p.m_eqns).m_rhs; - lean_assert(is_def_eq(infer_type(r), p.m_type)); - return r; - } else { - throw_non_exhaustive(); - } - } - } - - expr compile_pat_match(program const & p, unsigned i) { - flet set(m_prg_idx, i); // we only use m_prg_idx for producing error messages - buffer vars; - to_buffer(p.m_context, vars); - if (!is_proof_irrelevant()) { - // We have to include the global context because the proof relevant version - // uses the class-instance resolution, and must be able to "see" the complete - // context. - program new_p(p, append(to_list(m_global_context), p.m_context)); - return Fun(vars, compile_core(new_p)); - } else { - return Fun(vars, compile_core(p)); - } - } - - /** \brief Return true iff \c e is one of the functions being defined */ - bool is_fn(expr const & e) const { - return is_local(e) && contains_local(e, m_fns); - } - - /** \brief Return true iff the equations are recursive. */ - bool is_recursive(buffer const & prgs) const { - lean_assert(!prgs.empty()); - for (program const & p : prgs) { - for (eqn const & e : p.m_eqns) { - if (find(e.m_rhs, [&](expr const & e, unsigned) { return is_fn(e); })) - return true; - } - } - if (prgs.size() > 1) - throw_error(sstream() << "mutual recursion is not needed when defining non-recursive functions"); - return false; - } - - /** \brief Return true if all locals are distinct local constants. */ - static bool all_distinct_locals(unsigned num, expr const * locals) { - for (unsigned i = 0; i < num; i++) { - if (!is_local(locals[i])) - return false; - if (contains_local(locals[i], locals, locals + i)) - return false; - } - return true; - } - - /** \brief Return true iff \c t is an inductive datatype (I A j) which constains an associated brec_on definition, - and all indices of t are in ctx. */ - bool is_rec_inductive(list const & ctx, expr const & t) const { - expr const & I = get_app_fn(t); - if (is_constant(I) && env().find(name{const_name(I), "brec_on"})) { - unsigned nindices = *inductive::get_num_indices(env(), const_name(I)); - if (nindices > 0) { - buffer args; - get_app_args(t, args); - lean_assert(args.size() >= nindices); - return - all_distinct_locals(nindices, args.end() - nindices) && - std::all_of(args.end() - nindices, args.end(), - [&](expr const & idx) { return contains_local(idx, ctx); }); - } else { - return true; - } - } else { - return false; - } - } - - /** \brief Return true iff t1 and t2 are inductive datatypes of the same mutually inductive declaration. */ - bool is_compatible_inductive(expr const & t1, expr const & t2) { - buffer args1, args2; - name const & I1 = const_name(get_app_args(t1, args1)); - name const & I2 = const_name(get_app_args(t2, args2)); - inductive::inductive_decl decl = *inductive::is_inductive_decl(env(), I1); - unsigned nparams = decl.m_num_params; - if (decl.m_name == I2) { - // parameters must be definitionally equal - unsigned i = 0; - for (; i < nparams; i++) { - if (!is_def_eq(args1[i], args2[i])) - break; - } - if (i == nparams) - return true; - } - return false; - } - - /** \brief Return true iff \c t1 and \c t2 are instances of the same inductive datatype */ - static bool is_same_inductive(expr const & t1, expr const & t2) { - return const_name(get_app_fn(t1)) == const_name(get_app_fn(t2)); - } - - /** \brief Return true iff \c s is structurally smaller than \c t OR equal to \c t */ - bool is_le(expr const & s, expr const & t) { - return is_def_eq(s, t) || is_lt(s, t); - } - - /** Return true iff \c s is structurally smaller than \c t */ - bool is_lt(expr s, expr const & t) { - s = whnf(s); - if (is_app(s)) { - expr const & s_fn = get_app_fn(s); - if (!is_constructor(s_fn)) - return is_lt(s_fn, t); // f < t ==> s := f a_1 ... a_n < t - } - buffer t_args; - expr const & t_fn = get_app_args(t, t_args); - if (!is_constructor(t_fn)) - return false; - return std::any_of(t_args.begin(), t_args.end(), [&](expr const & t_arg) { return is_le(s, t_arg); }); - } - - /** \brief Auxiliary functional object for checking whether recursive application are structurally smaller or not */ - struct check_rhs_fn { - equation_compiler_fn & m_main; - buffer const & m_prgs; - buffer const & m_arg_pos; - - check_rhs_fn(equation_compiler_fn & m, buffer const & prgs, buffer const & arg_pos): - m_main(m), m_prgs(prgs), m_arg_pos(arg_pos) {} - - /** \brief Return true iff all recursive applications in \c e are structurally smaller than \c arg. */ - bool check_rhs(expr const & e, expr const & arg) const { - switch (e.kind()) { - case expr_kind::Var: case expr_kind::Meta: - case expr_kind::Local: case expr_kind::Constant: - case expr_kind::Sort: - return true; - case expr_kind::Macro: - for (unsigned i = 0; i < macro_num_args(e); i++) - if (!check_rhs(macro_arg(e, i), arg)) - return false; - return true; - case expr_kind::App: { - buffer args; - expr const & fn = get_app_args(e, args); - if (!check_rhs(fn, arg)) - return false; - for (unsigned i = 0; i < args.size(); i++) - if (!check_rhs(args[i], arg)) - return false; - if (is_local(fn)) { - for (unsigned j = 0; j < m_prgs.size(); j++) { - if (mlocal_name(fn) == mlocal_name(m_prgs[j].m_fn)) { - // it is a recusive application - unsigned pos_j = m_arg_pos[j]; - if (pos_j < args.size()) { - expr const & arg_j = args[pos_j]; - // arg_j must be structurally smaller than arg - if (!m_main.is_lt(arg_j, arg)) - return false; - } else { - return false; - } - break; - } - } - } - return true; - } - case expr_kind::Let: - // TODO(Leo): improve - return check_rhs(instantiate(let_body(e), let_value(e)), arg); - case expr_kind::Lambda: - case expr_kind::Pi: - if (!check_rhs(binding_domain(e), arg)) { - return false; - } else { - expr l = mk_local(mk_fresh_name(), binding_name(e), binding_domain(e), binding_info(e)); - return check_rhs(instantiate(binding_body(e), l), arg); - } - } - lean_unreachable(); - } - - bool operator()(expr const & e, expr const & arg) const { - return check_rhs(e, arg); - } - }; - - /** \brief Return true iff the recursive equations in prgs are "admissible" with respect to - the following configuration of recursive arguments. - We say the equations are admissible when every recursive application of prgs[i] - is structurally smaller at arguments arg_pos[i]. - */ - bool check_rec_args(buffer const & prgs, buffer const & arg_pos) { - lean_assert(prgs.size() == arg_pos.size()); - check_rhs_fn check_rhs(*this, prgs, arg_pos); - for (unsigned i = 0; i < prgs.size(); i++) { - program const & prg = prgs[i]; - unsigned pos_i = arg_pos[i]; - for (eqn const & e : prg.m_eqns) { - expr const & p_i = get_ith(e.m_patterns, pos_i); - if (!check_rhs(e.m_rhs, p_i)) - return false; - } - } - return true; - } - - bool find_rec_args(buffer const & prgs, unsigned i, buffer & arg_pos, buffer & arg_types) { - if (i == prgs.size()) { - return check_rec_args(prgs, arg_pos); - } else { - program const & p = prgs[i]; - unsigned j = 0; - for (optional const & n : p.m_var_stack) { - lean_assert(n); - expr const & v = p.get_var(*n); - expr const & t = mlocal_type(v); - if (// argument must be an inductive datatype - is_rec_inductive(p.m_context, t) && - // argument must be an inductive datatype different from the ones in arg_types - std::all_of(arg_types.begin(), arg_types.end(), - [&](expr const & prev_type) { return !is_same_inductive(t, prev_type); }) && - // argument type must be in the same mutually recursive declaration of previous argument types - (arg_types.empty() || is_compatible_inductive(t, arg_types[0]))) { - // Found candidate - arg_pos.push_back(j); - arg_types.push_back(t); - if (find_rec_args(prgs, i+1, arg_pos, arg_types)) - return true; - arg_pos.pop_back(); - arg_types.pop_back(); - } - j++; - } - return false; - } - } - - bool find_rec_args(buffer const & prgs, buffer & arg_pos) { - buffer arg_types; - return find_rec_args(prgs, 0, arg_pos, arg_types); - } - - // Auxiliary function object used to eliminate recursive applications using "below" applications - struct elim_rec_apps_fn { - equation_compiler_fn & m_main; - buffer const & m_prgs; - unsigned m_nparams; - buffer const & m_below_cnsts; // below constants - buffer const & m_Cs_locals; // auxiliary local constants representing the "motives" - buffer const & m_rec_arg_pos; // position of recursive argument for each program - buffer> const & m_rest_pos; // position of remaining arguments for each program - - elim_rec_apps_fn(equation_compiler_fn & m, buffer const & prgs, unsigned nparams, - buffer const & below_cnsts, buffer const & Cs_locals, - buffer const & rec_arg_pos, buffer> const & rest_pos): - m_main(m), m_prgs(prgs), m_nparams(nparams), m_below_cnsts(below_cnsts), m_Cs_locals(Cs_locals), - m_rec_arg_pos(rec_arg_pos), m_rest_pos(rest_pos) {} - - bool is_below_type(expr const & t) const { - expr const & fn = get_app_fn(t); - return is_constant(fn) && std::find(m_below_cnsts.begin(), m_below_cnsts.end(), fn) != m_below_cnsts.end(); - } - - /** \brief Return the number of arguments in the left-hand-side of program prg_idx */ - unsigned get_lhs_size(unsigned prg_idx) const { return length(m_prgs[prg_idx].m_context); } - - expr whnf(expr const & e) { - return m_main.m_tc.whnf(e).first; - } - - bool is_def_eq(expr const & a, expr const & b) { - return m_main.m_tc.is_def_eq(a, b).first; - } - - /** \brief Retrieve \c a from the below dictionary \c d. \c d is a term made of products, and C's from (m_Cs_locals). - \c b is the below constant that was used to create the below dictionary \c d. - */ - optional to_below(expr const & d, expr const & a, expr const & b) { - expr const & fn = get_app_fn(d); - if (is_constant(fn) && const_name(fn) == get_prod_name()) { - expr d_arg1 = whnf(app_arg(app_fn(d))); - expr d_arg2 = whnf(app_arg(d)); - if (auto r = to_below(d_arg1, a, mk_pr1(m_main.m_tc, b))) - return r; - else if (auto r = to_below(d_arg2, a, mk_pr2(m_main.m_tc, b))) - return r; - else - return none_expr(); - } else if (is_constant(fn) && const_name(fn) == get_and_name()) { - // For ibelow, we use "and" instead of products - expr d_arg1 = whnf(app_arg(app_fn(d))); - expr d_arg2 = whnf(app_arg(d)); - if (auto r = to_below(d_arg1, a, mk_and_elim_left(m_main.m_tc, b))) - return r; - else if (auto r = to_below(d_arg2, a, mk_and_elim_right(m_main.m_tc, b))) - return r; - else - return none_expr(); - } else if (is_local(fn)) { - for (expr const & C : m_Cs_locals) { - if (mlocal_name(C) == mlocal_name(fn) && is_def_eq(app_arg(d), a)) - return some_expr(b); - } - return none_expr(); - } else if (is_pi(d)) { - if (is_app(a)) { - expr new_d = whnf(instantiate(binding_body(d), app_arg(a))); - return to_below(new_d, a, mk_app(b, app_arg(a))); - } else { - return none_expr(); - } - } else { - return none_expr(); - } - } - - expr elim(unsigned prg_idx, buffer const & args, expr const & below, tag g) { - // Replace motives with abstract ones. We use the abstract motives (m_Cs_locals) as "markers" - buffer below_args; - expr const & below_cnst = get_app_args(mlocal_type(below), below_args); - buffer abst_below_args; - abst_below_args.append(m_nparams, below_args.data()); - abst_below_args.append(m_Cs_locals); - for (unsigned i = m_nparams + m_Cs_locals.size(); i < below_args.size(); i++) - abst_below_args.push_back(below_args[i]); - expr abst_below = mk_app(below_cnst, abst_below_args); - expr below_dict = whnf(abst_below); - expr rec_arg = whnf(args[m_rec_arg_pos[prg_idx]]); - unsigned lhs_size = get_lhs_size(prg_idx); - if (optional b = to_below(below_dict, rec_arg, below)) { - expr r = *b; - for (unsigned rest_pos : m_rest_pos[prg_idx]) { - if (rest_pos < args.size()) - r = mk_app(r, args[rest_pos], g); - } - for (unsigned i = lhs_size; i < args.size(); i++) { - r = mk_app(r, args[i], g); - } - return r; - } else { - m_main.throw_error(sstream() << "failed to compile equations using " - << "brec_on approach (possible solution: use well-founded recursion)"); - } - } - - /** \brief Return true iff all recursive applications in \c e are structurally smaller than \c arg. */ - expr elim(expr const & e, optional const & b) { - switch (e.kind()) { - case expr_kind::Var: case expr_kind::Meta: - case expr_kind::Local: case expr_kind::Constant: - case expr_kind::Sort: - return e; - case expr_kind::Macro: { - buffer new_args; - for (unsigned i = 0; i < macro_num_args(e); i++) - new_args.push_back(elim(macro_arg(e, i), b)); - return update_macro(e, new_args.size(), new_args.data()); - } - case expr_kind::App: { - buffer args; - expr const & fn = get_app_args(e, args); - expr new_fn = elim(fn, b); - buffer new_args; - for (expr const & arg : args) - new_args.push_back(elim(arg, b)); - if (is_local(fn) && b) { - for (unsigned j = 0; j < m_prgs.size(); j++) { - if (mlocal_name(fn) == mlocal_name(m_prgs[j].m_fn)) { - return elim(j, new_args, *b, e.get_tag()); - } - } - } - return mk_app(new_fn, new_args, e.get_tag()); - } - case expr_kind::Lambda: { - expr local = mk_local(mk_fresh_name(), binding_name(e), binding_domain(e), binding_info(e)); - expr body = instantiate(binding_body(e), local); - expr new_body; - if (is_below_type(binding_domain(e))) - new_body = elim(body, some_expr(local)); - else - new_body = elim(body, b); - return copy_tag(e, Fun(local, new_body)); - } - case expr_kind::Pi: { - expr new_domain = elim(binding_domain(e), b); - expr local = mk_local(mk_fresh_name(), binding_name(e), new_domain, binding_info(e)); - expr new_body = elim(instantiate(binding_body(e), local), b); - return copy_tag(e, Pi(local, new_body)); - } - case expr_kind::Let: { - // TODO(Leo): improve - return elim(instantiate(let_body(e), let_value(e)), b); - }} - lean_unreachable(); - } - - expr operator()(expr const & e) { - return elim(e, none_expr()); - } - }; - - // Fix the i-th argument in the Pi-type t - expr fix_fn_type(expr const & t, unsigned i, expr const & p) { - if (!is_pi(t)) { - throw_error(sstream() << "invalid equation, failed to move parameter '" << p << "'"); - } else if (i == 0) { - return instantiate(binding_body(t), p); - } else { - expr local = mk_local(mk_fresh_name(), binding_name(t), binding_domain(t), binding_info(t)); - expr body = fix_fn_type(instantiate(binding_body(t), local), i-1, p); - return Pi(local, body); - } - } - - // For each function application (fn ...) in e, replace it with (new_fn ...) and remove the i-th - // argument. - expr fix_rec_arg(expr const & fn, expr const & new_fn, unsigned i, expr const & e) { - return ::lean::replace(e, [&](expr const & e) { - if (is_app(e) && get_app_fn(e) == fn) { - buffer args; - get_app_args(e, args); - if (i < args.size()) - args.erase(i); - return some_expr(mk_app(new_fn, args)); - } else { - return none_expr(); - } - }); - } - - // Move inductive datatype parameters occuring in prg to m_additional_context - pair move_params(program const & prg, unsigned arg_pos) { - expr const & a_type = mlocal_type(get_ith(prg.m_context, arg_pos)); - buffer a_type_args; - expr const & I = get_app_args(a_type, a_type_args); - unsigned nparams = *inductive::get_num_params(env(), const_name(I)); - buffer params; - params.append(nparams, a_type_args.data()); - if (std::all_of(params.begin(), params.end(), - [&](expr const & p) { return !is_local(p) || contains_local(p, m_global_context); })) { - return mk_pair(prg, arg_pos); - } else { - list new_context = prg.m_context; - buffer> new_var_stack; - buffer new_eqns; - to_buffer(prg.m_var_stack, new_var_stack); - to_buffer(prg.m_eqns, new_eqns); - expr new_fn = prg.m_fn; - for (expr const & param : params) { - if (contains_local(param, m_global_context)) - continue; // parameter doesn't need to be moved - m_additional_context.push_back(param); - new_context = remove(new_context, param); - unsigned i = 0; - for (; i < new_var_stack.size(); i++) { - if (*new_var_stack[i] == mlocal_name(param)) - break; - } - lean_assert(i < new_var_stack.size()); - lean_assert(i != arg_pos); - expr new_fn_type = fix_fn_type(mlocal_type(new_fn), i, param); - expr new_new_fn = update_mlocal(new_fn, new_fn_type); - - if (i < arg_pos) - arg_pos--; - new_var_stack.erase(i); - for (eqn & e : new_eqns) { - expr const & p = get_ith(e.m_patterns, i); - if (!is_local(p)) { - throw_error(sstream() << "invalid equations, " - << "trying to pattern match inductive datatype parameter '" << p << "'"); - } else { - list new_local_ctx = remove(e.m_local_context, p); - list new_patterns = remove_ith(e.m_patterns, i); - expr new_rhs = fix_rec_arg(new_fn, new_new_fn, i, e.m_rhs); - e = replace(eqn(new_local_ctx, new_patterns, new_rhs), p, param); - } - } - new_fn = new_new_fn; - } - return mk_pair(program(new_fn, new_context, to_list(new_var_stack), to_list(new_eqns), prg.m_type), arg_pos); - } - } - - // Move inductive datatype parameters occuring in prg to m_additional_context - void move_params(buffer & prgs, buffer & arg_pos) { - if (prgs.size() != 1) { - // The parameters already occur in m_global_context when there is more than one program. - return; - } - auto p = move_params(prgs[0], arg_pos[0]); - prgs[0] = p.first; - arg_pos[0] = p.second; - lean_assert(check_program(prgs[0])); - } - - expr compile_brec_on_core(buffer const & prgs, buffer const & arg_pos) { - // Return the recursive argument of the i-th program - auto get_rec_arg = [&](unsigned i) -> expr { - program const & pi = prgs[i]; - return get_ith(pi.m_context, arg_pos[i]); - }; - - // Return the type of the recursive argument of the i-th program - auto get_rec_type = [&](unsigned i) -> expr { - return mlocal_type(get_rec_arg(i)); - }; - - // Return the program associated with the inductive datatype named I_name. - // Return none if there isn't one. - auto get_prg_for = [&](name const & I_name) -> optional { - for (unsigned i = 0; i < prgs.size(); i++) { - expr const & t = get_rec_type(i); - if (const_name(get_app_fn(t)) == I_name) - return optional(i); - } - return optional(); - }; - - expr const & a0_type = get_rec_type(0); - lean_assert(is_rec_inductive(prgs[0].m_context, a0_type)); - buffer a0_type_args; - expr const & I0 = get_app_args(a0_type, a0_type_args); - inductive::inductive_decl decl = *inductive::is_inductive_decl(env(), const_name(I0)); - unsigned nparams = decl.m_num_params; - buffer params; - params.append(nparams, a0_type_args.data()); - - // Return true if the local constant l is in the buffer b. - // This is similar to contains_local, but b may contain arbitrary terms - auto contains_local_at = [&](expr const & l, buffer const & b) { - lean_assert(is_mlocal(l)); - for (expr const & e : b) { - if (is_local(e) && mlocal_name(l) == mlocal_name(e)) - return true; - } - return false; - }; - - // Distribute parameters of the ith program intro three groups: - // indices, major premise (arg), and remaining arguments (rest) - // We store the position of the rest arguments in the buffer rest_pos. - // The buffer rest_pos is used to replace the recursive applications with below applications. - auto distribute_context_core = [&](unsigned i, buffer & indices, expr & arg, buffer & rest, - buffer & indices_pos, buffer & rest_pos) { - program const & p = prgs[i]; - arg = get_rec_arg(i); - list const & ctx = p.m_context; - buffer arg_args; - get_app_args(mlocal_type(arg), arg_args); - lean_assert(nparams <= arg_args.size()); - indices.append(arg_args.size() - nparams, arg_args.data() + nparams); - unsigned j = 0; - for (expr const & l : ctx) { - if (mlocal_name(l) == mlocal_name(arg) || contains_local_at(l, params)) { - // do nothing - } else if (contains_local_at(l, indices)) { - indices_pos.push_back(j); - } else { - rest.push_back(l); - rest_pos.push_back(j); - } - j++; - } - }; - - auto distribute_context = [&](unsigned i, buffer & indices, expr & arg, buffer & rest) { - buffer indices_pos, rest_pos; - distribute_context_core(i, indices, arg, rest, indices_pos, rest_pos); - }; - - // Compute the resulting universe level for brec_on - auto get_brec_on_result_level = [&]() -> level { - buffer indices, rest; expr arg; - distribute_context(0, indices, arg, rest); - expr r_type = Pi(rest, prgs[0].m_type); - return sort_level(m_tc.ensure_type(r_type).first); - }; - - level rlvl = get_brec_on_result_level(); - bool reflexive = env().prop_proof_irrel() && is_reflexive_datatype(m_tc.get_type_context(), const_name(I0)); - bool use_ibelow = reflexive && is_zero(rlvl); - if (reflexive) { - if (!is_zero(rlvl) && !is_not_zero(rlvl)) - throw_error(sstream() << "invalid equations, " - << "when trying to recurse over reflexive inductive datatype, " - << "the universe level of the resultant universe must be zero OR " - << "not zero for every level assignment"); - if (!is_zero(rlvl)) { - // For reflexive type, the type of brec_on and ibelow perform a +1 on the motive universe. - // Example: for a reflexive formula type, we have: - // formula.below.{l_1} : Π {C : formula → Type.{l_1+1}}, formula → Type.{max (l_1+1) 1} - if (auto dlvl = dec_level(rlvl)) { - rlvl = *dlvl; - } else { - throw_error(sstream() << "invalid equations, " - << "when trying to recurse over reflexive inductive datatype, " - << "the universe level of the resultant universe must be zero OR " - << "not zero for every level assignment, " - << "the compiler managed to establish that the resultant " - << "universe level L is never zero, but fail to comput L-1"); - } - } - } - levels brec_on_lvls; - expr brec_on; - if (use_ibelow) { - brec_on_lvls = const_levels(I0); - brec_on = mk_constant(name{const_name(I0), "binduction_on"}, brec_on_lvls); - } else { - brec_on_lvls = cons(rlvl, const_levels(I0)); - brec_on = mk_constant(name{const_name(I0), "brec_on"}, brec_on_lvls); - } - // add parameters - brec_on = mk_app(brec_on, params); - - buffer Cs; // brec_on "motives" - // The following loop fills Cs_locals with auxiliary local constants that will be used to - // convert recursive applications into "below applications". - // These constants are essentially abstracting Cs. - buffer Cs_locals; - buffer> C_args_buffer; - - name const & I_name = decl.m_name; - expr C; - C_args_buffer.push_back(buffer()); - buffer & C_args = C_args_buffer.back(); - expr C_type = whnf(infer_type(brec_on)); - expr C_local = mk_local(mk_fresh_name(), "C", C_type, binder_info()); - Cs_locals.push_back(C_local); - if (optional p_idx = get_prg_for(I_name)) { - buffer indices, rest; expr arg; - distribute_context(*p_idx, indices, arg, rest); - expr type = Pi(rest, prgs[*p_idx].m_type); - C_args.append(indices); - C_args.push_back(arg); - C = Fun(C_args, type); - } else { - expr d = binding_domain(C_type); - expr unit = mk_constant(get_poly_unit_name(), to_list(rlvl)); - to_telescope_ext(d, C_args); - C = Fun(C_args, unit); - } - brec_on = mk_app(brec_on, C); - Cs.push_back(C); - - // add indices and major - buffer indices0, rest0; expr arg0; - distribute_context(0, indices0, arg0, rest0); - brec_on = mk_app(mk_app(brec_on, indices0), arg0); - - // add functionals - unsigned i = 0; - buffer below_cnsts; - buffer> rest_arg_pos; - - expr below_cnst; - if (use_ibelow) - below_cnst = mk_constant(name{I_name, "ibelow"}, brec_on_lvls); - else - below_cnst = mk_constant(name{I_name, "below"}, brec_on_lvls); - below_cnsts.push_back(below_cnst); - expr below = mk_app(mk_app(below_cnst, params), Cs); - expr F; - rest_arg_pos.push_back(buffer()); - if (optional p_idx = get_prg_for(I_name)) { - program const & prg_i = prgs[*p_idx]; - buffer indices, rest; expr arg; buffer indices_pos; - buffer & rest_pos = rest_arg_pos.back(); - distribute_context_core(*p_idx, indices, arg, rest, indices_pos, rest_pos); - below = mk_app(mk_app(below, indices), arg); - expr b = mk_local(mk_fresh_name(), "b", below, binder_info()); - buffer new_ctx; - new_ctx.append(indices); - new_ctx.push_back(arg); - new_ctx.push_back(b); - new_ctx.append(rest); - F = compile_pat_match(program(prg_i, to_list(new_ctx)), *p_idx); - } else { - expr star = mk_constant(get_poly_unit_star_name(), to_list(rlvl)); - buffer F_args; - F_args.append(C_args); - below = mk_app(below, F_args); - F_args.push_back(mk_local(mk_fresh_name(), "b", below, binder_info())); - F = Fun(F_args, star); - } - brec_on = mk_app(brec_on, F); - i++; - expr r = elim_rec_apps_fn(*this, prgs, nparams, below_cnsts, Cs_locals, arg_pos, rest_arg_pos)(brec_on); - // add remaining arguments - r = mk_app(r, rest0); - - buffer ctx0_buffer; - to_buffer(prgs[0].m_context, ctx0_buffer); - r = Fun(m_additional_context, Fun(ctx0_buffer, r)); - return r; - } - - expr compile_brec_on(buffer & prgs) { - lean_assert(!prgs.empty()); - buffer arg_pos; - if (!find_rec_args(prgs, arg_pos)) { - throw_error(sstream() << "invalid equations, " - << "failed to find recursive arguments that are structurally smaller " - << "(possible solution: use well-founded recursion)"); - } - move_params(prgs, arg_pos); - buffer rs; - for (unsigned i = 0; i < prgs.size(); i++) { - if (i > 0) - rs.push_back(mlocal_type(prgs[i].m_fn)); - // Remark: this loop is very hackish. - // We are "compiling" the code prgs.size() times! - // This is wasteful. We should rewrite this. - std::swap(prgs[0], prgs[i]); - std::swap(arg_pos[0], arg_pos[i]); - rs.push_back(compile_brec_on_core(prgs, arg_pos)); - std::swap(prgs[0], prgs[i]); - std::swap(arg_pos[0], arg_pos[i]); - } - - if (rs.size() > 1) - return mk_equations_result(rs.size(), rs.data()); - else - return rs[0]; - } - - expr compile_wf(buffer & /* prgs */) { - // TODO(Leo) - return expr(); - } - - -public: - equation_compiler_fn(old_type_checker & tc, io_state const & ios, expr const & meta, expr const & meta_type): - m_tc(tc), m_ios(ios), m_meta(meta), m_meta_type(meta_type) { - get_app_args(m_meta, m_global_context); - } - - expr operator()(expr eqns) { - check_limitations(eqns); - buffer prgs; - initialize(eqns, prgs); - m_init_prgs.append(prgs); - if (is_recursive(prgs)) { - if (is_wf_equations(eqns)) { - return compile_wf(prgs); - } else { - return compile_brec_on(prgs); - } - } else { - lean_assert(prgs.size() == 1); - return compile_pat_match(prgs[0], 0); - } - } -}; - -expr compile_equations(old_type_checker & tc, io_state const & ios, expr const & eqns, - expr const & meta, expr const & meta_type) { - return equation_compiler_fn(tc, ios, meta, meta_type)(eqns); -} -} diff --git a/src/library/equations_compiler/old_compiler.h b/src/library/equations_compiler/old_compiler.h deleted file mode 100644 index 64f5f868bf..0000000000 --- a/src/library/equations_compiler/old_compiler.h +++ /dev/null @@ -1,12 +0,0 @@ -/* -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "library/equations_compiler/equations.h" -namespace lean { -expr compile_equations(old_type_checker & tc, io_state const & ios, expr const & eqns, - expr const & meta, expr const & meta_type); -} diff --git a/src/library/equations_compiler/old_goal.cpp b/src/library/equations_compiler/old_goal.cpp deleted file mode 100644 index 9856ade81a..0000000000 --- a/src/library/equations_compiler/old_goal.cpp +++ /dev/null @@ -1,182 +0,0 @@ -/* -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include "util/buffer.h" -#include "util/sstream.h" -#include "util/sexpr/option_declarations.h" -#include "kernel/replace_fn.h" -#include "kernel/for_each_fn.h" -#include "kernel/abstract.h" -#include "kernel/type_checker.h" -#include "library/metavar.h" -#include "library/util.h" -#include "library/old_util.h" -#include "library/equations_compiler/old_goal.h" - -namespace lean { -old_local_context old_goal::to_local_context() const { - buffer hyps; - get_hyps(hyps); - std::reverse(hyps.begin(), hyps.end()); - return old_local_context(to_list(hyps)); -} - -format old_goal::pp(formatter const & fmt) const { - return pp(fmt, substitution()); -} - -format old_goal::pp(formatter const & fmt, substitution const & s) const { - buffer hyps; - get_app_args(m_meta, hyps); - return format_goal(fmt, hyps, m_type, s); -} - -expr old_goal::abstract(expr const & v) const { - buffer locals; - get_app_args(m_meta, locals); - return Fun(locals, v); -} - -expr old_goal::mk_meta(name const & n, expr const & type) const { - buffer locals; - expr this_mvar = get_app_args(m_meta, locals); - expr mvar = copy_tag(this_mvar, mk_metavar(n, Pi(locals, type))); - return copy_tag(m_meta, mk_app(mvar, locals)); -} - -old_goal old_goal::instantiate(substitution const & s) const { - substitution s1(s); - return old_goal(s1.instantiate_all(m_meta), s1.instantiate_all(m_type)); -} - -static bool validate_locals(expr const & r, unsigned num_locals, expr const * locals) { - bool failed = false; - for_each(r, [&](expr const & e, unsigned) { - if (!has_local(e) || failed) return false; - if (is_local(e) && - !std::any_of(locals, locals + num_locals, - [&](expr const & l) { return mlocal_name(l) == mlocal_name(e); })) { - failed = true; - return false; - } - return true; - }); - return !failed; -} - -bool old_goal::validate_locals() const { - buffer locals; - get_app_args(m_meta, locals); - if (!::lean::validate_locals(m_type, locals.size(), locals.data())) - return false; - unsigned i = locals.size(); - while (i > 0) { - --i; - if (!::lean::validate_locals(mlocal_type(locals[i]), i, locals.data())) - return false; - } - return true; -} - -bool old_goal::validate(environment const & env) const { - if (validate_locals()) { - old_type_checker tc(env); - return tc.is_def_eq(tc.check(m_meta).first, m_type).first; - } else { - return false; - } -} - -list old_goal::to_context() const { - buffer locals; - get_app_rev_args(m_meta, locals); - return to_list(locals.begin(), locals.end()); -} - -template -static optional> find_hyp_core(expr const & meta, F && pred) { - expr const * it = &meta; - unsigned i = 0; - while (is_app(*it)) { - expr const & h = app_arg(*it); - if (pred(h)) - return some(mk_pair(h, i)); - i++; - it = &app_fn(*it); - } - return optional>(); -} - -optional> old_goal::find_hyp(name const & uname) const { - return find_hyp_core(m_meta, [&](expr const & h) { return local_pp_name(h) == uname; }); -} - -optional> old_goal::find_hyp_from_internal_name(name const & n) const { - return find_hyp_core(m_meta, [&](expr const & h) { return mlocal_name(h) == n; }); -} - -void old_goal::get_hyps(buffer & r) const { - get_app_args(m_meta, r); -} - -void assign(substitution & s, old_goal const & g, expr const & v) { - buffer hyps; - expr const & mvar = get_app_args(g.get_meta(), hyps); - s.assign(mvar, hyps, v); -} - -static bool uses_name(name const & n, buffer const & locals) { - for (expr const & local : locals) { - if (is_local(local) && local_pp_name(local) == n) - return true; - } - return false; -} - -name get_unused_name(name const & prefix, unsigned & idx, buffer const & locals) { - while (true) { - name curr = prefix.append_after(idx); - idx++; - if (!uses_name(curr, locals)) - return curr; - } -} - -name get_unused_name(name const & prefix, buffer const & locals) { - if (!uses_name(prefix, locals)) - return prefix; - unsigned idx = 1; - return get_unused_name(prefix, idx, locals); -} - -name get_unused_name(name const & prefix, unsigned & idx, expr const & meta) { - buffer locals; - get_app_rev_args(meta, locals); - return get_unused_name(prefix, idx, locals); -} - -name get_unused_name(name const & prefix, expr const & meta) { - buffer locals; - get_app_rev_args(meta, locals); - return get_unused_name(prefix, locals); -} - -name old_goal::get_unused_name(name const & prefix, unsigned & idx) const { - return ::lean::get_unused_name(prefix, idx, m_meta); -} - -name old_goal::get_unused_name(name const & prefix) const { - return ::lean::get_unused_name(prefix, m_meta); -} - -io_state_stream const & operator<<(io_state_stream const & out, old_goal const & g) { - options const & opts = out.get_options(); - out.get_stream() << mk_pair(g.pp(out.get_formatter()), opts); - return out; -} -} diff --git a/src/library/equations_compiler/old_goal.h b/src/library/equations_compiler/old_goal.h deleted file mode 100644 index ff8712fed2..0000000000 --- a/src/library/equations_compiler/old_goal.h +++ /dev/null @@ -1,113 +0,0 @@ -/* -Copyright (c) 2016 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 "util/list.h" -#include "util/name.h" -#include "kernel/formatter.h" -#include "kernel/environment.h" -#include "library/io_state_stream.h" -#include "library/old_local_context.h" - -namespace lean { -/** - \brief A goal is just encoding the synthesis problem (?m l_1 .... l_n) : t - That is, we want to find a term \c ?m s.t. (?m l_1 ... l_n) has type \c t - The terms \c l_i are just local constants. - - We can convert any metavariable - ?m : Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), B[x_1, ..., x_n] - into a goal by simply creating the local constants - l_1 : A_1, ..., l_n : A_n[l_1, ..., l_{n-1}] - and then, create the goal - ?m l_1 ... l_n : B[l_1, ..., l_n] - Now, suppose we find a term \c b with type B[l_1, ... l_n], then we can simply - find \c ?m by abstracting l_1, ..., l_n - - We can check whether a goal is well formed in an environment by type checking. -*/ -class old_goal { - expr m_meta; - expr m_type; -public: - old_goal() {} - old_goal(expr const & m, expr const & t):m_meta(m), m_type(t) {} - - expr const & get_meta() const { return m_meta; } - expr const & get_type() const { return m_type; } - - name get_name() const { return mlocal_name(get_app_fn(m_meta)); } - - expr get_mvar() const { return get_app_fn(m_meta); } - - /** \brief Given a term \c v with type get_type(), build a lambda abstraction - that is the solution for the metavariable associated with this old_goal. - */ - expr abstract(expr const & v) const; - - /** \brief Create a metavariable application (?m l_1 ... l_n) with the given type, - and the locals from this old_goal. - */ - expr mk_meta(name const & m, expr const & type) const; - - /** \brief Return true iff get_type() only contains local constants that arguments - of get_meta(), and each argument of get_meta() only contains local constants - that are previous arguments. - */ - bool validate_locals() const; - - /** \brief Return true iff \c validate_locals() return true and type of \c get_meta() in - \c env is get_type() - */ - bool validate(environment const & env) const; - - /** \brief Return the old_goal's "context". - That is, given ?m l_1 ... l_n, return the list - [l_n, ..., l_1] - */ - list to_context() const; - - old_local_context to_local_context() const; - - /** \brief Apply given substitution to old_goal */ - old_goal instantiate(substitution const & s) const; - - /** \brief Return hypothesis (and its position) with "user name" uname (i.e., local_pp_name). - - \remark The position is right to left. In the following old_goal (Ha is 2), (Hb is 1) and (Hc is 0): - - Ha : a, Hb : b, Hc : c |- P - */ - optional> find_hyp(name const & uname) const; - - /** \brief Similar to find_hyp but use internal name */ - optional> find_hyp_from_internal_name(name const & hname) const; - - /** \brief Store hypotheses in the given buffer. - - \remark The hypotheses are stored from left to right. - */ - void get_hyps(buffer & r) const; - - /** \brief Return a "user" name that is not used by any local constant in the given old_goal */ - name get_unused_name(name const & prefix, unsigned & idx) const; - - name get_unused_name(name const & prefix) const; - - format pp(formatter const & fmt, substitution const & s) const; - format pp(formatter const & fmt) const; -}; - -void assign(substitution & s, old_goal const & g, expr const & v); - -name get_unused_name(name const & prefix, unsigned & idx, buffer const & locals); -name get_unused_name(name const & prefix, buffer const & locals); -name get_unused_name(name const & prefix, unsigned & idx, expr const & meta); -name get_unused_name(name const & prefix, expr const & meta); - -io_state_stream const & operator<<(io_state_stream const & out, old_goal const & g); -} diff --git a/src/library/equations_compiler/old_inversion.cpp b/src/library/equations_compiler/old_inversion.cpp deleted file mode 100644 index bb265510d4..0000000000 --- a/src/library/equations_compiler/old_inversion.cpp +++ /dev/null @@ -1,1102 +0,0 @@ -/* -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include "util/sstream.h" -#include "util/fresh_name.h" -#include "kernel/abstract.h" -#include "kernel/instantiate.h" -#include "kernel/inductive/inductive.h" -#include "kernel/error_msgs.h" -#include "library/io_state_stream.h" -#include "library/locals.h" -#include "library/util.h" -#include "library/constants.h" -#include "library/reducible.h" -#include "library/class_instance_resolution.h" -#include "library/equations_compiler/old_inversion.h" - -namespace lean { -namespace inversion { -result::result(list const & gs, list> const & args, list const & imps, - list const & rs, substitution const & subst): - m_goals(gs), m_args(args), m_implementation_lists(imps), - m_renames(rs), m_subst(subst) { - lean_assert_eq(length(m_goals), length(m_args)); - lean_assert_eq(length(m_goals), length(m_implementation_lists)); - lean_assert_eq(length(m_goals), length(m_renames)); -} -} - -/** - \brief Given eq_rec of the form @eq.rec.{l₂ l₁} A a (λ (a' : A) (h : a = a'), B a') b a p, - apply the eq_rec_eq definition to produce the equality - - b = @eq.rec.{l₂ l₁} A a (λ (a' : A) (h : a = a'), B a') b a p - - The eq_rec_eq definition is of the form - - definition eq_rec_eq.{l₁ l₂} {A : Type.{l₁}} {B : A → Type.{l₂}} [h : is_set A] {a : A} (b : B a) (p : a = a) : - b = @eq.rec.{l₂ l₁} A a (λ (a' : A) (h : a = a'), B a') b a p := - ... -*/ -optional apply_eq_rec_eq(old_type_checker & tc, io_state const & ios, list const & ctx, expr const & eq_rec) { - buffer args; - expr const & eq_rec_fn = get_app_args(eq_rec, args); - if (args.size() != 6) - return none_expr(); - expr const & p = args[5]; - if (!is_local(p) || !is_eq_a_a(tc, mlocal_type(p))) - return none_expr(); - expr const & A = args[0]; - auto is_set_A = mk_set_instance(tc, ios.get_options(), ctx, A); - if (!is_set_A) - return none_expr(); - levels ls = const_levels(eq_rec_fn); - level l2 = head(ls); - level l1 = head(tail(ls)); - expr C = tc.whnf(args[2]).first; - if (!is_lambda(C)) - return none_expr(); - expr a1 = mk_local(mk_fresh_name(), binding_domain(C)); - C = tc.whnf(instantiate(binding_body(C), a1)).first; - if (!is_lambda(C)) - return none_expr(); - C = binding_body(C); - if (!closed(C)) - return none_expr(); - expr B = Fun(a1, C); - expr a = args[1]; - expr b = args[3]; - expr r = mk_constant(get_eq_rec_eq_name(), {l1, l2}); - return some_expr(mk_app({r, A, B, *is_set_A, a, b, p})); -} - -typedef inversion::implementation_ptr implementation_ptr; -typedef inversion::implementation_list implementation_list; - -static void replace(implementation_list const & imps, unsigned sz, expr const * from, expr const * to) { - lean_assert(std::all_of(from, from+sz, is_local)); - for (implementation_ptr const & imp : imps) { - imp->update_exprs([&](expr const & e) { - return instantiate_rev(abstract_locals(e, sz, from), sz, to); - }); - } -} - -static void replace(implementation_list const & imps, buffer const & from, buffer const & to) { - lean_assert(from.size() == to.size()); - return replace(imps, from.size(), from.data(), to.data()); -} - -static void replace(implementation_list const & imps, expr const & from, expr const & to) { - return replace(imps, 1, &from, &to); -} - -class inversion_tac { - environment const & m_env; - io_state const & m_ios; - old_type_checker & m_tc; - list m_ids; - substitution m_subst; - - bool m_dep_elim; - bool m_proof_irrel; - unsigned m_nparams; - unsigned m_nindices; - unsigned m_nminors; - declaration m_I_decl; - declaration m_cases_on_decl; - - bool m_clear_elim; // if true, then clear eliminated variables - - expr whnf(expr const & e) { return m_tc.whnf(e).first; } - expr infer_type(expr const & e) { return m_tc.infer(e).first; } - - void init_inductive_info(name const & n) { - m_dep_elim = inductive::has_dep_elim(m_env, n); - m_nindices = *inductive::get_num_indices(m_env, n); - m_nparams = *inductive::get_num_params(m_env, n); - // This tactic is bases on cases_on construction which only has - // minor premises for the introduction rules of this datatype. - // For non-mutually recursive datatypes inductive::get_num_intro_rules == inductive::get_num_minor_premises - m_nminors = *inductive::get_num_intro_rules(m_env, n); - m_I_decl = m_env.get(n); - m_cases_on_decl = m_env.get({n, "cases_on"}); - } - - bool is_inversion_applicable(expr const & t) { - buffer args; - expr const & fn = get_app_args(t, args); - if (!is_constant(fn)) - return false; - if (!inductive::is_inductive_decl(m_env, const_name(fn))) - return false; - if (!m_env.find(name{const_name(fn), "cases_on"}) || !m_env.find(get_eq_name())) - return false; - if (m_proof_irrel && !m_env.find(get_heq_name())) - return false; - init_inductive_info(const_name(fn)); - if (args.size() != m_nindices + m_nparams) - return false; - return true; - } - - pair mk_eq(expr const & lhs, expr const & rhs) { - expr lhs_type = infer_type(lhs); - expr rhs_type = infer_type(rhs); - level l = sort_level(m_tc.ensure_type(lhs_type).first); - constraint_seq cs; - if (m_tc.is_def_eq(lhs_type, rhs_type, justification(), cs) && !cs) { - return mk_pair(mk_app(mk_constant(get_eq_name(), to_list(l)), lhs_type, lhs, rhs), - mk_app(mk_constant(get_eq_refl_name(), to_list(l)), lhs_type, lhs)); - } else { - return mk_pair(mk_app(mk_constant(get_heq_name(), to_list(l)), lhs_type, lhs, rhs_type, rhs), - mk_app(mk_constant(get_heq_refl_name(), to_list(l)), lhs_type, lhs)); - } - } - - void assign(old_goal const & g, expr const & val) { - ::lean::assign(m_subst, g, val); - } - - /** \brief We say h has independent indices IF - 1- it is *not* an indexed inductive family, OR - 2- it is an indexed inductive family, but all indices are distinct local constants, - and all hypotheses of g different from h and indices, do not depend on the indices. - 3- if not m_dep_elim, then the conclusion does not depend on the indices. - */ - bool has_indep_indices(old_goal const & g, expr const & h, expr const & h_type) { - if (m_nindices == 0) - return true; - buffer args; - get_app_args(h_type, args); - lean_assert(m_nindices <= args.size()); - unsigned fidx = args.size() - m_nindices; - for (unsigned i = fidx; i < args.size(); i++) { - if (!is_local(args[i])) - return false; // the indices must be local constants - for (unsigned j = 0; j < i; j++) { - if (is_local(args[j]) && mlocal_name(args[j]) == mlocal_name(args[i])) - return false; // the indices must be distinct local constants - } - } - if (!m_dep_elim) { - expr const & g_type = g.get_type(); - if (depends_on(g_type, h)) - return false; - } - buffer hyps; - g.get_hyps(hyps); - for (expr const & h1 : hyps) { - if (mlocal_name(h1) == mlocal_name(h)) - continue; - if (std::any_of(args.end() - m_nindices, args.end(), - [&](expr const & arg) { return mlocal_name(arg) == mlocal_name(h1); })) - continue; - // h1 is not h nor any of the indices - // Thus, it must not depend on the indices - if (depends_on_any(h1, m_nindices, args.end() - m_nindices)) - return false; - } - return true; - } - - /** \brief Split hyps into two "telescopes". - - non_deps : hypotheses that do not depend on H - - deps : hypotheses that depend on H (directly or indirectly) - */ - void split_deps(buffer const & hyps, expr const & H, buffer & non_deps, buffer & deps, - bool clear_H = false) { - for (expr const & hyp : hyps) { - expr const & hyp_type = mlocal_type(hyp); - if (depends_on(hyp_type, H) || depends_on_any(hyp_type, deps)) { - deps.push_back(hyp); - } else if (hyp != H || !clear_H) { - non_deps.push_back(hyp); - } - } - } - - /** \brief Given a old_goal of the form - - Ctx, h : I A j, D |- T - - where the type of h is the inductive datatype (I A j) where A are parameters, - and j the indices. Generate the old_goal - - Ctx, h : I A j, D, j' : J, h' : I A j' |- j == j' -> h == h' -> T - - Remark: (j == j' -> h == h') is a "telescopic" equality. If the environment - is proof irrelevant, it is built using homogenous and heterogeneous equalities. - If the environment is proof relevant, it is built using homogeneous equality - and the eq.rec (this construction is much more complex than the proof irrelevant - one). - - Remark: j is sequence of terms, and j' a sequence of local constants. - - The original old_goal is solved if we can solve the produced old_goal. - - \remark h_type is mlocal_type(h) after normalization - */ - old_goal generalize_indices(old_goal const & g, expr const & h, expr const & h_type) { - buffer hyps; - g.get_hyps(hyps); - expr m = g.get_meta(); - expr m_type = g.get_type(); - name h_new_name = get_unused_name(local_pp_name(h), hyps); - buffer I_args; - expr const & I = get_app_args(h_type, I_args); - expr h_new_type = mk_app(I, I_args.size() - m_nindices, I_args.data()); - expr d = whnf(infer_type(h_new_type)); - name t_prefix("t"); - unsigned nidx = 1; - if (m_proof_irrel) { - unsigned eq_idx = 1; - name eq_prefix("H"); - buffer ts; - buffer eqs; - buffer refls; - auto add_eq = [&](expr const & lhs, expr const & rhs) { - pair p = mk_eq(lhs, rhs); - expr new_eq = p.first; - expr new_refl = p.second; - eqs.push_back(mk_local(mk_fresh_name(), g.get_unused_name(eq_prefix, eq_idx), new_eq, binder_info())); - refls.push_back(new_refl); - }; - for (unsigned i = I_args.size() - m_nindices; i < I_args.size(); i++) { - expr t_type = binding_domain(d); - expr t = mk_local(mk_fresh_name(), g.get_unused_name(t_prefix, nidx), t_type, binder_info()); - expr const & index = I_args[i]; - add_eq(index, t); - h_new_type = mk_app(h_new_type, t); - hyps.push_back(t); - ts.push_back(t); - d = instantiate(binding_body(d), t); - } - expr h_new = mk_local(mk_fresh_name(), h_new_name, h_new_type, local_info(h)); - if (m_dep_elim) - add_eq(h, h_new); - hyps.push_back(h_new); - expr new_type = Pi(eqs, g.get_type()); - expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(hyps, new_type)), hyps); - old_goal new_g(new_meta, new_type); - expr val = mk_app(mk_app(mk_app(Fun(ts, Fun(h_new, new_meta)), m_nindices, I_args.end() - m_nindices), h), - refls); - assign(g, val); - return new_g; - } else { - // proof relevant version - buffer ss; - buffer ts; - buffer refls; - for (unsigned i = I_args.size() - m_nindices; i < I_args.size(); i++) { - expr t_type = binding_domain(d); - expr t = mk_local(mk_fresh_name(), g.get_unused_name(t_prefix, nidx), t_type, binder_info()); - h_new_type = mk_app(h_new_type, t); - ss.push_back(I_args[i]); - refls.push_back(mk_refl(m_tc, I_args[i])); - hyps.push_back(t); - ts.push_back(t); - d = instantiate(binding_body(d), t); - } - expr h_new = mk_local(mk_fresh_name(), h_new_name, h_new_type, local_info(h)); - ts.push_back(h_new); - ss.push_back(h); - refls.push_back(mk_refl(m_tc, h)); - hyps.push_back(h_new); - buffer eqs; - mk_telescopic_eq(m_tc, ss, ts, eqs); - ts.pop_back(); - expr new_type = Pi(eqs, g.get_type()); - expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(hyps, new_type)), hyps); - old_goal new_g(new_meta, new_type); - expr val = mk_app(mk_app(mk_app(Fun(ts, Fun(h_new, new_meta)), m_nindices, I_args.end() - m_nindices), h), - refls); - assign(g, val); - return new_g; - } - } - - /** \brief Generalize h dependencies. - - This tactic uses this method only if has_indep_indices(hyps, h, h_type) returns true. - - The hypotheses that depend on h are stored in deps. - */ - old_goal generalize_dependecies(old_goal const & g, expr const & h, buffer & deps) { - buffer hyps; - g.get_hyps(hyps); - hyps.erase_elem(h); - buffer non_deps; - split_deps(hyps, h, non_deps, deps); - buffer & new_hyps = non_deps; - new_hyps.push_back(h); - expr new_type = Pi(deps, g.get_type()); - expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(new_hyps, new_type)), new_hyps); - old_goal new_g(new_meta, new_type); - expr val = mk_app(new_meta, deps); - assign(g, val); - return new_g; - } - - /** - \brief Given a old_goal of the form - - Ctx, h : I A j |- T[h] - - produce the subold_goals - - Ctx, h : I A j |- b_1 : B_1 -> T [C_1 A b_1] - ... - Ctx, h : I A j |- b_n : B_n -> T [C_n A b_n] - - where the C_i's are the constructors (aka introduction rules) of the inductive datatype h. - - The hypothesis h must be the last hypothesis in the input old_goal. Consequently, no other - hypothesis depends on it. - - The implementation list is external auxiliary data associated with constructors. - For example, we use it to compile recursive equations. Each implementation corresponds to one - equation. Each equation is tagged with a constructor C_i. The constructor is retrieved using - the virtual method get_constructor_name. We split the list imps in n lists. One for each - subold_goal. An implementation associated with the constructor i is in the i-th resulting list. - - \remark This method assumes the indices j are local constants, and only h and j may depend on j. - */ - std::pair, list> apply_cases_on(old_goal const & g, implementation_list const & imps, bool has_indep_indices) { - buffer hyps; - g.get_hyps(hyps); - expr const & h = hyps.back(); - expr const & h_type = whnf(mlocal_type(h)); - buffer I_args; - expr const & I = get_app_args(h_type, I_args); - name const & I_name = const_name(I); - expr g_type = g.get_type(); - expr cases_on; - level g_lvl = sort_level(m_tc.ensure_type(g_type).first); - if (m_cases_on_decl.get_num_univ_params() != m_I_decl.get_num_univ_params()) { - cases_on = mk_constant({I_name, "cases_on"}, cons(g_lvl, const_levels(I))); - } else { - if (!is_zero(g_lvl)) { - /* - if (m_throw_tactic_exception) - throw tactic_exception(sstream() << "invalid 'cases' tactic, '" << const_name(I) << "' can only eliminate to Prop"); - else - */ - throw inversion_exception(); - } - cases_on = mk_constant({I_name, "cases_on"}, const_levels(I)); - } - // add params - cases_on = mk_app(cases_on, m_nparams, I_args.data()); - // add type former - expr type_former = g_type; - if (m_dep_elim) - type_former = Fun(h, type_former); - type_former = Fun(m_nindices, I_args.end() - m_nindices, type_former); - cases_on = mk_app(cases_on, type_former); - // add indices - cases_on = mk_app(cases_on, m_nindices, I_args.end() - m_nindices); - // add h - cases_on = mk_app(cases_on, h); - buffer intro_names; - get_intro_rule_names(m_env, I_name, intro_names); - lean_assert(m_nminors == intro_names.size()); - buffer new_hyps; - if (has_indep_indices) - new_hyps.append(hyps.size() - 1, hyps.data()); - else - new_hyps.append(hyps.size() - m_nindices - 1, hyps.data()); - - // add a subold_goal for each minor premise of cases_on - expr cases_on_type = whnf(infer_type(cases_on)); - buffer new_goals; - buffer new_imps; - for (unsigned i = 0; i < m_nminors; i++) { - expr new_type = binding_domain(cases_on_type); - expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(new_hyps, new_type)), new_hyps); - old_goal new_g(new_meta, new_type); - new_goals.push_back(new_g); - cases_on = mk_app(cases_on, new_meta); - cases_on_type = whnf(binding_body(cases_on_type)); // the minor premises do not depend on each other - name const & intro_name = intro_names[i]; - new_imps.push_back(filter(imps, [&](implementation_ptr const & imp) { return imp->get_constructor_name() == intro_name; })); - } - assign(g, cases_on); - return mk_pair(to_list(new_goals), to_list(new_imps)); - } - - // Store in \c r the number of arguments for each cases_on minor. - void get_minors_nargs(buffer & r) { - expr cases_on_type = m_cases_on_decl.get_type(); - for (unsigned i = 0; i < m_nparams + 1 + m_nindices + 1; i++) - cases_on_type = binding_body(cases_on_type); - for (unsigned i = 0; i < m_nminors; i++) { - expr minor_type = binding_domain(cases_on_type); - unsigned nargs = 0; - while (is_pi(minor_type)) { - nargs++; - minor_type = binding_body(minor_type); - } - r.push_back(nargs); - cases_on_type = binding_body(cases_on_type); - } - } - - /** - The method apply_cases_on produces subgoals of the form - - Ctx, h : I A j |- b_i : B_i -> T [C_i A b_i] - - The b_i are the arguments of the constructor C_i. - This method moves the b_i's to the hypotheses list. - */ - std::pair, list>> intros_minors_args(list gs) { - buffer minors_nargs; - get_minors_nargs(minors_nargs); - lean_assert(length(gs) == minors_nargs.size()); - buffer new_gs; - buffer> new_args; - for (unsigned i = 0; i < minors_nargs.size(); i++) { - old_goal const & g = head(gs); - unsigned nargs = minors_nargs[i]; - buffer hyps; - g.get_hyps(hyps); - buffer new_hyps; - new_hyps.append(hyps); - expr g_type = g.get_type(); - buffer curr_new_args; - for (unsigned i = 0; i < nargs; i++) { - expr type = binding_domain(g_type); - name new_h_name; - if (m_ids) { - new_h_name = head(m_ids); - m_ids = tail(m_ids); - } else { - new_h_name = binding_name(g_type); - } - expr new_h = mk_local(mk_fresh_name(), get_unused_name(new_h_name, new_hyps), type, binder_info()); - curr_new_args.push_back(new_h); - new_hyps.push_back(new_h); - g_type = instantiate(binding_body(g_type), new_h); - } - new_args.push_back(to_list(curr_new_args)); - g_type = head_beta_reduce(g_type); - expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(new_hyps, g_type)), new_hyps); - old_goal new_g(new_meta, g_type); - new_gs.push_back(new_g); - expr val = Fun(nargs, new_hyps.end() - nargs, new_meta); - assign(g, val); - gs = tail(gs); - } - return mk_pair(to_list(new_gs), to_list(new_args)); - } - - // auxiliary exception used to interrupt execution - struct inversion_exception {}; - - [[ noreturn ]] void throw_ill_formed_goal() { - /* if (m_throw_tactic_exception) - throw tactic_exception("invalid 'cases' tactic, ill-formed goal"); - else - */ - throw inversion_exception(); - } - - [[ noreturn ]] void throw_ill_typed_goal() { - /* - if (m_throw_tactic_exception) - throw tactic_exception("invalid 'cases' tactic, ill-typed goal"); - else - */ - throw inversion_exception(); - } - - [[ noreturn ]] void throw_lift_down_failure() { - /* - if (m_throw_tactic_exception) - throw tactic_exception("invalid 'cases' tactic, lift.down failed"); - else - */ - throw inversion_exception(); - } - - void throw_unification_eq_rec_failure(old_goal const & /* g */, expr const & /* eq */) { - /* - if (m_throw_tactic_exception) { - throw tactic_exception([=](formatter const & fmt) { - format r("invalid 'cases' tactic, unification failed to eliminate eq.rec in the homogeneous equality"); - r += pp_indent_expr(fmt, eq); - r += compose(line(), format("auxiliary goal at time of failure")); - r += nest(get_pp_indent(fmt.get_options()), compose(line(), g.pp(fmt))); - return r; - }); - } else { - */ - throw inversion_exception(); - // } - } - - /** \brief Process goal of the form: Pi (H : eq.rec A s C a s p = b), R - The idea is to reduce it to - Pi (H : a = b), R - when A is a set - and then invoke intro_next_eq recursively. - - \remark \c type is the type of \c g after some normalization - */ - old_goal intro_next_eq_rec(old_goal const & g, expr const & type) { - lean_assert(is_pi(type)); - buffer hyps; - g.get_hyps(hyps); - expr const & eq = binding_domain(type); - expr const & lhs = app_arg(app_fn(eq)); - expr const & rhs = app_arg(eq); - lean_assert(is_eq_rec_core(lhs)); - // lhs is of the form (eq.rec A s C a s p) - // aux_eq is a term of type ((eq.rec A s C a s p) = a) - auto aux_eq = apply_eq_rec_eq(m_tc, m_ios, to_list(hyps), lhs); - if (!aux_eq || has_expr_metavar_relaxed(*aux_eq)) { - throw_unification_eq_rec_failure(g, eq); - } - buffer lhs_args; - get_app_args(lhs, lhs_args); - expr const & reduced_lhs = lhs_args[3]; - expr new_eq = ::lean::mk_eq(m_tc, reduced_lhs, rhs); - expr new_type = update_binding(type, new_eq, binding_body(type)); - expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(hyps, new_type)), hyps); - old_goal new_g(new_meta, new_type); - // create assignment for g - expr A = infer_type(lhs); - level lvl = sort_level(m_tc.ensure_type(A).first); - // old_eq : eq.rec A s C a s p = b - expr old_eq = mk_local(mk_fresh_name(), binding_name(type), eq, binder_info()); - // aux_eq : a = eq.rec A s C a s p - expr trans_eq = mk_app({mk_constant(get_eq_trans_name(), {lvl}), A, reduced_lhs, lhs, rhs, *aux_eq, old_eq}); - // trans_eq : a = b - expr val = Fun(old_eq, mk_app(new_meta, trans_eq)); - assign(g, val); - return intro_next_eq(new_g); - } - - /** - \brief Process goal of the form: Ctx |- Pi (H : a == b), R when a and b have the same type - The idea is to reduce it to - Ctx, H : a = b |- R - This method is only used if the environment has a proof irrelevant Prop. - */ - old_goal intro_next_heq(old_goal const & g) { - lean_assert(m_proof_irrel); - expr const & type = g.get_type(); - expr eq = binding_domain(type); - lean_assert(const_name(get_app_fn(eq)) == get_heq_name()); - buffer args; - expr const & heq_fn = get_app_args(eq, args); - constraint_seq cs; - if (m_tc.is_def_eq(args[0], args[2], justification(), cs) && !cs) { - buffer hyps; - g.get_hyps(hyps); - expr new_eq = mk_app(mk_constant(get_eq_name(), const_levels(heq_fn)), args[0], args[1], args[3]); - expr new_hyp = mk_local(mk_fresh_name(), g.get_unused_name(binding_name(type)), new_eq, binder_info()); - expr new_type = instantiate(binding_body(type), new_hyp); - hyps.push_back(new_hyp); - expr new_mvar = mk_metavar(mk_fresh_name(), Pi(hyps, new_type)); - expr new_meta = mk_app(new_mvar, hyps); - old_goal new_g(new_meta, new_type); - hyps.pop_back(); - expr H = mk_local(mk_fresh_name(), g.get_unused_name(binding_name(type)), binding_domain(type), binder_info()); - expr to_eq = mk_app(mk_constant(get_eq_of_heq_name(), const_levels(heq_fn)), args[0], args[1], args[3], H); - expr val = Fun(H, mk_app(mk_app(new_mvar, hyps), to_eq)); - assign(g, val); - return new_g; - } else { - /* - if (m_throw_tactic_exception) { - throw tactic_exception("invalid 'cases' tactic, unification failed to reduce heterogeneous equality into homogeneous one"); - } else { - */ - throw inversion_exception(); - // } - } - } - - /** \brief Process old_goal of the form: Ctx |- Pi (H : a = b), R - The idea is to reduce it to - Ctx, H : a = b |- R - - \remark \c type is the type of \c g after some normalization - */ - old_goal intro_next_eq_simple(old_goal const & g, expr const & type) { - expr eq = binding_domain(type); - lean_assert(const_name(get_app_fn(eq)) == get_eq_name()); - buffer hyps; - g.get_hyps(hyps); - expr new_hyp = mk_local(mk_fresh_name(), g.get_unused_name(binding_name(type)), binding_domain(type), binder_info()); - expr new_type = instantiate(binding_body(type), new_hyp); - hyps.push_back(new_hyp); - expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(hyps, new_type)), hyps); - old_goal new_g(new_meta, new_type); - expr val = Fun(new_hyp, new_meta); - assign(g, val); - return new_g; - } - - old_goal intro_next_eq(old_goal const & g) { - expr type = g.get_type(); - if (!is_pi(type)) - throw_ill_formed_goal(); - expr eq = binding_domain(type); - expr const & eq_fn = get_app_fn(eq); - if (!is_constant(eq_fn)) - throw_ill_formed_goal(); - if (const_name(eq_fn) == get_eq_name()) { - expr const & lhs = app_arg(app_fn(eq)); - expr const & rhs = app_arg(eq); - expr new_lhs = whnf(lhs); - expr new_rhs = whnf(rhs); - if (lhs != new_lhs || rhs != new_rhs) { - eq = mk_app(app_fn(app_fn(eq)), new_lhs, new_rhs); - type = update_binding(type, eq, binding_body(type)); - } - if (!m_proof_irrel && is_eq_rec_core(new_lhs)) { - return intro_next_eq_rec(g, type); - } else { - return intro_next_eq_simple(g, type); - } - } else if (m_proof_irrel && const_name(eq_fn) == get_heq_name()) { - return intro_next_heq(g); - } else { - throw_ill_formed_goal(); - } - } - - /** - \brief The no_confusion constructions uses lifts in the proof relevant version. - We must apply lift.down to eliminate the auxiliary lift. - */ - expr lift_down(expr const & v) { - if (auto r = lift_down_if_hott(m_tc, v)) - return *r; - else - throw_lift_down_failure(); - } - - buffer m_c_args; // current intro/constructor args that may be renamed by unify_eqs - rename_map m_renames; - implementation_list m_imps; - - void store_rename(expr const & old_hyp, expr const & new_hyp) { - for (expr & c_arg : m_c_args) { - if (is_local(c_arg) && mlocal_name(old_hyp) == mlocal_name(c_arg)) - c_arg = new_hyp; - } - if (is_local(new_hyp)) - m_renames.insert(mlocal_name(old_hyp), mlocal_name(new_hyp)); - } - - /** \brief Update m_renames with old_hyps --> new_hyps. */ - void store_renames(buffer const & old_hyps, buffer const & new_hyps) { - lean_assert(old_hyps.size() == new_hyps.size()); - for (unsigned i = 0; i < old_hyps.size(); i++) { - store_rename(old_hyps[i], new_hyps[i]); - } - } - - [[ noreturn ]] void throw_unify_eqs_failure(old_goal const & /* g */) { - /* - if (m_throw_tactic_exception) { - throw tactic_exception([=](formatter const & fmt) { - format r("invalid 'cases' tactic, unification failed"); - r += compose(line(), format("auxiliary goal at time of failure")); - r += nest(get_pp_indent(fmt.get_options()), compose(line(), g.pp(fmt))); - return r; - }); - } else { - */ - throw inversion_exception(); - // } - } - - // Remark: it also updates m_renames and m_imps - optional unify_eqs(old_goal g, unsigned neqs) { - if (neqs == 0) - return optional(g); // done - g = intro_next_eq(g); - buffer hyps; - g.get_hyps(hyps); - lean_assert(!hyps.empty()); - expr Heq = hyps.back(); - buffer Heq_args; - get_app_args(mlocal_type(Heq), Heq_args); - expr const & A = whnf(Heq_args[0]); - expr lhs = whnf(Heq_args[1]); - expr rhs = whnf(Heq_args[2]); - constraint_seq cs; - if (m_proof_irrel && m_tc.is_def_eq(lhs, rhs, justification(), cs) && !cs) { - // deletion transition: t == t - hyps.pop_back(); // remove t == t equality - expr new_type = g.get_type(); - expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(hyps, new_type)), hyps); - old_goal new_g(new_meta, new_type); - assign(g, new_meta); - return unify_eqs(new_g, neqs-1); - } - buffer lhs_args, rhs_args; - expr const & lhs_fn = get_app_args(lhs, lhs_args); - expr const & rhs_fn = get_app_args(rhs, rhs_args); - expr const & g_type = g.get_type(); - level const & g_lvl = sort_level(m_tc.ensure_type(g_type).first); - if (is_constant(lhs_fn) && - is_constant(rhs_fn) && - inductive::is_intro_rule(m_env, const_name(lhs_fn)) && - inductive::is_intro_rule(m_env, const_name(rhs_fn))) { - buffer A_args; - expr const & A_fn = get_app_args(A, A_args); - if (!is_constant(A_fn) || !inductive::is_inductive_decl(m_env, const_name(A_fn))) - throw_ill_typed_goal(); - name no_confusion_name(const_name(A_fn), "no_confusion"); - if (!m_env.find(no_confusion_name)) { - // if (m_throw_tactic_exception) - // throw tactic_exception(sstream() << "invalid 'cases' tactic, construction '" << no_confusion_name << "' is not available in the environment"); - // else - throw inversion_exception(); - } - expr no_confusion = mk_app(mk_app(mk_constant(no_confusion_name, cons(g_lvl, const_levels(A_fn))), A_args), g_type, lhs, rhs, Heq); - if (const_name(lhs_fn) == const_name(rhs_fn)) { - // injectivity transition - expr new_type = binding_domain(whnf(infer_type(no_confusion))); - if (m_proof_irrel || !depends_on(g_type, hyps.back())) - hyps.pop_back(); // remove processed equality - expr new_mvar = mk_metavar(mk_fresh_name(), Pi(hyps, new_type)); - expr new_meta = mk_app(new_mvar, hyps); - old_goal new_g(new_meta, new_type); - expr val = lift_down(mk_app(no_confusion, new_meta)); - assign(g, val); - unsigned A_nparams = *inductive::get_num_params(m_env, const_name(A_fn)); - lean_assert(lhs_args.size() >= A_nparams); - return unify_eqs(new_g, neqs - 1 + lhs_args.size() - A_nparams); - } else { - // conflict transition, Heq is of the form c_1 ... = c_2 ..., where c_1 and c_2 are different constructors/intro rules. - expr val = lift_down(no_confusion); - assign(g, val); - return optional(); // old_goal has been solved - } - } - if (is_local(rhs)) { - // solution transition, Heq is of the form t = y, where y is a local constant - - // assume the current old_goal is of the form - // - // non_deps, deps[rhs], H : lhs = rhs |- C[rhs] - // - // We use non_deps to denote hypotheses that do not depend on rhs, - // and deps[rhs] to denote hypotheses that depend on it. - // - // The resultant old_goal is of the form - // - // non_deps, deps[lhs] |- C[lhs] - // - // Now, assume ?m1 is a solution for the resultant old_goal. - // Then, - // - // @eq.rec A lhs (fun rhs, Pi(deps[rhs], C[rhs])) (?m1 non_deps) rhs H deps[rhs] - // - // is a solution for the original old_goal. - // Remark: A is the type of lhs and rhs - hyps.pop_back(); // remove processed equality - buffer non_deps, deps; - bool clear_rhs = m_clear_elim; - split_deps(hyps, rhs, non_deps, deps, clear_rhs); - if (deps.empty() && !depends_on(g_type, rhs)) { - // eq.rec is not necessary - buffer & new_hyps = non_deps; - expr new_type = g_type; - expr new_mvar = mk_metavar(mk_fresh_name(), Pi(new_hyps, new_type)); - expr new_meta = mk_app(new_mvar, new_hyps); - old_goal new_g(new_meta, new_type); - assign(g, new_meta); - return unify_eqs(new_g, neqs-1); - } else { - expr deps_g_type = Pi(deps, g_type); - level eq_rec_lvl1 = sort_level(m_tc.ensure_type(deps_g_type).first); - level eq_rec_lvl2 = sort_level(m_tc.ensure_type(A).first); - expr tformer; - if (m_proof_irrel) { - tformer = Fun(rhs, deps_g_type); - } else { - if (depends_on(lhs, rhs)) { - // tformer must be of the form - // fun x, fun (Heq : lhs = x, ...) - // If the lhs contains occurrences of rhs, then - // we would produce the following ill-typed tformer - // fun x, fun (Heq : lhs[x] = x, ...) - throw_unify_eqs_failure(g); - } - tformer = Fun(rhs, Fun(Heq, deps_g_type)); - } - expr eq_rec = mk_constant(get_eq_rec_name(), {eq_rec_lvl1, eq_rec_lvl2}); - eq_rec = mk_app(eq_rec, A, lhs, tformer); - buffer new_hyps; - new_hyps.append(non_deps); - expr new_type = instantiate(abstract_local(deps_g_type, rhs), lhs); - store_rename(rhs, lhs); - replace(m_imps, rhs, lhs); - if (!m_proof_irrel) { - new_type = abstract_local(new_type, Heq); - new_type = instantiate(new_type, mk_refl(m_tc, lhs)); - } - buffer new_deps; - for (unsigned i = 0; i < deps.size(); i++) { - expr new_hyp = mk_local(mk_fresh_name(), binding_name(new_type), binding_domain(new_type), - binding_info(new_type)); - new_hyps.push_back(new_hyp); - new_deps.push_back(new_hyp); - new_type = instantiate(binding_body(new_type), new_hyp); - } - replace(m_imps, deps, new_deps); - lean_assert(deps.size() == new_deps.size()); - store_renames(deps, new_deps); - expr new_mvar = mk_metavar(mk_fresh_name(), Pi(new_hyps, new_type)); - expr new_meta = mk_app(new_mvar, new_hyps); - old_goal new_g(new_meta, new_type); - expr eq_rec_minor = mk_app(new_mvar, non_deps); - eq_rec = mk_app(eq_rec, eq_rec_minor, rhs, Heq); - expr val = mk_app(eq_rec, deps); - assign(g, val); - return unify_eqs(new_g, neqs-1); - } - } else if (is_local(lhs)) { - // flip equation and reduce to previous case - expr symm_eq = mk_eq(rhs, lhs).first; - hyps.pop_back(); // remove processed equality - if (!depends_on(g_type, Heq)) { - expr new_type = mk_arrow(symm_eq, g_type); - expr new_mvar = mk_metavar(mk_fresh_name(), Pi(hyps, new_type)); - expr new_meta = mk_app(new_mvar, hyps); - old_goal new_g(new_meta, new_type); - expr Heq_inv = mk_symm(m_tc, Heq); - expr val = mk_app(new_meta, Heq_inv); - assign(g, val); - return unify_eqs(new_g, neqs); - } else { - // Let C[Heq] be the original conclusion which depends on the equality eq being processed. - expr new_Heq = update_mlocal(Heq, symm_eq); - expr new_Heq_inv = mk_symm(m_tc, new_Heq); - expr new_type = Pi(new_Heq, instantiate(abstract_local(g_type, Heq), new_Heq_inv)); - expr new_mvar = mk_metavar(mk_fresh_name(), Pi(hyps, new_type)); - expr new_meta = mk_app(new_mvar, hyps); - old_goal new_g(new_meta, new_type); - // Then, we have - // new_meta : Pi (new_Heq : rhs = lhs), C[symm new_Heq] - expr Heq_inv = mk_symm(m_tc, Heq); - expr val = mk_app(new_meta, Heq_inv); - // val : C[symm (symm Heq)] - // Remark: in proof irrelevant mode (symm (symm Heq)) is definitionally equal to Heq - if (!m_proof_irrel) { - expr C = Fun(Heq, g_type); - level A_lvl = sort_level(m_tc.ensure_type(A).first); - level g_lvl = sort_level(m_tc.ensure_type(g_type).first); - expr elim_inv_inv = mk_constant(get_eq_elim_inv_inv_name(), {A_lvl, g_lvl}); - val = mk_app({elim_inv_inv, A, lhs, rhs, C, Heq, val}); - // val : C[Heq] as we wanted - } - assign(g, val); - return unify_eqs(new_g, neqs); - } - } - throw_unify_eqs_failure(g); - } - - auto unify_eqs(list const & gs, list> args, list imps) -> - std::tuple, list>, list, list> { - lean_assert(length(gs) == length(imps)); - unsigned neqs = m_nindices + (m_dep_elim ? 1 : 0); - buffer new_goals; - buffer> new_args; - buffer new_imps; - buffer new_renames; - for (old_goal const & g : gs) { - flet set1(m_renames, rename_map()); - flet set2(m_imps, head(imps)); - m_c_args.clear(); - to_buffer(head(args), m_c_args); - if (optional new_g = unify_eqs(g, neqs)) { - new_goals.push_back(*new_g); - list new_as = to_list(m_c_args); - new_args.push_back(new_as); - new_imps.push_back(m_imps); - new_renames.push_back(m_renames); - } - imps = tail(imps); - args = tail(args); - } - return std::make_tuple(to_list(new_goals), to_list(new_args), to_list(new_imps), to_list(new_renames)); - } - - std::pair intro_deps(old_goal const & g, buffer const & deps) { - buffer hyps; - g.get_hyps(hyps); - buffer new_hyps; - new_hyps.append(hyps); - rename_map rs; - expr g_type = g.get_type(); - for (expr const & d : deps) { - expr type = binding_domain(g_type); - expr new_d = mk_local(mk_fresh_name(), get_unused_name(local_pp_name(d), new_hyps), type, local_info(d)); - rs.insert(mlocal_name(d), mlocal_name(new_d)); - new_hyps.push_back(new_d); - g_type = instantiate(binding_body(g_type), new_d); - } - expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(new_hyps, g_type)), new_hyps); - old_goal new_g(new_meta, g_type); - unsigned ndeps = deps.size(); - expr val = Fun(ndeps, new_hyps.end() - ndeps, new_meta); - assign(g, val); - return mk_pair(new_g, rs); - } - - std::pair, list> intro_deps(list const & gs, buffer const & deps) { - buffer new_goals; - buffer new_rs; - for (old_goal const & g : gs) { - auto p = intro_deps(g, deps); - new_goals.push_back(p.first); - new_rs.push_back(p.second); - } - return mk_pair(to_list(new_goals), to_list(new_rs)); - } - - old_goal clear_hypothesis(old_goal const & g, name const & h) { - if (auto p = g.find_hyp_from_internal_name(h)) { - expr const & h = p->first; - unsigned i = p->second; - buffer hyps; - g.get_hyps(hyps); - hyps.erase(hyps.size() - i - 1); - if (depends_on(g.get_type(), h) || depends_on(i, hyps.end() - i, h)) { - return g; // other hypotheses or result type depend on h - } - expr new_type = g.get_type(); - expr new_meta = mk_app(mk_metavar(mk_fresh_name(), Pi(hyps, new_type)), hyps); - old_goal new_g(new_meta, new_type); - assign(g, new_meta); - return new_g; - } else { - return g; - } - } - - // Remove hypothesis of the form (H : a = a) - old_goal remove_eq_refl_hypotheses(old_goal g) { - buffer to_remove; - buffer hyps; - g.get_hyps(hyps); - for (expr const & h : hyps) { - expr const & h_type = mlocal_type(h); - if (!is_eq(h_type)) - continue; - expr const & lhs = app_arg(app_fn(h_type)); - expr const & rhs = app_arg(h_type); - if (lhs == rhs) - to_remove.push_back(mlocal_name(h)); - } - for (name const & h : to_remove) { - g = clear_hypothesis(g, h); - } - return g; - } - - list clear_hypothesis(list const & gs, list rs, name const & h_name, expr const & h_type) { - buffer new_gs; - optional lhs_name; // If h_type is of the form lhs = rhs, and lhs is also a hypothesis, then we also remove it. - if (is_eq(h_type) && is_local(app_arg(app_fn(h_type)))) { - lhs_name = mlocal_name(app_arg(app_fn(h_type))); - } - for (old_goal const & g : gs) { - rename_map const & m = head(rs); - old_goal new_g = clear_hypothesis(g, m.find(h_name)); - if (lhs_name) - new_g = clear_hypothesis(new_g, *lhs_name); - if (!m_proof_irrel) - new_g = remove_eq_refl_hypotheses(new_g); - new_gs.push_back(new_g); - rs = tail(rs); - } - return to_list(new_gs); - } - -public: - inversion_tac(environment const & env, io_state const & ios, - old_type_checker & tc, substitution const & subst, list const & ids, - bool /* throw_tactic_ex */, bool clear_elim): - m_env(env), m_ios(ios), m_tc(tc), m_ids(ids), - m_subst(subst), - m_clear_elim(clear_elim) { - m_proof_irrel = m_env.prop_proof_irrel(); - } - - inversion_tac(environment const & env, io_state const & ios, old_type_checker & tc, bool clear_elim): - inversion_tac(env, ios, tc, substitution(), list(), false, clear_elim) {} - - typedef inversion::result result; - - optional execute(old_goal const & g, expr const & h, implementation_list const & imps) { - try { - expr h_type = whnf(mlocal_type(h)); - if (!is_inversion_applicable(h_type)) - return optional(); - if (has_indep_indices(g, h, h_type)) { - buffer deps; - old_goal g1 = generalize_dependecies(g, h, deps); - auto gs_imps_pair = apply_cases_on(g1, imps, true); - list gs2 = gs_imps_pair.first; - list new_imps = gs_imps_pair.second; - auto gs_args_pair = intros_minors_args(gs2); - list gs3 = gs_args_pair.first; - list> args = gs_args_pair.second; - auto gs_rs_pair = intro_deps(gs3, deps); - list gs4 = gs_rs_pair.first; - list rs = gs_rs_pair.second; - return optional(result(gs4, args, new_imps, rs, m_subst)); - } else { - old_goal g1 = generalize_indices(g, h, h_type); - auto gs_imps_pair = apply_cases_on(g1, imps, false); - list gs2 = gs_imps_pair.first; - list new_imps = gs_imps_pair.second; - auto gs_args_pair = intros_minors_args(gs2); - list gs3 = gs_args_pair.first; - list> args = gs_args_pair.second; - list gs4; - list rs; - std::tie(gs4, args, new_imps, rs) = unify_eqs(gs3, args, new_imps); - gs4 = clear_hypothesis(gs4, rs, mlocal_name(h), h_type); - return optional(result(gs4, args, new_imps, rs, m_subst)); - } - } catch (inversion_exception & ex) { - return optional(); - } - } - - optional execute(old_goal const & g, name const & n, implementation_list const & imps) { - auto p = g.find_hyp(n); - if (!p) { - // if (m_throw_tactic_exception) - // throw tactic_exception(sstream() << "invalid 'cases' tactic, unknown hypothesis '" << n << "'"); - return optional(); - } - expr const & h = p->first; - return execute(g, h, imps); - } -}; - -namespace inversion { -optional apply(environment const & env, io_state const & ios, old_type_checker & tc, - old_goal const & g, expr const & h, implementation_list const & imps, bool clear_elim) { - return inversion_tac(env, ios, tc, clear_elim).execute(g, h, imps); -} -} -} diff --git a/src/library/equations_compiler/old_inversion.h b/src/library/equations_compiler/old_inversion.h deleted file mode 100644 index 72a352750a..0000000000 --- a/src/library/equations_compiler/old_inversion.h +++ /dev/null @@ -1,62 +0,0 @@ -/* -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "kernel/expr.h" -#include "library/metavar.h" -#include "library/equations_compiler/old_goal.h" - - -namespace lean { -namespace inversion { -/** - \brief When we apply the inversion tactic/procedure on a hypothesis (h : I A j), where - I is an inductive datatpe, the hypothesis is "broken" into cases: one for each constructor. - Some cases may be in conflict with the type (I A j) and may be suppressed. - - Example of conflict: given the vector type - inductive vector (A : Type) : nat → Type := - nil {} : vector A zero, - cons : Π {n : nat}, A → vector A n → vector A (succ n) - Then, (h : vector A (succ n)) is in conflict with constructor nil. - - The user may provide possible implementations (example: in the form of equations). - Each possible implementation is associated with a case/constructor. - - The inversion tactic/procedure distributes the implementations over cases. - - The implementations may depend on hypotheses that may be modifed by the inversion procedure. - The method update_exprs of each implementation is invoked to update the expressions of - a given implementation. -*/ -class implementation { -public: - virtual ~implementation() {} - virtual name const & get_constructor_name() const = 0; - virtual void update_exprs(std::function const & fn) = 0; -}; - -typedef std::shared_ptr implementation_ptr; -typedef list implementation_list; - -struct result { - list m_goals; - list> m_args; // arguments of the constructor/intro rule - list m_implementation_lists; - list m_renames; - // invariant: length(m_goals) == length(m_args); - // invariant: length(m_goals) == length(m_implementation_lists); - // invariant: length(m_goals) == length(m_renames); - substitution m_subst; - result(list const & gs, list> const & args, list const & imps, - list const & rs, substitution const & subst); -}; - -optional apply(environment const & env, io_state const & ios, old_type_checker & tc, - old_goal const & g, expr const & h, implementation_list const & imps, - bool clear_elim); -} -}