Zulip Chat Archive

Stream: general

Topic: generating all `app`s


view this post on Zulip Scott Morrison (Apr 24 2018 at 22:31):

Say I have an e : expr, which is probably some function type, and some other collection of A : list expr, and I would like to find all ways of plugging something from A into the next argument of e. Should I:
1) Actually look at what type e is, in particular the type of its first argument, and then look through A checking if there is anything of that type?
2) Just invoking mk_app e [a] for each a in A, and collect whatever succeeds?

view this post on Zulip Scott Morrison (Apr 24 2018 at 22:34):

Option 2) is obviously much easier to write, I'm just wondering if I should expect that it is going to be way slower, or something.

view this post on Zulip Simon Hudon (Apr 24 2018 at 23:23):

It might be worth experimenting but I don't think 2) would be any slower than 1)

view this post on Zulip Scott Morrison (Apr 25 2018 at 01:03):

err... mk_app takes a name and a list expr worth of arguments. If I just have a b : expr, what's the idiomatic way to apply a to b, inferring implicit arguments and typechecking?

view this post on Zulip Simon Hudon (Apr 25 2018 at 01:08):

I think type_check (a b) might do the trick. You can also postpone type checking until you actually use those expressions.

view this post on Zulip Scott Morrison (Apr 25 2018 at 01:18):

Are there some backticks missing in your suggestion there?

view this post on Zulip Scott Morrison (Apr 25 2018 at 01:18):

I haven't quite internalised quoting and antiquoting ...

view this post on Zulip Simon Hudon (Apr 25 2018 at 01:20):

In this case, I'm just using the fact that expr has a has_coe_to_fun instance so you can use an expr as a function and it just wraps it in a expr.app

view this post on Zulip Scott Morrison (Apr 25 2018 at 01:25):

I think I can also use something like try_core (to_expr ``(%%e %%f)).

view this post on Zulip Simon Hudon (Apr 25 2018 at 01:30):

Yes I think that's right. It might be slower because your going from expr to pexpr and back.

view this post on Zulip Simon Hudon (Apr 25 2018 at 01:32):

Depending on what you do with the expressions after, you might be able to do better than my proposal. Whatever you do with the resulting expression might need to be type checked again so you could just return a b with the understanding that it might eventually fail to type check

view this post on Zulip Mario Carneiro (Apr 25 2018 at 02:19):

How did you get a in your application a b? Lean works at the application list level (i.e. f a1 a2 ... an) when it does implicits and such

view this post on Zulip Mario Carneiro (Apr 25 2018 at 02:28):

I think the fastest option is to whnf the type of a to a Pi type, get its binding domain, and then unify it with the type of b \in A for each b. That way you minimize the amount for repeated work for failures and don't have to check more than you need to (type_check will go through the whole term)

view this post on Zulip Simon Hudon (Apr 25 2018 at 02:30):

Interesting! So option 1). I went the other way because I think this work will have to be done by the type checker and since that's done in C++, I would think it would be faster than anything you'd come up with.

view this post on Zulip Mario Carneiro (Apr 25 2018 at 02:31):

type_check is never done in C++, it's only for debugging

view this post on Zulip Mario Carneiro (Apr 25 2018 at 02:31):

it's all incremental in the C++ stuff

view this post on Zulip Mario Carneiro (Apr 25 2018 at 02:32):

In scott's case the a is constant but the b changes, so it makes sense to precompute it

view this post on Zulip Simon Hudon (Apr 25 2018 at 02:32):

Good point

view this post on Zulip Mario Carneiro (Apr 25 2018 at 02:33):

I'm guessing that Scott is building a search algorithm that just strings everything together that's well typed (trying to prove the five lemma maybe?) and for that this will be a really hot path so quick failure is important

view this post on Zulip Mario Carneiro (Apr 25 2018 at 02:36):

Option 2 would possibly have worked, but it's not type correct as scott points out and there's no immediate fix, lean isn't optimized for this kind of checking

view this post on Zulip Scott Morrison (Apr 25 2018 at 10:23):

I'm going to defer trying @Mario Carneiro's suggested fastest option, as I'm not confident playing with binding domains yet.

view this post on Zulip Scott Morrison (Apr 25 2018 at 10:23):

In the meantime, it seems that when I try to_expr ``(%%e %%f), Lean doesn't manage to fill in implicit arguments.

