% This examples demonstrate the use the inductive logic programming predicates
% which are used in test coverage measurement or for learning resp. meta inference

:-eval(consult('ContractLog/list.prova')).	
:-eval(consult('ContractLog/utils.prova')).
:-eval(consult('ContractLog/math.prova')).
:-eval(consult('ContractLog/testcase.prova')).

%----------------
% substitution
%----------------

% two substitutions
:-solve(substitution(f(g(A),B),f(g(h(a)),i(b)),Subst)).

% minimalize
:-solve(substitution(f(g(A),A),f(g(h(a)),h(a)),Subst)).

%Typed
:-solve(substitution(f(g(java.lang.Integer.A)),f(g(1)),Subst)).

% no substitution
:-solve(substitution(f(g(j(A))),f(g(h(a))),Subst)).

% variable substitution
:-solve(substitution(f(g(X)),f(g(Y)),Subst)).

% variable constant substitution
:-solve(substitution(f(X),f(a),Subst)).

% constant constant substitution -> fails
:-solve(substitution(f(b),f(a),Subst)).

% complex substitutions
:-solve(substitution(f("XXX",g(A),B),f("XXX",g(h(a)),i(b)),Subst)).

%----------------
% specialization
%----------------

% substitute a variable
:-solve(substitute(p(X),Instance,[[X,h(a)]])).

% substitute a complex term
:-solve(substitute(f(g(A),A),Instance,[[A,["h","a"]],[B,["h","b"]]])).

% substitute with constant
:-solve(substitute(f(X),Instance,[[X,["a"]]])).

% substitute a clause p(X):-q(X) with X/h(a)
:-solve(substitute([p(X),q(X)],Instance,[[X,h(a)]])).

% substitute a clause p(X):-q(h(a)) with X/h(a)
:-solve(substitute([p(X),q(h(a))],Instance,[[X,h(a)]])).

% unify a goal with a clause and compute the specialized instance (top level instance)
:-solve(specializations([p(a),p(b)],[p(X),q(X)],Instances)).

% unify a goal with a clause and compute the specialized instance (top level instance)
:-solve(specializations([p(a),q(c),p(b),p(f(a))],[p(X),q(X)],Instances)).

% do not specialize facts
:-solve(specializations([p(a),q(c),p(b),p(f(a))],[["p","a"]],Instances)).

% specialize a LP (set of clauses) with a goal and compute the specialized
% LP consisting of the top level instances
:-solve(specialize([p(a),p(b)],[[p(X),q(X)]],Top_Level_Instances)).

% a more complex example with two rules and 4 subgoals and 2 facts
:-solve(specialize([p(a),p(b),q(a),q(b)],[[p(X),q(X)],[q(Y),r(Y)],[p(a)],[p(b)]],Top_Level_Instances)).

%--------------------------------
% least general generalization
%--------------------------------

% the lgg of two identical terms is the term itself
:-solve(lgg(f(X),f(X),LGG)).

% lgg(f(a1, .., an)), f(b1, ..bn)) = f(lgg(a1, b1), .., lgg(an, bn)):
:-solve(lgg(f(a1,a2,a3),f(b1,b2,b3),LGG)).

% lgg(p(s1, .., sm), q(t1, ..tn)) is undefined if p != q
:-solve(lgg(f(a1, an), g(b1, bn), LGG)).

%lgg(parent(uwe, adrian), parent(hariet, adrian)) = parent(X, adrian)
:-solve(lgg(parent(uwe, adrian), parent(hariet, adrian),LGG)).

%lgg = f(X, g(Y,Z), c).
:-solve(lgg(f(a, g(b, h(X)), c), f(d, g(j(X), a), c),LGG)).

:-solve(lgg(f(g(3),3,j(6)),f(g(2),2,j(h(6))),LGG)).


% lgg of two clauses; lgg = p(X) :- q(X)
:-solve(lgg([p(a),q(a)],[p(b),q(b)],LGG)).

% lgg of two clauses with unequal body atoms is undefined
:-solve(lgg([p(a),q(a),r(a)],[p(b),q(b)],LGG)).


%--------------------------------
% generalize a LP (set of clauses)
%--------------------------------

:-solve(generalize([
		[p(a),q(a)],
		[p(a),q(a),r(a)],
		[p(b),q(b)],
		[p(c),q(c)],
		[r(a)],[q(a)],[q(b)],[q(c)]],
	Generalization)).


% test different variants / no variants
:-solve(variant(X,Y)).
:-solve(variant(p(X),p(Y))).
:-solve(variant([p(X),q(X)],[p(a),q(a)])).
:-solve(variant([p(X),q(X)],[p(Y),q(Y)])).
:-solve(variant([p(a)],[p(X),q(X)])).
:-solve(variant([[p(X),q(X)]],[[p(Y),q(Y)]])).



%--------------------------------
% coverage / cover
%--------------------------------

:-solve(coverage(
	[p(a),p(b)], % goal with two subgoal
	[ 				
		[p(X),q(X)], % LP with one rule and two facts
		[r(X),z()],
		[q(a)],
		[q(b)]
	],
	CoveredClauses,
	NotCoveredClauses,
	CoverageLevel)).

%--------------------------------------------------
% Derive Meta LP from KB and partial KB (module)
%--------------------------------------------------


% create meta LP
p(LP):-	metaLP(LP).
%:-solve(p(LP)).

% query metaLP
%:-solve(metaLP(LP)).

% return all clauses in meta LP
all(X,Y) :- metaLP(LP), member(X,LP), type(X,Type), println([Type]), member(Y,X), println([Y]).
%:-solve(all(X,Member)).

% create partial meta LP with module OID
q(LP):-partial(metaLP(LP),"ContractLog/list.prova").
%:-solve(q(LP)).

