From b9489ce58562eb37244a6bf77ad035a79ee1d030 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 29 Aug 2014 09:58:11 -0700 Subject: [PATCH] fix(frontends/let): let-expression pretty printer Signed-off-by: Leonardo de Moura --- src/frontends/lean/builtin_exprs.cpp | 2 +- src/frontends/lean/elaborator.cpp | 7 +-- src/frontends/lean/parser.cpp | 4 +- src/frontends/lean/pp.cpp | 3 +- src/library/annotation.cpp | 9 ---- src/library/annotation.h | 4 -- src/library/let.cpp | 64 +++++++++++++++++++++++++++- src/library/let.h | 4 ++ src/util/thread.h | 3 ++ tests/lean/let4.lean | 19 +++++++++ tests/lean/let4.lean.expected.out | 7 +++ 11 files changed, 103 insertions(+), 23 deletions(-) create mode 100644 tests/lean/let4.lean create mode 100644 tests/lean/let4.lean.expected.out diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index c643dcb66..96b3654fc 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -104,7 +104,7 @@ static expr parse_let(parser & p, pos_info const & pos) { v = p.save_pos(mk_typed_expr(*type, value), p.pos_of(value)); else v = value; - v = p.save_pos(mk_let_value_annotation(v), id_pos); + v = p.save_pos(mk_let_value(v), id_pos); p.add_local_expr(id, v); expr b = parse_let_body(p, pos); return p.save_pos(mk_let(id, v, b), pos); diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 3c57e2978..c740d2824 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -26,6 +26,7 @@ Author: Leonardo de Moura #include "library/unifier.h" #include "library/opaque_hints.h" #include "library/locals.h" +#include "library/let.h" #include "library/deep_copy.h" #include "library/typed_expr.h" #include "library/tactic/tactic.h" @@ -1096,8 +1097,8 @@ public: cs += p->second; return p->first; } else { - auto ecs = visit(get_annotation_arg(e)); - expr r = copy_tag(ecs.first, mk_let_value_annotation(ecs.first)); + auto ecs = visit(get_let_value_expr(e)); + expr r = copy_tag(ecs.first, mk_let_value(ecs.first)); m_cache.insert(e, mk_pair(r, ecs.second)); cs += ecs.second; return r; @@ -1109,7 +1110,7 @@ public: return visit_placeholder(e, cs); } else if (is_choice(e)) { return visit_choice(e, none_expr(), cs); - } else if (is_let_value_annotation(e)) { + } else if (is_let_value(e)) { return visit_let_value(e, cs); } else if (is_by(e)) { return visit_by(e, none_expr(), cs); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 24fe908fa..3a4d5486d 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -27,7 +27,7 @@ Author: Leonardo de Moura #include "library/module.h" #include "library/scoped_ext.h" #include "library/explicit.h" -#include "library/annotation.h" +#include "library/let.h" #include "library/num.h" #include "library/string.h" #include "library/sorry.h" @@ -282,7 +282,7 @@ expr parser::rec_save_pos(expr const & e, pos_info p) { /** \brief Create a copy of \c e, and the position of new expression with p */ expr parser::copy_with_new_pos(expr const & e, pos_info p) { - if (is_let_value_annotation(e)) + if (is_let_value(e)) return e; switch (e.kind()) { case expr_kind::Sort: case expr_kind::Constant: case expr_kind::Meta: diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 7b6d0db0d..975c2c10c 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -324,7 +324,6 @@ static bool is_show(expr const & e) { return is_show_annotation(e) && is_app(get_annotation_arg(e)) && is_lambda(app_fn(get_annotation_arg(e))); } -static bool is_let_value(expr const & e) { return is_let_value_annotation(e); } auto pretty_fn::pp_have(expr const & e) -> result { expr proof = app_arg(e); @@ -431,7 +430,7 @@ auto pretty_fn::pp(expr const & e) -> result { if (is_have(e)) return pp_have(e); if (is_let(e)) return pp_let(e); if (is_typed_expr(e)) return pp(get_typed_expr_expr(e)); - if (is_let_value(e)) return pp(get_annotation_arg(e)); + if (is_let_value(e)) return pp(get_let_value_expr(e)); if (auto n = to_num(e)) return pp_num(*n); if (!m_metavar_args && is_meta(e)) return pp_meta(get_app_fn(e)); diff --git a/src/library/annotation.cpp b/src/library/annotation.cpp index e1c80daf9..742a75b98 100644 --- a/src/library/annotation.cpp +++ b/src/library/annotation.cpp @@ -91,12 +91,6 @@ expr const & get_annotation_arg(expr const & e) { return macro_arg(e, 0); } -name const & get_let_value_name() { - static name g_let("letv"); - static register_annotation_fn g_let_annotation(g_let); - return g_let; -} - name const & get_have_name() { static name g_have("have"); static register_annotation_fn g_have_annotation(g_have); @@ -109,14 +103,11 @@ name const & get_show_name() { return g_show; } -static name g_let_name = get_let_value_name(); // force 'let value' annotation to be registered static name g_have_name = get_have_name(); // force 'have' annotation to be registered static name g_show_name = get_show_name(); // force 'show' annotation to be registered -expr mk_let_value_annotation(expr const & e) { return mk_annotation(get_let_value_name(), e); } expr mk_have_annotation(expr const & e) { return mk_annotation(get_have_name(), e); } expr mk_show_annotation(expr const & e) { return mk_annotation(get_show_name(), e); } -bool is_let_value_annotation(expr const & e) { return is_annotation(e, get_let_value_name()); } bool is_have_annotation(expr const & e) { return is_annotation(e, get_have_name()); } bool is_show_annotation(expr const & e) { return is_annotation(e, get_show_name()); } } diff --git a/src/library/annotation.h b/src/library/annotation.h index 0e57878f8..8c598f48f 100644 --- a/src/library/annotation.h +++ b/src/library/annotation.h @@ -40,14 +40,10 @@ expr const & get_annotation_arg(expr const & e); */ name const & get_annotation_kind(expr const & e); -/** \brief Tag \c e as a 'let value'-expression. 'let value' is a pre-registered annotation. */ -expr mk_let_value_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 Tag \c e as a 'show'-expression. 'show' is a pre-registered annotation. */ expr mk_show_annotation(expr const & e); -/** \brief Return true iff \c e was created using #mk_let_value_annotation. */ -bool is_let_value_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 true iff \c e was created using #mk_show_annotation. */ diff --git a/src/library/let.cpp b/src/library/let.cpp index 82c74fe54..d11dadff4 100644 --- a/src/library/let.cpp +++ b/src/library/let.cpp @@ -5,10 +5,71 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include "util/thread.h" #include "kernel/expr.h" #include "library/kernel_serializer.h" namespace lean { +static name g_let_value("letv"); +std::string const & get_let_value_opcode() { + static std::string g_let_value_opcode("LetV"); + return g_let_value_opcode; +} + +static atomic g_next_let_value_id(0); +static unsigned next_let_value_id() { + return atomic_fetch_add_explicit(&g_next_let_value_id, 1u, memory_order_seq_cst); +} + +class let_value_definition_cell : public macro_definition_cell { + unsigned m_id; + void check_macro(expr const & m) const { + if (!is_macro(m) || macro_num_args(m) != 1) + throw exception("invalid let-value expression"); + } +public: + let_value_definition_cell():m_id(next_let_value_id()) {} + virtual name get_name() const { return g_let_value; } + 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_value_opcode()); + } + virtual bool operator==(macro_definition_cell const & other) const { + return + dynamic_cast(&other) != nullptr && + m_id == static_cast(other).m_id; + } + virtual unsigned hash() const { return m_id; } +}; + +expr mk_let_value(expr const & e) { + auto d = macro_definition(new let_value_definition_cell()); + return mk_macro(d, 1, &e); +} + +bool is_let_value(expr const & e) { + return is_macro(e) && dynamic_cast(macro_def(e).raw()); +} + +expr get_let_value_expr(expr const e) { + lean_assert(is_let_value(e)); + return macro_arg(e, 0); +} + +static register_macro_deserializer_fn +let_value_des_fn(get_let_value_opcode(), + [](deserializer &, unsigned num, expr const * args) { + if (num != 1) throw corrupted_stream_exception(); + return mk_let_value(args[0]); + }); + static name g_let("let"); std::string const & get_let_opcode() { static std::string g_let_opcode("Let"); @@ -67,8 +128,7 @@ expr const & get_let_body(expr const & e) { static register_macro_deserializer_fn let_des_fn(get_let_opcode(), [](deserializer & d, unsigned num, expr const * args) { - if (num != 2) - throw corrupted_stream_exception(); + if (num != 2) throw corrupted_stream_exception(); name n; d >> n; return mk_let(n, args[0], args[1]); diff --git a/src/library/let.h b/src/library/let.h index 96edbda60..ea5e4e8d8 100644 --- a/src/library/let.h +++ b/src/library/let.h @@ -8,6 +8,10 @@ Author: Leonardo de Moura #include "kernel/expr.h" namespace lean { +expr mk_let_value(expr const & e); +bool is_let_value(expr const & e); +expr get_let_value_expr(expr const e); + expr mk_let(name const & n, expr const & v, expr const & b); bool is_let(expr const & e); name const & get_let_var_name(expr const & e); diff --git a/src/util/thread.h b/src/util/thread.h index 16b3e4da1..03e8f9674 100644 --- a/src/util/thread.h +++ b/src/util/thread.h @@ -33,6 +33,7 @@ using std::atomic_fetch_sub_explicit; using std::memory_order_relaxed; using std::memory_order_release; using std::memory_order_acquire; +using std::memory_order_seq_cst; using std::atomic_thread_fence; namespace chrono = std::chrono; namespace this_thread = std::this_thread; @@ -51,6 +52,7 @@ using boost::atomic; using boost::memory_order_relaxed; using boost::memory_order_acquire; using boost::memory_order_release; +using boost::memory_order_seq_cst; using boost::condition_variable; using boost::unique_lock; using boost::lock_guard; @@ -79,6 +81,7 @@ typedef unsigned milliseconds; constexpr int memory_order_relaxed = 0; constexpr int memory_order_release = 0; constexpr int memory_order_acquire = 0; +constexpr int memory_order_seq_cst = 0; inline void atomic_thread_fence(int ) {} template class atomic { diff --git a/tests/lean/let4.lean b/tests/lean/let4.lean new file mode 100644 index 000000000..9b765e4e0 --- /dev/null +++ b/tests/lean/let4.lean @@ -0,0 +1,19 @@ +import data.num +using num + +variable f : num → num → num → num + +check + let a := 10, + b := 10, + c := 10 + in f a b (f a 10 c) + +check + let a := 10, + b := let c := 10 in f a c (f a a (f 10 a c)), + d := 10, + e := f (f 10 10 d) (f d 10 10) a + in f a b (f e d 10) + + diff --git a/tests/lean/let4.lean.expected.out b/tests/lean/let4.lean.expected.out new file mode 100644 index 000000000..a2a927e83 --- /dev/null +++ b/tests/lean/let4.lean.expected.out @@ -0,0 +1,7 @@ +let a := 10, b := 10, c := 10 in f a b (f a 10 c) : num +let a := 10, + b := let c := 10 in f a c (f a a (f 10 a c)), + d := 10, + e := f (f 10 10 d) (f d 10 10) a +in f a b (f e d 10) : + num