:- use_module(activation, [check_activation/0, check_activation/1]).
:- use_module(history, [not_in_history/3, add_to_history/3]).
:- use_module(lock, [lock/1, unlock/1]).
:- use_module(priority_queue, [insert/2]).
:- use_module(store,
	      [ make_ground/3,
		new_store/1,
		insert_in_store/4,
		store_lookup/3,
		delete_key/2,
		delete_first/2,
		select_by_id/4
	      ]).
:- use_module(id, [gen_id/1]).
:- use_module(library(lists)).

:- style_check(-singleton).

/*
    Suspension term layout for leq(X,Y):
    
    suspension(Id,State,History,X,Y,Back,Back_1,Back_2,Back_1_2)

    with Id the constraint identifier
         State = state(alive) or state(dead)
	 History = hash table representing part of the distributed propagation history
	 Back = backpointer for constant time removal from global index
	 Back_1 = backpointer for constant time removal from index on 1st argument
	 Back_2 = backpointer for constant time removal from index on 2nd argument
	 Back_1_2 = backpointer for constant time removal from index on combination of 1st and 2nd argument

    Constraint insertions and removals always check the backpointers to see if constraint was already inserted in some index:
    if so, the backpointer equals key(Key) or [_,Suspension|_] with Suspension the suspension of the constraint in question;
    otherwise the backpointer is a variable

*/

:- initialization 
	nb_setval('index(leq/2, [])', ht(4, 0, t(_, _, _, _))),
	nb_setval('index(leq/2, [2])', ht(4, 0, t(_, _, _, _))),
	nb_setval('index(leq/2, [1])', ht(4, 0, t(_, _, _, _))), 
	nb_setval('index(leq/2, [1, 2])', ht(4, 0, t(_, _, _, _))).

leq(B, C) :-
	gen_id(A),
	E=suspension(A, state(alive), ht(1, 0, t(_)), B, C, _, _, _, _),
	term_variables([B, C], D),
	'attach(leq/2)'(D, E),
	insert(1, 'occurrence(leq/2, 1, 1)'(E)).

user:attr_unify_hook(attr(H, B), A) :-
	(   var(A)
	->  (   get_attr(A, user, attr(F, C))
	    ->  sort(B, D),
		sort(C, E),
		merge_set(D, E, G),
		put_attr(A, user, attr(F, G)),
		'update_index(leq/2)'(B),
		'schedule(leq/2)'(B)
	    ;   put_attr(A, user, attr(H, B)),
		'schedule(leq/2)'(B)
	    )
	;   throw(unsupported)
	).

'schedule(leq/2)'([A|B]) :-
	insert(1, 'occurrence(leq/2, 1, 1)'(A)),
	'schedule(leq/2)'(B).
'schedule(leq/2)'([]).

