% mpe.pl - A simple meta interpreter with "unification with equality".

:- op(1150,xfy,'if'),
   op(1100,xfy,'or'),
   op(1000,xfy,'and'),
   op(900,fy,'~').
:- op(700,xfx,'<=>').
:- op(700,xfx,'=>').

:- dynamic if/2.

% true succeeds.
demo(true) :- !.

% false fails.
demo(false) :- !,fail.

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

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

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

% apply a rule
demo(P) :- 
  (Head if Body),
  eu(Head,P),
  demo(Body).

% fall through to prolog
demo(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 _)).


%% eu = unify with equality

% first try unifying w/o rewriting either term
eu(T1,T2) :- u(T1,T2).

% now try rewriting the 1st term
eu(T1,T2) :- rewrite(T1,X), eu(X,T2).

% now try rewriting the 2nd term
eu(T1,T2) :- rewrite(T2,X), eu(T1,X).

% if a term is atomic, try primitive unification.
u(T1,T2) :- atm(T1),atm(T2),T1=T2.

% recurse on the components of the term.
u(T1,T2) :- 
  split(T1,P,Args1),
  split(T2,P,Args2),
  uList(Args1,Args2).

% uList(L1,L2) iff list L1 unifies with list L2.
uList([],[]).
uList([Head1|Tail1],[Head2|Tail2]) :-
  eu(Head1,Head2),
  uList(Tail1,Tail2).

% split compound term T into its Predicate and arguments.
split(T,Pred,Args) :- nonvar(T), \+(atomic(T)), T=..[Pred|Args].

% atm(X) iff X is a variable or an atomic term.
atm(X) :- var(X);atomic(X).

% rewrite(A,B) if A can be rewritten as B.            
rewrite(X,Y) :- rewrite1(X,Y,[X]).

rewrite1(X,Y,L) :- X=>Y, notIn(Y,L).
rewrite1(X,Y,L) :- X=>Z, notIn(Z,L), rewrite1(Z,Y,[Z|L]).

% notIn(X,L) if X is not a top level member of list L.
notIn(_,[]).
notIn(X,[X|_]) :- !,fail.
notIn(X,[_|Rest]) :- notIn(X,Rest).

rrw(X,Y) :- rewrite(X,Y).
rrw(X,Y) :-
 split(X,P,Args),
 rrwl(Args,NewArgs),
 Y=..[P|NewArgs].