From b0e0e8235050317b966f89629adc3ec6b8a5a9ec Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 30 Apr 2014 18:42:01 -0700 Subject: [PATCH] refactor(kernel): separate type_checker and converter Signed-off-by: Leonardo de Moura --- src/kernel/CMakeLists.txt | 2 +- src/kernel/converter.cpp | 522 +++++++++++++++++++++++++++++ src/kernel/converter.h | 55 ++++ src/kernel/type_checker.cpp | 546 +++---------------------------- src/kernel/type_checker.h | 11 +- src/tests/kernel/environment.cpp | 2 +- 6 files changed, 639 insertions(+), 499 deletions(-) create mode 100644 src/kernel/converter.cpp create mode 100644 src/kernel/converter.h diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index fe62da1f3..44b99576e 100644 --- a/src/kernel/CMakeLists.txt +++ b/src/kernel/CMakeLists.txt @@ -2,7 +2,7 @@ add_library(kernel level.cpp diff_cnstrs.cpp expr.cpp expr_eq_fn.cpp for_each_fn.cpp replace_fn.cpp free_vars.cpp abstract.cpp instantiate.cpp context.cpp formatter.cpp max_sharing.cpp definition.cpp replace_visitor.cpp environment.cpp -justification.cpp pos_info_provider.cpp metavar.cpp +justification.cpp pos_info_provider.cpp metavar.cpp converter.cpp constraint.cpp type_checker.cpp error_msgs.cpp kernel_exception.cpp ) diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp new file mode 100644 index 000000000..2f758d516 --- /dev/null +++ b/src/kernel/converter.cpp @@ -0,0 +1,522 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "util/interrupt.h" +#include "util/lbool.h" +#include "kernel/converter.h" +#include "kernel/max_sharing.h" +#include "kernel/expr_maps.h" +#include "kernel/instantiate.h" +#include "kernel/free_vars.h" + +namespace lean { +bool converter::is_conv(expr const & t, expr const & s, context & c) { + delayed_justification j([]() { return justification(); }); + return is_conv(t, s, c, j); +} + +bool converter::is_def_eq(expr const & t, expr const & s, context & c) { + delayed_justification j([]() { return justification(); }); + return is_def_eq(t, s, c, j); +} + +/** \brief Do nothing converter */ +struct dummy_converter : public converter { + virtual expr whnf(expr const & e, context &) { return e; } + virtual bool is_conv(expr const &, expr const &, context &, delayed_justification &) { return true; } + virtual bool is_def_eq(expr const &, expr const &, context &, delayed_justification &) { return true; } +}; + +std::unique_ptr mk_dummy_converter() { + return std::unique_ptr(new dummy_converter()); +} + +struct default_converter : public converter { + environment m_env; + optional m_module_idx; + bool m_memoize; + name_set m_extra_opaque; + max_sharing_fn m_sharing; + expr_map m_whnf_core_cache; + expr_map m_whnf_cache; + + default_converter(environment const & env, optional mod_idx, bool memoize, name_set const & extra_opaque): + m_env(env), m_module_idx(mod_idx), m_memoize(memoize), m_extra_opaque(extra_opaque) {} + + class extended_context : public extension_context { + default_converter & m_conv; + context & m_ctx; + public: + extended_context(default_converter & conv, context & ctx):m_conv(conv), m_ctx(ctx) {} + virtual environment const & env() const { return m_conv.m_env; } + virtual expr whnf(expr const & e) { return m_conv.whnf(e, m_ctx); } + virtual expr infer_type(expr const & e) { return m_ctx.infer_type(e); } + virtual name mk_fresh_name() { return m_ctx.mk_fresh_name(); } + virtual void add_cnstr(constraint const & c) { m_ctx.add_cnstr(c); } + }; + + bool check_memoized(expr const & e) const { return !m_memoize || m_sharing.already_processed(e); } + expr max_sharing(expr const & e) { return m_memoize ? m_sharing(e) : e; } + expr instantiate(expr const & e, unsigned n, expr const * s) { return max_sharing(lean::instantiate(e, n, s)); } + expr instantiate(expr const & e, expr const & s) { return max_sharing(lean::instantiate(e, s)); } + expr mk_app(expr const & f, unsigned num, expr const * args) { return max_sharing(lean::mk_app(f, num, args)); } + expr mk_app(expr const & f, expr const & a) { return max_sharing(lean::mk_app(f, a)); } + expr mk_rev_app(expr const & f, unsigned num, expr const * args) { return max_sharing(lean::mk_rev_app(f, num, args)); } + expr mk_app_vars(expr const & f, unsigned num) { return max_sharing(lean::mk_app_vars(f, num)); } + optional expand_macro(expr const & m, context & c) { + lean_assert(is_macro(m)); + extended_context xctx(*this, c); + if (auto new_m = macro_def(m).expand(macro_num_args(m), macro_args(m), xctx)) + return some_expr(max_sharing(*new_m)); + else + return none_expr(); + } + expr instantiate_params(expr const & e, param_names const & ps, levels const & ls) { + return max_sharing(lean::instantiate_params(e, ps, ls)); + } + /** \brief Apply normalizer extensions to \c e. */ + optional norm_ext(expr const & e, context & c) { + extended_context xctx(*this, c); + if (auto new_e = m_env.norm_ext()(e, xctx)) + return some_expr(max_sharing(*new_e)); + else + return none_expr(); + } + + /** \brief Weak head normal form core procedure. It does not perform delta reduction nor normalization extensions. */ + expr whnf_core(expr const & e, context & c) { + check_system("whnf"); + lean_assert(check_memoized(e)); + + // handle easy cases + switch (e.kind()) { + case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: + case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Constant: + return e; + case expr_kind::Macro: case expr_kind::Let: case expr_kind::App: + break; + } + + // check cache + if (m_memoize) { + auto it = m_whnf_core_cache.find(e); + if (it != m_whnf_core_cache.end()) + return it->second; + } + + // do the actual work + expr r; + switch (e.kind()) { + case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: + case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Constant: + lean_unreachable(); // LCOV_EXCL_LINE + case expr_kind::Macro: + if (auto m = expand_macro(e, c)) + r = whnf_core(*m, c); + else + r = e; + break; + case expr_kind::Let: + r = whnf_core(instantiate(let_body(e), let_value(e)), c); + break; + case expr_kind::App: { + buffer args; + expr const * it = &e; + while (is_app(*it)) { + args.push_back(app_arg(*it)); + it = &(app_fn(*it)); + } + expr f = whnf_core(*it, c); + if (is_lambda(f)) { + unsigned m = 1; + unsigned num_args = args.size(); + while (is_lambda(binder_body(f)) && m < num_args) { + f = binder_body(f); + m++; + } + lean_assert(m <= num_args); + r = whnf_core(mk_rev_app(instantiate(binder_body(f), m, args.data() + (num_args - m)), num_args - m, args.data()), c); + } else { + r = is_eqp(f, *it) ? e : mk_rev_app(f, args.size(), args.data()); + } + break; + }} + + if (m_memoize) + m_whnf_core_cache.insert(mk_pair(e, r)); + return r; + } + + /** + \brief Predicate for deciding whether \c d is an opaque definition or not. + + Here is the basic idea: + + 1) Each definition has an opaque flag. This flag cannot be modified after a definition is added to the environment. + The opaque flag affects the convertability check. The idea is to minimize the number of delta-reduction steps. + We also believe it increases the modularity of Lean developments by minimizing the dependency on how things are defined. + We should view non-opaque definitions as "inline definitions" used in programming languages such as C++. + + 2) Whenever type checking an expression, the user can provide an additional set of definition names (m_extra_opaque) that + should be considered opaque. Note that, if \c t type checks when using an extra_opaque set S, then t also type checks + (modulo resource constraints) with the empty set. Again, the purpose of extra_opaque is to mimimize the number + of delta-reduction steps. + + 3) To be able to prove theorems about an opaque definition, we treat an opaque definition D in a module M as + transparent when we are type checking another definition/theorem D' also in M. This rule only applies if + D is not a theorem, nor D is in the set m_extra_opaque. To implement this feature, this class has a field + m_module_idx that is not none when this rule should be applied. + */ + bool is_opaque(definition const & d) const { + lean_assert(d.is_definition()); + if (d.is_theorem()) return true; // theorems are always opaque + if (m_extra_opaque.contains(d.get_name())) return true; // extra_opaque set overrides opaque flag + if (!d.is_opaque()) return false; // d is a transparent definition + if (m_module_idx && d.get_module_idx() == *m_module_idx) return false; // the opaque definitions in module_idx are considered transparent + return true; // d is opaque + } + + /** \brief Expand \c e if it is non-opaque constant with weight >= w */ + expr unfold_name_core(expr e, unsigned w) { + if (is_constant(e)) { + if (auto d = m_env.find(const_name(e))) { + if (d->is_definition() && !is_opaque(*d) && d->get_weight() >= w) + return unfold_name_core(instantiate_params(d->get_value(), d->get_params(), const_level_params(e)), w); + } + } + return e; + } + + /** + \brief Expand constants and application where the function is a constant. + + The unfolding is only performend if the constant corresponds to + a non-opaque definition with weight >= w. + */ + expr unfold_names(expr const & e, unsigned w) { + if (is_app(e)) { + expr const * it = &e; + while (is_app(*it)) { + it = &(app_fn(*it)); + } + expr f = unfold_name_core(*it, w); + if (is_eqp(f, *it)) { + return e; + } else { + buffer args; + expr const * it = &e; + while (is_app(*it)) { + args.push_back(app_arg(*it)); + it = &(app_fn(*it)); + } + return mk_rev_app(f, args.size(), args.data()); + } + } else { + return unfold_name_core(e, w); + } + } + + /** \brief Auxiliary method for \c is_delta */ + optional is_delta_core(expr const & e) { + if (is_constant(e)) { + if (auto d = m_env.find(const_name(e))) + if (d->is_definition() && !is_opaque(*d)) + return d; + } + return none_definition(); + } + + /** + \brief Return some definition \c d iff \c e is a target for delta-reduction, and the given definition is the one + to be expanded. + */ + optional is_delta(expr const & e) { + if (is_app(e)) { + expr const * it = &e; + while (is_app(*it)) { + it = &(app_fn(*it)); + } + return is_delta_core(*it); + } else { + return is_delta_core(e); + } + } + + /** + \brief Weak head normal form core procedure that perform delta reduction for non-opaque constants with + weight greater than or equal to \c w. + + This method is based on whnf_core(expr const &) and \c unfold_names. + + \remark This method does not use normalization extensions attached in the environment. + */ + expr whnf_core(expr e, unsigned w, context & c) { + while (true) { + expr new_e = unfold_names(whnf_core(e, c), w); + if (is_eqp(e, new_e)) + return e; + e = new_e; + } + } + + /** \brief Put expression \c t in weak head normal form */ + virtual expr whnf(expr const & e_prime, context & c) { + expr e = e_prime; + // check cache + if (m_memoize) { + e = max_sharing(e); + auto it = m_whnf_cache.find(e); + if (it != m_whnf_cache.end()) + return it->second; + } + + expr t = e; + while (true) { + expr t1 = whnf_core(t, 0, c); + auto new_t = norm_ext(t1, c); + if (new_t) { + t = *new_t; + } else { + if (m_memoize) + m_whnf_cache.insert(mk_pair(e, t1)); + return t1; + } + } + } + + /** \brief Eta-expand \c s and check if it is definitionally equal to \c t. */ + bool try_eta(expr const & t, expr const & s, context & c, delayed_justification & jst) { + lean_assert(is_lambda(t)); + lean_assert(!is_lambda(s)); + expr t_s = whnf(c.infer_type(s), c); + if (is_pi(t_s)) { + // new_s := lambda x : domain(t_s), s x + expr new_s = mk_lambda(c.mk_fresh_name(), binder_domain(t_s), mk_app(lift_free_vars(s, 1), mk_var(0))); + return is_def_eq_core(t, new_s, c, jst); + } else { + return false; + } + } + + /** + \brief Given lambda/Pi expressions \c t and \c s, return true iff \c t is convertible to \c s. + + The argument \c def_eq is used to decide whether the body of the binder is checked for + definitional equality or convertability. + + If t and s are lambda expressions, then then t is convertible to s + iff + domain(t) is definitionally equal to domain(s) + and + body(t) is definitionally equal to body(s) + + For Pi expressions, it is slighly different. + If t and s are Pi expressions, then then t is convertible to s + iff + domain(t) is definitionally equal to domain(s) + and + body(t) is convertible to body(s) + */ + bool is_conv_binder(expr t, expr s, bool def_eq, context & c, delayed_justification & jst) { + lean_assert(t.kind() == s.kind()); + lean_assert(is_binder(t)); + expr_kind k = t.kind(); + buffer subst; + do { + expr var_t_type = instantiate(binder_domain(t), subst.size(), subst.data()); + expr var_s_type = instantiate(binder_domain(s), subst.size(), subst.data()); + if (!is_def_eq_core(var_t_type, var_s_type, c, jst)) + return false; + subst.push_back(mk_local(c.mk_fresh_name() + binder_name(s), var_s_type)); + t = binder_body(t); + s = binder_body(s); + } while (t.kind() == k && s.kind() == k); + return is_conv(instantiate(t, subst.size(), subst.data()), instantiate(s, subst.size(), subst.data()), def_eq, c, jst); + } + + /** + \brief This is an auxiliary method for is_conv. It handles the "easy cases". + + If \c def_eq is true, then it checks for definitional equality. + */ + lbool quick_is_conv(expr const & t, expr const & s, bool def_eq, context & c, delayed_justification & jst) { + if (t == s) + return l_true; // t and s are structurally equal + if (is_meta(t) || is_meta(s)) { + // if t or s is a metavariable (or the application of a metavariable), then add constraint + if (def_eq) + c.add_cnstr(mk_eq_cnstr(t, s, jst.get())); + else + c.add_cnstr(mk_conv_cnstr(t, s, jst.get())); + return l_true; + } + if (t.kind() == s.kind()) { + switch (t.kind()) { + case expr_kind::Lambda: + return to_lbool(is_conv_binder(t, s, true, c, jst)); + case expr_kind::Pi: + return to_lbool(is_conv_binder(t, s, def_eq, c, jst)); + case expr_kind::Sort: + // t and s are Sorts + if (is_trivial(sort_level(t), sort_level(s)) && (!def_eq || is_trivial(sort_level(s), sort_level(t)))) + return l_true; + c.add_cnstr(mk_level_cnstr(sort_level(t), sort_level(s), jst.get())); + if (def_eq) + c.add_cnstr(mk_level_cnstr(sort_level(s), sort_level(t), jst.get())); + return l_true; + case expr_kind::Meta: + lean_unreachable(); // LCOV_EXCL_LINE + case expr_kind::Var: case expr_kind::Local: case expr_kind::App: + case expr_kind::Constant: case expr_kind::Macro: case expr_kind::Let: + // We do not handle these cases in this method. + break; + } + } + return l_undef; // This is not an "easy case" + } + + /** + \brief Return true if arguments of \c t are definitionally equal to arguments of \c s. + Constraint generation is disabled when performing this test. + This method is used to implement an optimization in the method \c is_conv. + */ + bool is_def_eq_args(expr t, expr s, context & c, delayed_justification & jst) { + context::disable_cnstrs_scope scope(c); + try { + while (is_app(t) && is_app(s)) { + if (!is_def_eq_core(app_arg(t), app_arg(s), c, jst)) + return false; + t = app_fn(t); + s = app_fn(s); + } + return !is_app(t) && !is_app(s); + } catch (add_cnstr_exception &) { + return false; + } + } + + /** + \brief If def_eq is false, then return true iff t is convertible to s. + If def_eq is true, then return true iff t is definitionally equal to s. + */ + bool is_conv(expr const & t, expr const & s, bool def_eq, context & c, delayed_justification & jst) { + check_system("is_convertible"); + lbool r = quick_is_conv(t, s, def_eq, c, jst); + if (r != l_undef) return r == l_true; + + // apply whnf (without using delta-reduction or normalizer extensions) + expr t_n = whnf_core(t, c); + expr s_n = whnf_core(s, c); + if (!is_eqp(t_n, t) || !is_eqp(s_n, s)) { + r = quick_is_conv(t_n, s_n, def_eq, c, jst); + if (r != l_undef) return r == l_true; + } + + // lazy delta-reduction and then normalizer extensions + while (true) { + // first, keep applying lazy delta-reduction while applicable + while (true) { + auto d_t = is_delta(t_n); + auto d_s = is_delta(s_n); + if (!d_t && !d_s) { + break; + } else if (d_t && !d_s) { + t_n = whnf_core(unfold_names(t_n, 0), c); + } else if (!d_t && d_s) { + s_n = whnf_core(unfold_names(s_n, 0), c); + } else if (d_t->get_weight() > d_s->get_weight()) { + t_n = whnf_core(unfold_names(t_n, d_s->get_weight() + 1), c); + } else if (d_t->get_weight() < d_s->get_weight()) { + s_n = whnf_core(unfold_names(s_n, d_t->get_weight() + 1), c); + } else { + lean_assert(d_t && d_s && d_t->get_weight() == d_s->get_weight()); + // If t_n and s_n are both applications of the same (non-opaque) definition, + // then we try to check if their arguments are definitionally equal. + // If they are, then t_n and s_n must be definitionally equal, and we can + // skip the delta-reduction step. + if (is_app(t_n) && is_app(s_n) && + is_eqp(*d_t, *d_s) && // same definition + !is_opaque(*d_t) && // if d_t is opaque, we don't need to try this optimization + d_t->use_conv_opt() && // the flag use_conv_opt() can be used to disable this optimization + is_def_eq_args(t_n, s_n, c, jst)) { + return true; + } + t_n = whnf_core(unfold_names(t_n, d_t->get_weight() - 1), c); + s_n = whnf_core(unfold_names(s_n, d_s->get_weight() - 1), c); + } + r = quick_is_conv(t_n, s_n, def_eq, c, jst); + if (r != l_undef) return r == l_true; + } + // try normalizer extensions + auto new_t_n = norm_ext(t_n, c); + auto new_s_n = norm_ext(s_n, c); + if (!new_t_n && !new_s_n) + break; // t_n and s_n are in weak head normal form + if (new_t_n) + t_n = whnf_core(*new_t_n, c); + if (new_s_n) + s_n = whnf_core(*new_s_n, c); + r = quick_is_conv(t_n, s_n, def_eq, c, jst); + if (r != l_undef) return r == l_true; + } + + // At this point, t_n and s_n are in weak head normal form (modulo meta-variables) + + if (m_env.eta()) { + lean_assert(!is_lambda(t_n) || !is_lambda(s_n)); + // Eta-reduction support + if ((is_lambda(t_n) && try_eta(t_n, s_n, c, jst)) || + (is_lambda(s_n) && try_eta(s_n, t_n, c, jst))) + return true; + } + + if (is_app(t_n) && is_app(s_n)) { + expr it1 = t_n; + expr it2 = s_n; + bool ok = true; + do { + if (!is_def_eq_core(app_arg(it1), app_arg(it2), c, jst)) { + ok = false; + break; + } + it1 = app_fn(it1); + it2 = app_fn(it2); + } while (is_app(it1) && is_app(it2)); + if (ok && is_def_eq_core(it1, it2, c, jst)) + return true; + } + + if (m_env.proof_irrel()) { + // Proof irrelevance support + expr t_type = c.infer_type(t); + return is_prop(t_type, c) && is_def_eq_core(t_type, c.infer_type(s), c, jst); + } + + return false; + } + + bool is_prop(expr const & e, context & c) { + return whnf(c.infer_type(e), c) == Bool; + } + + bool is_def_eq_core(expr const & t, expr const & s, context & c, delayed_justification & j) { + return is_conv(t, s, true, c, j); + } + + virtual bool is_conv(expr const & t, expr const & s, context & c, delayed_justification & j) { + return is_conv(max_sharing(t), max_sharing(s), false, c, j); + } + + virtual bool is_def_eq(expr const & t, expr const & s, context & c, delayed_justification & j) { + return is_def_eq_core(max_sharing(t), max_sharing(s), c, j); + } +}; + +std::unique_ptr mk_default_converter(environment const & env, optional mod_idx, + bool memoize, name_set const & extra_opaque) { + return std::unique_ptr(new default_converter(env, mod_idx, memoize, extra_opaque)); +} +} diff --git a/src/kernel/converter.h b/src/kernel/converter.h new file mode 100644 index 000000000..2f0e87525 --- /dev/null +++ b/src/kernel/converter.h @@ -0,0 +1,55 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "kernel/environment.h" + +namespace lean { +/** \brief Object to simulate delayed justification creation. */ +class delayed_justification { + optional m_jst; + std::function m_mk; +public: + template delayed_justification(Mk && mk):m_mk(mk) {} + justification get() { if (!m_jst) { m_jst = m_mk(); } return *m_jst; } +}; + +/** \brief Auxiliary exception used to sign that constraints cannot be created when \c m_cnstrs_enabled flag is false. */ +struct add_cnstr_exception {}; + +class converter { +public: + /** \brief Abstract context that must be provided to a converter object. */ + class context { + virtual bool enable_cnstrs(bool flag) = 0; + public: + virtual name mk_fresh_name() = 0; + virtual expr infer_type(expr const & e) = 0; + virtual void add_cnstr(constraint const & c) = 0; + class disable_cnstrs_scope { + context & m_ctx; + bool m_old; + public: + disable_cnstrs_scope(context & ctx):m_ctx(ctx), m_old(m_ctx.enable_cnstrs(false)) {} + ~disable_cnstrs_scope() { m_ctx.enable_cnstrs(m_old); } + }; + }; + + virtual ~converter() {} + + virtual expr whnf(expr const & e, context & c) = 0; + virtual bool is_conv(expr const & t, expr const & s, context & c, delayed_justification & j) = 0; + virtual bool is_def_eq(expr const & t, expr const & s, context & c, delayed_justification & j) = 0; + bool is_conv(expr const & t, expr const & s, context & c); + bool is_def_eq(expr const & t, expr const & s, context & c); +}; + +std::unique_ptr mk_dummy_converter(); +std::unique_ptr mk_default_converter(environment const & env, + optional mod_idx = optional(), + bool memoize = true, + name_set const & extra_opaque = name_set()); +} diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 30a07ff41..1e55e55fe 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -1,5 +1,5 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013-14 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura @@ -33,28 +33,23 @@ void no_constraint_handler::add_cnstr(constraint const &) { /** \brief Auxiliary functional object used to implement type checker. */ struct type_checker::imp { - environment m_env; - name_generator m_gen; - constraint_handler & m_chandler; - optional m_module_idx; - bool m_memoize; - name_set m_extra_opaque; - max_sharing_fn m_sharing; - expr_map m_infer_type_cache; - expr_map m_whnf_core_cache; - expr_map m_whnf_cache; - // The following mapping is used to store the relationship - // between temporary expressions created during type checking and the original ones. - // We need that to be able to produce error messages containing position information. - expr_map m_trace; + /** \brief Interface type_checker <-> converter */ + class converter_context : public converter::context { + imp & m_imp; + virtual bool enable_cnstrs(bool flag) { + bool r = m_imp.m_cnstrs_enabled; + m_imp.m_cnstrs_enabled = flag; + return r; + } - // temp flag - bool m_cnstrs_enabled; - - imp(environment const & env, name_generator const & g, constraint_handler & h, - optional mod_idx, bool memoize, name_set const & extra_opaque): - m_env(env), m_gen(g), m_chandler(h), m_module_idx(mod_idx), m_memoize(memoize), m_extra_opaque(extra_opaque), m_cnstrs_enabled(true) {} + public: + converter_context(imp & i):m_imp(i) {} + virtual name mk_fresh_name() { return m_imp.m_gen.next(); } + virtual expr infer_type(expr const & e) { return m_imp.infer_type(e); } + virtual void add_cnstr(constraint const & c) { m_imp.add_cnstr(c); } + }; + /** \brief Interface type_checker <-> macro & normalizer_extension */ class type_checker_context : public extension_context { imp & m_imp; public: @@ -66,33 +61,32 @@ struct type_checker::imp { virtual void add_cnstr(constraint const & c) { m_imp.add_cnstr(c); } }; - bool check_memoized(expr const & e) const { return !m_memoize || m_sharing.already_processed(e); } - expr max_sharing(expr const & e) { return m_memoize ? m_sharing(e) : e; } - expr instantiate(expr const & e, unsigned n, expr const * s) { return max_sharing(lean::instantiate(e, n, s)); } - expr instantiate(expr const & e, expr const & s) { return max_sharing(lean::instantiate(e, s)); } - expr mk_app(expr const & f, unsigned num, expr const * args) { return max_sharing(lean::mk_app(f, num, args)); } - expr mk_app(expr const & f, expr const & a) { return max_sharing(lean::mk_app(f, a)); } - expr mk_rev_app(expr const & f, unsigned num, expr const * args) { return max_sharing(lean::mk_rev_app(f, num, args)); } - expr mk_app_vars(expr const & f, unsigned num) { return max_sharing(lean::mk_app_vars(f, num)); } + environment m_env; + name_generator m_gen; + constraint_handler & m_chandler; + std::unique_ptr m_conv; + expr_map m_infer_type_cache; + converter_context m_conv_ctx; + type_checker_context m_tc_ctx; + // The following mapping is used to store the relationship + // between temporary expressions created during type checking and the original ones. + // We need that to be able to produce error messages containing position information. + expr_map m_trace; + bool m_memoize; + // temp flag + bool m_cnstrs_enabled; + + imp(environment const & env, name_generator const & g, constraint_handler & h, std::unique_ptr && conv, bool memoize): + m_env(env), m_gen(g), m_chandler(h), m_conv(std::move(conv)), m_conv_ctx(*this), m_tc_ctx(*this), + m_memoize(memoize), m_cnstrs_enabled(true) {} + optional expand_macro(expr const & m) { lean_assert(is_macro(m)); - type_checker_context ctx(*this); - if (auto new_m = macro_def(m).expand(macro_num_args(m), macro_args(m), ctx)) + if (auto new_m = macro_def(m).expand(macro_num_args(m), macro_args(m), m_tc_ctx)) return some_expr(max_sharing(*new_m)); else return none_expr(); } - expr instantiate_params(expr const & e, param_names const & ps, levels const & ls) { - return max_sharing(lean::instantiate_params(e, ps, ls)); - } - /** \brief Apply normalizer extensions to \c e. */ - optional norm_ext(expr const & e) { - type_checker_context ctx(*this); - if (auto new_e = m_env.norm_ext()(e, ctx)) - return some_expr(max_sharing(*new_e)); - else - return none_expr(); - } /** \brief Add entry new_e -> old_e in the traceability mapping */ void add_trace(expr const & old_e, expr const & new_e) { @@ -125,209 +119,6 @@ struct type_checker::imp { return mk_pair(instantiate_with_trace(binder_body(e), local), local); } - /** \brief Weak head normal form core procedure. It does not perform delta reduction nor normalization extensions. */ - expr whnf_core(expr const & e) { - check_system("whnf"); - lean_assert(check_memoized(e)); - - // handle easy cases - switch (e.kind()) { - case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: - case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Constant: - return e; - case expr_kind::Macro: case expr_kind::Let: case expr_kind::App: - break; - } - - // check cache - if (m_memoize) { - auto it = m_whnf_core_cache.find(e); - if (it != m_whnf_core_cache.end()) - return it->second; - } - - // do the actual work - expr r; - switch (e.kind()) { - case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: - case expr_kind::Lambda: case expr_kind::Pi: case expr_kind::Constant: - lean_unreachable(); // LCOV_EXCL_LINE - case expr_kind::Macro: - if (auto m = expand_macro(e)) - r = whnf_core(*m); - else - r = e; - break; - case expr_kind::Let: - r = whnf_core(instantiate(let_body(e), let_value(e))); - break; - case expr_kind::App: { - buffer args; - expr const * it = &e; - while (is_app(*it)) { - args.push_back(app_arg(*it)); - it = &(app_fn(*it)); - } - expr f = whnf_core(*it); - if (is_lambda(f)) { - unsigned m = 1; - unsigned num_args = args.size(); - while (is_lambda(binder_body(f)) && m < num_args) { - f = binder_body(f); - m++; - } - lean_assert(m <= num_args); - r = whnf_core(mk_rev_app(instantiate(binder_body(f), m, args.data() + (num_args - m)), num_args - m, args.data())); - } else { - r = is_eqp(f, *it) ? e : mk_rev_app(f, args.size(), args.data()); - } - break; - }} - - if (m_memoize) - m_whnf_core_cache.insert(mk_pair(e, r)); - return r; - } - - /** - \brief Predicate for deciding whether \c d is an opaque definition or not. - - Here is the basic idea: - - 1) Each definition has an opaque flag. This flag cannot be modified after a definition is added to the environment. - The opaque flag affects the convertability check. The idea is to minimize the number of delta-reduction steps. - We also believe it increases the modularity of Lean developments by minimizing the dependency on how things are defined. - We should view non-opaque definitions as "inline definitions" used in programming languages such as C++. - - 2) Whenever type checking an expression, the user can provide an additional set of definition names (m_extra_opaque) that - should be considered opaque. Note that, if \c t type checks when using an extra_opaque set S, then t also type checks - (modulo resource constraints) with the empty set. Again, the purpose of extra_opaque is to mimimize the number - of delta-reduction steps. - - 3) To be able to prove theorems about an opaque definition, we treat an opaque definition D in a module M as - transparent when we are type checking another definition/theorem D' also in M. This rule only applies if - D is not a theorem, nor D is in the set m_extra_opaque. To implement this feature, this class has a field - m_module_idx that is not none when this rule should be applied. - */ - bool is_opaque(definition const & d) const { - lean_assert(d.is_definition()); - if (d.is_theorem()) return true; // theorems are always opaque - if (m_extra_opaque.contains(d.get_name())) return true; // extra_opaque set overrides opaque flag - if (!d.is_opaque()) return false; // d is a transparent definition - if (m_module_idx && d.get_module_idx() == *m_module_idx) return false; // the opaque definitions in module_idx are considered transparent - return true; // d is opaque - } - - /** \brief Expand \c e if it is non-opaque constant with weight >= w */ - expr unfold_name_core(expr e, unsigned w) { - if (is_constant(e)) { - if (auto d = m_env.find(const_name(e))) { - if (d->is_definition() && !is_opaque(*d) && d->get_weight() >= w) - return unfold_name_core(instantiate_params(d->get_value(), d->get_params(), const_level_params(e)), w); - } - } - return e; - } - - /** - \brief Expand constants and application where the function is a constant. - - The unfolding is only performend if the constant corresponds to - a non-opaque definition with weight >= w. - */ - expr unfold_names(expr const & e, unsigned w) { - if (is_app(e)) { - expr const * it = &e; - while (is_app(*it)) { - it = &(app_fn(*it)); - } - expr f = unfold_name_core(*it, w); - if (is_eqp(f, *it)) { - return e; - } else { - buffer args; - expr const * it = &e; - while (is_app(*it)) { - args.push_back(app_arg(*it)); - it = &(app_fn(*it)); - } - return mk_rev_app(f, args.size(), args.data()); - } - } else { - return unfold_name_core(e, w); - } - } - - /** \brief Auxiliary method for \c is_delta */ - optional is_delta_core(expr const & e) { - if (is_constant(e)) { - if (auto d = m_env.find(const_name(e))) - if (d->is_definition() && !is_opaque(*d)) - return d; - } - return none_definition(); - } - - /** - \brief Return some definition \c d iff \c e is a target for delta-reduction, and the given definition is the one - to be expanded. - */ - optional is_delta(expr const & e) { - if (is_app(e)) { - expr const * it = &e; - while (is_app(*it)) { - it = &(app_fn(*it)); - } - return is_delta_core(*it); - } else { - return is_delta_core(e); - } - } - - /** - \brief Weak head normal form core procedure that perform delta reduction for non-opaque constants with - weight greater than or equal to \c w. - - This method is based on whnf_core(expr const &) and \c unfold_names. - - \remark This method does not use normalization extensions attached in the environment. - */ - expr whnf_core(expr e, unsigned w) { - while (true) { - expr new_e = unfold_names(whnf_core(e), w); - if (is_eqp(e, new_e)) - return e; - e = new_e; - } - } - - /** \brief Put expression \c e in weak head normal form */ - expr whnf(expr e) { - // check cache - if (m_memoize) { - e = max_sharing(e); - auto it = m_whnf_cache.find(e); - if (it != m_whnf_cache.end()) - return it->second; - } - - expr t = e; - while (true) { - expr t1 = whnf_core(t, 0); - auto new_t = norm_ext(t1); - if (new_t) { - t = *new_t; - } else { - if (m_memoize) - m_whnf_cache.insert(mk_pair(e, t1)); - return t1; - } - } - } - - /** \brief Auxiliary exception used to sign that constraints cannot be created when \c m_cnstrs_enabled flag is false. */ - struct add_cnstr_exception {}; - /** \brief Add given constraint to the constraint handler m_chandler. */ void add_cnstr(constraint const & c) { if (m_cnstrs_enabled) @@ -336,234 +127,14 @@ struct type_checker::imp { throw add_cnstr_exception(); } - /** \brief Object to simulate delayed justification creation. */ - class delayed_justification { - optional m_jst; - std::function m_mk; - public: - template delayed_justification(Mk && mk):m_mk(mk) {} - justification get() { if (!m_jst) { m_jst = m_mk(); } return *m_jst; } - }; - - /** \brief Eta-expand \c s and check if it is definitionally equal to \c t. */ - bool try_eta(expr const & t, expr const & s, delayed_justification & jst) { - lean_assert(is_lambda(t)); - lean_assert(!is_lambda(s)); - expr t_s = whnf(infer_type(s)); - if (is_pi(t_s)) { - // new_s := lambda x : domain(t_s), s x - expr new_s = mk_lambda(m_gen.next(), binder_domain(t_s), mk_app(lift_free_vars(s, 1), mk_var(0))); - return is_def_eq(t, new_s, jst); - } else { - return false; - } - } - - /** - \brief Given lambda/Pi expressions \c t and \c s, return true iff \c t is convertible to \c s. - - The argument \c def_eq is used to decide whether the body of the binder is checked for - definitional equality or convertability. - - If t and s are lambda expressions, then then t is convertible to s - iff - domain(t) is definitionally equal to domain(s) - and - body(t) is definitionally equal to body(s) - - For Pi expressions, it is slighly different. - If t and s are Pi expressions, then then t is convertible to s - iff - domain(t) is definitionally equal to domain(s) - and - body(t) is convertible to body(s) - */ - bool is_conv_binder(expr t, expr s, bool def_eq, delayed_justification & jst) { - lean_assert(t.kind() == s.kind()); - lean_assert(is_binder(t)); - expr_kind k = t.kind(); - buffer subst; - do { - expr var_t_type = instantiate(binder_domain(t), subst.size(), subst.data()); - expr var_s_type = instantiate(binder_domain(s), subst.size(), subst.data()); - if (!is_def_eq(var_t_type, var_s_type, jst)) - return false; - subst.push_back(mk_local(m_gen.next() + binder_name(s), var_s_type)); - t = binder_body(t); - s = binder_body(s); - } while (t.kind() == k && s.kind() == k); - return is_conv(instantiate(t, subst.size(), subst.data()), instantiate(s, subst.size(), subst.data()), def_eq, jst); - } - - /** - \brief This is an auxiliary method for is_conv. It handles the "easy cases". - - If \c def_eq is true, then it checks for definitional equality. - */ - lbool quick_is_conv(expr const & t, expr const & s, bool def_eq, delayed_justification & jst) { - if (t == s) - return l_true; // t and s are structurally equal - if (is_meta(t) || is_meta(s)) { - // if t or s is a metavariable (or the application of a metavariable), then add constraint - if (def_eq) - add_cnstr(mk_eq_cnstr(t, s, jst.get())); - else - add_cnstr(mk_conv_cnstr(t, s, jst.get())); - return l_true; - } - if (t.kind() == s.kind()) { - switch (t.kind()) { - case expr_kind::Lambda: - return to_lbool(is_conv_binder(t, s, true, jst)); - case expr_kind::Pi: - return to_lbool(is_conv_binder(t, s, def_eq, jst)); - case expr_kind::Sort: - // t and s are Sorts - if (is_trivial(sort_level(t), sort_level(s)) && (!def_eq || is_trivial(sort_level(s), sort_level(t)))) - return l_true; - add_cnstr(mk_level_cnstr(sort_level(t), sort_level(s), jst.get())); - if (def_eq) - add_cnstr(mk_level_cnstr(sort_level(s), sort_level(t), jst.get())); - return l_true; - case expr_kind::Meta: - lean_unreachable(); // LCOV_EXCL_LINE - case expr_kind::Var: case expr_kind::Local: case expr_kind::App: - case expr_kind::Constant: case expr_kind::Macro: case expr_kind::Let: - // We do not handle these cases in this method. - break; - } - } - return l_undef; // This is not an "easy case" - } - - /** - \brief Return true if arguments of \c t are definitionally equal to arguments of \c s. - Constraint generation is disabled when performing this test. - This method is used to implement an optimization in the method \c is_conv. - */ - bool is_def_eq_args(expr t, expr s, delayed_justification & jst) { - flet disable_cnstrs(m_cnstrs_enabled, false); // disable constraint generation when processing arguments. - try { - while (is_app(t) && is_app(s)) { - if (!is_def_eq(app_arg(t), app_arg(s), jst)) - return false; - t = app_fn(t); - s = app_fn(s); - } - return !is_app(t) && !is_app(s); - } catch (add_cnstr_exception &) { - return false; - } - } - - /** - \brief If def_eq is false, then return true iff t is convertible to s. - If def_eq is true, then return true iff t is definitionally equal to s. - */ - bool is_conv(expr const & t, expr const & s, bool def_eq, delayed_justification & jst) { - check_system("is_convertible"); - lbool r = quick_is_conv(t, s, def_eq, jst); - if (r != l_undef) return r == l_true; - - // apply whnf (without using delta-reduction or normalizer extensions) - expr t_n = whnf_core(t); - expr s_n = whnf_core(s); - if (!is_eqp(t_n, t) || !is_eqp(s_n, s)) { - r = quick_is_conv(t_n, s_n, def_eq, jst); - if (r != l_undef) return r == l_true; - } - - // lazy delta-reduction and then normalizer extensions - while (true) { - // first, keep applying lazy delta-reduction while applicable - while (true) { - auto d_t = is_delta(t_n); - auto d_s = is_delta(s_n); - if (!d_t && !d_s) { - break; - } else if (d_t && !d_s) { - t_n = whnf_core(unfold_names(t_n, 0)); - } else if (!d_t && d_s) { - s_n = whnf_core(unfold_names(s_n, 0)); - } else if (d_t->get_weight() > d_s->get_weight()) { - t_n = whnf_core(unfold_names(t_n, d_s->get_weight() + 1)); - } else if (d_t->get_weight() < d_s->get_weight()) { - s_n = whnf_core(unfold_names(s_n, d_t->get_weight() + 1)); - } else { - lean_assert(d_t && d_s && d_t->get_weight() == d_s->get_weight()); - // If t_n and s_n are both applications of the same (non-opaque) definition, - // then we try to check if their arguments are definitionally equal. - // If they are, then t_n and s_n must be definitionally equal, and we can - // skip the delta-reduction step. - if (is_app(t_n) && is_app(s_n) && - is_eqp(*d_t, *d_s) && // same definition - !is_opaque(*d_t) && // if d_t is opaque, we don't need to try this optimization - d_t->use_conv_opt() && // the flag use_conv_opt() can be used to disable this optimization - is_def_eq_args(t_n, s_n, jst)) { - return true; - } - t_n = whnf_core(unfold_names(t_n, d_t->get_weight() - 1)); - s_n = whnf_core(unfold_names(s_n, d_s->get_weight() - 1)); - } - r = quick_is_conv(t_n, s_n, def_eq, jst); - if (r != l_undef) return r == l_true; - } - // try normalizer extensions - auto new_t_n = norm_ext(t_n); - auto new_s_n = norm_ext(s_n); - if (!new_t_n && !new_s_n) - break; // t_n and s_n are in weak head normal form - if (new_t_n) - t_n = whnf_core(*new_t_n); - if (new_s_n) - s_n = whnf_core(*new_s_n); - r = quick_is_conv(t_n, s_n, def_eq, jst); - if (r != l_undef) return r == l_true; - } - - // At this point, t_n and s_n are in weak head normal form (modulo meta-variables) - - if (m_env.eta()) { - lean_assert(!is_lambda(t_n) || !is_lambda(s_n)); - // Eta-reduction support - if ((is_lambda(t_n) && try_eta(t_n, s_n, jst)) || - (is_lambda(s_n) && try_eta(s_n, t_n, jst))) - return true; - } - - if (is_app(t_n) && is_app(s_n)) { - expr it1 = t_n; - expr it2 = s_n; - bool ok = true; - do { - if (!is_def_eq(app_arg(it1), app_arg(it2), jst)) { - ok = false; - break; - } - it1 = app_fn(it1); - it2 = app_fn(it2); - } while (is_app(it1) && is_app(it2)); - if (ok && is_def_eq(it1, it2, jst)) - return true; - } - - if (m_env.proof_irrel()) { - // Proof irrelevance support - expr t_type = infer_type(t); - return is_prop(t_type) && is_def_eq(t_type, infer_type(s), jst); - } - - return false; - } - /** \brief Return true iff \c t is convertible to s */ bool is_conv(expr const & t, expr const & s, delayed_justification & jst) { - return is_conv(max_sharing(t), max_sharing(s), false, jst); + return m_conv->is_conv(t, s, m_conv_ctx, jst); } /** \brief Return true iff \c t and \c s are definitionally equal */ bool is_def_eq(expr const & t, expr const & s, delayed_justification & jst) { - return is_conv(max_sharing(t), max_sharing(s), true, jst); + return m_conv->is_conv(t, s, m_conv_ctx, jst); } /** \brief Return true iff \c e is a proposition */ @@ -788,8 +359,7 @@ struct type_checker::imp { buffer arg_types; for (unsigned i = 0; i < macro_num_args(e); i++) arg_types.push_back(infer_type_core(macro_arg(e, i), infer_only)); - type_checker_context ctx(*this); - r = macro_def(e).get_type(macro_num_args(e), macro_args(e), arg_types.data(), ctx); + r = macro_def(e).get_type(macro_num_args(e), macro_args(e), arg_types.data(), m_tc_ctx); if (!infer_only && macro_def(e).trust_level() <= m_env.trust_lvl()) { optional m = expand_macro(e); if (!m) @@ -856,25 +426,18 @@ struct type_checker::imp { expr infer_type(expr const & e) { return infer_type_core(e, true); } expr check(expr const & e) { return infer_type_core(e, false); } - bool is_conv(expr const & t, expr const & s) { - delayed_justification j([]() { return justification(); }); - return is_conv(t, s, j); - } - bool is_def_eq(expr const & t, expr const & s) { - delayed_justification j([]() { return justification(); }); - return is_conv(t, s, j); - } + bool is_conv(expr const & t, expr const & s) { return m_conv->is_conv(t, s, m_conv_ctx); } + bool is_def_eq(expr const & t, expr const & s) { return m_conv->is_def_eq(t, s, m_conv_ctx); } + expr whnf(expr const & t) { return m_conv->whnf(t, m_conv_ctx); } }; no_constraint_handler g_no_constraint_handler; -type_checker::type_checker(environment const & env, name_generator const & g, constraint_handler & h, - optional mod_idx, bool memoize, name_set const & extra_opaque): - m_ptr(new imp(env, g, h, mod_idx, memoize, extra_opaque)) {} +type_checker::type_checker(environment const & env, name_generator const & g, constraint_handler & h, std::unique_ptr && conv, bool memoize): + m_ptr(new imp(env, g, h, std::move(conv), memoize)) {} -type_checker::type_checker(environment const & env, name_generator const & g, - optional mod_idx, bool memoize, name_set const & extra_opaque): - type_checker(env, g, g_no_constraint_handler, mod_idx, memoize, extra_opaque) {} +type_checker::type_checker(environment const & env, name_generator const & g, std::unique_ptr && conv, bool memoize): + type_checker(env, g, g_no_constraint_handler, std::move(conv), memoize) {} type_checker::~type_checker() {} expr type_checker::infer(expr const & t) { return m_ptr->infer_type(t); } @@ -917,17 +480,16 @@ certified_definition check(environment const & env, name_generator const & g, de check_no_mlocal(env, d.get_value()); check_name(env, d.get_name()); - optional midx; - if (!d.is_definition() || d.is_opaque()) - midx = optional(d.get_module_idx()); - simple_constraint_handler chandler; - type_checker checker(env, g, chandler, midx, memoize, extra_opaque); - - checker.check(d.get_type()); + type_checker checker1(env, g, chandler, mk_default_converter(env, optional(), memoize, extra_opaque)); + checker1.check(d.get_type()); if (d.is_definition()) { - expr val_type = checker.check(d.get_value()); - if (!checker.is_conv(val_type, d.get_type())) { + optional midx; + if (d.is_opaque()) + midx = optional(d.get_module_idx()); + type_checker checker2(env, g, chandler, mk_default_converter(env, midx, memoize, extra_opaque)); + expr val_type = checker2.check(d.get_value()); + if (!checker2.is_conv(val_type, d.get_type())) { throw_kernel_exception(env, d.get_value(), [=](formatter const & fmt, options const & o) { return pp_def_type_mismatch(fmt, env, o, d.get_name(), d.get_type(), val_type); diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index e3da870d2..499a4db10 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -1,5 +1,5 @@ /* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Copyright (c) 2013-14 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "util/name_set.h" #include "kernel/environment.h" #include "kernel/constraint.h" +#include "kernel/converter.h" namespace lean { class constraint_handler { @@ -53,14 +54,14 @@ public: - memoize: inferred types are memoized/cached - extra_opaque: additional definitions that should be treated as opaque */ - type_checker(environment const & env, name_generator const & g, constraint_handler & h, - optional mod_idx = optional(), bool memoize = false, name_set const & extra_opaque = name_set()); + type_checker(environment const & env, name_generator const & g, constraint_handler & h, std::unique_ptr && conv, bool memoize = true); + type_checker(environment const & env, name_generator const & g, constraint_handler & h, bool memoize = true):type_checker(env, g, h, mk_default_converter(env), memoize) {} /** \brief Similar to the previous constructor, but if a method tries to create a constraint, then an exception is thrown. */ - type_checker(environment const & env, name_generator const & g, - optional mod_idx = optional(), bool memoize = false, name_set const & extra_opaque = name_set()); + type_checker(environment const & env, name_generator const & g, std::unique_ptr && conv, bool memoize = true); + type_checker(environment const & env, name_generator const & g, bool memoize = true):type_checker(env, g, mk_default_converter(env), memoize) {} ~type_checker(); /** diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp index 2988ae27f..3f6bc98ed 100644 --- a/src/tests/kernel/environment.cpp +++ b/src/tests/kernel/environment.cpp @@ -99,7 +99,7 @@ static void tst2() { lean_assert(checker.is_conv(f98(c1, id(Bool, id(Bool, c2))), f97(f97(c1, id(Bool, c2)), f97(c2, c1)))); name_set s; s.insert(name(base, 96)); - type_checker checker2(env, name_generator("tmp"), optional(), true, s); + type_checker checker2(env, name_generator("tmp"), mk_default_converter(env, optional(), true, s)); lean_assert_eq(checker2.whnf(f98(c1, c2)), f96(f96(f97(c1, c2), f97(c2, c1)), f96(f97(c2, c1), f97(c1, c2)))); }