'update_index(leq/2)'([A|R1]) :-
	A=suspension(_, _, _, B, C, P, _, _, D),
	make_ground(B, user, K),
	make_ground(C, user, L),
	(   nonvar(D)
	->  arg(9, A, E),
	    (	E=key(F)
	    ->  nb_getval('index(leq/2, [1, 2])', G),
		store_lookup(F, G, [_|H]),
		(   H=[]
		->  delete_key(F, G)
		;   H=[I|_],
		    setarg(9, I, key(F)),
		    delete_first(F, G)
		)
	    ;   E=[_, _|J],
		setarg(2, E, J),
		(   J=[I|_]
		->  setarg(9, I, E)
		;   true
		)
	    ),
	    nb_getval('index(leq/2, [1, 2])', M),
	    insert_in_store(A, a(K, L), M, N),
	    setarg(9, A, key(a(K, L))),
	    (   N=[_, O|_]
	    ->  setarg(9, O, N)
	    ;   true
	    ),
	    (   nonvar(P)
	    ->  arg(6, A, Q),
		(   Q=key(R)
		->  nb_getval('index(leq/2, [])', S),
		    store_lookup(R, S, [_|T]),
		    (   T=[]
		    ->  delete_key(R, S)
		    ;   T=[U|_],
			setarg(6, U, key(R)),
			delete_first(R, S)
		    )
		;   Q=[_, _|V],
		    setarg(2, Q, V),
		    (   V=[U|_]
		    ->  setarg(6, U, Q)
		    ;   true
		    )
		),
		arg(7, A, W),
		(   W=key(X)
		->  nb_getval('index(leq/2, [2])', Y),
		    store_lookup(X, Y, [_|Z]),
		    (   Z=[]
		    ->  delete_key(X, Y)
		    ;   Z=[A1|_],
			setarg(7, A1, key(X)),
			delete_first(X, Y)
		    )
		;   W=[_, _|B1],
		    setarg(2, W, B1),
		    (   B1=[A1|_]
		    ->  setarg(7, A1, W)
		    ;   true
		    )
		),
		arg(8, A, C1),
		(   C1=key(D1)
		->  nb_getval('index(leq/2, [1])', E1),
		    store_lookup(D1, E1, [_|F1]),
		    (   F1=[]
		    ->  delete_key(D1, E1)
		    ;   F1=[G1|_],
			setarg(8, G1, key(D1)),
			delete_first(D1, E1)
		    )
		;   C1=[_, _|H1],
		    setarg(2, C1, H1),
		    (   H1=[G1|_]
		    ->  setarg(8, G1, C1)
		    ;   true
		    )
		),
		nb_getval('index(leq/2, [])', I1),
		insert_in_store(A, a, I1, J1),
		setarg(6, A, key(a)),
		(   J1=[_, K1|_]
		->  setarg(6, K1, J1)
		;   true
		),
		nb_getval('index(leq/2, [2])', L1),
		insert_in_store(A, a(L), L1, M1),
		setarg(7, A, key(a(L))),
		(   M1=[_, N1|_]
		->  setarg(7, N1, M1)
		;   true
		),
		nb_getval('index(leq/2, [1])', O1),
		insert_in_store(A, a(K), O1, P1),
		setarg(8, A, key(a(K))),
		(   P1=[_, Q1|_]
		->  setarg(8, Q1, P1)
		;   true
		)
	    ;   true
	    )
	;   true
	),
	'update_index(leq/2)'(R1).
'update_index(leq/2)'([]).

'occurrence(leq/2, 2, 2)'(A) :-
	A=suspension(G, B, _, C, H, _, _, _, _),
	arg(1, B, alive),
	nb_getval('index(leq/2, [2])', E),
	make_ground(a(C), user, D),
	store_lookup(D, E, F),
	!,
	'occurrence(leq/2, 2, 2, 1)'(F, B, G, A, C, H).
'occurrence(leq/2, 2, 2)'(A) :-
	A=suspension(_, B, _, D, E, C, _, _, _),
	(   arg(1, B, alive),
	    var(C)
	->  make_ground(D, user, M),
	    make_ground(E, user, I),
	    nb_getval('index(leq/2, [])', F),
	    insert_in_store(A, a, F, G),
	    setarg(6, A, key(a)),
	    (   G=[_, H|_]
	    ->  setarg(6, H, G)
	    ;   true
	    ),
	    nb_getval('index(leq/2, [2])', J),
	    insert_in_store(A, a(I), J, K),
	    setarg(7, A, key(a(I))),
	    (   K=[_, L|_]
	    ->  setarg(7, L, K)
	    ;   true
	    ),
	    nb_getval('index(leq/2, [1])', N),
	    insert_in_store(A, a(M), N, O),
	    setarg(8, A, key(a(M))),
	    (   O=[_, P|_]
	    ->  setarg(8, P, O)
	    ;   true
	    )
	;   true
	).

'occurrence(leq/2, 2, 2, 1)'([A|R], Q, D, H, E, N) :-
	(   A=suspension(C, B, K, M, F, _, _, _, _),
	    arg(1, B, alive),
	    C\==D,
	    E==F,
	    G=t(4, C, D),
	    term_hash(G, J),
	    arg(3, H, I),
	    not_in_history(I, J, G),
	    not_in_history(K, J, G)
	->  add_to_history(K, J, G),
	    gen_id(L),
	    P=suspension(L, state(alive), ht(1, 0, t(_)), M, N, _, _, _, _),
	    term_variables([M, N], O),
	    'attach(leq/2)'(O, P),
	    'occurrence(leq/2, 1, 1)'(P),
	    check_activation(2),
	    (   arg(1, Q, alive)
	    ->  'occurrence(leq/2, 2, 2, 1)'(R, Q, D, H, E, N)
	    ;   true
	    )
	;   'occurrence(leq/2, 2, 2, 1)'(R, Q, D, H, E, N)
	).
