Previous: Implementing solver types, Up: Solver types [Contents]

Mercury’s negation and if-then-else goals
(and hence also inequalities and universal quantifications)
are implemented using *negation as failure*,
meaning that the failure to find a proof of one statement is regarded as a
proof of its negation.
Negation as failure is sound provided that no non-local variable
becomes further bound during the execution of a goal which may be negated.
This includes negated goals themselves, as well as the conditions of
if-then-elses, which are negated iff they fail without producing any solution,
and the bodies of pred or func expressions, which may be called or applied
in one of the other contexts, or indeed in another pred or func expression.

Mercury checks that any solver variables that are used in the above contexts
are used in such a way that negation as failure remains sound.
In the case of negation and if-then-else goals,
if any non-local solver type variable or higher-order variable
with inst `any`

is used in a negated context,
the goal must be placed inside a `promise_pure`

, `promise_semipure`

,
or `promise_impure`

scope.
The first two promises assert that (among other things)
no solver variable becomes further bound in the negated context.
The third promise makes the weaker assertion that the goal satisfies
the requirements of all impure goals (namely, that it doesn’t interfere
with the semantics of other pure goals).

In the case of pred and func expressions, Mercury allows three possibilities.
The higher-order value may be considered `ground`

, which means that
all non-local variables used in the body of the expression
(including those with other higher-order values) must themselves be ground.
Higher-order values that are ground can be safely called or applied
in any context, including negated contexts, since none of their (ground)
non-local variables can become further bound by doing so.
Alternatively, the higher-order value may be considered to have inst
`any`

, which allows non-local variables used in the body of the
expression to have inst `any`

.
Calling or applying these values *may* further bind non-local variables,
so if this occurs in a negated context then,
as in the case of solver variables, a promise will be required around the
negation or if-then-else.

Pred and func expressions with inst `any`

are written using
`any_pred`

and `any_func`

in place of `pred`

and `func`

,
respectively.

The third possibility is that the higher-order value can be given an impure type (see Higher-order impurity).

Previous: Implementing solver types, Up: Solver types [Contents]