From b37b1fb7c6d3e7183ccc1f18b7fb12bf2bd29bc5 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 28 Apr 2017 10:44:43 +0200 Subject: [PATCH] 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 | 10 ++++++++++ src/library/constants.cpp | 4 ++++ src/library/constants.h | 1 + src/library/constants.txt | 1 + src/library/type_context.cpp | 31 ----------------------------- tests/lean/run/check_constants.lean | 1 + 6 files changed, 17 insertions(+), 31 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index c39e55823f..5f62d38ab3 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/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 diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 91bda07730..c954a0e7c1 100644 --- a/src/library/constants.cpp +++ b/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; } diff --git a/src/library/constants.h b/src/library/constants.h index 715f8c6df2..927c05ab42 100644 --- a/src/library/constants.h +++ b/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(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 56c71c50a5..f30f83217e 100644 --- a/src/library/constants.txt +++ b/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 diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 992ecdd3cc..3f7b12b96e 100644 --- a/src/library/type_context.cpp +++ b/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); diff --git a/tests/lean/run/check_constants.lean b/tests/lean/run/check_constants.lean index 678931ee2f..617359d0a5 100644 --- a/tests/lean/run/check_constants.lean +++ b/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