[m-rev.] State variable syntax transformation
Ralph Becket
rafe at cs.mu.OZ.AU
Thu Feb 7 15:41:13 AEDT 2002
The transformation is complete in that it now handles lambdas correctly.
The code does not perform any sanity checking since that debate has yet
to come to any conclusion. I propose to check this in and start using
it if there are no objections.
I have a test harness and list of test cases (appended after the diffs)
which I would like to save somewhere for regression testing. However,
since the test harness directly imports the transformation module which
lives in the compiler directory, it cannot exist as a stand-alone test
program. Any suggestions?
I have not included the diffs for lexer.m, builtin.m, prog_io.m or
mercury_compile.m since these haven't changed since my last posting.
- Ralph
Estimated hours taken: 32
Branches: main
Added a new syntax to the language ("state variables") to simplify the
manipulation of threaded state. This is simpler and more general than
DCGs and is intended as a replacement.
NEWS:
Mention the new syntax, giving a pointer to the appropriate part
of the Reference Manual
doc/reference_manual.texi:
Documented the new syntax in the Syntax chapter, just before the
section on DCGs.
library/lexer.m:
Changed `!' from being a special token to being a graphical token.
library/ops.m:
Added three new prefix operators, `!', `!+' and `!-'.
library/builtin.m:
Commented out the declarations and definitions for !/0 and !/2.
compiler/mercury_compile.m:
Removed two calls to !/2 (remnants of the original Prolog version...)
compiler/prog_io_state_vars.m:
The code to perform the state variable syntactic transformation.
compiler/prog_io.m:
Add calls to the state variable transformation to parse_item/4.
Index: reference_manual.texi
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/reference_manual.texi,v
retrieving revision 1.239
diff -u -r1.239 reference_manual.texi
--- reference_manual.texi 30 Jan 2002 01:40:34 -0000 1.239
+++ reference_manual.texi 7 Feb 2002 03:33:31 -0000
@@ -51,6 +51,7 @@
@author Simon Taylor
@author Chris Speirs
@author Tyson Dowd
+ at author Ralph Becket
@page
@vskip 0pt plus 1filll
Copyright @copyright{} 1995-2001 The University of Melbourne.
@@ -162,6 +163,7 @@
* Facts::
* Rules::
* Goals::
+* State Variables::
* DCG-rules::
* DCG-goals::
* Data-terms::
@@ -738,9 +740,154 @@
@end table
+ at node State Variables
+ at section State Variables
+
+Clauses may use @samp{state variables} as a shorthand for naming
+intermediate values in a sequence.
+
+A state variable is written @samp{!. at var{X}} or @samp{!:@var{X}},
+denoting the "current" or "next" value of the sequence labelled
+ at var{X}. An argument @samp{!@var{X}} is shorthand for two state
+variable arguments @samp{!. at var{X}, !:@var{X}}; that is,
+ at samp{p(..., !@var{X}, ...)} is parsed as
+ at samp{p(..., !. at var{X}, !:@var{X}, ...)}.
+
+Clauses defined using state variables are transformed into equivalent
+forms that do not according to the state variable @samp{transform}
+function defined next (this function defines a syntactic relation
+between semantically equivalent formulae, it is not something that is
+part of the language.)
+
+The transformation is applied once for each state variable @var{X}
+with some fresh variables which we shall call @var{ThisX} and
+ at var{NextX}.
+
+(Fact clauses and lambdas are treated as though they have an implicit
+body containing just the goal @samp{true}.)
+
+The expression
+ at samp{substitute(@var{Term}, @var{X}, @var{ThisX}, @var{NextX})}
+stands for a copy of @var{Term} with occurrences of @samp{!. at var{X}}
+replaced with @var{ThisX} and occurrences of @samp{!:@var{X}}
+replaced with @var{NextX}.
+
+ at table @code
+
+ at item @var{Head} :- @var{Body}
+ at example
+transform((@var{Head} :- @var{Body}), @var{X}, @var{ThisX}, @var{NextX}) =
+substitute(@var{Head}, @var{X}, @var{ThisX}, @var{NextX}) :- transform(@var{Body}, @var{X}, @var{ThisX}, @var{NextX})
+ at end example
+
+ at item @var{Head} --> @var{Body}
+ at example
+transform((@var{Head} --> @var{Body}), @var{X}, @var{ThisX}, @var{NextX}) =
+substitute(@var{Head}, @var{X}, @var{ThisX}, @var{NextX}) :- transform(@var{Body}, @var{X}, @var{ThisX}, @var{NextX})
+ at end example
+
+ at item @var{Goal1}, @var{Goal2}
+ at example
+transform((@var{Goal1}, @var{Goal2}), @var{X}, @var{ThisX}, @var{NextX}) =
+transform(@var{Goal1}, @var{X}, @var{ThisX}, @var{TmpX}), transform(@var{Goal2}, @var{X}, @var{TmpX}, @var{NextX})
+ at end example
+for some fresh variable @var{TmpX}.
+
+ at item @var{Goal1} ; @var{Goal2}
+ at example
+transform((@var{Goal1} ; @var{Goal2}), @var{X}, @var{ThisX}, @var{NextX}) =
+transform(@var{Goal1}, @var{X}, @var{ThisX}, @var{NextX}) ; transform(@var{Goal2}, @var{X}, @var{ThisX}, @var{NextX})
+ at end example
+
+ at item not @var{Goal}
+ at item \+ @var{Goal}
+ at example
+transform((not @var{Goal}), @var{X}, @var{ThisX}, @var{NextX}) =
+not transform(@var{Goal1}, @var{X}, @var{ThisX}, @var{DummyX}), @var{ThisX} = @var{NextX}
+ at end example
+for some fresh variable @var{DummyX}.
+
+ at item if @var{Goal1} then @var{Goal2} else @var{Goal3}
+ at item @var{Goal1} -> @var{Goal2} ; @var{Goal3}
+ at example
+transform((if @var{Goal1} then @var{Goal2} else @var{Goal3}), @var{X}, @var{ThisX}, @var{NextX}) =
+if transform(@var{Goal1}, @var{X}, @var{ThisX}, @var{TmpX}) then transform(@var{Goal2}, @var{X}, @var{TmpX}, @var{NextX})
+ else transform(@var{Goal3}, @var{X}, @var{ThisX}, @var{NextX})
+ at end example
+for some fresh variable @var{TmpX}.
+
+ at item if @var{Goal1} then @var{Goal2}
+ at item @var{Goal1} -> @var{Goal2}
+ at example
+transform((if @var{Goal1} then @var{Goal2}), @var{X}, @var{ThisX}, @var{NextX}) =
+if transform(@var{Goal1}, @var{X}, @var{ThisX}, @var{TmpX}) then transform(@var{Goal2}, @var{X}, @var{TmpX}, @var{NextX})
+ else @var{ThisX} = @var{NextX}
+ at end example
+for some fresh variable @var{TmpX}.
+
+ at item @var{Goal1} => @var{Goal2}
+ at item @var{Goal2} <= @var{Goal1}
+ at example
+transform((@var{Goal1} => @var{Goal2}), @var{X}, @var{ThisX}, @var{NextX}) =
+transform(@var{Goal1}, @var{X}, @var{ThisX}, @var{TmpX}) => transform(@var{Goal2}, @var{X}, @var{TmpX}, @var{NextX}),
+ at var{ThisX} = @var{NextX}
+ at end example
+for some fresh variable @var{TmpX}.
+
+ at item all @var{Vars} @var{Goal}
+ at example
+transform((all @var{Vars} @var{Goal}), @var{X}, @var{ThisX}, @var{NextX}) =
+all @var{Vars} transform(@var{Goal}, @var{X}, @var{ThisX}, @var{DummyX}), @var{ThisX} = @var{NextX}
+ at end example
+for some fresh variable @var{DummyX}.
+
+ at item some @var{Vars} @var{Goal}
+ at example
+transform((some @var{Vars} @var{Goal}), @var{X}, @var{ThisX}, @var{NextX}) =
+some @var{Vars} transform(@var{Goal}, @var{X}, @var{ThisX}, @var{NextX})
+ at end example
+
+ at item @var{CallOrUnification}
+If @samp{!:@var{X}} does not appear in @var{CallOrUnification} then
+ at example
+transform(@var{CallOrUnification}, @var{X}, @var{ThisX}, @var{NextX}) =
+substitute(@var{CallOrUnification}, @var{X}, @var{ThisX}, @var{NextX}), @var{ThisX} = @var{NextX}
+ at end example
+If @samp{!:@var{X}} does appear in @var{CallOrUnification} then
+ at example
+transform(@var{CallOrUnification}, @var{X}, @var{ThisX}, @var{NextX}) =
+substitute(@var{CallOrUnification}, @var{X}, @var{ThisX}, @var{NextX})
+ at end example
+
+ at end table
+
+Note that this transformation can lead to the introduction of chains
+of unifications for variables that do not otherwise play a role in the
+definition. Such chains are removed transparently.
+
+ at emph{Note also} that the state variable transformation is applied to source
+code during parsing (before the code has been simplified to any normal form),
+hence the following somewhat perverse example
+ at example
+ ...,
+ p(f(g(!X), !X), !X),
+ ...
+ at end example
+is equivalent to
+ at example
+ ...,
+ ThisX = !.X,
+ p(f(g(ThisX, NextX), ThisX, NextX), ThisX, NextX),
+ !:X = NextX,
+ ...
+ at end example
+
@node DCG-rules
@section DCG-rules
+(Use of DCG syntax to thread hidden variables is now deprecated; the
+preferred mechanism is to use state variables instead.)
+
DCG-rules in Mercury have identical syntax and semantics to
DCG-rules in Prolog.
@@ -5283,7 +5430,7 @@
:- pragma foreign_proc("C", string__contains_char(Str::in, Ch::in),
[will_not_call_mercury],
- "SUCCESS_INDICATOR = (strchr(Str, Ch) != NULL);").
+ "SUCCESS_INDICATOR = (strchr(Str, Ch) !. NULL);").
@end example
@code{SUCCESS_INDICATOR} should not be used other than as the target of
@@ -5792,7 +5939,7 @@
:- pragma c_code(string__contains_char(Str::in, Ch::in),
[will_not_call_mercury],
- "SUCCESS_INDICATOR = (strchr(Str, Ch) != NULL);").
+ "SUCCESS_INDICATOR = (strchr(Str, Ch) !. NULL);").
@end example
@code{SUCCESS_INDICATOR} should not be used other than as the target of
Index: ops.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/ops.m,v
retrieving revision 1.38
diff -u -r1.38 ops.m
--- ops.m 10 Dec 2001 06:11:33 -0000 1.38
+++ ops.m 1 Feb 2002 07:15:36 -0000
@@ -342,6 +342,9 @@
ops__op_table("where", after, xfx, 1175). % NU-Prolog extension (*)
ops__op_table("~", before, fy, 900). % Goedel (*)
ops__op_table("~=", after, xfx, 700). % NU-Prolog (*)
+ops__op_table("!", before, fx, 40). % Mercury extension
+ops__op_table("!.", before, fx, 40). % Mercury extension
+ops__op_table("!:", before, fx, 40). % Mercury extension
% (*) means that the operator is not useful in Mercury
% and is provided only for compatibility.
Index: prog_io_state_vars.m
===================================================================
RCS file: prog_io_state_vars.m
diff -N prog_io_state_vars.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ prog_io_state_vars.m 7 Feb 2002 04:24:48 -0000
@@ -0,0 +1,597 @@
+%------------------------------------------------------------------------------%
+% prog_io_state_vars.m
+% Ralph Becket <rafe at cs.mu.oz.au>
+% Tue Jan 15 14:46:23 EST 2002
+% vim: ft=mercury ff=unix ts=4 sw=4 et tw=0 wm=0
+%
+% This module performs the state-variable transformation into code that
+% does not have state variables.
+%
+% A state variable X is identified in an atomic goal as !.X for its
+% current value at that goal and !:X for its successor value (i.e. % !.X
+% for the next goal referencing state variable X.) In the parser the
+% notation !X is interpreted as shorthand for two arguments !.X, !:X.
+%
+% TODO
+% * We should add checks too ensure that no state variable has the same name
+% as a normal var.
+% * There was some unresolved discussion on what constitutes an error w.r.t.
+% the use of state variables (e.g. using !.X before !:X has been mentioned).
+% Currently no errors are looked for.
+% * It would be nice if the names given to variables reflected the state
+% var they belong to, rather than just using the default _1, _2, _3, ...
+%
+%------------------------------------------------------------------------------%
+
+:- module prog_io_state_vars.
+
+:- interface.
+
+:- import_module varset, term.
+
+
+
+ % transform_state_vars(Head0, Head, Body0, Body, VarSet0, VarSet).
+ %
+:- pred transform_state_vars(term, term, term, term, varset, varset).
+:- mode transform_state_vars(in, out, in, out, in, out) is det.
+
+:- pred transform_clause(term, term, varset, varset).
+:- mode transform_clause(in, out, in, out) is det.
+
+%------------------------------------------------------------------------------%
+%------------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module map, list, std_util, bool.
+
+
+
+:- type varmap == map(var, var).
+
+:- type state_var == {this_or_next, var}.
+
+:- type state_vars == list(state_var).
+
+:- type subs
+ ---> subs(
+ this :: varmap,
+ next :: varmap
+ ).
+
+:- type this_or_next
+ ---> this
+ ; next.
+
+%------------------------------------------------------------------------------%
+
+:- func null_subs = subs.
+
+null_subs = subs(map__init, map__init).
+
+
+:- pred init_subs(term, term, subs, subs, varset, varset).
+:- mode init_subs(in, in, in, out, in, out) is det.
+
+init_subs(Head, Body, ParentSubs, LocalSubs, VS0, VS) :-
+ ParentSubs = subs(PThis, PNext),
+ HeadSVs = state_vars(yes, Head),
+ BodySVs = state_vars(no, Body),
+ SVs = list__merge_and_remove_dups(HeadSVs, BodySVs),
+ list__foldl2(set_state_var_map(this), SVs, map__init, LThis0, VS0, VS1),
+ list__foldl2(set_state_var_map(next), SVs, map__init, LNext0, VS1, VS ),
+
+ % The LocalSubs may inherit state variables provided they are
+ % not local (i.e. appear in the local Head.)
+ %
+ LThis = map__foldl(inherit_state_var(this,HeadSVs,BodySVs), PThis, LThis0),
+ LNext = map__foldl(inherit_state_var(next,HeadSVs,BodySVs), PNext, LNext0),
+
+ LocalSubs = subs(LThis, LNext).
+
+
+:- pred set_state_var_map(this_or_next, state_var,
+ varmap, varmap, varset, varset).
+:- mode set_state_var_map(in, in, in, out, in, out) is det.
+
+set_state_var_map(TorN, {XTorN, X}, Map0, Map, VS0, VS) :-
+ ( if TorN = XTorN then
+ varset__new_var(VS0, Y, VS),
+ Map = Map0 ^ elem(X) := Y
+ else
+ VS = VS0,
+ Map = Map0
+ ).
+
+
+:- func inherit_state_var(this_or_next,
+ state_vars, state_vars,
+ var, var, varmap
+ ) = varmap.
+
+inherit_state_var(TorN, HeadSVs, BodySVs, X, Y, Map) =
+ ( if not list__member({TorN, X}, HeadSVs),
+ list__member({TorN, X}, BodySVs)
+ then Map ^ elem(X) := Y
+ else Map
+ ).
+
+%------------------------------------------------------------------------------%
+
+ % OpenLambda is there to ensure that at the right level we
+ % do look inside lambdas for state variables.
+ %
+:- func state_vars(bool, term) = state_vars.
+
+state_vars(OpenLambda, T) = solutions(state_var(OpenLambda, T)).
+
+
+:- pred state_var(bool, term, state_var).
+:- mode state_var(in, in, out) is nondet.
+
+state_var(_OpenLambda, T @ functor(_F, _Ts, _C), {TorN, X}) :-
+ state_var_term(T, TorN, X).
+
+state_var(OpenLambda, T0 @ functor(_F, Ts, _C), SV) :-
+ ( OpenLambda = yes ; not lambda_term(T0, _, _, _) ),
+ list__member(T, Ts),
+ state_var(no, T, SV).
+
+
+:- pred state_var_term(term, this_or_next, var).
+:- mode state_var_term(in, out, out) is semidet.
+
+state_var_term(functor(atom("!."), [variable(X)], _), this, X).
+state_var_term(functor(atom("!:"), [variable(X)], _), next, X).
+
+%------------------------------------------------------------------------------%
+
+:- pred lambda_term(term, term, const, term).
+:- mode lambda_term(in, out, out, out) is semidet.
+
+lambda_term(T0, Head, Connective, Body) :-
+
+ T0 = functor(atom(A0), Args0, _),
+ (
+ A0 = ":-",
+ Args0 = [Head, Body],
+ Connective = atom(A0)
+ ;
+ A0 = "-->",
+ Args0 = [Head, Body],
+ Connective = atom(A0)
+ ;
+ A0 = "=",
+ Args0 = [functor(atom("func"), _, _), _RHS],
+ Head = T0,
+ Connective = atom(":-"),
+ Body = true_term
+ ;
+ A0 = "is",
+ Args0 = [functor(atom("pred"), _, _), _Detism],
+ Head = T0,
+ Connective = atom(":-"),
+ Body = true_term
+ ;
+ A0 = "is",
+ Args0 = [functor(atom("="), T1, _), _Detism],
+ T1 = [functor(atom("func"), _, _), _RHS],
+ Head = T0,
+ Connective = atom(":-"),
+ Body = true_term
+ ).
+
+%------------------------------------------------------------------------------%
+
+:- func true_term = term.
+
+true_term = functor(atom("true"), [], term__context_init).
+
+%------------------------------------------------------------------------------%
+
+transform_state_vars(Head0, Head, Body0, Body, VarSet0, VarSet) :-
+ transform_state_vars(Head0, Head, Body0, Body, null_subs, VarSet0, VarSet).
+
+
+:- pred transform_state_vars(term, term, term, term, subs, varset, varset).
+:- mode transform_state_vars(in, out, in, out, in, in, out) is det.
+
+transform_state_vars(Head0, Head, Body0, Body, ParentSubs, VarSet0, VarSet) :-
+
+ % Only apply the transformation if the clause contains
+ % state variables.
+ %
+ ( if ( contains_state_var(Head0) ; contains_state_var(Body0) ) then
+
+ % Ensure that we first strip off any determinism declaration
+ % on the head term (this can be the case with lambdas).
+ %
+ ( if Head0 = functor(atom("is"), [H, D], CIs) then
+
+ AddDetism = yes({D, CIs}),
+ Head1 = H
+
+ else
+
+ AddDetism = no,
+ Head1 = Head0
+ ),
+ Body1 = Body0,
+
+ % Ensure that we transform functions so that the RHS
+ % of the `=' is considered as part of the body.
+ %
+ ( if
+
+ Head1 = functor(atom("="), [LHS, RHS], C)
+
+ then
+
+ varset__new_var(VarSet0, X, VarSet1),
+ Head2 = functor(atom("="), [LHS, variable(X)], C),
+ Body2 = Body1 `conj` functor(atom("="), [variable(X), RHS], C)
+
+ else
+
+ VarSet1 = VarSet0,
+ Head2 = Head1,
+ Body2 = Body1
+ ),
+
+ Head3 = expand_thisnext_state_vars(Head2),
+ Body3 = expand_thisnext_state_vars(Body2),
+
+ init_subs(Head3, Body3, ParentSubs, S, VarSet1, VarSet2),
+
+ xform_head(S, Head3, Head4, VarSet2, VarSet3),
+ xform_goal(S, Body3, Body4, VarSet3, VarSet ),
+
+ % Re-add any determinism declaration.
+ %
+ Head =
+ ( if AddDetism = yes({DAgain, CIsAgain})
+ then functor(atom("is"), [Head4, DAgain], CIsAgain)
+ else Head4
+ ),
+ Body = Body4
+
+ else
+
+ Head = Head0,
+ Body = Body0,
+ VarSet = VarSet0
+ ).
+
+%------------------------------------------------------------------------------%
+
+:- pred contains_state_var(term).
+:- mode contains_state_var(in) is semidet.
+
+contains_state_var(functor(atom("!" ), [variable(_)], _)).
+contains_state_var(functor(atom("!."), [variable(_)], _)).
+contains_state_var(functor(atom("!:"), [variable(_)], _)).
+contains_state_var(functor(_, Ts, _)) :-
+ list__member(T, Ts),
+ contains_state_var(T).
+
+%------------------------------------------------------------------------------%
+
+ % Expand all arguments of the form !X into argument pairs of the form
+ % !.X, !:X.
+ %
+:- func expand_thisnext_state_vars(term) = term.
+
+expand_thisnext_state_vars(variable(X)) = variable(X).
+
+expand_thisnext_state_vars(functor(F, Ts0, C)) = functor(F, Ts, C) :-
+ Ts1 = list__foldr(expand_thisnext_state_var, Ts0, []),
+ Ts = list__map(expand_thisnext_state_vars, Ts1).
+
+
+:- func expand_thisnext_state_var(term, list(term)) = list(term).
+
+expand_thisnext_state_var(T, Ts) =
+ ( if T = functor(atom("!"), X @ [variable(_)], C)
+ then [functor(atom("!."), X, C), functor(atom("!:"), X, C) | Ts]
+ else [T | Ts]
+ ).
+
+%------------------------------------------------------------------------------%
+
+:- pred xform_head(subs, term, term, varset, varset).
+:- mode xform_head(in, in, out, in, out) is det.
+
+xform_head(S, T0, T, VS0, VS) :-
+ subs_state_vars(yes, S, T0, T, VS0, VS).
+
+%------------------------------------------------------------------------------%
+
+:- pred xform_atomic(subs, term, term, varset, varset).
+:- mode xform_atomic(in, in, out, in, out) is det.
+
+xform_atomic(S, T0, T, VS0, VS) :-
+ SVs = state_vars(no, T0),
+ subs_state_vars(yes, S, T0, T1, VS0, VS),
+ T = conj_unifiers(S, SVs, T1).
+
+%------------------------------------------------------------------------------%
+
+ % IsHead is there to ensure that we don't get into an infinite
+ % loop with lambdas (the head of a lambda looks just like a lambda
+ % fact).
+ %
+:- pred subs_state_vars(bool, subs, term, term, varset, varset).
+:- mode subs_state_vars(in, in, in, out, in, out) is det.
+
+subs_state_vars(_, _, variable(X), variable(X), VS, VS).
+ % XXX This might be a good place to make the state var/normal var
+ % separation check.
+
+subs_state_vars(IsHead, S, T0 @ functor(F, Ts0, C), T, VS0, VS) :-
+
+ ( if state_var_term(T0, TorN, X) then
+
+ T = subs_state_var(S, TorN, X),
+ VS = VS0
+
+ else if IsHead = no, lambda_term(T0, Head0, Connective, Body0) then
+
+ transform_state_vars(Head0, Head, Body0, Body, S, VS0, VS),
+ T = functor(Connective, [Head, Body], C)
+
+ else
+
+ list__map_foldl(subs_state_vars(no, S), Ts0, Ts, VS0, VS),
+ T = functor(F, Ts, C)
+ ).
+
+
+:- func subs_state_var(subs, this_or_next, var) = term.
+
+subs_state_var(S, this, X) = variable(S ^ this ^ det_elem(X)).
+
+subs_state_var(S, next, X) = variable(S ^ next ^ det_elem(X)).
+
+%------------------------------------------------------------------------------%
+
+:- func conj_unifiers(subs, state_vars, term) = term.
+
+conj_unifiers(S, SVs, T) =
+ map__foldl(conj_unifier(S, SVs), S ^ this, T).
+
+
+:- func conj_unifier(subs, state_vars, var, var, term) = term.
+
+conj_unifier(S, SVs, X, ThisX, T) =
+ ( if not list__member({next, X}, SVs),
+ S ^ next ^ elem(X) = NextX
+ then T `conj` (ThisX `unif` NextX)
+ else T
+ ).
+
+
+:- func term `conj` term = term.
+
+P `conj` Q = functor(atom(","), [P, Q], term__context_init).
+
+
+:- func var `unif` var = term.
+
+X `unif` Y = functor(atom("="), [variable(X), variable(Y)], term__context_init).
+
+%------------------------------------------------------------------------------%
+
+:- pred xform_goal(subs, term, term, varset, varset).
+:- mode xform_goal(in, in, out, in, out) is det.
+
+xform_goal(S, T0, T, VS0, VS) :-
+ ( if xform_compound(S, T0, T1, VS0, VS1)
+ then T = T1, VS = VS1
+ else xform_atomic(S, T0, T, VS0, VS )
+ ).
+
+%------------------------------------------------------------------------------%
+
+:- pred xform_compound(subs, term, term, varset, varset).
+:- mode xform_compound(in, in, out, in, out) is semidet.
+
+xform_compound(S,
+ functor(atom(","), [P0, Q0], C),
+ functor(atom(","), [P, Q ], C),
+ VS0, VS
+) :-
+ split_subs(S, SP, SQ, VS0, VS1),
+ xform_goal(SP, P0, P, VS1, VS2),
+ xform_goal(SQ, Q0, Q, VS2, VS ).
+
+xform_compound(S,
+ functor(atom(";"), Ts, C),
+ T,
+ VS0, VS
+) :-
+ ( if Ts = [functor(atom("->"), [P0, Q0], D), R0] then
+
+ % It's an if-then-else. P0 and Q0 are the "if" and "then"
+ % goals and are handled as a conjunctive formula in
+ % disjunction with R0.
+ %
+ split_subs(S, SP, SQ, VS0, VS1),
+ xform_goal(SP, P0, P, VS1, VS2),
+ xform_goal(SQ, Q0, Q, VS2, VS3),
+
+ xform_goal(S, R0, R, VS3, VS ),
+
+ T = functor(atom(";"), [functor(atom("->"), [P, Q], D), R], C)
+
+ else
+
+ % It could be an ordinary disjunction.
+ %
+ Ts = [P0, Q0],
+
+ xform_goal(S, P0, P, VS0, VS1),
+ xform_goal(S, Q0, Q, VS1, VS ),
+
+ T = functor(atom(";"), [P, Q], C)
+ ).
+
+xform_compound(S,
+ functor(atom("else"), [
+ functor(atom("if"), [
+ functor(atom("then"), [P0, Q0], E)], D), R0], C),
+ T,
+ VS0, VS
+) :-
+ % It's an if-then-else. P0 and Q0 are the "if" and "then"
+ % goals and are handled as a conjunctive formula in
+ % disjunction with R0.
+ %
+ split_subs(S, SP, SQ, VS0, VS1),
+ xform_goal(SP, P0, P, VS1, VS2),
+ xform_goal(SQ, Q0, Q, VS2, VS3),
+
+ xform_goal(S, R0, R, VS3, VS ),
+
+ T = functor(atom("else"), [
+ functor(atom("if"), [
+ functor(atom("then"), [P, Q], E)], D), R], C).
+
+xform_compound(S,
+ functor(atom("not"), [P0], C),
+ T,
+ VS0, VS
+) :-
+ % A negation cannot produce values visible outside the scope of
+ % the negation; we also have to add unifiers for the state
+ % variables.
+ %
+ split_subs(S, SP, _, VS0, VS1),
+ xform_goal(SP, P0, P, VS1, VS),
+ T = conj_unifiers(S, [], functor(atom("not"), [P], C)).
+
+xform_compound(S,
+ functor(atom("\\+"), [P0], C),
+ T,
+ VS0, VS
+) :-
+ % A negation cannot produce values visible outside the scope of
+ % the negation; we also have to add unifiers for the state
+ % variables.
+ %
+ split_subs(S, SP, _, VS0, VS1),
+ xform_goal(SP, P0, P, VS1, VS),
+ T = conj_unifiers(S, [], functor(atom("\\+"), [P], C)).
+
+xform_compound(S,
+ functor(atom("=>"), [P0, Q0], C),
+ T,
+ VS0, VS
+) :-
+ % (P => Q) is the same as not (P, not Q).
+ %
+ split_subs(S, SP, SPP, VS0, VS1),
+ split_subs(SPP, SQ, _, VS1, VS2),
+ xform_goal(SP, P0, P, VS2, VS3),
+ xform_goal(SQ, Q0, Q, VS3, VS ),
+ T = conj_unifiers(S, [], functor(atom("=>"), [P, Q], C)).
+
+xform_compound(S,
+ functor(atom("<="), [Q0, P0], C),
+ T,
+ VS0, VS
+) :-
+ % (Q <= P) is the same as not (P, not Q).
+ %
+ split_subs(S, SP, SPP, VS0, VS1),
+ split_subs(SPP, SQ, _, VS1, VS2),
+ xform_goal(SP, P0, P, VS2, VS3),
+ xform_goal(SQ, Q0, Q, VS3, VS ),
+ T = conj_unifiers(S, [], functor(atom("<="), [Q, P], C)).
+
+ % NOTE: since (P <=> Q) is the same as ((P => Q), (Q => P))
+ % there is no lexical ordering between P and Q, hence the
+ % state variable transformation is not applicable.
+
+ % NOTE: we do not allow explicit quantification of state variables.
+ %
+xform_compound(S,
+ functor(atom("some"), [Xs, P0], C),
+ functor(atom("some"), [Xs, P ], C),
+ VS0, VS
+) :-
+ xform_goal(S, P0, P, VS0, VS).
+
+ % NOTE: we do not allow explicit quantification of state variables.
+ %
+xform_compound(S,
+ functor(atom("all"), [Xs, P0], C),
+ T,
+ VS0, VS
+) :-
+ % Universally quantified goals occur in a negated context and
+ % must be treated like negated goals.
+ %
+ split_subs(S, SP, _, VS0, VS1),
+ xform_goal(SP, P0, P, VS1, VS),
+ T = conj_unifiers(S, [], functor(atom("all"), [Xs, P], C)).
+
+ % (P -> Q) is the same as (P -> Q ; true).
+ %
+xform_compound(S,
+ T0 @ functor(atom("->"), [_, _], _),
+ T,
+ VS0, VS
+) :-
+ C = term__context_init,
+ xform_compound(S,
+ functor(atom(";"), [T0, true_term], C),
+ T,
+ VS0, VS
+ ).
+
+ % (if P then Q) is the same as (if P then Q else true).
+ %
+xform_compound(S,
+ T0 @ functor(atom("if"), [functor(atom("then"), [_, _], _)], _),
+ T,
+ VS0, VS
+) :-
+ C = term__context_init,
+ xform_compound(S,
+ functor(atom("else"), [T0, true_term], C),
+ T,
+ VS0, VS
+ ).
+
+%------------------------------------------------------------------------------%
+
+:- pred split_subs(subs, subs, subs, varset, varset).
+:- mode split_subs(in, out, out, in, out) is det.
+
+split_subs(S, SA, SB, VS0, VS) :-
+ Xs = map__keys(S ^ this),
+ list__foldl2(map_to_new_var, Xs, map__init, MiddleMap, VS0, VS),
+ SA = ( S ^ next := MiddleMap),
+ SB = ( S ^ this := MiddleMap).
+
+
+:- pred map_to_new_var(var, varmap, varmap, varset, varset).
+:- mode map_to_new_var(in, in, out, in, out) is det.
+
+map_to_new_var(X, M, M ^ elem(X) := Y, VS0, VS) :-
+ varset__new_var(VS0, Y, VS).
+
+%------------------------------------------------------------------------------%
+%------------------------------------------------------------------------------%
+
+transform_clause(T0, T, VS0, VS) :-
+ ( if lambda_term(T0, Head0, Connective0, Body0) then
+ Connective = Connective0,
+ transform_state_vars(Head0, Head, Body0, Body, VS0, VS)
+ else
+ Connective = atom(":-"),
+ transform_state_vars(T0, Head, true_term, Body, VS0, VS)
+ ),
+ T = functor(Connective, [Head, Body], term__context_init).
+
Test harness code:
%------------------------------------------------------------------------------%
% state_vars_tests.m
% Ralph Becket <rafe at cs.mu.oz.au>
% Thu Jan 17 17:49:37 EST 2002
% vim: ft=mercury ff=unix ts=4 sw=4 et tw=0 wm=0
%
%------------------------------------------------------------------------------%
:- module state_vars_tests.
:- interface.
:- import_module io.
:- pred main(io::di, io::uo) is det.
%------------------------------------------------------------------------------%
%------------------------------------------------------------------------------%
:- implementation.
:- import_module prog_io_state_vars.
:- import_module term_io, pprint.
%------------------------------------------------------------------------------%
main -->
io__see("state_vars_tests.in", R),
(
{ R = ok },
transform_terms,
io__seen
;
{ R = error(_) },
io__print(R),
io__nl
).
%------------------------------------------------------------------------------%
:- pred transform_terms(io::di, io::uo) is det.
transform_terms -->
term_io__read_term(R),
(
{ R = eof }
;
{ R = error(_, _) },
io__print(R),
io__nl
;
{ R = term(VS0, T0) },
{ transform_clause(T0, T, VS0, VS) },
io__print("\nstate vars term\n"),
term_io__write_term(VS, T0),
io__print("\ntransforms into\n"),
term_io__write_term(VS, T),
io__nl,
transform_terms
).
%------------------------------------------------------------------------------%
%------------------------------------------------------------------------------%
Test results:
state vars term
foo
transforms into
foo :- true
state vars term
foo(X)
transforms into
foo(X) :- true
state vars term
foo(X) :- bar(X)
transforms into
foo(X) :- bar(X)
state vars term
foo(X, !. A, !: A)
transforms into
foo(X, _3, _4) :- true, _3 = _4
state vars term
foo(X, !. A, !: A) :- bar(X, !. A, !: A)
transforms into
foo(X, _3, _4) :- bar(X, _3, _4)
state vars term
foo(X, !. A, !: A) :- bar(X, !. A, !: A), baz(X, !. A, !: A)
transforms into
foo(X, _3, _4) :- bar(X, _3, _5), baz(X, _5, _4)
state vars term
foo(X, !. A, !: A) :- bar(X, !. A, !: A) ; baz(X, !. A, !: A)
transforms into
foo(X, _3, _4) :- bar(X, _3, _4) ; baz(X, _3, _4)
state vars term
foo(X, !. A, !: A) :- p(X) -> bar(X, !. A, !: A) ; baz(X, !. A, !: A)
transforms into
foo(X, _3, _4) :- p(X), _3 = _5 -> bar(X, _5, _4) ; baz(X, _3, _4)
state vars term
foo(X, !. A, !: A) :- p(X, !. A, !: A) -> bar(X, !. A, !: A) ; baz(X, !. A, !: A)
transforms into
foo(X, _3, _4) :- p(X, _3, _5) -> bar(X, _5, _4) ; baz(X, _3, _4)
state vars term
foo(X, !. A, !: A) :- p(X, !. A, !: A) -> bar(X, !. A, !: A)
transforms into
foo(X, _3, _4) :- p(X, _3, _5) -> bar(X, _5, _4) ; true, _3 = _4
state vars term
foo(X, !. A, !: A) :- if p(X) then bar(X, !. A, !: A) else baz(X, !. A, !: A)
transforms into
foo(X, _3, _4) :- if p(X), _3 = _5 then bar(X, _5, _4) else baz(X, _3, _4)
state vars term
foo(X, !. A, !: A) :- if p(X, !. A, !: A) then bar(X, !. A, !: A) else baz(X, !. A, !: A)
transforms into
foo(X, _3, _4) :- if p(X, _3, _5) then bar(X, _5, _4) else baz(X, _3, _4)
state vars term
foo(X, !. A, !: A) :- if p(X, !. A, !: A) then bar(X, !. A, !: A)
transforms into
foo(X, _3, _4) :- if p(X, _3, _5) then bar(X, _5, _4) else true, _3 = _4
state vars term
foo(!. A, !: A, !. B, !: B)
transforms into
foo(_3, _5, _4, _6) :- (true, _3 = _5), _4 = _6
state vars term
foo(!. A, !: A, !. B, !: B) :- bar(!. A, !: A), baz(!. B, !: B)
transforms into
foo(_3, _5, _4, _6) :- (bar(_3, _7), _4 = _8), baz(_8, _6), _7 = _5
state vars term
foo(!. A, !: A, !. B, !: B) :- bar(!. A, !: A) ; baz(!. B, !: B)
transforms into
foo(_3, _5, _4, _6) :- bar(_3, _5), _4 = _6 ; baz(_4, _6), _3 = _5
state vars term
foo(!. A, !: A) :- \+ bar(!. A, !: A)
transforms into
foo(_2, _3) :- \+ bar(_2, _4), _2 = _3
state vars term
foo(!. A, !: A) :- not bar(!. A, !: A)
transforms into
foo(_2, _3) :- not bar(_2, _4), _2 = _3
state vars term
foo(!. A, !: A) :- bar(!. A), baz(!. A, !: A)
transforms into
foo(_2, _3) :- (bar(_2), _2 = _4), baz(_4, _3)
state vars term
foo(!. A, !: A) :- bar(!. A, !: A), baz(!. A)
transforms into
foo(_2, _3) :- bar(_2, _4), baz(_4), _4 = _3
state vars term
foo(!. A, !: A) :- bar(!: A), baz(!. A, !: A)
transforms into
foo(_2, _3) :- bar(_4), baz(_4, _3)
state vars term
foo(!. A, !: A) :- bar(!. A, !: A), baz(!: A)
transforms into
foo(_2, _3) :- bar(_2, _4), baz(_3)
state vars term
foo(!. A, !: A) :- bar(!. A, !: A) => baz(!. A, !: A)
transforms into
foo(_2, _3) :- bar(_2, _4) => baz(_4, _5), _2 = _3
state vars term
foo(!. A, !: A) :- bar(!. A, !: A) <= baz(!. A, !: A)
transforms into
foo(_2, _3) :- bar(_4, _5) <= baz(_2, _4), _2 = _3
state vars term
foo(!. A, !: A) :- bar(!: A)
transforms into
foo(_2, _3) :- bar(_3)
state vars term
foo :- bar(!: A)
transforms into
foo :- bar(_2)
state vars term
foo(!. A, !: A) :- bar(!. B, !: B)
transforms into
foo(_3, _5) :- bar(_4, _6), _3 = _5
state vars term
foo
transforms into
foo :- true
state vars term
foo(X)
transforms into
foo(X) :- true
state vars term
foo(X) :- bar(X)
transforms into
foo(X) :- bar(X)
state vars term
foo(X, ! A)
transforms into
foo(X, _3, _4) :- true, _3 = _4
state vars term
foo(X, ! A) :- bar(X, ! A)
transforms into
foo(X, _3, _4) :- bar(X, _3, _4)
state vars term
foo(X, ! A) :- bar(X, ! A), baz(X, ! A)
transforms into
foo(X, _3, _4) :- bar(X, _3, _5), baz(X, _5, _4)
state vars term
foo(X, ! A) :- bar(X, ! A) ; baz(X, ! A)
transforms into
foo(X, _3, _4) :- bar(X, _3, _4) ; baz(X, _3, _4)
state vars term
foo(X, ! A) :- p(X) -> bar(X, ! A) ; baz(X, ! A)
transforms into
foo(X, _3, _4) :- p(X), _3 = _5 -> bar(X, _5, _4) ; baz(X, _3, _4)
state vars term
foo(X, ! A) :- p(X, ! A) -> bar(X, ! A) ; baz(X, ! A)
transforms into
foo(X, _3, _4) :- p(X, _3, _5) -> bar(X, _5, _4) ; baz(X, _3, _4)
state vars term
foo(X, ! A) :- p(X, ! A) -> bar(X, ! A)
transforms into
foo(X, _3, _4) :- p(X, _3, _5) -> bar(X, _5, _4) ; true, _3 = _4
state vars term
foo(X, ! A) :- if p(X) then bar(X, ! A) else baz(X, ! A)
transforms into
foo(X, _3, _4) :- if p(X), _3 = _5 then bar(X, _5, _4) else baz(X, _3, _4)
state vars term
foo(X, ! A) :- if p(X, ! A) then bar(X, ! A) else baz(X, ! A)
transforms into
foo(X, _3, _4) :- if p(X, _3, _5) then bar(X, _5, _4) else baz(X, _3, _4)
state vars term
foo(X, ! A) :- if p(X, ! A) then bar(X, ! A)
transforms into
foo(X, _3, _4) :- if p(X, _3, _5) then bar(X, _5, _4) else true, _3 = _4
state vars term
foo(! A, ! B)
transforms into
foo(_3, _5, _4, _6) :- (true, _3 = _5), _4 = _6
state vars term
foo(! A, ! B) :- bar(! A), baz(! B)
transforms into
foo(_3, _5, _4, _6) :- (bar(_3, _7), _4 = _8), baz(_8, _6), _7 = _5
state vars term
foo(! A, ! B) :- bar(! A) ; baz(! B)
transforms into
foo(_3, _5, _4, _6) :- bar(_3, _5), _4 = _6 ; baz(_4, _6), _3 = _5
state vars term
foo(! A) :- \+ bar(! A)
transforms into
foo(_2, _3) :- \+ bar(_2, _4), _2 = _3
state vars term
foo(! A) :- not bar(! A)
transforms into
foo(_2, _3) :- not bar(_2, _4), _2 = _3
state vars term
foo(! A) :- bar(!. A), baz(! A)
transforms into
foo(_2, _3) :- (bar(_2), _2 = _4), baz(_4, _3)
state vars term
foo(! A) :- bar(! A), baz(!. A)
transforms into
foo(_2, _3) :- bar(_2, _4), baz(_4), _4 = _3
state vars term
foo(! A) :- bar(!: A), baz(! A)
transforms into
foo(_2, _3) :- bar(_4), baz(_4, _3)
state vars term
foo(! A) :- bar(! A), baz(!: A)
transforms into
foo(_2, _3) :- bar(_2, _4), baz(_3)
state vars term
foo(! A) :- bar(! A) => baz(! A)
transforms into
foo(_2, _3) :- bar(_2, _4) => baz(_4, _5), _2 = _3
state vars term
foo(! A) :- bar(! A) <= baz(! A)
transforms into
foo(_2, _3) :- bar(_4, _5) <= baz(_2, _4), _2 = _3
state vars term
foo(! A) :- bar(!: A)
transforms into
foo(_2, _3) :- bar(_3)
state vars term
foo :- bar(!: A)
transforms into
foo :- bar(_2)
state vars term
foo(! A) :- bar(! B)
transforms into
foo(_3, _5) :- bar(_4, _6), _3 = _5
state vars term
foo(! A) :- bar(! A, ! A)
transforms into
foo(_2, _3) :- bar(_2, _3, _2, _3)
state vars term
foo(! A, ! A) :- bar(! A)
transforms into
foo(_2, _3, _2, _3) :- bar(_2, _3)
state vars term
p(Xs, ! A) :- foldl(pred(X, Y, f(X, Y)), Xs, ! A)
transforms into
p(Xs, _5, _6) :- foldl(pred(X, Y, f(X, Y)), Xs, _5, _6)
state vars term
p(Xs, ! A) :- foldl(pred(X, Y, Z) :- Z = f(X, Y), Xs, ! A)
transforms into
p(Xs, _6, _7) :- foldl(pred(X, Y, Z) :- Z = f(X, Y), Xs, _6, _7)
state vars term
p(Xs, ! A) :- foldl(pred(X, ! B) :- !: B = f(X, !. B), Xs, ! A)
transforms into
p(Xs, _5, _6) :- foldl(pred(X, _7, _8) :- _8 = f(X, _7), Xs, _5, _6)
state vars term
p(Xs, ! A) :- foldl(pred(X, ! A) :- !: A = f(X, !. A), Xs, ! A)
transforms into
p(Xs, _4, _5) :- foldl(pred(X, _6, _7) :- _7 = f(X, _6), Xs, _4, _5)
state vars term
p(Xs, ! A) :- !: A = foldl(func(X, Y) = f(X, Y), Xs, !. A)
transforms into
p(Xs, _5, _6) :- _6 = foldl(func(X, Y) = f(X, Y) :- true, Xs, _5)
state vars term
p(Xs, ! A) :- !: A = foldl(func(X, !. Y) = f(X, !. Y), Xs, !. A)
transforms into
p(Xs, _5, _6) :- _6 = foldl(func(X, _8) = _7 :- (true, _8 = _9), _7 = f(X, _9), Xs, _5)
state vars term
p(Xs, ! A) :- foldl(pred(X, Y, f(X, Y)) is det, Xs, ! A)
transforms into
p(Xs, _5, _6) :- foldl(pred(X, Y, f(X, Y)) is det :- true, Xs, _5, _6)
state vars term
p(Xs, ! A) :- foldl(pred(X, Y, Z) is det :- Z = f(X, Y), Xs, ! A)
transforms into
p(Xs, _6, _7) :- foldl(pred(X, Y, Z) is det :- Z = f(X, Y), Xs, _6, _7)
state vars term
p(Xs, ! A) :- foldl(pred(X, ! B) is det :- !: B = f(X, !. B), Xs, ! A)
transforms into
p(Xs, _5, _6) :- foldl(pred(X, _7, _8) is det :- _8 = f(X, _7), Xs, _5, _6)
state vars term
p(Xs, ! A) :- foldl(pred(X, ! A) is det :- !: A = f(X, !. A), Xs, ! A)
transforms into
p(Xs, _4, _5) :- foldl(pred(X, _6, _7) is det :- _7 = f(X, _6), Xs, _4, _5)
state vars term
p(Xs, ! A) :- !: A = foldl(func(X, Y) = f(X, Y) is semidet, Xs, !. A)
transforms into
p(Xs, _5, _6) :- _6 = foldl(func(X, Y) = f(X, Y) is semidet :- true, Xs, _5)
state vars term
p(Xs, ! A) :- !: A = foldl(func(X, !. Y) = f(X, !. Y) is semidet, Xs, !. A)
transforms into
p(Xs, _5, _6) :- _6 = foldl(func(X, _8) = _7 is semidet :- (true, _8 = _9), _7 = f(X, _9), Xs, _5)
state vars term
p(Xs, ! A) :- f(pred(X, ! B) :- g(pred(Y, ! C) :- h(Y, ! C), X, ! B), Xs, ! A)
transforms into
p(Xs, _7, _8) :- f(pred(X, _9, _10) :- g(pred(Y, _11, _12) :- h(Y, _11, _12), X, _9, _10), Xs, _7, _8)
state vars term
p(Xs, ! A) :- f(pred(X, ! A) :- g(pred(Y, ! A) :- h(Y, ! A), X, ! A), Xs, ! A)
transforms into
p(Xs, _5, _6) :- f(pred(X, _7, _8) :- g(pred(Y, _9, _10) :- h(Y, _9, _10), X, _7, _8), Xs, _5, _6)
state vars term
p(Xs, ! A) :- foldl(pred(X, ! B) is det :- !: B = f(X, !. A, !. B), Xs, ! A)
transforms into
p(Xs, _5, _6) :- foldl(pred(X, _8, _9) is det :- _9 = f(X, _5, _8), Xs, _5, _6)
state vars term
p(Xs, ! A) :- foldl(pred(X, ! B) is det :- !: B = f(X, !: A, !. B), Xs, ! A)
transforms into
p(Xs, _5, _6) :- foldl(pred(X, _7, _9) is det :- _9 = f(X, _6, _7), Xs, _5, _6)
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------
More information about the reviews
mailing list