error tolerant string parsing

Stream: metaprogramming / tactics

[Joe Palermo]

What I'm really trying to do is rewrite the following code to be error tolerant. Some strings in my input will fail to parse and currently if any string fails to parse the whole tactic fails.

import system.io
import data.list
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 parse_string (univs : list string) (proof : string) : tactic pexpr := lean.parser.run_with_input (parse_texpr_with_univs univs) proof

meta def process (proofs : list string) : tactic unit := do {
    let univs := ["u_1001", "u_1002", "u_1003", "u_1004", "u_1005", "u_1006"],
    pexprs <- proofs.traverse (parse_string univs),
    exprs <- pexprs.traverse tactic.to_expr,
    theorems <- exprs.traverse tactic.infer_type,
    tactic.trace theorems.length,
    tactic.trace theorems
  }

meta def main : io unit := do {
    let proofs :=
    ["this one should fail",
    "λ {α : Sort u_1001} {β : Sort u_1002} {f : α → β} {g : β → α} (h : @function.right_inverse.{u_1002 u_1001} β α f g),
    @funext.{u_1001 u_1001} α (λ (x : α), α) (@function.comp.{u_1001 u_1002 u_1001} α β α g f) (@id.{u_1001} α) h"],
    io.run_tactic $ process proofs
}

An idea I came up with was to rewrite traverse to take a second function that filters out strings that don't parse.

def traverse' {F : Type u → Type v} [applicative F] {α β : Type*} (f : α → F β) (g : (α → F β) → α → bool):
  list α → F (list β)
| [] := pure []
| (x :: xs) := if g f x then list.cons <$> f x <*> traverse' xs else traverse' xs

Hence why I'm trying to write that function can_parse above. However, I suspect there is a better way...

[Miroslav Olšák]

Well, the tactic monad is more than maybe, so I guess having a tactic success checker would be complicated (I am not sure if Lean can be "hacked" to do that).

[Miroslav Olšák]

On the other hand, if you just want to filter out errors, you don't need purely functional code, do you?

[Miroslav Olšák]

Is this what you essentially want?

meta def mmap_valid {α β : Type} (f : α → tactic β) (l : list α) : tactic (list β)
:= do
  res ← list.mmap (λ x, (do y ← f x, return (some y)) <|> return none) l,
  return (list.filter_map id res)

[Miroslav Olšák]

That should be a function which works like list.mmap, never fails, and skips elements on which f fails.

[Miroslav Olšák]

By the way, the same written with monadic symbols instead of do.

meta def mmap_valid {α β : Type} (f : α → tactic β) (l : list α) : tactic (list β)
:= list.filter_map id <$> list.mmap (λ x, (some <$> f x) <|> return none) l

[Joe Palermo]

@Miroslav Olšák That's exactly what I needed. Thanks!

[Yakov Pechersky]

docs#tactic.successes

[Yakov Pechersky]

or docs#try_all depending on if you need to keep or reset the state

[Yakov Pechersky]

This is for interactive tactics, might work for you still

[Yakov Pechersky]

And of course, docs#tactic.try and docs#tactic.try_core

[Miroslav Olšák]

:smile: I expected there would be library functions for this, I just don't know how to search for them.

[Kevin Buzzard]

#Is there code for X? + well-chosen thread title