matching binders

Stream: metaprogramming / tactics

[Reid Barton]

Is something like

meta def foo : expr → tactic expr
| `(Σ (_ : %%A), %%B) := failed
| _ := failed

ever a good idea? Or will B end up in some weird state (it should be an expression in a modified context)? Should I just use open_lambdas?

[Simon Hudon]

B will be an open term with one free de Bruijn variable. It's easy to repair. You can also match sigma applied to a lambda and use open_lambdas if you prefer. That seems over kill to me

[Reid Barton]

Just to check, by "match sigma applied to a lambda" you mean "match sigma applied to a variable, which I expect to be a lambda" right?

[Reid Barton]

In the MWE, everything is overkill :upside_down:

[Simon Hudon]

To be even more exact: "match sigma applied to a term, which I expect to be a lambda"

[Reid Barton]

right

[Reid Barton]

a term (which is the antiquotation of a variable)

[Simon Hudon]

I would say if you have only one bound variable, I wouldn't use open_*. If you have a few, you might need to write a specialized open_sigma function

[Reid Barton]

How do I "repair" B if I matched on it?

[Mario Carneiro]

expr.instantiate_local I think

[Simon Hudon]

do v <- mk_local_def `v A,
   let B := B.instantiate_var v,
   ...

[Reid Barton]

aha

[Reid Barton]

/-- `instantiate_var a b` takes the 0th de-Bruijn variable in `a` and replaces each occurrence with `b`. -/

[Simon Hudon]

Be careful, if B contains meta variables, the result will be messed up. You should use instantiate_mvars on B first.

[Simon Hudon]

Mario Carneiro said:

expr.instantiate_local I think

This is what you use when you're specifying a local constant to instantiate rather than a de Bruijn variable

[Simon Hudon]

There are a bunch of variations on abstract and instantiate, they're often easy to confuse for each other. (and not to mention kabstract)

[Reid Barton]

I want to think of B as a type in the context i : A anyways, and recurse on the structure of B, so maybe keeping B in this "open" form while I do the recursion is sensible anyways.
(I guess the alternative is, if i got turned into a local constant, then I need to recognize the variable i in the local_const case of expr.)

[Simon Hudon]

If you keep B open, tactics like infer_type and unify and anything that uses them breaks down. You may want to carry around a list of new locals instead

[Reid Barton]

Ah, that might be a problem, since expr doesn't have type information everywhere (e.g., not at app)

[Simon Hudon]

Exactly