feat(frontends/lean): add '?' for inspecting the type of any expression, it produces a EXTRA_TYPE info entry

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

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

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

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

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

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<unsigned>(k1) < static_cast<unsigned>(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<mutex> 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<mutex> 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); }

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

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

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

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