'occurrence(leq/2, 2, 2, 1)'([], _, _, A, _, _) :-
	A=suspension(_, B, _, D, E, C, _, _, _),
	(   arg(1, B, alive),
	    var(C)
	->  make_ground(D, user, M),
	    make_ground(E, user, I),
	    nb_getval('index(leq/2, [])', F),
	    insert_in_store(A, a, F, G),
	    setarg(6, A, key(a)),
	    (   G=[_, H|_]
	    ->  setarg(6, H, G)
	    ;   true
	    ),
	    nb_getval('index(leq/2, [2])', J),
	    insert_in_store(A, a(I), J, K),
	    setarg(7, A, key(a(I))),
	    (   K=[_, L|_]
	    ->  setarg(7, L, K)
	    ;   true
	    ),
	    nb_getval('index(leq/2, [1])', N),
	    insert_in_store(A, a(M), N, O),
	    setarg(8, A, key(a(M))),
	    (   O=[_, P|_]
	    ->  setarg(8, P, O)
	    ;   true
	    )
	;   true
	).

'occurrence(leq/2, 2, 1)'(A) :-
	(   A=suspension(G, B, _, H, C, _, _, _, _),
	arg(1, B, alive),
	nb_getval('index(leq/2, [1])', E),
	make_ground(a(C), user, D),
	store_lookup(D, E, F)
	), !,
	'occurrence(leq/2, 2, 1, 1)'(F, B, G, A, H, C).
'occurrence(leq/2, 2, 1)'(A) :-
	'occurrence(leq/2, 2, 2)'(A).

'occurrence(leq/2, 2, 1, 1)'([A|R], Q, D, H, M, E) :-
	(   A=suspension(C, B, K, F, N, _, _, _, _),
	    arg(1, B, alive),
	    C\==D,
	    E==F,
	    G=t(4, D, C),
	    term_hash(G, J),
	    arg(3, H, I),
	    not_in_history(I, J, G),
	    not_in_history(K, J, G)
	->  add_to_history(K, J, G),
	    gen_id(L),
	    P=suspension(L, state(alive), ht(1, 0, t(_)), M, N, _, _, _, _),
	    term_variables([M, N], O),
	    'attach(leq/2)'(O, P),
	    'occurrence(leq/2, 1, 1)'(P),
	    check_activation(2),
	    (   arg(1, Q, alive)
	    ->  'occurrence(leq/2, 2, 1, 1)'(R, Q, D, H, M, E)
	    ;   true
	    )
	;   'occurrence(leq/2, 2, 1, 1)'(R, Q, D, H, M, E)
	).
'occurrence(leq/2, 2, 1, 1)'([], _, _, A, _, _) :-
	'occurrence(leq/2, 2, 2)'(A).

'occurrence(leq/2, 1, 5)'(A) :-
	A=suspension(H, B, _, C, D, _, _, _, _),
	arg(1, B, alive),
	nb_getval('index(leq/2, [1, 2])', F),
	make_ground(a(C, D), user, E),
	store_lookup(E, F, G),
	!,
	'occurrence(leq/2, 1, 5, 1)'(G, B, H, A, C, D).
'occurrence(leq/2, 1, 5)'(A) :-
	A=suspension(_, B, _, D, E, _, _, _, C),
	(   arg(1, B, alive),
	    var(C)
	->  make_ground(D, user, F),
	    make_ground(E, user, G),
	    nb_getval('index(leq/2, [1, 2])', H),
	    insert_in_store(A, a(F, G), H, I),
	    setarg(9, A, key(a(F, G))),
	    (   I=[_, J|_]
	    ->  setarg(9, J, I)
	    ;   true
	    )
	;   true
	),
	insert(2, 'occurrence(leq/2, 2, 1)'(A)).

