%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Author:	Jon Sneyers
% Email:	jon@cs.kuleuven.ac.be
% Copyright:	K.U.Leuven 2004
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

:- module(guard_entailment,
	[
		entails_guard/2,
		simplify_guards/5
	]).

%:- use_module(library(chr)).
:- use_module(library(lists)).
:- use_module(hprolog).
:- use_module(builtins).

option(debug,off).
option(optimize,full).


:- constraints known/1,test/1,cleanup/0,variables/1.

% knowing the same thing twice is redundant
idempotence @ known(G) \ known(G) <=> true.


%--------------------------------------
% Rules to check if the argument of
% test/1 is entailed by known stuff
%--------------------------------------

% everything follows from an inconsistent theory
fail_implies_everything @ known(fail) \ test(X) <=> true.

% if it's known, it's entailed
trivial_entailment @ known(G) \ test(G) <=> true.

varfirst_nmatch @ test(X\==A) <=> nonvar(X) | test(A\==X).
distribute_nmatch @ test(X\==A) <=> nonvar(A),functor(A,Fu,Ar) | 
		A =.. [F|AArgs],
		length(XArgs,Ar), B =.. [Fu|XArgs],
		add_args_nmatch(XArgs,AArgs,ArgCond),
		C = (\+ functor(X,Fu,Ar) ; (functor(X,Fu,Ar),X=B,ArgCond)),
		test(C).

% eq implies leq
eq_implies_leq1 @ known(X=:=Y) \ test(X=<Y) <=> true.
eq_implies_leq2 @ known(X=:=Z) \ test(X=<Y) <=> number(Y), number(Z), Z=<Y |true.
eq_implies_leq3 @ known(X=:=Z) \ test(Y=<X) <=> number(Y), number(Z), Y=<Z |true.

% stronger inequality implies a weaker one
leq_implies_leq1 @ known(X=<Z) \ test(X=<Y) <=> number(Y), number(Z), Z=<Y |true.
leq_implies_leq2 @ known(X=<Y) \ test(Z=<Y) <=> number(X), number(Z), Z=<X | true.

% X =< Z implies X =\= Y for all Y > Z
leq_implies_neq1 @ known(X=<Z) \ test(X=\=Y) <=> number(Y), number(Z), Y>Z | true.
leq_implies_neq2 @ known(X=<Y) \ test(Y=\=Z) <=> number(X), number(Z), Z<X | true.


%--------------------------------------
% Rules to translate some stuff
%--------------------------------------

% we only want =<, =:= and =\=
known_g2l @ known(X>Y) <=> known(Y<X).
known_geq2leq @ known(X>=Y) <=> known(Y=<X).
known_l2leq_neq @ known(X<Y) <=> known(X=<Y), known(X=\=Y).
known_is2eq @ known(X is Y) <=> known(X=:=Y).
test_g2l @ test(X>Y) <=> test(Y<X).
test_geq2leq @test(X>=Y) <=> test(Y=<X).
test_l2leq_neq @test(X<Y) <=> test(((X=<Y),(X=\=Y))).
test_is2eq @ test(X is Y) <=> test(X=:=Y).

% propagate == and \== to =:= and =\=  (which is a weaker statement)
match2eq1 @ known(X==Y) ==> number(X) | known(X=:=Y).
match2eq2 @known(X==Y) ==> number(Y) | known(X=:=Y).
nmatch2neq1 @ known(X\==Y) ==> number(X) | known(X=\=Y).
nmatch2neq2 @ known(X\==Y) ==> number(Y) | known(X=\=Y).
 

%--------------------------------------
% Rules to extend the known stuff
%--------------------------------------

% if we derived inconsistency, all other knowledge is redundant
fail_is_better_than_anything_else @ known(fail) \ known(_) <=> true.

% conjunctions
conj @ known((A,B)) <=> known(A), known(B).

% no need to remember trivial stuff
forget_trivial01 @ known(X=:=X) <=> true.
forget_trivial02 @ known(X==X) <=> true.
forget_trivial03 @ known(X=<X) <=> true.
forget_trivial04 @ known(X=X) <=> true.


