feat(kernel/pos_info_provider): add support for file names in pos_info_provider

The idea is to include the file name when displaying justification objects.

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

src/frontends/lean/parser_error.cpp

@@ -66,6 +66,10 @@ std::pair<unsigned, unsigned> parser_imp::lean_pos_info_provider::get_pos_info(e
     return it->second;
 }
 
+char const * parser_imp::lean_pos_info_provider::get_file_name(expr const & ) const {
+    return m_ref.m_strm_name.c_str();
+}
+
 void parser_imp::display_error(elaborator_exception const & ex) {
     formatter fmt = m_io_state.get_formatter();
     options opts  = m_io_state.get_options();

src/frontends/lean/parser_imp.h

@@ -211,6 +211,7 @@ private:
         parser_imp const & m_ref;
         lean_pos_info_provider(parser_imp const & r):m_ref(r) {}
         virtual std::pair<unsigned, unsigned> get_pos_info(expr const & e) const;
+        virtual char const * get_file_name(expr const & e) const;
     };
 
     void display_error(elaborator_exception const & ex);

src/kernel/pos_info_provider.cpp

@@ -7,10 +7,13 @@ Author: Leonardo de Moura
 #include "kernel/pos_info_provider.h"
 
 namespace lean {
+char const * pos_info_provider::get_file_name(expr const & ) const {
+    return "unknown";
+}
 format pos_info_provider::pp(expr const & e) const {
     try {
         auto p = get_pos_info(e);
-        return paren(format{format("line"), colon(), space(), format(p.first), colon(), space(), format("pos"), colon(), space(), format(p.second)});
+        return format{format(get_file_name(e)), colon(), format(p.first), colon(), format(p.second), colon()};
     } catch (exception &) {
         return format();
     }

src/kernel/pos_info_provider.h

@@ -20,6 +20,7 @@ public:
        Throws an exception if the given expression does not have this kind of information associated with it.
     */
     virtual std::pair<unsigned, unsigned> get_pos_info(expr const & e) const = 0;
+    virtual char const * get_file_name(expr const & e) const;
     unsigned get_line(expr const & e) const { return get_pos_info(e).first; }
     unsigned get_pos(expr const & e) const { return get_pos_info(e).second; }
     /**

tests/lean/bug.lean.expected.out

@@ -2,7 +2,7 @@
   Set: pp::unicode
 Failed to solve
 A : (Type U), A' : (Type U), H : A == A' ⊢ ?M::3 ≺ TypeU
-    (line: 1: pos: 44) Type of argument 1 must be convertible to the expected type in the application of
+    bug.lean:1:44: Type of argument 1 must be convertible to the expected type in the application of
         @symm
     with arguments:
         ?M::0

tests/lean/elab1.lean.expected.out

@@ -3,7 +3,7 @@
   Assumed: f
 Failed to solve
  ⊢ Bool ≺ ℕ
-    (line: 2: pos: 6) Type of argument 3 must be convertible to the expected type in the application of
+    elab1.lean:2:6: Type of argument 3 must be convertible to the expected type in the application of
         @f
     with arguments:
         ℕ
@@ -15,7 +15,7 @@ Type
   Assumed: h
 Failed to solve
 x : ?M::0, A : Type ⊢ ?M::0 ≺ A
-    (line: 9: pos: 27) Type of argument 2 must be convertible to the expected type in the application of
+    elab1.lean:9:27: Type of argument 2 must be convertible to the expected type in the application of
         h
     with arguments:
         A
@@ -23,7 +23,7 @@ x : ?M::0, A : Type ⊢ ?M::0 ≺ A
   Assumed: my_eq
 Failed to solve
 A : Type, B : Type, a : ?M::0, b : ?M::1, C : Type ⊢ ?M::0[lift:0:3] ≺ C
-    (line: 13: pos: 51) Type of argument 2 must be convertible to the expected type in the application of
+    elab1.lean:13:51: Type of argument 2 must be convertible to the expected type in the application of
         my_eq
     with arguments:
         C
@@ -34,10 +34,10 @@ A : Type, B : Type, a : ?M::0, b : ?M::1, C : Type ⊢ ?M::0[lift:0:3] ≺ C
   Assumed: H
 Failed to solve
  ⊢ ∀ H1 : ?M::0, ?M::1 ∧ a ≺ b
-    (line: 18: pos: 18) Type of definition 't1' must be convertible to expected type.
+    elab1.lean:18:18: Type of definition 't1' must be convertible to expected type.
 Failed to solve
  ⊢ b == b ≺ a == b
-    (line: 20: pos: 22) Type of argument 6 must be convertible to the expected type in the application of
+    elab1.lean:20:22: Type of argument 6 must be convertible to the expected type in the application of
         @trans
     with arguments:
         ?M::1
@@ -48,7 +48,7 @@ Failed to solve
         refl b
 Failed to solve
  ⊢ ?M::1 ≺ Type
-    (line: 22: pos: 6) Type of argument 1 must be convertible to the expected type in the application of
+    elab1.lean:22:6: Type of argument 1 must be convertible to the expected type in the application of
         @f
     with arguments:
         ?M::0

tests/lean/ex3.lean.expected.out

@@ -6,7 +6,7 @@ myeq Bool ⊤ ⊥
   Assumed: a
 Failed to solve
  ⊢ Bool ≺ T
-    (line: 5: pos: 6) Type of argument 2 must be convertible to the expected type in the application of
+    ex3.lean:5:6: Type of argument 2 must be convertible to the expected type in the application of
         myeq
     with arguments:
         T
@@ -16,7 +16,7 @@ Failed to solve
   Set: lean::pp::implicit
 Failed to solve
  ⊢ Bool ≺ T
-    (line: 9: pos: 11) Type of argument 2 must be convertible to the expected type in the application of
+    ex3.lean:9:11: Type of argument 2 must be convertible to the expected type in the application of
         @myeq2
     with arguments:
         T

tests/lean/induction2.lean.expected.out

@@ -5,7 +5,7 @@
   Assumed: Induction
 Failed to solve
  ⊢ ∀ m : ℕ, 0 + m == m + 0 ≺ ?M::3 0
-    (line: 10: pos: 3) Type of argument 2 must be convertible to the expected type in the application of
+    induction2.lean:10:3: Type of argument 2 must be convertible to the expected type in the application of
         Induction
     with arguments:
         ?M::3

tests/lean/overload2.lean.expected.out

@@ -4,25 +4,25 @@
   Imported 'Real'
 Failed to solve
  ⊢ (?M::0 ≈ Nat::add) ⊕ (?M::0 ≈ Int::add) ⊕ (?M::0 ≈ Real::add)
-    (line: 3: pos: 8) Overloading at
+    overload2.lean:3:8: Overloading at
         (Real::add | Int::add | Nat::add) 1 ⊤
     Failed to solve
      ⊢ Bool ≺ ℕ
-        (line: 3: pos: 8) Type of argument 2 must be convertible to the expected type in the application of
+        overload2.lean:3:8: Type of argument 2 must be convertible to the expected type in the application of
             Nat::add
         with arguments:
             1
             ⊤
     Failed to solve
      ⊢ Bool ≺ ℤ
-        (line: 3: pos: 8) Type of argument 2 must be convertible to the expected type in the application of
+        overload2.lean:3:8: Type of argument 2 must be convertible to the expected type in the application of
             Int::add
         with arguments:
             1
             ⊤
     Failed to solve
      ⊢ Bool ≺ ℝ
-        (line: 3: pos: 8) Type of argument 2 must be convertible to the expected type in the application of
+        overload2.lean:3:8: Type of argument 2 must be convertible to the expected type in the application of
             Real::add
         with arguments:
             1

tests/lean/tst7.lean.expected.out

@@ -4,7 +4,7 @@
 λ (A B : Type) (a : B), f B a
 Failed to solve
 A : Type, a : ?M::0, B : Type ⊢ ?M::0[lift:0:2] ≺ B
-    (line: 4: pos: 42) Type of argument 2 must be convertible to the expected type in the application of
+    tst7.lean:4:42: Type of argument 2 must be convertible to the expected type in the application of
         f
     with arguments:
         B