implementation of `freeze' (coroutining)

[Fergus Henderson]

Hi,

Here's an implementation of freeze/2 in Mercury,
and a coroutining Mercury version of N-queens that uses it.

Bugs: this implementation does not detect floundering.
(Not too hard to add, although it will add 

-----------------------------------------------------------------------------
:- module var.
:- interface.

:- type var(T).

	% `init(Var)' can be used to initialize
	% the inst of a variable to `any'.
:- pred init(var(T)::out(any)) is det.

	% `Var = var(Value)' unifies a variable with its value.
	% This can be used in several ways:
	% to bind a variable to a particular value, `X = var(42)';
	% to extract the value of that variable, `X = var(Y)';
	% or (NYI) to initialize the inst of a variable to any, `X = var(_)'.
:- func var(T) = var(T).
:- mode var(in) = out is det.
:- mode var(in) = in(any) is semidet.
:- mode var(in) = in is semidet.
:- mode var(out) = in is det.
% :- mode var(free -> clobbered_any) = out(any) is det. % NYI

	% `Var1 == Var2' can be used to unify two variables.
:- pred var(T) == var(T).
:- mode in == in is semidet.
:- mode in == out is det.
:- mode out == in is det.
:- mode in(any) == in(any) is semidet.
:- mode in(any) == out(any) is det.
:- mode out(any) == out(any) is det.
:- mode out(any) == in(any) is det.

	% `freeze(Var, Pred)' can be used to delay execution of a goal
	% 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!)
	% 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).
:- 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.

/*****
NOT YET IMPLEMENTED -- the implementation requires existential types.
	% `freeze(Var1, Pred, Var2)' can be used to delay
	% execution of a goal until a variable is ground.
	% This version is more flexible than freeze/2, since
	% it allows the delayed goal to have an output.
	% 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).
:- pred freeze(var(T1), pred(T1, T2), var(T2)).
:- mode freeze(in(any), pred(in, out) is semidet, in(any)) is semidet.
:- mode freeze(out(any), pred(in, out) is det, out(any)) is semidet.

******/

%---------------------------------------------------------------------------%
:- implementation.
:- import_module list.
%---------------------------------------------------------------------------%
%
% The implementation is mostly written in Mercury
% (the exception being setarg/3).
% Apart from setarg/3, the C interface is used only
% as a means of providing different implementations
% for different modes of a predicate and for doing
% unchecked type casts (and inst/mode casts).
%
%---------------------------------------------------------------------------%


