monadic forgetting

Stream: general

[Patrick Massot]

What is the magic monadic combinator that would allow me to write a parser which throws away all the parsed tokens?

[Anne Baanen]

*> : m a -> m b -> m b?

[Rob Lewis]

What do you mean "throw away"? tk has type parser unit, it will consume a token and you don't have to do anything with it

[Patrick Massot]

I still want to return something, but it doesn't depend on the token.

[Patrick Massot]

The return type is an inductive with several constructors, and I want to choose one constructor depending on which token I see. But the constructor takes no argument.

[Anne Baanen]

*> would work, or <$: (mkX <$ token "x") <|> (mkY <$ token "y").

[Patrick Massot]

I think <$ is what I was missing.

[Patrick Massot]

I'm curious to know how you would do it with *>.

[Mario Carneiro]

you can use *> or <* depending on whether the thing you want to throw away is the left or right parser

[Anne Baanen]

a <$ mb is the same as pure a <* mb.

[Mario Carneiro]

for example tk "(" *> texpr <* tk ")" or thereabouts

[Patrick Massot]

Is there any way to end a tactic invocation with a token?

[Mario Carneiro]

what do you mean?

[Mario Carneiro]

are you writing a tactic or a parser?

[Patrick Massot]

both

[Patrick Massot]

Say I want to rewrite intro so that the syntax is now intro h bang, where bang is a token.

[Mario Carneiro]

def intro (h : parse texpr) (_ : parse (tk "bang")) : tactic unit

[Mario Carneiro]

or def intro (h : parse (texpr <* tk "bang")) : tactic unit

[Mario Carneiro]

However, keep in mind that this doesn't always work depending on the nature of the first parser, here texpr, because the parser monad does no backtracking

[Patrick Massot]

I'm sorry, I was interrupted. Thanks for you answer, I'll now try to process it.

[Patrick Massot]

I already noticed that no backtracking issue, it's quite annoying.

[Yakov Pechersky]

We can define a try parser, I'm surprised it wasn't defined in the core.

[Yakov Pechersky]

open parser parse_result

section try

variables {α : Type} {p : parser α}

def try (p : parser α) : parser α :=
λ cb n, match p cb n with
| (fail _ err) := fail n err
| ok := ok
end

@[simp] lemma try_of_done_iff {cb n n' a} :
  p.try cb n = done n' a ↔ p cb n = done n' a :=
by cases hp : p cb n; simp [hp, try]

@[simp] lemma try_of_fail_iff {cb n n' err} :
  p.try cb n = fail n' err ↔ n = n' ∧ ∃ np, p cb n = fail np err :=
by cases hp : p cb n; simp [hp, try]

lemma valid.try (h : p.valid) : p.try.valid :=
λ cb n, by { cases hp : p cb n; simpa [hp, try, parse_result.pos] using h cb n <|> simp [hp, try] }

@[simp] lemma mem_try_iff {a : α} : a ∈ p.try ↔ a ∈ p :=
by simp [mem_def]

end try

[Yakov Pechersky]

And here's a way to use it:

def p1 : parser ℕ := ch 'a' *> nat <* ch 'b'

def p2 : parser ℕ := ch 'a' *> nat <* ch 'c'

#eval run_string (p1 <|> p2) "a1c" -- fails: sum.inl "a1c\n  ^\n\nexpected: b\n"
#eval run_string (mfirst id [p1, p2]) "a1c" -- fails: equal to above
#eval run_string (mfirst try [p1, p2]) "a1c" -- succeeds: sum.inr 1

[Yakov Pechersky]

It fails in the first case because there is no backtracking after consuming that first a, so when the c is reached and p1 fails because it expects b, the orelse falls back to p2. However, orelse is defined for parsers to pass the position at the failure point, so p2 sees a b and expects an a, and fails too. Then, the whole orelse fails, and gives the failure message of the earlier (in terms of position) parser. That's why we only see the p1's error.

But if we wrap each one in try, then when p1 fails, we start parsing with p2 at the beginning of the buffer.

[Patrick Massot]

Oh thanks, this will probably help me clean up a lot of code. Up to now I was able to parse everything I wanted but I sort of simulate backtracking with unpleasant boilerplate.