% mpj.pl - A simple meta interpreter with "justifications"

:- op(1150,xfy,'if'),
   op(1150,xfy,'since'),
   op(1100,xfy,'or'),
   op(1000,xfy,'and'),
   op(900,fy,'~').
:- dynamic if/2.

% this prints the justification.
demo(P) :- demo(P,J), ppj(J).

% true and false.
demo(true,true) :- !.
demo(false,nil) :- !,fail.

% conjunction
demo((P and Q),(Pj and Qj)) :- 
  !,
  demo(P,Pj),
  demo(Q,Qj).

% disjunction
demo((P or _),Pj) :- demo(P,Pj).
demo((_ or Q),Qj) :- !,demo(Q,Qj).

% negation 
demo((~P),_) :- demo(P,_),!,fail.
demo((~P),(~P)) :- !.

% apply a rule
demo(P,(P since (Rule and Qj))) :- 
  mostGeneralTerm(P,Pg),
  (Pg if Q),
  copy_term((Pg if Q),Rule),
  Pg=P,
  demo(Q,Qj).

% fall through to prolog
demo(P,prolog(P)) :- 
  builtin(P),
  !,
  call(P).

% succeeds if P is a builtin predicate (i.e., there
% are no pclause rules for P).
builtin(P) :- 
  functor(P,Predicate,Arity),
  functor(P2,Predicate,Arity),
  \+((P2 if _)).

% pretty writes a justification structure.
ppj(J) :- ppj1(J,0).

ppj1((P since (P if true) and true),In) :- 
  !,
  format("~n~*c~p is a fact",[In,32,P]).

ppj1((P since Q),In) :- 
  !,
  format("~n~*c~p since ",[In,32,P]),
  In2 is In+5,
  ppj1(Q,In2).

ppj1((P and Q),In) :-  !,  ppj1(P,In),  ppj1(Q,In).

ppj1(P,In) :- format("~n~*c~p",[In,32,P]).


%% mostGeneralTerm(+Term,-MGTerm)
%% MGTerm is the most general term that unifies with Term.

mostGeneralTerm(T,Tg) :-
  functor(T,Pred,Arity),
  functor(Tg,Pred,Arity).