view this post on Zulip Scott Morrison (Apr 25 2018 at 10:24):

Is this expected? Is there a good way to do this? I'll try to come up with a MWE now.

view this post on Zulip Scott Morrison (Apr 25 2018 at 11:08):

It seems that the problem is that to_expr ``(%%e %%f) is over-eager about implicit arguments.

view this post on Zulip Scott Morrison (Apr 25 2018 at 11:09):

Say e represented something with a explicit argument then an implicit argument.

view this post on Zulip Scott Morrison (Apr 25 2018 at 11:09):

Then to_expr ``(%%e %%f) produces not e f but e f ?m_1.

view this post on Zulip Scott Morrison (Apr 25 2018 at 11:13):

axiom f :   Type
def g (n : ) {k : } (x : f k) := n

set_option pp.implicit true
example : true :=
begin
  do e  to_expr ```(g),
     f  to_expr ```(57),
     to_expr ```(%%e %%f) >>= pp >>= trace
end

view this post on Zulip Scott Morrison (Apr 25 2018 at 11:13):

produces @g 57 ?m_1

view this post on Zulip Scott Morrison (Apr 25 2018 at 11:13):

But I'd really like it to just produce g 57.

view this post on Zulip Scott Morrison (Apr 25 2018 at 11:28):

Hmm... I think this one is above my pay-grade for now. If anyone would like to help write a

meta def apps (e : expr) (F : list expr) : tactic (list expr) :=

that actually works (i.e. return a list of all ways to plug in an f ∈ F as the next explicit argument of e) that would be wonderful.

view this post on Zulip Scott Morrison (Apr 25 2018 at 11:28):

My current implementation is
do l ← F.mmap $ λ f, (do r ← try_core (to_expr ```(%%e %%f)), return r.to_list), return l.join

view this post on Zulip Scott Morrison (Apr 25 2018 at 11:30):

But that suffers from the problem explained above. Mario suggested to me that I first inspect e, find the first explicit binder in it, and try to unify it with each element of F.

view this post on Zulip Scott Morrison (Apr 25 2018 at 11:30):

Unfortunately I don't know what I'm meant to do with any earlier implicit binders I find before the first explicit one, or how they would end up getting assigned by unification.

view this post on Zulip Simon Hudon (Apr 25 2018 at 13:15):

When you encounter implicit binders, create a meta variable and use it as a parameter.

view this post on Zulip Scott Morrison (Apr 25 2018 at 13:16):

@Simon Hudon do you know of examples of this I can look at? I got pretty confused dealing with binders. :-(

view this post on Zulip Simon Hudon (Apr 25 2018 at 13:23):

Sure, have a look at https://github.com/leanprover/mathlib/blob/master/tactic/basic.lean#L100-L105

view this post on Zulip Scott Morrison (Apr 25 2018 at 13:47):

Okay, that's helpful. Do you know if there is any existing code that instead of just producing expr.app e f, produces e, with f stuck into the first explicit argument of e (and any earlier implicit arguments filled)?

view this post on Zulip Simon Hudon (Apr 25 2018 at 14:00):

I'm sure I have something like that around. Let's see ...

view this post on Zulip Simon Hudon (Apr 25 2018 at 14:11):

Actually, I can't find exactly that but let me sketch something for you

view this post on Zulip Scott Morrison (Apr 25 2018 at 14:18):

Thank you! I better go to sleep now, but I'll look forward to seeing your answer when I'm back.

view this post on Zulip Simon Hudon (Apr 25 2018 at 14:19):

Hopefully, this catches you before sleep does:

meta def mk_app_aux : expr  expr  expr  tactic expr
 | f (expr.pi n binder_info.default d b) arg := do
   infer_type arg >>= unify d,
   return $ f arg
 | f (expr.pi n _ d b) arg := do
   v  mk_meta_var d,
   t  whnf (b.instantiate_var v),
   mk_app_aux (f v) t arg
 | e _ _ := return e

meta def mk_app' (f arg : expr) : tactic expr :=
do t  infer_type f >>= whnf,
   mk_app_aux f t arg

view this post on Zulip Scott Morrison (Apr 25 2018 at 14:39):

Perfect.

view this post on Zulip Scott Morrison (Apr 25 2018 at 14:41):

(I changed | e _ _ := return e to | e _ _ := failed)


Last updated: May 14 2021 at 04:22 UTC