[mercury-users] unification problem

[Fergus Henderson]

On 29-Apr-2004, Stefan Hinterstoisser <supersteveee at gmx.de> wrote:
> I have the following predicate:
> 
> :- pred konto( string, string, string, string ).
> :- mode konto( in, in, out, out ) is nondet.
> :- mode konto( out, in, out, out ) is nondet.
> :- mode konto( in,  out, out, out ) is nondet.
> :- mode konto( out, out, out, out ) is nondet.
> konto( "Vater", "Mutter", "true", "konto(Vater,Mutter);" ).
> konto( _, _, "false", "konto(false,false)" ).
> 
> what I want is that this predicate (although definied as nondet) behaves
> like a predicate that always becomes true (and gave true and konto(Vater,
> Mutter) back if it matches Vater and Mutter and else false and
> konto(false,false) ).

The specification that you give has an infinite number of solutions
in the cases where either the first or second argument has mode "out".

> unfortunatly the wildcards dont fit because of missing
> groundness (because of the mode definition).

Yes.  Mercury won't let you write a predicate with an infinite number
of solutions by just writing an underscore, since a predicate with
an infinite number of solutions is usually a bug.

> is there any way to get that
> demanded behavior I described before without changing the modes (and note:
> every mode type could also be used in the later program!)....

Yes. You could write the code so that it explicitly generates
an infinite number of solutions, like this:

	konto( "Vater", "Mutter", "true", "konto(Vater,Mutter);" ).
	konto( S1, S2, "false", "konto(false,false)" ) :-
		not ( S1 = "Vater", S2 = "Mutter" ),
		gen_string(S1),
		gen_string(S2).

where gen_string is defined as

	:- pred gen_string(string).
	:- mode gen_string(in) is semidet. % really det, actually
	:- mode gen_string(out) is nondet.
	gen_string(S) :-
		string.from_char_list(L, S),
		gen_char_list(L).

	:- pred gen_char_list(list(char)).
	:- mode gen_char_list(in) is semidet. % really det, actually
	:- mode gen_char_list(out) is nondet.
	gen_char_list([]).
	gen_char_list([C|Cs]) :- gen_char(C), gen_char_list(Cs).

	:- pred gen_char(char).
	:- mode gen_char(in) is semidet. % really det, actually
	:- mode gen_char(out) is nondet.
	gen_char(C) :-
		char.to_int(C, I),
		list.member(I, char.min_char_value `..` char.max_char_value),

However, any uses of gen_string in the (out) mode will lead to an infinite
number of solutions, which is probably not going to be helpful!

P.S.
For advanced students of Mercury, I should point out that it is possible
to use different clauses for different modes to implement this more
efficiently and with a more accurate determinism specification:

	:- pred gen_string(string).
	:- mode gen_string(in) is det.
	:- mode gen_string(out) is nondet.
	:- pragma promise_pure(gen_string/1).
	gen_string(_::in).
	gen_string(S::out) :-
		string.from_char_list(L, S),
		gen_char_list(L).

However, this technique should NOT be used unless the user is 100%
confident about the safety of the "promise_pure" annotation guaranteeing
that the different clauses have the same set of solutions, and it is
easy for novices to be wrong about that, so I do not recommend this
technique to novice users.

-- 
Fergus Henderson                    |  "I have always known that the pursuit
                                    |  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
--------------------------------------------------------------------------