%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Unification Algorithm for set-terms with
%%% urelements, as described in
%%%    A. Dovier, A. Formisano, and E. G. Omodeo,
%%%    Decidability Results with Atoms,
%%%    ACM TOCL, to appear.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Updated Udine, June 2nd, 2004
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  Hints for using the program:
%  From a SICStus shell, "consult" the file.
%  Call the goal
%      :- meta.
%  The prompt becomes
%      s-unify :-
%  The interpreter is ready to solve "set" unification
%  problems. For instance,
%      s-unify :- {X,Y} = {a,b},{Y,Z} = {b,c}.
%  returns the (unique solution)
%      E: Z = c , X = a , Y = b
%      U:
%      Execution Time:         0
% Execution Time is expressed in ms.
% Another example:
%     s-unify :- {a,b/X} = {Y/X}.
% returns the solution:
%     E: X = {a, b, Y/_4735}
%     U:
%     Execution Time:         0
% For other solutions type "y.", to end type "n."
% The slash symbol "/" denotes the "rest" of a set.
% Basically { t / s } means { t } "union" s.
% (in the paper, instead, the vertical bar "|" is used.
% We have used "/" to avoid conflicts with the list constructor)
% Let us see a problem using properties of urelements
% as self-singleton
%     s-unify :- {a,b/b} = {b,a/a}.
% that returns true.
% To exit type "halt."
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Partial prints can be inserted by decommenting
% the predicate "partialwrite" here below.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

:-use_module(library(lists)).
:-use_module(library(terms)).
:-prolog_flag(unknown,_,fail).

%%% Comment/Decomment here to remove/add partial prints.
%%% partialwrite.

%%% Main predicate (meta, to properly deal with variable names)
%%% Input: a list e1,e2,...,en of equations or
%%% "halt" to exit from the program

meta :-
   write('s-unify :- '),
   read_term(Goal,[variable_names(VarNames)]),
   build_system(Goal,System),
   get_time(T1),
   (System = halt, abort;
    unify(System,SystemOut,U,VarNames),
    get_time(T2),
    nl,write('************Found a Solution:'),nl,
    write('E: '),
    my_print_list(SystemOut,VarNames),nl,
    write('U: '),
    my_print_list(U,VarNames),nl,
    writetime('Execution Time: ',T1,T2),nl,
    write('another solution (y./n.) ? '),
    read(Y),
   (Y = 'n', !, meta;
    fail)).

meta :-
   write('no more solutions'),nl,
   meta.

%%% unify(+Equation System,
%%%       - Equation system in solved form,
%%%       - The Constraint store
%%%       + The binding variable names/vars)

unify(Ein,Esf,U,VarNames) :-
    preproc_system(Ein,Epre),
    internal_unify(Epre,[], [],Esf,[],U,VarNames).

%%%%%%%%%%%%
%%% internal_unify( + E (System),
%%%        + Emembership,
%%%        + Esolved form,
%%%        - Esolved form,
%%%        + Constraints U
%%%        - Constraints U
%%%        + The binding variable names/vars)

internal_unify( [], [],  Esf , Esf , U , U , _VarNames).
internal_unify( [], Em,  Esfin, Esfout, Uin, Uout,VarNames) :-
    Em \= [],
    simplify_memberships(Em,Eint),
    internal_unify(Eint,[],Esfin,Esfout,Uin,Uout,VarNames).
internal_unify( [ (L = R) | E ], Em, Esfin, Esfout, Uin, Uout, VarNames) :-
    xe_membership(L, R),
    !,
    internal_unify(E, [(L = R)|Em], Esfin, Esfout,Uin,Uout, VarNames).
internal_unify( [ (L = R) | E ], Em, Esfin, Esfout, Uin, Uout, VarNames) :-
   (partialwrite,
    write('Selected equation: '),
    my_print(L, VarNames), write(' = '),
    my_print(R, VarNames),
    write('\t');
    \+ partialwrite),
   rewriting_rule(L, R, E, Eparz, Esfin, Esfparz, Uin, Uoutparz),
   internal_unify(Eparz, Em, Esfparz, Esfout, Uoutparz, Uout, VarNames).

%%%% Rewriting rules:
% 1
rewriting_rule(X,Y, E,E, Esf,Esf, U, U) :-
      X == Y,!,
      (partialwrite, write('Rule: 1-'),nl;
       \+ partialwrite).
