feat(kernel): add general purpose 'annotations', they are just a generalization of the 'let'-annotations

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/builtin_exprs.cpp

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include "util/sstream.h"
 #include "kernel/abstract.h"
+#include "kernel/annotation.h"
 #include "library/placeholder.h"
 #include "library/explicit.h"
 #include "library/tactic/tactic.h"
@@ -55,7 +56,7 @@ static expr parse_let_body(parser & p, pos_info const & pos) {
 
 static expr mk_let(parser & p, name const & id, expr const & t, expr const & v, expr const & b, pos_info const & pos, binder_info const & bi) {
     expr l = p.save_pos(mk_lambda(id, t, b, bi), pos);
-    return p.save_pos(mk_let_macro(p.save_pos(mk_app(l, v), pos)), pos);
+    return p.save_pos(mk_let_annotation(p.save_pos(mk_app(l, v), pos)), pos);
 }
 
 static void parse_let_modifiers(parser & p, bool & is_fact, bool & is_opaque) {

src/frontends/lean/pp.cpp

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include "util/flet.h"
 #include "kernel/replace_fn.h"
 #include "kernel/free_vars.h"
+#include "kernel/annotation.h"
 #include "library/aliases.h"
 #include "library/scoped_ext.h"
 #include "library/coercion.h"
@@ -294,9 +295,9 @@ auto pretty_fn::pp_pi(expr const & e) -> result {
 auto pretty_fn::pp_let(expr e) -> result {
     buffer<expr_pair> decls;
     while (true) {
-        if (!is_let_macro(e))
+        if (!is_let_annotation(e))
             break;
-        e = let_macro_arg(e);
+        e = get_annotation_arg(e);
         if (!is_app(e) || !is_lambda(app_fn(e)))
             break;
         expr v = app_arg(e);
@@ -325,7 +326,7 @@ auto pretty_fn::pp_let(expr e) -> result {
 }
 
 auto pretty_fn::pp_macro(expr const & e) -> result {
-    if (is_let_macro(e)) {
+    if (is_let_annotation(e)) {
         return pp_let(e);
     } else {
         // TODO(Leo): have macro annotations

src/kernel/CMakeLists.txt

@@ -2,6 +2,7 @@ add_library(kernel level.cpp expr.cpp expr_eq_fn.cpp for_each_fn.cpp
 replace_fn.cpp free_vars.cpp abstract.cpp instantiate.cpp
 formatter.cpp declaration.cpp replace_visitor.cpp environment.cpp
 justification.cpp pos_info_provider.cpp metavar.cpp converter.cpp
-constraint.cpp type_checker.cpp error_msgs.cpp kernel_exception.cpp )
+constraint.cpp type_checker.cpp error_msgs.cpp kernel_exception.cpp
+annotation.cpp)
 
 target_link_libraries(kernel ${LEAN_LIBS})

src/kernel/annotation.cpp

@@ -0,0 +1,92 @@
+/*
+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 <unordered_map>
+#include <memory>
+#include <string>
+#include "util/sstream.h"
+#include "kernel/annotation.h"
+
+namespace lean {
+static name g_annotation("annotation");
+
+std::string const & get_annotation_opcode() {
+    static std::string g_annotation_opcode("Annot");
+    return g_annotation_opcode;
+}
+
+/** \brief We use a macro to mark expressions that denote "let" and "have"-expressions.
+    These marks have no real semantic meaning, but are useful for helping Lean's pretty printer.
+*/
+class annotation_macro_definition_cell : public macro_definition_cell {
+    name m_name;
+    void check_macro(expr const & m) const {
+        if (!is_macro(m) || macro_num_args(m) != 1)
+            throw exception(sstream() << "invalid '" << m_name << "' annotation, incorrect number of arguments");
+    }
+public:
+    annotation_macro_definition_cell(name const & n):m_name(n) {}
+    name get_annotation_kind() const { return m_name; }
+    virtual name get_name() const { return g_annotation; }
+    virtual expr get_type(expr const & m, expr const * arg_types, extension_context &) const {
+        check_macro(m);
+        return arg_types[0];
+    }
+    virtual optional<expr> expand(expr const & m, extension_context &) const {
+        check_macro(m);
+        return some_expr(macro_arg(m, 0));
+    }
+    virtual void write(serializer & s) const {
+        s.write_string(get_annotation_opcode());
+        s << m_name;
+    }
+};
+
+typedef std::unordered_map<name, macro_definition, name_hash, name_eq> annotation_macros;
+static std::unique_ptr<annotation_macros> g_annotation_macros;
+annotation_macros & get_annotation_macros() {
+    if (!g_annotation_macros) g_annotation_macros.reset(new annotation_macros());
+    return *(g_annotation_macros.get());
+}
+
+void register_annotation(name const & n) {
+    annotation_macros & ms = get_annotation_macros();
+    lean_assert(ms.find(n) == ms.end());
+    ms.insert(mk_pair(n, macro_definition(new annotation_macro_definition_cell(n))));
+}
+
+expr mk_annotation(name const & kind, expr const & e) {
+    annotation_macros & ms = get_annotation_macros();
+    auto it = ms.find(kind);
+    if (it != ms.end()) {
+        return mk_macro(it->second, 1, &e);
+    } else {
+        throw exception(sstream() << "unknown annotation kind '" << kind << "'");
+    }
+}
+
+bool is_annotation(expr const & e) {
+    return is_macro(e) && macro_def(e).get_name() == g_annotation;
+}
+
+bool is_annotation(expr const & e, name const & kind) {
+    return is_annotation(e) && static_cast<annotation_macro_definition_cell const*>(macro_def(e).raw())->get_annotation_kind() == kind;
+}
+
+expr get_annotation_arg(expr const & e) {
+    lean_assert(is_annotation(e));
+    return macro_arg(e, 0);
+}
+
+static name g_let("let");
+static name g_have("have");
+register_annotation_fn g_let_annotation(g_let);
+register_annotation_fn g_have_annotation(g_have);
+expr mk_let_annotation(expr const & e) { return mk_annotation(g_let, e); }
+expr mk_have_annotation(expr const & e) { return mk_annotation(g_have, e); }
+bool is_let_annotation(expr const & e) { return is_annotation(e, g_let); }
+bool is_have_annotation(expr const & e) { return is_annotation(e, g_have); }
+}

src/kernel/annotation.h

@@ -0,0 +1,49 @@
+/*
+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
+#include <string>
+#include "kernel/expr.h"
+
+namespace lean {
+/** \brief Declare a new kind of annotation. It must only be invoked at startup time
+    Use helper obect #register_annotation_fn.
+*/
+void register_annotation(name const & n);
+/** \brief Helper object for declaring a new kind of annotation */
+struct register_annotation_fn {
+    register_annotation_fn(name const & kind) { register_annotation(kind); }
+};
+
+/** \brief Create an annotated expression with tag \c kind based on \c e.
+
+    \pre \c kind must have been registered using #register_annotation.
+
+    \remark Annotations have no real semantic meaning, but are useful for guiding pretty printer and/or automation.
+*/
+expr mk_annotation(name const & kind, expr const & e);
+/** \brief Return true iff \c e was created using #mk_annotation. */
+bool is_annotation(expr const & e);
+/** \brief Return true iff \c e was created using #mk_annotation, and has tag \c kind. */
+bool is_annotation(expr const & e, name const & kind);
+/** \brief Return the annotated expression, \c e must have been created using #mk_annotation.
+
+    \post get_annotation_arg(mk_annotation(k, e)) == e
+*/
+expr get_annotation_arg(expr const & e);
+
+/** \brief Tag \c e as a 'let'-expression. 'let' is a pre-registered annotation. */
+expr mk_let_annotation(expr const & e);
+/** \brief Tag \c e as a 'have'-expression. 'have' is a pre-registered annotation. */
+expr mk_have_annotation(expr const & e);
+/** \brief Return true iff \c e was created using #mk_let_annotation. */
+bool is_let_annotation(expr const & e);
+/** \brief Return true iff \c e was created using #mk_have_annotation. */
+bool is_have_annotation(expr const & e);
+
+/** \brief Return the serialization 'opcode' for annotation macros. */
+std::string const & get_annotation_opcode();
+}

src/kernel/expr.cpp

@@ -594,39 +594,6 @@ bool is_arrow(expr const & t) {
     }
 }
 
-static name g_let("let");
-std::string const & get_let_macro_opcode() {
-    static std::string g_let_macro_opcode("let");
-    return g_let_macro_opcode;
-}
-
-/**
-   \brief We use a macro to mark expressions that denote "let"-expressions.
-   This marks have no real semantic meaning, but are used by Lean's pretty printer.
-*/
-class let_macro_definition_cell : public macro_definition_cell {
-    static void check_macro(expr const & m) {
-        if (!is_macro(m) || macro_num_args(m) != 1)
-            throw exception("invalid 'let' macro");
-    }
-public:
-    virtual name get_name() const { return g_let; }
-    virtual expr get_type(expr const & m, expr const * arg_types, extension_context &) const {
-        check_macro(m);
-        return arg_types[0];
-    }
-    virtual optional<expr> expand(expr const & m, extension_context &) const {
-        check_macro(m);
-        return some_expr(macro_arg(m, 0));
-    }
-    virtual void write(serializer & s) const { s.write_string(get_let_macro_opcode()); }
-};
-
-static macro_definition g_let_macro_definition(new let_macro_definition_cell());
-expr mk_let_macro(expr const & e) { return mk_macro(g_let_macro_definition, 1, &e); }
-bool is_let_macro(expr const & e) { return is_macro(e) && macro_def(e) == g_let_macro_definition; }
-expr let_macro_arg(expr const & e) { lean_assert(is_let_macro(e)); return macro_arg(e, 0); }
-
 static bool has_free_var_in_domain(expr const & b, unsigned vidx) {
     if (is_pi(b)) {
         return has_free_var(binding_domain(b), vidx) || has_free_var_in_domain(binding_body(b), vidx+1);

src/kernel/expr.h

@@ -677,14 +677,6 @@ expr update_constant(expr const & e, levels const & new_levels);
 expr update_macro(expr const & e, unsigned num, expr const * args);
 // =======================================
 
-// =======================================
-// Auxiliary macro for "marking" let-expressions
-expr mk_let_macro(expr const & e);
-bool is_let_macro(expr const & e);
-expr let_macro_arg(expr const & e);
-std::string const & get_let_macro_opcode();
-// =======================================
-
 // =======================================
 // Implicit argument inference
 /**

src/kernel/formatter.cpp

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 #include "kernel/find_fn.h"
 #include "kernel/instantiate.h"
 #include "kernel/free_vars.h"
+#include "kernel/annotation.h"
 
 namespace lean {
 bool is_used_name(expr const & t, name const & n) {
@@ -78,9 +79,9 @@ struct print_expr_fn {
     }
 
     bool print_let(expr const & a) {
-        if (!is_let_macro(a))
+        if (!is_let_annotation(a))
             return false;
-        expr l = let_macro_arg(a);
+        expr l = get_annotation_arg(a);
         if (!is_app(l) || !is_lambda(app_fn(l)))
             return false;
         name n = binding_name(app_fn(l));

src/library/kernel_serializer.cpp

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "util/object_serializer.h"
 #include "kernel/expr.h"
 #include "kernel/declaration.h"
+#include "kernel/annotation.h"
 #include "library/max_sharing.h"
 #include "library/kernel_serializer.h"
 
@@ -353,12 +354,13 @@ inductive_decls read_inductive_decls(deserializer & d) {
     return inductive_decls(ps, num_params, to_list(decls.begin(), decls.end()));
 }
 
-
 static register_macro_deserializer_fn
-let_macro_des_fn(get_let_macro_opcode(),
-                 [](deserializer &, unsigned num, expr const * args) {
+annotation_des_fn(get_annotation_opcode(),
+                  [](deserializer & d, unsigned num, expr const * args) {
                       if (num != 1)
                           throw_corrupted_file();
-                     return mk_let_macro(args[0]);
+                      name k;
+                      d >> k;
+                      return mk_annotation(k, args[0]);
                   });
 }