[m-rev.] For review: state variable syntax (long diff)
Ralph Becket
rafe at cs.mu.OZ.AU
Mon Jan 21 17:05:30 AEDT 2002
I have implemented the state variable syntax transformation that was
discussed a few weeks ago. Let the flaming begin...
- Ralph
p.s. HTML for the documentation can be found at
file:///home/staff/rafe/mercury/ws-svars/mercury/doc/reference_manual.html#SEC12
This should be easier to read than the .texi diffs.
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 of 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: NEWS
===================================================================
RCS file: /home/mercury1/repository/mercury/NEWS,v
retrieving revision 1.237
diff -u -r1.237 NEWS
--- NEWS 15 Jan 2002 07:19:04 -0000 1.237
+++ NEWS 21 Jan 2002 05:44:41 -0000
@@ -3,6 +3,10 @@
Changes to the Mercury language:
+* A more general replacement for DCG syntax has been added to the language
+ to simplify the manipulation of threaded state. See the section on State
+ Variables in the Syntax chapter in the reference manual.
+
* If a higher-order function term has inst 'ground' it is now assumed to have
the standard higher-order function inst 'func(in, .., in) = out is det'.
This makes higher-order functional programming much easier, particularly when
Index: reference_manual.texi
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/reference_manual.texi,v
retrieving revision 1.236
diff -u -r1.236 reference_manual.texi
--- reference_manual.texi 16 Jan 2002 01:13:47 -0000 1.236
+++ reference_manual.texi 21 Jan 2002 05:39:21 -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,8 +740,133 @@
@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{!- at 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}, !- at var{X}}; that is,
+ at samp{p(..., !@var{X}, ...)} is parsed as
+ at samp{p(..., !+ at var{X}, !- at 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}.
+
+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{!- at 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{!- at 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{!- at 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.
+
@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.
Index: lexer.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/lexer.m,v
retrieving revision 1.34
diff -u -r1.34 lexer.m
--- lexer.m 28 Mar 2000 03:40:38 -0000 1.34
+++ lexer.m 18 Jan 2002 04:53:38 -0000
@@ -511,8 +511,9 @@
lexer__special_token('|', ht_sep).
lexer__special_token(',', comma).
lexer__special_token(';', name(";")).
-lexer__special_token('!', name("!")).
+% lexer__special_token('!', name("!")).
+lexer__graphic_token_char('!').
lexer__graphic_token_char('#').
lexer__graphic_token_char('$').
lexer__graphic_token_char('&').
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 18 Jan 2002 05:32:28 -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: builtin.m
===================================================================
RCS file: /home/mercury1/repository/mercury/library/builtin.m,v
retrieving revision 1.64
diff -u -r1.64 builtin.m
--- builtin.m 19 Dec 2001 02:54:04 -0000 1.64
+++ builtin.m 18 Jan 2002 04:58:18 -0000
@@ -174,11 +174,11 @@
% backwards compatibility with Prolog systems. But of course it only works
% if all your cuts are green cuts.
-:- pred ! is det.
-
-:- pred !(T, T).
-:- mode !(di, uo) is det.
-:- mode !(in, out) is det.
+% :- pred ! is det.
+%
+% :- pred !(T, T).
+% :- mode !(di, uo) is det.
+% :- mode !(in, out) is det.
%-----------------------------------------------------------------------------%
@@ -269,8 +269,8 @@
%-----------------------------------------------------------------------------%
-!.
-!(X, X).
+% !.
+% !(X, X).
%-----------------------------------------------------------------------------%
Index: mercury_compile.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mercury_compile.m,v
retrieving revision 1.229
diff -u -r1.229 mercury_compile.m
--- mercury_compile.m 11 Jan 2002 07:41:20 -0000 1.229
+++ mercury_compile.m 18 Jan 2002 05:20:12 -0000
@@ -1752,8 +1752,8 @@
mercury_compile__maybe_unneeded_code(HLDS39, Verbose, Stats, HLDS40),
mercury_compile__maybe_dump_hlds(HLDS40, "40", "unneeded_code"),
- mercury_compile__maybe_lco(HLDS40, Verbose, Stats, HLDS42), !,
- mercury_compile__maybe_dump_hlds(HLDS42, "42", "lco"), !,
+ mercury_compile__maybe_lco(HLDS40, Verbose, Stats, HLDS42),
+ mercury_compile__maybe_dump_hlds(HLDS42, "42", "lco"),
% DNF transformations should be after inlining.
mercury_compile__maybe_transform_dnf(HLDS40, Verbose, Stats, HLDS44),
Index: prog_io.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_io.m,v
retrieving revision 1.197
diff -u -r1.197 prog_io.m
--- prog_io.m 16 Jul 2001 08:21:04 -0000 1.197
+++ prog_io.m 21 Jan 2002 01:07:05 -0000
@@ -80,7 +80,7 @@
% Program is the parse tree.
:- type module_error
- ---> no_module_errors % no errors
+ ---> no_module_errors % no errors
; some_module_errors % some syntax errors
; fatal_module_errors. % couldn't open the file
@@ -193,7 +193,7 @@
:- implementation.
:- import_module prog_io_goal, prog_io_dcg, prog_io_pragma, prog_io_util.
-:- import_module prog_io_typeclass.
+:- import_module prog_io_typeclass, prog_io_state_vars.
:- import_module hlds_data, hlds_pred, prog_util, prog_out.
:- import_module globals, options, (inst).
:- import_module recompilation, recompilation_version.
@@ -433,13 +433,13 @@
%-----------------------------------------------------------------------------%
- % Read a source file from standard in, first reading in
+ % Read a source file from standard in, first reading in
% the input term by term and then parsing those terms and producing
% a high-level representation.
% Parsing is actually a 3-stage process instead of the
% normal two-stage process:
% lexical analysis (chars -> tokens),
- % parsing stage 1 (tokens -> terms),
+ % parsing stage 1 (tokens -> terms),
% parsing stage 2 (terms -> items).
% The final stage produces a list of program items, each of
% which may be a declaration or a clause.
@@ -514,7 +514,7 @@
{ FirstItem = pragma(source_file(NewSourceFileName)) }
->
read_first_item(DefaultModuleName, NewSourceFileName,
- ModuleName, Messages, Items, Error)
+ ModuleName, Messages, Items, Error)
;
%
% check if the first term was a `:- module' decl
@@ -539,12 +539,12 @@
ModuleName = StartModuleName,
Messages0 = []
;
- prog_out__sym_name_to_string(StartModuleName,
+ prog_out__sym_name_to_string(StartModuleName,
StartModuleNameString),
- string__append_list(["source file `", SourceFileName,
+ string__append_list(["source file `", SourceFileName,
"' contains module named `", StartModuleNameString,
"'"], WrongModuleWarning),
- maybe_add_warning(WarnWrong, MaybeFirstTerm, FirstContext,
+ maybe_add_warning(WarnWrong, MaybeFirstTerm, FirstContext,
WrongModuleWarning, [], Messages0),
% Which one should we use here?
@@ -568,7 +568,7 @@
{ MaybeFirstItem = ok(_FirstItem, FirstContext0) ->
FirstContext = FirstContext0
;
- term__context_init(SourceFileName, 1, FirstContext)
+ term__context_init(SourceFileName, 1, FirstContext)
},
{ WarnMissing = yes ->
dummy_term_with_context(FirstContext, FirstTerm),
@@ -638,7 +638,7 @@
read_items_loop(ModuleName, SourceFileName, Msgs1, Items1, Error1,
Msgs, Items, Error) -->
read_item(ModuleName, SourceFileName, MaybeItem),
- read_items_loop_2(MaybeItem, ModuleName, SourceFileName,
+ read_items_loop_2(MaybeItem, ModuleName, SourceFileName,
Msgs1, Items1, Error1, Msgs, Items, Error).
%-----------------------------------------------------------------------------%
@@ -679,7 +679,7 @@
Items1 = Items0,
Error1 = some_module_errors
},
- read_items_loop(ModuleName, SourceFileName, Msgs1, Items1, Error1,
+ read_items_loop(ModuleName, SourceFileName, Msgs1, Items1, Error1,
Msgs, Items, Error).
read_items_loop_2(ok(Item0, Context), ModuleName0, SourceFileName0,
@@ -739,7 +739,7 @@
ModuleName = ModuleName0,
Items1 = [Item - Context | Items0]
},
- read_items_loop(ModuleName, SourceFileName, Msgs1, Items1, Error1,
+ read_items_loop(ModuleName, SourceFileName, Msgs1, Items1, Error1,
Msgs, Items, Error).
%-----------------------------------------------------------------------------%
@@ -777,17 +777,24 @@
convert_item(ok(Item, Context), ok(Item, Context)).
convert_item(error(M, T), error(M, T)).
-parse_item(ModuleName, VarSet, Term, Result) :-
- ( %%% some [Decl, DeclContext]
+parse_item(ModuleName, VarSet0, Term, Result) :-
+ ( %%% some [Decl, DeclContext]
Term = term__functor(term__atom(":-"), [Decl], _DeclContext)
->
% It's a declaration
- parse_decl(ModuleName, VarSet, Decl, Result)
+ parse_decl(ModuleName, VarSet0, Decl, Result)
; %%% some [DCG_H, DCG_B, DCG_Context]
% It's a DCG clause
- Term = term__functor(term__atom("-->"), [DCG_H, DCG_B],
+ Term = term__functor(term__atom("-->"), [DCG_H0, DCG_B0],
DCG_Context)
->
+ % First perform the state variable transformation.
+ %
+ transform_state_vars(DCG_H0, DCG_H, DCG_B0, DCG_B,
+ VarSet0, VarSet),
+
+ % Then the DCG expansion.
+ %
parse_dcg_clause(ModuleName, VarSet, DCG_H, DCG_B,
DCG_Context, Result)
;
@@ -797,24 +804,30 @@
TermContext)
->
% it's a rule
- Head = H,
- Body = B,
+ Head0 = H,
+ Body0 = B,
TheContext = TermContext
;
% it's a fact
- Head = Term,
+ Head0 = Term,
(
- Head = term__functor(_Functor, _Args,
- HeadContext)
+ Head0 = term__functor(_Functor, _Args,
+ Head0Context)
->
- TheContext = HeadContext
+ TheContext = Head0Context
;
% term consists of just a single
% variable - the context has been lost
term__context_init(TheContext)
),
- Body = term__functor(term__atom("true"), [], TheContext)
+ Body0 = term__functor(term__atom("true"), [],
+ TheContext)
),
+
+ % Now we perform the state variable transformation.
+ %
+ transform_state_vars(Head0, Head, Body0, Body, VarSet0, VarSet),
+
varset__coerce(VarSet, ProgVarSet),
parse_goal(Body, ProgVarSet, Body2, ProgVarSet2),
(
@@ -1795,7 +1808,7 @@
ClassContext, Attributes0, Result) :-
( convert_type_and_mode_list(As0, As) ->
( verify_type_and_mode_list(As) ->
- get_purity(Attributes0, Purity, Attributes),
+ get_purity(Attributes0, Purity, Attributes),
varset__coerce(VarSet0, TVarSet),
varset__coerce(VarSet0, IVarSet),
Result0 = ok(pred_or_func(TVarSet, IVarSet, ExistQVars,
@@ -1851,7 +1864,7 @@
% 2. existential quantifiers some 950
% 3. universal constraints <= 920
% 4. existential constraints => 920 [*]
- % 5. the decl itself pred or func 800
+ % 5. the decl itself pred or func 800
%
% When we reach here, Attributes0 contains declaration attributes
% in the opposite order -- innermost to outermost -- so we reverse
@@ -2630,7 +2643,7 @@
process_maybe1(make_cons_symbol_specifier, Result0, Result)
).
-% Once we've parsed the appropriate type of symbol specifier, we
+% Once we've parsed the appropriate type of symbol specifier, we
% need to convert it to a sym_specifier.
:- pred make_pred_symbol_specifier(pred_specifier::in, sym_specifier::out)
@@ -2752,7 +2765,7 @@
( Args0 = [] ->
Result = sym(name(Name))
;
- list__map(term__coerce, Args0, Args),
+ list__map(term__coerce, Args0, Args),
Result = name_args(Name, Args)
).
process_typed_predicate_specifier(error(Msg, Term), error(Msg, Term)).
@@ -2763,8 +2776,8 @@
%-----------------------------------------------------------------------------%
-% Parsing the name & argument types of a constructor specifier is
-% exactly the same as parsing a predicate specifier...
+% Parsing the name & argument types of a constructor specifier is
+% exactly the same as parsing a predicate specifier...
:- pred parse_arg_types_specifier(term, maybe1(pred_specifier)).
:- mode parse_arg_types_specifier(in, out) is det.
@@ -2779,8 +2792,8 @@
process_typed_predicate_specifier(TermResult, Result)
).
-% ... but we have to convert the result back into the appropriate
-% format.
+% ... but we have to convert the result back into the appropriate
+% format.
:- pred process_typed_constructor_specifier(maybe1(pred_specifier),
maybe1(type), maybe1(cons_specifier)).
@@ -2812,7 +2825,7 @@
:- mode parse_symbol_name_specifier(in, out) is det.
parse_symbol_name_specifier(Term, Result) :-
( %%% some [NameTerm, ArityTerm, Context]
- Term = term__functor(term__atom("/"), [NameTerm, ArityTerm], _Context)
+ Term = term__functor(term__atom("/"), [NameTerm, ArityTerm], _Context)
->
( %%% some [Arity, Context2]
ArityTerm = term__functor(term__integer(Arity), [], _Context2)
@@ -2857,17 +2870,17 @@
:- mode parse_symbol_name(in, out) is det.
parse_symbol_name(Term, Result) :-
(
- Term = term__functor(term__atom(":"), [ModuleTerm, NameTerm], _Context)
+ Term = term__functor(term__atom(":"), [ModuleTerm, NameTerm], _Context)
->
(
NameTerm = term__functor(term__atom(Name), [], _Context1)
->
parse_symbol_name(ModuleTerm, ModuleResult),
(
- ModuleResult = ok(Module),
+ ModuleResult = ok(Module),
Result = ok(qualified(Module, Name))
;
- ModuleResult = error(_, _),
+ ModuleResult = error(_, _),
term__coerce(Term, ErrorTerm),
Result = error("module name identifier expected before ':' in qualified symbol name", ErrorTerm)
)
@@ -2879,7 +2892,7 @@
(
Term = term__functor(term__atom(Name), [], _Context3)
->
- string_to_sym_name(Name, "__", SymName),
+ string_to_sym_name(Name, "__", SymName),
Result = ok(SymName)
;
term__coerce(Term, ErrorTerm),
@@ -2950,7 +2963,7 @@
parse_qualified_term(Term, ContainingTerm, Msg, Result) :-
(
- Term = term__functor(term__atom(":"), [ModuleTerm, NameArgsTerm],
+ Term = term__functor(term__atom(":"), [ModuleTerm, NameArgsTerm],
_Context)
->
(
@@ -2958,10 +2971,10 @@
->
parse_symbol_name(ModuleTerm, ModuleResult),
(
- ModuleResult = ok(Module),
- Result = ok(qualified(Module, Name), Args)
+ ModuleResult = ok(Module),
+ Result = ok(qualified(Module, Name), Args)
;
- ModuleResult = error(_, _),
+ ModuleResult = error(_, _),
term__coerce(Term, ErrorTerm),
Result = error("module name identifier expected before ':' in qualified symbol name", ErrorTerm)
)
@@ -2983,9 +2996,9 @@
% (hopefully that _will_ have a term__context).
%
( Term = term__variable(_) ->
- ErrorTerm0 = ContainingTerm
+ ErrorTerm0 = ContainingTerm
;
- ErrorTerm0 = Term
+ ErrorTerm0 = Term
),
term__coerce(ErrorTerm0, ErrorTerm),
Result = error(ErrorMsg, ErrorTerm)
@@ -3031,7 +3044,7 @@
%-----------------------------------------------------------------------------%
% For the moment, an OpSpecifier is just a symbol name specifier.
-% XXX We should allow specifying the fixity of an operator
+% XXX We should allow specifying the fixity of an operator
:- pred parse_op_specifier(term, maybe1(op_specifier)).
:- mode parse_op_specifier(in, out) is det.
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 21 Jan 2002 01:09:30 -0000
@@ -0,0 +1,411 @@
+%------------------------------------------------------------------------------%
+% 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.
+%
+% XXX Add a check that no state variable has the same name as a normal var.
+%
+%------------------------------------------------------------------------------%
+
+:- 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, exception.
+
+
+
+:- type subs
+ ---> subs(
+ this :: map(var, var),
+ next :: map(var, var)
+ ).
+
+:- type this_or_next
+ ---> this
+ ; next.
+
+%------------------------------------------------------------------------------%
+
+:- pred init_subs(term, subs, varset, varset).
+:- mode init_subs(in, out, in, out) is det.
+
+init_subs(T, subs(This, Next), VS0, VS) :-
+ ThisXs = in_state_vars(T),
+ NextXs = out_state_vars(T),
+ list__foldl2(set_state_var_map, ThisXs, map__init, This, VS0, VS1),
+ list__foldl2(set_state_var_map, NextXs, map__init, Next, VS1, VS ).
+
+
+:- pred set_state_var_map(var, map(var, var), map(var, var), varset, varset).
+:- mode set_state_var_map(in, in, out, in, out) is det.
+
+set_state_var_map(X, Map, Map ^ elem(X) := Y, VS0, VS) :-
+ varset__new_var(VS0, Y, VS).
+
+%------------------------------------------------------------------------------%
+
+:- func in_state_vars(term) = list(var).
+
+in_state_vars(T) = solutions(state_var(this, T)).
+
+
+:- func out_state_vars(term) = list(var).
+
+out_state_vars(T) = solutions(state_var(next, T)).
+
+
+:- pred state_var(this_or_next, term, var).
+:- mode state_var(in, in, out) is nondet.
+
+state_var(TorN, T @ functor(_F, _Ts, _C), X) :-
+ state_var_term(T, TorN, X).
+
+state_var(TorN, functor(_F, Ts, _C), X) :-
+ list__member(T, Ts),
+ state_var(TorN, T, X).
+
+%------------------------------------------------------------------------------%
+
+:- 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).
+
+%------------------------------------------------------------------------------%
+
+transform_state_vars(Head0, Head, Body0, Body, VarSet0, VarSet) :-
+
+ Head1 = expand_thisnext_state_vars(Head0),
+ Body1 = expand_thisnext_state_vars(Body0),
+
+ init_subs(
+ functor(atom(":-"), [Head1, Body1], term__context_init),
+ S,
+ VarSet0, VarSet1
+ ),
+
+ xform_head(S, Head1, Head, VarSet1, VarSet2),
+ xform_goal(S, Body1, Body, VarSet2, VarSet ).
+
+%------------------------------------------------------------------------------%
+
+ % 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, VS, VS) :-
+ T = subs_state_vars(S, T0).
+
+%------------------------------------------------------------------------------%
+
+:- pred xform_atomic(subs, term, term, varset, varset).
+:- mode xform_atomic(in, in, out, in, out) is det.
+
+xform_atomic(S, T0, T, VS, VS) :-
+ NextXs = out_state_vars(T0),
+ T1 = subs_state_vars(S, T0),
+ T = conj_unifiers(S, NextXs, T1).
+
+%------------------------------------------------------------------------------%
+
+:- func subs_state_vars(subs, term) = term.
+
+subs_state_vars(_, variable(X)) = variable(X).
+ % XXX This might be a good place to make the state var/normal var
+ % separation check.
+
+subs_state_vars(S, T @ functor(F, Ts, C)) =
+ ( if state_var_term(T, TorN, X)
+ then subs_state_var(S, TorN, X)
+ else functor(F, list__map(subs_state_vars(S), 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, list(var), term) = term.
+
+conj_unifiers(S, NextXs, T) =
+ map__foldl(conj_unifier(S, NextXs), S ^ this, T).
+
+
+:- func conj_unifier(subs, list(var), var, var, term) = term.
+
+conj_unifier(S, NextXs, X, ThisX, T) =
+ ( if not list__member(X, NextXs), 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, functor(atom("true"), [], C)], 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, functor(atom("true"), [], C)], 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(set_state_var_map, Xs, map__init, MiddleMap, VS0, VS),
+ SA = ( S ^ next := MiddleMap),
+ SB = ( S ^ this := MiddleMap).
+
+%------------------------------------------------------------------------------%
+%------------------------------------------------------------------------------%
+
+transform_clause(T0, T, VS0, VS) :-
+ ( if T0 = functor(atom(":-"), [Head0, Body0], _) then
+ transform_state_vars(Head0, Head, Body0, Body, VS0, VS)
+ else
+ transform_state_vars(T0, Head,
+ functor(atom("true"), [], term__context_init), Body, VS0, VS)
+ ),
+ T = functor(atom(":-"), [Head, Body], term__context_init).
+
--------------------------------------------------------------------------
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