diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean index 9f93853e23..f90b548d0b 100644 --- a/library/init/lean/elaborator.lean +++ b/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 diff --git a/library/init/lean/expander.lean b/library/init/lean/expander.lean index 7370c3e0eb..8b2fa1e0fb 100644 --- a/library/init/lean/expander.lean +++ b/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 := diff --git a/library/init/lean/message.lean b/library/init/lean/message.lean index 7d366da95a..fca132fce0 100644 --- a/library/init/lean/message.lean +++ b/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) diff --git a/library/init/lean/parser/basic.lean b/library/init/lean/parser/basic.lean index ea5bc1e6dc..3b3423e0f4 100644 --- a/library/init/lean/parser/basic.lean +++ b/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) α) : diff --git a/library/init/lean/parser/parsec.lean b/library/init/lean/parser/parsec.lean index 63a979000f..ec8be30e47 100644 --- a/library/init/lean/parser/parsec.lean +++ b/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⟩ diff --git a/tests/lean/parser1.lean b/tests/lean/parser1.lean index 0ec070a9df..29400d59f7 100644 --- a/tests/lean/parser1.lean +++ b/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 := "", tokens := t, + filename := "", 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 := "", 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 := "", 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)⟩, diff --git a/tests/lean/parser1.lean.expected.out b/tests/lean/parser1.lean.expected.out index a24851ab34..a6ff99711f 100644 --- a/tests/lean/parser1.lean.expected.out +++ b/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 +:1:0: error: expected command partial syntax tree: [(module.header [] []) (module.eoi "")] -error at line 1, column 6: -unexpected end of input +: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 +: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 +:1:5: error: expected identifier +:1:9: error: unexpected end of input expected identifier partial syntax tree: [(module.header [] []) (command.open "open" [ ]) (command.open "open" [ ]) (module.eoi "")] -error at line 1, column 8: -expected command +:1:8: error: expected command partial syntax tree: [(module.header [] []) (command.open "open" [(command.open_spec `me [] [] [] [])])