Metadata-aware rule processing and rule traceability in Prova

The old Prova version had an interesting but somewhat patchy approach to run-time processing of the rule metadata. The new rewrite is aiming to improve on this. The first question is what to annotate with metadata? It is clear that all Prova clauses (rules and facts) should be allowed to carry metadata. As you'll see below, I also annotate body literals so that whenever unification occurs, it uses metadata matching if metadata is present on the body literal.

The examples below are taken from a new test rules/reloaded/label.prova. This is the way metadata is added to rules:

@label(rule1) r1(X):-q(X).
@label(rule2) r2(X):-q(X).
@label(rule3) r2(X):-q(X).

Metadata is a set of annotations each of which is a pair defined as: @key(value /,value/*). Both keys and values are arbitrary strings defined by their occurrence in an annotation. All rules in a rulebase consulted from a file automatically have a special annotation @src(FILENAME). Apart from that, all other rule annotations are defined by the user. There could be more than one user-defined annotation associated with a single rule. There is no requirement for annotations to be on the same line as the rule head.

So far so good. Now there wouldn't be any real use for this if we couldn't somehow take this metadata into account when the rulebase is executed. To achieve that, the body literals in a rule can be optionally annotated as well. Here is an example that returns 3 solutions (1,2,3):

p1(X):-
	@label(rule1)
	r1(X).
q(1).
q(2).
q(3).

:-solve(p1(X2)).

The annotations on literals (as opposed to rules) are a set of constraints on the target rules during unification. For each literal annotation, there must be at least one match between a value listed for that annotation and a value listed for the same key in the target rule. This is a more complex example that also has three solutions (1,2,3):

% succeeds since scope is EITHER "rule2" OR "rule1"
p2a(X):-
	@label(rule2,rule1)
	r1(X). 
:-solve(p2a(X4)).

Imagine now that we do not know what are the target annotation values and would like to discover and possibly trace the annotations for target rules matching a literal. How about trying to use a variable instead of a constant value in a literal annotation? The following returns 6 solutions where Label6 takes values 'rule2' and 'rule3' 3 times each.

p4(X,Y):-
	@label(Y)
	r2(X).
:-solve(p4(X6,Label6)).

Observe that if a match is found, execution continues for r2(X) as though the @label annotation was not present.

Now since we have variables in literal annotations, we can also pre-assign values to these variables dynamically. The following code sets the annotation value at run-time to 'rule2' so that only 3 solutions for X7 are returned (1,2,3).

% dynamically set the metadata value expected from matching rules
:-solve(p4(X7,rule2)).

Finally, we can also find the rulebase of the target clause in a unification. The final example shows how we can constrain one annotation (@label) while enquiring on the value of another (@src). In this way, any match can be traced from the source rulebase of the target clause. This returns 3 solutions with Src9 set to the filename of the rulebase in each solution.

% get module label
p6(X,Y):-
	@src(Y) @label(rule3)
	r2(X).
:-solve(p6(X9,Src9)).