## Stream: general

### Topic: more expr munging

#### Scott Morrison (Sep 09 2018 at 11:28):

Say I have an expr representing an iterated pi type, which is finally an equation, something like Π (a : ℕ) (b : ℕ), f a b = g (a + b). From that, I want to produce f ?m_1 ?m_2, where ?m_1 and ?m_2 are newly created metavariables of the appropriate types.

Any suggestions?

#### Reid Barton (Sep 09 2018 at 11:31):

Are you guaranteed that the left hand side will be literally <something> a b, where a and b are the variables introduced by the Pis in order? Or could it be some arbitrary expression involving a and b?

#### Simon Hudon (Sep 09 2018 at 11:34):

meta def get_lhs : expr -> tactic expr
| (expr.pi n bi d b) :=
do v <- mk_local' n bi d,
b' <- whnf $b.instantiate_var v get_lhs b' | (%%a = %%b) := pure a | _ := failed  #### Reid Barton (Sep 09 2018 at 11:36): Yes this strategy is what I was about to suggest. Peel off one outer Pi at a type, leaving a formula with a free variable, and then substitute a fresh metavariable or whatever else you want for that free variable #### Simon Hudon (Sep 09 2018 at 11:37): Actually, we can be more direct: meta def get_lhs : expr -> tactic expr | (expr.pi n bi d b) := do v <- mk_meta_var d, b' <- whnf$ b.instantiate_var v
get_lhs b'
| (%%a = %%b) := pure a
| _ := failed


#### Scott Morrison (Sep 09 2018 at 11:37):

(I'm doubly impressed, Simon, that your code often doesn't quite compile: there's a comma missing in that first one. :-)

#### Simon Hudon (Sep 09 2018 at 11:38):

Where would be the fun if you didn't have to fix my mistakes?

#### Scott Morrison (Sep 09 2018 at 11:48):

So I'm trying to do something a bit fancier here, and while get_lhs work as requested, really I want something more. :-)

#### Simon Hudon (Sep 09 2018 at 11:49):

I'm listening (sort of)

#### Scott Morrison (Sep 09 2018 at 11:50):

meta def substitutions' : expr → bool → list expr →
tactic (tactic (expr × expr × list expr))
| (expr.pi n bi d b) symm types :=
do substitutions' b symm (d :: types)
| (%%lhs = %%rhs) symm types :=
do let (lhs, rhs) := if symm then (rhs, lhs) else (lhs, rhs),
let tac := (do mvars ← types.mmap mk_meta_var,
let pattern := lhs.instantiate_vars mvars,
ty ← infer_type pattern,
return (pattern, ty, mvars)),
return tac
| _ _ _ := failed


#### Scott Morrison (Sep 09 2018 at 11:51):

The idea being to return a tactic, which could be invoked multiple times, each time producing the pattern with "fresh" mvars.

#### Scott Morrison (Sep 09 2018 at 11:51):

However it's ... still somewhat mysteriously ... not working in all cases. (Sorry this is far from a MWE.)

#### Reid Barton (Sep 09 2018 at 11:53):

Is this supposed to be more efficient than just invoking something like get_lhs repeatedly?

#### Scott Morrison (Sep 09 2018 at 11:54):

Yeah, I guess so.

#### Scott Morrison (Sep 09 2018 at 11:54):

But maybe I am needlessly complicating things. :-(

#### Simon Hudon (Sep 09 2018 at 11:55):

I think you need to reverse mvars

#### Reid Barton (Sep 09 2018 at 11:56):

It's probably about equally or less efficient because the representation of that tactic object in the VM is going to be basically the same as or a more complicated structure than the outer Pis of the original type.

#### Scott Morrison (Sep 09 2018 at 11:59):

Hmm. I had tried (on a purely voodoo basis) reversing mvars, without apparent success. Let me go away on de-complicate for a bit. :-)

#### Scott Morrison (Sep 09 2018 at 11:59):

Thanks for the help!

#### Simon Hudon (Sep 09 2018 at 11:59):

After squinting at it for a while, I agree with @Reid Barton

#### Reid Barton (Sep 09 2018 at 12:02):

(Or at least, that would be true in the GHC runtime system, which is probably a terrible mental model for the Lean VM but the best one I have available.)

#### Simon Hudon (Sep 09 2018 at 12:04):

My reasoning is that, for each bound variable, the expensive thing is instantiate_var, the number of which does not decrease in this approach

#### Reid Barton (Sep 09 2018 at 12:05):

Right, you only save the decomposition of the Pis.

#### Reid Barton (Sep 09 2018 at 12:08):

Which is cheap anyways, but to make things worse, you replace it by having to do an equal number of applications-of-variable-functions (the inner tacticwhich you build up).

#### Reid Barton (Sep 09 2018 at 12:11):

Oh wait, you implemented it in a way so that there is only one closure being built (tac), but still each invocation of tac has to process the list types`, which has the same information as the outer Pis of the original expression.

#### Scott Morrison (Sep 09 2018 at 12:13):

and, happily it all seems to work now!

#### Scott Morrison (Sep 09 2018 at 12:13):

(or at least the "all" that I hoped to have done tonight!)

Last updated: May 11 2021 at 00:31 UTC