'occurrence(leq/2, 1, 5, 1)'([A|K1], J1, D, L1, E, G) :-
	(   A=suspension(C, B, _, F, H, _, _, _, _),
	    arg(1, B, alive),
	    C\==D,
	    E==F,
	    G==H
	->  setarg(1, B, dead),
	    (   arg(9, A, I),
		nonvar(I)
	    ->  arg(9, A, J),
		(   J=key(K)
		->  nb_getval('index(leq/2, [1, 2])', L),
		    store_lookup(K, L, [_|M]),
		    (   M=[]
		    ->  delete_key(K, L)
		    ;   M=[N|_],
			setarg(9, N, key(K)),
			delete_first(K, L)
		    )
		;   J=[_, _|O],
		    setarg(2, J, O),
		    (   O=[N|_]
		    ->  setarg(9, N, J)
		    ;   true
		    )
		),
		(   arg(6, A, P),
		    nonvar(P)
		->  arg(6, A, Q),
		    (   Q=key(R)
		    ->  nb_getval('index(leq/2, [])', S),
			store_lookup(R, S, [_|T]),
			(   T=[]
			->  delete_key(R, S)
			;   T=[U|_],
			    setarg(6, U, key(R)),
			    delete_first(R, S)
			)
		    ;   Q=[_, _|V],
			setarg(2, Q, V),
			(   V=[U|_]
			->  setarg(6, U, Q)
			;   true
			)
		    ),
		    arg(7, A, W),
		    (   W=key(X)
		    ->  nb_getval('index(leq/2, [2])', Y),
			store_lookup(X, Y, [_|Z]),
			(   Z=[]
			->  delete_key(X, Y)
			;   Z=[A1|_],
			    setarg(7, A1, key(X)),
			    delete_first(X, Y)
			)
		    ;   W=[_, _|B1],
			setarg(2, W, B1),
			(   B1=[A1|_]
			->  setarg(7, A1, W)
			;   true
			)
		    ),
		    arg(8, A, C1),
		    (   C1=key(D1)
		    ->  nb_getval('index(leq/2, [1])', E1),
			store_lookup(D1, E1, [_|F1]),
			(   F1=[]
			->  delete_key(D1, E1)
			;   F1=[G1|_],
			    setarg(8, G1, key(D1)),
			    delete_first(D1, E1)
			)
		    ;   C1=[_, _|H1],
			setarg(2, C1, H1),
			(   H1=[G1|_]
			->  setarg(8, G1, C1)
			;   true
			)
		    )
		;   true
		)
	    ;   true
	    ),
	    term_variables([E, G], I1),
	    'detach(leq/2)'(I1, A),
	    (   arg(1, J1, alive)
	    ->  'occurrence(leq/2, 1, 5, 1)'(K1, J1, D, L1, E, G)
	    ;   true
	    )
	;   'occurrence(leq/2, 1, 5, 1)'(K1, J1, D, L1, E, G)
	).
'occurrence(leq/2, 1, 5, 1)'([], _, _, A, _, _) :-
	A=suspension(_, B, _, D, E, _, _, _, C),
	(   arg(1, B, alive),
	    var(C)
	->  make_ground(D, user, F),
	    make_ground(E, user, G),
	    nb_getval('index(leq/2, [1, 2])', H),
	    insert_in_store(A, a(F, G), H, I),
	    setarg(9, A, key(a(F, G))),
	    (   I=[_, J|_]
	    ->  setarg(9, J, I)
	    ;   true
	    )
	;   true
	),
	insert(2, 'occurrence(leq/2, 2, 1)'(A)).

'occurrence(leq/2, 1, 4)'(A) :-
	A=suspension(H, B, _, C, D, _, _, _, _),
	arg(1, B, alive),
	nb_getval('index(leq/2, [1, 2])', F),
	make_ground(a(C, D), user, E),
	store_lookup(E, F, G),
	!,
	'occurrence(leq/2, 1, 4, 1)'(G, B, H, A, C, D).
'occurrence(leq/2, 1, 4)'(A) :-
	'occurrence(leq/2, 1, 5)'(A).

