feat(library): add composition manager

This commit is contained in:
Leonardo de Moura 2015-06-17 14:25:02 -07:00
parent 14c33c4e01
commit c59e1f49db
4 changed files with 136 additions and 1 deletions

View file

@ -14,6 +14,6 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
local_context.cpp choice_iterator.cpp pp_options.cpp
unfold_macros.cpp app_builder.cpp projection.cpp abbreviation.cpp
relation_manager.cpp export.cpp user_recursors.cpp
class_instance_synth.cpp idx_metavar.cpp)
class_instance_synth.cpp idx_metavar.cpp composition_manager.cpp)
target_link_libraries(library ${LEAN_LIBS})

View file

@ -0,0 +1,112 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <utility>
#include <string>
#include "util/sstream.h"
#include "kernel/type_checker.h"
#include "kernel/declaration.h"
#include "kernel/instantiate.h"
#include "kernel/abstract.h"
#include "library/util.h"
#include "library/module.h"
namespace lean {
struct composition_manager_ext : public environment_extension {
typedef rb_map<name_pair, name, name_pair_quick_cmp> cache;
cache m_cache;
};
struct composition_manager_ext_reg {
unsigned m_ext_id;
composition_manager_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<composition_manager_ext>()); }
};
static composition_manager_ext_reg * g_ext = nullptr;
static std::string * g_key = nullptr;
static composition_manager_ext const & get_extension(environment const & env) {
return static_cast<composition_manager_ext const &>(env.get_extension(g_ext->m_ext_id));
}
static environment update(environment const & env, composition_manager_ext const & ext) {
return env.update(g_ext->m_ext_id, std::make_shared<composition_manager_ext>(ext));
}
pair<environment, name> compose(type_checker & tc, name const & g, name const & f, optional<name> const & gf) {
environment const & env = tc.env();
composition_manager_ext ext = get_extension(env);
if (name const * it = ext.m_cache.find(mk_pair(g, f)))
return mk_pair(env, *it);
declaration const & f_decl = env.get(f);
levels f_ls = param_names_to_levels(f_decl.get_univ_params());
expr f_type = instantiate_type_univ_params(f_decl, f_ls);
buffer<expr> f_domain;
name_generator ngen = tc.mk_ngen();
expr f_codomain = to_telescope(ngen, f_type, f_domain);
buffer<expr> B_args;
expr const & B = get_app_args(f_codomain, B_args);
if (!is_constant(B))
throw exception(sstream() << "invalid function composition, '" << f << "' codomain must be of the form (B ...), "
"where B is a constant");
expr b = mk_app(mk_constant(f, f_ls), f_domain);
expr new_val = Fun(f_domain, mk_app(mk_app(mk_constant(g, const_levels(B)), B_args), b));
expr new_type;
try {
new_type = tc.infer(new_val).first;
} catch (exception &) {
throw exception(sstream() << "invalid function composition '" << g << "' o '" << f << "'\n");
}
new_type = head_beta_reduce(new_type);
name base_name;
if (gf) {
base_name = *gf;
} else {
base_name = g + f;
}
name new_name = base_name;
unsigned idx = 1;
// make sure name is unique
while (env.find(new_name)) {
new_name = base_name.append_after(idx);
idx++;
}
ext.m_cache.insert(mk_pair(g, f), new_name);
environment new_env = module::add(env, check(env, mk_definition(env, new_name, f_decl.get_univ_params(),
new_type, new_val)));
new_env = module::add(new_env, *g_key, [=](environment const &, serializer & s) { s << g << f << new_name; });
return mk_pair(update(new_env, ext), new_name);
}
pair<environment, name> compose(environment const & env, name const & g, name const & f, optional<name> const & gf) {
type_checker tc(env);
return compose(tc, g, f, gf);
}
static void composition_reader(deserializer & d, shared_environment & senv,
std::function<void(asynch_update_fn const &)> &,
std::function<void(delayed_update_fn const &)> &) {
name g, f, gf;
d >> g >> f >> gf;
senv.update([=](environment const & env) -> environment {
composition_manager_ext ext = get_extension(env);
ext.m_cache.insert(mk_pair(g, f), gf);
return update(env, ext);
});
}
void initialize_composition_manager() {
g_ext = new composition_manager_ext_reg();
g_key = new std::string("comp");
register_module_object_reader(*g_key, composition_reader);
}
void finalize_composition_manager() {
delete g_key;
delete g_ext;
}
}

View file

@ -0,0 +1,20 @@
/*
Copyright (c) 2015 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/type_checker.h"
namespace lean {
/** \brief Define the composition of g and f, if the environment already contains one created using \c compose, returns it.
Otherwise, this procedure defines one and uses name \c gf. If \c gf is none, then use g+f as the name.
If the environment already has a definition with this name, then adds the prefix _idx, where idx is a numeral.
The result is a pair (new environment, new constant name).
*/
pair<environment, name> compose(type_checker & tc, name const & g, name const & f, optional<name> const & gf = optional<name>());
pair<environment, name> compose(environment const & env, name const & g, name const & f, optional<name> const & gf = optional<name>());
void initialize_composition_manager();
void finalize_composition_manager();
}

View file

@ -39,6 +39,7 @@ Author: Leonardo de Moura
#include "library/relation_manager.h"
#include "library/user_recursors.h"
#include "library/class_instance_synth.h"
#include "library/composition_manager.h"
namespace lean {
void initialize_library_module() {
@ -77,9 +78,11 @@ void initialize_library_module() {
initialize_relation_manager();
initialize_user_recursors();
initialize_class_instance_elaborator();
initialize_composition_manager();
}
void finalize_library_module() {
finalize_composition_manager();
finalize_class_instance_elaborator();
finalize_user_recursors();
finalize_relation_manager();