fix(library/init/lean/elaborator): check for and consume end of input

library/init/lean/elaborator.lean

@@ -220,6 +220,11 @@ def commands.elaborate (stop_on_end_cmd : bool) : ℕ → coelaborator
     else
       -- TODO(Sebastian): should recover
       error cmd "invalid 'end', there is no open scope to end"
+  | syntax.node ⟨module.eoi, _⟩ :=
+    if stop_on_end_cmd then
+      error cmd "invalid end of input, expected 'end'"
+    else
+      pure ()
   | syntax.node ⟨@«notation», _⟩ := do
     let nota := view «notation» cmd,
     if nota.local.is_some then do {
@@ -270,14 +275,12 @@ def elaborators : rbmap name coelaborator (<) := rbmap.from_list [
 protected def max_recursion := 100
 protected def max_commands := 10000
 
-protected def run (cfg : elaborator_config) : coroutine syntax elaborator_state unit :=
+protected def run (cfg : elaborator_config) : coroutine syntax elaborator_state message_log :=
 do
   let st := {elaborator_state . parser_cfg := cfg.initial_parser_cfg},
-  -- NOTE: ignores errors outside in the final output (should never happen) and the final state
-  except_t.run $ flip state_t.run st $ flip reader_t.run cfg $ rec_t.run
+  p ← except_t.run $ flip state_t.run st $ flip reader_t.run cfg $ rec_t.run
     (commands.elaborate ff elaborator.max_commands)
-    -- TODO(Sebastian): "out of fuel" error
-    (λ _, pure ())
+    (λ _, modify $ λ st, {st with messages := st.messages.add {filename := "foo", pos := ⟨1,0⟩, text := "elaborator.run: out of fuel"}})
     (λ _, do
       cmd ← current_command,
       -- TODO(Sebastian): throw error on unknown command when we get serious
@@ -286,7 +289,9 @@ do
       catch elab $ λ e,
         modify $ λ st, {st with messages := st.messages.add e})
     elaborator.max_recursion,
-  pure ()
+  match p with
+  | except.ok ((), st) := pure st.messages
+  | except.error e     := pure $ message_log.empty.add e
 
 end elaborator
 end lean

library/init/lean/parser/basic.lean

@@ -101,9 +101,8 @@ class has_view (r : ρ) (α : out_param Type) :=
 
 export has_view (view review)
 
-def try_view {α : Type} (k : syntax_node_kind) [has_view k α] : syntax → option α
-| stx@(syntax.node ⟨some k', _⟩) := if k.name = k'.name then some (has_view.view k stx) else none
-| _ := none
+def try_view {α : Type} (k : syntax_node_kind) [has_view k α] (stx : syntax) : option α :=
+if stx.is_of_kind k then some (has_view.view k stx) else none
 
 instance has_view.default (r : ρ) : inhabited (parser.has_view r syntax) :=
 ⟨{ view := id, review := id }⟩

library/init/lean/parser/module.lean

@@ -106,7 +106,7 @@ instance commands.tokens : parser.has_tokens commands.parser :=
 instance commands.parser.has_view : has_view commands.parser (list syntax) :=
 {..many.view command.parser}
 
-def eoi : syntax_node_kind := ⟨`lean.parser.eoi⟩
+@[pattern] def eoi : syntax_node_kind := ⟨`lean.parser.eoi⟩
 end module
 open module
 

library/init/lean/parser/syntax.lean

@@ -57,6 +57,10 @@ def substring.to_string (s : substring) : string :=
 namespace syntax
 open lean.format
 
+def is_of_kind (k : syntax_node_kind) : syntax → bool
+| (syntax.node ⟨some k', _⟩) := k.name = k'.name
+| _ := ff
+
 private def ident_to_format : syntax → format
 | stx := option.get_or_else (do
   syntax.node ⟨_, [syntax.node ⟨_, [syntax.node ⟨some ⟨idx⟩, part⟩]⟩, suffix]⟩ ← pure stx | failure,

library/init/lean/parser/term.lean

@@ -286,7 +286,7 @@ def builtin_leading_parsers : list term_parser := [
 
 @[derive parser.has_tokens parser.has_view]
 def sort_app.parser : trailing_term_parser :=
-do { l ← get_leading, guard (try_view sort l).is_some } *>
+do { l ← get_leading, guard $ l.is_of_kind sort } *>
 node! sort_app [fn: get_leading, arg: monad_lift (level.parser max_prec).run]
 
 @[derive parser.has_tokens parser.has_view]

tests/lean/parser1.lean

@@ -86,18 +86,16 @@ universes u v
   [header, nota, eoi] ← parse_module "infixl `+`:65 := nat.add" | throw "huh",
   except.ok cmd' ← pure $ (expand nota.cmd).run {filename := "init/core.lean"} | throw "heh",
   pure cmd'.reprint
-#exit
 
--- slowly progressing...
---set_option profiler true
-#eval (do {
-  s ← io.fs.read_file "../../library/init/core.lean",
-  let s := (s.mk_iterator.nextn 50000).prev_to_string,
+def run_frontend (input : string) : except_t string io unit := do
   parser_cfg ← monad_except.lift_except $ mk_config,
-  let parser_k := parser.run parser_cfg s (λ _, module.parser),
+  let parser_k := parser.run parser_cfg input (λ _, module.parser),
   let elab_k := elaborator.run {filename := "foo", initial_parser_cfg := parser_cfg},
   outs ← io.prim.iterate_eio (parser_k, elab_k, parser_cfg, ([] : list module_parser_output)) $ λ ⟨parser_k, elab_k, parser_cfg, outs⟩, match parser_k.resume parser_cfg with
-    | coroutine_result_core.done p := pure (sum.inr outs.reverse)
+    | coroutine_result_core.done p := do {
+      io.println "parser died!!",
+      pure (sum.inr outs.reverse)
+    }
     | coroutine_result_core.yielded out parser_k := do {
       match out.messages.to_list with
       | [] := pure () /-do
@@ -113,7 +111,12 @@ universes u v
       | except.ok cmd' := do {
         --io.println cmd',
         match elab_k.resume cmd' with
-        | coroutine_result_core.done p := io.println "elaborator died!!" *> pure (sum.inr outs.reverse)
+        | 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,
+          pure (sum.inr outs.reverse)
+        }
         | coroutine_result_core.yielded elab_out elab_k := do {
           elab_out.messages.to_list.mfor $ λ e, io.println e.text,
           pure (sum.inl (parser_k, elab_k, elab_out.parser_cfg, out :: outs))
@@ -121,9 +124,15 @@ universes u v
       }
       | except.error e := io.println e.text *> pure (sum.inl (parser_k, elab_k, parser_cfg, out :: outs))
     },
-  check_reprint outs s/-,
+  check_reprint outs input/-,
   let stx := syntax.node ⟨none, outs.map (λ r, r.cmd)⟩,
   let stx := stx.update_leading s,
   io.println "result:",
   io.println (to_string stx)-/
-} : except_t string io unit)
+#exit
+
+-- slowly progressing...
+set_option profiler true
+#eval do
+  s ← io.fs.read_file "../../library/init/core.lean",
+  run_frontend s