'occurrence(leq/2, 1, 4, 1)'([A|L1], I, D, J, E, G) :-
	(   A=suspension(C, B, _, F, H, _, _, _, _),
	    arg(1, B, alive),
	    C\==D,
	    E==F,
	    G==H
	->  setarg(1, I, dead),
	    (   arg(9, J, K),
		nonvar(K)
	    ->  arg(9, J, L),
		(   L=key(M)
		->  nb_getval('index(leq/2, [1, 2])', N),
		    store_lookup(M, N, [_|O]),
		    (   O=[]
		    ->  delete_key(M, N)
		    ;   O=[P|_],
			setarg(9, P, key(M)),
			delete_first(M, N)
		    )
		;   L=[_, _|Q],
		    setarg(2, L, Q),
		    (   Q=[P|_]
		    ->  setarg(9, P, L)
		    ;   true
		    )
		),
		(   arg(6, J, R),
		    nonvar(R)
		->  arg(6, J, S),
		    (   S=key(T)
		    ->  nb_getval('index(leq/2, [])', U),
			store_lookup(T, U, [_|V]),
			(   V=[]
			->  delete_key(T, U)
			;   V=[W|_],
			    setarg(6, W, key(T)),
			    delete_first(T, U)
			)
		    ;   S=[_, _|X],
			setarg(2, S, X),
			(   X=[W|_]
			->  setarg(6, W, S)
			;   true
			)
		    ),
		    arg(7, J, Y),
		    (   Y=key(Z)
		    ->  nb_getval('index(leq/2, [2])', A1),
			store_lookup(Z, A1, [_|B1]),
			(   B1=[]
			->  delete_key(Z, A1)
			;   B1=[C1|_],
			    setarg(7, C1, key(Z)),
			    delete_first(Z, A1)
			)
		    ;   Y=[_, _|D1],
			setarg(2, Y, D1),
			(   D1=[C1|_]
			->  setarg(7, C1, Y)
			;   true
			)
		    ),
		    arg(8, J, E1),
		    (   E1=key(F1)
		    ->  nb_getval('index(leq/2, [1])', G1),
			store_lookup(F1, G1, [_|H1]),
			(   H1=[]
			->  delete_key(F1, G1)
			;   H1=[I1|_],
			    setarg(8, I1, key(F1)),
			    delete_first(F1, G1)
			)
		    ;   E1=[_, _|J1],
			setarg(2, E1, J1),
			(   J1=[I1|_]
			->  setarg(8, I1, E1)
			;   true
			)
		    )
		;   true
		)
	    ;   true
	    ),
	    term_variables([E, G], K1),
	    'detach(leq/2)'(K1, J)
	;   'occurrence(leq/2, 1, 4, 1)'(L1, I, D, J, E, G)
	).
'occurrence(leq/2, 1, 4, 1)'([], _, _, A, _, _) :-
	'occurrence(leq/2, 1, 5)'(A).

'occurrence(leq/2, 1, 3)'(A) :-
	A=suspension(H, B, _, D, C, _, _, _, _),
	arg(1, B, alive),
	nb_getval('index(leq/2, [1, 2])', F),
	make_ground(a(C, D), user, E),
	store_lookup(E, F, G),
	!,
	'occurrence(leq/2, 1, 3, 1)'(G, B, H, A, D, C).
'occurrence(leq/2, 1, 3)'(A) :-
	'occurrence(leq/2, 1, 4)'(A).