% 2.1
rewriting_rule(T,X, Ein,[(X = T) |Ein], Esf,Esf, U, U) :-
      var(X),nonvar(T),!,
      (partialwrite, write('Rule: 2.1-'),nl;
       \+ partialwrite).
% 2.2
rewriting_rule(T,C,Ein,[(C = T)|Ein], Esf, Esf, U, U) :-
      urelement(C),
      xe_list(T),!,
      (partialwrite, write('Rule: 2.2-'),nl;
       \+ partialwrite).
% 3.1
rewriting_rule(X,List,Ein,Eout, Esf,Esf, Uin,[X|Uin]) :-
      var(X),
      xe_list(List),
      member_nested(X,List),
      tail(List,_,Y,_),
      var(Y),
      !,
      generate_equations_all(X,List,Ein,Einp),
      ( (partialwrite, write('Rule: 3.1(i)-'),nl;
         \+ partialwrite),
         Eout = [(Y = []) |Einp] ; %%% (i)
         (partialwrite, write('Rule: 3.1(ii)-'),nl;
         \+ partialwrite),
         Eout = [(Y = X) |Einp] ). %%% (ii)
% 3.2
rewriting_rule(X,List,Ein,Einp, Esf ,Esf , Uin,[X|Uin]) :-
      var(X),
      xe_list(List),
      member_nested(X,List),
      tail(List,_,Y,_),
      Y == [],
      !,
      (partialwrite, write('Rule: 3.2-'),nl;
       \+ partialwrite),
      generate_equations_all(X,List,Ein,Einp).
% 3.3
rewriting_rule(X,List,Ein,Eout, Esf,Esf, U,U) :-
      var(X),
      xe_list(List),
      non_member_nested(X,List),
      tail(List,_,Y,_),
      var(Y),
      member_strong(X,U),
      !,
      generate_equations_all(X,List,Ein,Einp),
      ( (partialwrite, write('Rule: 3.3(i)-'),nl;
         \+ partialwrite), Eout = [(Y = []) |Einp] ; %%% (i)
        (partialwrite, write('Rule: 3.3(ii)-'),nl;
         \+ partialwrite), Eout = [(Y = X) |Einp] ). %%% (ii)
% 3.4
rewriting_rule(X,List,Ein,Einp, Esf,Esf, U,U) :-
        var(X),
        xe_list(List),
        non_member_nested(X,List),
        tail(List,_,Y,_),
        Y == [],
        member_strong(X,U),
        !,
        (partialwrite, write('Rule: 3.4-'),nl;
         \+ partialwrite),
        generate_equations_all(X,List,Ein,Einp).
% 3.5
rewriting_rule(X,List,Ein,[(X = Y) | Einp], Esf,Esf, U,U) :-
        var(X),
        xe_list(List),
        non_member_nested(X,List),
        tail(List,_,Y,_),
        urelement(Y),
        member_strong(X,U),
        !,
        (partialwrite, write('Rule: 3.5-'),nl;
         \+ partialwrite),
         generate_equations_all(X,List,Ein,Einp).
% 4.1
rewriting_rule(X,Y,Ein, Einp, Esf,[(X = Y)|Esfnew], U,[Y|U]) :-
        var(X),
        var(Y),
        X \== Y,
        member_strong(X,U), %% ur(X)
        !,
        (partialwrite, write('Rule: 4.1-'),nl;
         \+ partialwrite),
        apply_subst(X,Y,Ein,Einp),
        apply_subst(X,Y,Esf,Esfnew).
% 4.2
rewriting_rule(X,Y,Ein, Einp, Esf,[(X = Y)|Esfnew], U, U) :-
      var(X),
        urelement(Y),
        !,
        (partialwrite, write('Rule: 4.2-'),nl;
         \+ partialwrite),
        apply_subst(X,Y,Ein,Einp),
        apply_subst(X,Y,Esf,Esfnew).
% 4.3
rewriting_rule(X,Y,Ein, Einp, Esf,[(X = Y)|Esfnew], U, U) :-
      var(X),
        occur_check(X,Y),
        non_member_strong(X,U),
        !,
        (partialwrite, write('Rule: 4.2-'),nl;
         \+ partialwrite),
        apply_subst(X,Y,Ein,Einp),
        apply_subst(X,Y,Esf,Esfnew).
