[m-rev.] For review: State Variables

[Simon Taylor]

On 02-May-2002, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> Estimated hours taken: 340
> Branches: main
> 
> Added state variables to the language.  State variables provide a
> lightweight syntax for giving names to sequences that bear some
> resemblance to destructively updated variables found in imperative
> languages.  Code using state variables is translated into code that
> uses only ordinary logic variables.  State variables are intended
> to simplify code that passes (multiple) in-out state threads, without
> the limitations attached to abusing DCG syntax for this purpose.

> Index: compiler/make_hlds.m
> ===================================================================
> RCS file: /home/mercury1/repository/mercury/compiler/make_hlds.m,v
> retrieving revision 1.408
> diff -u -r1.408 make_hlds.m
> --- compiler/make_hlds.m	7 Apr 2002 10:22:34 -0000	1.408
> +++ compiler/make_hlds.m	2 May 2002 05:30:12 -0000
> @@ -3582,9 +3582,12 @@
>  :- mode module_add_clause(in, in, in, in, in, in, in, in, in,
>  		out, in, out, di, uo) is det.
>  
> -module_add_clause(ModuleInfo0, ClauseVarSet, PredOrFunc, PredName, Args, Body,
> +module_add_clause(ModuleInfo0, ClauseVarSet, PredOrFunc, PredName, Args0, Body,
>  			Status, Context, GoalType, ModuleInfo,
>  			Info0, Info) -->
> +
> +	{ Args = expand_dot_colon_state_var_args(Args0) },
> +

That doesn't do the right thing for function clauses.

> @@ -7128,10 +7240,28 @@
>  	% In the trivial case `X = c', no unravelling occurs.
>  
>  unravel_unification(term__variable(X), RHS,
> -			Context, MainContext, SubContext, VarSet0, Purity,
> -			Goal, VarSet, Info0, Info) -->
> +		Context, MainContext, SubContext, VarSet0, Purity,
> +		Goal, VarSet, Info0, Info, SInfo0, SInfo) -->
>  	{ RHS = term__functor(F, Args, FunctorContext) },
>  	(
> +		% Handle !.X state variable references.
> +		{ F = term__atom("!.") },
> +		{ Args = [term__variable(StateVar)] }
> +	->
> +		dot(Context, StateVar, Var, VarSet0, VarSet,
> +			SInfo0, SInfo),
> +		{ Goal = svar_unification(Context, X, Var) },
> +		{ Info = Info0 }
> +	;
> +		% Handle !:X state variable references.
> +		{ F = term__atom("!:") },
> +		{ Args = [term__variable(StateVar)] }
> +	->
> +		colon(Context, StateVar, Var, VarSet0, VarSet,
> +			SInfo0, SInfo),
> +		{ Goal = svar_unification(Context, X, Var) },
> +		{ Info = Info0 }

The way you've done this the type and mode error messages for
state variable references will be really awful. 

For example, code such as

	:- func f(int) = int.
	f(!.X) = !:X :-
		!:X = !.X / 2.

will be transformed into

	:- func f(int) = float.
	f(HeadVar__1) = HeadVar__2 :-
		HeadVar__1 = STATE_VAR_X_0,
		HeadVar__2 = STATE_VAR_X,
		V_1 = STATE_VAR_X_2,
		V_2 = STATE_VAR_X_0,
		V_1 = V_2 / 1.0.
		STATE_VAR_X = STATE_VAR_X_2.

Type and mode error message for the call to '/' will refer to
the introduced `V_' variables, not the state variables.

It would be better to expand state variable references before calling
make_fresh_arg_vars.

> @@ -7246,16 +7380,18 @@
>  		{ parse_some_vars_goal(IfTerm, VarSet0, Vars,
>  			IfParseTree, VarSet11) }

You should allow state variable quantifiers on if-then-elses.

> @@ -7732,19 +7890,21 @@
>  
>  :- pred get_conj(goal, prog_substitution, list(hlds_goal), prog_varset,
>  	list(hlds_goal), prog_varset, transform_info, transform_info,
> -	io__state, io__state).
> -:- mode get_conj(in, in, in, in, out, out, in, out, di, uo) is det.
> +	svar_info, svar_info, io__state, io__state).
> +:- mode get_conj(in, in, in, in, out, out, in, out, in, out, di, uo) is det.
>  
> -get_conj(Goal, Subst, Conj0, VarSet0, Conj, VarSet, Info0, Info) -->
> +get_conj(Goal, Subst, Conj0, VarSet0, Conj, VarSet, Info0, Info,
> +		SInfo0, SInfo) -->
>  	(
>  		{ Goal = (A,B) - _Context }
>  	->
> -		get_conj(B, Subst, Conj0, VarSet0, Conj1, VarSet1,
> -						Info0, Info1),
> -		get_conj(A, Subst, Conj1, VarSet1, Conj, VarSet, Info1, Info)
> +		get_conj(A, Subst, Conj0, VarSet0, Conj1, VarSet1,
> +			Info0, Info1, SInfo0, SInfo1),
> +		get_conj(B, Subst, Conj1, VarSet1, Conj, VarSet,
> +			Info1, Info,  SInfo1, SInfo)
>  	;
>  		transform_goal(Goal, VarSet0, Subst, Goal1, VarSet,
> -						Info0, Info),
> +			Info0, Info,  SInfo0, SInfo),
>  		{ goal_to_conj_list(Goal1, ConjList) },
>  		{ list__append(ConjList, Conj0, Conj) }
>  	).

