[mercury-users] impure predicates

[Fergus Henderson]

Henk Vandecasteele <Henk.Vandecasteele at cs.kuleuven.ac.be> wrote:
> Ralph Becket wrote:
> > Backtracking over impure operations also sounds rather dodgy to me -
> > what are you trying to do?
> 
> I'm still porting a finite domain solver to mercury. I have already a 
> version using an input and output representing the state of the world.

In this case it is really the state of the _constraint store_
that you are interested in.

> For effiency reasons I use backtrackable destructive assignment 
> for updating the information about finite domain-variables.
> When implementing this stuff it is far more easy to store the
> information IN the finite domain variable.

Yes, indeed.  The same technique is used in extras/trailed_update/var.m
(a module in the mercury-extras distribution which provides
some support for "unification constraints", i.e. Prolog-style variables).

> As a result some predicates have no output arguments, ... .

You should probably be using a mode such as `any -> any',
rather than `in' plus `impure'; if you used `any' insts,
the compiler would not insert any pruning over that.

In general when building constraint solvers, there are two different
levels of abstraction that you want to use.  For users of the
constraint solver, you want a high level of abstraction;
generally want to the constraint store to be implicit,
and you should use `any' insts for variables which are constrained:

	:- module constraint_solver.
	:- interface.

		% this is the type which your constraint solver works on
	:- type constrained_var.

		% the predicate some_constraint/1 is just an example of
		% a predicate which adds a constraint on a variable
	:- pred some_constraint(constrained_var).
	:- mode some_constraint(free -> any) is det.
	:- mode some_constraint(any -> any) is semidet.

At the implementation level, you're dealing with backtrackable (trailed)
destructive update.  If you are actually interfacing to a solver written in
another language, then you can just use `pragma import' or `pragma c_code'
to implement each mode of the constraint predicates, and be done with it.

However, you may wish to implement the solver in Mercury too.
At first glance, it may seem that the solver implementation is
necessarily impure.  However, in fact much of the implementation
level can be pure too.  If you want to make the implementation level
pure, then its interface should look something like the following:

	:- implementation.

	:- pred some_constraint_impl_1(constrained_var_ptr,
				constraint_store, constraint_store).
	:- mode some_constraint_impl_1(out, mdi, muo) is det.

	:- pred some_constraint_impl_2(constrained_var_ptr,
				constraint_store, constraint_store).
	:- mode some_constraint_impl_2(in, mdi, muo) is semidet.


Note that
    (1) the constraint store has been made explicit, with mdi/muo modes
	to signify backtrackable destructive update;
    (2) we have a different predicate at the low level for each
	different mode of the high-level predicate; and
    (3) instead of passing arguments of type `constrained_var'
	with `any' insts, we pass arguments of type `constrained_var_ptr',
	which holds a pointer to the representation of the variable,
	with ground insts (i.e. modes `in' and `out').

The `constraint_store' type can be defined as an alias for the `store'
type defined in the standard library module `store';

	:- import_module store.

	:- type constraint_store == store(constraints).

There are primitives for doing backtrackable destructive update on stores
in the module extras/trailed_update/tr_store.m.
(The `constraints' type here is just a dummy type:

	:- type constraints ---> constraints.

The parameter `S' in the `store(S)' and `mutvar(T, S)' types defined
in store.m is used to ensure static type safety of certain operations
on stores, to avoid the need for any run time checking.)

The `constrained_var_ptr' type can then be defined as a `mutvar'
or `ref' type that points to a `constrained_var_rep' type,
which holds the actual representation (which can be anything you want),
e.g.

	:- type constrained_var_ptr ==
		mutvar(constrained_var_rep, constraints).

You can then use the operations in tr_store, such as `tr_store__get_mutvar'
and `tr_store__set_mutvar', to perform backtrackable destructive update
on the variable's representation.

So the only part that needs to be impure is the interface layer
which connects the high-level and the low-level views. 
The simplest way of doing this is to use `pragma import' and `pragma export':

	:- pragma import(some_constraint(free->any), "some_constraint_impl_1").
	:- pragma import(some_constraint(any->any), "some_constraint_impl_2").

	:- pragma export(some_constraint_impl_1(out, mdi, muo),
			"some_constraint_impl_1").
	:- pragma export(some_constraint_impl_2(in, mdi, muo),
			"some_constraint_impl_2").

An alternative but significantly more complicated method is as follows.
This method is slightly more efficient, in case you want to squeeze
out every possible ounce of performance ;-)

	:- pragma promise_pure(some_constraint/1).
	some_constraint(Var) :-
		impure get_constraint_store(Store0),
		impure is_bound(Var, IsBound),
		( IsBound = 0,
			some_constraint_impl_2(VarRep, Store0, Store),
			impure set_var_rep(VarRep, Var)
		; IsBound = 1,
			impure get_var_rep(Var, VarRep),
			some_constraint_impl_1(VarRep, Store0, Store)
		),
		impure save_constraint_store(Store).

Here the impure procedure `is_bound' is used to select between
different modes.  This is a bit like var/1 in Prolog.
It can be implemented using the C interface, as shown below.
In fact, however, most of the work is really done at compile time.

	:- impure pred is_bound(T, int).
	:- mode is_bound(free -> free, out(bound(0))) is det.
	:- mode is_bound(any -> any, out(bound(1))) is det.

	:- pragma c_code(is_bound(_Var::free->free, Bound::out(bound(0))),
		will_not_call_mercury, "Bound = 0;").
	:- pragma c_code(is_bound(_Var::any->any, Bound::out(bound(1))),
		will_not_call_mercury, "Bound = 1;").

The impure procedures `get_constraint_store', and `save_constraint_store'
are just NOPs, operationally, while `get_var_rep' and `set_var_rep'
are just casts; their purpose is just to convert between the high-level view
and the low-level view.  Their implementations are pretty trivial:

	:- impure pred get_constraint_store(constraint_store::muo) is det.
	:- impure pred save_constraint_store(constraint_store::mdi) is det.
	:- impure pred get_var_rep(constrained_var::any->any,
			constrained_var_ptr::out) is det.
	:- impure pred set_var_rep(constrained_var_ptr::in,
			constrained_var::free->any) is det.

	:- pragma c_code(get_constraint_store(_S0::muo),
		will_not_call_mercury, "").
	:- pragma c_code(save_constraint_store(_S0::mdi),
		will_not_call_mercury, "").
	:- pragma c_code(get_var_rep(Var::any->any, VarRep::out),
		will_not_call_mercury, "VarRep = Var;").
	:- pragma c_code(set_var_rep(VarRep::in, Var::free->any),
		will_not_call_mercury, "Var = VarRep;").

Note that the reason `get_constraint_store' need not actually
initialize its argument is that variables of type `store(S)'
have no actual run-time representation; like `io__state', they
just serve as place-markers to ensure referential transparency.

In theory, the Mercury compiler could optimize all that stuff away
entirely.  The current Mercury compiler is able to do a reasonable but
not perfect job of optimizing away most of the overhead for those
procedures.  What's left over is about the same as the cost of a
(non-inline non-tail-call) procedure call.  Using `pragma import' and
`pragma export' costs about twice as much.  (These figures are
guestimates, really -- I haven't run any benchmarks.)

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.