% Meta-intepreter for parameterized logic programs (in Cilog)
% Copyright David Poole, 1997

% pprove(G,E) means prove G with parameter settings E.
% E is a list of the value assignments of the
% form val(P,V)

pprove(true,_).
pprove((A & B),E) <-
   pprove(A,E) &
   pprove(B,E).
pprove((A is Exp),E) <-
   eval(Exp,A,E).
pprove(H,E) <-
   (H <= B) &
   pprove(B,E).

% eval(E,V,P) true if expression E has value V
% given parameter settings P
eval((A+B),S,P) <-
   eval(A,VA,P) &
   eval(B,VB,P) &
   S is VA+VB.
eval((A*B),S,P) <-
   eval(A,VA,P) &
   eval(B,VB,P) &
   S is VA*VB.
eval((A-B),S,P) <-
   eval(A,VA,P) &
   eval(B,VB,P) &
   S is VA-VB.
eval((A/B),S,P) <-
   eval(A,VA,P) &
   eval(B,VB,P) &
   S is VA/VB.
eval(N,N,_) <-
   number(N).
eval(N,V,P) <-
   lookup(N,V,P).

% lookup(N,V,P) is true is parameter name N has value V in envirnment E
lookup(N,V,E) <-
   member(val(N,V),E).

% member(E,L) is true is E is a member of list L
member(A,[A|_]).
member(A,[_|L]) <-
   member(A,L).