From dcc94dde825e7c38221206880efb46399708d695 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 27 Apr 2015 11:20:15 -0700 Subject: [PATCH] refactor(kernel): rename may_reduce_later to is_stuck, and make is_stuck more precise It now reflects the definition used in the elaboration paper. --- hott/algebra/precategory/functor.hlean | 4 ++-- hott/init/path.hlean | 2 +- src/kernel/converter.cpp | 2 +- src/kernel/converter.h | 2 +- src/kernel/default_converter.cpp | 12 ++++++------ src/kernel/default_converter.h | 4 ++-- src/kernel/extension_context.cpp | 3 +++ src/kernel/extension_context.h | 2 ++ src/kernel/hits/hits.cpp | 4 ++-- src/kernel/hits/hits.h | 2 +- src/kernel/inductive/inductive.cpp | 11 +++++++++-- src/kernel/inductive/inductive.h | 2 +- src/kernel/normalizer_extension.cpp | 8 ++++---- src/kernel/normalizer_extension.h | 2 +- src/kernel/quotient/quotient.cpp | 4 ++-- src/kernel/quotient/quotient.h | 2 +- src/kernel/type_checker.cpp | 2 +- src/kernel/type_checker.h | 3 ++- src/tests/kernel/environment.cpp | 2 +- 19 files changed, 43 insertions(+), 30 deletions(-) diff --git a/hott/algebra/precategory/functor.hlean b/hott/algebra/precategory/functor.hlean index 902210150..7413458bf 100644 --- a/hott/algebra/precategory/functor.hlean +++ b/hott/algebra/precategory/functor.hlean @@ -69,10 +69,10 @@ namespace functor apply concat, rotate_left 1, exact (pi_transport_constant (eq_of_homotopy pF) (H₁ c c') f), apply (apD10' f), - apply concat, rotate_left 1, + apply concat, rotate_left 1, esimp, exact (pi_transport_constant (eq_of_homotopy pF) (H₁ c) c'), apply (apD10' c'), - apply concat, rotate_left 1, + apply concat, rotate_left 1, esimp, exact (pi_transport_constant (eq_of_homotopy pF) H₁ c), apply idp end)))) diff --git a/hott/init/path.hlean b/hott/init/path.hlean index 5e4b18a2d..e3afe84a4 100644 --- a/hott/init/path.hlean +++ b/hott/init/path.hlean @@ -362,7 +362,7 @@ namespace eq definition con_con_ap_eq_con_con {g : A → A} (p : id ∼ g) {x y : A} (q : x = y) {w : A} (r : w = x) : (r ⬝ p x) ⬝ ap g q = (r ⬝ q) ⬝ p y := - eq.rec_on q idp + begin cases q, exact idp end definition con_ap_con_eq_con_con' {g : A → A} (p : id ∼ g) {x y : A} (q : x = y) {z : A} (s : g y = z) : diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp index 3dadbb207..d6b636763 100644 --- a/src/kernel/converter.cpp +++ b/src/kernel/converter.cpp @@ -38,7 +38,7 @@ struct dummy_converter : public converter { virtual optional get_module_idx() const { return optional(); } virtual bool is_opaque(declaration const &) const { return false; } virtual optional is_delta(expr const &) const { return optional(); } - virtual bool may_reduce_later(expr const &, type_checker &) { return false; } + virtual bool is_stuck(expr const &, type_checker &) { return false; } }; std::unique_ptr mk_dummy_converter() { diff --git a/src/kernel/converter.h b/src/kernel/converter.h index dad641948..e66a23f54 100644 --- a/src/kernel/converter.h +++ b/src/kernel/converter.h @@ -22,7 +22,7 @@ public: virtual bool is_opaque(declaration const & d) const = 0; virtual optional is_delta(expr const & e) const = 0; - virtual bool may_reduce_later(expr const & e, type_checker & c) = 0; + virtual bool is_stuck(expr const & e, type_checker & c) = 0; virtual pair whnf(expr const & e, type_checker & c) = 0; virtual pair is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & j) = 0; diff --git a/src/kernel/default_converter.cpp b/src/kernel/default_converter.cpp index 4a0bddbf2..e7ce26170 100644 --- a/src/kernel/default_converter.cpp +++ b/src/kernel/default_converter.cpp @@ -47,12 +47,12 @@ optional default_converter::d_norm_ext(expr const & e, constraint_seq & cs } /** \brief Return true if \c e may be reduced later after metavariables are instantiated. */ -bool default_converter::may_reduce_later(expr const & e) { - return static_cast(m_env.norm_ext().may_reduce_later(e, get_extension(*m_tc))); +bool default_converter::is_stuck(expr const & e) { + return static_cast(m_env.norm_ext().is_stuck(e, get_extension(*m_tc))); } -bool default_converter::may_reduce_later(expr const & e, type_checker & c) { - return static_cast(m_env.norm_ext().may_reduce_later(e, get_extension(c))); +bool default_converter::is_stuck(expr const & e, type_checker & c) { + return static_cast(m_env.norm_ext().is_stuck(e, get_extension(c))); } /** \brief Weak head normal form core procedure. It does not perform delta reduction nor normalization extensions. */ @@ -524,7 +524,7 @@ pair default_converter::is_def_eq_core(expr const & t, exp d_s = is_delta(s_n); if (d_t && d_s && is_eqp(*d_t, *d_s)) delay_check = true; - else if (may_reduce_later(t_n) && may_reduce_later(s_n)) + else if (is_stuck(t_n) && is_stuck(s_n)) delay_check = true; } @@ -539,7 +539,7 @@ pair default_converter::is_def_eq_core(expr const & t, exp if (is_def_eq_proof_irrel(t, s, pi_cs)) return to_bcs(true, pi_cs); - if (may_reduce_later(t_n) || may_reduce_later(s_n) || delay_check) { + if (is_stuck(t_n) || is_stuck(s_n) || delay_check) { cs += constraint_seq(mk_eq_cnstr(t_n, s_n, m_jst->get())); return to_bcs(true, cs); } diff --git a/src/kernel/default_converter.h b/src/kernel/default_converter.h index 4bbd2e7b6..8992d672c 100644 --- a/src/kernel/default_converter.h +++ b/src/kernel/default_converter.h @@ -28,7 +28,7 @@ protected: type_checker * m_tc; delayed_justification * m_jst; - virtual bool may_reduce_later(expr const & e); + virtual bool is_stuck(expr const & e); virtual optional> norm_ext(expr const & e); pair infer_type(expr const & e) { return converter::infer_type(*m_tc, e); } @@ -80,7 +80,7 @@ public: virtual bool is_opaque(declaration const & d) const; virtual optional get_module_idx() const { return m_module_idx; } - virtual bool may_reduce_later(expr const & e, type_checker & c); + virtual bool is_stuck(expr const & e, type_checker & c); virtual pair whnf(expr const & e_prime, type_checker & c); virtual pair is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & jst); }; diff --git a/src/kernel/extension_context.cpp b/src/kernel/extension_context.cpp index 8957ac74a..7510eefdc 100644 --- a/src/kernel/extension_context.cpp +++ b/src/kernel/extension_context.cpp @@ -11,6 +11,9 @@ namespace lean { expr extension_context::whnf(expr const & e, constraint_seq & cs) { auto p = whnf(e); cs += p.second; return p.first; } +pair extension_context::infer(expr const & e) { + return infer_type(e); +} expr extension_context::infer_type(expr const & e, constraint_seq & cs) { auto p = infer_type(e); cs += p.second; return p.first; } diff --git a/src/kernel/extension_context.h b/src/kernel/extension_context.h index 1f7d51aa0..0bb6f4d83 100644 --- a/src/kernel/extension_context.h +++ b/src/kernel/extension_context.h @@ -28,8 +28,10 @@ public: virtual pair whnf(expr const & e) = 0; virtual pair is_def_eq(expr const & e1, expr const & e2, delayed_justification & j) = 0; virtual pair infer_type(expr const & e) = 0; + virtual optional is_stuck(expr const & e) = 0; virtual name mk_fresh_name() = 0; expr whnf(expr const & e, constraint_seq & cs); + pair infer(expr const & e); expr infer_type(expr const & e, constraint_seq & cs); bool is_def_eq(expr const & e1, expr const & e2, delayed_justification & j, constraint_seq & cs); }; diff --git a/src/kernel/hits/hits.cpp b/src/kernel/hits/hits.cpp index 609dbd303..315e79c3f 100644 --- a/src/kernel/hits/hits.cpp +++ b/src/kernel/hits/hits.cpp @@ -115,10 +115,10 @@ optional is_hits_meta_app_core(Ctx & ctx, expr const & e) { return none_expr(); expr mk_app = ctx.whnf(args[mk_pos]).first; - return has_expr_metavar_strict(mk_app); + return ctx.is_stuck(mk_app); } -optional hits_normalizer_extension::may_reduce_later(expr const & e, extension_context & ctx) const { +optional hits_normalizer_extension::is_stuck(expr const & e, extension_context & ctx) const { return is_hits_meta_app_core(ctx, e); } diff --git a/src/kernel/hits/hits.h b/src/kernel/hits/hits.h index b11896bdc..38f23d61a 100644 --- a/src/kernel/hits/hits.h +++ b/src/kernel/hits/hits.h @@ -15,7 +15,7 @@ namespace lean { class hits_normalizer_extension : public normalizer_extension { public: virtual optional> operator()(expr const & e, extension_context & ctx) const; - virtual optional may_reduce_later(expr const & e, extension_context & ctx) const; + virtual optional is_stuck(expr const & e, extension_context & ctx) const; virtual bool supports(name const & feature) const; }; diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp index 51b8f3dec..1ec262258 100644 --- a/src/kernel/inductive/inductive.cpp +++ b/src/kernel/inductive/inductive.cpp @@ -965,7 +965,14 @@ optional is_elim_meta_app_core(Ctx & ctx, expr const & e) { if (elim_args.size() < major_idx + 1) return none_expr(); expr intro_app = ctx.whnf(elim_args[major_idx]).first; - return has_expr_metavar_strict(intro_app); + if (it1->m_K_target) { + // TODO(Leo): make it more precise. Remark: this piece of + // code does not affect the correctness of the kernel, but the + // effectiveness of the elaborator. + return has_expr_metavar_strict(intro_app); + } else { + return ctx.is_stuck(intro_app); + } } bool is_elim_meta_app(type_checker & tc, expr const & e) { @@ -973,7 +980,7 @@ bool is_elim_meta_app(type_checker & tc, expr const & e) { } // Return true if \c e is of the form (elim ... (?m ...)) -optional inductive_normalizer_extension::may_reduce_later(expr const & e, extension_context & ctx) const { +optional inductive_normalizer_extension::is_stuck(expr const & e, extension_context & ctx) const { return is_elim_meta_app_core(ctx, e); } diff --git a/src/kernel/inductive/inductive.h b/src/kernel/inductive/inductive.h index 08a49d9ca..cccc7f1e7 100644 --- a/src/kernel/inductive/inductive.h +++ b/src/kernel/inductive/inductive.h @@ -17,7 +17,7 @@ namespace inductive { class inductive_normalizer_extension : public normalizer_extension { public: virtual optional> operator()(expr const & e, extension_context & ctx) const; - virtual optional may_reduce_later(expr const & e, extension_context & ctx) const; + virtual optional is_stuck(expr const & e, extension_context & ctx) const; virtual bool supports(name const & feature) const; }; diff --git a/src/kernel/normalizer_extension.cpp b/src/kernel/normalizer_extension.cpp index a3babdc66..c79f9594d 100644 --- a/src/kernel/normalizer_extension.cpp +++ b/src/kernel/normalizer_extension.cpp @@ -12,7 +12,7 @@ public: virtual optional> operator()(expr const &, extension_context &) const { return optional>(); } - virtual optional may_reduce_later(expr const &, extension_context &) const { return none_expr(); } + virtual optional is_stuck(expr const &, extension_context &) const { return none_expr(); } virtual bool supports(name const &) const { return false; } }; @@ -34,11 +34,11 @@ public: return (*m_ext2)(e, ctx); } - virtual optional may_reduce_later(expr const & e, extension_context & ctx) const { - if (auto r = m_ext1->may_reduce_later(e, ctx)) + virtual optional is_stuck(expr const & e, extension_context & ctx) const { + if (auto r = m_ext1->is_stuck(e, ctx)) return r; else - return m_ext2->may_reduce_later(e, ctx); + return m_ext2->is_stuck(e, ctx); } virtual bool supports(name const & feature) const { diff --git a/src/kernel/normalizer_extension.h b/src/kernel/normalizer_extension.h index 4c3346972..6538258cf 100644 --- a/src/kernel/normalizer_extension.h +++ b/src/kernel/normalizer_extension.h @@ -21,7 +21,7 @@ public: /** \brief Return a non-none expression if the extension may reduce \c e after metavariables are instantiated. The expression returned is a meta-variable that if instantiated my allow the reduction to continue. */ - virtual optional may_reduce_later(expr const & e, extension_context & ctx) const = 0; + virtual optional is_stuck(expr const & e, extension_context & ctx) const = 0; /** \brief Return true iff the extension supports a feature with the given name, this method is only used for sanity checking. */ virtual bool supports(name const & feature) const = 0; diff --git a/src/kernel/quotient/quotient.cpp b/src/kernel/quotient/quotient.cpp index 5568a8e08..d6dbe7fc6 100644 --- a/src/kernel/quotient/quotient.cpp +++ b/src/kernel/quotient/quotient.cpp @@ -105,10 +105,10 @@ optional is_quot_meta_app_core(Ctx & ctx, expr const & e) { return none_expr(); expr mk_app = ctx.whnf(args[mk_pos]).first; - return has_expr_metavar_strict(mk_app); + return ctx.is_stuck(mk_app); } -optional quotient_normalizer_extension::may_reduce_later(expr const & e, extension_context & ctx) const { +optional quotient_normalizer_extension::is_stuck(expr const & e, extension_context & ctx) const { return is_quot_meta_app_core(ctx, e); } diff --git a/src/kernel/quotient/quotient.h b/src/kernel/quotient/quotient.h index 138d4d211..0d1dce473 100644 --- a/src/kernel/quotient/quotient.h +++ b/src/kernel/quotient/quotient.h @@ -13,7 +13,7 @@ namespace lean { class quotient_normalizer_extension : public normalizer_extension { public: virtual optional> operator()(expr const & e, extension_context & ctx) const; - virtual optional may_reduce_later(expr const & e, extension_context & ctx) const; + virtual optional is_stuck(expr const & e, extension_context & ctx) const; virtual bool supports(name const & feature) const; }; diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index d37e6d760..e816ab270 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -435,7 +435,7 @@ optional type_checker::is_stuck(expr const & e) { if (is_meta(e)) { return some_expr(e); } else { - return m_env.norm_ext().may_reduce_later(e, m_tc_ctx); + return m_env.norm_ext().is_stuck(e, m_tc_ctx); } } diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h index 917914964..0da64341d 100644 --- a/src/kernel/type_checker.h +++ b/src/kernel/type_checker.h @@ -81,6 +81,7 @@ class type_checker { } virtual pair infer_type(expr const & e) { return m_tc.infer_type(e); } virtual name mk_fresh_name() { return m_tc.m_gen.next(); } + virtual optional is_stuck(expr const & e) { return m_tc.is_stuck(e); } }; environment m_env; @@ -215,7 +216,7 @@ public: optional is_delta(expr const & e) const { return m_conv->is_delta(e); } - bool may_reduce_later(expr const & e) { return m_conv->may_reduce_later(e, *this); } + bool may_reduce_later(expr const & e) { return m_conv->is_stuck(e, *this); } template typename std::result_of::type with_params(level_param_names const & ps, F && f) { diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp index 127643777..ddaaf7717 100644 --- a/src/tests/kernel/environment.cpp +++ b/src/tests/kernel/environment.cpp @@ -134,7 +134,7 @@ public: // In a real implementation, we must check if proj1 and mk were defined in the environment. return optional>(app_arg(app_fn(a_n)), constraint_seq()); } - virtual optional may_reduce_later(expr const &, extension_context &) const { return none_expr(); } + virtual optional is_stuck(expr const &, extension_context &) const { return none_expr(); } virtual bool supports(name const &) const { return false; } };