[mercury-users] Getting 'any' insts to ground

[Fergus Henderson]

Bas de Bakker wrote:
> I've been experimenting a bit with the new 'any' inst, but I'm running
> into the following problem:
> 
> Let's say I have
> 
> :- pred fill_list(list(int)).
> :- mode fill_list(list_skel(any) -> list_skel(any)) is nondet.

That doesn't quite make sense, because the type `int' has
no representation for the inst `any'.  Perhaps you meant

	:- pred fill_list(list(var(int))).

?

> I know that each successful call of fill_list will instantiate exactly
> one element of the list, but which one will be hard to predict (and
> vary when backtracking).
> 
> If I have a list of length N with free variables for all elements, I
> can call fill_list N times in a simple recursive predicate.  When I've
> done this I know that the list is ground, but the compiler doesn't.
> But to do something useful with the list, like print it, the compiler
> must know it is ground.
> 
> In extras/trailed_update/unsafe, there's an "unsafe_promise_ground"
> predicate which does what I need, but it's unsafe and can't test
> whether my algorithm is correct.  I'd like something along the lines
> of
> 
> :- pred is_ground(T).
> :- mode is_ground(any -> ground) is semidet.
> 
> which fails if the term isn't ground, but this is non-logical.
> Is there any (logical) way to do this, either in the current Mercury
> implementation or just potentially, or is it simply impossible?

What's your aim -- do you (a) want your algorithm to be able to handle
the case where the variable turns out not to be ground, or (b) do you
expect that the variable will always be ground, but want to ensure that
if you make a mistake, then the error will be detected at runtime?

Both of these aims can be achieved using predicates that have
a logical interface with a proper declarative semantics.
Currently the Mercury library packages which provide support 
for `any' insts (namely the `cfloat' and `var' packages)
do not provide the necessary primitives, but they are easy to
implement.


Case (a):

For the first aim (algorithms that do different things depending on
whether a value is ground or not), to make it logical, you need to use
`cc_multi'.  For example:

	:- pred is_ground(var(T), maybe(T)).
	:- mode is_ground(in(any), out) is cc_multi.

Declaratively, is_ground(Var, Result) is true iff
either Result = no or Var = var(Value) and Result = yes(Value);
that is, its declarative semantics are equivalent to the semantics
specified by the following clauses:

	is_ground(var(Value), yes(Value)).
	is_ground(_, no).

Operationally, is_ground(Var, Result) returns Result = no
if Var is non-ground, and Result = yes(Value) if Var is ground;
that is, execution will select the first clause if the variable
is ground, and the second clause if the variable is non-ground.

At the end of this mail is a patch to extras/trailed_update/var.m
which adds such a predicate; this will probably also be included
in the next release.


Case (b):

The predicate cfloat__get_val in extras/clpr/cfloat.m is an example of
the second aim (detecting errors at runtime).

	:- pred cfloat__get_val(cfloat, float).
	:- mode cfloat__get_val(any -> any, out) is cc_multi.

Declaratively, cfloat__get_val(X, Y) is true iff Y and X have the same
value.  Operationally, cfloat__get_val(X, Y) succeeds only if Y is the
only value which the solver variable X can take, given the constraints
on X; if there is no unique value for X, then the predicate will abort
at runtime.

[In the current distribution, cfloat__get_val/2 is declared `det',
rather than `cc_multi', but (as explained below) that is a bug.]

This could be done for the var/1 type too:

	:- pred var__get_val(var(T), T).
	:- mode var__get_val(any -> any, out) is cc_multi.

	% Declaratively, var__get_val(X, Y) is true iff Y = var(X).
	% Operationally, cfloat__get_val(X, Y) succeeds only if Y is ground;
	% if Y is non-ground, it will abort.

	var__get_val(Var, Value) :-
		is_ground(Var, MaybeValue),
		( MaybeValue = yes(V) ->
			Value = V
		;
			error("var__get_val: variable not ground"), fail
		).


OK, that was the good news.  Now for the bad news ;-)
The var__get_val/2 predicate lets you convince the compiler that a variable
is ground, with this assertion being checked at runtime.
However, in the case where the variable is non-ground,
declaratively speaking var__get_val/2 can have multiple solutions,
even though operationally it just calls error/1.
Thus it needs to be `cc_multi', and so depending on the context in
which get_val/2 is used, you may now need to convince
the compiler that the goal will only have one solution.
In other words, we've fixed one problem, but we may have introduced another.

Fortunately there are a number of different solutions to this problem
of calling cc_multi predicates from a det context, as has been
discussed in detail in recent mail to mercury-users.  I haven't
investigated how well they work in these sort of cases, however.

Cheers,
	Fergus.


Index: var.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/extras/trailed_update/var.m,v
retrieving revision 1.6
diff -u -u -r1.6 var.m
--- var.m	1997/10/12 13:32:51	1.6
+++ var.m	1997/11/10 10:49:50
@@ -97,6 +97,22 @@
 	% dump_var prints out a representation of a variable.
 :- pred dump_var(var(T)::in(any), io__state::di, io__state::uo) is cc_multi.
 
+	% var__is_ground/2 can be used to test if a variable is ground.
+	%
+	% Declaratively, is_ground(Var, Result) is true iff
+	% either Result = no or Var = var(Value) and Result = yes(Value);
+	% that is, it is equivalent to the following clauses:
+	%
+	%	is_ground(var(Value), yes(Value)).
+	%	is_ground(_, no).
+	%
+	% Operationally, is_ground(Var, Result) returns Result = no
+	% if Var is non-ground, and Result = yes(Value) if Var is ground;
+	% that is, execution will select the first clause if the variable
+	% is ground, and the second clause if the variable is non-ground.
+
+:- pred is_ground(var(T)::in(any), maybe(T)::out) is cc_multi.
+
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
 :- implementation.
@@ -322,6 +338,32 @@
 		wakeup_delayed_goals(DelayedGoals, Value)
 	).
 
+:- pragma c_code( is_ground(Var::in(any), Result::out) /* cc_multi */,
+	may_call_mercury,
+"
+	ML_var_is_ground(TypeInfo_for_T, Var, &Result);
+").
+
+:- pred var__rep_is_ground(var_rep(T), maybe(T)).
+:- mode var__rep_is_ground(in(ptr(var_rep_any)), out) is det.
+:- pragma export(var__rep_is_ground(in(ptr(var_rep_any)), out),
+	"ML_var_is_ground").
+var__rep_is_ground(VarPtr, Result) :-
+	VarPtr = alias(Var),
+	( 
+		Var = alias(_),
+		var__rep_is_ground(Var, Result)
+	;
+		Var = ground(Value),
+		Result = yes(Value)
+	;
+		Var = free,
+		Result = no
+	;
+		Var = free(_DelayedGoals),
+		Result = no
+	).
+
 %-----------------------------------------------------------------------------%
 
 %

-- 
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.