:- pragma c_header_code("
/* XXX should change the name in runtime/mercury_trail.h */
#ifndef MR_trail_current_value
  #define MR_trail_current_value(addr) MR_trail_value_at_address((addr))
#endif

/* XXX this should go in runtime/tags.h */
#ifndef strip_tag
  #ifdef HIGH_TAGS
    #define strip_tag(w)	((w) & ((~(Word)0) >> TAGBITS))
  #else
    #define strip_tag(w)	((w) & ((~(Word)0) << TAGBITS))
  #endif
#endif
").

/* impure */
:- pred destructively_update_binding(var_rep(T), var_rep(T)).
:- mode destructively_update_binding(in(ptr(var_rep_any)), in(var_rep_any))
	is det.

destructively_update_binding(DereffedVar, NewBinding) :-
	setarg(DereffedVar, 1, NewBinding).

/*
** setarg/3 provides non-logical backtrackable destructive update.
**
** WARNING: setarg/3 uses side-effects and is not type-safe!
**          Also it does not work for types with exactly one
**	    functor that has exactly one arg.
**          Use only with great care!
*/
/* impure */
:- pred setarg(T1, int, T2).
:- mode setarg(in(any), in, in(any)) is det.
:- pragma c_code(
	setarg(MercuryTerm::in(any), ArgNum::in, NewValue::in(any)),
	will_not_call_mercury,
"{
	Word *ptr = (Word *) strip_tag(MercuryTerm); /* strip off tag bits */
	MR_trail_current_value(&ptr[ArgNum - 1]);
	ptr[ArgNum - 1] = NewValue;
}").

:- type var(T) ---> var_rep(var_rep(T))
	where equality is (==).

:- type var_rep(T)
	--->	free
	;	free(list(pred(T)))	% list of delayed goals
	;	alias(var_rep(T))
	;	ground(T).

:- inst var_rep_any =
	bound(	free
	;	free(list_skel(pred(in) is semidet))
	;	alias(var_rep_any)
	;	ground(ground)
	).
:- inst var_rep_ground =
	bound(	alias(var_rep_ground)
	;	ground(ground)
	).
:- inst var_rep_deref =
	bound(	free
	;	free(list_skel(pred(in) is semidet))
	;	ground(ground)
	).
:- inst ptr(I) = bound(alias(I)).
:- inst uniq_ptr(I) = unique(alias(I)).

%-----------------------------------------------------------------------------%

:- pragma c_code(init(Var::out(any)), may_call_mercury, "
	Var = ML_var_alias(TypeInfo_for_T, ML_var_free(TypeInfo_for_T));
").

/*
% the compiler generates wrong code for this --
% the output is not unique
:- pred var__rep_init(var_rep(T)::out(uniq_ptr(var_rep_any))) is det.
:- pragma export(var__rep_init(out(uniq_ptr(var_rep_any))), "ML_var_init").
var__rep_init(alias(free)).
*/

:- func var__rep_free = (var_rep(T)::out(var_rep_any)) is det.
:- pragma export(var__rep_free = out(var_rep_any), "ML_var_free").
var__rep_free = free.

:- func var__rep_alias(var_rep(T)::in(var_rep_any)) =
		(var_rep(T)::out(var_rep_any)) is det.
:- pragma export(var__rep_alias(in(var_rep_any)) = out(var_rep_any),
		"ML_var_alias").
var__rep_alias(T) = alias(T).

%-----------------------------------------------------------------------------%

/****
:- pragma c_code( var(Value::(free -> clobbered_any)) = (Var::out(any)), % det
	may_call_mercury,
"
	* Value unused *
	ML_var_init(&Var);
").
****/

:- pragma c_code( var(Value::in) = (Var::out) /* det */,
	may_call_mercury,
"
	ML_var_init_with_value(TypeInfo_for_T, Value, &Var);
").

:- pred var__rep_init_with_value(T::in, var_rep(T)::out(var_rep_ground)) is det.
:- pragma export(var__rep_init_with_value(in, out(var_rep_ground)),
	"ML_var_init_with_value").
var__rep_init_with_value(Value, ground(Value)).

:- pragma c_code( var(Value::out) = (Var::in) /* det */, may_call_mercury,
"
	ML_var_get_value(TypeInfo_for_T, Var, &Value);
").

:- pred var__rep_get_value(var_rep(T)::in(var_rep_ground), T::out) is det.
:- pragma export(var__rep_get_value(in(var_rep_ground), out),
	"ML_var_get_value").
var__rep_get_value(ground(Value), Value).
var__rep_get_value(alias(Var), Value) :-
	var__rep_get_value(Var, Value).

:- pragma c_code( var(Value::in) = (Var::in) /* semidet */,
	may_call_mercury,
"
	SUCCESS_INDICATOR = ML_var_test_value(TypeInfo_for_T, Var, Value);
").

:- pred var__rep_test_value(var_rep(T)::in(var_rep_ground), T::in) is semidet.
:- pragma export(var__rep_test_value(in(var_rep_ground), in),
	"ML_var_test_value").
var__rep_test_value(Var, Value) :-
	var__rep_get_value(Var, VarValue),
	Value = VarValue.

:- pragma c_code( var(Value::in) = (Var::in(any)) /* semidet */,
	may_call_mercury,
"
	SUCCESS_INDICATOR = ML_var_unify_with_val(TypeInfo_for_T, Value, Var);
").

:- pred var__rep_unify_with_val(T, var_rep(T)).
:- mode var__rep_unify_with_val(in, in(ptr(var_rep_any))) is semidet.
:- pragma export(var__rep_unify_with_val(in, in(ptr(var_rep_any))),
	"ML_var_unify_with_val").
var__rep_unify_with_val(Value, Var) :-
	deref_var(Var, DereffedVar),
	DereffedVar = alias(OldVarRep),
	( OldVarRep = ground(OldValue) ->
		Value = OldValue
	;
		var__rep_bind_var(OldVarRep, Value, NewVarRep),
		destructively_update_binding(DereffedVar, NewVarRep)
	).

:- pred var__rep_bind_var(var_rep(T)::in(var_rep_any), T::in,
				var_rep(T)::out(var_rep_ground)) is semidet.
var__rep_bind_var(free, Value, ground(Value)).
var__rep_bind_var(free(DelayedGoals), Value, ground(Value)) :-
	call_delayed_goals(DelayedGoals, Value).

%-----------------------------------------------------------------------------%

:- pred call_delayed_goals(list(pred(T)), T).
:- mode call_delayed_goals(in(list_skel(pred(in) is semidet)), in) is semidet.

call_delayed_goals([], _).
call_delayed_goals([Goal|Goals], Value) :-
	call_delayed_goals(Goals, Value),
	call(Goal, Value).

%-----------------------------------------------------------------------------%

	% Beware, the implementation of this is rather unsafe,
	% if the compiler does strange things... 
	% might be better to just implement it in C.
:- pred deref_var(var_rep(T), var_rep(T)).
:- mode deref_var(in(ptr(var_rep_any)), out(ptr(var_rep_any))).
			       % really out(ptr(var_rep_deref)).
deref_var(Var, DerefVar) :-
	Var = alias(Deref1),
	(if Deref1 = alias(_) then
		deref_var(Deref1, DerefVar)
	else
		DerefVar = Var
	).

%-----------------------------------------------------------------------------%

/*
:- 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.
*/

:- pragma c_code(
	freeze(Var::in(any), Pred::(pred(in) is semidet)) /* semidet */,
	may_call_mercury,
"
	ML_var_freeze_in(TypeInfo_for_T, Var, Pred);
").
:- pragma c_code(
	freeze(Var::out(any), Pred::(pred(in) is semidet)) /* semidet */,
	may_call_mercury,
"
	ML_var_freeze_out(TypeInfo_for_T, &Var, Pred);
").


:- pred var__rep_freeze_out(var_rep(T), pred(T)).
:- mode var__rep_freeze_out(out(ptr(var_rep_any)), pred(in) is semidet)
	is semidet.
:- pragma export(
	var__rep_freeze_out(out(ptr(var_rep_any)), pred(in) is semidet),
	"ML_var_freeze_out").

var__rep_freeze_out(Var, Pred) :-
	Var = alias(free([Pred])).

:- pred var__rep_freeze_in(var_rep(T), pred(T)).
:- mode var__rep_freeze_in(in(ptr(var_rep_any)), pred(in) is semidet) is semidet.
:- pragma export(
	var__rep_freeze_in(in(ptr(var_rep_any)), pred(in) is semidet),
	"ML_var_freeze_in").

var__rep_freeze_in(Var, Pred) :-
	deref_var(Var, DereffedVar),
	DereffedVar = alias(OldRep),
	( OldRep = ground(Value) ->
		call(Pred, Value)
	;
		( OldRep = free(OldPreds) ->
			NewPreds = [Pred | OldPreds]
		;
			NewPreds = [Pred]
		),
		NewRep = free(NewPreds),
		/* impure */ destructively_update_binding(DereffedVar, NewRep)
	).

%-----------------------------------------------------------------------------%

:- import_module require.
_ == _ :-
	error("var:'==' not yet implemented").

%-----------------------------------------------------------------------------%

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