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