%%%%%%%%%%%%%%%%%%%%%
%  Meta-interpreter
%%%%%%%%%%%%%%%%%%%%%

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

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

% eval(E,V,P) true if expression E has value V
% given parameter settings P
deterministic eval(E,V,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(sigmoid(E),V,P) <-
   eval(E,EV,P) &
   V is 1/(1+exp(-EV)).
eval(N,N,_) <-
   number(N).
eval(N,V,P) <-
   lookup(N,V,P).
      
% lookup(N,V,P) is true if V is the first value assigned to
% N in parameter settings P
lookup(N,V,[val(N,V)|_]).
lookup(N,V,[val(N1,_)|R]) <-
   N \= N1 &
   lookup(N,V,R).



%%%%%%%%%%%%%%%%%%
% DATA
%%%%%%%%%%%%%%%%%%
% oav(Object,Attribute,Value) - here is the data
oav(e1,reads,0) <= true.
oav(e1,known,1) <= true.
oav(e1,new,1) <= true.
oav(e1,short,0) <= true.
oav(e1,home,1) <= true.

oav(e2,reads,1) <= true.
oav(e2,known,0) <= true.
oav(e2,new,1) <= true.
oav(e2,short,1) <= true.
oav(e2,home,0) <= true.

oav(e3,reads,0) <= true.
oav(e3,known,0) <= true.
oav(e3,new,0) <= true.
oav(e3,short,0) <= true.
oav(e3,home,0) <= true.

oav(e4,reads,0) <= true.
oav(e4,known,1) <= true.
oav(e4,new,0) <= true.
oav(e4,short,0) <= true.
oav(e4,home,1) <= true.

oav(e5,reads,1) <= true.
oav(e5,known,1) <= true.
oav(e5,new,1) <= true.
oav(e5,short,1) <= true.
oav(e5,home,1) <= true.

oav(e6,reads,0) <= true.
oav(e6,known,1) <= true.
oav(e6,new,0) <= true.
oav(e6,short,0) <= true.
oav(e6,home,0) <= true.

oav(e7,reads,0) <= true.
oav(e7,known,0) <= true.
oav(e7,new,0) <= true.
oav(e7,short,1) <= true.
oav(e7,home,0) <= true.

oav(e8,reads,1) <= true.
oav(e8,known,0) <= true.
oav(e8,new,1) <= true.
oav(e8,short,1) <= true.
oav(e8,home,0) <= true.

oav(e9,reads,0) <= true.
oav(e9,known,1) <= true.
oav(e9,new,0) <= true.
oav(e9,short,0) <= true.
oav(e9,home,1) <= true.

oav(e10,reads,0) <= true.
oav(e10,known,1) <= true.
oav(e10,new,1) <= true.
oav(e10,short,0) <= true.
oav(e10,home,0) <= true.

oav(e11,reads,0) <= true.
oav(e11,known,0) <= true.
oav(e11,new,0) <= true.
oav(e11,short,1) <= true.
oav(e11,home,1) <= true.

oav(e12,reads,0) <= true.
oav(e12,known,1) <= true.
oav(e12,new,1) <= true.
oav(e12,short,0) <= true.
oav(e12,home,0) <= true.

oav(e13,reads,1) <= true.
oav(e13,known,1) <= true.
oav(e13,new,0) <= true.
oav(e13,short,1) <= true.
oav(e13,home,1) <= true.

oav(e14,reads,1) <= true.
oav(e14,known,1) <= true.
oav(e14,new,1) <= true.
oav(e14,short,1) <= true.
oav(e14,home,0) <= true.

oav(e15,reads,1) <= true.
oav(e15,known,1) <= true.
oav(e15,new,1) <= true.
oav(e15,short,1) <= true.
oav(e15,home,1) <= true.

oav(e16,reads,1) <= true.
oav(e16,known,1) <= true.
oav(e16,new,0) <= true.
oav(e16,short,1) <= true.
oav(e16,home,0) <= true.

oav(e17,reads,1) <= true.
oav(e17,known,1) <= true.
oav(e17,new,1) <= true.
oav(e17,short,1) <= true.
oav(e17,home,1) <= true.

oav(e18,reads,1) <= true.
oav(e18,known,0) <= true.
oav(e18,new,1) <= true.
oav(e18,short,1) <= true.
oav(e18,home,0) <= true.

% Neural network with two hidden units
predicted_oav(Obj,reads,V) <=
   oav(Obj,h_1,I_1) &
   oav(Obj,h_2,I_2) &
   V is sigmoid(w_0+w_1* I_1+w_2* I_2).
%   V is w_0+w_1* I_1+w_2* I_2.        % linear threshold
oav(Obj,h_1,V) <=
   oav(Obj,known,I_1) &
   oav(Obj,new,I_2) &
   oav(Obj,short,I_3) &
   oav(Obj,home,I_4) &
   V is sigmoid(w_3+w_4* I_1+w_5* I_2+w_6* I_3+ w_7*I_4).
oav(Obj,h_2,V) <=
   oav(Obj,known,I_1) &
   oav(Obj,new,I_2) &
   oav(Obj,short,I_3) &
   oav(Obj,home,I_4) &
   V is sigmoid(w_8+w_9* I_1+w_10* I_2+w_11* I_3+w_12*I_4).
error(Obj,E) <=
   predicted_oav(Obj,reads,VC) &
   oav(Obj,reads,V) &
   E is (VC-V)*(VC-V).

%%%%%%%%%%%%%%%%%
% Example Queries
%%%%%%%%%%%%%%%%%%

% ask pprove(predicted_oav(e1,reads,V), [val(w_0, -2.97675), val(w_1, 6.87946), val(w_2, -2.10272), val(w_3, -5.25324), val(w_4, 1.97948), val(w_5, 1.86477), val(w_6, 4.71896), val(w_7, -0.388561), val(w_8, 0.492504), val(w_9, -1.03345), val(w_10, -1.0644), val(w_11, -0.749366), val(w_12, 0.126164)] ).

% New case with unknown user action:
oav(e19,known,0) <= true.
oav(e19,new,1) <= true.
oav(e19,short,0) <= true.
oav(e19,home,0) <= true.

% Example query, for the new case:
%?pprove(predicted_oav(e19,reads,V),[val(w_0, -2.97675), val(w_1, 6.87946), val(w_2, -2.10272), val(w_3, -5.25324), val(w_4, 1.97948), val(w_5, 1.86477), val(w_6, 4.71896), val(w_7, -0.388561), val(w_8, 0.492504), val(w_9, -1.03345), val(w_10, -1.0644), val(w_11, -0.749366), val(w_12, 0.126164)]).