From fc288929a2e6229f38286ca2dfa8ea8202aa693d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 1 Oct 2013 10:25:18 -0700 Subject: [PATCH] feat(type_checker): add trace objects to justify constraints created by the type checker Signed-off-by: Leonardo de Moura --- src/kernel/CMakeLists.txt | 2 +- src/kernel/trace.h | 18 ++--- src/kernel/type_checker_trace.cpp | 87 ++++++++++++++++++++ src/kernel/type_checker_trace.h | 128 ++++++++++++++++++++++++++++++ 4 files changed, 224 insertions(+), 11 deletions(-) create mode 100644 src/kernel/type_checker_trace.cpp create mode 100644 src/kernel/type_checker_trace.h diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index 9946262dd..36ca3fc83 100644 --- a/src/kernel/CMakeLists.txt +++ b/src/kernel/CMakeLists.txt @@ -2,6 +2,6 @@ add_library(kernel expr.cpp free_vars.cpp abstract.cpp instantiate.cpp normalizer.cpp context.cpp level.cpp object.cpp environment.cpp type_checker.cpp builtin.cpp occurs.cpp metavar.cpp trace.cpp unification_constraint.cpp printer.cpp formatter.cpp - kernel_exception.cpp) + kernel_exception.cpp type_checker_trace.cpp) target_link_libraries(kernel ${LEAN_LIBS}) diff --git a/src/kernel/trace.h b/src/kernel/trace.h index d4e072c93..babaf3c7c 100644 --- a/src/kernel/trace.h +++ b/src/kernel/trace.h @@ -10,6 +10,8 @@ Author: Leonardo de Moura #include "util/rc.h" #include "util/buffer.h" #include "util/sexpr/format.h" +#include "kernel/expr.h" +#include "kernel/formatter.h" namespace lean { class trace; @@ -23,9 +25,11 @@ class trace_cell { MK_LEAN_RC(); void dealloc() { delete this; } public: + trace_cell():m_rc(0) {} virtual ~trace_cell() {} - virtual format pp() const = 0; + virtual format pp(formatter const & fmt, options const & opts) const = 0; virtual void get_children(buffer & r) const = 0; + virtual expr const & get_main_expr() const { return expr::null(); } }; /** @@ -33,9 +37,9 @@ public: */ class trace { trace_cell * m_ptr; - explicit trace(trace_cell * ptr):m_ptr(ptr) {} public: trace():m_ptr(nullptr) {} + trace(trace_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); } trace(trace const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); } trace(trace && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } ~trace() { if (m_ptr) m_ptr->dec_ref(); } @@ -48,15 +52,9 @@ public: trace & operator=(trace const & s) { LEAN_COPY_REF(trace, s); } trace & operator=(trace && s) { LEAN_MOVE_REF(trace, s); } - format pp() const { lean_assert(m_ptr); return m_ptr->pp(); } + format pp(formatter const & fmt, options const & opts) const { lean_assert(m_ptr); return m_ptr->pp(fmt, opts); } + expr const & get_main_expr() const { return m_ptr ? m_ptr->get_main_expr() : expr::null(); } void get_children(buffer & r) const { if (m_ptr) m_ptr->get_children(r); } bool has_children() const; }; - -inline unsigned get_rc(trace const & t) { return t.raw()->get_rc(); } -inline bool is_shared(trace const & t) { return get_rc(t) > 1; } -inline format pp(trace const & t) { return t.pp(); } -inline void get_children(trace const & t, buffer & r) { - return t.get_children(r); -} } diff --git a/src/kernel/type_checker_trace.cpp b/src/kernel/type_checker_trace.cpp new file mode 100644 index 000000000..113b12d44 --- /dev/null +++ b/src/kernel/type_checker_trace.cpp @@ -0,0 +1,87 @@ +/* +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_trace.h" + +namespace lean { + +function_expected_trace_cell::~function_expected_trace_cell() { +} + +format function_expected_trace_cell::pp(formatter const & fmt, options const & opts) const { + unsigned indent = get_pp_indent(opts); + format expr_fmt = fmt(m_ctx, m_app, false, opts); + format r; + r += format("function expected at"); + r += nest(indent, compose(line(), expr_fmt)); + return r; +} + +void function_expected_trace_cell::get_children(buffer &) const { +} + +expr const & function_expected_trace_cell::get_main_expr() const { + return m_app; +} + +app_type_match_trace_cell::~app_type_match_trace_cell() { +} + +format app_type_match_trace_cell::pp(formatter const & fmt, options const & opts) const { + unsigned indent = get_pp_indent(opts); + format app_fmt = fmt(m_ctx, m_app, false, opts); + format r; + r += format("type of argument "); + r += format(m_i); + r += format(" of application"); + r += nest(indent, compose(line(), app_fmt)); + return r; +} + +void app_type_match_trace_cell::get_children(buffer &) const { +} + +expr const & app_type_match_trace_cell::get_main_expr() const { + return m_app; +} + +type_expected_trace_cell::~type_expected_trace_cell() { +} + +format type_expected_trace_cell::pp(formatter const & fmt, options const & opts) const { + unsigned indent = get_pp_indent(opts); + format expr_fmt = fmt(m_ctx, m_type, false, opts); + format r; + r += format("type expected at"); + r += nest(indent, compose(line(), expr_fmt)); + return r; +} + +void type_expected_trace_cell::get_children(buffer &) const { +} + +expr const & type_expected_trace_cell::get_main_expr() const { + return m_type; +} + +def_type_match_trace_cell::~def_type_match_trace_cell() { +} + +format def_type_match_trace_cell::pp(formatter const &, options const &) const { + format r; + r += format("type of definition of '"); + r += format(get_name()); + r += format("'"); + return r; +} + +void def_type_match_trace_cell::get_children(buffer &) const { +} + +expr const & def_type_match_trace_cell::get_main_expr() const { + return m_value; +} +} diff --git a/src/kernel/type_checker_trace.h b/src/kernel/type_checker_trace.h new file mode 100644 index 000000000..4e5370a5f --- /dev/null +++ b/src/kernel/type_checker_trace.h @@ -0,0 +1,128 @@ +/* +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/trace.h" +#include "kernel/expr.h" +#include "kernel/context.h" + +namespace lean { +/** + \brief Trace produced by the type checker when the application \c m_app + 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 x + + where, \c ?A and \c ?B are fresh metavariables. + This trace cell is used to justify/trace the new constraint. +*/ +class function_expected_trace_cell : public trace_cell { + context m_ctx; + expr m_app; +public: + function_expected_trace_cell(context const & c, expr const & app):m_ctx(c), m_app(app) {} + virtual ~function_expected_trace_cell(); + virtual format pp(formatter const & fmt, options const & opts) const; + virtual void get_children(buffer &) const; + virtual expr const & get_main_expr() const; + context const & get_context() const { return m_ctx; } + expr const & get_app() const { return m_app; } +}; + +/** + \brief Trace produced by the type checker for application argument type matching. + When checking an application (f a_1 ... a_i ...), the type + \c T_inferred of \c a_i must be 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 trace cell is used to justify this constraint. +*/ +class app_type_match_trace_cell : public trace_cell { + context m_ctx; + expr m_app; + unsigned m_i; +public: + app_type_match_trace_cell(context const & c, expr const & a, unsigned i):m_ctx(c), m_app(a), m_i(i) {} + virtual ~app_type_match_trace_cell(); + virtual format pp(formatter const & fmt, options const & opts) const; + virtual void get_children(buffer &) const; + virtual expr const & 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 Trace 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 + + This trace cell is used to justify these constraints. +*/ +class type_expected_trace_cell : public trace_cell { + context m_ctx; + expr m_type; +public: + type_expected_trace_cell(context const & c, expr const & t):m_ctx(c), m_type(t) {} + virtual ~type_expected_trace_cell(); + virtual format pp(formatter const & fmt, options const & opts) const; + virtual void get_children(buffer &) const; + virtual expr const & 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 trace cell is used to justify the new constraint. +*/ +class max_type_trace_cell : public type_expected_trace_cell { +public: + max_type_trace_cell(context const & c, expr const & t):type_expected_trace_cell(c, t) {} +}; + +/** + \brief Trace 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 trace cell is used to justify this constraint. +*/ +class def_type_match_trace_cell : public trace_cell { + context m_ctx; + name m_name; + expr m_value; +public: + def_type_match_trace_cell(context const & c, name const & n, expr const & v):m_ctx(c), m_name(n), m_value(v) {} + virtual ~def_type_match_trace_cell(); + virtual format pp(formatter const & fmt, options const & opts) const; + virtual void get_children(buffer &) const; + virtual expr const & 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; } +}; + +inline trace mk_function_expected_trace(context const & ctx, expr const & app) { return trace(new function_expected_trace_cell(ctx, app)); } +inline trace mk_app_type_match_trace(context const & ctx, expr const & app, unsigned i) { return trace(new app_type_match_trace_cell(ctx, app, i)); } +inline trace mk_type_expected_trace(context const & ctx, expr const & type) { return trace(new type_expected_trace_cell(ctx, type)); } +inline trace mk_max_type_trace(context const & ctx, expr const & type) { return trace(new max_type_trace_cell(ctx, type)); } +inline trace mk_def_type_match_trace(context const & ctx, name const & n, expr const & v) { return trace(new def_type_match_trace_cell(ctx, n, v)); } +}