feat(compiler): mark computationally irrelevant terms

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)

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<expr> 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;
+}
+}

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();
+}

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);
+}
 }

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;

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);

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();
 }

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());

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 {