'occurrence(leq/2, 1, 3, 1)'([A|M2], I, D, J, G, E) :-
	(   A=suspension(C, B, _, F, H, _, _, _, _),
	    arg(1, B, alive),
	    C\==D,
	    E==F,
	    G==H
	->  setarg(1, I, dead),
	    (   arg(9, J, K),
		nonvar(K)
	    ->  arg(9, J, L),
		(   L=key(M)
		->  nb_getval('index(leq/2, [1, 2])', N),
		    store_lookup(M, N, [_|O]),
		    (   O=[]
		    ->  delete_key(M, N)
		    ;   O=[P|_],
			setarg(9, P, key(M)),
			delete_first(M, N)
		    )
		;   L=[_, _|Q],
		    setarg(2, L, Q),
		    (   Q=[P|_]
		    ->  setarg(9, P, L)
		    ;   true
		    )
		),
		(   arg(6, J, R),
		    nonvar(R)
		->  arg(6, J, S),
		    (   S=key(T)
		    ->  nb_getval('index(leq/2, [])', U),
			store_lookup(T, U, [_|V]),
			(   V=[]
			->  delete_key(T, U)
			;   V=[W|_],
			    setarg(6, W, key(T)),
			    delete_first(T, U)
			)
		    ;   S=[_, _|X],
			setarg(2, S, X),
			(   X=[W|_]
			->  setarg(6, W, S)
			;   true
			)
		    ),
		    arg(7, J, Y),
		    (   Y=key(Z)
		    ->  nb_getval('index(leq/2, [2])', A1),
			store_lookup(Z, A1, [_|B1]),
			(   B1=[]
			->  delete_key(Z, A1)
			;   B1=[C1|_],
			    setarg(7, C1, key(Z)),
			    delete_first(Z, A1)
			)
		    ;   Y=[_, _|D1],
			setarg(2, Y, D1),
			(   D1=[C1|_]
			->  setarg(7, C1, Y)
			;   true
			)
		    ),
		    arg(8, J, E1),
		    (   E1=key(F1)
		    ->  nb_getval('index(leq/2, [1])', G1),
			store_lookup(F1, G1, [_|H1]),
			(   H1=[]
			->  delete_key(F1, G1)
			;   H1=[I1|_],
			    setarg(8, I1, key(F1)),
			    delete_first(F1, G1)
			)
		    ;   E1=[_, _|J1],
			setarg(2, E1, J1),
			(   J1=[I1|_]
			->  setarg(8, I1, E1)
			;   true
			)
		    )
		;   true
		)
	    ;   true
	    ),
	    term_variables([G, E], K1),
	    'detach(leq/2)'(K1, J),
	    setarg(1, B, dead),
	    (   arg(9, A, L1),
		nonvar(L1)
	    ->  arg(9, A, M1),
		(   M1=key(N1)
		->  nb_getval('index(leq/2, [1, 2])', O1),
		    store_lookup(N1, O1, [_|P1]),
		    (   P1=[]
		    ->  delete_key(N1, O1)
		    ;   P1=[Q1|_],
			setarg(9, Q1, key(N1)),
			delete_first(N1, O1)
		    )
		;   M1=[_, _|R1],
		    setarg(2, M1, R1),
		    (   R1=[Q1|_]
		    ->  setarg(9, Q1, M1)
		    ;   true
		    )
		),
		(   arg(6, A, S1),
		    nonvar(S1)
		->  arg(6, A, T1),
		    (   T1=key(U1)
		    ->  nb_getval('index(leq/2, [])', V1),
			store_lookup(U1, V1, [_|W1]),
			(   W1=[]
			->  delete_key(U1, V1)
			;   W1=[X1|_],
			    setarg(6, X1, key(U1)),
			    delete_first(U1, V1)
			)
		    ;   T1=[_, _|Y1],
			setarg(2, T1, Y1),
			(   Y1=[X1|_]
			->  setarg(6, X1, T1)
			;   true
			)
		    ),
		    arg(7, A, Z1),
		    (   Z1=key(A2)
		    ->  nb_getval('index(leq/2, [2])', B2),
			store_lookup(A2, B2, [_|C2]),
			(   C2=[]
			->  delete_key(A2, B2)
			;   C2=[D2|_],
			    setarg(7, D2, key(A2)),
			    delete_first(A2, B2)
			)
		    ;   Z1=[_, _|E2],
			setarg(2, Z1, E2),
			(   E2=[D2|_]
			->  setarg(7, D2, Z1)
			;   true
			)
		    ),
		    arg(8, A, F2),
		    (   F2=key(G2)
		    ->  nb_getval('index(leq/2, [1])', H2),
			store_lookup(G2, H2, [_|I2]),
			(   I2=[]
			->  delete_key(G2, H2)
			;   I2=[J2|_],
			    setarg(8, J2, key(G2)),
			    delete_first(G2, H2)
			)
		    ;   F2=[_, _|K2],
			setarg(2, F2, K2),
			(   K2=[J2|_]
			->  setarg(8, J2, F2)
			;   true
			)
		    )
		;   true
		)
	    ;   true
	    ),
	    term_variables([E, G], L2),
	    'detach(leq/2)'(L2, A),
	    E=G
	;   'occurrence(leq/2, 1, 3, 1)'(M2, I, D, J, G, E)
	).
'occurrence(leq/2, 1, 3, 1)'([], _, _, A, _, _) :-
	'occurrence(leq/2, 1, 4)'(A).

'occurrence(leq/2, 1, 2)'(A) :-
	A=suspension(H, B, _, D, C, _, _, _, _),
	arg(1, B, alive),
	nb_getval('index(leq/2, [1, 2])', F),
	make_ground(a(C, D), user, E),
	store_lookup(E, F, G),
	!,
	'occurrence(leq/2, 1, 2, 1)'(G, B, H, A, D, C).
'occurrence(leq/2, 1, 2)'(A) :-
	'occurrence(leq/2, 1, 3)'(A).

