refactor(library/typed_expr): do not use macros for implementing type…

…d_expr

Remark: in Lean4, we will not have macro_defs.

library/init/core.lean

@@ -104,6 +104,9 @@ a
 /-- Gadget for marking output parameters in type classes. -/
 @[reducible] def out_param (α : Sort u) : Sort u := α
 
+/-- Auxiliary declaration used to implement the notation (a : α) -/
+@[reducible] def typed_expr (α : Type u) (a : α) : α := a
+
 /-
   id_rhs is an auxiliary declaration used in the equation compiler to address performance
   issues when proving equational lemmas. The equation compiler uses it as a marker.

src/frontends/lean/elaborator.cpp

@@ -3306,8 +3306,6 @@ expr elaborator::visit_macro(expr const & e, optional<expr> const & expected_typ
         return visit_anonymous_constructor(e, expected_type);
     } else if (is_prenum(e)) {
         return visit_prenum(e, expected_type);
-    } else if (is_typed_expr(e)) {
-        return visit_typed_expr(e);
     } else if (is_choice(e) || is_explicit(e) || is_partial_explicit(e)) {
         return visit_app_core(e, buffer<expr>(), expected_type, e);
     } else if (is_by(e)) {
@@ -3567,6 +3565,8 @@ expr elaborator::visit(expr const & e, optional<expr> const & expected_type) {
     return recover_expr_from_exception(expected_type, e, [&] () -> expr {
         if (is_placeholder(e)) {
             return visit_placeholder(e, expected_type);
+        } else if (is_typed_expr(e)) {
+            return visit_typed_expr(e);
         } else if (is_have_expr(e)) {
             return copy_tag(e, visit_have_expr(e, expected_type));
         } else if (is_suffices_annotation(e)) {

src/library/constants.cpp

@@ -341,6 +341,7 @@ name const * g_trans_rel_left = nullptr;
 name const * g_trans_rel_right = nullptr;
 name const * g_true = nullptr;
 name const * g_true_intro = nullptr;
+name const * g_typed_expr = nullptr;
 name const * g_unification_hint = nullptr;
 name const * g_unification_hint_mk = nullptr;
 name const * g_unit = nullptr;
@@ -698,6 +699,7 @@ void initialize_constants() {
     g_trans_rel_right = new name{"trans_rel_right"};
     g_true = new name{"true"};
     g_true_intro = new name{"true", "intro"};
+    g_typed_expr = new name{"typed_expr"};
     g_unification_hint = new name{"unification_hint"};
     g_unification_hint_mk = new name{"unification_hint", "mk"};
     g_unit = new name{"unit"};
@@ -1056,6 +1058,7 @@ void finalize_constants() {
     delete g_trans_rel_right;
     delete g_true;
     delete g_true_intro;
+    delete g_typed_expr;
     delete g_unification_hint;
     delete g_unification_hint_mk;
     delete g_unit;
@@ -1413,6 +1416,7 @@ name const & get_trans_rel_left_name() { return *g_trans_rel_left; }
 name const & get_trans_rel_right_name() { return *g_trans_rel_right; }
 name const & get_true_name() { return *g_true; }
 name const & get_true_intro_name() { return *g_true_intro; }
+name const & get_typed_expr_name() { return *g_typed_expr; }
 name const & get_unification_hint_name() { return *g_unification_hint; }
 name const & get_unification_hint_mk_name() { return *g_unification_hint_mk; }
 name const & get_unit_name() { return *g_unit; }

src/library/constants.h

@@ -343,6 +343,7 @@ name const & get_trans_rel_left_name();
 name const & get_trans_rel_right_name();
 name const & get_true_name();
 name const & get_true_intro_name();
+name const & get_typed_expr_name();
 name const & get_unification_hint_name();
 name const & get_unification_hint_mk_name();
 name const & get_unit_name();

src/library/constants.txt

@@ -336,6 +336,7 @@ trans_rel_left
 trans_rel_right
 true
 true.intro
+typed_expr
 unification_hint
 unification_hint.mk
 unit

src/library/init_module.cpp

@@ -7,7 +7,6 @@ Author: Leonardo de Moura
 #include "library/trace.h"
 #include "library/constants.h"
 #include "library/kernel_serializer.h"
-#include "library/typed_expr.h"
 #include "library/choice.h"
 #include "library/class.h"
 #include "library/num.h"
@@ -85,7 +84,6 @@ void initialize_library_module() {
     initialize_idx_metavar();
     initialize_io_state();
     initialize_kernel_serializer();
-    initialize_typed_expr();
     initialize_choice();
     initialize_string();
     initialize_num();
@@ -159,7 +157,6 @@ void finalize_library_module() {
     finalize_num();
     finalize_string();
     finalize_choice();
-    finalize_typed_expr();
     finalize_kernel_serializer();
     finalize_io_state();
     finalize_idx_metavar();

src/library/typed_expr.cpp

@@ -5,89 +5,18 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <string>
-#include "kernel/error_msgs.h"
-#include "kernel/kernel_exception.h"
-#include "kernel/abstract_type_context.h"
 #include "library/util.h"
-#include "library/kernel_serializer.h"
+#include "library/constants.h"
 
 namespace lean {
-static name * g_typed_expr_name = nullptr;
-static std::string * g_typed_expr_opcode = nullptr;
-static macro_definition * g_typed_expr = nullptr;
-
-name const & get_typed_expr_name() { return *g_typed_expr_name; }
-std::string const & get_typed_expr_opcode() { return *g_typed_expr_opcode; }
-
-/** \brief This macro is used to "enforce" a given type to an expression.
-    It is equivalent to
-
-        definition typed_expr (A : Type) (a : A) := a
-
-    We use a macro instead of the definition because we want to be able
-    to use in any environment, even one that does not contain the
-    definition 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 check_type(expr const & m, abstract_type_context & ctx, bool infer_only) const {
-        check_macro(m);
-        expr given_type = macro_arg(m, 0);
-        if (!infer_only) {
-            ctx.check(given_type, infer_only);
-            expr inferred_type = ctx.check(macro_arg(m, 1), infer_only);
-            if (!ctx.is_def_eq(inferred_type, given_type)) {
-                throw_kernel_exception(ctx.env(), m, [=](formatter const & fmt) {
-                    return format("type mismatch at term") + pp_type_mismatch(fmt, macro_arg(m, 1), inferred_type, given_type);
-                });
-            }
-        }
-        return given_type;
-    }
-    virtual optional<expr> expand(expr const & m, abstract_type_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());
-    }
-};
-
 bool is_typed_expr(expr const & e) {
-    return is_macro(e) && macro_def(e) == *g_typed_expr;
+    return is_app_of(e, get_typed_expr_name(), 2);
 }
 
 expr mk_typed_expr(expr const & t, expr const & v) {
-    expr args[2] = {t, v};
-    return mk_macro(*g_typed_expr, 2, args);
+    return mk_app(mk_constant(get_typed_expr_name()), t, v);
 }
 
-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); }
-
-void initialize_typed_expr() {
-    g_typed_expr_name = new name("typed_expr");
-    g_typed_expr_opcode = new std::string("TyE");
-    g_typed_expr = new macro_definition(new typed_expr_macro_definition_cell());
-    register_macro_deserializer(*g_typed_expr_opcode,
-                                [](deserializer &, unsigned num, expr const * args) {
-                                    if (num != 2)
-                                        throw corrupted_stream_exception();
-                                    return mk_typed_expr(args[0], args[1]);
-                                });
-}
-
-void finalize_typed_expr() {
-    delete g_typed_expr;
-    delete g_typed_expr_opcode;
-    delete g_typed_expr_name;
-}
+expr get_typed_expr_type(expr const & e) { lean_assert(is_typed_expr(e)); return app_arg(app_fn(e)); }
+expr get_typed_expr_expr(expr const & e) { lean_assert(is_typed_expr(e)); return app_arg(e); }
 }

src/library/typed_expr.h

@@ -19,10 +19,6 @@ bool is_typed_expr(expr const & e);
 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
-*/
+    \remark get_typed_expr_type(mk_typed_expr(t, e)) == e */
 expr get_typed_expr_expr(expr const & e);
-
-void initialize_typed_expr();
-void finalize_typed_expr();
 }

tests/lean/run/check_constants.lean

@@ -341,6 +341,7 @@ run_cmd script_check_id `trans_rel_left
 run_cmd script_check_id `trans_rel_right
 run_cmd script_check_id `true
 run_cmd script_check_id `true.intro
+run_cmd script_check_id `typed_expr
 run_cmd script_check_id `unification_hint
 run_cmd script_check_id `unification_hint.mk
 run_cmd script_check_id `unit