[m-rev.] State variable syntax transformation

[Simon Taylor]

On 07-Feb-2002, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> Index: reference_manual.texi
> ===================================================================
> @@ -162,6 +163,7 @@
>  * Facts::
>  * Rules::
>  * Goals::
> +* State Variables::

I think we normally only capitalise the first word in section headings.

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

It would be nice to expand this a bit to explain the need for this
feature to users who are unfamiliar with single assignment languages. 

> +A state variable is written @samp{!. at var{X}} or @samp{!:@var{X}},
> +denoting the "current" or "next" value of the sequence labelled

Use ``current'' rather than "current".

> + 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}, ...)}.

Use @dots{} rather than `...'.

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

This sentence doesn't parse well.

> +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}.)

I'd just remove this (this is documented in the "Facts" section of the
"Syntax" chapter).

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

`CallOrUnification' is displayed as `CALLORUNIFICATION' in the info file.
Use Call_or_Unification instead.

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

I don't think you should refer to compilation passes when describing
the language semantics.

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

You should include an example showing a sensible use of state variables. 

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

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