Expressing parsing

Stream: metaprogramming / tactics

[Patrick Massot]

Do we have a nice way to parse an expression analogous to how we parse tactic arguments? Or are we meant to use nested matches on the expr constructors?

[Patrick Massot]

I have about a dozen shapes of expressions I'd like to recognize and be able to act depending on which shape was recognized and what were the components.

[Patrick Massot]

For instance if I have ∀ k, ∃ n, P n k as input then I would like to get : this is forall_exists_prop with components k, n, P.

[Mario Carneiro]

You can use expr match for a lot of these use cases, but binders can be tricky

[Patrick Massot]

Thanks. I managed to do something. I won't claim there wasn't times where I simply tried all matched arguments in order until I found the one that worked...

[Patrick Massot]

If you don't feel like doing more important or entertaining things then you can have a look at:

import tactic.basic

meta def rel_symb : expr → tactic (expr × expr × string)
| `(%%x < %%y) := pure (x, y, " < ")
| `(%%x ≤ %%y) := pure (x, y, " ≤ ")
| `(%%x > %%y) := pure (x, y, " > ")
| `(%%x ≥ %%y) := pure (x, y, " ≥ ")
| `(%%x ∈ %%y) := pure (x, y, " ∈ ")
| e := do pe ← tactic.pp e, tactic.fail $ "Not a relation: " ++ pe.to_string


meta inductive my_expr
| forall_rel (var_name : name) (typ : expr) (rel : string) (rel_rhs : expr) (propo : my_expr) : my_expr
| forall_simple (var_name : name) (typ : expr) (propo : my_expr) : my_expr
| exist_rel (var_name : name) (typ : expr) (rel : string) (rel_rhs : expr) (propo : my_expr) : my_expr
| exist_simple (var_name : name) (typ : expr) (propo : my_expr) : my_expr
| impl (lhs : expr) (rhs : expr) : my_expr
| prop (e : expr) : my_expr
| data (e : expr) : my_expr

namespace my_expr

meta def tofmt : my_expr →  tactic format
| (forall_rel var_name typ rel rel_rhs propo) := do
    rhs ← tactic.pp rel_rhs,
    p ← tofmt propo,
    pure $ "forall_rel " ++ var_name.to_string ++ rel ++ rhs.to_string ++ ", " ++ p
| (forall_simple var_name typ propo) := do
    p ← tofmt propo,
    pure $ "forall_simple " ++ var_name.to_string ++ ", " ++ p
| (exist_rel var_name typ rel rel_rhs propo) := do
    rhs ← tactic.pp rel_rhs,
    p ← tofmt propo,
    pure $ "exist_rel " ++ var_name.to_string ++ rel ++ rhs.to_string ++ ", " ++ p
| (exist_simple var_name typ propo) := do
    p ← tofmt propo,
    pure $ "exist_simple " ++ var_name.to_string ++ ", " ++ p
| (impl lhs rhs) := do
  l ← tactic.pp lhs,
  r ← tactic.pp rhs,
  pure $ "impl " ++ l ++ " ⇒ " ++ r
| (prop e) := do p ← tactic.pp e, pure $ "prop: " ++ p
| (data e) := do p ← tactic.pp e, pure $ "data: " ++ p


meta instance : has_to_tactic_format my_expr :=
⟨my_expr.tofmt⟩

meta def parse : expr → tactic my_expr
| e@(expr.pi n _ t b) := match b with
    | e'@(expr.pi n' _ t' b') :=
      do { (x, y, symbole) ← rel_symb t',
           my_expr.forall_rel n t symbole y <$> parse b' } <|>
      do { body ← parse e',
           pure $ my_expr.forall_simple n t body }
    | e' := if e.binding_name = "ᾰ" then
              pure (impl t e')
            else
              forall_simple n t <$> parse b
    end
|`(@Exists %%α %%p) := do
  `(@Exists %%α' %%p') ← pure p.binding_body |
      exist_simple p.binding_name α <$> parse p.binding_body ,
  (x, y, symbole) ← rel_symb α'.binding_body,
  exist_rel p.binding_name α symbole y <$> parse p'.binding_body
| e := do { t ← tactic.infer_type e, pure $ if t = `(Prop) then prop e else data e } <|> pure (prop e)

end my_expr

[Patrick Massot]

This defines a specialized grammar for expression where bounded quantifiers become first class citizens.

[Patrick Massot]

Note that I'm especially not proud of my detection of implication using if e.binding_name = "ᾰ". A better solution would be welcome.

[Mario Carneiro]

I think docs#expr.is_arrow exists

[Patrick Massot]

This is what I used in the beginning, but it didn't work.

[Patrick Massot]

I think it doesn't work for open terms.

[Patrick Massot]

I hope I'm not inventing the meaning of "open term".

[Patrick Massot]

I mean I had issue where I was traversing an expr and the implication referred to variables introduced earlier in the expression.

[Mario Carneiro]

You should not be directly manipulating open terms if possible

[Mario Carneiro]

(where open means containing free occurrences of var constructor)

[Mario Carneiro]

Instead you should instantiate as you descend into binders

[Alex J. Best]

How come Mario? Certainly I can see why it is nicer to have closed terms a lot of the time, but are there specific reasons we should try and avoid it? I've written a lot of code that manipulates open terms :sweat:

[Mario Carneiro]

An example of a simple tactic that has to descend into binders is generalize_proofs, see https://github.com/leanprover-community/mathlib/blob/master/src/tactic/generalize_proofs.lean#L50-L53

[Mario Carneiro]

Mostly because all of lean's API assumes closed terms

[Mario Carneiro]

If you can do the whole job yourself, constructing / manipulating exprs without consulting lean, then it's fine to work on open terms

[Mario Carneiro]