'occurrence(leq/2, 1, 2, 1)'([A|M2], I, D, J, G, E) :-
	(   A=suspension(C, B, _, F, H, _, _, _, _),
	    arg(1, B, alive),
	    C\==D,
	    E==F,
	    G==H
	->  setarg(1, I, dead),
	    (   arg(9, J, K),
		nonvar(K)
	    ->  arg(9, J, L),
		(   L=key(M)
		->  nb_getval('index(leq/2, [1, 2])', N),
		    store_lookup(M, N, [_|O]),
		    (   O=[]
		    ->  delete_key(M, N)
		    ;   O=[P|_],
			setarg(9, P, key(M)),
			delete_first(M, N)
		    )
		;   L=[_, _|Q],
		    setarg(2, L, Q),
		    (   Q=[P|_]
		    ->  setarg(9, P, L)
		    ;   true
		    )
		),
		(   arg(6, J, R),
		    nonvar(R)
		->  arg(6, J, S),
		    (   S=key(T)
		    ->  nb_getval('index(leq/2, [])', U),
			store_lookup(T, U, [_|V]),
			(   V=[]
			->  delete_key(T, U)
			;   V=[W|_],
			    setarg(6, W, key(T)),
			    delete_first(T, U)
			)
		    ;   S=[_, _|X],
			setarg(2, S, X),
			(   X=[W|_]
			->  setarg(6, W, S)
			;   true
			)
		    ),
		    arg(7, J, Y),
		    (   Y=key(Z)
		    ->  nb_getval('index(leq/2, [2])', A1),
			store_lookup(Z, A1, [_|B1]),
			(   B1=[]
			->  delete_key(Z, A1)
			;   B1=[C1|_],
			    setarg(7, C1, key(Z)),
			    delete_first(Z, A1)
			)
		    ;   Y=[_, _|D1],
			setarg(2, Y, D1),
			(   D1=[C1|_]
			->  setarg(7, C1, Y)
			;   true
			)
		    ),
		    arg(8, J, E1),
		    (   E1=key(F1)
		    ->  nb_getval('index(leq/2, [1])', G1),
			store_lookup(F1, G1, [_|H1]),
			(   H1=[]
			->  delete_key(F1, G1)
			;   H1=[I1|_],
			    setarg(8, I1, key(F1)),
			    delete_first(F1, G1)
			)
		    ;   E1=[_, _|J1],
			setarg(2, E1, J1),
			(   J1=[I1|_]
			->  setarg(8, I1, E1)
			;   true
			)
		    )
		;   true
		)
	    ;   true
	    ),
	    term_variables([G, E], K1),
	    'detach(leq/2)'(K1, J),
	    setarg(1, B, dead),
	    (   arg(9, A, L1),
		nonvar(L1)
	    ->  arg(9, A, M1),
		(   M1=key(N1)
		->  nb_getval('index(leq/2, [1, 2])', O1),
		    store_lookup(N1, O1, [_|P1]),
		    (   P1=[]
		    ->  delete_key(N1, O1)
		    ;   P1=[Q1|_],
			setarg(9, Q1, key(N1)),
			delete_first(N1, O1)
		    )
		;   M1=[_, _|R1],
		    setarg(2, M1, R1),
		    (   R1=[Q1|_]
		    ->  setarg(9, Q1, M1)
		    ;   true
		    )
		),
		(   arg(6, A, S1),
		    nonvar(S1)
		->  arg(6, A, T1),
		    (   T1=key(U1)
		    ->  nb_getval('index(leq/2, [])', V1),
			store_lookup(U1, V1, [_|W1]),
			(   W1=[]
			->  delete_key(U1, V1)
			;   W1=[X1|_],
			    setarg(6, X1, key(U1)),
			    delete_first(U1, V1)
			)
		    ;   T1=[_, _|Y1],
			setarg(2, T1, Y1),
			(   Y1=[X1|_]
			->  setarg(6, X1, T1)
			;   true
			)
		    ),
		    arg(7, A, Z1),
		    (   Z1=key(A2)
		    ->  nb_getval('index(leq/2, [2])', B2),
			store_lookup(A2, B2, [_|C2]),
			(   C2=[]
			->  delete_key(A2, B2)
			;   C2=[D2|_],
			    setarg(7, D2, key(A2)),
			    delete_first(A2, B2)
			)
		    ;   Z1=[_, _|E2],
			setarg(2, Z1, E2),
			(   E2=[D2|_]
			->  setarg(7, D2, Z1)
			;   true
			)
		    ),
		    arg(8, A, F2),
		    (   F2=key(G2)
		    ->  nb_getval('index(leq/2, [1])', H2),
			store_lookup(G2, H2, [_|I2]),
			(   I2=[]
			->  delete_key(G2, H2)
			;   I2=[J2|_],
			    setarg(8, J2, key(G2)),
			    delete_first(G2, H2)
			)
		    ;   F2=[_, _|K2],
			setarg(2, F2, K2),
			(   K2=[J2|_]
			->  setarg(8, J2, F2)
			;   true
			)
		    )
		;   true
		)
	    ;   true
	    ),
	    term_variables([E, G], L2),
	    'detach(leq/2)'(L2, A),
	    G=E
	;   'occurrence(leq/2, 1, 2, 1)'(M2, I, D, J, G, E)
	).
