:- module('VEOMEGAR', ['[[]]'/2]).
:- use_module('TOOLS', ['universal?'/1, 'existential?'/1, sub_binder/2, find/7, write_tag/1, const_Cont/9]).

% The transition semantics of QCHR is extended as follows: Disjunction in the body is allowed.

'[[]]'(conf(Binder, [state([(Goal_1 ; _Goal_2) | Omega], S, H, C) | States]), Final_Configuration) :-

    Cont = conf(Binder, [state([Goal_1 | Omega], S, H, C) | States]),

    '[[]]'(Cont, Final_Configuration).

'[[]]'(conf(Binder, [state([(_Goal_1 ; Goal_2) | Omega], S, H, C) | States]), Final_Configuration) :-
    !,

    Cont = conf(Binder, [state([Goal_2 | Omega], S, H, C) | States]),

    '[[]]'(Cont, Final_Configuration).

'[[]]'(conf(Binder, [state([write(T) | Omega], S, H, C) | States]), Final_Configuration) :-
    !,

    Cont = conf(Binder, [state(Omega, S, H, C) | States]),

    write(T),
    
    '[[]]'(Cont, Final_Configuration).

'[[]]'(conf(Binder, [state([writeln(T) | Omega], S, H, C) | States]), Final_Configuration) :-
    !,

    Cont = conf(Binder, [state(Omega, S, H, C) | States]),

    writeln(T),
    
    '[[]]'(Cont, Final_Configuration).

%%%%%%%%%%%%%%%%%%%%%%%%%
% Existential unfolding %
%%%%%%%%%%%%%%%%%%%%%%%%%
'[[]]'(conf(Binder, [state(['<E>'(It, LowerBound, UpperBound, E, B) | Omega],S,H,C) | States]), Final_Configuration) :-
    'existential?'(Binder),
    LowerBound =< UpperBound,
    
    !,
    
    copy_term((It, E, B, S), (It_, E_, B_, S_)),  
    It_ = LowerBound,
    call(E_),
    LowerBound_ is LowerBound + 1,

    Cont = conf(Binder, 
	    [state(B_,S_,H,C),
	     state(['<E>'(It, LowerBound_, UpperBound, E, B) | Omega],S,H,C) | States]
	   ),

    (show -> write(Cont), write(' [E Unfolding]'), nl ; true),

    '[[]]'(Cont, Final_Configuration).

%%%%%%%%%%%%%%%%%%%%%%%
% Existential Failure %
%%%%%%%%%%%%%%%%%%%%%%%
'[[]]'(conf(Binder, [state(['<E>'(_It, LowerBound, UpperBound, _E, _B) | _Omega],_S,_H,_C) | States]), Final_Configuration) :-
    'existential?'(Binder),
    LowerBound > UpperBound,
    
    !,

    sub_binder(Binder, Binder_),
    
    Cont = conf(Binder_, [failure | States]),
    
    (show -> write(Cont), write(' [E Failure]'), nl; true),
    
    '[[]]'(Cont, Final_Configuration).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Existential Failure Propagate %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'[[]]'(conf(Binder, [failure | States]), Final_Configuration) :-
    'existential?'(Binder),
    !,

    Cont = conf(Binder, States),

    (show -> write(Cont), write(' [E FailurePropagate]'), nl; true),
    
    '[[]]'(Cont, Final_Configuration).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Existential Success Propagate %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'[[]]'(conf(Binder,
	    [success, state(['<E>'(_It, _LowerBound, _UpperBound, _E, _B) | Omega],S,H,C) | States]
	    ),
       Final_Configuration) :-
    'existential?'(Binder),
    
    !,
    
    sub_binder(Binder, Binder_),
    
    Cont = conf(Binder_, [state(Omega,S,H,C) | States]), % Modification !!!
    
    (show -> write(Cont), write(' [E SuccessPropagate]'), nl ; true),

    '[[]]'(Cont, Final_Configuration).

%%%%%%%%%%%%%%%%%%%%%%%
% Universal unfolding %
%%%%%%%%%%%%%%%%%%%%%%%
'[[]]'(conf(Binder, [state(['<V>'(It, LowerBound, UpperBound, E, B) | Omega],S,H,C) | States]), Final_Configuration) :-
    'universal?'(Binder),
    LowerBound =< UpperBound,
    
    !,

    copy_term((It, E, B, S), (It_, E_, B_, S_)), It_ = LowerBound,
    call(E_),
    
    LowerBound_ is LowerBound + 1, 
    Cont = conf(Binder,
		[state(B_,S_,H,C),
		 state(['<V>'(It, LowerBound_, UpperBound, E, B) | Omega],S,H,C) | States]
		),

    (show -> write(Cont), write(' [U Unfolding]'), nl; true),

    '[[]]'(Cont, Final_Configuration).

