[m-dev.] implementation of `freeze' (coroutining)

[Fergus Henderson]

Fergus Henderson, you wrote:
> 
> Here's an implementation of freeze/2 in Mercury,
> and a coroutining Mercury version of N-queens that uses it.

Sorry, that mail was incomplete (someone was rebooting mubboon, so I just
shot it off without finishing it).  Let me try again.

Here's the following:

	var.m: Prolog-style variables + freeze/2

	unsafe.m: unsafe_perform_io/1, setarg/3, and unsafe_cast_to_ground/1
		(these are used by var.m)

	vqueens.m: a coroutining N-queens problem implemented using var.m.

I plan to put the first two in extras/trailed_update,
and to put vqueens.m in a new subdirectory extras/trailed_update/samples.

TODO:
	- modify freeze/2 so that we detect floundering
	- implement var:'=='/2
	- implement freeze/3
	- improve documentation

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

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

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

	% `debug_freeze(Message, Var, Pred)'
	% is the same as `freeze(Var, Pred)' except
	% that it also prints out some debugging information.
	% IMPORTANT: this is a non-logical hack, use only for debugging!
:- pred debug_freeze(string, var(T), pred(T)).
:- mode debug_freeze(in, in(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, std_util.
:- import_module unsafe, io.

%---------------------------------------------------------------------------%
%
% The implementation is mostly written in Mercury, although we do use
% setarg/3 from the `unsafe' module.  The C interface is used only
% as a means of providing different implementations for different
% modes of a predicate and for doing unchecked type/inst casts to
% cast values of type and inst `var(T)::any' to `var_rep(T)::ground'
% and back again -- that is, to convert from variables to their concrete
% representation and back.
%
%---------------------------------------------------------------------------%

:- 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.
% It puts the `alias(free)' term in read-only memory.  Hence, to avoid this,
% we use separate calls to functions for alias/1 and free/0.
:- 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").

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

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

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

debug_freeze(Msg, Var, Pred) :-
	unsafe_perform_io(print("freezing: ")),
	unsafe_perform_io(print(Msg)),
	unsafe_perform_io(print(": ")),
	unsafe_perform_io(print_any(Var)),
	unsafe_perform_io(nl),
	( freeze(Var, debug_pred(Msg, Pred)) ->
		unsafe_perform_io(print("frozen: ")),
		unsafe_perform_io(print(Msg)),
		unsafe_perform_io(print(": ")),
		unsafe_perform_io(print_any(Var)),
		unsafe_perform_io(nl)
	;
		unsafe_perform_io(print("freeze failed: ")),
		unsafe_perform_io(print(Msg)),
		unsafe_perform_io(print(": ")),
		unsafe_perform_io(print_any(Var)),
		unsafe_perform_io(nl),
		semidet_fail
	).


:- pred debug_pred(string::in, pred(T)::(pred(in) is semidet), T::in)
	is semidet.

debug_pred(Msg, Pred, Var) :-
	unsafe_perform_io(print("woke: ")),
	unsafe_perform_io(print(Msg)),
	unsafe_perform_io(print(": ")),
	unsafe_perform_io(print(Var)),
	unsafe_perform_io(nl),
	( call(Pred, Var) ->
		unsafe_perform_io(print("succeeded: ")),
		unsafe_perform_io(print(Msg)),
		unsafe_perform_io(print(": ")),
		unsafe_perform_io(print(Var)),
		unsafe_perform_io(nl)
	;
		unsafe_perform_io(print("failed: ")),
		unsafe_perform_io(print(Msg)),
		unsafe_perform_io(print(": ")),
		unsafe_perform_io(print(Var)),
		unsafe_perform_io(nl),
		semidet_fail
	).

:- pred print_any(T::in(any), io__state::di, io__state::uo) is det.
print_any(X) -->
	print(unsafe_cast_to_ground(X)).

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

%-----------------------------------------------------------------------------%
:- module unsafe.
%-----------------------------------------------------------------------------%

/*
** WARNING: the procedures defined in this module are non-logical.
**          They may have side effects, they may violate type safety,
**	    they may interfere with certain memory management strategies,
**	    and in general they may do lots of nasty things.
**	    They may not work with future release of the Mercury compiler,
**	    or with other Mercury implementations.
**          Use only as a last resort, and only with great care!
**
** You have been warned.
*/

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

:- interface.
:- import_module io.

/*
** unsafe_perform_io/1 performs I/O, in an unsafe manner.
** It can be used to call a goal that does I/O or has
** side effects from a context where you do not have an io__state.
** It can be useful for printf-style debugging.
** But backtracking over a call to `unsafe_perform_io'
** can be very dangerous indeed, because with certain
** memory allocation policies it can result in dangling pointers.
*/
:- pred unsafe_perform_io(pred(io__state, io__state)).
:- mode unsafe_perform_io(pred(di, uo) is det) is det.
:- mode unsafe_perform_io(pred(di, uo) is cc_multi) is det.

