diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index a34065b1c..f103feb8a 100644 --- a/src/kernel/CMakeLists.txt +++ b/src/kernel/CMakeLists.txt @@ -3,8 +3,8 @@ for_each_fn.cpp occurs.cpp replace_fn.cpp free_vars.cpp abstract.cpp instantiate.cpp context.cpp formatter.cpp max_sharing.cpp kernel_exception.cpp object.cpp environment.cpp replace_visitor.cpp io_state.cpp normalizer.cpp justification.cpp pos_info_provider.cpp metavar.cpp +constraint.cpp # type_checker.cpp -# unification_constraint.cpp # type_checker_justification.cpp ) diff --git a/src/kernel/constraint.cpp b/src/kernel/constraint.cpp new file mode 100644 index 000000000..2862c0937 --- /dev/null +++ b/src/kernel/constraint.cpp @@ -0,0 +1,140 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "util/rc.h" +#include "kernel/constraint.h" +namespace lean { +struct constraint_cell { + void dealloc(); + MK_LEAN_RC() + constraint_kind m_kind; + unsigned m_hash; + justification m_jst; + constraint_cell(constraint_kind k, unsigned h, justification const & j):m_rc(1), m_kind(k), m_hash(h), m_jst(j) {} +}; +struct eqc_constraint_cell : public constraint_cell { + expr m_lhs; + expr m_rhs; + eqc_constraint_cell(constraint_kind k, expr const & lhs, expr const & rhs, justification const & j): + constraint_cell(k, hash(hash(lhs.hash(), rhs.hash()), static_cast(k)), j), + m_lhs(lhs), m_rhs(rhs) {} +}; +struct level_constraint_cell : public constraint_cell { + level m_lhs; + level m_rhs; + level_constraint_cell(level const & lhs, level const & rhs, justification const & j): + constraint_cell(constraint_kind::Level, hash(hash(lhs), hash(rhs)), j), + m_lhs(lhs), m_rhs(rhs) {} +}; +static unsigned hash(list const & ls) { + return is_nil(ls) ? 17 : hash(car(ls).hash(), hash(cdr(ls))); +} +struct choice_constraint_cell : public constraint_cell { + expr m_expr; + list m_choices; + choice_constraint_cell(expr const & e, list const & s, justification const & j): + constraint_cell(constraint_kind::Choice, hash(e.hash(), hash(s)), j), + m_expr(e), m_choices(s) {} +}; + +constraint::constraint(constraint_cell * ptr):m_ptr(ptr) { lean_assert(m_ptr->get_rc() == 1); } +constraint::constraint(constraint const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); } +constraint::constraint(constraint && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } +constraint::~constraint() { if (m_ptr) m_ptr->dec_ref(); } +constraint & constraint::operator=(constraint const & c) { LEAN_COPY_REF(c); } +constraint & constraint::operator=(constraint && c) { LEAN_MOVE_REF(c); } +constraint_kind constraint::kind() const { lean_assert(m_ptr); return m_ptr->m_kind; } +unsigned constraint::hash() const { lean_assert(m_ptr); return m_ptr->m_hash; } +justification const & constraint::get_justification() const { lean_assert(m_ptr); return m_ptr->m_jst; } + +constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j) { + return constraint(new eqc_constraint_cell(constraint_kind::Eq, lhs, rhs, j)); +} +constraint mk_conv_cnstr(expr const & lhs, expr const & rhs, justification const & j) { + return constraint(new eqc_constraint_cell(constraint_kind::Convertible, lhs, rhs, j)); +} +constraint mk_level_cnstr(level const & lhs, level const & rhs, justification const & j) { + return constraint(new level_constraint_cell(lhs, rhs, j)); +} +constraint mk_choice_cnstr(expr const & t, list const & s, justification const & j) { + return constraint(new choice_constraint_cell(t, s, j)); +} + +bool operator==(constraint const & c1, constraint const & c2) { + if (c1.kind() != c2.kind() || c1.hash() != c2.hash()) + return false; + switch (c1.kind()) { + case constraint_kind::Eq: case constraint_kind::Convertible: + return cnstr_lhs_expr(c1) == cnstr_lhs_expr(c2) && cnstr_rhs_expr(c1) == cnstr_rhs_expr(c2); + case constraint_kind::Level: + return cnstr_lhs_level(c1) == cnstr_lhs_level(c2) && cnstr_rhs_level(c1) == cnstr_rhs_level(c2); + case constraint_kind::Choice: + return + cnstr_choice_expr(c1) == cnstr_choice_expr(c2) && + compare(cnstr_choice_set(c1), cnstr_choice_set(c2), [](expr const & e1, expr const & e2) { return e1 == e2; }); + } +} + +expr const & cnstr_lhs_expr(constraint const & c) { lean_assert(is_eqc_cnstr(c)); return static_cast(c.raw())->m_lhs; } +expr const & cnstr_rhs_expr(constraint const & c) { lean_assert(is_eqc_cnstr(c)); return static_cast(c.raw())->m_rhs; } +level const & cnstr_lhs_level(constraint const & c) { + lean_assert(is_level_cnstr(c)); return static_cast(c.raw())->m_lhs; +} +level const & cnstr_rhs_level(constraint const & c) { + lean_assert(is_level_cnstr(c)); return static_cast(c.raw())->m_rhs; +} +expr const & cnstr_choice_expr(constraint const & c) { + lean_assert(is_choice_cnstr(c)); return static_cast(c.raw())->m_expr; +} +list const & cnstr_choice_set(constraint const & c) { + lean_assert(is_choice_cnstr(c)); return static_cast(c.raw())->m_choices; +} + +constraint updt_eqc_cnstr(constraint const & c, expr const & new_lhs, expr const & new_rhs, justification const & new_jst) { + lean_assert(is_eqc_cnstr(c)); + if (!is_eqp(cnstr_lhs_expr(c), new_lhs) || !is_eqp(cnstr_rhs_expr(c), new_rhs)) { + if (is_eq_cnstr(c)) + return mk_eq_cnstr(new_lhs, new_rhs, new_jst); + else + return mk_conv_cnstr(new_lhs, new_rhs, new_jst); + } else { + return c; + } +} +constraint updt_eqc_cnstr(constraint const & c, expr const & new_lhs, expr const & new_rhs) { + return updt_eqc_cnstr(c, new_lhs, new_rhs, c.get_justification()); +} +constraint updt_level_cnstr(constraint const & c, level const & new_lhs, level const & new_rhs, justification const & new_jst) { + lean_assert(is_level_cnstr(c)); + if (!is_eqp(cnstr_lhs_level(c), new_lhs) || !is_eqp(cnstr_rhs_level(c), new_rhs)) + return mk_level_cnstr(new_lhs, new_rhs, new_jst); + else + return c; +} +constraint updt_level_cnstr(constraint const & c, level const & new_lhs, level const & new_rhs) { + return updt_level_cnstr(c, new_lhs, new_rhs, c.get_justification()); +} + +std::ostream & operator<<(std::ostream & out, constraint const & c) { + switch (c.kind()) { + case constraint_kind::Eq: + out << cnstr_lhs_expr(c) << " ≈ " << cnstr_rhs_expr(c); + case constraint_kind::Convertible: + out << cnstr_lhs_expr(c) << " ↠ " << cnstr_rhs_expr(c); + case constraint_kind::Level: + out << cnstr_lhs_level(c) << " ≤ " << cnstr_rhs_level(c); + case constraint_kind::Choice: + out << cnstr_choice_expr(c) << " ∊ {"; + bool first = true; + for (expr const & e : cnstr_choice_set(c)) { + if (first) first = false; else out << ", "; + out << e; + } + out << "}"; + } + return out; +} +} diff --git a/src/kernel/constraint.h b/src/kernel/constraint.h new file mode 100644 index 000000000..ebd0e2879 --- /dev/null +++ b/src/kernel/constraint.h @@ -0,0 +1,97 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "kernel/expr.h" +#include "kernel/justification.h" +namespace lean { +/** + \brief The lean kernel type checker produces three kinds of constraints: + + - Equality constraint: t ≈ s + The terms t and s must be definitionally equal. + - Convertability constraint: t ↠ s + The term t must be convertible to s + - Universe level constaint: l ≤ m + The universe level l must be less than or equal to m. + + \remark The first two kinds are only generated if the input term + contains metavariables. + + Each constraint is associated with a justification object. + + Finally, we also include a choice constraint. The choice is an auxiliary + constraint used to implement overloading and coercions in Lean. + This constraint is not generated by the kernel. + A choice constraint has the form: + t ∊ {s_1, ..., s_k} + It means, t must be definitionally equal to one of the terms in the (finite) + set {s_1, ..., s_k}. +*/ +enum constraint_kind { Eq, Convertible, Level, Choice }; +struct constraint_cell; +class constraint { + constraint_cell * m_ptr; + constraint(constraint_cell * ptr); +public: + constraint(constraint const & c); + constraint(constraint && s); + ~constraint(); + + constraint_kind kind() const; + unsigned hash() const; + justification const & get_justification() const; + + constraint & operator=(constraint const & c); + constraint & operator=(constraint && c); + + friend bool is_eqp(constraint const & c1, constraint const & c2) { return c1.m_ptr == c2.m_ptr; } + friend void swap(constraint & l1, constraint & l2) { std::swap(l1, l2); } + + friend constraint mk_eq_cnstr(expr const & lhs, expr const & rhs, justification const & j); + friend constraint mk_conv_cnstr(expr const & lhs, expr const & rhs, justification const & j); + friend constraint mk_level_cnstr(level const & lhs, level const & rhs, justification const & j); + friend constraint mk_choice_cnstr(expr const & t, list const & s, justification const & j); + + constraint_cell * raw() const { return m_ptr; } +}; + +bool operator==(constraint const & c1, constraint const & c2); +inline bool operator!=(constraint const & c1, constraint const & c2) { return !(c1 == c2); } + +bool is_eq_cnstr(constraint const & c) { return c.kind() == constraint_kind::Eq; } +bool is_conv_cnstr(constraint const & c) { return c.kind() == constraint_kind::Convertible; } +bool is_level_cnstr(constraint const & c) { return c.kind() == constraint_kind::Level; } +bool is_choice_cnstr(constraint const & c) { return c.kind() == constraint_kind::Choice; } +bool is_eqc_cnstr(constraint const & c) { return is_eq_cnstr(c) || is_conv_cnstr(c); } + +/** \brief Return the lhs of an equality/convertability constraint. */ +expr const & cnstr_lhs_expr(constraint const & c); +/** \brief Return the rhs of an equality/convertability constraint. */ +expr const & cnstr_rhs_expr(constraint const & c); +/** \brief Return the lhs of an level constraint. */ +level const & cnstr_lhs_level(constraint const & c); +/** \brief Return the rhs of an level constraint. */ +level const & cnstr_rhs_level(constraint const & c); +/** \brief Return the main term a choice constraint. */ +expr const & cnstr_choice_expr(constraint const & c); +/** \brief Return the choice set of a choice constraint. */ +list const & cnstr_choice_set(constraint const & c); + +/** \brief Update equality/convertability constraint c with new_lhs, new_rhs and justification. */ +constraint updt_eqc_cnstr(constraint const & c, expr const & new_lhs, expr const & new_rhs, justification const & new_jst); +/** \brief Update equality/convertability constraint c with new_lhs and new_rhs, but keeping the same justification. */ +constraint updt_eqc_cnstr(constraint const & c, expr const & new_lhs, expr const & new_rhs); +/** \brief Update level constraint c with new_lhs, new_rhs and justification. */ +constraint updt_level_cnstr(constraint const & c, level const & new_lhs, level const & new_rhs, justification const & new_jst); +/** \brief Update level constraint c with new_lhs and new_rhs, but keeping the same justification. */ +constraint updt_level_cnstr(constraint const & c, level const & new_lhs, level const & new_rhs); + +/** \brief Printer for debugging purposes */ +std::ostream & operator<<(std::ostream & out, constraint const & c); + +typedef list constraints; +} diff --git a/src/kernel/unification_constraint.cpp b/src/kernel/unification_constraint.cpp deleted file mode 100644 index d4b24ca5d..000000000 --- a/src/kernel/unification_constraint.cpp +++ /dev/null @@ -1,174 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include "kernel/unification_constraint.h" -#include "kernel/metavar.h" - -namespace lean { -unification_constraint_cell::unification_constraint_cell(unification_constraint_kind k, context const & c, justification const & j): - m_kind(k), m_ctx(c), m_justification(j), m_rc(1) { -} -unification_constraint_cell::~unification_constraint_cell() { -} -void unification_constraint_cell::dealloc() { - delete this; -} - -static format add_context(formatter const & fmt, options const & opts, context const & ctx, format const & body, optional const & menv) { - bool unicode = get_pp_unicode(opts); - format ctx_fmt = fmt(instantiate_metavars(menv, ctx), opts); - format turnstile = unicode ? format("\u22A2") /* ⊢ */ : format("|-"); - return group(format{ctx_fmt, space(), turnstile, line(), body}); -} - -static format add_justification(formatter const & fmt, options const & opts, format const & body, justification const & jst, pos_info_provider const * p, bool include_justification, optional const & menv) { - if (jst && include_justification) { - unsigned indent = get_pp_indent(opts); - return format{body, line(), format("Justification:"), nest(indent, compose(line(), jst.pp(fmt, opts, p, true, menv)))}; - } else { - return body; - } -} - -static format mk_binary(formatter const & fmt, options const & opts, context const & ctx, expr const & lhs, expr const & rhs, format const & op, - optional const & menv) { - format lhs_fmt = fmt(ctx, instantiate_metavars(menv, lhs), false, opts); - format rhs_fmt = fmt(ctx, instantiate_metavars(menv, rhs), false, opts); - return group(format{lhs_fmt, space(), op, line(), rhs_fmt}); -} - -static format mk_unification_op(options const & opts) { - bool unicode = get_pp_unicode(opts); - return unicode ? format("\u2248") /* ≈ */ : format("=?="); -} - -unification_constraint_eq::unification_constraint_eq(context const & c, expr const & lhs, expr const & rhs, justification const & j): - unification_constraint_cell(unification_constraint_kind::Eq, c, j), - m_lhs(lhs), - m_rhs(rhs) { -} - -unification_constraint_eq::~unification_constraint_eq() { -} - -format unification_constraint_eq::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification, - optional const & menv) const { - format op = mk_unification_op(opts); - format body = mk_binary(fmt, opts, m_ctx, m_lhs, m_rhs, op, menv); - body = add_context(fmt, opts, m_ctx, body, menv); - return add_justification(fmt, opts, body, m_justification, p, include_justification, menv); -} - -unification_constraint unification_constraint_eq::updt_justification(justification const & j) const { - return mk_eq_constraint(m_ctx, m_lhs, m_rhs, j); -} - -unification_constraint_convertible::unification_constraint_convertible(context const & c, expr const & from, expr const & to, justification const & j): - unification_constraint_cell(unification_constraint_kind::Convertible, c, j), - m_from(from), - m_to(to) { -} - -unification_constraint_convertible::~unification_constraint_convertible() { -} - -format unification_constraint_convertible::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, - bool include_justification, optional const & menv) const { - bool unicode = get_pp_unicode(opts); - format op = unicode ? format("\u227A") /* ≺ */ : format("<<"); - format body = mk_binary(fmt, opts, m_ctx, m_from, m_to, op, menv); - body = add_context(fmt, opts, m_ctx, body, menv); - return add_justification(fmt, opts, body, m_justification, p, include_justification, menv); -} - -unification_constraint unification_constraint_convertible::updt_justification(justification const & j) const { - return mk_convertible_constraint(m_ctx, m_from, m_to, j); -} - -unification_constraint_max::unification_constraint_max(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, justification const & j): - unification_constraint_cell(unification_constraint_kind::Max, c, j), - m_lhs1(lhs1), - m_lhs2(lhs2), - m_rhs(rhs) { -} - -unification_constraint_max::~unification_constraint_max() { -} - -format unification_constraint_max::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification, - optional const & menv) const { - format op = mk_unification_op(opts); - format lhs1_fmt = fmt(m_ctx, instantiate_metavars(menv, m_lhs1), false, opts); - format lhs2_fmt = fmt(m_ctx, instantiate_metavars(menv, m_lhs2), false, opts); - format rhs_fmt = fmt(m_ctx, instantiate_metavars(menv, m_rhs), false, opts); - format body = group(format{format("max"), lp(), lhs1_fmt, comma(), nest(4, compose(line(), lhs2_fmt)), rp(), space(), op, line(), rhs_fmt}); - body = add_context(fmt, opts, m_ctx, body, menv); - return add_justification(fmt, opts, body, m_justification, p, include_justification, menv); -} - -unification_constraint unification_constraint_max::updt_justification(justification const & j) const { - return mk_max_constraint(m_ctx, m_lhs1, m_lhs2, m_rhs, j); -} - -unification_constraint_choice::unification_constraint_choice(context const & c, expr const & mvar, unsigned num, expr const * choices, justification const & j): - unification_constraint_cell(unification_constraint_kind::Choice, c, j), - m_mvar(mvar), - m_choices(choices, choices + num) { -} - -unification_constraint_choice::~unification_constraint_choice() { -} - -format unification_constraint_choice::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification, - optional const & menv) const { - bool unicode = get_pp_unicode(opts); - format m_fmt = fmt(m_ctx, m_mvar, false, opts); - format eq_op = mk_unification_op(opts); - format or_op = unicode ? format("\u2295") : format("OR"); - format body; - for (unsigned i = 0; i < m_choices.size(); i++) { - body += group(paren(format{m_fmt, space(), eq_op, compose(line(), fmt(m_ctx, instantiate_metavars(menv, m_choices[i]), false, opts))})); - if (i + 1 < m_choices.size()) - body += format{space(), or_op, line()}; - } - body = group(body); - body = add_context(fmt, opts, m_ctx, body, menv); - return add_justification(fmt, opts, body, m_justification, p, include_justification, menv); -} - -unification_constraint unification_constraint_choice::updt_justification(justification const & j) const { - return mk_choice_constraint(m_ctx, m_mvar, m_choices.size(), m_choices.data(), j); -} - -format unification_constraint::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification, - optional const & menv) const { - return m_ptr->pp(fmt, opts, p, include_justification, menv); -} - -format unification_constraint::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification) const { - return pp(fmt, opts, p, include_justification, optional()); -} - -unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, justification const & j) { - return unification_constraint(new unification_constraint_eq(c, lhs, rhs, j)); -} - -unification_constraint mk_convertible_constraint(context const & c, expr const & from, expr const & to, justification const & j) { - return unification_constraint(new unification_constraint_convertible(c, from, to, j)); -} - -unification_constraint mk_max_constraint(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, justification const & j) { - return unification_constraint(new unification_constraint_max(c, lhs1, lhs2, rhs, j)); -} - -unification_constraint mk_choice_constraint(context const & c, expr const & mvar, unsigned num, expr const * choices, justification const & j) { - return unification_constraint(new unification_constraint_choice(c, mvar, num, choices, j)); -} - -unification_constraint mk_choice_constraint(context const & c, expr const & mvar, std::initializer_list const & choices, justification const & j) { - return mk_choice_constraint(c, mvar, choices.size(), choices.begin(), j); -} -} diff --git a/src/kernel/unification_constraint.h b/src/kernel/unification_constraint.h deleted file mode 100644 index 14dd37b78..000000000 --- a/src/kernel/unification_constraint.h +++ /dev/null @@ -1,214 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include -#include -#include "kernel/expr.h" -#include "kernel/context.h" -#include "kernel/justification.h" - -namespace lean { -class metavar_env; -class unification_constraint; -/** - \brief There are four kinds of unification constraints in Lean - - 1- ctx |- t == s t is (definitionally) equal to s - 2- ctx |- t << s t is convertible to s (this is weaker than equality) - 3- ctx |- max(t1, t2) == s The maximum of t1 and t2 is equal to s, if t2 is Bool, then s is Bool. - 4- ctx |- ?m == t_1 Or ... Or ?m == t_k The metavariable ?m is equal to t_1, ..., or t_k - - \remark The constraint ctx |- t == s implies that ctx |- t << s, but - the converse is not true. Example: ctx |- Type 1 << Type 2, but - we don't have ctx |- Type 1 == Type 2. - - \remark In the max constraint, \c t1 and \c t2 must be eventually unifiable with a Type term or Bool. - For example, assume the constraint ctx |- max(?m1, Type 1) == ?m2. Now, suppose - ?m2 is assigned to Type 1. Then, ?m1 can be assigned to Type 0 - or Type 1. - - \remark The max constraint is produced when type checking Pi expressions of the form (Pi x : A, B), - and the type of A is t1 and the type of B is t2. So, if t2 == Bool, then max(t1, t2) == Bool -*/ -enum class unification_constraint_kind { Eq, Convertible, Max, Choice }; - -/** - \brief Base class for all Lean unification constraints. -*/ -class unification_constraint_cell { -protected: - unification_constraint_kind m_kind; - context m_ctx; - justification m_justification; //!< justification for this constraint - MK_LEAN_RC(); - void dealloc(); -public: - unification_constraint_cell(unification_constraint_kind k, context const & c, justification const & j); - virtual ~unification_constraint_cell(); - unification_constraint_kind kind() const { return m_kind; } - justification const & get_justification() const { return m_justification; } - context const & get_context() const { return m_ctx; } - virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification, - optional const & menv) const = 0; - void set_justification(justification const & j) { lean_assert(!m_justification); m_justification = j; } - /** \brief Return a new constraint equal to this one, but with the new justification */ - virtual unification_constraint updt_justification(justification const & j) const = 0; -}; - -class unification_constraint_eq; -class unification_constraint_convertible; -class unification_constraint_max; -class unification_constraint_choice; - -class unification_constraint { -private: - unification_constraint_cell * m_ptr; - explicit unification_constraint(unification_constraint_cell * ptr):m_ptr(ptr) {} -public: - unification_constraint(unification_constraint const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); } - unification_constraint(unification_constraint && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } - ~unification_constraint() { if (m_ptr) m_ptr->dec_ref(); } - - friend void swap(unification_constraint & a, unification_constraint & b) { std::swap(a.m_ptr, b.m_ptr); } - - unification_constraint & operator=(unification_constraint const & s) { LEAN_COPY_REF(s); } - unification_constraint & operator=(unification_constraint && s) { LEAN_MOVE_REF(s); } - - unification_constraint_kind kind() const { return m_ptr->kind(); } - - format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification, - optional const & menv) const; - format pp(formatter const & fmt, options const & opts, pos_info_provider const * p = nullptr, bool include_justification = false) const; - justification const & get_justification() const { return m_ptr->get_justification(); } - void set_justification(justification const & j) { lean_assert(!get_justification()); lean_assert(m_ptr); m_ptr->set_justification(j); } - - context const & get_context() const { return m_ptr->get_context(); } - - virtual unification_constraint updt_justification(justification const & j) const { lean_assert(m_ptr); return m_ptr->updt_justification(j); } - - friend unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, justification const & j); - friend unification_constraint mk_convertible_constraint(context const & c, expr const & from, expr const & to, justification const & j); - friend unification_constraint mk_max_constraint(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, justification const & j); - friend unification_constraint mk_choice_constraint(context const & c, expr const & mvar, unsigned num, expr const * choices, justification const & j); - - friend unification_constraint_eq * to_eq(unification_constraint const & c); - friend unification_constraint_convertible * to_convertible(unification_constraint const & c); - friend unification_constraint_max * to_max(unification_constraint const & c); - friend unification_constraint_choice * to_choice(unification_constraint const & c); -}; - -/** - \brief Unification constraint of the form ctx |- lhs == rhs -*/ -class unification_constraint_eq : public unification_constraint_cell { - expr m_lhs; - expr m_rhs; -public: - unification_constraint_eq(context const & c, expr const & lhs, expr const & rhs, justification const & j); - virtual ~unification_constraint_eq(); - expr const & get_lhs() const { return m_lhs; } - expr const & get_rhs() const { return m_rhs; } - virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification, - optional const & menv) const; - virtual unification_constraint updt_justification(justification const & j) const; -}; - -/** - \brief Unification constraint of the form ctx |- from << to. - The meaning is \c from is convertible to \c to. Example: ctx |- Type 1 << Type 2. - It is weaker than ctx |- from == rhs. -*/ -class unification_constraint_convertible : public unification_constraint_cell { - expr m_from; - expr m_to; -public: - unification_constraint_convertible(context const & c, expr const & from, expr const & to, justification const & j); - virtual ~unification_constraint_convertible(); - expr const & get_from() const { return m_from; } - expr const & get_to() const { return m_to; } - virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification, - optional const & menv) const; - virtual unification_constraint updt_justification(justification const & j) const; -}; - -/** - \brief Unification constraint of the form ctx |- max(lhs1, lhs2) == rhs. -*/ -class unification_constraint_max : public unification_constraint_cell { - expr m_lhs1; - expr m_lhs2; - expr m_rhs; -public: - unification_constraint_max(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, justification const & j); - virtual ~unification_constraint_max(); - expr const & get_lhs1() const { return m_lhs1; } - expr const & get_lhs2() const { return m_lhs2; } - expr const & get_rhs() const { return m_rhs; } - virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification, - optional const & menv) const; - virtual unification_constraint updt_justification(justification const & j) const; -}; - -/** - \brief Unification constraint of the form ctx |- mvar == choices[0] OR ... OR mvar == choices[size-1]. -*/ -class unification_constraint_choice : public unification_constraint_cell { - expr m_mvar; - std::vector m_choices; -public: - unification_constraint_choice(context const & c, expr const & mvar, unsigned num, expr const * choices, justification const & j); - virtual ~unification_constraint_choice(); - expr const & get_mvar() const { return m_mvar; } - unsigned get_num_choices() const { return m_choices.size(); } - expr const & get_choice(unsigned idx) const { return m_choices[idx]; } - std::vector::const_iterator begin_choices() const { return m_choices.begin(); } - std::vector::const_iterator end_choices() const { return m_choices.end(); } - virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool include_justification, - optional const & menv) const; - virtual unification_constraint updt_justification(justification const & j) const; -}; - -unification_constraint mk_eq_constraint(context const & c, expr const & lhs, expr const & rhs, justification const & j); -unification_constraint mk_convertible_constraint(context const & c, expr const & from, expr const & to, justification const & j); -unification_constraint mk_max_constraint(context const & c, expr const & lhs1, expr const & lhs2, expr const & rhs, justification const & j); -unification_constraint mk_choice_constraint(context const & c, expr const & mvar, unsigned num, expr const * choices, justification const & j); -unification_constraint mk_choice_constraint(context const & c, expr const & mvar, std::initializer_list const & choices, justification const & j); - -inline bool is_eq(unification_constraint const & c) { return c.kind() == unification_constraint_kind::Eq; } -inline bool is_convertible(unification_constraint const & c) { return c.kind() == unification_constraint_kind::Convertible; } -inline bool is_max(unification_constraint const & c) { return c.kind() == unification_constraint_kind::Max; } -inline bool is_choice(unification_constraint const & c) { return c.kind() == unification_constraint_kind::Choice; } - -inline unification_constraint_eq * to_eq(unification_constraint const & c) { - lean_assert(is_eq(c)); return static_cast(c.m_ptr); -} - -inline unification_constraint_convertible * to_convertible(unification_constraint const & c) { - lean_assert(is_convertible(c)); return static_cast(c.m_ptr); -} - -inline unification_constraint_max * to_max(unification_constraint const & c) { - lean_assert(is_max(c)); return static_cast(c.m_ptr); -} - -inline unification_constraint_choice * to_choice(unification_constraint const & c) { - lean_assert(is_choice(c)); return static_cast(c.m_ptr); -} - -inline context const & get_context(unification_constraint const & c) { return c.get_context(); } -inline justification const & get_justification(unification_constraint const & c) { return c.get_justification(); } -inline expr const & eq_lhs(unification_constraint const & c) { return to_eq(c)->get_lhs(); } -inline expr const & eq_rhs(unification_constraint const & c) { return to_eq(c)->get_rhs(); } -inline expr const & convertible_from(unification_constraint const & c) { return to_convertible(c)->get_from(); } -inline expr const & convertible_to(unification_constraint const & c) { return to_convertible(c)->get_to(); } -inline expr const & max_lhs1(unification_constraint const & c) { return to_max(c)->get_lhs1(); } -inline expr const & max_lhs2(unification_constraint const & c) { return to_max(c)->get_lhs2(); } -inline expr const & max_rhs(unification_constraint const & c) { return to_max(c)->get_rhs(); } -inline expr const & choice_mvar(unification_constraint const & c) { return to_choice(c)->get_mvar(); } -inline unsigned choice_size(unification_constraint const & c) { return to_choice(c)->get_num_choices(); } -inline expr const & choice_ith(unification_constraint const & c, unsigned i) { return to_choice(c)->get_choice(i); } -}