parser should fail

Stream: metaprogramming / tactics

[Joe Palermo]

Hi all,

The following parsing script is succeeding on cases I would prefer it to fail on. For example in the case λ {α : Type u} [_inst_1 : linear_ordered_add_comm_group α], @with_top.linear_ordered_add_comm_monoid_with_top α), there is an extra ")" at the very end which has no opening parenthesis to match it. This proof term successfully parses and type checks because the final ")" is just ignored.

How can I force the parser to consume the whole string, and fail if the whole string can't be parsed?

import system.io
import all

meta def parse_texpr_with_univs (univs : list string): lean.parser pexpr := do
  -- add all universe names in the list as universe levels
  univs.mmap $ (λ s, lean.parser.add_local_level s),
  -- parse the buffer as a pexpr
  interactive.types.texpr

meta def main : io unit := do
  let s := "λ {α : Type u} [_inst_1 : linear_ordered_add_comm_group α], @with_top.linear_ordered_add_comm_monoid_with_top α)",
  let univs := ["u"],

  io.run_tactic $ do {
    -- parse the expression using the universe names
    t <- lean.parser.run_with_input (parse_texpr_with_univs univs) s,

    -- convert to proof term and check type
    e <- tactic.to_expr t,
    tp <- tactic.infer_type e,
    tactic.trace tp
  }

Thanks!

[Eric Wieser]

I think using run (with_input p s) instead of run_with_input will solve your problem

[Eric Wieser]

src#lean.parser.run_with_input just calls what I suggest, then throws away the information about the remaining input

[Eric Wieser]

Since run_with_input is used nowhere in core lean or mathlib, perhaps the thing to do is just change run_with_input to perform the necessary check

[Eric Wieser]

This does the job:

meta def run_with_input' {α} : parser α → string → tactic α := λ p s,
do
  (p, "") ← run (with_input p s),
  pure p

although you probably want it to emit a better error about the remaining content rather than just failing a pattern match

[Joe Palermo]

Ahh great! Thank you @Eric Wieser

[Joe Palermo]

I tested it and it works, but I don't understand why this works. On the surface it appears that the only difference between run_with_input and run_with_input' is how the result is retrieved.

meta def run_with_input {α} : parser α → string → tactic α := λ p s,
  prod.fst <$> run (with_input p s)

meta def run_with_input' {α} : parser α → string → tactic α := λ p s,
do
  (p, "") ← run (with_input p s),
  pure p

[Mario Carneiro]

I think the intended use is to call run_with_input with a parser chain that ends with the eof parser

[Eric Wieser]

(p, "") ← ... means "call failure if the second item is not """

[Eric Wieser]

I wasn't able to find the eof parser. docs#lean.parser.eof doesn't exist.

[Eric Wieser]

We have docs#parser.eof, but isn't that a very different parser?