feat(frontends/lean): associate type information with left '('

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

src/emacs/lean-syntax.el

@@ -80,8 +80,6 @@
       . 'font-lock-constant-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 qinfo.cpp)
+structure_cmd.cpp info_manager.cpp noinfo.cpp extra_info.cpp)
 
 target_link_libraries(lean_frontend ${LEAN_LIBS})

src/frontends/lean/builtin_exprs.cpp

@@ -19,7 +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/extra_info.h"
 #include "frontends/lean/util.h"
 
 namespace lean {
@@ -363,10 +363,8 @@ 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;
+static expr parse_rparen(parser & p, unsigned, expr const * args, pos_info const & pos) {
+    return p.save_pos(mk_extra_info(args[0]), pos);
 }
 
 parse_table init_nud_table() {
@@ -374,15 +372,13 @@ parse_table init_nud_table() {
     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);
     r = r.add({transition("have", mk_ext_action(parse_have))}, x0);
     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("(", Expr), transition(")", mk_ext_action(parse_rparen))}, 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,7 +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"
+#include "frontends/lean/extra_info.h"
 
 #ifndef LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES
 #define LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES true
@@ -1198,7 +1198,7 @@ public:
         }
     }
 
-    expr visit_qinfo(expr const & e, constraint_seq & cs) {
+    expr visit_extra_info(expr const & e, constraint_seq & cs) {
         auto ecs = visit(get_annotation_arg(e));
         cs += ecs.second;
         save_extra_type_data(e, ecs.first);
@@ -1219,8 +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 if (is_extra_info(e)) {
+            return visit_extra_info(e, cs);
         } else {
             switch (e.kind()) {
             case expr_kind::Local:      return e;

src/frontends/lean/extra_info.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/extra_info.h"
+
+namespace lean {
+name const & get_extra_info() {
+    static name g_extra_info("extra_info");
+    static register_annotation_fn g_extra_info_annotation(g_extra_info);
+    return g_extra_info;
+}
+static name g_extra_info_name = get_extra_info(); // force 'extra_info' annotation to be registered
+
+expr mk_extra_info(expr const & e) { return mk_annotation(get_extra_info(), e); }
+bool is_extra_info(expr const & e) { return is_annotation(e, get_extra_info()); }
+}

src/frontends/lean/extra_info.h

@@ -8,10 +8,10 @@ Author: Leonardo de Moura
 #include "library/annotation.h"
 
 namespace lean {
-/** \brief Annotate \c e with "?" annotation.
+/** \brief Annotate \c e with "extra-info" 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);
+expr mk_extra_info(expr const & e);
+/** \brief Return true iff \c e is a term annotated with mk_extra_info */
+bool is_extra_info(expr const & e);
 }

src/frontends/lean/qinfo.cpp

@@ -1,19 +0,0 @@
-/*
-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/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}, {"using", 0},
-         {"|", 0}, {"!", 0}, {"?", 0}, {"with", 0}, {"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"::", 0}, {"calc", 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}};