%%%%%%%%%%%%%%%%%%%%%
% Universal Success %
%%%%%%%%%%%%%%%%%%%%%
'[[]]'(conf(Binder, [state(['<V>'(_It, LowerBound, UpperBound, _E, _B) | Omega], S, H, C) | States]), Final_Configuration) :-
    'universal?'(Binder),
    LowerBound > UpperBound,

    !,

    sub_binder(Binder, Binder_), 
    
    Cont = conf(Binder_, [state(Omega, S, H, C) | States]),

    (show -> write(Cont), write(' [U Success]'), nl ; true),

    '[[]]'(Cont, Final_Configuration).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Universal Success Propagate %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'[[]]'(conf(Binder, [success | States]), Final_Configuration) :-
    'universal?'(Binder),
    
    !,

    Cont = conf(Binder, States),

    (show -> write(Cont), write(' [U SuccessPropagate]'), nl; true),

    '[[]]'(Cont, Final_Configuration).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Universal Failure Propagate %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'[[]]'(conf(Binder, [failure, _Sigma | States]), Final_Configuration) :-
    'universal?'(Binder),

    !,

    sub_binder(Binder, Binder_),
   
    Cont = conf(Binder_, [failure | States]),

    (show -> write(Cont), write(' [U FailurePropagate]'), nl; true),
    
    '[[]]'(Cont, Final_Configuration).

%%%%%%%%%%%%
% Activate %
%%%%%%%%%%%%
'[[]]'(conf(Binder, [state([A|Omega],S,H,C) | States]), Final_Configuration) :-
    A \= false, A \= ':'(_,_), A \= '<E>'(_It, _L, _U, _E, _B), A \= '<V>'(__It, __L, __U, __E, __B),
    
    !,
    
    C_ is C + 1,
    Cont = conf(Binder, [state([':'(token(A,C),1)|Omega],[token(A,C)|S],H,C_) | States]),
    
   (show -> write(Cont), write(' [Activate]'), nl ; true),

    '[[]]'(Cont, Final_Configuration).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% (E/V-) Simplify  & (E/V-) Propagate %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
'[[]]'(conf(Binder, [state([':'(Token,O) |Omega], S, H, C) | States]), Final_Configuration) :-
    program(Programme),
    find(Type, O, Token, Programme, S, S_, Args),

    !,
    
    const_Cont(Type, Binder, Omega, S_, H, C, States, Args, Cont),
    
    (show -> write(Cont), write_tag(Type), nl ; true),
    
    '[[]]'(Cont, Final_Configuration).

%%%%%%%%%%%
% Failure %
%%%%%%%%%%%
'[[]]'(conf(Binder, [state([false | _Omega],_S,_H,_C) | States]), Final_Configuration) :-
    !,
    
    Cont = conf(Binder, [failure | States]),

    (show -> write(Cont), write(' [Failure]'), nl ; true),
    
    '[[]]'(Cont, Final_Configuration).

%%%%%%%%
% True %
%%%%%%%%
'[[]]'(conf(Binder, [state([true | Omega], S, H, C) | States]), Final_Configuration) :-
    !,
    
    Cont = conf(Binder, [state(Omega, S, H, C) | States]),

    (show -> write(Cont), write(' [True]'), nl ; true),
    
    '[[]]'(Cont, Final_Configuration).

%%%%%%%%%%%
% Success %
%%%%%%%%%%%
'[[]]'(conf(Binder, [state([], _S, _H, _C) | States]), Final_Configuration) :-
    !,

    Cont = conf(Binder, [success | States]),
    
    (show -> write(Cont), write(' [Success]'), nl ; true),
    
    '[[]]'(Cont, Final_Configuration).

%%%%%%%%
% Drop %
%%%%%%%%
'[[]]'(conf(Binder, [state([':'(_Token,_O) | Omega], S, H, C) | States]), Final_Configuration) :-
    !,
    
    Cont = conf(Binder, [state(Omega, S, H, C) | States]),
    
    (show -> write(Cont), write(' [Drop]'), nl ; true),
    
    '[[]]'(Cont, Final_Configuration).



'[[]]'(conf([], [failure]), _Final_Configuration) :- !, fail.


'[[]]'(Final_Configuration, Final_Configuration) :- write(Final_Configuration), nl.