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

% Type = propagate or simplify

find(Type, O, Token, [Rule | _Programme], S, S__, Args) :- 
    Token = token(A, _I),
    this_one(Type,O, A, Rule, K, D, Guard, Args),
    ((Type = simplify ; Type = e_simplify ; Type = u_simplify) -> delete(S, Token, S_) ; S_ = S),
    mapmember_store(K, S_),
    mapdelete_store(D, S_, S__),
    call(Guard), !.
find(Type, O, Token, [Rule | Programme], S, S_, Args) :-
    Token = token(A, _I),
    next_one(O, O_, A, Rule),
    find(Type, O_, Token, Programme, S, S_, Args).

write_tag(simplify) :- write(' [Simplify]').
write_tag(propagate) :- write(' [Propagate]').
write_tag(e_simplify) :- write(' [E Simplify]').
write_tag(e_propagate) :- write(' [E propagate]').
write_tag(u_simplify) :- write(' [U Simplify]').
write_tag(u_propagate) :- write(' [U Propagate]').

const_Cont(Type, Binder, Omega, S, H, C, States, arg(B), Cont) :-
    (Type = simplify ; Type = propagate),
    !,
    append(B, Omega, BOmega),
    Cont = conf(Binder, [state(BOmega, S, H, C) | States]).
    
const_Cont(Type, Binder, Omega, S, H, C, States, arg(It, LowerBound, UpperBound, E, B), Cont) :-
    (Type = e_simplify ; Type = e_propagate),
    !,
    append(Binder, [e], Binder_),
    
    Cont = conf(Binder_, [state(['<E>'(It, LowerBound, UpperBound, E, B) | Omega], S, H, C) | States]).

const_Cont(Type, Binder, Omega, S, H, C, States, arg(It, LowerBound, UpperBound, E, B), Cont) :-
    (Type = u_simplify ; Type = u_propagate),
    !,
    append(Binder, [u], Binder_),

    Cont = conf(Binder_, [state(['<V>'(It, LowerBound, UpperBound, E, B) | Omega], S, H, C) | States]).

this_one_rec(1, A, D_1, [A | D_2], D_1_2) :-
    !,
    append(D_1, D_2, D_1_2).
this_one_rec(O, A, D_1, [A_ | D_2], D_1_2) :-
    O > 1,
    \+(A \= A_),
    !,
    O_ is O - 1,
    append(D_1, [A_], D_1_A),
    this_one_rec(O_, A, D_1_A, D_2, D_1_2).
this_one_rec(O, A, D_1, [A_ | D_2], D_1_2) :-
    !,
    append(D_1, [A_], D_1_A_),
    this_one_rec(O, A, D_1_A_, D_2, D_1_2). 


next_one(O, O_, A, '<=>'(K, D, _G, _B)) :-
    next_one_rec(O, O_, A, K, D).

next_one(O, O_, A, '<=>'(D, _G, _B)) :-
    next_one_rec(O, O_, A, D).

next_one(O, O_, A, '==>'(K, _G, _B)) :-
    next_one_rec(O, O_, A, K).

next_one(O, O_, A, '<V>'(K, D, _, _G, _B)) :-
    next_one_rec(O, O_, A, K, D).

next_one(O, O_, A, '<V>'(D, _, _G, _B)) :-
    next_one_rec(O, O_, A, D).

next_one(O, O_, A, '=V>'(K, _, _G, _B)) :-
    next_one_rec(O, O_, A, K).

next_one(O, O_, A, '<E>'(K, D, _, _G, _B)) :-
    next_one_rec(O, O_, A, K, D).

next_one(O, O_, A, '<E>'(D, _, _G, _B)) :-
    next_one_rec(O, O_, A, D).

next_one(O, O_, A, '=E>'(K, _, _G, _B)) :-
    next_one_rec(O, O_, A, K).

next_one_rec(O, O_, A, [A_ | K], D) :-
    O > 1,
    \+(A \= A_),
    !,
    O__ is O - 1,
    next_one_rec(O__, O_, A, K, D).
