refactor(library/type_context,frontends/lean/elaborator): move reflected code back into elaborator

Since we do not want recursive special handling of `reflected`, this seems to be
the simpler design.

src/frontends/lean/elaborator.cpp

@@ -264,6 +264,16 @@ expr elaborator::mk_type_metavar(expr const & ref) {
 }
 
 expr elaborator::mk_instance_core(local_context const & lctx, expr const & C, expr const & ref) {
+    // synthesize `reflected e` by quoting e
+    if (is_app_of(C, get_reflected_name(), 2)) {
+        expr const & r = app_arg(C);
+        if (closed(r) && !has_local(r)) {
+            expr r_ty = app_arg(app_fn(C));
+            level l = *::lean::dec_level(::lean::get_level(m_ctx, r_ty));
+            return mk_reflected(r, r_ty, l);
+        }
+    }
+
     scope_traces_as_messages traces_as_messages(get_pos_info_provider(), ref);
 
     // TODO(gabriel): cache failures so that we do not report errors twice

src/library/constants.cpp

@@ -312,6 +312,7 @@ name const * g_real_has_mul = nullptr;
 name const * g_real_has_sub = nullptr;
 name const * g_real_has_lt = nullptr;
 name const * g_real_has_le = nullptr;
+name const * g_reflected = nullptr;
 name const * g_rfl = nullptr;
 name const * g_right_distrib = nullptr;
 name const * g_ring = nullptr;
@@ -683,6 +684,7 @@ void initialize_constants() {
     g_real_has_sub = new name{"real", "has_sub"};
     g_real_has_lt = new name{"real", "has_lt"};
     g_real_has_le = new name{"real", "has_le"};
+    g_reflected = new name{"reflected"};
     g_rfl = new name{"rfl"};
     g_right_distrib = new name{"right_distrib"};
     g_ring = new name{"ring"};
@@ -1055,6 +1057,7 @@ void finalize_constants() {
     delete g_real_has_sub;
     delete g_real_has_lt;
     delete g_real_has_le;
+    delete g_reflected;
     delete g_rfl;
     delete g_right_distrib;
     delete g_ring;
@@ -1426,6 +1429,7 @@ name const & get_real_has_mul_name() { return *g_real_has_mul; }
 name const & get_real_has_sub_name() { return *g_real_has_sub; }
 name const & get_real_has_lt_name() { return *g_real_has_lt; }
 name const & get_real_has_le_name() { return *g_real_has_le; }
+name const & get_reflected_name() { return *g_reflected; }
 name const & get_rfl_name() { return *g_rfl; }
 name const & get_right_distrib_name() { return *g_right_distrib; }
 name const & get_ring_name() { return *g_ring; }

src/library/constants.h

@@ -314,6 +314,7 @@ name const & get_real_has_mul_name();
 name const & get_real_has_sub_name();
 name const & get_real_has_lt_name();
 name const & get_real_has_le_name();
+name const & get_reflected_name();
 name const & get_rfl_name();
 name const & get_right_distrib_name();
 name const & get_ring_name();

src/library/constants.txt

@@ -307,6 +307,7 @@ real.has_mul
 real.has_sub
 real.has_lt
 real.has_le
+reflected
 rfl
 right_distrib
 ring

src/library/type_context.cpp

@@ -3488,40 +3488,9 @@ struct instance_synthesizer {
         return false;
     }
 
-    bool process_special(stack_entry const & e) {
-        expr const & mvar_type = mlocal_type(e.m_mvar);
-        if (is_app_of(mvar_type, "reflected", 2)) {
-            expr const & r = app_arg(mvar_type);
-            if (!closed(r) || has_local(r)) {
-                lean_trace_plain("class_instances",
-                                 scope_trace_env scope(m_ctx.env(), m_ctx);
-                                 tout() << "not using special support for `reflected` synthesis because '" << r
-                                        << "' is not closed and locals-free";);
-
-                return false;
-            }
-            expr r_ty = app_arg(app_fn(mvar_type));
-            level l = *dec_level(get_level(m_ctx, r_ty));
-            lean_trace_plain("class_instances",
-                             scope_trace_env scope(m_ctx.env(), m_ctx);
-                             trace(e.m_depth, e.m_mvar, mvar_type, r););
-            if (!m_ctx.is_def_eq(e.m_mvar, mk_reflected(r, r_ty, l))) {
-                lean_trace_plain("class_instances", tout() << "failed is_def_eq\n";);
-                return false;
-            } else {
-                return true;
-            }
-        }
-        return false;
-    }
-
     bool process_next_mvar() {
         lean_assert(!is_done());
         stack_entry e = head(m_state.m_stack);
-        if (process_special(e)) {
-            m_state.m_stack = tail(m_state.m_stack);
-            return true;
-        }
         if (!mk_choice_point(e.m_mvar))
             return false;
         m_state.m_stack = tail(m_state.m_stack);

tests/lean/run/check_constants.lean

@@ -312,6 +312,7 @@ run_cmd script_check_id `real.has_mul
 run_cmd script_check_id `real.has_sub
 run_cmd script_check_id `real.has_lt
 run_cmd script_check_id `real.has_le
+run_cmd script_check_id `reflected
 run_cmd script_check_id `rfl
 run_cmd script_check_id `right_distrib
 run_cmd script_check_id `ring