fix(*): revert broken typed_expr refactorings

The refactoring will instead be part of Lean 4

library/init/core.lean

@@ -104,9 +104,6 @@ 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 (α : Sort 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/CMakeLists.txt

@@ -9,4 +9,4 @@ prenum.cpp print_cmd.cpp elaborator.cpp
 match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp
 brackets.cpp tactic_notation.cpp info_manager.cpp json.cpp module_parser.cpp
 interactive.cpp completion.cpp
-user_notation.cpp user_command.cpp typed_expr.cpp)
+user_notation.cpp user_command.cpp)

src/frontends/lean/builtin_cmds.cpp

@@ -31,6 +31,7 @@ Author: Leonardo de Moura
 #include "library/private.h"
 #include "library/type_context.h"
 #include "library/reducible.h"
+#include "library/typed_expr.h"
 #include "library/documentation.h"
 #include "library/placeholder.h"
 #include "library/vm/vm.h"
@@ -52,7 +53,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/parse_table.h"
 #include "frontends/lean/decl_attributes.h"
-#include "frontends/lean/typed_expr.h"
 
 namespace lean {
 environment section_cmd(parser & p) {

src/frontends/lean/builtin_exprs.cpp

@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "library/explicit.h"
 #include "library/aliases.h"
 #include "library/scoped_ext.h"
+#include "library/typed_expr.h"
 #include "library/choice.h"
 #include "library/constants.h"
 #include "library/quote.h"
@@ -35,7 +36,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/brackets.h"
 #include "frontends/lean/tactic_notation.h"
 #include "frontends/lean/elaborator.h"
-#include "frontends/lean/typed_expr.h"
 
 #ifndef LEAN_DEFAULT_PARSER_CHECKPOINT_HAVE
 #define LEAN_DEFAULT_PARSER_CHECKPOINT_HAVE true

src/frontends/lean/calc.cpp

@@ -22,11 +22,11 @@ Author: Leonardo de Moura
 #include "library/explicit.h"
 #include "library/scoped_ext.h"
 #include "library/annotation.h"
+#include "library/typed_expr.h"
 #include "library/sorry.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/tokens.h"
-#include "frontends/lean/typed_expr.h"
 
 namespace lean {
 static name * g_calc_name  = nullptr;

src/frontends/lean/decl_attributes.cpp

@@ -9,12 +9,12 @@ Author: Leonardo de Moura
 #include "library/constants.h"
 #include "library/class.h"
 #include "library/num.h"
+#include "library/typed_expr.h"
 #include "library/vm/vm_nat.h"
 #include "frontends/lean/decl_attributes.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/util.h"
-#include "frontends/lean/typed_expr.h"
 
 namespace lean {
 // ==========================================

src/frontends/lean/definition_cmds.cpp

@@ -19,6 +19,7 @@ Author: Leonardo de Moura
 #include "library/trace.h"
 #include "library/constants.h"
 #include "library/explicit.h"
+#include "library/typed_expr.h"
 #include "library/private.h"
 #include "library/protected.h"
 #include "library/scoped_ext.h"
@@ -41,7 +42,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/decl_util.h"
 #include "frontends/lean/decl_attributes.h"
 #include "frontends/lean/definition_cmds.h"
-#include "frontends/lean/typed_expr.h"
 
 namespace lean {
 environment ensure_decl_namespaces(environment const & env, name const & full_n) {

src/frontends/lean/elaborator.cpp

@@ -30,6 +30,7 @@ Author: Leonardo de Moura
 #include "library/sorry.h"
 #include "library/quote.h"
 #include "library/util.h"
+#include "library/typed_expr.h"
 #include "library/annotation.h"
 #include "library/pp_options.h"
 #include "library/replace_visitor.h"
@@ -62,7 +63,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/structure_cmd.h"
 #include "frontends/lean/structure_instance.h"
 #include "frontends/lean/elaborator.h"
-#include "frontends/lean/typed_expr.h"
 
 #ifndef LEAN_DEFAULT_ELABORATOR_COERCIONS
 #define LEAN_DEFAULT_ELABORATOR_COERCIONS true
@@ -3306,6 +3306,8 @@ 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)) {
@@ -3565,8 +3567,6 @@ 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/frontends/lean/notation_cmd.cpp

@@ -16,12 +16,12 @@ Author: Leonardo de Moura
 #include "library/num.h"
 #include "library/aliases.h"
 #include "library/constants.h"
+#include "library/typed_expr.h"
 #include "library/vm/vm_nat.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/decl_attributes.h"
-#include "frontends/lean/typed_expr.h"
 
 namespace lean {
 static std::string parse_symbol(parser & p, char const * msg) {

src/frontends/lean/parser.cpp

@@ -41,6 +41,7 @@ Author: Leonardo de Moura
 #include "library/module.h"
 #include "library/scoped_ext.h"
 #include "library/explicit.h"
+#include "library/typed_expr.h"
 #include "library/num.h"
 #include "library/string.h"
 #include "library/sorry.h"
@@ -63,7 +64,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/elaborator.h"
 #include "frontends/lean/local_context_adapter.h"
 #include "frontends/lean/structure_instance.h"
-#include "frontends/lean/typed_expr.h"
 
 #ifndef LEAN_DEFAULT_PARSER_SHOW_ERRORS
 #define LEAN_DEFAULT_PARSER_SHOW_ERRORS true

src/frontends/lean/pp.cpp

@@ -26,6 +26,7 @@ Author: Leonardo de Moura
 #include "library/protected.h"
 #include "library/quote.h"
 #include "library/explicit.h"
+#include "library/typed_expr.h"
 #include "library/num.h"
 #include "library/util.h"
 #include "library/print.h"
@@ -51,7 +52,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/parser_config.h"
 #include "frontends/lean/scanner.h"
 #include "frontends/lean/tokens.h"
-#include "frontends/lean/typed_expr.h"
 
 #include "library/trace.h"
 

src/frontends/lean/tactic_notation.cpp

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "library/quote.h"
 #include "library/io_state_stream.h"
 #include "library/trace.h"
+#include "library/typed_expr.h"
 #include "library/placeholder.h"
 #include "library/explicit.h"
 #include "kernel/scope_pos_info_provider.h"
@@ -28,7 +29,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/decl_util.h"
 #include "frontends/lean/pp.h"
 #include "frontends/lean/builtin_exprs.h"
-#include "frontends/lean/typed_expr.h"
 
 /* The auto quotation currently supports two classes of tactics: tactic and smt_tactic.
    To add a new class Tac, we have to

src/frontends/lean/util.cpp

@@ -21,6 +21,7 @@ Author: Leonardo de Moura
 #include "library/explicit.h"
 #include "library/aliases.h"
 #include "library/constants.h"
+#include "library/typed_expr.h"
 #include "library/placeholder.h"
 #include "library/unfold_macros.h"
 #include "library/choice.h"
@@ -35,7 +36,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/decl_util.h" // TODO(Leo): remove
 #include "frontends/lean/prenum.h"
-#include "frontends/lean/typed_expr.h"
 
 #ifndef LEAN_DEFAULT_AUTO_PARAM_CHECK_EXISTS
 #define LEAN_DEFAULT_AUTO_PARAM_CHECK_EXISTS true

src/library/CMakeLists.txt

@@ -5,7 +5,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
   update_declaration.cpp scoped_ext.cpp sorry.cpp replace_visitor.cpp
   explicit.cpp num.cpp string.cpp head_map.cpp
   class.cpp util.cpp print.cpp annotation.cpp quote.cpp
-  protected.cpp reducible.cpp init_module.cpp
+  typed_expr.cpp protected.cpp reducible.cpp init_module.cpp
   exception.cpp fingerprint.cpp pp_options.cpp
   unfold_macros.cpp app_builder.cpp projection.cpp relation_manager.cpp
   export.cpp user_recursors.cpp idx_metavar.cpp noncomputable.cpp

src/library/constants.cpp

@@ -341,7 +341,6 @@ 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;
@@ -699,7 +698,6 @@ 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"};
@@ -1058,7 +1056,6 @@ 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;
@@ -1416,7 +1413,6 @@ 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,7 +343,6 @@ 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,7 +336,6 @@ trans_rel_left
 trans_rel_right
 true
 true.intro
-typed_expr
 unification_hint
 unification_hint.mk
 unit

src/library/init_module.cpp

@@ -7,6 +7,7 @@ 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"
@@ -84,6 +85,7 @@ void initialize_library_module() {
     initialize_idx_metavar();
     initialize_io_state();
     initialize_kernel_serializer();
+    initialize_typed_expr();
     initialize_choice();
     initialize_string();
     initialize_num();
@@ -157,6 +159,7 @@ void finalize_library_module() {
     finalize_num();
     finalize_string();
     finalize_choice();
+    finalize_typed_expr();
     finalize_kernel_serializer();
     finalize_io_state();
     finalize_idx_metavar();