From 6a6c9f472e3903e1f2c91817abed18ddcaca2cc5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 15 Aug 2014 12:45:54 -0700 Subject: [PATCH] feat(frontends/lean): add synthesis information only for 'explicit' placeholder Signed-off-by: Leonardo de Moura --- src/frontends/lean/builtin_exprs.cpp | 2 +- src/frontends/lean/elaborator.cpp | 16 ++++++++------ src/library/placeholder.cpp | 31 +++++++++++++++++++++------- src/library/placeholder.h | 17 +++++++++++---- 4 files changed, 48 insertions(+), 18 deletions(-) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 9855f1f42..e4a259001 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -130,7 +130,7 @@ static expr parse_let_expr(parser & p, unsigned, expr const *, pos_info const & } static expr parse_placeholder(parser & p, unsigned, expr const *, pos_info const & pos) { - return p.save_pos(mk_expr_placeholder(), pos); + return p.save_pos(mk_explicit_expr_placeholder(), pos); } static expr parse_by(parser & p, unsigned, expr const *, pos_info const & pos) { diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 85ce12d35..98d156182 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -648,11 +648,17 @@ public: return none_expr(); } + void save_placeholder_info(expr const & e, expr const & r) { + if (is_explicit_placeholder(e)) { + save_info_data(e, r); + save_synth_data(e, r); + } + } + expr visit_expecting_type(expr const & e) { if (is_placeholder(e) && !placeholder_type(e)) { expr r = m_context.mk_type_meta(e.get_tag()); - save_info_data(e, r); - save_synth_data(e, r); + save_placeholder_info(e, r); return r; } else { return visit(e); @@ -662,8 +668,7 @@ public: expr visit_expecting_type_of(expr const & e, expr const & t) { if (is_placeholder(e) && !placeholder_type(e)) { expr r = mk_placeholder_meta(some_expr(t), e.get_tag(), is_strict_placeholder(e)); - save_info_data(e, r); - save_synth_data(e, r); + save_placeholder_info(e, r); return r; } else if (is_choice(e)) { return visit_choice(e, some_expr(t)); @@ -865,8 +870,7 @@ public: expr visit_placeholder(expr const & e) { expr r = mk_placeholder_meta(placeholder_type(e), e.get_tag(), is_strict_placeholder(e)); - save_info_data(e, r); - save_synth_data(e, r); + save_placeholder_info(e, r); return r; } diff --git a/src/library/placeholder.cpp b/src/library/placeholder.cpp index fb97dac45..e1c28bbb0 100644 --- a/src/library/placeholder.cpp +++ b/src/library/placeholder.cpp @@ -10,8 +10,10 @@ Author: Leonardo de Moura #include "library/kernel_bindings.h" namespace lean { -static name g_placeholder_name = name(name::mk_internal_unique_name(), "_"); -static name g_strict_placeholder_name = name(name::mk_internal_unique_name(), "_"); +static name g_implicit_placeholder_name = name(name::mk_internal_unique_name(), "_"); +static name const & g_placeholder_name = g_implicit_placeholder_name; +static name g_strict_placeholder_name = name(name::mk_internal_unique_name(), "_"); +static name g_explicit_placeholder_name = name(name::mk_internal_unique_name(), "_"); MK_THREAD_LOCAL_GET(unsigned, get_placeholder_id, 0) static unsigned next_placeholder_id() { unsigned & c = get_placeholder_id(); @@ -20,20 +22,33 @@ static unsigned next_placeholder_id() { return r; } level mk_level_placeholder() { return mk_global_univ(name(g_placeholder_name, next_placeholder_id())); } -expr mk_expr_placeholder(optional const & type, bool strict) { - name const & prefix = strict ? g_strict_placeholder_name : g_placeholder_name; - name n(prefix, next_placeholder_id()); +static name const & to_prefix(expr_placeholder_kind k) { + switch (k) { + case expr_placeholder_kind::Implicit: return g_implicit_placeholder_name; + case expr_placeholder_kind::StrictImplicit: return g_strict_placeholder_name; + case expr_placeholder_kind::Explicit: return g_explicit_placeholder_name; + } + lean_unreachable(); // LCOV_EXCL_LINE +} +expr mk_expr_placeholder(optional const & type, expr_placeholder_kind k) { + name n(to_prefix(k), next_placeholder_id()); if (type) return mk_local(n, *type); else return mk_constant(n); } static bool is_placeholder(name const & n) { - return !n.is_atomic() && (n.get_prefix() == g_placeholder_name || n.get_prefix() == g_strict_placeholder_name); + if (n.is_atomic()) + return false; + name const & p = n.get_prefix(); + return p == g_implicit_placeholder_name || p == g_strict_placeholder_name || p == g_explicit_placeholder_name; } static bool is_strict_placeholder(name const & n) { return !n.is_atomic() && n.get_prefix() == g_strict_placeholder_name; } +static bool is_explicit_placeholder(name const & n) { + return !n.is_atomic() && n.get_prefix() == g_explicit_placeholder_name; +} bool is_placeholder(level const & e) { return is_global(e) && is_placeholder(global_id(e)); } bool is_placeholder(expr const & e) { return (is_constant(e) && is_placeholder(const_name(e))) || (is_local(e) && is_placeholder(mlocal_name(e))); @@ -41,7 +56,9 @@ bool is_placeholder(expr const & e) { bool is_strict_placeholder(expr const & e) { return (is_constant(e) && is_strict_placeholder(const_name(e))) || (is_local(e) && is_strict_placeholder(mlocal_name(e))); } - +bool is_explicit_placeholder(expr const & e) { + return (is_constant(e) && is_explicit_placeholder(const_name(e))) || (is_local(e) && is_explicit_placeholder(mlocal_name(e))); +} optional placeholder_type(expr const & e) { if (is_local(e) && is_placeholder(e)) return some_expr(mlocal_type(e)); diff --git a/src/library/placeholder.h b/src/library/placeholder.h index 9f122a0e2..ce3196d58 100644 --- a/src/library/placeholder.h +++ b/src/library/placeholder.h @@ -14,19 +14,28 @@ namespace lean { /** \brief Return a new universe level placeholder. */ level mk_level_placeholder(); +enum class expr_placeholder_kind { Implicit, StrictImplicit, Explicit }; /** \brief Return a new expression placeholder expression. */ -expr mk_expr_placeholder(optional const & type = none_expr(), bool strict = false); -inline expr mk_strict_expr_placeholder(optional const & type = none_expr()) { return mk_expr_placeholder(type, true); } +expr mk_expr_placeholder(optional const & type = none_expr(), expr_placeholder_kind k = expr_placeholder_kind::Implicit); +inline expr mk_explicit_expr_placeholder(optional const & type = none_expr()) { + return mk_expr_placeholder(type, expr_placeholder_kind::Explicit); +} +inline expr mk_strict_expr_placeholder(optional const & type = none_expr()) { + return mk_expr_placeholder(type, expr_placeholder_kind::StrictImplicit); +} /** \brief Return true if the given level is a placeholder. */ bool is_placeholder(level const & e); -/** \brief Return true iff the given expression is a placeholder (strict or not). */ +/** \brief Return true iff the given expression is a placeholder (strict, explicit or implicit). */ bool is_placeholder(expr const & e); -/** \brief Return true iff the given expression is a strict placeholder (strict or not). */ +/** \brief Return true iff the given expression is a strict placeholder. */ bool is_strict_placeholder(expr const & e); +/** \brief Return true iff the given expression is an explicit placeholder. */ +bool is_explicit_placeholder(expr const & e); + /** \brief Return the type of the placeholder (if available) */ optional placeholder_type(expr const & e);