Next: , Previous: Goals, Up: Syntax   [Contents]

2.12 State variables

Clauses may use ‘state variables’ as a shorthand for naming intermediate values in a sequence. That is, where in the plain syntax one might write 

    main(IO0, IO) :-
        io.write_string("The answer is ", IO0, IO1),
        io.write_int(calculate_answer(…), IO1, IO2),
        io.nl(IO3, IO).

using state variable syntax one could write 

    main(!IO) :-
        io.write_string("The answer is ", !IO),
        io.write_int(calculate_answer(…), !IO),
        io.nl(!IO).

A state variable is written ‘!.X’ or ‘!:X’, denoting the “current” or “next” value of the sequence labelled X. An argument ‘!X’ is shorthand for two state variable arguments ‘!.X, !:X’; that is, ‘p(…, !X, …)’ is parsed as ‘p(…, !.X, !:X, …)’.

State variables obey special scope rules. A state variable X must be explicitly introduced, and this can happen in one of four ways:

A state variable X in the enclosing scope of a lambda or if-then-else expression may only be referred to as ‘!.X’ (unless the enclosing X is shadowed by a more local state variable of the same name.)

For instance, the following clause employing a lambda expression 

p(A, B, !S) :-
    F =
        ( pred(C::in, D::out) is det :-
            q(C, D, !S)
        ),
    ( if F(A, E) then
        B = E
    else
        B = A
    ).

is illegal because it implicitly refers to ‘!:S’ inside the lambda expression. However 

p(A, B, !S) :-
    F =
        ( pred(C::in, D::out, !.S::in, !:S::out) is det :-
            q(C, D, !S)
        ),
    ( if F(A, E, !S) then
        B = E
    else
        B = A
    ).

is acceptable because the state variable S accessed inside the lambda expression is locally scoped to the lambda expression (shadowing the state variable of the same name outside the lambda expression), and the lambda expression may refer to the next version of a local state variable.

There are two restrictions concerning state variables in functions, whether they are defined by clauses or lambda expressions.

Within each clause, the compiler replaces each occurrence of !X in an argument list with two arguments: !.X, !:X, where !.X represents the current version of the state of !X, and !:X represents its next state. It then replaces all occurrences of !.X and !:X with ordinary variables in way that (in the general case) represents a sequence of updates to the state of X from an initial state to a final state.

This replacement is done by code that is equivalent to the ‘transform_goal’ and ‘transform_clause’ functions below. The basic operation used by these functions is substitution: ‘substitute(Goal, [!.X -> CurX, !:X -> NextX])’ stands for a copy of Goal in which every free occurrence of ‘!.X’ is replaced with CurX, and every free occurrence of ‘!:X’ is replaced with NextX. (A free occurrence is one not bound by the head of a clause or lambda, or by an explicit quantification.)

The ‘transform_goal(Goal, X, CurX, NextX)’ function’s inputs are

It returns a transformed version of Goal.

‘transform_goal’ has a case for each kind of Mercury goal. These cases are as follows.

Calls

Given a first order call such as ‘predname(ArgTerm1, ..., ArgTermN)’ or a higher-order call such as ‘PredVar(ArgTerm1, ..., ArgTermN)’, if any of the ArgTermI is !X, ‘transform_goal’ replaces that argument with two arguments: !.X and !:X. It then checks whether ‘!:X’ appears in the updated Call.

Note that !.X can occur in Call on its own (i.e. without !:X). Likewise, !:X can occur in Call without !.X, but this does not need separate handling.

Note that PredVar in a higher-order call may not be a reference to a state var, i.e it may not be !X, !.X or !:X.

Unifications

In a unification ‘TermA = TermB’, each of TermA and TermB may have one of the following four forms:

Note that TermA and TermB may not have the form !S.

State variable field updates

A state variable field update goal has the form 

!S ^ field_list := Term

where field_list is a valid field list See Record syntax. This means that 

!S ^ field1 := Term
!S ^ field1 ^ field2 := Term
!S ^ field1 ^ field2 ^ field3 := Term

are all valid field update goals. If S is X, ‘transform_goal’ replaces such goals with 

NextX = CurX ^ field_list := Term

Otherwise, it leaves the goal unchanged.

Conjunctions

Given a nonempty conjunction, whether a sequential conjunction such as Goal1, Goal2 or a parallel conjunction such as Goal1 & Goal2, ‘transform_goal’

This implies that first Goal1 updates the state of X from CurX to MidX, and then Goal2 updates the state of X from MidX to NextX.

