feat(library/init/lean): compute and show error positions

library/init/lean/elaborator.lean

@@ -640,7 +640,7 @@ protected def run (cfg : elaborator_config) : coroutine syntax elaborator_state
 do
   let st := {elaborator_state .
     parser_cfg := cfg.initial_parser_cfg,
-    expander_cfg := {filename := cfg.filename, transformers := expander.builtin_transformers},
+    expander_cfg := {transformers := expander.builtin_transformers, ..cfg},
     ngen := ⟨`fixme, 0⟩,
     options := options.mk},
   p ← except_t.run $ flip state_t.run st $ flip reader_t.run cfg $ rec_t.run

library/init/lean/expander.lean

@@ -40,8 +40,10 @@ def error {m : Type → Type} {ρ : Type} [monad m] [monad_reader ρ m] [has_lif
   [monad_except message m] {α : Type}
   (context : syntax) (text : string) : m α :=
 do cfg ← read,
-   -- TODO(Sebastian): convert position
-   throw {filename := frontend_config.filename ↑cfg, pos := /-context.get_pos.get_or_else-/ ⟨1,0⟩, text := text}
+   let pos : position := match context.get_pos with
+   | some pos := let (line, col) := (frontend_config.input ↑cfg).line_column pos in ⟨line, col⟩
+   | none     := ⟨1, 0⟩,
+   throw {filename := frontend_config.filename ↑cfg, pos := pos, text := text}
 
 /-- Coercion useful for introducing macro-local variables. Use `glob_id` to refer to global bindings instead. -/
 instance coe_name_ident : has_coe name syntax_ident :=

library/init/lean/message.lean

@@ -6,7 +6,7 @@ Author: Sebastian Ullrich
 Message type used by the Lean frontend
 -/
 prelude
-import init.data.string.basic
+import init.data.to_string
 
 namespace lean
 structure position :=
@@ -15,6 +15,7 @@ structure position :=
 inductive message_severity
 | information | warning | error
 
+-- TODO: structured messages
 structure message :=
 (filename : string)
 (pos      : position)
@@ -23,6 +24,20 @@ structure message :=
 (caption  : string           := "")
 (text     : string)
 
+namespace message
+protected def to_string (msg : message) : string :=
+msg.filename ++ ":" ++ to_string msg.pos.line ++ ":" ++ to_string msg.pos.column ++ ": " ++
+(match msg.severity with
+ | message_severity.information := ""
+ | message_severity.warning := "warning: "
+ | message_severity.error := "error: ") ++
+(if msg.caption = "" then "" else msg.caption ++ ":\n") ++
+msg.text
+
+instance : has_to_string message :=
+⟨message.to_string⟩
+end message
+
 structure message_log :=
 -- messages are stored in reverse for efficient append
 (rev_list : list message)

library/init/lean/parser/basic.lean

@@ -59,6 +59,7 @@ structure parser_cache :=
 
 structure frontend_config :=
 (filename : string)
+(input    : string)
 
 /- Remark: if we have a node in the trie with `some token_config`, the string induced by the path is equal to the `token_config.prefix`. -/
 structure parser_config extends frontend_config :=
@@ -121,8 +122,8 @@ instance has_view.default (r : ρ) : inhabited (parser.has_view syntax r) :=
 class has_view_default (r : ρ) (α : out_param Type) [has_view α r] (default : α) := mk {}
 
 def message_of_parsec_message {μ : Type} (cfg : frontend_config) (msg : parsec.message μ) : message :=
--- FIXME: translate position
-{filename := cfg.filename, pos := ⟨0, 0⟩, text := to_string msg}
+let (line, col) := msg.it.to_string.line_column msg.it.offset in
+{filename := cfg.filename, pos := ⟨line, col⟩, text := msg.text}
 
 /-- Run parser stack, returning a partial syntax tree in case of a fatal error -/
 protected def run {m : Type → Type} {α ρ : Type} [monad m] [has_coe_t ρ frontend_config] (cfg : ρ) (s : string) (r : state_t parser_state (parser_t ρ m) α) :

library/init/lean/parser/parsec.lean

@@ -30,14 +30,17 @@ def expected.to_string : list string → string
 | [e1, e2] := e1 ++ " or " ++ e2
 | (e::es)  := e ++ ", " ++ expected.to_string es
 
-protected def message.to_string {μ : Type} (msg : message μ) : string :=
-let (line, col) := msg.it.to_string.line_column msg.it.offset in
--- always print ":"; we assume at least one of `unexpected` and `expected` to be non-empty
-let loc := ["error at line " ++ to_string line ++ ", column " ++ to_string col ++ ":"] in
+def message.text {μ : Type} (msg : message μ) : string :=
 let unexpected := (if msg.unexpected = "" then [] else ["unexpected " ++ msg.unexpected]) in
 let ex_list := msg.expected.to_list in
 let expected := if ex_list = [] then [] else ["expected " ++ expected.to_string ex_list] in
-"\n".intercalate $ loc ++ unexpected ++ expected
+"\n".intercalate $ unexpected ++ expected
+
+
+protected def message.to_string {μ : Type} (msg : message μ) : string :=
+let (line, col) := msg.it.to_string.line_column msg.it.offset in
+-- always print ":"; we assume at least one of `unexpected` and `expected` to be non-empty
+"error at line " ++ to_string line ++ ", column " ++ to_string col ++ ":\n" ++ msg.text
 
 instance {μ : Type} : has_to_string (message μ) :=
 ⟨message.to_string⟩

tests/lean/parser1.lean

@@ -22,7 +22,7 @@ match msgs with
   io.println "result:",
   io.println (to_string stx)
 | msgs := do
-  msgs.mfor $ λ e, io.println e.text,
+  msgs.mfor $ λ e, io.println e.to_string,
   io.println "partial syntax tree:",
   io.println (to_string stx)
 
@@ -33,7 +33,7 @@ do t ← parser.mk_token_trie $
     parser.tokens term.builtin_leading_parsers ++
     parser.tokens term.builtin_trailing_parsers,
    pure $ {
-     filename := "<unknown>", tokens := t,
+     filename := "<unknown>", input := "", tokens := t,
      command_parsers := command.builtin_command_parsers,
      leading_term_parsers := term.builtin_leading_parsers,
      trailing_term_parsers := term.builtin_trailing_parsers,
@@ -84,7 +84,7 @@ universes u v
 
 #eval do
   [header, nota, eoi] ← parse_module "infixl `+`:65 := nat.add" | throw "huh",
-  except.ok cmd' ← pure $ (expand nota.cmd).run {filename := "init/core.lean", transformers := builtin_transformers} | throw "heh",
+  except.ok cmd' ← pure $ (expand nota.cmd).run {filename := "foo", input := "", transformers := builtin_transformers} | throw "heh",
   pure cmd'.reprint
 
 -- for structuring the profiler output
@@ -94,9 +94,9 @@ universes u v
 
 def run_frontend (input : string) : except_t string io unit := do
   parser_cfg ← monad_except.lift_except $ mk_config,
-  let expander_cfg : expander_config := {filename := "foo", transformers := builtin_transformers},
+  let expander_cfg : expander_config := {filename := "<stdin>", input := input, transformers := builtin_transformers},
   let parser_k := parser.run parser_cfg input (λ st _, module.parser st),
-  let elab_k := elaborator.run {filename := "foo", initial_parser_cfg := parser_cfg},
+  let elab_k := elaborator.run {filename := "<stdin>", input := input, initial_parser_cfg := parser_cfg},
   outs ← io.prim.iterate_eio (parser_k, elab_k, parser_cfg, expander_cfg, ([] : list module_parser_output)) $ λ ⟨parser_k, elab_k, parser_cfg, expander_cfg, outs⟩, match run_parser parser_k.resume parser_cfg with
     | coroutine_result_core.done p := do {
       io.println "parser died!!",
@@ -108,7 +108,7 @@ def run_frontend (input : string) : except_t string io unit := do
         io.println "result:",
         io.println (to_string stx)-/
       | msgs := do {
-        msgs.mfor $ λ e, io.println e.text/-,
+        msgs.mfor $ λ e, io.println e.to_string/-,
         io.println "partial syntax tree:",
         io.println (to_string out.cmd)-/
       },
@@ -120,17 +120,17 @@ def run_frontend (input : string) : except_t string io unit := do
         | coroutine_result_core.done msgs := do {
           when ¬(cmd'.is_of_kind module.eoi) $
             io.println "elaborator died!!",
-          msgs.to_list.mfor $ λ e, io.println e.text,
+          msgs.to_list.mfor $ λ e, io.println e.to_string,
           io.println $ "parser cache hit rate: " ++ to_string out.cache.hit ++ "/" ++
             to_string (out.cache.hit + out.cache.miss),
           pure $ sum.inr (out::outs).reverse
         }
         | coroutine_result_core.yielded elab_out elab_k := do {
-          elab_out.messages.to_list.mfor $ λ e, io.println e.text,
+          elab_out.messages.to_list.mfor $ λ e, io.println e.to_string,
           pure (sum.inl (parser_k, elab_k, elab_out.parser_cfg, elab_out.expander_cfg, out :: outs))
         }
       }
-      | except.error e := io.println e.text *> pure (sum.inl (parser_k, elab_k, parser_cfg, expander_cfg, out :: outs))
+      | except.error e := io.println e.to_string *> pure (sum.inl (parser_k, elab_k, parser_cfg, expander_cfg, out :: outs))
     },
   check_reprint outs input/-,
   let stx := syntax.node ⟨none, outs.map (λ r, r.cmd)⟩,

tests/lean/parser1.lean.expected.out

@@ -3,12 +3,10 @@ result:
 result:
 [(module.header [] [(module.import "import" [(module.import_path [] `me)])])
  (module.eoi "")]
