From f948241bb910529658a268229b45bb25b0bdb4da Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 2 Dec 2014 20:23:53 -0800 Subject: [PATCH] feat(library/definitional): add auxiliary functions --- src/init/init.cpp | 3 + src/library/bin_app.h | 15 +++ src/library/definitional/CMakeLists.txt | 2 +- src/library/definitional/init_module.cpp | 17 +++ src/library/definitional/init_module.h | 12 +++ src/library/definitional/util.cpp | 128 +++++++++++++++++++++++ src/library/definitional/util.h | 21 ++++ 7 files changed, 197 insertions(+), 1 deletion(-) create mode 100644 src/library/definitional/init_module.cpp create mode 100644 src/library/definitional/init_module.h diff --git a/src/init/init.cpp b/src/init/init.cpp index 214dc5563..255b438b4 100644 --- a/src/init/init.cpp +++ b/src/init/init.cpp @@ -13,6 +13,7 @@ Author: Leonardo de Moura #include "kernel/inductive/inductive.h" #include "library/init_module.h" #include "library/tactic/init_module.h" +#include "library/definitional/init_module.h" #include "library/print.h" #include "frontends/lean/init_module.h" #include "frontends/lua/register_modules.h" @@ -29,12 +30,14 @@ void initialize() { init_default_print_fn(); initialize_library_module(); initialize_tactic_module(); + initialize_definitional_module(); initialize_frontend_lean_module(); register_modules(); } void finalize() { run_thread_finalizers(); finalize_frontend_lean_module(); + finalize_definitional_module(); finalize_tactic_module(); finalize_library_module(); finalize_inductive_module(); diff --git a/src/library/bin_app.h b/src/library/bin_app.h index 4c1943dbb..ebd23bca4 100644 --- a/src/library/bin_app.h +++ b/src/library/bin_app.h @@ -20,6 +20,21 @@ bool is_bin_app(expr const & t, expr const & f, expr & lhs, expr & rhs); expr mk_bin_rop(expr const & op, expr const & unit, unsigned num_args, expr const * args); expr mk_bin_rop(expr const & op, expr const & unit, std::initializer_list const & l); +template +expr foldr(MkBin && mkb, MkUnit && mku, unsigned num_args, expr const * args) { + if (num_args == 0) { + return mku(); + } else { + expr r = args[num_args - 1]; + unsigned i = num_args - 1; + while (i > 0) { + --i; + r = mkb(args[i], r); + } + return r; + } +} + /** \brief Return unit if num_args == 0, args[0] if num_args == 1, and (op ... (op (op args[0] args[1]) args[2]) ...) diff --git a/src/library/definitional/CMakeLists.txt b/src/library/definitional/CMakeLists.txt index abd7de53a..3cce4fea9 100644 --- a/src/library/definitional/CMakeLists.txt +++ b/src/library/definitional/CMakeLists.txt @@ -1,4 +1,4 @@ add_library(definitional rec_on.cpp induction_on.cpp cases_on.cpp - no_confusion.cpp util.cpp projection.cpp brec_on.cpp) + no_confusion.cpp util.cpp projection.cpp brec_on.cpp init_module.cpp) target_link_libraries(definitional ${LEAN_LIBS}) diff --git a/src/library/definitional/init_module.cpp b/src/library/definitional/init_module.cpp new file mode 100644 index 000000000..b4b20f1bd --- /dev/null +++ b/src/library/definitional/init_module.cpp @@ -0,0 +1,17 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "library/definitional/util.h" + +namespace lean{ +void initialize_definitional_module() { + initialize_definitional_util(); +} + +void finalize_definitional_module() { + finalize_definitional_util(); +} +} diff --git a/src/library/definitional/init_module.h b/src/library/definitional/init_module.h new file mode 100644 index 000000000..b58ff37fb --- /dev/null +++ b/src/library/definitional/init_module.h @@ -0,0 +1,12 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once + +namespace lean { +void initialize_definitional_module(); +void finalize_definitional_module(); +} diff --git a/src/library/definitional/util.cpp b/src/library/definitional/util.cpp index 0cd8466c4..946aea5d4 100644 --- a/src/library/definitional/util.cpp +++ b/src/library/definitional/util.cpp @@ -130,4 +130,132 @@ expr to_telescope(type_checker & tc, expr type, buffer & telescope, option } return type; } + +static expr * g_true = nullptr; +static expr * g_and = nullptr; +static expr * g_and_intro = nullptr; +static expr * g_and_elim_left = nullptr; +static expr * g_and_elim_right = nullptr; + +static name * g_unit = nullptr; +static name * g_prod_name = nullptr; +static name * g_prod_mk_name = nullptr; +static name * g_pr1_name = nullptr; +static name * g_pr2_name = nullptr; + +void initialize_definitional_util() { + g_true = new expr(mk_constant("true")); + g_and = new expr(mk_constant("and")); + g_and_intro = new expr(mk_constant({"and", "intro"})); + g_and_elim_left = new expr(mk_constant({"and", "elim_left"})); + g_and_elim_right = new expr(mk_constant({"and", "elim_right"})); + + g_unit = new name("unit"); + g_prod_name = new name("prod"); + g_prod_mk_name = new name{"prod", "mk"}; + g_pr1_name = new name{"prod", "pr1"}; + g_pr2_name = new name{"prod", "pr2"}; +} + +void finalize_definitional_util() { + delete g_true; + delete g_and; + delete g_and_intro; + delete g_and_elim_left; + delete g_and_elim_right; + delete g_unit; + delete g_prod_name; + delete g_prod_mk_name; + delete g_pr1_name; + delete g_pr2_name; +} + +expr mk_true() { + return *g_true; +} + +expr mk_and(expr const & a, expr const & b) { + return mk_app(*g_and, a, b); +} + +expr mk_and_intro(type_checker & tc, expr const & Ha, expr const & Hb) { + return mk_app(*g_and_intro, tc.infer(Ha).first, tc.infer(Hb).first, Ha, Hb); +} + +expr mk_and_elim_left(type_checker & tc, expr const & H) { + expr a_and_b = tc.whnf(tc.infer(H).first).first; + return mk_app(*g_and_elim_left, app_arg(app_fn(a_and_b)), app_arg(a_and_b), H); +} + +expr mk_and_elim_right(type_checker & tc, expr const & H) { + expr a_and_b = tc.whnf(tc.infer(H).first).first; + return mk_app(*g_and_elim_right, app_arg(app_fn(a_and_b)), app_arg(a_and_b), H); +} + +expr mk_unit(level const & l) { + return mk_constant(*g_unit, {l}); +} + +expr mk_prod(type_checker & tc, expr const & A, expr const & B) { + level l1 = sort_level(tc.ensure_type(A).first); + level l2 = sort_level(tc.ensure_type(B).first); + return mk_app(mk_constant(*g_prod_name, {l1, l2}), A, B); +} + +expr mk_pair(type_checker & tc, expr const & a, expr const & b) { + expr A = tc.infer(a).first; + expr B = tc.infer(b).first; + level l1 = sort_level(tc.ensure_type(A).first); + level l2 = sort_level(tc.ensure_type(B).first); + return mk_app(mk_constant(*g_prod_mk_name, {l1, l2}), A, B, a, b); +} + +expr mk_pr1(type_checker & tc, expr const & p) { + expr AxB = tc.whnf(tc.infer(p).first).first; + expr const & A = app_arg(app_fn(AxB)); + expr const & B = app_arg(AxB); + return mk_app(mk_constant(*g_pr1_name, const_levels(AxB)), A, B, p); +} + +expr mk_pr2(type_checker & tc, expr const & p) { + expr AxB = tc.whnf(tc.infer(p).first).first; + expr const & A = app_arg(app_fn(AxB)); + expr const & B = app_arg(AxB); + return mk_app(mk_constant(*g_pr2_name, const_levels(AxB)), A, B, p); +} + +expr mk_unit(level const & l, bool prop) { + if (prop) + return mk_true(); + else + return mk_unit(l); +} + +expr mk_prod(type_checker & tc, expr const & a, expr const & b, bool prop) { + if (prop) + return mk_and(a, b); + else + return mk_prod(tc, a, b); +} + +expr mk_pair(type_checker & tc, expr const & a, expr const & b, bool prop) { + if (prop) + return mk_and_intro(tc, a, b); + else + return mk_pair(tc, a, b); +} + +expr mk_pr1(type_checker & tc, expr const & p, bool prop) { + if (prop) + return mk_and_elim_left(tc, p); + else + return mk_pr1(tc, p); +} + +expr mk_pr2(type_checker & tc, expr const & p, bool prop) { + if (prop) + return mk_and_elim_right(tc, p); + else + return mk_pr2(tc, p); +} } diff --git a/src/library/definitional/util.h b/src/library/definitional/util.h index ccc3b7a9c..b3afffba8 100644 --- a/src/library/definitional/util.h +++ b/src/library/definitional/util.h @@ -52,4 +52,25 @@ expr to_telescope(type_checker & tc, expr type, buffer & telescope, level get_datatype_level(expr ind_type); expr instantiate_univ_param (expr const & e, name const & p, level const & l); + +expr mk_true(); +expr mk_and(expr const & a, expr const & b); +expr mk_and_intro(type_checker & tc, expr const & Ha, expr const & Hb); +expr mk_and_elim_left(type_checker & tc, expr const & H); +expr mk_and_elim_right(type_checker & tc, expr const & H); + +expr mk_unit(level const & l); +expr mk_prod(type_checker & tc, expr const & A, expr const & B); +expr mk_pair(type_checker & tc, expr const & a, expr const & b); +expr mk_pr1(type_checker & tc, expr const & p); +expr mk_pr2(type_checker & tc, expr const & p); + +expr mk_unit(level const & l, bool prop); +expr mk_prod(type_checker & tc, expr const & a, expr const & b, bool prop); +expr mk_pair(type_checker & tc, expr const & a, expr const & b, bool prop); +expr mk_pr1(type_checker & tc, expr const & p, bool prop); +expr mk_pr2(type_checker & tc, expr const & p, bool prop); + +void initialize_definitional_util(); +void finalize_definitional_util(); }