This chapter covers the semantics of Mercury clauses, and the goals and expressions they contain. The first section gives an informal overview of the semantics; if you are already familiar with logic programming you may wish to skip it and start with Goals.
Full details of the language semantics can be found in Formal semantics.
There is no agreed upon definition of “declarative programming”. One notable characteristic of Mercury as a declarative language, however, is that it has both a declarative and an operational semantics. The declarative semantics is conceptually the simpler of the two: it is only concerned with the relationship between inputs and outputs, and not the steps taken to execute a program. The operational semantics is additionally concerned with these steps. This is often expressed by saying that the declarative semantics is about “what” whereas the operational semantics is about “how”.
In the remainder of this section we introduce each of these semantics.
The declarative semantics is concerned with “truth”. For example, it is true that 1 plus 1 is 2, and that the length of the list [1, 2, 3] is 3. Statements that are either true or false like this are known as propositions, e.g., 1 + 1 = 2 and 1 + 2 = 5 are both propositions; if + is interpreted as integer addition then the first proposition is true and the second is false.
Mercury clauses state things that are true about the function or predicate being defined. To illustrate we will use an example from the previous chapter. (Note that, here and below, some declarations would need to be added to make this compile.)
length([]) = 0. length([_ | Xs]) = 1 + length(Xs).
Both of these clauses are facts about the function length/1.
The first simply states that the length of an empty list is zero.
The second states that no matter what expressions we substitute for
the variables ‘Xs’ and ‘_’,
the length of ‘[_ | Xs]’ will be one greater than
the length of ‘Xs’.
In other words, the length of a non-empty list
is one greater than the length of its tail.
These two statements are true according to our intuitive idea of length. Furthermore, we can see that the clauses cover every possible list, since every list is either empty or non-empty, and every non-empty list has a tail that is also a list. Perhaps surprisingly, this is enough to conclude that our implementation of list length is correct, at least as far as its arguments and return values are concerned.
As another example,
the following clauses define a predicate named append/3,
which is intended to be true if
the third argument is the list that results from appending
the first and second arguments.
(Equivalently, we could say that it is intended to be true if
it is possible to split the list in the third argument
to produce the first and second arguments.)
append([], Bs, Bs).
append([X | As], Bs, [X | Cs]) :-
append(As, Bs, Cs).
The first clause is a fact that states if you append the empty list and any other list, the result will be the same as that other list. The second clause is a rule; these are taken as logical implications in which the body implies the head (i.e. ‘:-’ is interpreted as reverse implication). So this is stating that, for any substitution, if ‘Cs’ is the result of appending ‘As’ and ‘Bs’, then ‘[X | Cs]’ is the result of appending ‘[X | As]’ and ‘Bs’.
Again, both clauses are true according to the intended interpretation, which is defined as all of the propositions about the functions and predicates in the program that the programmer intends to be true. And the definition is complete, meaning that for every proposition that is intended to be true there is either a fact that covers it, or a rule whose head covers it and (under the same substitution) whose body is intended to be true. Thus we can conclude in a similar way to above that our code is correct.
The declarative semantics of a Mercury program is defined as all of the propositions that can be inferred to be true from the clauses of the program (with some additional axioms). If the program is producing incorrect output, this implies that there is a difference between the declarative semantics and the intended interpretation. From the above discussion, there must be some clause that is false in the intended interpretation, or some definition that is incomplete.
This is the reason for having a declarative semantics. Despite it being relatively simple—you only need to know about which propositions are true and which are false, and not how the program actually executes—it is still effective in reasoning about your program, even so far as to be able to localize a bug observed in the output down to individual clauses or definitions.
The declarative semantics does not tell us whether our program will terminate, for example, or what its computational complexity is. For that we need the operational semantics, which tells us how the program will be executed.
Execution in Mercury starts with a goal, which is a proposition that may contain some variables. The aim of execution is to find a substitution for which the proposition is true. If it does, we refer to this as success, and we refer to the substitution that was found as a solution. If execution determines that there are no such substitutions, we refer to this as failure.
Say, for example,
we start with a goal of ‘N = length([1, 2])’.
Function evaluation is strict,
depth-first, and left-to-right,
so we want to call the ‘length/1’ function first.
To do this, we match the argument with
the heads of the clauses that define the function
to find the clause that is applicable.
In this case the second clause matches,
with the substitution of Xs → [2]
(the substitution for ‘_’ is irrelevant,
since any other occurrence of ‘_’
is considered a distinct variable).
Applying this substitution to the body
then replacing it in the goal gives us a new goal,
namely ‘N = 1 + length([2])’.
Repeating this process a second time
gives us the goal ‘N = 1 + 1 + length([])’.
When we call the function the third time
it will match the first clause,
and the new goal will be ‘N = 1 + 1 + 0’.
At this point we can evaluate the ‘+/2’ calls
and get a result of ‘N = 2’.
It is trivial to find a substitution that makes this proposition true:
just map N to the literal 2.
Now consider the goal ‘append(As, Bs, [1])’.
In this case the first two arguments are free,
meaning that they are variables that
are not mapped to anything in the current substitution,
and the third argument is ground,
meaning that it does not contain any variables
after applying the current substitution.
In this case when we try to match (or unify)
the goal with a clause,
both clauses match.
We arbitrarily pick the first one,
but we also push a choice point onto a stack,
which will allow us to return to this point later on
and try the other clause if we need to.
Matching with the first clause gives us
the substitution As → [], Bs → [1];
since this clause is a fact,
we succeed with this substitution as our solution.
If a later goal fails, we pop the previous choice point off the stack in order to search for a different solution. This time we want to try unifying our goal with the head of the second clause, that is, we want to find a substitution such that
append(As, Bs, [1]) = append([X1 | As1], Bs1, [X1 | Cs1])
(the variables from the clause have been given a numerical suffix,
which is to indicate that they came from a different scope
and are not the same variables as those in the goal).
The substitution we use is
As → [1 | As1], Bs → Bs1, X1 → 1, Cs1 → [];
you can check that this does indeed unify the two terms.
Note that information is effectively flowing in both directions:
variables from both the goal and the clause
(i.e. the caller and callee) are bound by this substitution.
This is different from pattern matching in many other languages,
in which only variables in the pattern are bound.
Applying this substitution to the body of the selected clause
gives us our new goal,
‘append(As1, Bs1, [])’.
Only the first clause matches,
with the substitution of As1 → [], Bs1 → [],
and the clause is a fact,
so this is a solution to this call to append.
To find the solution to the parent goal we compose this substitution
with the one from before,
giving As → [1], Bs → [].
We have now found two solutions for our goal:
one with As being the empty list and Bs being [1],
and the other with As being [1]
and Bs being the empty list.
These are all of the possible solutions;
if we wanted to search for another
we would find the choice point stack to be empty,
hence we would fail.
A goal is a term that takes one of the following forms.
CallAny goal which is a functor term that does not match any of the other forms below is a first-order predicate call. The principal functor determines the predicate called, which must be visible (see Modules). The arguments, if present, are expressions.
call(Closure)call(Closure1, Arg1)call(Closure2, Arg1, Arg2)call(Closure3, Arg1, Arg2, Arg3)…ClosureClosure1(Arg1)Closure2(Arg1, Arg2)Closure3(Arg1, Arg2, Arg3)…A higher-order predicate call.
The closure and arguments are expressions.
‘call(Closure)’ and ‘Closure’ just call the specified closure.
The other forms append the specified arguments
onto the argument list of the closure before calling it.
A higher-order predicate call written using
an apply term with N arguments
is equivalent to the form using call/N+1.
See Higher-order.
Expr1 = Expr2A unification. Expr1 and Expr2 are expressions.
!Var ^ field_list := ExprA state variable field update. See State variables.
Goal1, Goal2A conjunction. Goal1 and Goal2 are goals.
Goal1 & Goal2A parallel conjunction.
Goal1 and Goal2 are goals.
This has the same declarative semantics as normal conjunction.
Operationally,
implementations may execute Goal1 & Goal2 in parallel.
The order in which parallel conjuncts begin execution is not fixed.
It is an error for Goal1 or Goal2
to have a determinism other than det or cc_multi.
See Determinism categories.
Goal1 ; Goal2A disjunction, where Goal1 is not of the form ‘Goal1a -> Goal1b’ (since that would make it an if-then-else, below). Goal1 and Goal2 are goals.
trueThe empty conjunction. Always succeeds exactly once.
failThe empty disjunction. Always fails.
if CondGoal then ThenGoal else ElseGoalCondGoal -> ThenGoal ; ElseGoalAn if-then-else. The two different syntaxes have identical semantics. CondGoal, ThenGoal, and ElseGoal are goals. Note that the “else” part is not optional.
The declarative semantics of an if-then-else is given by
( CondGoal, ThenGoal ; not(CondGoal), ElseGoal ),
but the operational semantics is different,
and it is treated differently for the purposes of determinism inference
(see Determinism).
Operationally, it executes the CondGoal,
and if that succeeds, then execution continues with the ThenGoal;
otherwise, i.e. if CondGoal fails without producing any solutions,
it executes the ElseGoal.
Note that CondGoal can be nondeterministic—if the CondGoal
succeeds more than once then
the ThenGoal is executed once for each of the solutions.
If CondGoal is an explicit existential quantification,
some Vars QuantifiedCondGoal, then the variables Vars
are existentially quantified over the conjunction of the goals
QuantifiedCondGoal and ThenGoal
(see existential quantifications, below).
Explicit existential quantifications that occur as subgoals of CondGoal
do not affect the scope of variables in the “then” part.
For example, in
( if some [V] C then T else E )
the variable V is quantified over the conjunction of the goals C and T because the top-level goal of the condition is an explicit existential quantification, but in
( if true, some [V] C then T else E )
the variable V is only quantified over C because the top-level goal of the condition is not an explicit existential quantification.
not Goal\+ GoalA negation. Goal is a goal. The two different syntaxes have identical semantics: both forms are operationally equivalent to ‘if Goal then fail else true’.
Expr1 \= Expr2An inequality. Expr1 and Expr2 are expressions. This is an abbreviation for ‘not (Expr1 = Expr2)’.
try Params Goal … catch Expr -> CGoal …A try goal. Exceptions thrown during the execution of Goal may be caught and handled. A summary of the try goal syntax is:
try Params Goal
then ThenGoal
else ElseGoal
catch Expr -> CatchGoal
…
catch_any CatchAnyVar -> CatchAnyGoal
See Exception handling for the full details.
some Vars GoalAn existential quantification. Goal is a goal and Vars is a list whose elements are either variables or state variables (a single list may contain both). The case where there are state variables is described in State variables; here we discuss the case where they are all plain variables.
Each existential quantification introduces a new scope. The variables in Vars are local to the goal Goal: for each variable named in Vars, any occurrences of variables with that name in Goal are considered to name a different variable than any variables with the same name that occur outside of the existential quantification.
Operationally, existential quantification has no effect, so apart from its effect on variable scoping, ‘some Vars Goal’ is the same as ‘Goal’.
Mercury’s rules for implicit quantification (see Implicit quantification) mean that variables are often implicitly existentially quantified. There is usually no need to write existential quantifiers explicitly.
all Vars GoalA universal quantification. Goal is a goal and Vars is a list of variables (they may not be state variables). This goal is an abbreviation for ‘not (some Vars not Goal)’.
Goal1 => Goal2An implication. Goal1 and Goal2 are goals. This is an abbreviation for ‘not (Goal1, not Goal2)’.
Goal1 <= Goal2A reverse implication. Goal1 and Goal2 are goals. This is an abbreviation for ‘not (Goal2, not Goal1)’.
Goal1 <=> Goal2A logical equivalence. Goal1 and Goal2 are goals. This is an abbreviation for ‘(Goal1 => Goal2), (Goal1 <= Goal2’).
promise_pure GoalA purity cast. Goal is a goal. This goal promises that Goal implements a pure interface, even though it may include impure and semipure components.
promise_semipure GoalA purity cast. Goal is a goal. This goal promises that Goal implements a semipure interface, even though it may include impure components.
promise_impure GoalA purity cast. Goal is a goal. This goal instructs the compiler to treat Goal as though it were impure, regardless of its actual purity.
promise_equivalent_solutions Vars GoalA determinism cast.
Vars is a list of variables
and Goal is a goal.
This goal promises that Vars
is the set of variables bound by Goal,
and that while Goal may have more than one solution,
all of these solutions are equivalent
with respect to the equality theories of the variables in Vars.
It is an error for Vars to include a variable not bound by Goal
or for Goal to bind a non-local variable
that is not listed in Vars
(non-local variables with inst any are assumed to be further constrained
by Goal and must also be included in Vars).
If Goal has determinism multi or cc_multi then
promise_equivalent_solutions Vars Goal
has determinism det.
If Goal has determinism nondet or cc_nondet then
promise_equivalent_solutions Vars Goal
has determinism semidet.
promise_equivalent_solution_sets Vars GoalA determinism cast,
of the kind performed by promise_equivalent_solutions,
on any goals of the form
arbitrary ArbVars ArbGoal inside Goal,
of which there should be at least one.
Vars and ArbVars must be lists of variables,
and Goal and ArbGoal must be goals.
Vars must be the set of variables bound by Goal,
and ArbVars must be the set of variables bound by ArbGoal,
It is an error for Vars to include a variable not bound by Goal
or for Goal to bind a non-local variable
that is not listed in Vars,
and similarly for ArbVars and ArbGoal.
The intersection of Vars and the ArbVars list
of any arbitrary ArbVars ArbGoal goal
included inside Goal must be empty.
The overall promise_equivalent_solution_sets goal promises that
the set of solutions computed for Vars by Goal
is not influenced by which of the possible solutions
for ArbVars is computed by each ArbGoal;
while different choices of solutions for some of the ArbGoals
may lead to syntactically different solutions for Vars for Goal,
all of these solutions are equivalent
with respect to the equality theories of the variables in Vars.
If an ArbGoal has determinism multi or cc_multi then
arbitrary ArbVars ArbGoal has determinism det.
If ArbGoal has determinism nondet or cc_nondet then
arbitrary ArbVars ArbGoal has determinism semidet.
Goal itself may have any determinism.
There is no requirement that given one of the ArbGoals, all its solutions must be equivalent with respect to the equality theories of the corresponding ArbVars; in fact, in typical usage, this won’t be the case. The different solutions of the nested arbitrary goals are not required to be equivalent in any context except the promise_equivalent_solution_sets goal they are nested inside.
arbitrary ArbVars ArbGoalGoals of this form are only allowed to occur inside
promise_equivalent_solution_sets Vars Goal goals.
See the preceding description for details.
require_det Goalrequire_semidet Goalrequire_multi Goalrequire_nondet Goalrequire_cc_multi Goalrequire_cc_nondet Goalrequire_erroneous Goalrequire_failure GoalA determinism check, typically used to enhance the robustness of code.
Goal is a goal.
If Goal is det, then
require_det Goal is equivalent to just Goal.
If Goal is not det,
then the compiler is required to generate an error message.
The require_det keyword may be replaced with
require_semidet,
require_multi,
require_nondet,
require_cc_multi,
require_cc_nondet,
require_erroneous or
require_failure,
each of which requires Goal to have the named determinism.
require_complete_switch [Var] GoalA switch completeness check, typically used to enhance the robustness of code.
Var is a variable and Goal is a goal.
If Goal is a switch on Var
and the switch is complete,
i.e. the switch has an arm for every function symbol that Var
could be bound to at this point in the code,
then require_complete_switch [Var] Goal
is equivalent to Goal.
If Goal is a switch on Var but is not complete,
or Goal is not a switch on Var at all,
then the compiler is required to generate an error message.
require_switch_arms_det [Var] Goalrequire_switch_arms_semidet [Var] Goalrequire_switch_arms_multi [Var] Goalrequire_switch_arms_nondet [Var] Goalrequire_switch_arms_cc_multi [Var] Goalrequire_switch_arms_cc_nondet [Var] Goalrequire_switch_arms_erroneous [Var] Goalrequire_switch_arms_failure [Var] Goalrequire_switch_arms_det is a determinism check,
typically used to enhance the robustness of code.
Var is a variable and Goal is a goal.
If Goal is a switch on Var,
and all arms of the switch would be allowable in a det context,
require_switch_arms_det [Var] Goal
is equivalent to Goal.
If Goal is not a switch on Var,
or if it is a switch on Var
but some of its arms would not be allowable in a det context,
then the compiler is required to generate an error message.
The require_switch_arms_det keyword may be replaced with
require_switch_arms_semidet,
require_switch_arms_multi,
require_switch_arms_nondet,
require_switch_arms_cc_multi,
require_switch_arms_cc_nondet,
require_switch_arms_erroneous or
require_switch_arms_failure,
each of which requires
the arms of the switch on Var to have a determinism
that is at least as tight as the named determinism.
The determinism match need not be exact;
the requirement is that the arms’ determinisms should make
all the promises about the minimum and maximum number of solutions
as the named determinism does.
For example, it is ok to have a det switch arm
in a require_switch_arms_semidet scope,
even though it would not be ok
to have a det goal in a require_semidet scope.
disable_warnings [Warnings] Goaldisable_warning [Warnings] GoalGoal is a goal
and Warnings is a comma-separated list of names.
The Mercury compiler can generate warnings
about several kinds of constructs that whose legal Mercury semantics
is likely to differ from the semantics intended by the programmer.
While such warnings are useful most of the time,
they are a distraction in cases where the programmer’s intention
does match the legal semantics.
Programmers can disable all warnings of a particular kind for an entire module
by compiling that module with the appropriate compiler option,
but in many cases this is not a good idea,
since some of the warnings it disables may not have been mistaken.
This is what these goals are for.
The goal disable_warnings [Warnings] Goal
is equivalent to Goal in all respects, with one exception:
the Mercury compiler will not generate warnings of any of the categories
whose names appear in [Warnings].
At the moment, the Mercury compiler supports the disabling of the following warning categories:
singleton_varsDisable the generation of singleton variable warnings.
suspected_occurs_check_failureDisable the generation of warnings about code that looks like it unifies a variable with a term that contains that same variable.
suspicious_recursionDisable the generation of warnings about suspicious recursive calls.
no_solution_disjunctDisable the generation of warnings about disjuncts that can have no solution. This is usually done to shut up such a warning in a multi-mode predicate where the disjunct in question is a switch arm in another mode. (The difference is that a disjunct that cannot succeed has no meaningful use, but a switch arm that cannot succeed does have one: a switch may need that arm to make it complete.)
unknown_format_callsDisable the generation of warnings about calls to
string.format, io.format or stream.string_writer.format
for which the compiler cannot tell whether there are any mismatches
between the format string and the supplied values.
The keyword starting this scope may be written
either as disable_warnings or as disable_warning.
This is intended to make the code read more naturally
regardless of whether the list contains the name of
more than one warning category.
trace Params GoalA trace goal, typically used for debugging or logging. Goal is a goal and Params is a list of trace parameters. Some trace parameters specify compile time or run time conditions; if any of these conditions are false, Goal will not be executed. Since in some program invocations Goal may be replaced by ‘true’ in this way, Goal may not bind or change the instantiation state of any variables it shares with the surrounding context. The things it may do are thus restricted to side effects; good programming style requires these side effects to not have any effect on the execution of the program itself, but to be confined to the provision of extra information for the user of the program. See Trace goals for the details.
event GoalAn event goal. Goal is a predicate call. Event goals are an extension used by the Melbourne Mercury implementation to support user-defined events in the Mercury debugger, ‘mdb’. See the “Debugging” chapter of the Mercury User’s Guide for further details.
Syntactically, an expression is just a term. Semantically, an expression is a variable, a literal, a functor expression, or a special expression. A special expression is a conditional expression, a unification expression, a state variable, an explicit type qualification, a type conversion expression, a lambda expression, an apply expression, or a field access expression.
A literal is a string, an integer, a float, or an implementation-defined literal (note that character literals are just single character names; see below).
Implementation-defined literals are symbolic names whose value represents a property of the compilation environment or the context in which it appears. The implementation replaces these symbolic names with actual literals during compilation. Implementation-defined literals can only appear within clauses. The following must be supported by all Mercury implementations:
A string that gives the name of the file that contains the module being compiled. If the name of the file cannot be determined, then it is replaced by an arbitrary string.
The line number (integer) of the goal in which the literal appears, or -1 if it cannot be determined.
A string representation of the fully qualified module name.
A string containing the fully qualified predicate or function name and arity.
The Melbourne Mercury implementation additionally supports the following extension:
The grade (string) in which the module is compiled.
A functor expression is a name or a compound expression. A compound expression is a compound term that does not match the form of a special expression, and whose arguments are expressions. If a functor expression is not a character literal, its principal functor must be the name of a visible function, predicate, or data constructor (except for field specifiers, for which the corresponding field access function must be visible; see below).
Character literals in Mercury are single character names,
possibly quoted.
Since they sometimes require quotes
and sometimes require parentheses,
for code consistency we recommend
writing all character literals with quotes and
(except where used as arguments)
parentheses.
For example, Char = ('+') ; Char = ('''').
Special expressions (not including field access expressions, which are covered below) take one of the following forms.
if Goal then ThenExpr else ElseExprGoal -> ThenExpr ; ElseExprA conditional expression. Goal is a goal; ThenExpr and ElseExpr are both expressions. The two forms are equivalent. The meaning of a conditional expression is that if Goal is true it is equivalent to ThenExpr, otherwise it is equivalent to ElseExpr.
If Goal takes the form some [X, Y, Z] …
then the scope of X, Y, and Z includes ThenExpr.
See the related discussion regarding if-then-else goals.
X @ YA unification expression. X and Y are both expressions. The meaning of a unification expression is that the arguments are unified, and the expression is equivalent to the unified value.
The strict sequential operational semantics (see Formal semantics)
of an expression X @ Y
is that the expression is replaced by a fresh variable Z,
and immediately after Z is evaluated,
the conjunction Z = X, Z = Y is evaluated.
For example
p(X @ f(_, _), X).
is equivalent to
p(Z, X) :-
Z = X,
Z = f(_, _).
Unification expressions are particularly useful when writing switches (see Determinism checking and inference), as the arguments of a unification expression are examined when checking for switches. The arguments of an equivalent user-defined function would not be.
!.S!:SA state variable. S is a variable. See State variables.
Expr : TypeAn explicit type qualification. Expr is an expression, and Type is a type (see Types). An explicit type qualification constrains the specified expression to have the specified type; these expressions are occasionally useful to resolve ambiguities that can arise from polymorphic types or overloading. Apart from that, the explicit type qualification is equivalent to Expr.
Currently we also support
Expr `with_type` Type
as an alternative syntax for explicit type qualification.
coerce(Expr)A type conversion expression. Expr is an expression. See Type conversions.
pred(Arg1::Mode1, Arg2::Mode2, …) is Det :- Goalpred(Arg1::Mode1, Arg2::Mode2, …, DCGMode0, DCGMode1) is Det --> DCGGoalfunc(Arg1::Mode1, Arg2::Mode2, …) = (Result::Mode) is Det :- Goalfunc(Arg1, Arg2, …) = (Result) is Det :- Goalfunc(Arg1, Arg2, …) = Result :- GoalA lambda expression. Arg1, Arg2, … are zero or more expressions, Result is an expression, Goal is a goal, DCGGoal is a DCG-goal, Mode1, Mode2, …, DCGMode0, and DCGMode1 are modes (see Modes), and Det is a determinism category (see Determinism). The ‘:- Goal’ part is optional; if it is not specified, then ‘:- true’ is assumed.
A lambda expression denotes a higher-order predicate or function term whose value is the predicate or function of the specified arguments determined by the specified goal. See Higher-order.
A lambda expression introduces a new scope: any variables occurring in the arguments Arg1, Arg2, … are locally quantified, i.e. they are distinct from other variables with the same name that occur outside of the lambda expression. For variables which occur in Result or Goal, but not in the arguments, the usual Mercury rules for implicit quantification apply (see Implicit quantification).
The form of lambda expression using ‘-->’ as its top level functor is a syntactic abbreviation. It is equivalent to
pred(Var1::Mode1, Var2::Mode2, …,
DCGVar0::DCGMode0, DCGVar1::DCGMode1) is Det :- Goal
where DCGVar0 and DCGVar1 are fresh variables,
and Goal is transform(DCGVar0, DCGVar1, DCGGoal)
where transform is the function
specified in Definite clause grammars.
apply(Func, Arg1, Arg2, …, ArgN)Func(Arg1, Arg2, …, ArgN)An apply expression (i.e. a higher-order function call). N >= 0, Func is an expression of type ‘func(T1, T2, …, Tn) = T’, and Arg1, Arg2, …, ArgN are expressions of types ‘T1’, ‘T2’, …, ‘Tn’. The type of the apply expression is T. It denotes the result of applying the specified function to the specified arguments. See Higher-order.
Field access expressions provide a convenient way to select or update fields of data constructors, independent of the definition of the constructor. Field access expressions are transformed into sequences of calls to field selection or update functions (see Field access functions).
A field specifier is a functor expression.
A field list is a sequence of field specifiers
separated by ^ (circumflex).
E.g., ‘field’, ‘field1 ^ field2’
and ‘field1(A) ^ field2(B, C)’
are all field lists.
If the principal functor of a field specifier is field/N,
there must be a visible selection function field/(N + 1).
If the field specifier occurs in a field update expression,
there must also be a visible update function
named 'field :='/(N + 2).
Field access expressions have one of the following forms. There are also DCG goals for field access (see Definite clause grammars), which provide similar functionality to field access expressions, except that they act on the DCG arguments of a DCG clause.
Expr ^ field_listA field selection. Expr is an expression and field_list is a field list. For each field specifier in field_list, apply the corresponding selection function in turn.
A field selection is transformed using the following rules:
transform(Expr ^ field(Arg1, …)) = field(Arg1, …, Expr).
transform(Expr ^ field(Arg1, …) ^ Rest) =
transform(field(Arg1, …, Expr) ^ Rest).
Expr ^ field_list := FieldExprA field update. Expr and FieldExpr are expressions and field_list is a field list. Returns a copy of Expr with the value of the field specified by field_list replaced with FieldExpr.
A field update is transformed using the following rules:
transform(Expr ^ field(Arg1, …) := FieldExpr) =
'field:='(Arg1, …, Expr, FieldExpr)).
transform(Expr0 ^ field(Arg1, …) ^ Rest := FieldExpr) = Expr :-
OldFieldValue = field(Arg1, …, Expr0),
NewFieldValue = transform(OldFieldValue ^ Rest := FieldExpr),
Expr = 'field :='(Arg1, …, Expr0, NewFieldValue).
Examples:
transform(Expr ^ field) = field(Expr).
transform(Expr ^ field(Arg)) = field(Arg, Expr).
transform(Expr ^ field1(Arg1) ^ field2(Arg2, Arg3)) =
field2(Arg2, Arg3, field1(Arg1, Expr)).
transform(Expr ^ field := FieldExpr) = 'field :='(Expr, FieldExpr).
transform(Expr ^ field(Arg) := FieldExpr) = 'field :='(Arg, Expr, FieldExpr).
transform(Expr0 ^ field1(Arg1) ^ field2(Arg2) := FieldExpr) = Expr :-
OldField1 = field1(Arg1, Expr0),
NewField1 = 'field2 :='(Arg2, OldField1, FieldExpr),
Expr = 'field1 :='(Arg1, Expr0, NewField1).
Clauses may use state variables as a shorthand for naming intermediate values in a sequence. For example, the following clauses
main(IO0, IO) :-
write_string("The answer is ", IO0, IO1),
write_int(42, IO1, IO2),
nl(IO3, IO).
could be written equivalently using state variable syntax as
main(!IO) :-
write_string("The answer is ", !IO),
write_int(42, !IO),
nl(!IO).
One advantage of doing this is that if in future more operations need to be added in the middle of the sequence, the state variables will not need to be renumbered.
A state variable is written ‘!.X’ or ‘!:X’,
denoting the “current” or “next” value of the sequence labelled X.
A predicate argument ‘!X’ is shorthand
for two state variable arguments ‘!.X, !:X’;
that is,
‘p(…, !X, …)’
is equivalent to
‘p(…, !.X, !:X, …)’.
The variables ‘!.X’ and ‘!:X’
are referred to as the current and next components of ‘!X’,
respectively.
Note that,
since predicate arguments of the form ‘!X’
stand for two arguments,
the arity of a predicate may be greater than it appears.
E.g. ‘p(!X)’ is a call to the predicate p/2.
State variables obey special scope rules. A state variable X must be explicitly introduced, and this can happen in one of four ways:
Only the current component of a state variable X in the enclosing scope of a lambda or if-then-else expression may be referred to (unless the enclosing X is shadowed by a more local state variable of the same name.)
For instance, the following clause employs a lambda expression and is illegal because it implicitly refers to the next component, ‘!:S’, inside the lambda expression.
p(A, B, !S) :-
P = ( pred(C::in, D::out) is det :-
q(C, D, !S)
),
( if P(A, E) then
B = E
else
B = A
).
However
p(A, B, !S) :-
P = ( pred(C::in, D::out, !.S::in, !:S::out) is det :-
q(C, D, !S)
),
( if P(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 component 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.
CallsGiven a first order call such as ‘predname(Arg1, ..., ArgN)’ or a higher-order call such as ‘Expr(Arg1, ..., ArgN)’, if any of the arguments is !X, ‘transform_goal’ replaces that argument with two arguments: !.X and !:X. It then checks whether ‘!:X’ appears in the updated Call.
substitute(Call, [!.X -> CurX, !:X -> NextX])
substitute(Call, [!.X -> CurX]), NextX = CurX
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.
The expression Expr in a higher-order call may not be of the form !X, !.X or !:X. It may be parenthesised as (!.X), however.
UnificationsIn a unification ‘ExprA = ExprB’, each of ExprA and ExprB are expressions that may have one of the following four forms:
Note that ExprA and ExprB may not have the form !S.
State variable field updatesA state variable field update goal has the form
!S ^ field_list := Expr
where field_list is a valid field list See Field access expressions. This means that
!S ^ field1 := Expr !S ^ field1 ^ field2 := Expr !S ^ field1 ^ field2 ^ field3 := Expr
are all valid field update goals. If S is X, ‘transform_goal’ replaces such goals with
NextX = CurX ^ field_list := Expr
Otherwise, it leaves the goal unchanged.
ConjunctionsGiven a nonempty conjunction, whether a sequential conjunction such as Goal1, Goal2 or a parallel conjunction such as Goal1 & Goal2, ‘transform_goal’
substitute(Goal1, [!.X -> CurX, !:X -> MidX])
substitute(Goal2, [!.X -> MidX, !:X -> NextX])
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
DisjunctionsGiven a disjunction such as Goal1 ; Goal2, ‘transform_goal’
substitute(Goal1, [!.X -> CurX, !:X -> NextX])
substitute(Goal2, [!.X -> CurX, !:X -> NextX])
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.
NegationsGiven a negated goal of the form ‘not NegatedGoal’, ‘transform_goal’
‘not’ substitute(‘NegatedGoal’, [!.X -> CurX, !:X -> DummyX]), NextX = CurX
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-elsesGiven an if-then-else, whether it uses ( if Cond then Then else Else ) syntax or ( Cond -> Then ; Else ) syntax, ‘transform_goal’
substitute(Cond, [!.X -> CurX, !:X -> MidX])
substitute(Then, [!.X -> MidX, !:X -> NextX])
substitute(Else, [!.X -> CurX, !:X -> NextX])
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 quantificationsIn 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.)
substitute(SubGoal, [!.X -> CurX, !:X -> NextX])
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.
main(!IO) :-
io.write_string("The 100th prime is ", !IO),
X = prime(100),
io.write_int(X, !IO),
io.nl(!IO).
foldl2(_, [], !A, !B).
foldl2(P, [X | Xs], !A, !B) :-
P(X, !A, !B),
foldl2(P, Xs, !A, !B).
iterate_while2(Test, Update, !A, !B) :-
( if Test(!.A, !.B) then
Update(!A, !B),
iterate_while2(Test, Update, !A, !B)
else
true
).
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)
).
There are three sorts of variables in Mercury: ordinary variables, type variables, and inst variables.
Variables occurring in types, type classes, and instances are called type variables. Variables occurring in insts or modes are called inst variables. Variables that occur in expressions, and that are not inst variables or type variables, are called ordinary variables.
Note that type variables can occur in expressions in the right-hand (Type) operand of an explicit type qualification. Inst variables can occur in expressions in the right-hand (Mode) operand of an explicit mode qualification. Apart from that, all other variables in expressions are ordinary variables.
The three different variable sorts occupy different namespaces: there is no semantic relationship between two variables of different sorts (e.g. a type variable and an ordinary variable) even if they happen to share the same name. However, as a matter of programming style, it is generally a bad idea to use the same name for variables of different sorts in the same clause.
The scope of ordinary variables is the clause or declaration in which they occur, unless they are quantified, either explicitly (see Goals) or implicitly (see Implicit quantification).
The scope of type variables in a predicate or function’s type declaration extends over any explicit type qualifications (see Expressions) in the clauses for that predicate or function, and over ‘pragma type_spec’ (see Type specialization) declarations for that predicate or function, so that explicit type qualifications and ‘pragma type_spec’ declarations can refer to those type variables. The scope of any type variables in an explicit type qualification which do not occur in the predicate or function’s type declaration is the clause in which they occur.
The scope of inst variables is the clause or declaration in which they occur.
The rule for implicit quantification in Mercury is not the same as the usual one in mathematical logic. In Mercury, variables that do not occur in the head term of a clause are implicitly existentially quantified around their closest enclosing scope (in a sense to be made precise in the following paragraphs). This allows most existential quantifiers to be omitted, and leads to more concise code.
An occurrence of a variable is in a negated context if it is in a negation, in a universal quantification, in the condition of an if-then-else, in an inequality, or in a lambda expression.
Two goals are parallel if they are different disjuncts of the same disjunction, or if one is the “else” part of an if-then-else and the other goal is either the “then” part or the condition of the if-then-else, or if they are the goals of disjoint (distinct and non-overlapping) lambda expressions.
If a variable occurs in a negated context and does not occur outside of that negated context other than in parallel goals (and in the case of a variable in the condition of an if-then-else, other than in the “then” part of the if-then-else), then that variable is implicitly existentially quantified inside the negated context.
The treatment of inequality, universal quantification, implication, and logical equivalence as abbreviations can cause the introduction of double negations which could make otherwise well-formed code mode-incorrect. To avoid this problem, the language specifies that after syntax analysis and implicit quantification, and before mode analysis is performed, the implementation must delete any double negations and must replace any negations of conjunctions of negations with disjunctions. (Both of these transformations preserve the logical meaning and type-correctness of the code, and they preserve or improve mode-correctness: they never transform code fragments that would be well-moded into ones that would be ill-moded. See Modes.)
A definite clause grammar (DCG) is a way of expressing parsing rules, and is intended for writing parsers and sequence generators. In the past it has also been used to thread an implicit state variable, typically the I/O state, through code. We now recommend that DCGs only be used for writing parsers and sequence generators, and that state variable syntax (see State variables), which performs a similar transformation but is more flexible, be used for other purposes such as threading state variables.
A DCG-rule is a clause that takes the form
DCG_Head --> DCG_Body.
where DCG_Head is a predicate head term and DCG_Body is a DCG-goal. It is an abbreviation for the rule
Head --> Body.
where Head is DCG_Head
with two fresh variables,
V_in and V_out,
appended to the argument list,
and Body is transform(V_in, V_out, DCG_Body),
where transform is the function defined below.
A DCG-goal is a term of one of the following forms:
some Vars DCG-goalA DCG existential quantification. Vars is a list of variables and DCG-goal is a DCG-goal.
all Vars DCG-goalA DCG universal quantification. Vars is a list of variables and DCG-goal is a DCG-goal.
DCG-goal1, DCG-goal2A DCG sequence. DCG-goal1 and DCG-goal2 are DCG-goals. Intuitively, this means “parse DCG-goal1 and then parse DCG-goal2” or “do DCG-goal1 and then do DCG-goal2”. (Note that the only way this construct actually forces the desired sequencing is by the modes of the implicit DCG arguments.)
DCG-goal1 ; DCG-goal2A disjunction. DCG-goal1 and DCG-goal2 are DCG-goals. DCG-goal1 must not be of the form ‘DCG-goal1a -> DCG-goal1b’. (If it is, then the goal is an if-then-else, not a disjunction.)
{ Goal }A brace-enclosed ordinary goal. Goal is a goal.
[Expr, …]A DCG input match. Expr is an expression. Unifies the implicit DCG input variable V_in, which must have type ‘list(_)’, with a list whose initial elements are the expressions specified and whose tail is the implicit DCG output variable V_out.
[]The null DCG goal (an empty DCG input match). Equivalent to ‘{ true }’.
not DCG-goal\+ DCG-goalA DCG negation. DCG-goal is a DCG-goal. The two different syntaxes have identical semantics.
if CondGoal then ThenGoal else ElseGoalCondGoal -> ThenGoal ; ElseGoalA DCG if-then-else. The two different syntaxes have identical semantics. CondGoal, ThenGoal, and ElseGoal are DCG-goals.
=(Expr)A DCG unification. Expr is an expression. Unifies Expr with the implicit DCG argument.
:=(Expr)A DCG output unification. Expr is an expression. Unifies Expr with the implicit DCG output argument, ignoring the input DCG argument.
Expr =^ field_listA DCG field selection. Expr is an expression and field_list is a field list. Unifies Expr with the result of applying the field selection field_list to the implicit DCG argument. See Field access expressions.
^ field_list := ExprA DCG field update. Expr is an expression and field_list is a field list. Replaces a field in the implicit DCG argument. See Field access expressions.
DCG-callA term which does not match any of the above forms is a DCG predicate call. If DCG-call is a variable Var, it is treated as if it were ‘call(Var)’. Then, the two implicit DCG arguments are appended to the specified arguments.
The semantics is given by the following function, where each occurrence of V_new is a fresh variable.
transform(V_in, V_out, some Vars DCG_goal) =
some Vars transform(V_in, V_out, DCG_goal)
transform(V_in, V_out, all Vars DCG_goal) =
all Vars transform(V_in, V_out, DCG_goal)
transform(V_in, V_out, (DCG-goal1, DCG-goal2)) =
(transform(V_in, V_new, DCG_goal1), transform(V_new, V_out, DCG_goal2))
transform(V_in, V_out, (DCG_goal1 ; DCG_goal2)) =
( transform(V_in, V_out, DCG_goal1)
; transform(V_in, V_out, DCG_goal2)
)
transform(V_in, V_out, { Goal }) = (Goal, V_out = V_in)
transform(V_in, V_out, [Expr, …]) = (V_in = [Expr, … | V_Out])
transform(V_in, V_out, []) = (V_out = V_in)
transform(V_in, V_out, not DCG_goal) =
(not transform(V_in, V_new, DCG_goal), V_out = V_in)
transform(V_in, V_out, if CondGoal then ThenGoal else ElseGoal) =
( if transform(V_in, V_new, CondGoal) then
transform(V_new, V_out, ThenGoal)
else
transform(V_in, V_out, ElseGoal)
)
transform(V_in, V_out, =(Expr)) = (Expr = V_in, V_out = V_in)
transform(V_in, V_out, :=(Expr)) = (V_out = Expr)
transform(V_in, V_out, Expr =^ field_list) =
(Expr = V_in ^ field_list, V_out = V_in)
transform(V_in, V_out, ^ field_list := Expr) =
(V_out = V_in ^ field_list := Expr)
transform(V_in, V_out, p(A1, …, AN)) =
p(A1, …, AN, V_in, V_out)
Previous: Elimination of double negation, Up: Clauses [Contents]