Hi, The source code is here: https://github.com/yav/type-nat-solver There is an example of a module using a plugin in `examples/A.hs`.
Things may be a bit broken at the moment though, as we've been changing things a bit, to work with the new constraint solver, and plugin system. -Iavor On Fri, Nov 14, 2014 at 9:45 AM, Francesco Mazzoli <f...@mazzo.li> wrote: > For what it's worth, I'd be very excited to have that feature in 7.10. > > Iavor, is there anywhere I can read on how to try your solver for > type-level naturals? > > Francesco > > On 14 November 2014 18:14, Adam Gundry <a...@well-typed.com> wrote: > > Thanks, Simon! I've been convinced that TcS is more than we need, and I > > think the right thing to do is to (optionally) invoke the plugin after > > the constraints have been unflattened anyway. I've just pushed a commit > > to wip/tc-plugins-amg that does this. Iavor, Eric, your views on how > > convenient this alternative is would be most welcome. I'm also wondering > > if the plugin should be told how many times it has been called, to make > > it easier to prevent infinite loops. > > > > I'm very keen to get this into 7.10, appropriately branded as a very > > experimental feature. Austin, have I sufficiently addressed your > > concerns about the hs-boot file and multiple flags? Is there anything > > else we need, apart perhaps from tests and documentation, which I'll put > > together next week? > > > > Thanks, > > > > Adam > > > > > > On 12/11/14 11:16, Simon Peyton Jones wrote: > >> Iavor, Adam, Eric > >> > >> > >> > >> I’m happy with the general direction of the plugins stuff, so I’m mostly > >> going to leave it to you guys to plough ahead; but I am happy to respond > >> to questions. > >> > >> > >> > >> * I still think it would be better to provide an escape hatch to the > >> TcS, not merely the TcM, alongside the nice TcPluginM wrapper. Notably, > >> Simon's new TcFlatten.unflatten needs TcS... > >> > >> > >> > >> It think the only reason for this is that ‘unflatten’ needs to set > >> evidence bindings, which in turn requires access to tcs_ev_binds. I > >> think that everything else is in TcM. So I suppose you could carry > >> around the EvBindsVar if you really didn’t want TcS. (And I can see why > >> you wouldn’t; TcS has a lot of stuff you don’t need.) > >> > >> > >> > >> Simon > >> > >> > >> > >> > >> > >> *From:*Iavor Diatchki [mailto:iavor.diatc...@gmail.com] > >> *Sent:* 10 November 2014 19:15 > >> *To:* Adam Gundry > >> *Cc:* ghc-devs@haskell.org; Simon Peyton Jones > >> *Subject:* Re: Typechecker plugins: request for review and another > >> workflow question > >> > >> > >> > >> Hi, > >> > >> > >> > >> On Mon, Nov 10, 2014 at 1:31 AM, Adam Gundry <a...@well-typed.com > >> <mailto:a...@well-typed.com>> wrote: > >> > >> > >> On the subject of that "nearly", I'm interested to learn whether you > >> have a suggestion to deal with unflattening, because the interface > still > >> works with flat constraints only. Simon's changes should make it > more > >> practical to unflatten inside the plugin, but it would be far > easier (at > >> least for my purposes) if it was simply given unflattened > constraints. I > >> realise that this would require the plugin loop to be pushed further > >> out, however, which has other difficulties. > >> > >> > >> > >> Not sure what to do about this. With the current setup, I think either > >> way, the plugin would have to do some extract work. Perhaps we should > >> run the plugins on the unflattened constraints, and leave to the plugins > >> to manually temporarily "flatten" terms from external theories? For > >> example, if the type-nat plugin saw `2 * F a ~ 4`, it could temporarily > >> work with `2 * x ~ 4`, and then when it figures out that `x ~ 2`, it > >> could emit `F a ~ 2` (non-canonical), which would go around again, and > >> hopefully get fully simplified. > >> > >> > >> > >> > >> > >> > >> A few other issues, of lesser importance: > >> > >> * I still think it would be better to provide an escape hatch to > the > >> TcS, not merely the TcM, alongside the nice TcPluginM wrapper. > Notably, > >> Simon's new TcFlatten.unflatten needs TcS... > >> > >> I don't mind that but, if I recall correctly, to do this without more > >> recursive modules, we had to split `TCSMonad` in two parts, one with the > >> types, and one with other stuff. Eric and I did this once, but we > >> didn't commit it, because it seemed like an orthogonal change. > >> > >> > >> > >> > >> > >> * Is there a way for my plugin to "solve" a given constraint (e.g. > to > >> discard the uninformative "a * 1 ~ a")? > >> > >> Yes, you'd say something like: `TcPluginOK [(evidence, "a * 1 ~ a")] []` > >> > >> > >> > >> The first field of `TcPluginOK` are things that are solved, the second > >> one is new work. > >> > >> > >> > >> * It is unfortunately easy to create infinite loops by writing > plugins > >> that emit wanteds but make no useful progress. Perhaps there should > be a > >> limit on the number of times round the loop (like SubGoalDepth but > for > >> all constraints)? > >> > >> > >> > >> Indeed, if a plugin keeps generating new work, we could go in a loop, so > >> maybe a limit of some sort is useful. However, note that if the plugin > >> generates things that are already in the inert set, GHC should notice > >> this and filter them, so we won't keep going. > >> > >> > >> > >> > >> > >> * Perhaps runTcPlugin should skip invoking the plugin if there are > no > >> wanteds? > >> > >> > >> > >> Oh, there is an important detail here that needs documentation! GHC > >> will call the plugin twice: once to improve the givens, and once to > >> solve the wanteds. The way to distinguish the two is exactly by the > >> presence of the wanteds. > >> > >> > >> > >> Why might you want to improve the givens? Suppose you had something > >> like `x * 2 ~ 4` as a given: then you'd really want the plugin to > >> generate another given: `x ~ 2`, as this is likely to help the rest of > >> the constraint solving process. > >> > >> > >> > >> > >> * The use of ctev_evar in runTcPlugin is partial, and fails with a > >> nasty error if the plugin returns a non-wanted in the solved > constraints > >> list. Would it be worth catching this error and issuing a sensible > >> message that chastises the plugin author appropriately? > >> > >> > >> > >> Aha, good idea. Bad plugin! :-) > >> > >> > >> > >> > >> > >> * Finally, I presume the comment on runTcPlugin that "The plugin is > >> provided only with CTyEq and CFunEq constraints" is simply outdated > and > >> should be removed? > >> > >> Yep, thanks! > >> > >> > >> > >> Apologies for the deluge of questions - please take them as > evidence of > >> my eagerness to use this feature! > >> > >> > >> > >> Thanks for your feedback! Also, if you feel like doing some hacking > >> please do so---I am quite busy at the moment so I don't have a ton of > >> time to work on it, so any help you be most appreciated. I know Eric is > >> also quite keen on helping out so we can just coordinate over e-mail. > >> > >> > >> > >> -Iavor > > > > > > -- > > Adam Gundry, Haskell Consultant > > Well-Typed LLP, http://www.well-typed.com/ > > _______________________________________________ > > ghc-devs mailing list > > ghc-devs@haskell.org > > http://www.haskell.org/mailman/listinfo/ghc-devs >
_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://www.haskell.org/mailman/listinfo/ghc-devs