-error at line 1, column 0:
-expected command
+<unknown>:1:0: error: expected command
 partial syntax tree:
 [(module.header [] []) (module.eoi "")]
-error at line 1, column 6:
-unexpected end of input
+<unknown>:1:6: error: unexpected end of input
 expected "." or identifier
 partial syntax tree:
 [(module.header
@@ -45,26 +43,22 @@ result:
       ")")]
     [(command.open_spec.hiding "(" "hiding" [`a `b] ")")])])
  (module.eoi "")]
-error at line 1, column 11:
-expected command
+<unknown>:1:11: error: expected command
 partial syntax tree:
 [(module.header [] [])
  (command.open
   "open"
   [(command.open_spec `me [] [] [] []) (command.open_spec `you [] [] [] [])])
  (module.eoi "")]
-error at line 1, column 5:
-expected identifier
-error at line 1, column 9:
-unexpected end of input
+<unknown>:1:5: error: expected identifier
+<unknown>:1:9: error: unexpected end of input
 expected identifier
 partial syntax tree:
 [(module.header [] [])
  (command.open "open" [<missing> <missing>])
  (command.open "open" [<missing> <missing>])
  (module.eoi "")]
-error at line 1, column 8:
-expected command
+<unknown>:1:8: error: expected command
 partial syntax tree:
 [(module.header [] [])
  (command.open "open" [(command.open_spec `me [] [] [] [])])