package examples.unionfind;

import runtime.Logical;
import static util.arithmetics.primitives.intUtil.*;

public handler guf<E> {
	solver runtime.EqualitySolver<E>;

	public constraint make(+E), 
		union(+E, +E), find(+E, Logical<E> Result);

	private constraint root(+E Root, int Rank), 
		link(+E Root1, +E Root2),
		arrow(+E Node, +E Parent) infix '~>';

	rules {
		local Logical<E> R_x, R_y;
        
		make @ make(X) <=> root(X,0);

		union @ union(X, Y) <=> find(X, R_x), find(Y, R_y), link(R_x, R_y);

		// path compression with immediate update thanks to logical variable
		findNode @ X '~>' Parent_x, find(X, R) <=> find(Parent_x, R), X '~>' R;
		// return function result in second argument
		findRoot @ root(X, _) \ find(X, R) <=> R = X;     /* found */
		
		// root treatment
		linkEq   @ link(R, R) <=> true.
		linkLeft @ link(R_x, R_y), root(R_x, Rank_x), root(R_y, Rank_y) <=> 
			Rank_x >= Rank_y | R_y '~>' R_x, root(R_x, max(Rank_x, inc(Rank_y)));
		linkRight@ link(R_y, R_x), root(R_x, Rank_x), root(R_y, Rank_y) <=> 
			Rank_x >= Rank_y | R_y '~>' R_x, root(R_x, max(Rank_x, inc(Rank_y)));
	}
}