You're now building Conj in reverse, so ConjList needs to be reversed
before adding it to Conj0 (same for get_par_conj and get_disj).

> +%------------------------------------------------------------------------------%
> +
> +	% This synonym improves code legibility.
> +	%
> +:- type svar == prog_var.

It would probably be better to do
:- type svar == var(svar_type).
:- type svar_type ---> svar_type.

This would help avoid confusing state variables with ordinary variables.

> +:- pred dot(prog_context, svar, prog_var,
> +		prog_varset, prog_varset, svar_info, svar_info, io, io).
> +:- mode dot(in, in, out, in, out, in, out, di, uo) is det.

This predicate needs documentation and a more descriptive name.

> +:- pred colon(prog_context, svar, prog_var,
> +		prog_varset, prog_varset, svar_info, svar_info, io, io).
> +:- mode colon(in, in, out, in, out, in, out, di, uo) is det.

Ditto.

> +colon(Context, StateVar, Var, VarSet0, VarSet, SInfo0, SInfo, IO0, IO) :-
> +
> +	( if SInfo0 ^ ctxt = in_head then
> +
> +		( if SInfo0 ^ colon ^ elem(StateVar) = Var0 then
> +			Var    = Var0,
> +			VarSet = VarSet0,
> +			SInfo  = SInfo0,
> +			IO     = IO0
> +		  else
> +		  	new_final_state_var(StateVar, Var,
> +				VarSet0, VarSet, SInfo0, SInfo),
> +			IO     = IO0
> +		)
> +
> +	  else
> +
> +		( if SInfo0 ^ colon ^ elem(StateVar) = Var0 then
> +			Var    = Var0,
> +			VarSet = VarSet0,
> +			SInfo  = SInfo0 `with_updated_svar` StateVar,
> +			IO     = IO0
> +		  else
> +		  	Var    = StateVar,
> +			VarSet = VarSet0,
> +			SInfo  = SInfo0,
> +			Name   = varset__lookup_name(VarSet0, StateVar),
> +			prog_out__write_context(Context, IO0, IO1),
> +		  	report_warning(string__format("\
> +Error: reference to !:%s, no such state variable in scope.\n", [s(Name)]),
> +				IO1, IO2),
> +			( if SInfo0 ^ external_dot `contains` StateVar then
> +				prog_out__write_context(Context, IO2, IO3),
> +				report_warning(string__format("\
> +       (although state variable !.%s is in scope.)\n", [s(Name)]),
> +       					IO3, IO)
> +			  else
> +			  	IO = IO2
> +			)
> +		)
> +	).

The error message for references to !:X in a lambda or if-then-else
expression is pretty ordinary.

> +	% We have to conjoin the head and body and add unifiers to tie up all
> +	% the final values of the state variables to the head variables.
> +	%
> +:- pred finish_head_and_body(prog_context, svar_map,
> +		hlds_goal, hlds_goal, hlds_goal, svar_info).
> +:- mode finish_head_and_body(in, in, in, in, out, in) is det.
> +
> +finish_head_and_body(Context, FinalSVarMap, Head, Body, Goal, SInfo) :-
> +	goal_info_init(Context, GoalInfo),
> +	goal_to_conj_list(Head, HeadGoals),
> +	goal_to_conj_list(Body, BodyGoals),
> +	Unifiers = svar_unifiers(Context, FinalSVarMap, SInfo ^ dot),
> +	conj_list_to_goal(HeadGoals ++ BodyGoals ++ Unifiers, GoalInfo, Goal).

It's probably better to substitute in the head rather than adding
unifications (adding too many variables will cause slow compilation).

