:- module(eq,[eq/2]).
:- use_module(library(chr)).

same_functor(T1,T2) :- functor(T1,P,N), functor(T2,P,N).

args2list(T,L) :- T=..[_|L].

same_args([],[]).
same_args([T1|L1],[T2|L2]):- eq(T1,T2), same_args(L1,L2).

:- chr_constraint eq/2.

reflexivity @ eq(X,X) <=> var(X) | true.

orientation @ eq(T,X) <=> var(X), X @< T | eq(X,T).

decomposition @ eq(T1,T2) <=> nonvar(T1),nonvar(T2) |
    same_functor(T1,T2),args2list(T1,L1),args2list(T2,L2),same_args(L1,L2).

confrontation @ eq(X,T1), eq(X,T2) <=> var(X),X @< T1,T1 @=< T2 |
    eq(X,T1), eq(T1,T2).

/*

?- eq(a,a).
true .

?- eq(a,b).
false.

?- eq(a,X).
eq(_G26935,a)
true ;
false.

?- eq(p(a,X,f(g(Y))),p(Z,f(Z),f(U))).
eq(_G26944,g(_G26934))
eq(_G26939,f(_G26942))
eq(_G26942,a)
true ;
false.

?- eq(p(X,f(X),f(f(X))),p(f(f(Y)),Y,f(Y))).
eq(_G26597,f(_G26587))
eq(_G26587,f(f(_G26597)))
true ;
false.

*/