next_one_rec(O, O_, A, [_A_ | K], D) :-
    !,
    next_one_rec(O, O_, A, K, D).
next_one_rec(O, O_, A, [], D) :-
    next_one_rec(O, O_, A, D).

next_one_rec(O, O, _A, []).
next_one_rec(O, O_, A, [A_ | D]) :-
    O > 1,
    \+(A \= A_),
    !,
    O__ is O - 1,
    next_one_rec(O__, O_, A, D).
next_one_rec(O, O_, A, [_A_ | D]) :-
    next_one_rec(O, O_, A, D).

mapmember_store([], _).
mapmember_store([A | L], S) :-
    memberchk(token(A, _), S),
    mapmember_store(L, S).


mapdelete_store([], S, S).
mapdelete_store([A | L], SI, SO) :-
    mydelete(SI, A, S_),
    mapdelete_store(L, S_, SO).

mydelete([T | S], A, S) :-
    token(A,_) = T, !.
mydelete([T | S], A, [T | S_]) :-
    mydelete(S, A, S_).


this_one(simplify,O, A, '<=>'(K, D, G, B), K, D_1_2, G, arg(B)) :-
    next_one_rec(O, O_, A, K),
    this_one_rec(O_, A, [], D, D_1_2). 

this_one(simplify,O, A, '<=>'(D, G, B), [], D_1_2, G, arg(B)) :-
    this_one_rec(O, A, [], D, D_1_2). 


this_one(e_simplify,O, A, '<E>'(K, D, [It, L, U, E], G, B), K, D_1_2, G, arg(It, L, U, E, B)) :-
    next_one_rec(O, O_, A, K),
    this_one_rec(O_, A, [], D, D_1_2). 

this_one(e_simplify,O, A, '<E>'(D, [It, L, U, E], G, B), [], D_1_2, G, arg(It, L, U, E, B)) :-
    this_one_rec(O, A, [], D, D_1_2). 

this_one(u_simplify,O, A, '<V>'(K, D, [It, L, U, E], G, B), K, D_1_2, G, arg(It, L, U, E, B)) :-
    next_one_rec(O, O_, A, K),
    this_one_rec(O_, A, [], D, D_1_2). 

this_one(u_simplify,O, A, '<V>'(D, [It, L, U, E], G, B), [], D_1_2, G, arg(It, L, U, E, B)) :-
    this_one_rec(O, A, [], D, D_1_2). 

this_one(propagate,O, A, '<=>'(K, D, G, B), K_1_2, D, G, arg(B)) :-
    this_one_rec(O, A, [], K, K_1_2).

this_one(propagate,O, A, '==>'(K, G, B), K_1_2, [], G, arg(B)) :-
    this_one_rec(O, A, [], K, K_1_2). 


this_one(e_propagate,O, A, '<E>'(K, D, [It, L, U, E], G, B), K_1_2, D, G, arg(It, L, U, E, B)) :-
    this_one_rec(O, A, [], K, K_1_2).

this_one(e_propagate,O, A, '=E>'(K, [It, L, U, E], G, B), K_1_2, [], G, arg(It, L, U, E, B)) :-
    this_one_rec(O, A, [], K, K_1_2). 

this_one(u_propagate,O, A, '<V>'(K, D, [It, L, U, E], G, B), K_1_2, D, G, arg(It, L, U, E, B)) :-
    this_one_rec(O, A, [], K, K_1_2).

this_one(u_propagate,O, A, '=V>'(K, [It, L, U, E], G, B), K_1_2, [], G, arg(It, L, U, E, B)) :-
    this_one_rec(O, A, [], K, K_1_2). 


'existential?'(Binder) :-
    append(_, [e], Binder).

'universal?'(Binder) :-
    append(_, [u], Binder).

sub_binder(Binder, Binder_) :-
    append(Binder_, [_], Binder).