% 5.1
rewriting_rule(C,T,_, _, _,_ , _,_) :-
      urelement(C),
        tail(T,_,D,_),
        urelement(D),
        D \== C,
        !,
        (partialwrite, write('Rule: 5.1-fail'),nl;
         \+ partialwrite),
        fail.
% 5.2
rewriting_rule(C,T,_, _, _,_ , _,_) :-
      urelement(C),
        T == [],
        !,
        (partialwrite, write('Rule: 5.2-fail'),nl;
         \+ partialwrite),
        fail.
% 5.3
rewriting_rule([],T,_, _, _,_ , _,_) :-
        nonvar(T),
        functor(T,'.',2),
        !,
        (partialwrite, write('Rule: 5.3-fail'),nl;
         \+ partialwrite),
        fail.
% 5.4
rewriting_rule(T,[],_, _, _,_ , _,_) :-
        nonvar(T),
        functor(T,'.',2),
        !,
        (partialwrite, write('Rule: 5.4-fail'),nl;
         \+ partialwrite),
        fail.
% 6.1
rewriting_rule(C,List,Ein,Eout, Esf,Esf, Uin,Uin) :-
      urelement(C),
        xe_list(List),
        tail(List,_,Y,_),
        var(Y),
        !,
        generate_equations_all(C,List,Ein,Einp),
         ( (partialwrite, write('Rule: 6.1(i)-'),nl;
            \+ partialwrite), Eout = [(Y = []) |Einp] ; %%% (i)
           (partialwrite, write('Rule: 6.1(ii)-'),nl;
            \+ partialwrite), Eout = [(Y = C) |Einp] ). %%% (ii)
% 6.2
rewriting_rule(C,List,Ein,Eout, Esf,Esf, Uin,Uin) :-
        urelement(C),
        xe_list(List),
        tail(List,_,T,_),
        (T == C;
         T == []),
        !,
        (partialwrite, write('Rule: 6.2-'),nl;
         \+ partialwrite),
        generate_equations_all(C,List,Ein,Eout).
%7.1
rewriting_rule(Set1,Set2,Ein,Eout, Esf,Esf,U,U) :-
       nonvar(Set1),
         nonvar(Set2),
         Set1 = [T|S],
         Set2 = [T1 |S1],
         tail(S,_,H,_),
         tail(S1,_,K,_),
         var(H), var(K), H == K,
         !,
         ( (partialwrite, write('Rule: 7.1(iv)-'),nl;
            \+ partialwrite),Eout = [(S = [T1|S1]), (H = [T|H])|Ein]; %d
          (my_select(Ti,[T1 |S1],Si),
        ((partialwrite, write('Rule: 7.1(i)-'),nl;
          \+ partialwrite), Eout = [(S= Si),(T = Ti)|Ein]; %a
           (partialwrite, write('Rule: 7.1(ii)-'),nl;
            \+ partialwrite), Eout = [([T|S]=Si),(T = Ti)|Ein];  %b
         (partialwrite, write('Rule: 7.1(iii)-'),nl;
           \+ partialwrite),Eout = [ (S = [T1 |S1]),(T = Ti)|Ein]))). %c
 % 7.2
rewriting_rule(Set1,Set2,Ein,Eout, Esf,Esf, U,U) :-
       nonvar(Set1),
         nonvar(Set2),
         Set1 = [T|S],
         Set2 = [T1 |S1],
         tail(S,_,H,_),
         tail(S1,_,K,_),
         (var(H), var(K), H \== K ;
          nonvar(H), var(K);
          nonvar(K) ),
          ((partialwrite, write('Rule: 7.2(i)-'),nl;
            \+ partialwrite), Eout = [(S= S1),(T = T1)|Ein]; %a
           (partialwrite,  write('Rule: 7.2(ii)-'),nl;
            \+ partialwrite), Eout = [(S=[T1|S1]),(T = T1)|Ein];  %b
           (partialwrite, write('Rule: 7.2(iii)-'),nl;
            \+ partialwrite), Eout = [([T|S]=S1), (T = T1)|Ein];  %c
           (partialwrite, write('Rule: 7.2(iv)-'),nl;
            \+ partialwrite), Eout = [(S=[T1| N]),(S1=[T |N])|Ein] ).  %d

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Predicates for handling membership equations
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

