From 4543dc4a7fb1905bf95fb8880b661760e5f1a292 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 5 Mar 2016 12:53:45 -0800 Subject: [PATCH] feat(library): add metavar_context --- src/library/CMakeLists.txt | 2 +- src/library/init_module.cpp | 6 + src/library/metavar_context.cpp | 232 ++++++++++++++++++++++++++++++++ src/library/metavar_context.h | 59 ++++++++ 4 files changed, 298 insertions(+), 1 deletion(-) create mode 100644 src/library/metavar_context.cpp create mode 100644 src/library/metavar_context.h diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index a6d00fc052..8855dcf13b 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -19,5 +19,5 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp tmp_type_context.cpp fun_info_manager.cpp congr_lemma_manager.cpp abstract_expr_manager.cpp light_lt_manager.cpp trace.cpp attribute_manager.cpp error_handling.cpp unification_hint.cpp defeq_simp_lemmas.cpp - defeq_simplifier.cpp proof_irrel_expr_manager.cpp local_context.cpp + defeq_simplifier.cpp proof_irrel_expr_manager.cpp local_context.cpp metavar_context.cpp legacy_type_context.cpp) diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index 2f37a345d4..67c674058b 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -44,6 +44,8 @@ Author: Leonardo de Moura #include "library/class_instance_resolution.h" #include "library/old_type_context.h" #include "library/legacy_type_context.h" +#include "library/local_context.h" +#include "library/metavar_context.h" #include "library/congr_lemma_manager.h" #include "library/app_builder.h" #include "library/attribute_manager.h" @@ -54,6 +56,8 @@ Author: Leonardo de Moura namespace lean { void initialize_library_module() { + initialize_local_context(); + initialize_metavar_context(); initialize_attribute_manager(); initialize_trace(); initialize_constants(); @@ -151,5 +155,7 @@ void finalize_library_module() { finalize_constants(); finalize_trace(); finalize_attribute_manager(); + finalize_metavar_context(); + finalize_local_context(); } } diff --git a/src/library/metavar_context.cpp b/src/library/metavar_context.cpp new file mode 100644 index 0000000000..5b7182faaa --- /dev/null +++ b/src/library/metavar_context.cpp @@ -0,0 +1,232 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "util/fresh_name.h" +#include "kernel/for_each_fn.h" +#include "kernel/instantiate.h" +#include "library/replace_visitor.h" +#include "library/metavar_context.h" + +namespace lean { +static name * g_meta_prefix; +static expr * g_dummy_type; + +name mk_meta_decl_name() { + return mk_tagged_fresh_name(*g_meta_prefix); +} + +expr mk_meta_ref(name const & n) { + return mk_metavar(n, *g_dummy_type); +} + +bool is_univ_metavar_decl_ref(level const & u) { + return is_meta(u) && is_tagged_by(meta_id(u), *g_meta_prefix); +} + +bool is_metavar_decl_ref(expr const & e) { + return is_metavar(e) && mlocal_type(e) == *g_dummy_type; +} + +level metavar_context::mk_univ_metavar_decl() { + return mk_meta_univ(mk_meta_decl_name()); +} + +expr metavar_context::mk_metavar_decl(local_context const & ctx, expr const & type) { + name n = mk_meta_decl_name(); + m_decls.insert(n, metavar_decl(ctx.to_local_decls(), type)); + return mk_meta_ref(n); +} + +optional metavar_context::get_metavar_decl(expr const & e) const { + lean_assert(is_metavar_decl_ref(e)); + if (auto r = m_decls.find(mlocal_name(e))) + return optional(*r); + else + return optional(); +} + +void metavar_context::assign(level const & u, level const & l) { + lean_assert(!is_assigned(u)); + m_uassignment.insert(meta_id(u), l); +} + +void metavar_context::assign(expr const & e, expr const & v) { + lean_assert(!is_assigned(e)); + m_eassignment.insert(mlocal_name(e), v); +} + +bool metavar_context::has_assigned(level const & l) const { + if (!has_meta(l)) + return false; + bool found = false; + for_each(l, [&](level const & l) { + if (!has_meta(l)) + return false; // stop search + if (found) + return false; // stop search + if (is_univ_metavar_decl_ref(l) && is_assigned(l)) { + found = true; + return false; // stop search + } + return true; // continue search + }); + return found; +} + +bool metavar_context::has_assigned(levels const & ls) const { + for (level const & l : ls) { + if (has_assigned(l)) + return true; + } + return false; +} + +bool metavar_context::has_assigned(expr const & e) const { + if (!has_expr_metavar(e) && !has_univ_metavar(e)) + return false; + bool found = false; + for_each(e, [&](expr const & e, unsigned) { + if (!has_expr_metavar(e) && !has_univ_metavar(e)) + return false; // stop search + if (found) + return false; // stop search + if ((is_metavar_decl_ref(e) && is_assigned(e)) || + (is_constant(e) && has_assigned(const_levels(e))) || + (is_sort(e) && has_assigned(sort_level(e)))) { + found = true; + return false; // stop search + } + return true; // continue search + }); + return found; +} + +level metavar_context::instantiate(level const & l) { + if (!has_assigned(l)) + return l; + return replace(l, [&](level const & l) { + if (!has_meta(l)) { + return some_level(l); + } else if (is_univ_metavar_decl_ref(l)) { + if (auto v1 = m_uassignment.find(meta_id(l))) { + level v2 = instantiate(*v1); + if (*v1 != v2) { + m_uassignment.insert(meta_id(l), v2); + return some_level(v2); + } else { + return some_level(*v1); + } + } + } + return none_level(); + }); +} + +struct instantiate_fn : public replace_visitor { + metavar_context & m_owner; + + level visit_level(level const & l) { + return m_owner.instantiate(l); + } + + levels visit_levels(levels const & ls) { + return map_reuse(ls, + [&](level const & l) { return visit_level(l); }, + [](level const & l1, level const & l2) { return is_eqp(l1, l2); }); + } + + virtual expr visit_sort(expr const & s) override { + return update_sort(s, visit_level(sort_level(s))); + } + + virtual expr visit_constant(expr const & c) override { + return update_constant(c, visit_levels(const_levels(c))); + } + + virtual expr visit_local(expr const & e) override { + return update_mlocal(e, visit(mlocal_type(e))); + } + + virtual expr visit_meta(expr const & m) override { + if (is_metavar_decl_ref(m)) { + if (auto v1 = m_owner.m_eassignment.find(mlocal_name(m))) { + if (!has_expr_metavar(*v1)) { + return *v1; + } else { + expr v2 = m_owner.instantiate(*v1); + if (v2 != *v1) + m_owner.m_eassignment.insert(mlocal_name(m), v2); + return v2; + } + } else { + return m; + } + } else { + return m; + } + } + + virtual expr visit_app(expr const & e) override { + buffer args; + expr const & f = get_app_rev_args(e, args); + if (is_metavar_decl_ref(f)) { + if (auto v = m_owner.m_eassignment.find(mlocal_name(f))) { + expr new_app = apply_beta(*v, args.size(), args.data()); + if (has_expr_metavar(new_app)) + return visit(new_app); + else + return new_app; + } + } + expr new_f = visit(f); + buffer new_args; + bool modified = !is_eqp(new_f, f); + for (expr const & arg : args) { + expr new_arg = visit(arg); + if (!is_eqp(arg, new_arg)) + modified = true; + new_args.push_back(new_arg); + } + if (!modified) + return e; + else + return mk_rev_app(new_f, new_args, e.get_tag()); + } + + virtual expr visit_macro(expr const & e) override { + lean_assert(is_macro(e)); + buffer new_args; + for (unsigned i = 0; i < macro_num_args(e); i++) + new_args.push_back(visit(macro_arg(e, i))); + return update_macro(e, new_args.size(), new_args.data()); + } + + virtual expr visit(expr const & e) override { + if (!has_expr_metavar(e) && !has_univ_metavar(e)) + return e; + else + return replace_visitor::visit(e); + } + +public: + instantiate_fn(metavar_context & o):m_owner(o) {} + expr operator()(expr const & e) { return visit(e); } +}; + +expr metavar_context::instantiate(expr const & e) { + return e; +} + +void initialize_metavar_context() { + g_meta_prefix = new name(name::mk_internal_unique_name()); + g_dummy_type = new expr(mk_constant(name::mk_internal_unique_name())); +} + +void finalize_metavar_context() { + delete g_meta_prefix; + delete g_dummy_type; +} +} diff --git a/src/library/metavar_context.h b/src/library/metavar_context.h new file mode 100644 index 0000000000..1febb003c7 --- /dev/null +++ b/src/library/metavar_context.h @@ -0,0 +1,59 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "library/local_context.h" + +namespace lean { +class metavar_decl { + local_decls m_context; + expr m_type; + friend class metavar_context; + metavar_decl(local_decls const & ctx, expr const & type):m_context(ctx), m_type(type) {} +public: + metavar_decl() {} + expr const & get_type() const { return m_type; } + local_decls const & get_context() const { return m_context; } +}; + +bool is_univ_metavar_decl_ref(level const & l); +bool is_metavar_decl_ref(expr const & e); + +class metavar_context { + name_map m_decls; + name_map m_uassignment; + name_map m_eassignment; + friend struct instantiate_fn; +public: + level mk_univ_metavar_decl(); + expr mk_metavar_decl(local_context const & ctx, expr const & type); + + optional get_metavar_decl(expr const & e) const; + + bool is_assigned(level const & l) const { + lean_assert(is_univ_metavar_decl_ref(l)); + return m_uassignment.contains(meta_id(l)); + } + + bool is_assigned(expr const & m) const { + lean_assert(is_metavar_decl_ref(m)); + return m_eassignment.contains(mlocal_name(m)); + } + + void assign(level const & u, level const & l); + void assign(expr const & e, expr const & v); + + level instantiate(level const & l); + expr instantiate(expr const & e); + + bool has_assigned(level const & l) const; + bool has_assigned(levels const & ls) const; + bool has_assigned(expr const & e) const; +}; + +void initialize_metavar_context(); +void finalize_metavar_context(); +}