From a5ae4b65709813d4bcc5a59ca213aadf09b448e9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 1 May 2014 10:35:02 -0700 Subject: [PATCH] feat(kernel): add binder annotations (implicit, cast) Signed-off-by: Leonardo de Moura --- src/kernel/expr.cpp | 32 ++++++++++++++++++++--------- src/kernel/expr.h | 40 +++++++++++++++++++++++++++++-------- src/kernel/type_checker.cpp | 2 +- 3 files changed, 56 insertions(+), 18 deletions(-) diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index 8e17bad6b..b42a4a3ac 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -133,7 +133,7 @@ void expr_app::dealloc(buffer & todelete) { static unsigned dec(unsigned k) { return k == 0 ? 0 : k - 1; } // Expr binders (Lambda, Pi) -expr_binder::expr_binder(expr_kind k, name const & n, expr const & t, expr const & b): +expr_binder::expr_binder(expr_kind k, name const & n, expr const & t, expr const & b, expr_binder_info const & i): expr_composite(k, ::lean::hash(t.hash(), b.hash()), t.has_metavar() || b.has_metavar(), t.has_local() || b.has_local(), @@ -142,7 +142,8 @@ expr_binder::expr_binder(expr_kind k, name const & n, expr const & t, expr const std::max(get_free_var_range(t), dec(get_free_var_range(b)))), m_name(n), m_domain(t), - m_body(b) { + m_body(b), + m_info(i) { lean_assert(k == expr_kind::Lambda || k == expr_kind::Pi); } void expr_binder::dealloc(buffer & todelete) { @@ -389,7 +390,7 @@ expr update_rev_app(expr const & e, unsigned num, expr const * new_args) { expr update_binder(expr const & e, expr const & new_domain, expr const & new_body) { if (!is_eqp(binder_domain(e), new_domain) || !is_eqp(binder_body(e), new_body)) - return mk_binder(e.kind(), binder_name(e), new_domain, new_body); + return mk_binder(e.kind(), binder_name(e), new_domain, new_body, binder_info(e)); else return e; } @@ -468,8 +469,8 @@ expr copy(expr const & a) { case expr_kind::Sort: return mk_sort(sort_level(a)); case expr_kind::Macro: return mk_macro(to_macro(a)->m_definition, macro_num_args(a), macro_args(a)); case expr_kind::App: return mk_app(app_fn(a), app_arg(a)); - case expr_kind::Lambda: return mk_lambda(binder_name(a), binder_domain(a), binder_body(a)); - case expr_kind::Pi: return mk_pi(binder_name(a), binder_domain(a), binder_body(a)); + case expr_kind::Lambda: return mk_lambda(binder_name(a), binder_domain(a), binder_body(a), binder_info(a)); + case expr_kind::Pi: return mk_pi(binder_name(a), binder_domain(a), binder_body(a), binder_info(a)); case expr_kind::Let: return mk_let(let_name(a), let_type(a), let_value(a), let_body(a)); case expr_kind::Meta: return mk_metavar(mlocal_name(a), mlocal_type(a)); case expr_kind::Local: return mk_local(mlocal_name(a), mlocal_type(a)); @@ -477,6 +478,18 @@ expr copy(expr const & a) { lean_unreachable(); // LCOV_EXCL_LINE } +serializer & operator<<(serializer & s, expr_binder_info const & i) { + s.write_bool(i.is_implicit()); + s.write_bool(i.is_cast()); + return s; +} + +static expr_binder_info read_expr_binder_info(deserializer & d) { + bool imp = d.read_bool(); + bool cast = d.read_bool(); + return expr_binder_info(imp, cast); +} + class expr_serializer : public object_serializer { typedef object_serializer super; max_sharing_fn m_max_sharing_fn; @@ -506,7 +519,7 @@ class expr_serializer : public object_serializer { public: expr read_binder(expr_kind k) { deserializer & d = get_owner(); - name n = read_name(d); - expr t = read(); - return mk_binder(k, n, t, read()); + name n = read_name(d); + expr_binder_info i = read_expr_binder_info(d); + expr t = read(); + return mk_binder(k, n, t, read(), i); } expr read() { diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 5758cf3aa..3fed9dcf5 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -72,6 +72,7 @@ public: }; class macro_definition; +class expr_binder_info; /** \brief Exprs for encoding formulas/expressions, types and proofs. @@ -118,7 +119,7 @@ public: friend expr mk_app(expr const & f, expr const & a); friend expr mk_pair(expr const & f, expr const & s, expr const & t); friend expr mk_proj(bool fst, expr const & p); - friend expr mk_binder(expr_kind k, name const & n, expr const & t, expr const & e); + friend expr mk_binder(expr_kind k, name const & n, expr const & t, expr const & e, expr_binder_info const & i); friend expr mk_let(name const & n, expr const & t, expr const & v, expr const & e); friend expr mk_macro(macro_definition * m, unsigned num, expr const * args); @@ -204,18 +205,33 @@ public: expr const & get_arg() const { return m_arg; } }; +/** + \brief Auxiliary annotation for binders (Lambda and Pi). This information + is only used for elaboration. +*/ +class expr_binder_info { + bool m_implicit; //! if true, binder argument is an implicit argument + bool m_cast; //! if true, binder argument is a target for using cast +public: + expr_binder_info(bool implicit = false, bool cast = false):m_implicit(implicit), m_cast(cast) {} + bool is_implicit() const { return m_implicit; } + bool is_cast() const { return m_cast; } +}; + /** \brief Super class for lambda, pi and sigma */ class expr_binder : public expr_composite { - name m_name; - expr m_domain; - expr m_body; + name m_name; + expr m_domain; + expr m_body; + expr_binder_info m_info; friend class expr_cell; void dealloc(buffer & todelete); public: - expr_binder(expr_kind k, name const & n, expr const & t, expr const & e); + expr_binder(expr_kind k, name const & n, expr const & t, expr const & e, expr_binder_info const & i = expr_binder_info()); name const & get_name() const { return m_name; } expr const & get_domain() const { return m_domain; } expr const & get_body() const { return m_body; } + expr_binder_info const & get_info() const { return m_info; } }; /** \brief Let expressions */ @@ -354,9 +370,15 @@ template expr mk_app(T const & args) { return mk_app(args.size(), ar expr mk_rev_app(unsigned num_args, expr const * args); template expr mk_rev_app(T const & args) { return mk_rev_app(args.size(), args.data()); } template expr mk_rev_app(expr const & f, T const & args) { return mk_rev_app(f, args.size(), args.data()); } -inline expr mk_binder(expr_kind k, name const & n, expr const & t, expr const & e) { return expr(new expr_binder(k, n, t, e)); } -inline expr mk_lambda(name const & n, expr const & t, expr const & e) { return mk_binder(expr_kind::Lambda, n, t, e); } -inline expr mk_pi(name const & n, expr const & t, expr const & e) { return mk_binder(expr_kind::Pi, n, t, e); } +inline expr mk_binder(expr_kind k, name const & n, expr const & t, expr const & e, expr_binder_info const & i = expr_binder_info()) { + return expr(new expr_binder(k, n, t, e, i)); +} +inline expr mk_lambda(name const & n, expr const & t, expr const & e, expr_binder_info const & i = expr_binder_info()) { + return mk_binder(expr_kind::Lambda, n, t, e, i); +} +inline expr mk_pi(name const & n, expr const & t, expr const & e, expr_binder_info const & i = expr_binder_info()) { + return mk_binder(expr_kind::Pi, n, t, e, i); +} inline expr mk_let(name const & n, expr const & t, expr const & v, expr const & e) { return expr(new expr_let(n, t, v, e)); } inline expr mk_sort(level const & l) { return expr(new expr_sort(l)); } @@ -444,6 +466,7 @@ inline expr const & app_arg(expr_cell * e) { return to_app(e)->g inline name const & binder_name(expr_cell * e) { return to_binder(e)->get_name(); } inline expr const & binder_domain(expr_cell * e) { return to_binder(e)->get_domain(); } inline expr const & binder_body(expr_cell * e) { return to_binder(e)->get_body(); } +inline expr_binder_info const & binder_info(expr_cell * e) { return to_binder(e)->get_info(); } inline level const & sort_level(expr_cell * e) { return to_sort(e)->get_level(); } inline name const & let_name(expr_cell * e) { return to_let(e)->get_name(); } inline expr const & let_value(expr_cell * e) { return to_let(e)->get_value(); } @@ -467,6 +490,7 @@ inline expr const & app_arg(expr const & e) { return to_app(e)-> inline name const & binder_name(expr const & e) { return to_binder(e)->get_name(); } inline expr const & binder_domain(expr const & e) { return to_binder(e)->get_domain(); } inline expr const & binder_body(expr const & e) { return to_binder(e)->get_body(); } +inline expr_binder_info const & binder_info(expr const & e) { return to_binder(e)->get_info(); } inline level const & sort_level(expr const & e) { return to_sort(e)->get_level(); } inline name const & let_name(expr const & e) { return to_let(e)->get_name(); } inline expr const & let_value(expr const & e) { return to_let(e)->get_value(); } diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 1e55e55fe..11a0e571b 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -377,7 +377,7 @@ struct type_checker::imp { ensure_sort(t, binder_domain(e)); } auto b = open_binder_body(e); - r = mk_pi(binder_name(e), binder_domain(e), abstract_p(infer_type_core(b.first, infer_only), b.second)); + r = mk_pi(binder_name(e), binder_domain(e), abstract_p(infer_type_core(b.first, infer_only), b.second), binder_info(e)); break; } case expr_kind::Pi: {