'occurrence(leq/2, 1, 2, 1)'([], _, _, A, _, _) :-
	'occurrence(leq/2, 1, 3)'(A).

'occurrence(leq/2, 1, 1)'(A) :-
	A=suspension(_, B, _, C, D, _, _, _, _),
	arg(1, B, alive),
	C==D,
	!,
	setarg(1, B, dead),
	(   arg(9, A, E),
	    nonvar(E)
	->  arg(9, A, F),
	    (   F=key(G)
	    ->  nb_getval('index(leq/2, [1, 2])', H),
		store_lookup(G, H, [_|I]),
		(   I=[]
		->  delete_key(G, H)
		;   I=[J|_],
		    setarg(9, J, key(G)),
		    delete_first(G, H)
		)
	    ;   F=[_, _|K],
		setarg(2, F, K),
		(   K=[J|_]
		->  setarg(9, J, F)
		;   true
		)
	    ),
	    (   arg(6, A, L),
		nonvar(L)
	    ->  arg(6, A, M),
		(   M=key(N)
		->  nb_getval('index(leq/2, [])', O),
		    store_lookup(N, O, [_|P]),
		    (   P=[]
		    ->  delete_key(N, O)
		    ;   P=[Q|_],
			setarg(6, Q, key(N)),
			delete_first(N, O)
		    )
		;   M=[_, _|R],
		    setarg(2, M, R),
		    (   R=[Q|_]
		    ->  setarg(6, Q, M)
		    ;   true
		    )
		),
		arg(7, A, S),
		(   S=key(T)
		->  nb_getval('index(leq/2, [2])', U),
		    store_lookup(T, U, [_|V]),
		    (   V=[]
		    ->  delete_key(T, U)
		    ;   V=[W|_],
			setarg(7, W, key(T)),
			delete_first(T, U)
		    )
		;   S=[_, _|X],
		    setarg(2, S, X),
		    (   X=[W|_]
		    ->  setarg(7, W, S)
		    ;   true
		    )
		),
		arg(8, A, Y),
		(   Y=key(Z)
		->  nb_getval('index(leq/2, [1])', A1),
		    store_lookup(Z, A1, [_|B1]),
		    (   B1=[]
		    ->  delete_key(Z, A1)
		    ;   B1=[C1|_],
			setarg(8, C1, key(Z)),
			delete_first(Z, A1)
		    )
		;   Y=[_, _|D1],
		    setarg(2, Y, D1),
		    (   D1=[C1|_]
		    ->  setarg(8, C1, Y)
		    ;   true
		    )
		)
	    ;   true
	    )
	;   true
	),
	term_variables([C, C], E1),
	'detach(leq/2)'(E1, A).
'occurrence(leq/2, 1, 1)'(A) :-
	'occurrence(leq/2, 1, 2)'(A).

'attach(leq/2)'([A|F], C) :-
	(   get_attr(A, user, B)
	->  arg(2, B, D),
	    setarg(2, B, [C|D])
	;   gen_id(E),
	    put_attr(A, user, attr(E, [C]))
	),
	'attach(leq/2)'(F, C).
'attach(leq/2)'([], _).

'detach(leq/2)'([A|G], C) :-
	get_attr(A, user, B),
	arg(2, B, D),
	arg(1, C, E),
	select_by_id(D, E, 1, F),
	setarg(2, B, F),
	'detach(leq/2)'(G, C).
'detach(leq/2)'([], _).

show_store :-
	nb_getval('index(leq/2, [])', A),
	(   store_lookup(a, A, B)
	->  forall(member(suspension(_, _, _, C, D, _, _, _, _), B), writeln(leq(C, D)))
	;   true
	).
