Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: matching binders


view this post on Zulip Reid Barton (Oct 18 2020 at 16:53):

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?

view this post on Zulip Simon Hudon (Oct 18 2020 at 16:59):

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

view this post on Zulip Reid Barton (Oct 18 2020 at 17:01):

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?

view this post on Zulip Reid Barton (Oct 18 2020 at 17:02):

In the MWE, everything is overkill :upside_down:

view this post on Zulip Simon Hudon (Oct 18 2020 at 17:02):

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

view this post on Zulip Reid Barton (Oct 18 2020 at 17:02):

right

view this post on Zulip Reid Barton (Oct 18 2020 at 17:02):

a term (which is the antiquotation of a variable)

view this post on Zulip Simon Hudon (Oct 18 2020 at 17:03):

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

view this post on Zulip Reid Barton (Oct 18 2020 at 17:04):

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

view this post on Zulip Mario Carneiro (Oct 18 2020 at 17:04):

expr.instantiate_local I think

view this post on Zulip Simon Hudon (Oct 18 2020 at 17:05):

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

view this post on Zulip Reid Barton (Oct 18 2020 at 17:05):

aha

view this post on Zulip Reid Barton (Oct 18 2020 at 17:06):

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

view this post on Zulip Simon Hudon (Oct 18 2020 at 17:06):

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

view this post on Zulip Simon Hudon (Oct 18 2020 at 17:08):

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

view this post on Zulip Simon Hudon (Oct 18 2020 at 17:08):

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

view this post on Zulip Reid Barton (Oct 18 2020 at 17:20):

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.)

view this post on Zulip Simon Hudon (Oct 18 2020 at 17:25):

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

view this post on Zulip Reid Barton (Oct 18 2020 at 17:30):

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

view this post on Zulip Simon Hudon (Oct 18 2020 at 17:31):

Exactly


Last updated: May 09 2021 at 23:10 UTC