diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index d972aeca8b..b12c8f000e 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -1,3 +1,3 @@ add_library(library basic_thms.cpp deep_copy.cpp max_sharing.cpp toplevel.cpp printer.cpp - formatter.cpp context_to_lambda.cpp state.cpp beta.cpp metavar_env.cpp) + formatter.cpp context_to_lambda.cpp state.cpp beta.cpp metavar_env.cpp elaborator.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/library/elaborator.cpp b/src/library/elaborator.cpp new file mode 100644 index 0000000000..5f8afd5650 --- /dev/null +++ b/src/library/elaborator.cpp @@ -0,0 +1,146 @@ +/* +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 "elaborator.h" +#include "free_vars.h" +#include "beta.h" +#include "instantiate.h" +#include "builtin.h" +#include "exception.h" + +namespace lean { + +expr elaborator::lookup(context const & c, unsigned i) { + auto p = lookup_ext(c, i); + context_entry const & def = p.first; + context const & def_c = p.second; + lean_assert(length(c) > length(def_c)); + return lift_free_vars(def.get_domain(), length(c) - length(def_c)); +} + +elaborator::elaborator(environment & env): + m_env(env), m_metaenv(env) { +} + +void elaborator::unify(expr const & e1, expr const & e2, context const & ctx) { + if (has_metavar(e1) || has_metavar(e2)) { + // std::cout << "UNIFY: " << e1 << " <--> " << e2 << "\n"; + m_metaenv.unify(e1, e2, ctx); + } +} + +expr elaborator::check_pi(expr const & e, context const & ctx) { + if (!e) { + // e is the type of a metavariable. + // approx: assume it is Type() + return Type(); + } else if (is_pi(e)) { + return e; + } else { + expr r = head_reduce(e, m_env); + if (!is_eqp(r, e)) { + return check_pi(r, ctx); + } else if (is_var(e)) { + auto p = lookup_ext(ctx, var_idx(e)); + context_entry const & entry = p.first; + context const & entry_ctx = p.second; + if (entry.get_body()) { + return lift_free_vars(check_pi(entry.get_body(), entry_ctx), + length(ctx) - length(entry_ctx)); + } + } + throw exception("function expected"); + } +} + +level elaborator::check_universe(expr const & e, context const & ctx) { + if (!e) { + // e is the type of a metavariable + // approx: assume it is level 0 + return level(); + } else if (is_type(e)) { + return ty_level(e); + } else { + expr r = head_reduce(e, m_env); + if (!is_eqp(r, e)) { + return check_universe(r, ctx); + } else if (is_var(e)) { + auto p = lookup_ext(ctx, var_idx(e)); + context_entry const & entry = p.first; + context const & entry_ctx = p.second; + if (entry.get_body()) { + return check_universe(entry.get_body(), entry_ctx); + } + } + throw exception("type expected"); + } +} + +/** + \brief Given e and a context, try to instantiate the + meta-variables in \c e. Return an inferred type for \c e. +*/ +expr elaborator::process(expr const & e, context const & ctx) { + switch (e.kind()) { + case expr_kind::Constant: + if (is_metavar(e)) { + return expr(); + } else { + return m_env.get_object(const_name(e)).get_type(); + } + case expr_kind::Var: + return lookup(ctx, var_idx(e)); + case expr_kind::Type: + return mk_type(ty_level(e) + 1); + case expr_kind::Value: + return to_value(e).get_type(); + case expr_kind::App: { + buffer types; + unsigned num = num_args(e); + for (unsigned i = 0; i < num; i++) { + types.push_back(process(arg(e,i), ctx)); + } + // TODO: handle overload in args[0] + expr f_t = types[0]; + if (!f_t) { + throw exception("invalid use of placeholder, the function must be provided to an application"); + } + for (unsigned i = 1; i < num; i++) { + f_t = check_pi(f_t, ctx); + if (types[i]) + unify(abst_domain(f_t), types[i], ctx); + f_t = instantiate(abst_body(f_t), arg(e, i)); + } + return f_t; + } + case expr_kind::Eq: { + process(eq_lhs(e), ctx); + process(eq_rhs(e), ctx); + return mk_bool_type(); + } + case expr_kind::Pi: { + expr dt = process(abst_domain(e), ctx); + expr bt = process(abst_body(e), extend(ctx, abst_name(e), abst_domain(e))); + return mk_type(max(check_universe(dt, ctx), check_universe(bt, ctx))); + } + case expr_kind::Lambda: { + expr dt = process(abst_domain(e), ctx); + expr bt = process(abst_body(e), extend(ctx, abst_name(e), abst_domain(e))); + return mk_pi(abst_name(e), abst_domain(e), bt); + } + case expr_kind::Let: { + expr lt = process(let_value(e), ctx); + return process(let_body(e), extend(ctx, let_name(e), lt, let_value(e))); + }} + lean_unreachable(); + return expr(); +} + +expr elaborator::operator()(expr const & e) { + expr t = process(e, context()); + return m_metaenv.instantiate_metavars(e); +} +} diff --git a/src/library/elaborator.h b/src/library/elaborator.h new file mode 100644 index 0000000000..2c84c04ef1 --- /dev/null +++ b/src/library/elaborator.h @@ -0,0 +1,31 @@ +/* +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 "metavar_env.h" + +namespace lean { +/** + \brief Expression elaborator, it is responsible for "filling" holes + in terms left by the user. This is the main module resposible for computing + the value of implicit arguments. +*/ +class elaborator { + environment & m_env; + metavar_env m_metaenv; + + expr lookup(context const & c, unsigned i); + void unify(expr const & e1, expr const & e2, context const & ctx); + expr check_pi(expr const & e, context const & ctx); + level check_universe(expr const & e, context const & ctx); + expr process(expr const & e, context const & ctx); + +public: + elaborator(environment & env); + metavar_env & menv() { return m_metaenv; } + expr operator()(expr const & e); +}; +}