simplify_memberships(Ein,Eout) :-
      compact_membership(Ein,Eint),
      untail(Eint,Eout).

%%%%%%%%%

compact_membership([],[]).
compact_membership([ (X = T) | R],Enew) :-
     xe_membership(X,T),
      pick_equation(X,R,(X = T1),S),
      !,
      concatena(T,T1,T2),
      compact_membership([(X = T2) |S],Enew).
compact_membership([ (X = T) | R],[(X = T)|Enew]) :-
     xe_membership(X,T),
      !,
      compact_membership(R,Enew).
compact_membership([ Eq | R],[Eq | Enew]) :-
      compact_membership(R, Enew).

%%%%%%%%%%%%%%%%

%%% xe_membership(+X,+T)
%%% states if X = T is a membership
%%% equation.

xe_membership(X,T) :-
      var(X),
      xe_list(T),
      tail(T,[],Y,T1),
      Y == X,
      occur_check(X,T1).

%%% xe_list(+Term)
%%% states if Term is a list

xe_list(A) :-
     nonvar(A),
      A = [_|_].

%%% Auxiliary predicates for unification

my_select(_,S,_):-
       var(S), !, fail.
my_select(Z, [Z|R], R).
my_select(Z, [Y|R], [Y|A]):-
       my_select(Z, R, A).

generate_equations_all(_X,R,E,E) :-
    var(R),!.
generate_equations_all(_X,At,E,E):-
    atomic(At),!.
generate_equations_all(X,[A|R],E,Eout) :-
     generate_equations_all(X, R , [(X = A) | E], Eout).

urelement(C) :-
        atomic(C),
        C \= [].

%%%% VARIE SU LISTE

occur_check(X,Term):-
      term_variables(Term, Vars),
      non_member_strong(X,Vars).

%%%%%%%%%

apply_subst(_,_,G,G) :-
      ground(G), !.
apply_subst(X,_,V,V) :-
      var(V),
        V \== X,
        !.
apply_subst(X,T,Y,T) :-
      var(Y),
      Y == X,
      !.
apply_subst(X,T,In,Out):-
       In =.. [F|List],
       apply_subst_all(X,T,List,List1),
       Out =.. [F|List1].
apply_subst_all(_X,_T,[],[]).
apply_subst_all(X,T,[A|R],[B|S]) :-
       apply_subst(X,T,A,B),
       apply_subst_all(X,T,R,S).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%     Preprocessing
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

preproc_system([],[]).
preproc_system([(L = R)|A],[(L1 = R1) | B]) :-
    preproc(L,L1),
    preproc(R,R1),
    preproc_system(A,B).

%%% preproc( +term, -variable)
%%% tranlates a term of the form
%%% a: urelement
%%% X: variable
%%% {t_1,\dots,t_n / r}
%%% into internal notation.

preproc(X,X):-
        var(X),!.
preproc(X,Y):-
        is_set(X),
        !,
        set_preproc(X,Y).
preproc(X,X):-
        atomic(X).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

set_preproc({},[]):- !.
set_preproc('{}'(A),B):-
       set_preproc_elems(A,B),!.
set_preproc(_,_):-
       write('bad term!'),nl, fail.
set_preproc_elems( (A), [[]]) :-
   A == {},
   !.
set_preproc_elems( (A), [A]) :-
   (atomic(A);
    var(A)),
    !.
set_preproc_elems('{}'(A),[B]):-
       set_preproc_elems(A,B),!.
set_preproc_elems( (A / X), [B|Y]) :-
   preproc(A,B),
   preproc(X,Y).
set_preproc_elems((A,(B)), [C|D]) :-
   preproc(A,C),
   set_preproc_elems(B,D).

is_set(X):- nonvar(X),
            functor(X,{},_).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Timing predicates :
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

get_time(T) :-
    statistics(runtime,[T|_]).
writetime(Avviso,InitialTime,FinalTime) :-
    Delta is FinalTime - InitialTime,
    write(Avviso),write('\t'),
    write(Delta),nl.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% my_print( + term , + VarNames )
%% print a term where internal variables are
%% replaced by their input names stored in the
%% list VarNames
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

my_print( X , VarNames) :-
  var(X),
  var_name(X,VarNames,Name), !,
  write(Name).
my_print( X ,_) :-
  var(X),!,
  write(X).