Given the empty conjunction, i.e. the goal ‘true’, ‘transform_goal’ will replace it with 

NextX = CurX
Disjunctions

Given a disjunction such as Goal1 ; Goal2, ‘transform_goal’

This shows that both disjuncts start with the CurX, and both end with NextX. If a disjunct has no update of !X, then the value of NextX in that disjunct will be set to CurX.

The empty disjunction, i.e. the goal ‘fail’, cannot succeed, so what the value of !:X would be if it did succeed is moot. Therefore ‘transform_goal’ returns empty disjunctions unchanged.

Negations

Given a negated goal of the form ‘not NegatedGoal’ ‘transform_goal’

It does this because negated goals may not generate any outputs visible from the rest of the code, which means that any output they do generate must be local to the negated goal.

Negations that use ‘\+ NegatedGoal’ notation are handled exactly the same way,

If-then-elses

Given an if-then-else, whether it uses ( if Cond then Then else Else ) syntax or ( Cond -> Then ; Else ) syntax, ‘transform_goal’

This effectively treats an if-then-else as being a disjunction, with the first disjunct being the conjunction of the Cond and Then goals, and the second disjunct being the Else goal. (The Else goal is implicitly conjoined inside the second disjunct with the negation of the existential closure of Cond, since the else case is executed only if the condition has no solution.)

Bidirectional implications

‘transform_goal’ treats a bidirectional implication goal, which has the form GoalA <=> GoalB, as it were the conjunction of its two constituent unidirectional implications: GoalA => GoalB, GoalA <= GoalB.

Unidirectional implications

‘transform_goal’ treats a unidirectional implication, which has one of the two forms ‘GoalA => GoalB’ and ‘GoalB <= GoalA’, as if they were written as ‘not (GoalA, not GoalB)’.

Universal quantifications

‘transform_goal’ treats universal quantifications, which have the form ‘all Vars SubGoal’ as if they were written as ‘not (some Vars (not SubGoal))’. Note that in universal quantifications, Vars must a list of ordinary variables.

Existential quantifications

In existential quantifications, which have the form ‘some Vars SubGoal’, Vars must be a list, in which every element must be either ordinary variable (such as A), or a state variable (such as !B). (Note that Vars may not contain any element whose form is !.B or !:B.)

Note that state variables in Vars are handled by ‘transform_clause’ below.

The ‘transform_clause’ function’s input is a clause, which may be a non-DCG clause or a DCG clause, which have the forms 

predname(ArgTerm1, ..., ArgTermN) :- BodyGoal.

and 

predname(ArgTerm1, ..., ArgTermN) --> BodyGoal.

respectively. ‘transform_clause’ handles both the same way.

Actual application of this transformation would, in the general case, result in the generation of many different versions of each state variable, for which we need more names than just ‘CurX’, ‘TmpX’ and ‘NextX’. The Mercury compiler therefore uses

This transformation can lead to the introduction of chains of unifications for variables that do not otherwise play a role in the definition, such as ‘STATE_VARIABLE_X_5 = STATE_VARIABLE_X_6, STATE_VARIABLE_X_6 = STATE_VARIABLE_X_7, STATE_VARIABLE_X_7 = STATE_VARIABLE_X_8’. Where possible, the compiler automatically shortcircuits such sequences by removing any unneeded intermediate variables. In the above case, this would yield ‘STATE_VARIABLE_X_5 = STATE_VARIABLE_X_8’.

The following code fragments illustrate some appropriate uses of state variable syntax.

Threading the I/O state
main(!IO) :-
    io.write_string("The 100th prime is ", !IO),
    X = prime(100),
    io.write_int(X, !IO),
    io.nl(!IO).
Handling accumulators (1)
foldl2(_, [], !A, !B).
foldl2(P, [X | Xs], !A, !B) :-
    P(X, !A, !B),
    foldl2(P, Xs, !A, !B).
Handling accumulators (2)
iterate_while2(Test, Update, !A, !B) :-
    ( if Test(!.A, !.B) then
        Update(!A, !B),
        iterate_while2(Test, Update, !A, !B)
    else
        true
    ).
Introducing state
compute_out(InA, InB, InsC, Out) :-
    some [!State]
    (
        init_state(!:State),
        update_state_a(InA, !State),
        update_state_b(InB, !State),
        list.foldl(update_state_c, InC, !State),
        compute_output(!.State, Out)
    ).

Next: , Previous: Goals, Up: Syntax   [Contents]