From 5a203d1c7508df8208e217cf40a99843b57cfcc2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 3 Sep 2014 11:52:35 -0700 Subject: [PATCH] feat(frontends/lean): add '?' for inspecting the type of any expression, it produces a EXTRA_TYPE info entry Signed-off-by: Leonardo de Moura --- src/emacs/lean-syntax.el | 2 ++ src/frontends/lean/CMakeLists.txt | 2 +- src/frontends/lean/builtin_exprs.cpp | 9 +++++++ src/frontends/lean/elaborator.cpp | 28 ++++++++++++++++++--- src/frontends/lean/info_manager.cpp | 37 +++++++++++++++++++++++++++- src/frontends/lean/info_manager.h | 3 +++ src/frontends/lean/qinfo.cpp | 19 ++++++++++++++ src/frontends/lean/qinfo.h | 17 +++++++++++++ src/frontends/lean/token_table.cpp | 2 +- 9 files changed, 112 insertions(+), 7 deletions(-) create mode 100644 src/frontends/lean/qinfo.cpp create mode 100644 src/frontends/lean/qinfo.h diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index bea59f468..1ec641e49 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -77,6 +77,8 @@ (,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face) ;; sorry (,(rx symbol-start "sorry" symbol-end) . 'font-lock-warning-face) + ;; ? query + (,(rx "?") . 'font-lock-warning-face) ;; lean-keywords (, (concat "\\(" (regexp-opt lean-keywords 'words) "\\)") (1 'font-lock-keyword-face))))) diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index 6a9d6972b..dac0da954 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -5,6 +5,6 @@ server.cpp notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp inductive_cmd.cpp elaborator.cpp dependencies.cpp parser_bindings.cpp begin_end_ext.cpp class.cpp pp_options.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp -structure_cmd.cpp info_manager.cpp noinfo.cpp) +structure_cmd.cpp info_manager.cpp noinfo.cpp qinfo.cpp) target_link_libraries(lean_frontend ${LEAN_LIBS}) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 96b3654fc..d98305ee0 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -19,6 +19,7 @@ Author: Leonardo de Moura #include "frontends/lean/calc.h" #include "frontends/lean/begin_end_ext.h" #include "frontends/lean/parser.h" +#include "frontends/lean/qinfo.h" #include "frontends/lean/util.h" namespace lean { @@ -362,11 +363,18 @@ static expr parse_sorry(parser & p, unsigned, expr const *, pos_info const & pos return p.mk_sorry(pos); } +static expr parse_question_mark(parser & p, unsigned, expr const *, pos_info const & pos) { + expr e = p.parse_expr(get_max_prec()); + e = p.save_pos(mk_qinfo(e), pos); + return e; +} + parse_table init_nud_table() { action Expr(mk_expr_action()); action Skip(mk_skip_action()); action Binders(mk_binders_action()); expr x0 = mk_var(0); + expr x1 = mk_var(1); parse_table r; r = r.add({transition("_", mk_ext_action(parse_placeholder))}, x0); r = r.add({transition("by", mk_ext_action(parse_by))}, x0); @@ -374,6 +382,7 @@ parse_table init_nud_table() { r = r.add({transition("show", mk_ext_action(parse_show))}, x0); r = r.add({transition("obtain", mk_ext_action(parse_obtain))}, x0); r = r.add({transition("(", Expr), transition(")", Skip)}, x0); + r = r.add({transition("?", mk_ext_action(parse_question_mark))}, x0); r = r.add({transition("fun", Binders), transition(",", mk_scoped_expr_action(x0))}, x0); r = r.add({transition("Pi", Binders), transition(",", mk_scoped_expr_action(x0, 0, false))}, x0); r = r.add({transition("Type", mk_ext_action(parse_Type))}, x0); diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index cdb940f9f..9dd5d718e 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -38,6 +38,7 @@ Author: Leonardo de Moura #include "frontends/lean/info_manager.h" #include "frontends/lean/elaborator.h" #include "frontends/lean/noinfo.h" +#include "frontends/lean/qinfo.h" #ifndef LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES #define LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES true @@ -550,7 +551,7 @@ public: expr mk_app(expr const & f, expr const & a, tag g) { return save_tag(::lean::mk_app(f, a), g); } /** \brief Store the pair (pos(e), type(r)) in the info_data if m_info_manager is available. */ - void save_info_data(expr const & e, expr const & r) { + void save_type_data(expr const & e, expr const & r) { if (!m_noinfo && infom() && pip() && (is_constant(e) || is_local(e) || is_placeholder(e))) { if (auto p = pip()->get_pos_info(e)) { expr t = m_tc[m_relax_main_opaque]->infer(r).first; @@ -559,6 +560,16 @@ public: } } + /** \brief Store type information at pos(e) for r if \c e is marked as "extra" in the info_manager */ + void save_extra_type_data(expr const & e, expr const & r) { + if (!m_noinfo && infom() && pip()) { + if (auto p = pip()->get_pos_info(e)) { + expr t = m_tc[m_relax_main_opaque]->infer(r).first; + m_pre_info_data.add_extra_type_info(p->first, p->second, r, t); + } + } + } + /** \brief Auxiliary function for saving information about which overloaded identifier was used by the elaborator. */ void save_identifier_info(expr const & f) { if (!m_noinfo && infom() && pip() && is_constant(f)) { @@ -577,7 +588,7 @@ public: void save_placeholder_info(expr const & e, expr const & r) { if (is_explicit_placeholder(e)) { - save_info_data(e, r); + save_type_data(e, r); save_synth_data(e, r); } } @@ -1001,7 +1012,7 @@ public: } if (!first) { // we save the info data again for application of functions with strict implicit arguments - save_info_data(get_app_fn(e), f); + save_type_data(get_app_fn(e), f); } } constraint_seq a_cs; @@ -1187,6 +1198,13 @@ public: } } + expr visit_qinfo(expr const & e, constraint_seq & cs) { + auto ecs = visit(get_annotation_arg(e)); + cs += ecs.second; + save_extra_type_data(e, ecs.first); + return ecs.first; + } + expr visit_core(expr const & e, constraint_seq & cs) { if (is_placeholder(e)) { return visit_placeholder(e, cs); @@ -1201,6 +1219,8 @@ public: return visit(get_annotation_arg(e), cs); } else if (is_typed_expr(e)) { return visit_typed_expr(e, cs); + } else if (is_qinfo(e)) { + return visit_qinfo(e, cs); } else { switch (e.kind()) { case expr_kind::Local: return e; @@ -1247,7 +1267,7 @@ public: } } } - save_info_data(b, r); + save_type_data(b, r); return mk_pair(r, cs); } diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp index ca6992ea6..81ef56680 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -16,7 +16,7 @@ Author: Leonardo de Moura namespace lean { class info_data; -enum class info_kind { Type = 0, Synth, Overload, Coercion, Symbol, Identifier }; +enum class info_kind { Type = 0, ExtraType, Synth, Overload, Coercion, Symbol, Identifier }; bool operator<(info_kind k1, info_kind k2) { return static_cast(k1) < static_cast(k2); } class info_data_cell { @@ -102,6 +102,31 @@ public: } }; +class extra_type_info_data : public info_data_cell { +protected: + expr m_expr; + expr m_type; +public: + extra_type_info_data() {} + extra_type_info_data(unsigned c, expr const & e, expr const & t):info_data_cell(c), m_expr(e), m_type(t) {} + + virtual info_kind kind() const { return info_kind::ExtraType; } + + virtual void display(io_state_stream const & ios, unsigned line) const { + ios << "-- EXTRA_TYPE|" << line << "|" << get_column() << "\n"; + ios << m_expr << endl; + ios << "--" << endl; + ios << m_type << endl; + ios << "-- ACK" << endl; + } + + virtual info_data_cell * instantiate(substitution & s) const { + expr e = s.instantiate(m_expr); + expr t = s.instantiate(m_type); + return is_eqp(e, m_expr) && is_eqp(t, m_type) ? nullptr : new extra_type_info_data(get_column(), e, t); + } +}; + class synth_info_data : public type_info_data { public: synth_info_data(unsigned c, expr const & e):type_info_data(c, e) {} @@ -190,6 +215,7 @@ public: }; info_data mk_type_info(unsigned c, expr const & e) { return info_data(new type_info_data(c, e)); } +info_data mk_extra_type_info(unsigned c, expr const & e, expr const & t) { return info_data(new extra_type_info_data(c, e, t)); } info_data mk_synth_info(unsigned c, expr const & e) { return info_data(new synth_info_data(c, e)); } info_data mk_overload_info(unsigned c, expr const & e) { return info_data(new overload_info_data(c, e)); } info_data mk_coercion_info(unsigned c, expr const & e, expr const & t) { return info_data(new coercion_info_data(c, e, t)); } @@ -264,6 +290,14 @@ struct info_manager::imp { m_line_data[l].insert(mk_type_info(c, e)); } + void add_extra_type_info(unsigned l, unsigned c, expr const & e, expr const & t) { + lock_guard lc(m_mutex); + if (m_block_new_info) + return; + synch_line(l); + m_line_data[l].insert(mk_extra_type_info(c, e, t)); + } + void add_synth_info(unsigned l, unsigned c, expr const & e) { lock_guard lc(m_mutex); if (m_block_new_info) @@ -538,6 +572,7 @@ struct info_manager::imp { info_manager::info_manager():m_ptr(new imp()) {} info_manager::~info_manager() {} void info_manager::add_type_info(unsigned l, unsigned c, expr const & e) { m_ptr->add_type_info(l, c, e); } +void info_manager::add_extra_type_info(unsigned l, unsigned c, expr const & e, expr const & t) { m_ptr->add_extra_type_info(l, c, e, t); } void info_manager::add_synth_info(unsigned l, unsigned c, expr const & e) { m_ptr->add_synth_info(l, c, e); } void info_manager::add_overload_info(unsigned l, unsigned c, expr const & e) { m_ptr->add_overload_info(l, c, e); } void info_manager::add_coercion_info(unsigned l, unsigned c, expr const & e, expr const & t) { m_ptr->add_coercion_info(l, c, e, t); } diff --git a/src/frontends/lean/info_manager.h b/src/frontends/lean/info_manager.h index 08b8e6e5f..2812d0a37 100644 --- a/src/frontends/lean/info_manager.h +++ b/src/frontends/lean/info_manager.h @@ -19,13 +19,16 @@ public: ~info_manager(); void add_type_info(unsigned l, unsigned c, expr const & e); + void add_extra_type_info(unsigned l, unsigned c, expr const & e, expr const & t); void add_synth_info(unsigned l, unsigned c, expr const & e); void add_overload_info(unsigned l, unsigned c, expr const & e); void add_coercion_info(unsigned l, unsigned c, expr const & e, expr const & t); void erase_coercion_info(unsigned l, unsigned c); void add_symbol_info(unsigned l, unsigned c, name const & n); void add_identifier_info(unsigned l, unsigned c, name const & full_id); + void instantiate(substitution const & s); + void merge(info_manager const & m, bool overwrite); void insert_line(unsigned l); void remove_line(unsigned l); diff --git a/src/frontends/lean/qinfo.cpp b/src/frontends/lean/qinfo.cpp new file mode 100644 index 000000000..b5a1a70d2 --- /dev/null +++ b/src/frontends/lean/qinfo.cpp @@ -0,0 +1,19 @@ +/* +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 "frontends/lean/qinfo.h" + +namespace lean { +name const & get_qinfo() { + static name g_qinfo("qinfo"); + static register_annotation_fn g_qinfo_annotation(g_qinfo); + return g_qinfo; +} +static name g_qinfo_name = get_qinfo(); // force 'qinfo' annotation to be registered + +expr mk_qinfo(expr const & e) { return mk_annotation(get_qinfo(), e); } +bool is_qinfo(expr const & e) { return is_annotation(e, get_qinfo()); } +} diff --git a/src/frontends/lean/qinfo.h b/src/frontends/lean/qinfo.h new file mode 100644 index 000000000..0996b814a --- /dev/null +++ b/src/frontends/lean/qinfo.h @@ -0,0 +1,17 @@ +/* +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 "library/annotation.h" + +namespace lean { +/** \brief Annotate \c e with "?" annotation. + It instructs elaborator to store the type of \c e. +*/ +expr mk_qinfo(expr const & e); +/** \brief Return true iff \c e is a term annotated with mk_qinfo */ +bool is_qinfo(expr const & e); +} diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 6cb3728bd..08d7aae7c 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -69,7 +69,7 @@ token_table init_token_table() { {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"have", 0}, {"show", 0}, {"obtain", 0}, {"by", 0}, {"then", 0}, {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec}, {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec}, {"Type'", g_max_prec}, - {"|", 0}, {"!", 0}, {"with", 0}, {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0}, + {"|", 0}, {"!", 0}, {"?", 0}, {"with", 0}, {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0}, {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec}, {"including", 0}, {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}};