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

@@ -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))))

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) :

src/kernel/converter.cpp

@@ -38,7 +38,7 @@ struct dummy_converter : public converter {
     virtual optional<module_idx> get_module_idx() const { return optional<module_idx>(); }
     virtual bool is_opaque(declaration const &) const { return false; }
     virtual optional<declaration> is_delta(expr const &) const { return optional<declaration>(); }
-    virtual bool may_reduce_later(expr const &, type_checker &) { return false; }
+    virtual bool is_stuck(expr const &, type_checker &) { return false; }
 };
 
 std::unique_ptr<converter> mk_dummy_converter() {

src/kernel/converter.h

@@ -22,7 +22,7 @@ public:
     virtual bool is_opaque(declaration const & d) const = 0;
     virtual optional<declaration> 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<expr, constraint_seq> whnf(expr const & e, type_checker & c) = 0;
     virtual pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & j) = 0;
 

src/kernel/default_converter.cpp

@@ -47,12 +47,12 @@ optional<expr> 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<bool>(m_env.norm_ext().may_reduce_later(e, get_extension(*m_tc)));
+bool default_converter::is_stuck(expr const & e) {
+    return static_cast<bool>(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<bool>(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<bool>(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<bool, constraint_seq> 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<bool, constraint_seq> 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);
     }

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<pair<expr, constraint_seq>> norm_ext(expr const & e);
 
     pair<expr, constraint_seq> 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<module_idx> 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<expr, constraint_seq> whnf(expr const & e_prime, type_checker & c);
     virtual pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s, type_checker & c, delayed_justification & jst);
 };

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<expr, constraint_seq> 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;
 }

src/kernel/extension_context.h

@@ -28,8 +28,10 @@ public:
     virtual pair<expr, constraint_seq> whnf(expr const & e) = 0;
     virtual pair<bool, constraint_seq> is_def_eq(expr const & e1, expr const & e2, delayed_justification & j) = 0;
     virtual pair<expr, constraint_seq> infer_type(expr const & e) = 0;
+    virtual optional<expr> is_stuck(expr const & e) = 0;
     virtual name mk_fresh_name() = 0;
     expr whnf(expr const & e, constraint_seq & cs);
+    pair<expr, constraint_seq> 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);
 };

src/kernel/hits/hits.cpp

@@ -115,10 +115,10 @@ optional<expr> 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<expr> hits_normalizer_extension::may_reduce_later(expr const & e, extension_context & ctx) const {
+optional<expr> hits_normalizer_extension::is_stuck(expr const & e, extension_context & ctx) const {
     return is_hits_meta_app_core(ctx, e);
 }
 

src/kernel/hits/hits.h

@@ -15,7 +15,7 @@ namespace lean {
 class hits_normalizer_extension : public normalizer_extension {
 public:
     virtual optional<pair<expr, constraint_seq>> operator()(expr const & e, extension_context & ctx) const;
-    virtual optional<expr> may_reduce_later(expr const & e, extension_context & ctx) const;
+    virtual optional<expr> is_stuck(expr const & e, extension_context & ctx) const;
     virtual bool supports(name const & feature) const;
 };
 

src/kernel/inductive/inductive.cpp

@@ -965,7 +965,14 @@ optional<expr> 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<expr> inductive_normalizer_extension::may_reduce_later(expr const & e, extension_context & ctx) const {
+optional<expr> inductive_normalizer_extension::is_stuck(expr const & e, extension_context & ctx) const {
     return is_elim_meta_app_core(ctx, e);
 }
 

src/kernel/inductive/inductive.h

@@ -17,7 +17,7 @@ namespace inductive {
 class inductive_normalizer_extension : public normalizer_extension {
 public:
     virtual optional<pair<expr, constraint_seq>> operator()(expr const & e, extension_context & ctx) const;
-    virtual optional<expr> may_reduce_later(expr const & e, extension_context & ctx) const;
+    virtual optional<expr> is_stuck(expr const & e, extension_context & ctx) const;
     virtual bool supports(name const & feature) const;
 };
 

src/kernel/normalizer_extension.cpp

@@ -12,7 +12,7 @@ public:
     virtual optional<pair<expr, constraint_seq>> operator()(expr const &, extension_context &) const {
         return optional<pair<expr, constraint_seq>>();
     }
-    virtual optional<expr> may_reduce_later(expr const &, extension_context &) const { return none_expr(); }
+    virtual optional<expr> 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<expr> may_reduce_later(expr const & e, extension_context & ctx) const {
-        if (auto r = m_ext1->may_reduce_later(e, ctx))
+    virtual optional<expr> 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 {

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<expr> may_reduce_later(expr const & e, extension_context & ctx) const = 0;
+    virtual optional<expr> 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;

src/kernel/quotient/quotient.cpp

@@ -105,10 +105,10 @@ optional<expr> 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<expr> quotient_normalizer_extension::may_reduce_later(expr const & e, extension_context & ctx) const {
+optional<expr> quotient_normalizer_extension::is_stuck(expr const & e, extension_context & ctx) const {
     return is_quot_meta_app_core(ctx, e);
 }
 

src/kernel/quotient/quotient.h

@@ -13,7 +13,7 @@ namespace lean {
 class quotient_normalizer_extension : public normalizer_extension {
 public:
     virtual optional<pair<expr, constraint_seq>> operator()(expr const & e, extension_context & ctx) const;
-    virtual optional<expr> may_reduce_later(expr const & e, extension_context & ctx) const;
+    virtual optional<expr> is_stuck(expr const & e, extension_context & ctx) const;
     virtual bool supports(name const & feature) const;
 };
 

src/kernel/type_checker.cpp

@@ -435,7 +435,7 @@ optional<expr> 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);
     }
 }
 

src/kernel/type_checker.h

@@ -81,6 +81,7 @@ class type_checker {
         }
         virtual pair<expr, constraint_seq> infer_type(expr const & e) { return m_tc.infer_type(e); }
         virtual name mk_fresh_name() { return m_tc.m_gen.next(); }
+        virtual optional<expr> is_stuck(expr const & e) { return m_tc.is_stuck(e); }
     };
 
     environment                m_env;
@@ -215,7 +216,7 @@ public:
 
     optional<declaration> 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 F>
     typename std::result_of<F()>::type with_params(level_param_names const & ps, F && f) {

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<pair<expr, constraint_seq>>(app_arg(app_fn(a_n)), constraint_seq());
     }
-    virtual optional<expr> may_reduce_later(expr const &, extension_context &) const { return none_expr(); }
+    virtual optional<expr> is_stuck(expr const &, extension_context &) const { return none_expr(); }
     virtual bool supports(name const &) const { return false; }
 };