%=========================================
% A  Better Meta-interpreter
%
%    Many improvement are possible for enhancing
%          proof explanations, 
%          interactivity,
%          support for Prolog features, like or and cut.
%=========================================
solve(Goal) :-
   solve(Goal,system,P,R),
   printProof(P),nl,
   writeseqnl(['****',Goal,R]).

%------------------------------------
% The Goal true is true.
%------------------------------------
solve(true,FactBase,[],true) :-  !.

%-----------------------------------
% Negated Goal, Goal is not a Fact.
%       Negation as failure for a Rule Head
%-----------------------------------
solve(not(A),FactBase,Proof,true) :-
   not(fact(A)),
   solve(A,FactBase,Proof,unk),!.

solve(not(A),FactBase,Proof,false) :-
   not(fact(A)),!,
   solve(A,FactBase,Proof,Result).

%------------------------------------
% Goal is a conjunct.
%
% The conjuncts of a conjuctive goal
%    are solved sequentially and the results
%    are merged.
%------------------------------------
solve((A,B),FactBase,Proof,Result) :-
      !, solve(A,FactBase,ProofA,ResultA),
      ( ResultA = true
            ->  (solve(B,FactBase,ProofB,ResultB),
                   mergeResults(ResultA,ResultB,Result),
                   append(ProofA,ProofB,Proof))
            ;    (Proof = ProofA,
                   Result = ResultA)).

%------------------------------------
% The Goal is a system (non-dynamic) Predicate
%    NB: sysPred will succeed for a conjunct.
%------------------------------------
solve(G,FactBase,Proof,Result) :-  
    syspred(G),!,
    (\+(G) 
          -> (Result = unk, Proof=[(`cant prove`,G)] )
          ;  (G, Result = true, Proof = [G])).

%------------------------------------------
% If a goal is a fact its truth-value is
%    is determined in the factbase.
%------------------------------------------

%-----------------------------------
% Negation as failure for a Fact.
%-----------------------------------
solve(not(A),FactBase,[(A,`is unknown`)],true) :-
   fact(A),
   factUnk(A,FactBase),!.

solve(not(A),FactBase,Proof,false) :-
   fact(A),!,
   solve(A,FactBase,Proof,Result).

%-----------------------------------
%-----------------------------------
solve(A,FactBase,[A],true) :-
  fact(A),
  factTrue(A,FactBase).

solve(A,FactBase,[(A,is,unknown)],unk) :-
   fact(A),
   factUnk(A,FactBase),!.

solve(A,FactBase,[(A,`cant be true because`,Proof)],false) :-
       fact(A),
       factFalse(A,FactBase,Proof),!.


%---------------------------------------------
% If a goal is not a fact, it is a rule head.
%    "solve" is recursively called.
%---------------------------------------------

solve(A,FactBase,[(A,implies) | Proof],Result) :-
   \+(fact(A)),
   clause(A,Body),
   solve(Body,FactBase,Proof,Result).


%----------------------------------------------------------
%
% Check a Fact "truth value" in an Agents belief space
%
%  NB:  "Negfact" might have a derivation.
%----------------------------------------------------------
factTrue(Fact,Agent) :-
          belief(Agent,Fact).

factFalse(Fact,Agent,Proof) :-
    negate(Fact,NegFact),
    solve(NegFact,Agent,Proof,true).

factUnk(Fact,Agent) :-
       \+(belief(Agent,Fact)),
        negate(Fact,NegFact),
       \+(solve(NegFact,Agent,Proof,true)).