diff --git a/src/kernel/type_checker_justification.cpp b/src/kernel/type_checker_justification.cpp deleted file mode 100644 index 571fc2e80..000000000 --- a/src/kernel/type_checker_justification.cpp +++ /dev/null @@ -1,138 +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/type_checker_justification.h" -#include "kernel/metavar.h" - -namespace lean { -abstraction_expected_justification_cell::~abstraction_expected_justification_cell() { -} - -format abstraction_expected_justification_cell::pp_header(formatter const & fmt, options const & opts, optional const & menv) const { - unsigned indent = get_pp_indent(opts); - format expr_fmt = fmt(instantiate_metavars(menv, m_ctx), instantiate_metavars(menv, m_expr), false, opts); - format r; - r += format(get_abst_str()); - r += format(" expected at"); - r += nest(indent, compose(line(), expr_fmt)); - return r; -} - -void abstraction_expected_justification_cell::get_children(buffer &) const { -} - -optional abstraction_expected_justification_cell::get_main_expr() const { - return some_expr(m_expr); -} - -char const * function_expected_justification_cell::get_abst_str() const { return "Function"; } - -char const * pair_expected_justification_cell::get_abst_str() const { return "Pair"; } - -app_type_match_justification_cell::~app_type_match_justification_cell() { -} - -format app_type_match_justification_cell::pp_header(formatter const & fmt, options const & opts, optional const & menv) const { - unsigned indent = get_pp_indent(opts); - format r; - r += format("Type of argument "); - r += format(m_i); - r += format(" must be convertible to the expected type in the application of"); - expr new_app = instantiate_metavars(menv, m_app); - r += nest(indent, compose(line(), fmt(instantiate_metavars(menv, m_ctx), arg(new_app, 0), false, opts))); - unsigned num = num_args(m_app); - r += line(); - if (num == 2) - r += format("with argument:"); - else - r += format("with arguments:"); - for (unsigned i = 1; i < num; i++) - r += nest(indent, compose(line(), fmt(m_ctx, arg(new_app, i), false, opts))); - return r; -} - -void app_type_match_justification_cell::get_children(buffer &) const { -} - -optional app_type_match_justification_cell::get_main_expr() const { - return some_expr(m_app); -} - -pair_type_match_justification_cell::~pair_type_match_justification_cell() { -} - -format pair_type_match_justification_cell::pp_header(formatter const & fmt, options const & opts, optional const & menv) const { - unsigned indent = get_pp_indent(opts); - format r; - r += format("Type of "); - if (m_first) - r += format("1st"); - else - r += format("2nd"); - r += format(" component must be convertible to the expected type in the pair"); - expr new_expr = instantiate_metavars(menv, m_expr); - r += nest(indent, compose(line(), fmt(instantiate_metavars(menv, m_ctx), new_expr, false, opts))); - return r; -} - -void pair_type_match_justification_cell::get_children(buffer &) const { -} - -optional pair_type_match_justification_cell::get_main_expr() const { - return some_expr(m_expr); -} - -type_expected_justification_cell::~type_expected_justification_cell() { -} - -format type_expected_justification_cell::pp_header(formatter const & fmt, options const & opts, optional const & menv) const { - unsigned indent = get_pp_indent(opts); - format expr_fmt = fmt(instantiate_metavars(menv, m_ctx), instantiate_metavars(menv, m_type), false, opts); - format r; - r += format("Type expected at"); - r += nest(indent, compose(line(), expr_fmt)); - return r; -} - -void type_expected_justification_cell::get_children(buffer &) const { -} - -optional type_expected_justification_cell::get_main_expr() const { - return some_expr(m_type); -} - -def_type_match_justification_cell::~def_type_match_justification_cell() { -} - -format def_type_match_justification_cell::pp_header(formatter const &, options const &, optional const &) const { - format r; - r += format("Type of definition '"); - r += format(get_name()); - r += format("' must be convertible to expected type."); - return r; -} - -void def_type_match_justification_cell::get_children(buffer &) const { -} - -optional def_type_match_justification_cell::get_main_expr() const { - return some_expr(m_value); -} - -type_match_justification_cell::~type_match_justification_cell() { -} - -format type_match_justification_cell::pp_header(formatter const &, options const &, optional const &) const { - return format("Type of expression must be convertible to expected type."); -} - -void type_match_justification_cell::get_children(buffer &) const { -} - -optional type_match_justification_cell::get_main_expr() const { - return some_expr(m_value); -} -} diff --git a/src/kernel/type_checker_justification.h b/src/kernel/type_checker_justification.h deleted file mode 100644 index 3cac654a6..000000000 --- a/src/kernel/type_checker_justification.h +++ /dev/null @@ -1,196 +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 "kernel/justification.h" -#include "kernel/expr.h" -#include "kernel/context.h" - -namespace lean { -class metavar_env; -/** - \brief Justification produced by the type checker when processing applications and pairs. - Suppose \c m_expr is an application (f ...), the type \c T of \c f contains metavariables, and - it is not clear whether it is a Pi or not. In this case, the type checker adds - the constraint - - ctx |- T == Pi (x : ?A), ?B - - where, \c ?A and \c ?B are fresh metavariables. - This justification cell is used to justify the new constraint. - - Similarly, suppose \c m_expr is a projection (proj_i t), and it is not clear whether - type of \c t is a Sigma type because it contains metavariables. In this case, the type checker - adds the constraints - - ctx |- T == Sigma (x : ?A), ?B -*/ -class abstraction_expected_justification_cell : public justification_cell { - context m_ctx; - expr m_expr; - virtual char const * get_abst_str() const = 0; -public: - abstraction_expected_justification_cell(context const & c, expr const & e):m_ctx(c), m_expr(e) {} - virtual ~abstraction_expected_justification_cell(); - virtual format pp_header(formatter const & fmt, options const & opts, optional const & menv) const; - virtual void get_children(buffer &) const; - virtual optional get_main_expr() const; - context const & get_context() const { return m_ctx; } - expr const & get_expr() const { return m_expr; } -}; - -class function_expected_justification_cell : public abstraction_expected_justification_cell { - virtual char const * get_abst_str() const; -public: - function_expected_justification_cell(context const & c, expr const & e):abstraction_expected_justification_cell(c, e) {} -}; - -class pair_expected_justification_cell : public abstraction_expected_justification_cell { - virtual char const * get_abst_str() const; -public: - pair_expected_justification_cell(context const & c, expr const & e):abstraction_expected_justification_cell(c, e) {} -}; - -/** - \brief Justification produced by the type checker for application argument type matching. - When checking an application (f a_1 ... a_i ...), the type - inferred for \c a_i must be convertible to the expected type. - If the expected or inferred type contain metavariables, and it is not clear whether - the inferred is convertible to expected, then the type checker adds the constraint - - ctx |- inferred << expected - - This justification cell is used to justify this constraint. -*/ -class app_type_match_justification_cell : public justification_cell { - context m_ctx; - expr m_app; - unsigned m_i; -public: - app_type_match_justification_cell(context const & c, expr const & a, unsigned i):m_ctx(c), m_app(a), m_i(i) {} - virtual ~app_type_match_justification_cell(); - virtual format pp_header(formatter const & fmt, options const & opts, optional const & menv) const; - virtual void get_children(buffer &) const; - virtual optional get_main_expr() const; - context const & get_context() const { return m_ctx; } - expr const & get_app() const { return m_app; } - unsigned get_arg_pos() const { return m_i; } -}; - -/** - \brief Justification produced by the type checker for pairs. - When checking a pair (pair f s t), the type - inferred for \c f (\c s) must be convertible to the expected type in the sigma type \c t. - If the expected or inferred type contain metavariables, and it is not clear whether - the inferred is convertible to expected, then the type checker adds the constraint - - ctx |- inferred << expected - - This justification cell is used to justify this constraint. -*/ -class pair_type_match_justification_cell : public justification_cell { - context m_ctx; - expr m_expr; - bool m_first; // first/second component -public: - pair_type_match_justification_cell(context const & c, expr const & a, bool f):m_ctx(c), m_expr(a), m_first(f) {} - virtual ~pair_type_match_justification_cell(); - virtual format pp_header(formatter const & fmt, options const & opts, optional const & menv) const; - virtual void get_children(buffer &) const; - virtual optional get_main_expr() const; - context const & get_context() const { return m_ctx; } - expr const & get_expr() const { return m_expr; } - bool first() const { return m_first; } -}; - -/** - \brief Justification produced by the type checker when the type \c T of \c type must be of the form - Type l, and \c T constains metavariables, and it is not of this form. - The type checker adds the following constraint - - ctx |- T << Type U+1 - - This justification cell is used to justify these constraints. -*/ -class type_expected_justification_cell : public justification_cell { - context m_ctx; - expr m_type; -public: - type_expected_justification_cell(context const & c, expr const & t):m_ctx(c), m_type(t) {} - virtual ~type_expected_justification_cell(); - virtual format pp_header(formatter const & fmt, options const & opts, optional const & menv) const; - virtual void get_children(buffer &) const; - virtual optional get_main_expr() const; - context const & get_context() const { return m_ctx; } - expr const & get_type() const { return m_type; } -}; - -/** - \brief If \c type is of the form Pi x : A, B, where \c A has type \c T1 and \c B has type \c T2, - and \c T1 or \c T2 have metavariables, then the type checker adds the following constraint - - ctx |- max(T1, T2) == ?T - - where ?T is a new metavariable, and this justification cell is used to justify the new constraint. -*/ -class max_type_justification_cell : public type_expected_justification_cell { -public: - max_type_justification_cell(context const & c, expr const & t):type_expected_justification_cell(c, t) {} -}; - -/** - \brief Justification produced by the type checker when checking whether the type \c T_inferred of \c value - is convertible to the expected type \c T_expected. If \c T_expected or \c T_inferred contain - metavariables, and it is not clear whether \c T_inferred is convertible to \c T_expected, - then the type checker adds the constraint - - ctx |- T_inferred << T_expected - - This justification cell is used to justify this constraint. -*/ -class def_type_match_justification_cell : public justification_cell { - context m_ctx; - name m_name; - expr m_value; -public: - def_type_match_justification_cell(context const & c, name const & n, expr const & v):m_ctx(c), m_name(n), m_value(v) {} - virtual ~def_type_match_justification_cell(); - virtual format pp_header(formatter const & fmt, options const & opts, optional const & menv) const; - virtual void get_children(buffer &) const; - virtual optional get_main_expr() const; - context const & get_context() const { return m_ctx; } - name const & get_name() const { return m_name; } - expr const & get_value() const { return m_value; } -}; - -/** - \brief Similar to def_type_match_justification_cell. It is used to sign that type of \c m_value - must be convertible to \c m_type at context \c m_ctx. -*/ -class type_match_justification_cell : public justification_cell { - context m_ctx; - expr m_type; - expr m_value; -public: - type_match_justification_cell(context const & c, expr const & t, expr const & v):m_ctx(c), m_type(t), m_value(v) {} - virtual ~type_match_justification_cell(); - virtual format pp_header(formatter const & fmt, options const & opts, optional const & menv) const; - virtual void get_children(buffer &) const; - virtual optional get_main_expr() const; - context const & get_context() const { return m_ctx; } - expr const & get_type() const { return m_type; } - expr const & get_value() const { return m_value; } -}; - -inline justification mk_function_expected_justification(context const & ctx, expr const & app) { return justification(new function_expected_justification_cell(ctx, app)); } -inline justification mk_pair_expected_justification(context const & ctx, expr const & app) { return justification(new pair_expected_justification_cell(ctx, app)); } -inline justification mk_app_type_match_justification(context const & ctx, expr const & app, unsigned i) { return justification(new app_type_match_justification_cell(ctx, app, i)); } -inline justification mk_pair_type_match_justification(context const & ctx, expr const & e, bool first) { return justification(new pair_type_match_justification_cell(ctx, e, first)); } -inline justification mk_type_expected_justification(context const & ctx, expr const & type) { return justification(new type_expected_justification_cell(ctx, type)); } -inline justification mk_max_type_justification(context const & ctx, expr const & type) { return justification(new max_type_justification_cell(ctx, type)); } -inline justification mk_def_type_match_justification(context const & ctx, name const & n, expr const & v) { return justification(new def_type_match_justification_cell(ctx, n, v)); } -inline justification mk_type_match_justification(context const & ctx, expr const & t, expr const & v) { return justification(new type_match_justification_cell(ctx, t, v)); } -}