feat(library): add typed_expr macro

We use it to enforce that a let-variable has the expected type

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

src/frontends/lean/builtin_exprs.cpp

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "library/explicit.h"
 #include "library/tactic/tactic.h"
 #include "library/tactic/expr_to_tactic.h"
+#include "library/typed_expr.h"
 #include "frontends/lean/builtin_exprs.h"
 #include "frontends/lean/token_table.h"
 #include "frontends/lean/calc.h"
@@ -108,7 +109,7 @@ static expr parse_let(parser & p, pos_info const & pos) {
         // expr body = abstract(parse_let_body(p, pos), l);
         //     return mk_let(p, id, type, value, body, pos, mk_contextual_info(is_fact));
         // } else  {
-        p.add_local_expr(id, value);
+        p.add_local_expr(id, p.save_pos(mk_typed_expr(type, value), p.pos_of(value)));
         return parse_let_body(p, pos);
         // }
     }

src/frontends/lean/elaborator.cpp

@@ -27,6 +27,7 @@ Author: Leonardo de Moura
 #include "library/opaque_hints.h"
 #include "library/locals.h"
 #include "library/deep_copy.h"
+#include "library/typed_expr.h"
 #include "library/tactic/tactic.h"
 #include "library/tactic/expr_to_tactic.h"
 #include "library/error_handling/error_handling.h"
@@ -1045,6 +1046,30 @@ public:
     expr visit_pi(expr const & e, constraint_seq & cs) { return visit_binding(e, expr_kind::Pi, cs); }
     expr visit_lambda(expr const & e, constraint_seq & cs) { return visit_binding(e, expr_kind::Lambda, cs); }
 