%--------------------------------------
% Rules for = and \= (and functor)
%--------------------------------------
unify_vars1 @ known(X=Y) <=> var(X) | X=Y.
unify_vars2 @ known(X=Y) <=> var(Y) | X=Y.
%functor @ known(functor(X,F,A)) <=> var(X),ground(F),ground(A) | functor(X,F,A).
inconsistency4     @ known(X\=Y) <=> var(X),var(Y),X=Y | known(fail).
inconsistency4     @ known(X\=Y) <=> ground(X),ground(Y),X=Y | known(fail).

functor @ variables(V),known(functor(X,F,A)) <=> 
	    var(X), ground(F), ground(A) | 
	    functor(X,F,A),
	    X =.. [_|Args],
	    append(Args,V,NewV),
	    variables(NewV).

functor_inconsistency1 @ known(functor(X,F1,A1)) <=> nonvar(X), \+ functor(X,F1,A1) | known(fail).
negfunctor_trivial @ known(\+ functor(X,F1,A1)) <=> nonvar(X), functor(X,F1,A1) | known(fail).
functor_inconsistency2 @ known(functor(X,F1,A1)), known(functor(X,F2,A2)) <=> 
			nonvar(F1),nonvar(A1),nonvar(F2),nonvar(A2) 
			% (F1 \= F2 ; A1 \= A2) is entailed by idempotence
			| known(fail).
nunify_inconsistency @ known(X\=X) <=> known(fail).
nonvar_unification @ known(X=Y) <=> nonvar(X), nonvar(Y),functor(X,F,A) |
		    ( functor(Y,F,A),X=Y ->
			true
		    ;
			known(fail)
		    ).
nunify_expand    @ known(X\=Y) <=> var(X),nonvar(Y), functor(Y,F,A), A>0 |
		    length(Args,A),
		    Y =.. [F|YArgs],
		    Y1 =.. [F|Args],
		    add_args_nunif(YArgs,Args,Nunif),
		    C = (\+ functor(X,F,A) ; (X = Y1, Nunif )),
		    known(C).
nunify_expand2    @ known(X\=Y) <=> nonvar(X),nonvar(Y), functor(X,F,A) |
		    (functor(Y,F,A) ->
			X =.. [F|XArgs],
			Y =.. [F|YArgs],
			add_args_nunif(XArgs,YArgs,Nunif),
			known(Nunif)
		    ;
			true
		    ).
nunify_symmetry    @ known(X\=Y) ==> known(Y\=X).


%--------------------------------------
% Rules for =<
%--------------------------------------

groundleq2 @ known(X=<Y) <=> number(X), number(Y), X>Y | known(fail).

% only keep the strictest inequality
remove_redundant_leq1 @ known(X=<Y) \ known(X=<Z) <=> number(Y), number(Z), Y=<Z | true.
remove_redundant_leq1 @ known(Z=<Y) \ known(X=<Y) <=> number(X), number(Z), X=<Z | true.
 
leq_antisymmetry @ known(X=<Y), known(Y=<X) <=> known(X=:=Y).
leq_transitivity @ known(X=<Y), known(Y=<Z) ==> known(X=<Z).

strict_leq_transitivity @ known(X=<Y),known(X=\=Y),known(Y=<Z),known(Y=\=Z) ==> known(X=\=Z).


%--------------------------------------
% Rules for =:=   (and =\=)
%--------------------------------------

groundeq2 @ known(X=:=Y) <=> number(X), number(Y), X=\=Y | known(fail).
groundneq2 @ known(X=\=Y) <=> number(X), number(Y), X=:=Y | known(fail).

neq_inconsistency  @ known(X=\=X) <=> known(fail).
inconsistency @ known(X=:=Y), known(X=\=Y) <=> known(fail).

eq_transitivity @ known(X=:=Y), known(Y=:=Z) ==> X \== Z | known(X=:=Z).

