[m-dev.] Resources example
Peter Schachte
schachte at cs.mu.OZ.AU
Fri Apr 22 17:45:13 AEST 2005
Hi all,
I've rewritten Ralph's simple example partial order solver using
resources, to see how much it simplified the code. It does simplify
it significantly, though some impurity remains. Here's my annotated
rewrite:
================================================================
% A partial order vertex type supporting unification and ordering
% constraints. Written to conserve space on the page.
:- module po_solver.
:- interface.
:- solver type po_vertex.
:- pred init(po_vertex::oa) is det.
:- pred eq(po_vertex::ia, po_vertex::ia) is semidet.
:- pred (po_vertex::ia) =< (po_vertex::ia) is semidet.
:- pred (po_vertex::ia) < (po_vertex::ia) is semidet.
:- implementation.
:- import_module counter, eqvclass, list, ref, svset.
:- solver type po_vertex where representation is vertex,
initialisation is init,
equality is eq.
:- type cstore ---> cs(counter, set(constraint)).
:- type constraint ---> lt(vertex, vertex) ; le(vertex, vertex).
:- type vertex == int.
:- type path_kind ---> nonstrict ; strict.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
First change: declare two resources, one holding the constraint
store, as a set of constraints, and the other holding a counter used
to generate variable numbers. Then we declare that the predicates
exported above are actually implemented using these resources. But
this promises that the interface is pure outside this module.
Note there's no longer a need for tabling a function and *depending*
on it never being recomputed (ie, lying to the compiler).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
:- resource po_store : set(constraint) = empty.
:- resource var_supply : int = 0.
:- pred init/1 using var_supply promise commutative.
:- pred eq/2 using tell(po_store).
:- pred (=<)/2 using tell(po_store).
:- pred (<)/2 using tell(po_store)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
The previous code for these predicates used to have a lot more
impurity for grabbing the current counter and store, and for putting
them back. The only remaining impurity is for converting between
po_vertex and vertex types.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
init(A) :-
counter.supply_next(X, !var_supply),
promise_pure(impure A = 'representation to any po_vertex/0'(X)).
eq(A, B) :-
promise_pure (impure X = 'representation of any po_vertex/0'(A),
impure Y = 'representation of any po_vertex/0'(B)),
( if path(X, Y, [], nonstrict)
then path(Y, X, [], nonstrict)
else not path(X, Y, [], strict),
svset.insert(le(Y,X), !po_store),
svset.insert(le(X,Y), !po_store)
).
A =< B :-
promise_pure (impure X = 'representation of any po_vertex/0'(A),
impure Y = 'representation of any po_vertex/0'(B)),
( if path(X, Y, [], _)
then true
else not path(Y, X, [], strict),
svset.insert(le(X,Y), !po_store)
).
A < B :-
promise_pure (impure X = 'representation of any po_vertex/0'(A),
impure Y = 'representation of any po_vertex/0'(B)),
( if path(X, Y, [], strict)
then true
else not path(Y, X, [], _),
svset.delete(le(X,Y), !po_store),
svset.insert(lt(X,Y), !po_store)
).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Although the set of constraints is unchanged by this code, it still
makes this code a bit simpler to treat the store as a resource. Since
we don't change it, it's a read-only resource.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
:- pred path(vertex::in, vertex::in, list(vertex)::in, path_kind::out)
using !.po_store is semidet.
path(X, X, _Path, nonstrict).
path(X, Y, Path, strict) :-
member(lt(X, Z), !.po_store),
path(Z, Y, [X | Path], _).
path(X, Y, Path, PathKind) :-
member(le(X, Z), !.po_store),
not member(Z, Path),
path(Z, Y, [X | Path], PathKind).
================================================================
I'm not very happy with the impurity that's still there, though.
Since it only exists for converting between a solver type and its
representation, it occurred to me that we could make a small extension
to the solver type declaration to allow the user to specify predicates
whose solver type arguments should be converted to/from representation
type when they are called. That is, their pred/func declarations
mention solver types, but their actual implementations work on the
implementation types. By doing this, the programmer solemnly promises
that these predicates would behave identically for any representation
of an equal solver variable.
So the solver type declaration might look like:
:- solver type po_vertex where representation is vertex,
initialisation is init,
equality is eq
converting (=<)/2,(<)/2.
And then the code becomes much simpler looking:
init(X) :-
counter.supply_next(X, !var_supply).
eq(X, Y) :-
if path(X, Y, [], nonstrict)
then path(Y, X, [], nonstrict)
else not path(X, Y, [], strict),
svset.insert(le(Y,X), !po_store),
svset.insert(le(X,Y), !po_store).
X =< Y :-
if path(X, Y, [], _)
then true
else not path(Y, X, [], strict),
svset.insert(le(X,Y), !po_store).
X < Y :-
if path(X, Y, [], strict)
then true
else not path(Y, X, [], _),
svset.delete(le(X,Y), !po_store),
svset.insert(lt(X,Y), !po_store).
With the rest of the code unchanged.
How does this look?
--
Peter Schachte American business needs a lifting purpose greater
schachte at cs.mu.OZ.AU than the struggle of materialism.
www.cs.mu.oz.au/~schachte/ -- Herbert Hoover
Phone: +61 3 8344 1338
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------
More information about the developers
mailing list