From da8f37d7cce6c0ec6af470ce17fd28036daa0ca4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 2 May 2016 16:23:54 -0700 Subject: [PATCH] feat(compiler): mark computationally irrelevant terms --- src/compiler/CMakeLists.txt | 3 +- src/compiler/comp_irrelevant.cpp | 110 +++++++++++++++++++++++++ src/compiler/comp_irrelevant.h | 17 ++++ src/compiler/compiler_step_visitor.cpp | 8 ++ src/compiler/compiler_step_visitor.h | 2 + src/compiler/eta_expansion.cpp | 5 +- src/compiler/init_module.cpp | 3 + src/compiler/preprocess_rec.cpp | 6 +- src/frontends/lean/pp.cpp | 3 + 9 files changed, 153 insertions(+), 4 deletions(-) create mode 100644 src/compiler/comp_irrelevant.cpp create mode 100644 src/compiler/comp_irrelevant.h diff --git a/src/compiler/CMakeLists.txt b/src/compiler/CMakeLists.txt index 63c5e786a1..e41f863d7c 100644 --- a/src/compiler/CMakeLists.txt +++ b/src/compiler/CMakeLists.txt @@ -1,2 +1,3 @@ add_library(compiler OBJECT util.cpp eta_expansion.cpp simp_pr1_rec.cpp preprocess_rec.cpp - compiler_step_visitor.cpp fresh_constant.cpp lambda_lifting.cpp init_module.cpp) + compiler_step_visitor.cpp fresh_constant.cpp lambda_lifting.cpp comp_irrelevant.cpp + init_module.cpp) diff --git a/src/compiler/comp_irrelevant.cpp b/src/compiler/comp_irrelevant.cpp new file mode 100644 index 0000000000..c24c1a2d04 --- /dev/null +++ b/src/compiler/comp_irrelevant.cpp @@ -0,0 +1,110 @@ +/* +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 "library/annotation.h" +#include "compiler/compiler_step_visitor.h" + +namespace lean { +static name * g_comp_irrel = nullptr; + +static expr mark_comp_irrelevant(expr const & e) { + return mk_annotation(*g_comp_irrel, e); +} + +bool is_comp_irrelevant(expr const & e) { + return is_annotation(e, *g_comp_irrel); +} + +class mark_comp_irrelevant_fn : public compiler_step_visitor { +protected: + optional mark_if_irrel_core(expr const & e) { + expr type = ctx().whnf(ctx().infer(e)); + if (is_sort(type) || ctx().is_prop(type)) + return some_expr(mark_comp_irrelevant(e)); + else + return none_expr(); + } + + expr mark_if_irrel(expr const & e) { + if (auto v = mark_if_irrel_core(e)) + return *v; + else + return e; + } + + expr mark_lambda_let(expr const & e) { + /* if body is marked as computationally irrelevant, then mark e */ + expr body = e; + while (true) { + if (is_lambda(body)) + body = binding_body(body); + else if (is_let(body)) + body = let_body(body); + else + break; + } + if (is_comp_irrelevant(body)) + return mark_comp_irrelevant(e); + else + return e; + } + + virtual expr visit_sort(expr const & e) override { + return mark_comp_irrelevant(e); + } + + virtual expr visit_pi(expr const & e) override { + return mark_comp_irrelevant(e); + } + + virtual expr visit_macro(expr const & e) override { + if (is_comp_irrelevant(e)) + return e; + else if (auto v = mark_if_irrel_core(e)) + return *v; + else + return compiler_step_visitor::visit_macro(e); + } + + virtual expr visit_constant(expr const & e) override { + return mark_if_irrel(e); + } + + virtual expr visit_local(expr const & e) override { + return mark_if_irrel(e); + } + + virtual expr visit_app(expr const & e) override { + if (auto v = mark_if_irrel_core(e)) + return *v; + else + return compiler_step_visitor::visit_app(e); + } + + virtual expr visit_lambda(expr const & e) override { + return mark_lambda_let(compiler_step_visitor::visit_lambda(e)); + } + + virtual expr visit_let(expr const & e) override { + return mark_lambda_let(compiler_step_visitor::visit_let(e)); + } +public: + mark_comp_irrelevant_fn(environment const & env):compiler_step_visitor(env) {} +}; + +expr mark_comp_irrelevant(environment const & env, expr const & e) { + return mark_comp_irrelevant_fn(env)(e); +} + +void initialize_comp_irrelevant() { + g_comp_irrel = new name("comp_irrel"); + register_annotation(*g_comp_irrel); +} + +void finalize_comp_irrelevant() { + delete g_comp_irrel; +} +} diff --git a/src/compiler/comp_irrelevant.h b/src/compiler/comp_irrelevant.h new file mode 100644 index 0000000000..27ffacac46 --- /dev/null +++ b/src/compiler/comp_irrelevant.h @@ -0,0 +1,17 @@ +/* +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 "kernel/environment.h" + +namespace lean { +/** \brief Mark sub-expressions of \c e that are computationally irrelevant. */ +expr mark_comp_irrelevant(environment const & env, expr const & e); +/** \brief Return true iff \c e is annotated with the comp-irrelevant annotation */ +bool is_comp_irrelevant(expr const & e); +void initialize_comp_irrelevant(); +void finalize_comp_irrelevant(); +} diff --git a/src/compiler/compiler_step_visitor.cpp b/src/compiler/compiler_step_visitor.cpp index 1b98be6699..91299159c7 100644 --- a/src/compiler/compiler_step_visitor.cpp +++ b/src/compiler/compiler_step_visitor.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include "kernel/instantiate.h" #include "compiler/compiler_step_visitor.h" +#include "compiler/comp_irrelevant.h" namespace lean { compiler_step_visitor::compiler_step_visitor(environment const & env): @@ -46,4 +47,11 @@ expr compiler_step_visitor::visit_lambda(expr const & e) { expr compiler_step_visitor::visit_let(expr const & e) { return visit_lambda_let(e); } + +expr compiler_step_visitor::visit_macro(expr const & e) { + if (is_comp_irrelevant(e)) + return e; + else + return replace_visitor::visit_macro(e); +} } diff --git a/src/compiler/compiler_step_visitor.h b/src/compiler/compiler_step_visitor.h index e9d335017f..014848d5f6 100644 --- a/src/compiler/compiler_step_visitor.h +++ b/src/compiler/compiler_step_visitor.h @@ -26,6 +26,8 @@ protected: environment const & env() const { return m_env; } type_context & ctx() { return m_ctx; } + virtual expr visit_macro(expr const & e) override; + virtual expr visit_pi(expr const & e) override { /* Compiler steps ignore types. */ return e; diff --git a/src/compiler/eta_expansion.cpp b/src/compiler/eta_expansion.cpp index bbbdda2f6b..7ec4252467 100644 --- a/src/compiler/eta_expansion.cpp +++ b/src/compiler/eta_expansion.cpp @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include "kernel/abstract.h" #include "kernel/instantiate.h" #include "compiler/compiler_step_visitor.h" +#include "compiler/comp_irrelevant.h" #include "compiler/eta_expansion.h" namespace lean { @@ -30,7 +31,9 @@ class eta_expand_fn : public compiler_step_visitor { } virtual expr visit_macro(expr const & e) override { - if (auto r = expand_core(e)) + if (is_comp_irrelevant(e)) + return e; + else if (auto r = expand_core(e)) return *r; else return compiler_step_visitor::visit_macro(e); diff --git a/src/compiler/init_module.cpp b/src/compiler/init_module.cpp index b791db4fb6..1157461722 100644 --- a/src/compiler/init_module.cpp +++ b/src/compiler/init_module.cpp @@ -6,13 +6,16 @@ Author: Leonardo de Moura */ #include "compiler/preprocess_rec.h" #include "compiler/fresh_constant.h" +#include "compiler/comp_irrelevant.h" namespace lean{ void initialize_compiler_module() { initialize_preprocess_rec(); initialize_fresh_constant(); + initialize_comp_irrelevant(); } void finalize_compiler_module() { + finalize_comp_irrelevant(); finalize_preprocess_rec(); finalize_fresh_constant(); } diff --git a/src/compiler/preprocess_rec.cpp b/src/compiler/preprocess_rec.cpp index c725c5406a..59f97dc6e6 100644 --- a/src/compiler/preprocess_rec.cpp +++ b/src/compiler/preprocess_rec.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "library/user_recursors.h" #include "library/util.h" #include "compiler/compiler_step_visitor.h" +#include "compiler/comp_irrelevant.h" #include "compiler/eta_expansion.h" #include "compiler/simp_pr1_rec.h" #include "compiler/lambda_lifting.h" @@ -67,10 +68,10 @@ class preprocess_rec_fn { for (name const & n : m_aux_decls) { std::cout << ">> " << n << "\n"; declaration d = m_env.get(n); - ::pp(m_env, d.get_value()); + ::pp_detail(m_env, d.get_value()); } std::cout << ">> main\n"; - ::pp(m_env, v); + ::pp_detail(m_env, v); } public: @@ -80,6 +81,7 @@ public: environment operator()(declaration const & d) { expr v = d.get_value(); v = expand_aux_recursors(m_env, v); + v = mark_comp_irrelevant(m_env, v); v = eta_expand(m_env, v); v = simp_pr1_rec(m_env, v); v = lambda_lifting(m_env, v, m_aux_decls, d.is_trusted()); diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index b68512e35a..782a2cd2ec 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -34,6 +34,7 @@ Author: Leonardo de Moura #include "library/constants.h" #include "library/replace_visitor.h" #include "library/definitional/equations.h" +#include "compiler/comp_irrelevant.h" #include "frontends/lean/pp.h" #include "frontends/lean/util.h" #include "frontends/lean/token_table.h" @@ -813,6 +814,8 @@ auto pretty_fn::pp_macro(expr const & e) -> result { return result(group(nest(1, li + pp(get_annotation_arg(e)).fmt() + ri))); // } else if (is_pattern_hint(e)) { // return result(group(nest(2, format("(:") + pp(get_pattern_hint_arg(e)).fmt() + format(":)")))); + } else if (is_comp_irrelevant(e)) { + return m_unicode ? format("◾") : format("irrel"); } else if (is_annotation(e)) { return pp(get_annotation_arg(e)); } else {