eq_symmetry  @ known(X=:=Y) ==> known(Y=:=X).
neq_symmetry @ known(X=\=Y) ==> known(Y=\=X).

%--------------------------------------
% Rules for number/1, float/1, integer/1
%--------------------------------------

notnumber @ known(number(X)) <=> nonvar(X), \+ number(X) | known(fail).
notfloat @ known(float(X)) <=> nonvar(X), \+ float(X)| known(fail).
notinteger @ known(integer(X)) <=> nonvar(X), \+ integer(X) | known(fail).
int2number @ known(integer(X)) ==> known(number(X)).
float2number @ known(float(X)) ==> known(number(X)).


%--------------------------------------
% Rules for \+
%--------------------------------------

inconsistency2 @ known(X), known(\+ X) <=> known(fail).


%--------------------------------------
% Rules for == and \==
%--------------------------------------

inconsistency3 @ known(X\==Y), known(X==Y) <=> known(fail).
eq_transitivity2 @ known(X==Y), known(Y==Z) ==> known(X==Z).
neq_substitution @ known(X==Y), known(Y\==Z) ==> known(X\==Z).
eq_symmetry2   @ known(X==Y) ==> known(Y==X).
neq_symmetry2  @ known(X\==Y) ==> known(Y\==X).
neq_inconsistency @ known(X\==X) ==> known(fail).
functorsmatch@ known(X\==Y) <=> nonvar(X), nonvar(Y), functor(X,F,A) |
				(functor(Y,F,A) ->
				    X =.. [F|XArgs],
				    Y =.. [F|YArgs],
				    add_args_nmatch(XArgs,YArgs,ArgCond),
				    known(ArgCond)
				;
				    true
				).
eq_implies_unif @ known(X==Y) ==> known(X=Y).


%--------------------------------------
% Rules for var/1 and nonvar/1
%--------------------------------------

ground2nonvar @ known(ground(X)) ==> known(nonvar(X)).
compound2nonvar @ known(compound(X)) ==> known(nonvar(X)).
atomic2nonvar @ known(atomic(X)) ==> known(nonvar(X)).
number2nonvar @ known(number(X)) ==> known(nonvar(X)).
atom2nonvar @ known(atom(X)) ==> known(nonvar(X)).

var_inconsistency @ known(var(X)), known(nonvar(X)) <=> known(fail).


%--------------------------------------
% Rules for disjunctions
%--------------------------------------

%ad-hoc disjunction optimization:
simplify_disj1 @ known(A) \ known((\+ A; B)) <=> known(B).
simplify_disj1b @ known(A) \ known((\+ A, C; B)) <=> known(B).
simplify_disj1c @ known(\+ A) \ known((A; B)) <=> known(B).
simplify_disj1d @ known(\+ A) \ known((A, C; B)) <=> known(B).

simplify_disj2 @ known((fail; B)) <=> known(B).
simplify_disj3 @ known((B ; fail)) <=> known(B).

simplify_disj4 @ known(functor(X,F1,A1)) \ known((\+ functor(X,F,A); B)) <=>
    % F1 \== F or A1 \== A
    true.	% the disjunction does not provide any additional information

simplify_disj5 @ known((\+ functor(X,F,A); B)) <=>
    nonvar(X), functor(X,F,A) |
    known(B).	
simplify_disj6 @ known((\+ functor(X,F,A); B)) <=>
    nonvar(X), \+ functor(X,F,A) |
    true.	% the disjunction does not provide any additional information

test_simplify_disj1 @test((fail;B)) <=> test(B).
test_simplify_disj2 @test((B;fail)) <=> test(B).


%--------------------------------------
% Rules to test unifications
%--------------------------------------

trivial_unif @ test(X=Y) <=> X=Y | X=Y.
testgroundunif @ test(X=A) <=> ground(X),ground(A) | X=A.
varfirst @ test(X=A) <=> nonvar(X),var(A) | test(A=X).
distribute_unif @ variables(V) \ test(X=A) <=>   var(X),nonvar(A),
		functor(A,F,Arit),Arit>0,
		A =.. [F|AArgs],\+ all_unique_vars(AArgs,V) |
		C=(functor(X,F,Arit),X=A),
		test(C).
