Type checker plugins

[Iavor Diatchki]

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.diatchki at gmail.com>
wrote:

> Hello,
>
> On Thu, Oct 16, 2014 at 3:58 AM, Adam Gundry <adam at 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/
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20141018/e4b79ce0/attachment.html>