From 022a151cf7b5cf8b59cbfec38abe409438de5cd1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 25 Jul 2014 09:33:31 -0700 Subject: [PATCH] feat(kernel): add general purpose 'annotations', they are just a generalization of the 'let'-annotations Signed-off-by: Leonardo de Moura --- src/frontends/lean/builtin_exprs.cpp | 3 +- src/frontends/lean/pp.cpp | 7 ++- src/kernel/CMakeLists.txt | 3 +- src/kernel/annotation.cpp | 92 ++++++++++++++++++++++++++++ src/kernel/annotation.h | 49 +++++++++++++++ src/kernel/expr.cpp | 33 ---------- src/kernel/expr.h | 8 --- src/kernel/formatter.cpp | 5 +- src/library/kernel_serializer.cpp | 16 ++--- 9 files changed, 161 insertions(+), 55 deletions(-) create mode 100644 src/kernel/annotation.cpp create mode 100644 src/kernel/annotation.h diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 303fd12049..695730bb14 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/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) { diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 817fccda84..bd8260bcee 100644 --- a/src/frontends/lean/pp.cpp +++ b/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 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 diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index f846dac2e9..7f150297b5 100644 --- a/src/kernel/CMakeLists.txt +++ b/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}) diff --git a/src/kernel/annotation.cpp b/src/kernel/annotation.cpp new file mode 100644 index 0000000000..84ae9b99d0 --- /dev/null +++ b/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 +#include +#include +#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 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 annotation_macros; +static std::unique_ptr 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(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); } +} diff --git a/src/kernel/annotation.h b/src/kernel/annotation.h new file mode 100644 index 0000000000..d9c1135171 --- /dev/null +++ b/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 +#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(); +} diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index d47d080ded..2f8980c78e 100644 --- a/src/kernel/expr.cpp +++ b/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 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); diff --git a/src/kernel/expr.h b/src/kernel/expr.h index f5d96239e2..37a058fb61 100644 --- a/src/kernel/expr.h +++ b/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 /** diff --git a/src/kernel/formatter.cpp b/src/kernel/formatter.cpp index 5fa813baec..c90ca258bf 100644 --- a/src/kernel/formatter.cpp +++ b/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)); diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp index 92bd28766e..b37e999688 100644 --- a/src/library/kernel_serializer.cpp +++ b/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) { - if (num != 1) - throw_corrupted_file(); - return mk_let_macro(args[0]); - }); +annotation_des_fn(get_annotation_opcode(), + [](deserializer & d, unsigned num, expr const * args) { + if (num != 1) + throw_corrupted_file(); + name k; + d >> k; + return mk_annotation(k, args[0]); + }); }