%%%% CILog implementation of ArLog the logic programming language
%%%% with parameterized arithmetic expressions.

arprove(A&B,E1,E3) <-
   arprove(A,E1,E2) &
   arprove(B,E2,E3).
arprove(G,E1,E2) <-
   (G <= B) &
   arprove(B,E1,E2).
arprove(true,E,E).
arprove((V is Exp),E1,E1) <-
   eval(Exp,V,E1).
arprove(assign(X,Exp),E1,E2) <-
   eval(Exp,Val,E1) &
   update(X,Val,E1,E2).
arprove(X > Y,E1,E1) <-
   eval(X,XV,E1) &
   eval(Y,YV,E1) &
   XV > YV.

eval(N,N,E) <-
   number(N).
eval(C,V,E) <-
   member(val(C,V),E).
eval((X+Y),V,E) <-
   eval(X,XV,E)&
   eval(Y,YV,E)&
   V is XV+YV.
eval((X*Y),V,E) <-
   eval(X,XV,E)&
   eval(Y,YV,E)&
   V is XV*YV.
eval((X-Y),V,E) <-
   eval(X,XV,E)&
   eval(Y,YV,E)&
   V is XV-YV.
eval((X/Y),V,E) <-
   eval(X,XV,E)&
   eval(Y,YV,E)&
   V is XV/YV.
eval(UD,V,E) <-
   (UD=Exp <= B) &
   arprove(B,E,_) &
   eval(Exp,V,E).

member(E,[E|R]).
member(E,[H|T]) <-
   member(E,T).

update(X,Val,[val(X,OV)|Rest],[val(X,Val)|Rest]).
update(X,Val,[val(X1,V1)|Rest0],[val(X1,V1)|Rest1]) <-
   update(X,Val,Rest0,Rest1).

