refactor(kernel/type_checker): use read-only metavariable environment in methods that do not require write access to the metavariable environment

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/kernel/metavar.cpp

@@ -424,10 +424,6 @@ context metavar_env_cell::instantiate_metavars(context const & ctx) const {
     return context(new_entries.size(), new_entries.data());
 }
 
-metavar_env::metavar_env(ro_metavar_env const & s):m_ptr(s.m_ptr) {
-    if (m_ptr) m_ptr->inc_ref();
-}
-
 template<typename MEnv>
 bool cached_metavar_env_tpl<MEnv>::update(optional<MEnv> const & menv) {
     if (!menv) {

src/kernel/metavar.h

@@ -206,8 +206,6 @@ class metavar_env {
     friend class metavar_env_cell;
     metavar_env_cell * m_ptr;
     explicit metavar_env(metavar_env_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); }
-    friend class type_checker;
-    explicit metavar_env(ro_metavar_env const & s);
 public:
     metavar_env():m_ptr(new metavar_env_cell()) { m_ptr->inc_ref(); }
     metavar_env(name const & prefix):m_ptr(new metavar_env_cell(prefix)) { m_ptr->inc_ref(); }
@@ -251,6 +249,16 @@ class ro_metavar_env {
     friend class metavar_env;
     metavar_env_cell * m_ptr;
     explicit ro_metavar_env(metavar_env_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); }
+    friend class type_checker;
+    /*
+      \brief (Hack) The following two methods are used by the type_checker. Some methods
+      in the type checker only need read-only access when unification constraints are not
+      used. For these methods, we can relax the interface and accept a read-only metavariable
+      environment. However, the type checker internally uses the read-write version. So,
+      this constructor is a hack to workaround that.
+    */
+    static optional<metavar_env> const & to_rw(optional<ro_metavar_env> const & menv) { return reinterpret_cast<optional<metavar_env> const &>(menv); }
+    metavar_env const & to_rw() const { return reinterpret_cast<metavar_env const&>(*this); }
 public:
     ro_metavar_env():m_ptr(new metavar_env_cell()) { m_ptr->inc_ref(); }
     ro_metavar_env(metavar_env const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }

src/kernel/type_checker.cpp

@@ -479,12 +479,12 @@ expr type_checker::infer_type(expr const & e, context const & ctx, optional<meta
 expr type_checker::infer_type(expr const & e, context const & ctx, metavar_env const & menv, buffer<unification_constraint> & uc) {
     return m_ptr->infer_type(e, ctx, some_menv(menv), &uc);
 }
-expr type_checker::infer_type(expr const & e, context const & ctx, metavar_env const & menv) {
-    return m_ptr->infer_type(e, ctx, some_menv(menv), nullptr);
-}
 expr type_checker::infer_type(expr const & e, context const & ctx, ro_metavar_env const & menv) {
     // metavariable environment is not updated when unification constraints are not provided
-    return infer_type(e, ctx, metavar_env(menv));
+    return infer_type(e, ctx, some_menv(menv.to_rw()), nullptr);
+}
+expr type_checker::infer_type(expr const & e, context const & ctx, optional<ro_metavar_env> const & menv) {
+    return infer_type(e, ctx, ro_metavar_env::to_rw(menv), nullptr);
 }
 expr type_checker::infer_type(expr const & e, context const & ctx) {
     return infer_type(e, ctx, none_menv(), nullptr);
@@ -495,8 +495,9 @@ expr type_checker::check(expr const & e, context const & ctx, optional<metavar_e
 expr type_checker::check(expr const & e, context const & ctx, metavar_env const & menv, buffer<unification_constraint> & uc) {
     return m_ptr->check(e, ctx, some_menv(menv), &uc);
 }
-expr type_checker::check(expr const & e, context const & ctx, metavar_env const & menv) {
+expr type_checker::check(expr const & e, context const & ctx, ro_metavar_env const & menv) {
-    return m_ptr->check(e, ctx, some_menv(menv), nullptr);
+    // metavariable environment is not updated when unification constraints are not provided
+    return check(e, ctx, some_menv(menv.to_rw()), nullptr);
 }
 expr type_checker::check(expr const & e, context const & ctx) {
     return check(e, ctx, none_menv(), nullptr);
@@ -513,31 +514,27 @@ void type_checker::check_type(expr const & e, context const & ctx) {
 expr type_checker::ensure_pi(expr const & e, context const & ctx) {
     return m_ptr->ensure_pi(e, ctx);
 }
-bool type_checker::is_proposition(expr const & e, context const & ctx, optional<metavar_env> const & menv) {
+bool type_checker::is_proposition(expr const & e, context const & ctx, optional<ro_metavar_env> const & menv) {
-    return m_ptr->is_proposition(e, ctx, menv);
+    return m_ptr->is_proposition(e, ctx, ro_metavar_env::to_rw(menv));
 }
 bool type_checker::is_proposition(expr const & e, context const & ctx) {
-    return is_proposition(e, ctx, none_menv());
+    return is_proposition(e, ctx, none_ro_menv());
-}
-bool type_checker::is_proposition(expr const & e, context const & ctx, metavar_env const & menv) {
-    return is_proposition(e, ctx, some_menv(menv));
 }
 bool type_checker::is_proposition(expr const & e, context const & ctx, ro_metavar_env const & menv) {
-    // metavariable environment is not updated when unification constraints are not provided
+    return is_proposition(e, ctx, some_ro_menv(menv));
-    return is_proposition(e, ctx, metavar_env(menv));
 }
-bool type_checker::is_flex_proposition(expr e, context ctx, optional<metavar_env> const & menv) {
+bool type_checker::is_flex_proposition(expr e, context ctx, optional<ro_metavar_env> const & menv) {
     while (is_pi(e)) {
         ctx = extend(ctx, abst_name(e), abst_domain(e));
         e   = abst_body(e);
     }
     return is_proposition(e, ctx, menv);
 }
-bool type_checker::is_flex_proposition(expr const & e, context const & ctx, metavar_env const & menv) {
+bool type_checker::is_flex_proposition(expr const & e, context const & ctx, ro_metavar_env const & menv) {
-    return is_flex_proposition(e, ctx, some_menv(menv));
+    return is_flex_proposition(e, ctx, some_ro_menv(menv));
 }
 bool type_checker::is_flex_proposition(expr const & e, context const & ctx) {
-    return is_flex_proposition(e, ctx, none_menv());
+    return is_flex_proposition(e, ctx, none_ro_menv());
 }
 void type_checker::clear() { m_ptr->clear(); }
 normalizer & type_checker::get_normalizer() { return m_ptr->get_normalizer(); }
@@ -547,13 +544,13 @@ expr  type_check(expr const & e, ro_environment const & env, context const & ctx
 bool is_convertible(expr const & given, expr const & expected, ro_environment const & env, context const & ctx) {
     return type_checker(env).is_convertible(given, expected, ctx);
 }
-bool is_proposition(expr const & e, ro_environment const & env, context const & ctx, optional<metavar_env> const & menv) {
+bool is_proposition(expr const & e, ro_environment const & env, context const & ctx, optional<ro_metavar_env> const & menv) {
     return type_checker(env).is_proposition(e, ctx, menv);
 }
-bool is_proposition(expr const & e, ro_environment const & env, context const & ctx, metavar_env const & menv) {
+bool is_proposition(expr const & e, ro_environment const & env, context const & ctx, ro_metavar_env const & menv) {
-    return is_proposition(e, env, ctx, some_menv(menv));
+    return is_proposition(e, env, ctx, some_ro_menv(menv));
 }
 bool is_proposition(expr const & e, ro_environment const & env, context const & ctx) {
-    return is_proposition(e, env, ctx, none_menv());
+    return is_proposition(e, env, ctx, none_ro_menv());
 }
 }

src/kernel/type_checker.h

@@ -49,8 +49,8 @@ public:
     */
     expr infer_type(expr const & e, context const & ctx, optional<metavar_env> const & menv, buffer<unification_constraint> * new_constraints);
     expr infer_type(expr const & e, context const & ctx, metavar_env const & menv, buffer<unification_constraint> & new_constraints);
-    expr infer_type(expr const & e, context const & ctx, metavar_env const & menv);
     expr infer_type(expr const & e, context const & ctx, ro_metavar_env const & menv);
+    expr infer_type(expr const & e, context const & ctx, optional<ro_metavar_env> const & menv);
 
     /**
         \brief Return the type of \c e in the context \c ctx.
@@ -71,7 +71,7 @@ public:
     */
     expr check(expr const & e, context const & ctx, optional<metavar_env> const & menv, buffer<unification_constraint> * new_constraints);
     expr check(expr const & e, context const & ctx, metavar_env const & menv, buffer<unification_constraint> & new_constraints);
-    expr check(expr const & e, context const & ctx, metavar_env const & menv);
+    expr check(expr const & e, context const & ctx, ro_metavar_env const & menv);
 
     /**
         \brief Type check the given expression, and return the type of \c e in the context \c ctx.
@@ -94,14 +94,13 @@ public:
     bool is_definitionally_equal(expr const & t1, expr const & t2, context const & ctx = context());
 
     /** \brief Return true iff \c e is a proposition (i.e., it has type Bool) */
-    bool is_proposition(expr const & e, context const & ctx, optional<metavar_env> const & menv);
+    bool is_proposition(expr const & e, context const & ctx, optional<ro_metavar_env> const & menv);
-    bool is_proposition(expr const & e, context const & ctx, metavar_env const & menv);
     bool is_proposition(expr const & e, context const & ctx, ro_metavar_env const & menv);
     bool is_proposition(expr const & e, context const & ctx = context());
 
     /** \brief Return true iff \c e is a proposition or is a Pi s.t. the range is a flex_proposition */
-    bool is_flex_proposition(expr e, context ctx, optional<metavar_env> const & menv);
+    bool is_flex_proposition(expr e, context ctx, optional<ro_metavar_env> const & menv);
-    bool is_flex_proposition(expr const & e, context const & ctx, metavar_env const & menv);
+    bool is_flex_proposition(expr const & e, context const & ctx, ro_metavar_env const & menv);
     bool is_flex_proposition(expr const & e, context const & ctx = context());
 
     /** \brief Return a Pi if \c e is convertible to Pi. Throw an exception otherwise. */
@@ -122,7 +121,7 @@ public:
     expr operator()(expr const & e, context const & ctx, metavar_env const & menv, buffer<unification_constraint> & new_constraints) {
         return infer_type(e, ctx, menv, new_constraints);
     }
-    expr operator()(expr const & e, context const & ctx, metavar_env const & menv) {
+    expr operator()(expr const & e, context const & ctx, ro_metavar_env const & menv) {
         return infer_type(e, ctx, menv);
     }
     expr operator()(expr const & e, context const & ctx = context()) {
@@ -131,7 +130,7 @@ public:
 };
 expr type_check(expr const & e, ro_environment const & env, context const & ctx = context());
 bool is_convertible(expr const & t1, expr const & t2, ro_environment const & env, context const & ctx = context());
-bool is_proposition(expr const & e, ro_environment const & env, context const & ctx, optional<metavar_env> const & menv);
+bool is_proposition(expr const & e, ro_environment const & env, context const & ctx, optional<ro_metavar_env> const & menv);
-bool is_proposition(expr const & e, ro_environment const & env, context const & ctx, metavar_env const & menv);
+bool is_proposition(expr const & e, ro_environment const & env, context const & ctx, ro_metavar_env const & menv);
 bool is_proposition(expr const & e, ro_environment const & env, context const & ctx = context());
 }

src/library/tactic/proof_state.cpp

@@ -90,7 +90,7 @@ void proof_state::get_goal_names(name_set & r) const {
 }
 
 name arg_to_hypothesis_name(name const & n, expr const & d, ro_environment const & env, context const & ctx, optional<metavar_env> const & menv) {
-    if (is_default_arrow_var_name(n) && is_proposition(d, env, ctx, menv))
+    if (is_default_arrow_var_name(n) && is_proposition(d, env, ctx, to_ro_menv(menv)))
         return name("H");
     else
         return n;