fix(kernel/expr): remove 'cast_binder_info'

We should put it back when we decide to implement it.
We also fix the bogus comment at src/frontends/lean/parser.cpp.

see issue #667

src/frontends/lean/parser.cpp

@@ -797,10 +797,11 @@ auto parser::elaborate_definition_at(environment const & env, local_level_decls
 
 /**
    \brief Return an optional binder_info object based on the current token
-      - '('           : default
+      - '('          : default
       - '{'          : implicit
       - '{{' or '⦃'  : strict implicit
-      - '['          : cast
+      - '['          : inst_implicit (i.e., implicit argument that should be
+                       synthesized using type class resolution)
 
    If simple_only, then only `(` is considered
 */

src/kernel/expr.cpp

@@ -136,7 +136,7 @@ void expr_const::dealloc() {
 }
 
 unsigned binder_info::hash() const {
-    return (m_implicit << 4) | (m_cast << 3) | (m_contextual << 2) | (m_strict_implicit << 1) | m_inst_implicit;
+    return (m_implicit << 3) | (m_contextual << 2) | (m_strict_implicit << 1) | m_inst_implicit;
 }
 
 // Expr metavariables and local variables
@@ -197,7 +197,6 @@ static unsigned dec(unsigned k) { return k == 0 ? 0 : k - 1; }
 bool operator==(binder_info const & i1, binder_info const & i2) {
     return
         i1.is_implicit() == i2.is_implicit() &&
-        i1.is_cast() == i2.is_cast() &&
         i1.is_contextual() == i2.is_contextual() &&
         i1.is_strict_implicit() == i2.is_strict_implicit() &&
         i1.is_inst_implicit() == i2.is_inst_implicit();

src/kernel/expr.h

@@ -212,7 +212,6 @@ public:
 */
 class binder_info {
     unsigned m_implicit:1;        //! if true, binder argument is an implicit argument
-    unsigned m_cast:1;            //! if true, binder argument is a target for using cast
     /** if m_contextual is true, binder argument is assumed to be part of the context,
         and may be argument for metavariables. */
     unsigned m_contextual:1;
@@ -221,24 +220,21 @@ class binder_info {
         inferred by class-instance resolution. */
     unsigned m_inst_implicit:1;
 public:
-    binder_info(bool implicit = false, bool cast = false, bool contextual = true, bool strict_implicit = false,
-                bool inst_implicit = false):
-        m_implicit(implicit), m_cast(cast), m_contextual(contextual), m_strict_implicit(strict_implicit),
+    binder_info(bool implicit = false, bool contextual = true, bool strict_implicit = false, bool inst_implicit = false):
+        m_implicit(implicit), m_contextual(contextual), m_strict_implicit(strict_implicit),
         m_inst_implicit(inst_implicit) {}
     bool is_implicit() const { return m_implicit; }
-    bool is_cast() const { return m_cast; }
     bool is_contextual() const { return m_contextual; }
     bool is_strict_implicit() const { return m_strict_implicit; }
     bool is_inst_implicit() const { return m_inst_implicit; }
     unsigned hash() const;
-    binder_info update_contextual(bool f) const { return binder_info(m_implicit, m_cast, f, m_strict_implicit, m_inst_implicit); }
+    binder_info update_contextual(bool f) const { return binder_info(m_implicit, f, m_strict_implicit, m_inst_implicit); }
 };
 
-inline binder_info mk_implicit_binder_info() { return binder_info(true); }
-inline binder_info mk_strict_implicit_binder_info() { return binder_info(false, false, true, true); }
-inline binder_info mk_inst_implicit_binder_info() { return binder_info(false, false, true, false, true); }
-inline binder_info mk_cast_binder_info() { return binder_info(false, true); }
-inline binder_info mk_contextual_info(bool f) { return binder_info(false, false, f); }
+inline binder_info mk_implicit_binder_info()        { return binder_info(true); }
+inline binder_info mk_strict_implicit_binder_info() { return binder_info(false, true, true); }
+inline binder_info mk_inst_implicit_binder_info()   { return binder_info(false, true, false, true); }
+inline binder_info mk_contextual_info(bool f)       { return binder_info(false, f); }
 
 inline bool is_explicit(binder_info const & bi) {
     return !bi.is_implicit() && !bi.is_strict_implicit() && !bi.is_inst_implicit();

src/library/kernel_bindings.cpp

@@ -283,14 +283,12 @@ static int mk_binder_info(lua_State * L) {
         return push_binder_info(L, binder_info(lua_toboolean(L, 1), lua_toboolean(L, 2), lua_toboolean(L, 3), lua_toboolean(L, 4)));
 }
 static int binder_info_is_implicit(lua_State * L) { return push_boolean(L, to_binder_info(L, 1).is_implicit()); }
-static int binder_info_is_cast(lua_State * L) { return push_boolean(L, to_binder_info(L, 1).is_cast()); }
 static int binder_info_is_contextual(lua_State * L) { return push_boolean(L, to_binder_info(L, 1).is_contextual()); }
 static int binder_info_is_strict_implicit(lua_State * L) { return push_boolean(L, to_binder_info(L, 1).is_strict_implicit()); }
 static int binder_info_is_inst_implicit(lua_State * L) { return push_boolean(L, to_binder_info(L, 1).is_inst_implicit()); }
 static const struct luaL_Reg binder_info_m[] = {
     {"__gc",               binder_info_gc},
     {"is_implicit",        safe_function<binder_info_is_implicit>},
-    {"is_cast",            safe_function<binder_info_is_cast>},
     {"is_contextual",      safe_function<binder_info_is_contextual>},
     {"is_strict_implicit", safe_function<binder_info_is_strict_implicit>},
     {"is_inst_implicit",   safe_function<binder_info_is_inst_implicit>},

src/library/kernel_serializer.cpp

@@ -118,8 +118,7 @@ static expr read_macro_definition(deserializer & d, unsigned num, expr const * a
 
 serializer & operator<<(serializer & s, binder_info const & i) {
     unsigned w =
-        (i.is_implicit() ?       16 : 0) +
-        (i.is_cast() ?            8 : 0) +
+        (i.is_implicit() ?        8 : 0) +
         (i.is_contextual() ?      4 : 0) +
         (i.is_strict_implicit() ? 2 : 0) +
         (i.is_inst_implicit() ?   1 : 0);
@@ -129,12 +128,11 @@ serializer & operator<<(serializer & s, binder_info const & i) {
 
 static binder_info read_binder_info(deserializer & d) {
     unsigned w = d.read_char();
-    bool imp   = (w & 16) != 0;
-    bool cast  = (w & 8)  != 0;
-    bool ctx   = (w & 4)  != 0;
-    bool s_imp = (w & 2)  != 0;
-    bool i_imp = (w & 1)  != 0;
-    return binder_info(imp, cast, ctx, s_imp, i_imp);
+    bool imp   = (w & 8) != 0;
+    bool ctx   = (w & 4) != 0;
+    bool s_imp = (w & 2) != 0;
+    bool i_imp = (w & 1) != 0;
+    return binder_info(imp, ctx, s_imp, i_imp);
 }
 
 static name * g_binder_name = nullptr;

tests/lua/expr1.lua

@@ -1,12 +1,7 @@
 assert(not binder_info():is_implicit())
-assert(not binder_info():is_cast())
 assert(not binder_info(false, false):is_implicit())
-assert(not binder_info(false, false):is_cast())
 assert(binder_info(true):is_implicit())
-assert(not binder_info(true):is_cast())
 assert(binder_info(true, true):is_implicit())
-assert(binder_info(true, true):is_cast())
 assert(binder_info():is_contextual())
-assert(not binder_info(true, true, false):is_contextual())
-assert(binder_info(false, false, true):is_contextual())
-
+assert(not binder_info(true, false):is_contextual())
+assert(binder_info(false, true):is_contextual())

tests/lua/expr3.lua

@@ -1,6 +1,5 @@
 local b1 = binder_info()
 assert(not b1:is_implicit())
-assert(not b1:is_cast())
 
 local f = Const("f")
 local a = Const("a")
@@ -78,7 +77,6 @@ assert(a1 == name("a"))
 assert(t == Prop)
 assert(b1 == Var(0))
 assert(bi:is_implicit())
-assert(not bi:is_cast())
 assert(f:is_constant())
 f(f(a)):for_each(function (e, o) print(tostring(e)); return true; end)
 assert(f(Var(0)):lift_free_vars(1) == f(Var(1)))