2.11 Goals

A goal is a term of one of the following forms.

some Vars Goal

An existential quantification. Goal must be a valid goal. Vars must be a list whose elements are either variables or state variables. (A single list may contain both.) The case where they are state variables is described in State variables; here we discuss the case where they are 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 Goal

A universal quantification. Goal must be a valid goal. Vars must be a list of variables (they may not be state variables). This goal is an abbreviation for ‘not (some Vars not Goal)’.

Goal1, Goal2

A conjunction. Goal1 and Goal2 must be valid goals.

Goal1 & Goal2

A parallel conjunction. This has the same declarative semantics as the 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 ; Goal2

where Goal1 is not of the form ‘Goal1a -> Goal1b’: a disjunction. Goal1 and Goal2 must be valid goals.

true

The empty conjunction. Always succeeds.

fail

The empty disjunction. Always fails.

not Goal

\+ Goal

A negation. The two different syntaxes have identical semantics. Goal must be a valid goal. Both forms are equivalent to ‘if Goal then fail else true’.

Goal1 => Goal2

An implication. This is an abbreviation for ‘not (Goal1, not Goal2)’.

Goal1 <= Goal2

A reverse implication. This is an abbreviation for ‘not (Goal2, not Goal1)’.

Goal1 <=> Goal2

A logical equivalence. This is an abbreviation for ‘(Goal1 => Goal2), (Goal1 <= Goal2’).

if CondGoal then ThenGoal else ElseGoal

CondGoal -> ThenGoal ; ElseGoal

An if-then-else. The two different syntaxes have identical semantics. CondGoal, ThenGoal, and ElseGoal must be valid 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 are 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, it executes the ElseGoal. Note that CondGoal can be nondeterministic — unlike Prolog, Mercury’s if-then-else does not commit to the first solution of the condition if the condition succeeds.

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

Term1 = Term2

A unification. Term1 and Term2 must be valid data-terms.

Term1 \= Term2

An inequality. Term1 and Term2 must be valid data-terms. This is an abbreviation for ‘not (Term1 = Term2)’.

call(Closure)

call(Closure1, Arg1)

call(Closure2, Arg1, Arg2)

call(Closure3, Arg1, Arg2, Arg3)

…

A higher-order predicate call. The closure and arguments must be valid data-terms. ‘call(Closure)’ just calls the specified closure. The other forms append the specified arguments onto the argument list of the closure before calling it. See Higher-order.

Var

Var(Arg1)

Var(Arg2)

Var(Arg2, Arg3)

…

A higher-order predicate call. Var must be a variable. The semantics are exactly the same as for the corresponding higher-order call using the call/N syntax, i.e. ‘call(Var)’, ‘call(Var, Arg1)’, etc.

promise_pure Goal

A purity cast. Goal must be a valid goal. This goal promises that Goal implements a pure interface, even though it may include impure and semipure components.

promise_semipure Goal

A purity cast. Goal must be a valid goal. This goal promises that Goal implements a semipure interface, even though it may include impure components.

promise_impure Goal

A purity cast. Goal must be a valid goal. This goal instructs the compiler to treat Goal as though it were impure, regardless of its actual purity.

promise_equivalent_solutions Vars Goal

A determinism cast. Vars must be a list of variables. Goal must be a valid 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 Goal

A 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 valid 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.

Goals of the form arbitrary ArbVars ArbGoal are not allowed to occur outside promise_equivalent_solution_sets Vars Goal goals.

require_det Goal

require_semidet Goal

require_multi Goal

require_nondet Goal

require_cc_multi Goal

require_cc_nondet Goal

require_erroneous Goal

require_failure Goal

A determinism check, typically used to enhance the robustness of code. Goal must be a valid 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] Goal

A switch completeness check, typically used to enhance the robustness of code. 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] Goal

require_switch_arms_semidet [Var] Goal

require_switch_arms_multi [Var] Goal

require_switch_arms_nondet [Var] Goal

require_switch_arms_cc_multi [Var] Goal

require_switch_arms_cc_nondet [Var] Goal

require_switch_arms_erroneous [Var] Goal

require_switch_arms_failure [Var] Goal

require_switch_arms_det is a determinism check, typically used to enhance the robustness of code. Goal must be a valid 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 [Warning] Goal

disable_warning [Warning] Goal

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 [Warning] 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 [Warning].

At the moment, the Mercury compiler supports the disabling of the following warning categories:

singleton_vars

Disable the generation of singleton variable warnings.

suspected_occurs_check_failure

Disable the generation of warnings about code that looks like it unifies a variable with a term that contains that same variable.

suspicious_recursion

Disable the generation of warnings about suspicious recursive calls.

no_solution_disjunct

Disable the generation of warnings about disjuncts that can have no solution. This is usually done to shut up such a warning 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.)

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 disabled warning category.

trace Params Goal

A trace goal, typically used for debugging or logging. Goal must be a valid goal; Params must be a valid 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 affect 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.

try Params Goal … catch Term -> 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 Term -> CatchGoal
    …
    catch_any CatchAnyVar -> CatchAnyGoal

See Exception handling for the full details.

event Goal

An event goal. Goal must be 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.

Call

Any goal which does not match any of the above forms must be a predicate call. The top-level functor of the term determines the predicate called; the predicate must be declared in a pred declaration in the module or in the interface of an imported module. The arguments must be valid data-terms.