+       % When we finish a call, we're either still inside the
+       % atomic formula, in which case we simply propagate the set of
+       % "updated" state variables, or we've just emerged, in which
case
+       % we need to set up the svar_info for the next conjunct.
+       %
+:- pred finish_call(prog_varset, prog_varset, svar_info, svar_info).
+:- mode finish_call(in, out, in, out) is det.

How can you still be inside an atomic formula when you've finished a
call?

> +	% We have to add unifiers to the Then and Else clauses of an
> +	% if-then-else to make sure all the state variables match up.
> +	%
> +	% We construct new mappings for the state variables and then
> +	% add unifiers.
> +	%
> +:- pred finish_if_then_else(prog_context,
> +		hlds_goal, hlds_goal, hlds_goal, hlds_goal,
> +		prog_varset, prog_varset, svar_info, svar_info, svar_info).
> +:- mode finish_if_then_else(in, in, out, in, out, in, out, in, in, out) is det.
> +
> +finish_if_then_else(Context, Then0, Then, Else0, Else, VarSet0, VarSet,
> +		SInfoT, SInfoE, SInfo) :-
> +	SInfo0       = SInfoT,
> +	N            = int__max(SInfoT ^ num, SInfoE ^ num),
> +	next_svar_info(N, VarSet0, VarSet, SInfo0, SInfo),
> +
> +	goal_info_init(Context, GoalInfo),
> +
> +	goal_to_conj_list(Then0, ThenGoals0),
> +	ThenUnifiers = svar_unifiers(Context, SInfo ^ dot, SInfoT ^ dot),
> +	conj_list_to_goal(ThenGoals0 ++ ThenUnifiers, GoalInfo, Then),
> +
> +	goal_to_conj_list(Else0, ElseGoals0),
> +	ElseUnifiers = svar_unifiers(Context, SInfo ^ dot, SInfoE ^ dot),
> +	conj_list_to_goal(ElseGoals0 ++ ElseUnifiers, GoalInfo, Else).

This doesn't handle code like the following properly:

	( p(!X) ->
		q
	;
		r(!X)
	).

It would also be nice to avoid adding lots of extra variables at the
end of each branch (you do this for disjunctions as well). See how
prog_io_dcg.m does this.

> +%------------------------------------------------------------------------------%
> +
> +:- pred next_svar_info(int, prog_varset, prog_varset, svar_info, svar_info).
> +:- mode next_svar_info(in, in, out, in, out) is det.

Documentation please.

> +%------------------------------------------------------------------------------%
> +
> +	% We assume that a negation updates all state variables in scope,
> +	% so we construct new mappings for the state variables and then
> +	% add unifiers from their pre-negated goal mappings.
> +	%
> +:- pred finish_negation(prog_context, hlds_goal, hlds_goal,
> +		prog_varset, prog_varset, svar_info, svar_info, svar_info).
> +:- mode finish_negation(in, in, out, in, out, in, in, out) is det.
> +
> +finish_negation(Context, Goal0, Goal, VarSet0, VarSet,
> +		SInfoBefore, SInfoNeg, SInfo) :-
> +	SInfo0    = SInfoBefore,
> +	N         = SInfoNeg ^ num,
> +	next_svar_info(N, VarSet0, VarSet, SInfo0, SInfo),
> +
> +	goal_info_init(Context, GoalInfo),
> +
> +	goal_to_conj_list(Goal0, Goals0),
> +	Unifiers  = svar_unifiers(Context, SInfo ^ dot, SInfo0 ^ dot),
> +	conj_list_to_goal(Goals0 ++ Unifiers, GoalInfo, Goal).

You should be able to do this without adding unifications.
I think you're making life difficult for yourself by trying
to maintain the `dot' and `colon' mappings all the time, rather
than generating a `colon' mapping only when a reference to `!:X'
is seen in an atom (as prog_io_dcg.m does).

> @@ -220,10 +242,29 @@
>  	parse_goal(A0, V0, A, V1),
>  	parse_goal(B0, V1, B, V).
>  
> -parse_goal_2("some", [Vars0, A0], V0, some(Vars, A), V):-
> -	parse_list_of_vars(Vars0, Vars1),
> -	list__map(term__coerce_var, Vars1, Vars),
> -	parse_goal(A0, V0, A, V).
> +parse_goal_2("some", [QVars, A0], V0, GoalExpr, V):-

You also need to modify the similar code in prog_io_dcg.m.

You should also handle state variables in the quantifiers
on if-then-elses.

To be continued.

Simon.
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------