my_print([], _ ) :-
  !,
  write('{}').
my_print([T|C], VarNames) :-
  !,
  print_set([T|C],VarNames).
my_print(Term, _VarNames) :-
  Term =.. [ Const ], !,
  write(Const).
my_print(Term, VarNames) :-
  Term =.. [ '=', L, R ], !,
  my_print(L, VarNames),
  write(' = '),
  my_print(R, VarNames).
my_print(Term, VarNames) :-
  Term =.. [ F | Args ], !,
  write(F),write('('),
  my_print_list(Args, VarNames),
  write(')').

%%%%% auxiliary recursive proc.
my_print_list([], _ ).
my_print_list([T], VarNames) :-
  my_print(T, VarNames),
  !.
my_print_list([T|R], VarNames) :-
  my_print(T, VarNames),
  write(' , '),
  my_print_list(R, VarNames).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% print_set + Set (actually a list) + VarNames
%%% prints the set representes by Set with real
%%% variable names
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

print_set(Set, VarNames) :-
  write('{'),
  print_elements(Set,VarNames),
  write('}').
print_elements([ T | C], VarNames) :-
  var(C),
  !,
  my_print(T, VarNames),
  write('/'),
  my_print(C,VarNames).
print_elements([T], VarNames) :-
   !,
   my_print(T, VarNames).
print_elements([ T | C], VarNames) :-
  urelement(C),!,
  my_print(T, VarNames),
  write(' / '),
  write(C).
print_elements([ T | R ], VarNames) :-
  my_print(T, VarNames),
  write(', '),
  print_elements(R, VarNames).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% var_name finds the external name
%%% for the (internal) variable A
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

var_name(A, [Name=C|_], Name) :-
        var(A),
        A==C,
        !.
var_name(A, [_|B], Name) :-
        var_name(A, B, Name).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% Ausiliary list predicates
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

untail([],[]).
untail([(X = T) |R],[(X = T1) | S]) :-
     tail(T,_New,_Old,T1),
      untail(R,S).
pick_equation(X,[(Y = T) | S],(X = T),S):-
     var(Y),
      Y == X,
     xe_membership(X,T),
      !.
pick_equation(X,[ _ | S],(X = T),S):-
     pick_equation(X,S,(X=T),S).

%%% concatena is an append introducing
%%% a new rest variable

concatena(V,R,R) :-
     var(V),
     !.
concatena([],R,R).
concatena([A|R],B,[A|S]) :-
    concatena(R,B,S).


%%% tail(+Term,+NewTail,-Tail,-TermNEw)
%%% returns the Tail of the Term (variable or
%%% atomic) and the term in which the tail has been
%%% replaced by NewTail

tail(R,NewTail,R,NewTail) :-
    var(R),!.
tail(At,NewTail,At,NewTail) :-
    atomic(At),!.
tail([A|R],NewTail,T,[A|S]) :-
      tail(R,NewTail,T,S).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% member_strong/non member_strong are the
%%% syntactic versions of member/non_member
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

member_strong(A,B):-
       nonvar(B),
       B = [ X |_ ],
       A == X,!.
member_strong(A,B):-
       nonvar(B),
       B = [_|Y],
       member_strong(A,Y).
non_member_strong(_A,R) :-
     var(R), !.
non_member_strong(_A,At):-
    atomic(At).
non_member_strong(A,[B|R]) :-
     A \== B,
      non_member_strong(A,R).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% member_nested check recursively
%%% the syntactic membership
%%% non_member_nested is its negation
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

member_nested(A,T) :-
     nonvar(T),
      T = [B|_R],
     A == B,
      !.
member_nested(A,T) :-
     nonvar(T),
      T =  [B|_R],
     member_nested(A,B).
member_nested(A,T) :-
     nonvar(T),
      T = [_B|R],
     member_nested(A,R).

non_member_nested(_A,R) :-
     var(R), !.
non_member_nested(_A,At):-
    atomic(At).
non_member_nested(A,[B|R]) :-
     A \== B,
      non_member_nested(A,B),
      non_member_nested(A,R).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% build_system transform a
%%% list (e1,e2,...,en) of input equations
%%% into the set of equations [e1,e2,...,e_n]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

build_system(halt,halt) :-
  !.
build_system(','(A,B),[A|R]) :-
  !,
  build_system(B,R).
build_system((A),[A]).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%