<div dir="ltr">Hi,<div><br></div><div>It shouldn't be hard to do the merge, but I am not sure that I'll have time to do it before the weekend---I'll give it a go then.</div><div><br></div><div>-Iavor  </div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Oct 21, 2014 at 9:40 AM, Adam Gundry <span dir="ltr"><<a href="mailto:adam@well-typed.com" target="_blank">adam@well-typed.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Thanks Iavor, this is really helpful!<br>
<br>
If you have a moment to merge Simon's more recent changes on<br>
wip/new-flatten-skolems-Aug14, I'm keen to try out the new<br>
unflattening... or I can have a go at the merge if it would help?<br>
<br>
You may be right that flattened constraints are easier to work with in<br>
some cases, so it would be great if the plugin could choose which it<br>
sees. Unfortunately I'm not sure we can easily unflatten *some*<br>
constraints, given the way unflattening will work in the new<br>
getInertUnsolved. One option might be for tcPluginSolve to be called in<br>
both places, with a boolean parameter.<br>
<br>
Cheers,<br>
<br>
Adam<br>
<span class="im HOEnZb"><br>
<br>
On 18/10/14 23:33, Iavor Diatchki wrote:<br>
> Hello,<br>
><br>
> Just a heads up, if anyone is playing around with this:  I just updated<br>
> the plugin interface a bit.<br>
><br>
> Here are the changes:<br>
>    - A plugin now gets 3 sets of constraints: given, derived, and wanted<br>
> (in that order)<br>
>    - Plugins are now also presented with dictionary constraints (i.e.,<br>
> you may see equalities, function equalities, and dictionaries)<br>
>    - A plugin does not need to return all constraints that need to be<br>
> put back in the inert set.  This is both simpler and more efficient, I<br>
> think.  So, now a plugin can return one of these two results:<br>
>       - All is good:  plugin returns some solved constraints, and some<br>
> new constraints to be processed by the constraint solver. The solved<br>
> constraints are removed from the inert set, and their evidence variables<br>
> are defined.  The new work is added to the work list.<br>
>       - Found contradiction: plugin returns a list of the conflicting<br>
> constraint; these are removed from the inert set, and re-added as<br>
> insoluable.<br>
><br>
> Happy hacking,<br>
> -Iavor<br>
><br>
><br>
><br>
><br>
><br>
><br>
> On Fri, Oct 17, 2014 at 3:36 PM, Iavor Diatchki<br>
</span><span class="im HOEnZb">> <<a href="mailto:iavor.diatchki@gmail.com">iavor.diatchki@gmail.com</a> <mailto:<a href="mailto:iavor.diatchki@gmail.com">iavor.diatchki@gmail.com</a>>> wrote:<br>
><br>
>     Hello,<br>
><br>
>     On Thu, Oct 16, 2014 at 3:58 AM, Adam Gundry <<a href="mailto:adam@well-typed.com">adam@well-typed.com</a><br>
</span><div class="HOEnZb"><div class="h5">>     <mailto:<a href="mailto:adam@well-typed.com">adam@well-typed.com</a>>> wrote:<br>
><br>
><br>
><br>
>         One problem I've run into is transforming the flattened<br>
>         CFunEqCans into<br>
>         unflattened form (so the flatten-skolems don't get in the way of<br>
>         AG-unification). Do you know if there is an easy way to do this,<br>
>         or do I<br>
>         need to rebuild the tree manually in the plugin?<br>
><br>
><br>
>     One thing that occurred to me about this:  when constraints are<br>
>     "flattened",<br>
>     it is easy for a plugin to pick-out only the one that it cares<br>
>     about.  If things were fully<br>
>     unflattened, this would not be the case... For example, if I have a<br>
>     constraint:<br>
><br>
>     (2 + F a) ~ F a + F a<br>
><br>
>     In the flattened form, this will become:<br>
>     (F a ~ f1, 2 + f1 ~ f2, f1 + f2 ~ f3, f2 ~ f3)<br>
><br>
>     So, the type-nats plugin would pick out: (2 + f1 ~ f2, f1 + f2 ~ f3,<br>
>     f2 ~ f3),<br>
>     and ignore (F a ~ f1), as it knows nothing about arbitrary type<br>
>     functions.<br>
><br>
>     So, if we want to do un-flattening, I think we should do it only on<br>
>     those constraints<br>
>     that are of interest to the plugin.<br>
><br>
><br>
><br>
><br>
>         Also, I notice that you are providing only equality constraints<br>
>         to the<br>
>         plugin. Is there any reason we can't make other types of constraint<br>
>         available as well? For example, one might want to introduce a<br>
>         typeclass<br>
>         with a special solution strategy (cf. Coercible, or the Has class in<br>
>         OverloadedRecordFields).<br>
><br>
><br>
>     Yeah, we should probably pass-in all constraints, inlcluding derived<br>
>     ones.<br>
>     The reason it is not like that is pretty much historical now.<br>
>     So I'll have a go at making this change.<br>
><br>
>     -Iavor<br>
><br>
><br>
><br>
><br>
><br>
><br>
><br>
>         >   - As an example, I've extracted my work on using an SMT solver at the<br>
>         > type level as a separate plugin:<br>
>         ><br>
>         >       <a href="https://github.com/yav/type-nat-solver" target="_blank">https://github.com/yav/type-nat-solver</a><br>
>         ><br>
>         >    - To see how to invoke a module that uses a plugin, have a look in<br>
>         > `examples/A.hs`.<br>
>         >      (Currently, the plugin assumes that you have `cvc4` installed and<br>
>         > available in the path).<br>
>         ><br>
>         >     - Besides this, we don't have much documentation yet.  For hackers:<br>
>         > we tried to use `tcPlugin` on<br>
>         >     `TcPlugin` in the names of all things plugin related, so you could<br>
>         > grep for this.  The basic API<br>
>         >      types and functions are defined in `TcRnTypes` and `TcRnMonad`.<br>
>         ><br>
>         > Happy hacking,<br>
>         > -Iavor<br>
<br>
--<br>
Adam Gundry, Haskell Consultant<br>
Well-Typed LLP, <a href="http://www.well-typed.com/" target="_blank">http://www.well-typed.com/</a><br>
</div></div></blockquote></div><br></div>