/*
** setarg/3 provides non-logical backtrackable destructive update.
** `setarg(Term, N, Value)' destructively modifies the Nth
** argument of `Term' to be `Value'.  The modification will be undone
** on backtracking.
**
** 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.
**	    It may not work with future release of the Mercury compiler,
**	    or with other Mercury implementations.
**          Use only with great care!
*/
:- pred setarg(T1, int, T2).
:- mode setarg(in(any), in, in(any)) is det.

/*
** The function unsafe_cast_to_ground/1 can be used to assert to the
** compiler that a particular value of inst `any' is in fact ground.
** The assertion is *not* checked.  If it is false, all hell will break out.
*/
:- func unsafe_cast_to_ground(T::in(any)) = (T::out) is det.

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

:- implementation.

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

:- pragma c_code(unsafe_cast_to_ground(X::in(any)) = (Y::out), "Y = X;").

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

:- pragma c_code(
unsafe_perform_io(P::(pred(di, uo) is det)),
	may_call_mercury,
"{
	Word dummy_io_state = 0;
	call_io_pred_det(P, dummy_io_state, &dummy_io_state);
}").
:- pragma c_code(
unsafe_perform_io(P::(pred(di, uo) is cc_multi)),
	may_call_mercury,
"{
	Word dummy_io_state = 0;
	call_io_pred_cc_multi(P, dummy_io_state, &dummy_io_state);
}").

:- pred call_io_pred(pred(io__state, io__state), io__state, io__state).
:- mode call_io_pred(pred(di, uo) is det, di, uo) is det.
:- mode call_io_pred(pred(di, uo) is cc_multi, di, uo) is cc_multi.

:- pragma export(call_io_pred(pred(di, uo) is det, di, uo),
		"call_io_pred_det").
:- pragma export(call_io_pred(pred(di, uo) is cc_multi, di, uo),
		"call_io_pred_cc_multi").

call_io_pred(P) --> P.

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

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

").

:- 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;
}").

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

% 9-queens program -- using the `var' module and freeze/2.

:- module queens.

:- interface.

:- import_module list, int, io.

:- pred main1(list(int)).
:- mode main1(out) is nondet.

:- pred main(io__state, io__state).
:- mode main(di, uo) is cc_multi.

:- implementation.
:- import_module var, unsafe, std_util.

main1(Out) :-	
	data(Data),
	queen(Data, Out).

main -->
	( { data(Data), queen(Data, Out) } ->
		print(Out), nl
	;
		io__write_string("No solution\n")
	).

:- pred data(list(int)).
:- mode data(out) is det.

data([1,2,3,4,5,6,7,8,9]).

:- pred queen(list(int), list(int)).
:- mode queen(in, out) is nondet.

queen(Data, Out) :-
	same_len(Data, Posn),
	safe(Posn),
	qperm(Data, Posn, Posn2),
	conv_posn(Posn2, Out).

:- pred same_len(list(int)::in, list(var(int))::out(list_skel(any))) is det.
same_len([], []).
same_len([_|Xs], [N|Ys]) :- init(N), same_len(Xs, Ys).

:- pred conv_posn(list(var(int))::in, list(int)::out) is det.
conv_posn([], []).
conv_posn([var(N)|Xs], [N|Ys]) :- conv_posn(Xs, Ys).

:- pred qperm(list(int), list(var(int)), list(var(int))).
:- mode qperm(in, in(list_skel(any)), out) is nondet.

qperm([], [], []).
qperm([X|Y], [var(U)|V], [var(U)|V2]) :-
	qdelete(U, [X|Y], Z),
	qperm(Z, V, V2).

:- pred qdelete(int, list(int), list(int)).
:- mode qdelete(out, in, out) is nondet.

qdelete(A, [A|L], L).
qdelete(X, [A|Z], [A|R]) :-
	qdelete(X, Z, R).

:- pred safe(list(var(int))).
:- mode safe(in(list_skel(any))) is semidet.

safe([]).
safe([NVar|L]) :-
	freeze(NVar, (pred(N::in) is semidet :- nodiag(N, 1, L))),
	safe(L).

:- pred nodiag(int, int, list(var(int))).
:- mode nodiag(in, in, in(list_skel(any))) is semidet.

nodiag(_, _, []).
nodiag(B, D, [NVar|L]) :-
	freeze(NVar, (pred(N::in) is semidet :- D \= N - B, D \= B - N)),
	nodiag(B, D + 1, L).

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

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