module gcdt[Operand]

-- Top-level GCDT signature:
sig GCDT {
	-- A domain of operands
	operand: Operand,

	-- A universe of possible operations
	ops: set Operation,

	-- Sub-universe of commutative ops:
	cOps: CommutativeOp & ops,

	-- Sub-universe of pseudo-commutative ops:
	pcOps: PseudoCommutativeOp & ops
} {
	ops = cOps + pcOps
}



-- All operations over GCDT's are binary:
abstract sig Operation {
	op: Operand one->one (Operand one->one Operand)
}

-- All operations should reflexively commute:
fact commutes {
	all opr: Operation | all opd1, opd2: Operand |
		opr.op[opd1][opd2] = opr.op[opd2][opd1]
}



-- Commutative operations:
sig CommutativeOp extends Operation {}

-- Commutative operations distribute trivially:
fact distributes {
	all cop1, cop2: CommutativeOp | all op1, op2, op3: Operand |
		cop1.op[cop2.op[op1][op2], op3] = cop1.op[op1, cop2.op[op2][op3]]
}



-- Pseudo-commutative operations:
sig PseudoCommutativeOp extends Operation {
	right: Operand
}

-- Pseudo-commutative operations fold into subsequent operands:
fact pseudoCommutes {
	all cop1, cop2: CommutativeOp | all pop: PseudoCommutativeOp |
	all opd1, opd2, opd3, opd4: Operand |
		pop.op[cop1.op[cop2.op[opd1, opd2], opd3], opd4] =
			cop1.op[cop2.op[pop.op[opd1, opd4], pop.op[opd2, opd4]], pop.op[opd3, opd4]]
}



-- A single operation applied to a GCDT:
sig GCDTDiff {
	op: one Operation,
	right: one Operand
}


-- An order-agnostic set of operations applied to a GCDT:
sig GCDTBatch {
	type: one GCDT,
	base: one Operand,
	ops: set GCDTDiff,
	fold: Operand one->one Operand
} {
	base in type.operand
	ops = {diff: ops | diff.op in type.ops && diff.right in type.operand}
}


fun applyDiff [diff: GCDTDiff, opd: Operand]: Operand {
	diff.op.op[opd][diff.right]
}

run applyDiff for 4

fun composeFold [opr: one Operation, right: one Operand, fold: Operand one->one Operand]: Operand one->one Operand {
	{lhs, rhs: Operand | rhs = fold[opr.op[lhs][right]] }
}

pred batchStep [batch1, batch2: GCDTBatch, diff: one GCDTDiff] {
	diff in batch1.ops
	batch1.type = batch2.type
	batch2.base = diff.op.op[batch1.fold[batch1.base]][batch1.fold[diff.right]]
	(diff.op in batch1.type.pcOps) => batch2.fold = composeFold[diff.op, diff.right, batch1.fold]
	else batch2.fold = batch1.fold
	batch2.ops = batch1.ops - diff
}

run batchStep for 4

fun batchSteps [] : GCDTBatch one->one GCDTBatch {
	{ batch1, batch2 : GCDTBatch | some diff: GCDTDiff | batchStep[batch1, batch2, diff] }
}

run batchSteps for 4

/*batchCommutes2: check {
	some dt: GCDT | all cop1, cop2: CommutativeOp | all pop: PseudoCommutativeOp |
		all diff1, diff2, diff3: GCDTDiff | all opBase: Operand |
		all batch1, batch2, batch3, batch4, batch5, batch6, batch7: GCDTBatch |
		all batch8, batch9, batch10, batch11, batch12, batch13, batch14: GCDTBatch |
			(dt.cOps = cop1 + cop2 && dt.pcOps = pop) =>
			(diff1.op = cop1 && diff2.op = cop2 && diff3.op = pop) =>
			(batch1.type = dt && batch1.base = opBase && batch1.fold = iden) =>
			(batch1.ops = diff1 + diff2 + diff3) =>
		 		   batchStep[batch1,  batch2,  diff1]
				&& batchStep[batch2,  batch3,  diff2]
				&& batchStep[batch3,  batch4,  diff3]
				&& batchStep[batch1,  batch5,  diff1]
				&& batchStep[batch5,  batch6,  diff3]
				&& batchStep[batch6,  batch4,  diff2]
				&& batchStep[batch1,  batch7,  diff2]
				&& batchStep[batch7,  batch8,  diff1]
				&& batchStep[batch8,  batch4,  diff3]
				&& batchStep[batch1,  batch9,  diff2]
				&& batchStep[batch9,  batch10, diff3]
				&& batchStep[batch10, batch4,  diff1]
				&& batchStep[batch1,  batch11, diff3]
				&& batchStep[batch11, batch12, diff1]
				&& batchStep[batch12, batch4,  diff2]
				&& batchStep[batch1,  batch13, diff3]
				&& batchStep[batch13, batch14, diff2]
				&& batchStep[batch14, batch2,  diff1]  -- FIXME: this is wrong. Should be batch4 
} for exactly 1 GCDT, 2 CommutativeOp, 1 PseudoCommutativeOp, 3 GCDTDiff, 6 Operand, 14 GCDTBatch

/*pred batchOneStep[batch: one GCDTBatch, fold: Operand one->one Operand] {
	result in batch.type.operand
	batch = {diff: batch |
		some val | val = diff.op.op[
}*/

-- This is wrong as it doesn't accumulate pseudo-commutative operations
/*pred recApplyDiff [type: GCDT, batch: set GCDTDiff, inOpd, outOpd: Operand] {
	inOpd in type.operand
	outOpd in type.operand
	batch = {diff: batch |
		diff.op in type.ops
		&& diff.right in type.operand
		&& recApplyDiff[type, (batch - diff), applyDiff[type, diff, inOpd], outOpd]
		&& outOpd in type.operand}
}

pred evalBatch [batch: one GCDTBatch, result: Operand] {
	recApplyDiff[batch.type, batch.ops, batch.base, result]
}*/