fix(frontends/lean): EXTRA_TYPE info

src/frontends/lean/builtin_exprs.cpp

@@ -376,7 +376,7 @@ static expr parse_sorry(parser & p, unsigned, expr const *, pos_info const & pos
 
 static expr parse_rparen(parser & p, unsigned, expr const * args, pos_info const & pos) {
     if (p.collecting_info())
-        return p.save_pos(mk_extra_info(args[0]), pos);
+        return p.save_pos(mk_extra_info(args[0], nulltag), pos);
     else
         return args[0];
 }

src/frontends/lean/extra_info.cpp

@@ -10,6 +10,7 @@ namespace lean {
 static name * g_extra_info = nullptr;
 name const & get_extra_info() { return *g_extra_info; }
 
+expr mk_extra_info(expr const & e, tag g) { return mk_annotation(get_extra_info(), e, g); }
 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

@@ -11,6 +11,7 @@ namespace lean {
 /** \brief Annotate \c e with "extra-info" annotation.
     It instructs elaborator to store the type of \c e.
 */
+expr mk_extra_info(expr const & e, tag g);
 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/library/annotation.cpp

@@ -58,16 +58,20 @@ void register_annotation(name const & n) {
     ms.insert(mk_pair(n, macro_definition(new annotation_macro_definition_cell(n))));
 }
 
-expr mk_annotation(name const & kind, expr const & e) {
+expr mk_annotation(name const & kind, expr const & e, tag g) {
     annotation_macros & ms = get_annotation_macros();
     auto it = ms.find(kind);
     if (it != ms.end()) {
-        return copy_tag(e, mk_macro(it->second, 1, &e));
+        return mk_macro(it->second, 1, &e, g);
     } else {
         throw exception(sstream() << "unknown annotation kind '" << kind << "'");
     }
 }
 
+expr mk_annotation(name const & kind, expr const & e) {
+    return mk_annotation(kind, e, e.get_tag());
+}
+
 bool is_annotation(expr const & e) {
     return is_macro(e) && macro_def(e).get_name() == get_annotation_name();
 }

src/library/annotation.h

@@ -20,6 +20,7 @@ void register_annotation(name const & n);
 
     \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, tag g);
 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);

tests/lean/interactive/extra_type.input

@@ -0,0 +1,27 @@
+VISIT extra_type.lean
+SET
+pp.notation false
+SYNC 20
+import general_notation
+import logic.connectives logic.decidable logic.inhabited
+
+open eq eq.ops decidable
+
+inductive bool : Type :=
+  ff : bool,
+  tt : bool
+namespace bool
+  protected definition rec_on {C : bool → Type} (b : bool) (H₁ : C ff) (H₂ : C tt) : C b :=
+  rec H₁ H₂ b
+
+  protected definition cases_on {p : bool → Prop} (b : bool) (H₁ : p ff) (H₂ : p tt) : p b :=
+  rec H₁ H₂ b
+
+  definition cond {A : Type} (b : bool) (t e : A) :=
+  rec_on b e t
+
+  theorem dichotomy (b : bool) : b = ff ∨ b = tt :=
+  cases_on b (or.inl rfl) (or.inr rfl)
+end bool
+WAIT
+INFO 20 13

tests/lean/interactive/extra_type.input.expected.out

@@ -0,0 +1,15 @@
+-- BEGINSET
+-- ENDSET
+-- ERROR unexpected command line: end bool
+-- BEGINWAIT
+-- ENDWAIT
+-- BEGININFO
+-- EXTRA_TYPE|20|13
+or.inl rfl
+--
+or (eq ff ff) (eq ff tt)
+-- ACK
+-- SYMBOL|20|13
+(
+-- ACK
+-- ENDINFO