+    expr visit_typed_expr(expr const & e, constraint_seq & cs) {
+        constraint_seq t_cs;
+        expr t      = visit(get_typed_expr_type(e), t_cs);
+        constraint_seq v_cs;
+        expr v      = visit(get_typed_expr_expr(e), v_cs);
+        expr v_type = infer_type(v, v_cs);
+        justification j = mk_justification(e, [=](formatter const & fmt, substitution const & subst) {
+                substitution s(subst);
+                format expected_fmt, given_fmt;
+                std::tie(expected_fmt, given_fmt) = pp_until_different(fmt, s.instantiate(t), s.instantiate(v_type));
+                format r("type mismatch at term");
+                r += pp_indent_expr(fmt, s.instantiate(v));
+                r += format("has type");
+                r += given_fmt;
+                r += compose(line(), format("but is expected to have type"));
+                r += expected_fmt;
+                return r;
+            });
+        auto new_vcs    = ensure_has_type(v, v_type, t, j, m_relax_main_opaque);
+        v = new_vcs.first;
+        cs += t_cs + new_vcs.second + v_cs;
+        return v;
+    }
+
     expr visit_core(expr const & e, constraint_seq & cs) {
         if (is_placeholder(e)) {
             return visit_placeholder(e, cs);
@@ -1055,6 +1080,8 @@ public:
         } else if (is_noinfo(e)) {
             flet<bool> let(m_noinfo, true);
             return visit(get_annotation_arg(e), cs);
+        } else if (is_typed_expr(e)) {
+            return visit_typed_expr(e, cs);
         } else {
             switch (e.kind()) {
             case expr_kind::Local:      return e;

src/frontends/lean/pp.cpp

@@ -15,6 +15,7 @@ Author: Leonardo de Moura
 #include "library/placeholder.h"
 #include "library/private.h"
 #include "library/explicit.h"
+#include "library/typed_expr.h"
 #include "library/num.h"
 #include "library/print.h"
 #include "frontends/lean/pp.h"
@@ -419,8 +420,10 @@ auto pretty_fn::pp(expr const & e) -> result {
     if (is_show(e))         return pp_show(e);
     if (is_let(e))          return pp_let(e);
     if (is_have(e))         return pp_have(e);
+    if (is_typed_expr(e))   return pp(get_typed_expr_expr(e));
     if (auto n = to_num(e)) return pp_num(*n);
-    if (!m_metavar_args && is_meta(e)) return pp_meta(get_app_fn(e));
+    if (!m_metavar_args && is_meta(e))
+        return pp_meta(get_app_fn(e));
 
     switch (e.kind()) {
     case expr_kind::Var:       return pp_var(e);

src/library/CMakeLists.txt

@@ -8,6 +8,6 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   unifier.cpp unifier_plugin.cpp inductive_unifier_plugin.cpp
   explicit.cpp num.cpp string.cpp opaque_hints.cpp head_map.cpp
   match.cpp definition_cache.cpp declaration_index.cpp
-  print.cpp annotation.cpp)
+  print.cpp annotation.cpp typed_expr.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})

src/library/typed_expr.cpp

@@ -0,0 +1,74 @@
+/*
+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 <string>
+#include "library/kernel_serializer.h"
+
+namespace lean {
+name const & get_typed_expr_name() {
+    static name g_typed_expr("typed_expr");
+    return g_typed_expr;
+}
+
+std::string const & get_typed_expr_opcode() {
+    static std::string g_typed_expr_opcode("TyE");
+    return g_typed_expr_opcode;
+}
+
+
+/** \brief This macro is used to "enforce" a given type to an expression.
+    It is equivalent to the abbreviation
+
+        abbreviation typed_expr (A : Type) (a : A) := a
+
+    We use a macro instead of an abbreviation because we want to be able
+    to use in any environment, even one that does not contain the
+    abbreviation such as typed_expr.
+
+    The macro is also slightly for efficient because we don't need a
+    universe parameter.
+*/
+class typed_expr_macro_definition_cell : public macro_definition_cell {
+    void check_macro(expr const & m) const {
+        if (!is_macro(m) || macro_num_args(m) != 2)
+            throw exception("invalid typed-expr, incorrect number of arguments");
+    }
+public:
+    virtual name get_name() const { return get_typed_expr_name(); }
+    virtual expr get_type(expr const & m, expr const * arg_types, extension_context &) const {
+        check_macro(m);
+        return arg_types[0];
+    }
+    virtual optional<expr> expand(expr const & m, extension_context &) const {
+        check_macro(m);
+        return some_expr(macro_arg(m, 1));
+    }
+    virtual void write(serializer & s) const {
+        s.write_string(get_typed_expr_opcode());
+    }
+};
+
+static macro_definition g_typed_expr(new typed_expr_macro_definition_cell());
+
+bool is_typed_expr(expr const & e) {
+    return is_macro(e) && macro_def(e) == g_typed_expr;
+}
+
+expr mk_typed_expr(expr const & t, expr const & v) {
+    expr args[2] = {t, v};
+    return mk_macro(g_typed_expr, 2, args);
+}
+
+expr get_typed_expr_type(expr const & e) { lean_assert(is_typed_expr(e)); return macro_arg(e, 0); }
+expr get_typed_expr_expr(expr const & e) { lean_assert(is_typed_expr(e)); return macro_arg(e, 1); }
+
+static register_macro_deserializer_fn
+typed_expr_macro_des_fn(get_typed_expr_opcode(), [](deserializer &, unsigned num, expr const * args) {
+        if (num != 2)
+            throw corrupted_stream_exception();
+        return mk_typed_expr(args[0], args[1]);
+    });
+}

src/library/typed_expr.h

@@ -0,0 +1,25 @@
+/*
+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
+
+namespace lean {
+class expr;
+/** \brief Create an expression definitionally equal to \c e, but it must have type \c t. */
+expr mk_typed_expr(expr const & t, expr const & e);
+/** \brief Return true iff \c e was created using #mk_typed_expr */
+bool is_typed_expr(expr const & e);
+/** \brief Return the type of a typed expression
+
+    \remark get_typed_expr_type(mk_typed_expr(t, e)) == t
+*/
+expr get_typed_expr_type(expr const & e);
+/** \brief Return the expression/denotation of a typed expression
+
+    \remark get_typed_expr_type(mk_typed_expr(t, e)) == e
+*/
+expr get_typed_expr_expr(expr const & e);
+}

tests/lean/let1.lean.expected.out

@@ -2,7 +2,11 @@
   H H1 H2 :
   ∀ (p q : Prop),
     p → q → (∀ (c : Prop), (p → q → c) → c)
-λ (p q : Prop) (H1 : p) (H2 : q) (c : Prop) (H : p → q → c),
+let1.lean:19:19: error: type mismatch at term
-  H H1 H2 :
+  λ (p q : Prop) (H1 : p) (H2 : q) (c : Prop) (H : p → q → c),
+    H H1 H2has type
   ∀ (p q : Prop),
     p → q → (∀ (c : Prop), (p → q → c) → c)
+but is expected to have type
+  ∀ (p q : Prop),
+    p → q → (λ (p q : Prop), ∀ (c : Prop), (p → q → c) → c) q p