but for example if you ever want to call infer_type then you are stuck

[Mario Carneiro]

(and for some things you have to consult the local context, for example if you encounter a local constant or metavariable in the expr)

[Mario Carneiro]

an example of a function working directly on open terms nontrivially is src#tactic.alias.mk_iff_mp_app

[Patrick Massot]

I'm clearly having issues with this. Below is a slightly updated version of my code including parsing tests. I'm almost happy with the result except precisely for the appearing of induces where I would like to see the original names. Do you see what I mean?

import tactic.basic

meta def rel_symb : expr → tactic (expr × expr × string)
| `(%%x < %%y) := pure (x, y, " < ")
| `(%%x ≤ %%y) := pure (x, y, " ≤ ")
| `(%%x > %%y) := pure (x, y, " > ")
| `(%%x ≥ %%y) := pure (x, y, " ≥ ")
| `(%%x ∈ %%y) := pure (x, y, " ∈ ")
| e := do pe ← tactic.pp e, tactic.fail $ "Not a relation: " ++ pe.to_string

meta inductive my_expr
| forall_rel (var_name : name) (typ : expr) (rel : string) (rel_rhs : expr) (propo : my_expr) : my_expr
| forall_simple (var_name : name) (typ : expr) (propo : my_expr) : my_expr
| exist_rel (var_name : name) (typ : expr) (rel : string) (rel_rhs : expr) (propo : my_expr) : my_expr
| exist_simple (var_name : name) (typ : expr) (propo : my_expr) : my_expr
| impl (lhs : expr) (rhs : expr) : my_expr
| prop (e : expr) : my_expr
| data (e : expr) : my_expr

namespace my_expr

meta def tofmt : my_expr →  tactic format
| (forall_rel var_name typ rel rel_rhs propo) := do
    rhs ← tactic.pp rel_rhs,
    p ← tofmt propo,
    pure $ "∀ " ++ var_name.to_string ++ rel ++ rhs.to_string ++ ", " ++ p
| (forall_simple var_name typ propo) := do
    p ← tofmt propo,
    pure $ "∀ " ++ var_name.to_string ++ ", " ++ p
| (exist_rel var_name typ rel rel_rhs propo) := do
    rhs ← tactic.pp rel_rhs,
    p ← tofmt propo,
    pure $ "∃ " ++ var_name.to_string ++ rel ++ rhs.to_string ++ ", " ++ p
| (exist_simple var_name typ propo) := do
    p ← tofmt propo,
    pure $ "∃ " ++ var_name.to_string ++ ", " ++ p
| (impl lhs rhs) := do
  l ← tactic.pp lhs,
  r ← tactic.pp rhs,
  pure $ l ++ " ⇒ " ++ r
| (prop e) := tactic.pp e
| (data e) := tactic.pp e

meta instance : has_to_tactic_format my_expr :=
⟨my_expr.tofmt⟩

meta def parse : expr → tactic my_expr
| e@(expr.pi n _ t b) := match b with
    | e'@(expr.pi n' _ t' b') :=
      do { (x, y, symbole) ← rel_symb t',
           my_expr.forall_rel n t symbole y <$> parse b' } <|>
      do { body ← parse e',
           pure $ my_expr.forall_simple n t body }
    | e' := if e.binding_name = "ᾰ" then
              pure (impl t e')
            else
              forall_simple n t <$> parse b
    end
|`(@Exists %%α %%p) := do
  `(@Exists %%α' %%p') ← pure p.binding_body |
      exist_simple p.binding_name α <$> parse p.binding_body ,
  (x, y, symbole) ← rel_symb α'.binding_body,
  exist_rel p.binding_name α symbole y <$> parse p'.binding_body
| e := do { t ← tactic.infer_type e, pure $ if t = `(Prop) then prop e else data e } <|> pure (prop e)

end my_expr

namespace tactic.interactive
setup_tactic_parser
open tactic my_expr

meta def test (h : parse ident) : tactic unit :=
get_local h >>= infer_type >>= parse >>= trace

end tactic.interactive

example (Q R : ℕ → Prop) (P : ℕ → ℕ → Prop)
  (h₁ : R 1 → Q 2)
  (h₂ : ∀ k ≥ 2, ∃ n ≥ 3, ∀ l, l - n = 0 → P l k)
  (h₃ : ∃ n ≥ 5, Q n)
  (h₄ : ∀ k ≥ 2, ∃ n ≥ 3, P n k)
  (h₅ : ∃ n, Q n)
  (h₆ : ∀ k, ∃ n, P n k)
  (h₇ : ∀ k ≥ 2, ∃ n, P n k) : true :=
begin
  test h₁,
  test h₂,
  test h₃,
  test h₄,
  test h₅,
  test h₆,
  test h₇,
  trivial
end

[Mario Carneiro]

induces?

[Patrick Massot]

So really I don't want those open terms, I simply lack the knowledge of how to close them back

[Patrick Massot]

Mario Carneiro said:

induces?

Sorry, I don't understand that message at all.

[Mario Carneiro]

you said induces and it didn't make sense

[Patrick Massot]

oh sorry! I wanted to write indices

[Patrick Massot]

de Bruijn indices

[Patrick Massot]

modulo spelling of that name

[Mario Carneiro]

So that's what the first link was about:

| (expr.pi n b d e) := do
  nh ← collect_proofs_in d ctx (ns, hs),
  var ← mk_local' n b d,
  collect_proofs_in (expr.instantiate_var e var) (var::ctx) nh

You use var <- mk_local' n b d to get a new local constant and then use expr.instantiate_var e var to instantiate the body before recursing

[Mario Carneiro]

and hold on to var as the "variable being bound" in your inductive representation of the binder

[Patrick Massot]

Thanks, I'll try that.