/* Testing infrastructure */ 

sel interval: int * int -> [int]; // interval function: interval (m, n) provides the numbers m, ..., n-1

op valueMoreAbstractThan (a: AbsDom, b:AbsDom): bool :=
	match (a, b) with 
	| (@T, _) => true
	| (@V(x), @V(y)) => x = y
	| _ => false; 

// Checks whether there exists a position where the two stacks disagree
op stackInequalExists{!size: int}(sa: array<AbsDom>, sb: array<AbsDom>): bool := 
	for (!i: int) in interval(0,!size): || ((select sa !i) != (select sb !i));

// Checks whether the stacks agree at all positions
op stackEqualForall{!size: int}(sa: array<AbsDom>, sb: array<AbsDom>): bool := 
	for (!i: int) in interval(0,!size): && ((select sa !i) = (select sb !i));

// Checks that the first stack is more abstract than the second one at all positions
op stackMoreAbstractThanForall{!size: int}(sa: array<AbsDom>, sb: array<AbsDom>): bool := 
	for (!i: int) in interval(0,!size): && (valueMoreAbstractThan(select sa !i, select sb !i));

// Update representation for AbsDom arrays. Used for easily checking against a sequence of probing points in memory or storage
datatype Update := @UP<int*AbsDom>; 
datatype UpdateList := @UPLIST<int*array<Update>>;

const UPDATEDUMMY := @UP(0, @T);
const UPDATELISTDUMMY := @UPLIST(0, [UPDATEDUMMY]);

op addUpdate(updates: UpdateList, up: Update): UpdateList := 
	match updates with 
	| @UPLIST(size,  ups) => @UPLIST(size + 1, store ups size up)
	| _ => UPDATELISTDUMMY;

// Checks whether the array sa agrees with all updates of the Update array sb
op arrayEqual{!size:int} (sa: array<AbsDom>, sb: array<Update>): bool := 
	for (!i:int) in interval(0, !size): &&
		(match (select sb !i) with 
		| @UP(p, v) => (select sa p) = v
		| _ => false)
	;

// Checks whether the array sa is at all update points more concrete than the updates in sb
op arrayMoreAbstractThan{!size:int} (sa: array<AbsDom>, sb: array<Update>): bool := 
	for (!i:int) in interval(0, !size): &&
		(match (select sb !i) with 
		| @UP(p, v) => valueMoreAbstractThan(select sa p, v)
		| _ => false)
	;

// Checks whether array sa disagrees on one of the  update points with the updates in sb
op arrayInequalExists{!size:int} (sa: array<AbsDom>, sb: array<Update>): bool := 
	for (!i:int) in interval(0, !size): ||
		(match (select sb !i) with 
		| @UP(p, v) => (select sa p) != v
		| _ => false)
	;

// Configurations that we use for testing. Consist of the stack size, the stack array, and update lists for memory and storage (to probe at the specified points)
datatype Config := @C<int*array<AbsDom>*UpdateList*UpdateList>;

op getStackSize(conf: Config): int := 
	match conf with
	| @C(size, sa, mem, stor) => size
	| _ => 0;

op getStackArray(conf: Config): array<AbsDom> := 
	match conf with
	| @C(size, sa, mem, stor) => sa
	| _ => [@T];

op getMemUpdateList(conf: Config): UpdateList := 
	match conf with
	| @C(size, sa, mem, stor) => mem
	| _ => UPDATELISTDUMMY;

op getStorUpdateList(conf: Config): UpdateList := 
	match conf with
	| @C(size, sa, mem, stor) => stor
	| _ => UPDATELISTDUMMY;

op getUpdateSize(ul: UpdateList): int := 
	match ul with 
	| @UPLIST(s, ua) => s
	| _ => 0;

op getUpdates(ul: UpdateList): array<Update> := 
	match ul with
	| @UPLIST(s, ua) => ua
	| _ => [UPDATEDUMMY];