Prova Developers Blog

The new update implements Prova guards on literals. Let's start with an example. Imagine that during unification, the target rule matches the source literal but we do not want to proceed with further evaluation unless a "guard" condition evaluates to true. The guards are specified in a syntax that is similar to the one used in Erlang (using brackets instead of the 'when' keyword) but the semantics are more appropriate for a rule language like Prova. See rules/reloaded/guard.prova and ProvaMetadataTest.java.

@author(dev1) r1(X):-q(X).
@author(dev22) r2(X):-q(X).
@author(dev32) r2(X):-s(X).

q(2).

s(-2).

trusted(dev1).
trusted(dev22).

% Author dev22 is trusted but dev32 is not, so one solution is found: X1=2  
p1(X):-
	@author(A)
	r2(X) [trusted(A)].
:-solve(p1(X1)).

This example uses metadata annotations on rules for predicates r1 and r2 and on the literal r2(X) in the body of the rule for p1(X) (see the previous post here for details on metadata handling, http://prova.ws/csp/node/18). Since variable A in @author(A) is initially free, it gets instantiated from the matching target rule(s). Once A is instantiated to the target rule's @author annotation's value ('dev22', for the first r2 rule), the body of the target rule is dynamically non-destructively modified to include all the literals in the guard [trusted(A)] before the body start, after which the processing continues. Since trusted(dev22) is true but trusted(dev32) is not, only the first rule for predicate r2 is used and so one solution X1=2 is returned by solve(p1(X1)).

Guards can include arbitrary lists of Prova literals including Java calls, arithmetic expressions, relations, and even CUT. The next example shows how CUT can be used in the literal guard.

a(X):-qq(X).
a(X):-s(X).

s(-2).

% This example shows how guards can be used to implement a "dynamic CUT".
% The CUT in the guard is dynamically spliced into the start of the target rule body.
% As qq(X) has no solutions, the CUT prevents further backtracking to the second rule for a(X):-s(X),
%    that would have yielded a solution but does not due to that dynamic CUT.
p2(X):-
	a(X) [!].
:-solve(p2(X2)).

If the CUT was included as part of the p2(X) rule after a(X) like in the following version, the a(X) rule including qq(X) would have failed but the second rule would have provided one solution: -2.

p2(X):-
	a(X),!.