Zulip Chat Archive

Stream: general

Topic: more expr munging


view this post on Zulip 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.

view this post on Zulip Scott Morrison (Sep 09 2018 at 11:28):

Any suggestions?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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. :-)

view this post on Zulip Simon Hudon (Sep 09 2018 at 11:38):

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

view this post on Zulip 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. :-)

view this post on Zulip Simon Hudon (Sep 09 2018 at 11:49):

I'm listening (sort of)

view this post on Zulip Scott Morrison (Sep 09 2018 at 11:50):

I had written:

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

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip Reid Barton (Sep 09 2018 at 11:53):

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

view this post on Zulip Scott Morrison (Sep 09 2018 at 11:54):

Yeah, I guess so.

view this post on Zulip Scott Morrison (Sep 09 2018 at 11:54):

But maybe I am needlessly complicating things. :-(

view this post on Zulip Simon Hudon (Sep 09 2018 at 11:55):

I think you need to reverse mvars

view this post on Zulip 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.

view this post on Zulip 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. :-)

view this post on Zulip Scott Morrison (Sep 09 2018 at 11:59):

Thanks for the help!

view this post on Zulip Simon Hudon (Sep 09 2018 at 11:59):

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

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip Reid Barton (Sep 09 2018 at 12:05):

Right, you only save the decomposition of the Pis.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Sep 09 2018 at 12:13):

and, happily it all seems to work now!

view this post on Zulip 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