% METABAYES VERSION 1.0
% MAP version is essentially the same as before. Iterative deepening until find one. This one 

% METABAYES VERSION 0.0
%
% Regular sampling of derivation based on generalised meta-interpreter.
%	Regular sampling works by maintaining a counter which is used
%	to direct sampling from the derivation space. Considering
% 	a counter Cnt as a variable base number we use the digits to select
% 	choices at every step in the proof.
% Termination of the enumerataion of hypotheses is achieved by keeping
% 	a tally of Sum Probability of hypotheses so far and
% 	terminate when Sum = 1. It is sufficient to assume uniform
% 	probability choices, though a similar approach should work
% 	for non-uniform (ie SLP).
% Generalised form of meta-interpreter which supports tabulated
%	Metarules and background knowledge as MetaSubstitution.

% proveMAP(Pos,Neg,[],Prog2,KBound,KBoundRemaining),


% Prover for Meta-interptretive SLP

proveMAP([],_,Prog,Prog,KBound,KBound).
proveMAP([Atom|As],Neg,Prog1,Prog2,KBound1,KBound2) :-
	d_prove([Atom],Prog1), !,	% Atom already proveable
	proveMAP(As,Neg,Prog1,Prog2,KBound1,KBound2).
proveMAP([Atom|As],Neg,Prog1,Prog2,KBound1,KBound2) :-
		% Atom is a list of Constant/Variables
		% Program is list of RuleName/MetaSubstitution pairs
    metarule(RuleName,MetaSub,(Atom :- Body),OrderTest),
    OrderTest,  % you have included cut '!' in the second clause of proveMAP,therefore
    abduceMAP(metasub(RuleName,MetaSub),Prog1,Prog3,KBound1,KBound3,Neg),
	proveMAP(Body,Neg,Prog3,Prog4,KBound3,KBound4), 
	proveMAP(As,Neg,Prog4,Prog2,KBound4,KBound2).

exist(metasub(RuleName,MetaSub),_):-
    metasub(RuleName,MetaSub),!.
exist(MetaClause,Prog):-
    element(MetaClause,Prog). 

abduceMAP(MetaClause,Prog,Prog,KBound,KBound,Neg) :-
    exist(MetaClause,Prog), !.
abduceMAP(MetaClause,Prog,[MetaClause|Prog],s(KBound),KBound,Neg):-
    \+break_constraint(MetaClause,Prog),
    consistent(Neg,[MetaClause|Prog]).



% Deductive prover
/* Slower d_prove 
d_prove([],Prog).
d_prove([Atom|As],Prog) :-
% Atom is a list of Constant/Variables
% Program is list of RuleName/MetaSubstitution pairs
    metarule(RuleName,MetaSub,(Atom :- Body),OrderTest), OrderTest,
    exist(metasub(RuleName,MetaSub),Prog), % OrderTest has grounded, therefore it is safe to use exist_with_cut
    d_prove(Body,Prog),
    d_prove(As,Prog).
*/

% the only difference from d_prove is: not to include OrderTest--speed up the proof. 
d_prove([],Prog).
d_prove([Atom|As],Prog) :-
			% Atom is a list of Constant/Variables
			% Program is list of RuleName/MetaSubstitution pairs
    metarule(RuleName,MetaSub,(Atom :- Body),OrderTest),
	exist_slower(metasub(RuleName,MetaSub),Prog), %considering that it is grounded, then it is safe to call just once. 
	d_prove(Body,Prog),
	d_prove(As,Prog).

% similar to exist, but does not include cut, because the query is unbound, therefore allow backtracking, fore example, a parent have multiple childen
exist_slower(metasub(RuleName,MetaSub),_) :-
    metasub(RuleName,MetaSub).  %Call =.. [RuleName|MetaSub], Call, !.
exist_slower(metasub(RuleName,MetaSub),Prog) :-
    element(metasub(RuleName,MetaSub),Prog).