[m-dev.] Re: [HAL-dev] Adding Herbrand types to Mercury

[Ralph Becket]

Having done some more homework and experimenting, I've come up with a
concrete plan.


(1) Solver types in Mercury

Solver types are provided to support the implementation of constrained
types such as constrained integers, partial orders and so forth.
Implementation of solver types inevitably involves some impure coding
behind the scenes to implement constraint stores and the like.

The syntax for solver type definitions will be as follows:

:- solver type <typename>
	where initialisation is <initpred>, unification is <unifypred>.

Calls to <initpred> are inserted during mode analysis to convert
variables free >> any where necessary.

Calls to <unifypred> are used to unify variables of the solver type (the
only mode is <unifypred>(in(any), in(any)) is semidet.)

Any view of values of the solver type must be provided by predicates in
the solver type's defining module.

Rather than make a special case of having an "internal" view of the
solver type (e.g. an int or a c_pointer or whatever) vs an "external"
view (i.e. the solver type itself), solver type implementors will have
to define their own conversion functions, e.g.

:- func convert(<internaltype>) = <solvertype>.
:- mode convert(out)            = in(any)  is det.
:- mode convert(in)             = out(any) is det.

:- pragma foreign_code(
	"C",
	convert(A::out) = (B::in(any)),
	[will_not_call_mercury, promise_pure],
	"A = B;"
).

:- pragma foreign_code(
	"C",
	convert(A::in) = (B::out(any)),
	[will_not_call_mercury, promise_pure],
	"B = A;"
).

[The HAL approach is to make the compiler aware of the distinction
between internal and external representations of solver types, so the
programmer doesn't have to use things like convert/1.  We can add
syntactic sugar for this sort of thing later if the convert/1 approach
proves too cumbersome in practice.]


TODO:
- Support the new syntax.
- Record the <initpred> and <unifypred> info somewhere in the HLDS.
- Get mode analysis to schedule calls to <initpred> and <unifypred>.
- I think that's it.


(2) Herbrand types in Mercury

Herbrand types are a special kind of solver type supporting Prolog
style unification.

The syntax for Herbrand type definitions will be as follows:

:- herbrand type <typename> ---> <du constructors>.

Herbrand types have private builtin <initpred> and <unifypred>
definitions with signatures

:- pred init_Herbrand(T::out(any)) is det.

:- pred unify_Herbrand(T::in(any), T:in(any)) is semidet.

The unification procedure generated for <typename> is almost identical
to what would be generated if it were an ordinary du type, with the
exception that unify_Herbrand/2 is called where one or both of the
variables being unified is "unbound" (i.e. has been initialised, but is
not currently bound to a ground value.)

Scheduling of the Herbrand unification X = Y works as follows:

inst(X) | inst(Y) | scheduled goal
--------+---------+----------------
free    | free    | <<unification deferred until X or Y becomes non-free>>
free    | any     | assign X := Y
--------+---------+----------------
any     | free    | assign Y := X
any     | any     | unify(X, Y)

Scheduling of the Herbrand unification X = f(Y, ...) (for some data
constructor f) works as follows:

inst(X) | inst(Y, ...) | scheduled goals
--------+--------------+----------------
free    | some or all  | init_Herbrand(V), ...,   [for each free V in Y, ...]
        | free         | construct X = f(Y, ...)
--------+--------------+----------------
any     | some or all  | init_Herbrand(V), ...,   [for each free V in Y, ...]
        | free         | construct Z = f(Y, ...)  [for some new variable Z  ]
        |              | unify(X, Z)

The unification procedure for Herbrand types handles unification of
any "unbound" value (i.e. with the reserved tag) by calling
unify_Herbrand which handles that side of things.

TODO:
- Support for the syntax is already there.
- Add init_Herbrand and unify_Herbrand to private_builtin.m.
- Adapt unify_proc.m to generate calls to unify_Herbrand when it sees
  the reserved tag on Herbrand types.
- Adapt goal scheduling to handle Herbrand types.
- I think that's it.


If anyone can see any howlers in there, please let me know.

-- Ralph
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------