distribute_unif2 @ test(X=A) <=>   var(X),nonvar(A),
		functor(A,F,Arit),%Arit>0,
		A =.. [F|AArgs] % , all_unique_vars(AArgs)
		| 
		C=functor(X,F,Arit),
		test(C).
distribute_unif3 @ test(X=A) <=>   nonvar(X),nonvar(A),functor(A,F,Arit),
		A =.. [F|AArgs] |
		functor(X,F,Arit),
		X =.. [F|XArgs],
		add_args_unif(XArgs,AArgs,ArgCond),
		test(ArgCond).

testvarunif @ variables(V) \ test(X=A) <=> \+ (memberchk_eq(A,V),memberchk_eq(X,V)) | X=A.
testvarunif @ variables(V) \ test(functor(X,F,A)) <=> 
                var(X),ground(F),ground(A),\+ memberchk_eq(X,V) |
		functor(X,F,A).       % X is a singleton variable

% trivial truths
true_is_true @ test(true) <=> true.
trivial01 @ test(X==Y) <=> X==Y | true.
trivial02 @ test(X=:=Y) <=> X==Y | true.
trivial03 @ test(X=<Y) <=> X==Y | true.
trivial04 @ test(X=<Y) <=> ground(X), ground(Y), X=<Y | true.
trivial05 @ test(X=<Y) <=> ground(X), ground(Y), X>Y | fail.
trivial06 @ test(X=:=Y) <=> ground(X), ground(Y), X=:=Y | true.
trivial07 @ test(X=:=Y) <=> ground(X), ground(Y), X=\=Y | fail.
trivial08 @ test(X=\=Y) <=> ground(X), ground(Y), X=\=Y | true.
trivial09 @ test(X=\=Y) <=> ground(X), ground(Y), X=:=Y | fail.
trivial10 @ test(functor(X,F1,A1)) <=> nonvar(X), functor(X,F1,A1) | true.
trivial11 @ test(functor(X,F1,A1)) <=> nonvar(X) | fail.
trivial12 @ test(ground(X)) <=> ground(X) | true.
trivial13 @ test(number(X)) <=> number(X) | true.
trivial14 @ test(float(X)) <=> float(X) | true.
trivial15 @ test(integer(X)) <=> integer(X) | true.
trivial16 @ test(number(X)) <=> nonvar(X) | fail.
trivial17 @ test(float(X)) <=> nonvar(X) | fail.
trivial18 @ test(integer(X)) <=> nonvar(X) | fail.
trivial19 @ test(\+ functor(X,F1,A1)) <=> nonvar(X), functor(X,F1,A1) | fail.
trivial20 @ test(\+ functor(X,F1,A1)) <=> nonvar(X) | true.
trivial21 @ test(\+ ground(X)) <=> ground(X) | fail.
trivial22 @ test(\+ number(X)) <=> number(X) | fail.
trivial23 @ test(\+ float(X)) <=> float(X) | fail.
trivial24 @ test(\+ integer(X)) <=> integer(X) | fail.
trivial25 @ test(\+ number(X)) <=> nonvar(X) | true.
trivial26 @ test(\+ float(X)) <=> nonvar(X) | true.
trivial27 @ test(\+ integer(X)) <=> nonvar(X) | true.

test_conjunction @ test((A,B)) <=> test(A),  known(A), test(B).
test_disjunction @ test((A;B)) <=> true | negate_b(A,NotA),negate_b(B,NotB),
		     (known(NotB),test(A) ; known(NotA),test(B)).

% disjunctions in the known stuff --> both options should entail the goals
% delay disjunction unfolding until everything is added, perhaps we can
% find entailed things without using the disjunctions
disjunction @ test(X), known((A;B)) <=>
    true |
    \+ try(A,X),!,
    negate_b(A,NotA),
    known(NotA),
    \+ try(B,X).


% not entailed or entailment not detected
could_not_prove_entailment @ test(_) <=>  fail.


