[mercury-users] IO in nondet or semidet functions

[Fergus Henderson]

On 13-Oct-2003, Aditya Raj PATHANIA <adityarp at students.cs.mu.OZ.AU> wrote:
>   presently i'm writing an fd solver in mercury.

Great!  One thing that you should be aware of is that the current support
for constraint solving in Mercury (in particular the support for dynamic
modes) is not yet documented in the Mercury language reference manual.

There are however some examples of how to write constraint solvers in
Mercury, e.g. extras/clpr in the mercury-extras distribution.

The most important point is that for constrained variables, you should
use the inst "any".

> the problem i'm facing is
> that i need to generate multiple solutions, using labeling. since labeling
> is almost always a nondet function (i guess), i'm unable to do IO using
> mercury's io__write and io__print, since mercury does not backtrack over
> IO.

The solution here is to use the all-solutions predicates in the std_util
library module, e.g. unsorted_aggregate or do_while.  These allow you to
interleave computing new solutions with performing I/O, while preserving
a proper declarative semantics.

>   my labeling procedure is simply this...
> 
> :- pred labeling(list(int)).
> :- mode labeling(in) is nondet.

That should probably be

	:- solver type fd_var.

	:- pred labeling(list(fd_var)).
	:- mode labeling(list_skel(any) >> ground) is nondet.

If you declare the mode as "in", then the procedure has no output
arguments, so it could not have more than one solution -- the Mercury
compiler would automatically prune away any additional solutions.  That is
not what you want.  So you need to use the "any" inst.

You will also need to use a separate abstract type, which I have here
named "fd_var", rather than using "int", because

(The "solver" prefix on the type declaration is only needed for and
only works with quite recent release-of-the-day releases of Mercury;
for earlier releases, it should be omitted.)

> labeling(Thelist) :-
> (
> 		Thelist = [],
> 		solver_print_all_variables, % this is a C procedure which
> i want to replace with io__print or io__write
> 		all_solns % this just makes the clause fail or succeed
> depending on whether i want to generate multiple soltuions
> 	;
> 		Thelist = [V|Vs],
> 		solver_min_domain(V,Min),
> 		solver_max_domain(V,Max),
> 		(if Min = Max then
> 			labeling(Vs)
> 		else
> 			label(V,Min,Vs)
> 		)
> ).

This sort of thing can be done using unsorted_aggregate/2 like so:

	:- pred print_labeling(list(fd_var), io__state, io__state).
	:- mode print_labeling(in(list_skel(any)), di, uo) is cc_multi.

	print_labeling(Vars) -->
		unsorted_aggregate(labeling, print_solution).

	:- pred print_solution(list(fd_var), io__state, io__state).
	:- mode print_solution(in, di, uo) is det.

	print_solution(VarS) --> ...

	:- pred labeling(list(fd_var), list(fd_var)).
	:- mode labeling(in(list_skel(any)), out) is nondet.

If you want to stop in the middle rather than processing all solutions,
you can use do_while rather than unsorted_aggregate.

Enclosed below is a more complete example module.

	:- module solv.
	:- interface.
	:- import_module io, list, int.

	% :- type fd_var.	% For Mercury versions < rotd-25-07-03
	:- solver type fd_var.  % For Mercury versions > rotd-25-07-03

		% initialize an unconstrained fd_var
	:- pred init_any(fd_var).
	:- mode init_any(free >> any) is det.

		% unify an fd_var with an int
	:- pred fd_var == int.
	:- mode in == out is det.
	:- mode (any >> ground) == in is semidet.

		% constrain an fd_var to be greater than the specified int
	:- pred fd_var > int.
	:- mode in(any) > in is semidet.

		% constrain an fd_var to be less than the specified int
	:- pred fd_var < int.
	:- mode in(any) < in is semidet.

		% Given a list of constrained fd_vars, nondeterminstically
		% find bindings for the variables that meet those constraints.
		% The output list here will be the same as the input list,
		% but with ground values for all the variables.
	:- pred labeling(list(fd_var), list(fd_var)).
	:- mode labeling(in(list_skel(any)), out) is nondet.

		% Given a list of constrained fd_vars, 
		% print out all possible bindings for the variables
		% that meet those constraints.  The order in which
		% the solutions will be printed is unspecified.
	:- pred print_labeling(list(fd_var), io__state, io__state).
	:- mode print_labeling(in(list_skel(any)), di, uo) is cc_multi.

	:- implementation.
	:- import_module std_util.

	:- solver type fd_var
		---> fd_var(c_pointer).

	print_labeling(Vars) -->
		unsorted_aggregate(labeling(Vars), print_solution).

	:- pred print_solution(list(fd_var), io__state, io__state).
	:- mode print_solution(in, di, uo) is det.

	print_solution(Vars) -->
		io__print("Here's a solution: "),
		io__write_list(Vars, ", ", print_var),
		io__nl.

	:- pred print_var(fd_var, io__state, io__state).
	:- mode print_var(in, di, uo) is det.
	print_var(Var) -->
		{ Var == Val }, % convert ground fd_var to int
		io__write_int(Val).

	labeling([], []).
	labeling([V | Vs0], [V | Vs]) :-
		label(V),
		labeling(Vs0, Vs).

	:- pred label(fd_var).
	:- mode label(any >> ground) is nondet.
	:- pragma promise_pure(label/1).
	
	label(V) :-
		impure solver_min_domain(V, Min),
		impure solver_max_domain(V, Max),
		(if Min = Max then
			promise_ground(V)
		else
			( V == Min
			; V > Min,
			  label(V)
			)
		).

	:- pred promise_ground(fd_var).
	:- mode promise_ground(any >> ground) is det.

	:- pragma foreign_proc("C", promise_ground(X :: any >> ground),
		[promise_pure, will_not_call_mercury, thread_safe],
		"/* assert(X->min == X->max); */").

	:- impure pred solver_min_domain(fd_var, int).
	:-        mode solver_min_domain(in(any), out) is det.

	:- impure pred solver_max_domain(fd_var, int).
	:-        mode solver_max_domain(in(any), out) is det.

	% Implementing the following is left as an exercise for the reader...
	:- external(init_any/1).
	:- external(solver_min_domain/2).
	:- external(solver_max_domain/2).
	:- external((==)/2).
	:- external((>)/2).
	:- external((<)/2).

(Note that the compiler will issue a warning about infinite recursion in
label/1; this warning is spurious, and can be safely ignored.)

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------