for review: allow `any' insts as non-local vars in higher-order terms

[Fergus Henderson]

On 15-Feb-1998, Andrew Bromage <bromage at cs.mu.OZ.AU> wrote:
> G'day all.
> 
> Fergus Henderson wrote:
> 
> > Comments, please?
> > Andrew, is this OK with you?
> 
> Seeing as we have to revisit this stuff sooner or later anyway, and
> playing with `any' isn't actually unsound in our implementation, we
> might as well do this now.

Actually playing around with `any' *is* unsound in our implementation.
For example, if you compile the following module with `-O-1',

	:- module bug.
	:- interface.
	:- import_module io.
	:- pred main(state::di, state::uo) is det.
	:- implementation.
	:- import_module var.
	main -->
		( { init(X), \+ q(X), X = var(43) } ->
			print("this should not happen!"), nl
		;
			print("ok"), nl
		).

	:- pred q(var(int)).
	:- mode q(in(any)) is semidet.
	q(X) :-
		\+ call(((pred) is semidet :- X = var(42))).

then the resulting executable will print out "this should not happen!",
which it should not.

(If you don't disable optimization, then inlining and double-negation 
elimination eliminate the problem, and it will print out "ok".)

> However, I think you should also add some documentation to the definition
> of freeze to say that the idiom may be revisited at some point in the
> future.

Good idea.

extras/trailed_update/var.m:
	Document that the interface to freeze/{2,3} is not stable.

cvs diff  extras/trailed_update/var.m
Index: extras/trailed_update/var.m
===================================================================
RCS file: /home/mercury1/repository/mercury/extras/trailed_update/var.m,v
retrieving revision 1.10
diff -u -r1.10 var.m
--- var.m	1998/02/14 15:06:41	1.10
+++ var.m	1998/02/15 21:20:59
@@ -10,8 +10,14 @@
 %
 % This module provides constraint solving for unification constraints;
 % in other words, it provides Prolog-style variables.
+%
 % It also provides some features for delaying (a.k.a dynamic scheduling,
-% or corouting), specifically freeze/2 and freeze/3.
+% or corouting), specifically freeze/2 and freeze/3.  However, this
+% interface is not yet stable; it may undergo significant changes,
+% or even be removed, in future releases.  (The reason for this is
+% that there are some problems with mode checking higher-order terms
+% containing non-local vars whose inst is `any', and we have not yet
+% solved those problems.)
 %
 % There is no occurs check -- this module does not provide Herbrand terms.
 % Values of type var/1 may be cyclic.  However, the solver not complete
@@ -57,10 +63,12 @@
 	% until a variable is ground.
 	% Often the freeze/3 version is more useful, though,
 	% since this version doesn't allow `Pred' to have any outputs.
-	% (XXX the compiler doesn't check that yet - this is a bug!)
+	% (XXX the compiler doesn't always check that yet - this is a bug!)
 	% Declaratively, freeze(Var, Pred) is true iff Pred(Var) is true.
 	% Operationally, freeze(Var, Pred) delays until Var becomes ground
 	% and then calls Pred(Var).
+	% Warning: the interface to this predicate may be modified in
+	% future releases.
 :- pred freeze(var(T), pred(T)).
 :- mode freeze(in(any), pred(in) is semidet) is semidet.
 :- mode freeze(out(any), pred(in) is semidet) is semidet.
@@ -72,6 +80,8 @@
 	% Declaratively, freeze(X, Pred, Y) is true iff Pred(X, Y) is true.
 	% Operationally, freeze(X, Pred, Y) delays until X becomes ground
 	% and then calls Pred(X, Y).
+	% Warning: the interface to this predicate may be modified in
+	% future releases.
 :- pred freeze(var(T1),  pred(T1, T2), var(T2)).
 :- mode freeze(in,	 pred(in, out) is det, out) is semidet. % really det
 :- mode freeze(in,	 pred(in, out) is semidet, out) is semidet.

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