clean_store1 @ cleanup \ known(_) <=> true.
clean_store2 @ cleanup \ variables(_) <=> true.
clean_store3 @ cleanup <=> true.


%--------------------------------------
% End of CHR part
%--------------------------------------


entails_guard(List,Guard) :- 
    copy_term_nat((List,Guard),(CopyList,CopyGuard)),
    term_variables(CopyList,CLVars),
    variables(CLVars),
    entails_guard2(CopyList),
    !,test(CopyGuard),!,
    cleanup.

entails_guard2([]).
entails_guard2([A|R]) :- 
    known(A), entails_guard2(R).

simplify_guards(List,Body,GuardList,SimplifiedGuards,NewBody) :- 
%    write(starting),nl,
    copy_term_nat((List,GuardList),(CopyList,CopyGuard)),
    term_variables(CopyList,CLVars),
%    write(variables(CLVars)),nl,
    variables(CLVars),
%    write(gonna_add(CopyList)),nl,
    entails_guard2(CopyList),
%    write(ok_gonna_add),nl,
    !,
%    write(gonna_simplify(CopyGuard)),nl,
    simplify(CopyGuard,L),
%    write(ok_gonna_simplify(CopyGuard,L)),nl,
    simplified(GuardList,L,SimplifiedGuards,Body,NewBody),
%    write(ok_done),nl,
    !,
    cleanup.

simplified([],[],[],B,B).
simplified([G|RG],[keep|RL],[G|RSG],B,NB) :- simplified(RG,RL,RSG,B,NB).
simplified([G|RG],[fail|RL],fail,B,B).
simplified([G|RG],[true|RL],[X|RSG],B,NB) :- 
	builtins:binds_b(G,GVars), term_variables(RG,RGVars),
	intersect_eq(GVars,RGVars,SharedWithRestOfGuard),!,
	( SharedWithRestOfGuard = []	->
	    term_variables(B,BVars),
	    intersect_eq(GVars,BVars,SharedWithBody),!,
	    ( SharedWithBody = []	->
		X=true,		% e.g. c(X) <=> Y=X | true.
		NB=NB2
	    ;
		X=true,		% e.g. c(X) <=> Y=X | writeln(Y).
		NB=(G,NB2)
	    )
	;
	    X=G,		% e.g. c(X) <=> Y=X,p(Y) | true.
	    NB=NB2
	),
	simplified(RG,RL,RSG,B,NB2).

simplify([],[]).
simplify([G|R],[SG|RS]) :-
    ( \+ try(true,G) ->
	SG = true
    ;
	builtins:negate_b(G,NotG),
	(\+ try(true,NotG) ->
	    SG = fail    
	;
	    SG = keep
	)
    ),
    known(G),
    simplify(R,RS).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%  AUXILIARY PREDICATES
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

try(A,X) :- (known(A) ->
		true
	    ;
		format(' ERROR: entailment checker: this is not supposed to happen.\n',[])
	    ),
	 (test(X) -> 
		fail
	    ;
		true).


lookup([],[],_,_) :- fail.
lookup([K|R],[V|R2],X,Y) :-
    (X == K ->
	Y=V
    ;
	lookup(R,R2,X,Y)
    ).


add_args_unif([],[],true).
add_args_unif([X|RX],[Y|RY],(X=Y,RC)) :-
    add_args_unif(RX,RY,RC).

add_args_nunif([],[],fail).
add_args_nunif([X|RX],[Y|RY],(X\=Y;RC)) :-
    add_args_nunif(RX,RY,RC).

add_args_nmatch([],[],fail).
add_args_nmatch([X|RX],[Y|RY],(X\==Y;RC)) :-
    add_args_nmatch(RX,RY,RC).

all_unique_vars(T,V) :- all_unique_vars(T,V,[]).

all_unique_vars([],V,C).
all_unique_vars([V|R],Vars,C) :-
    var(V),
    \+ memberchk_eq(V,Vars),
    \+ memberchk_eq(V,C),
    all_unique_vars(R,[V|C]).