module gcdt2[Operand]

-- Operations over the operands:
abstract sig Operation {
	fn: Operand one->one (Operand one->one Operand)
}

sig Commutative, PseudoCommutative extends Operation {}

fact { Operation = Commutative + PseudoCommutative }


sig GCDT {
	universe: set Operand,
	operations: set Operation
}


sig Frame {
	op: one Operation,
	right: one Operand
}


sig Reducer {
	base: Operand,
	fold: Operand one->one Operand
}

fun baseReducer [val: Operand]: Reducer {
	{ r: Reducer | r.base = val && r.fold = iden }
}

pred typeFrame[type: GCDT, frame: Frame] {
	frame.op in type.operations
	frame.right in type.universe
}

pred typeReducer[type: GCDT, reducer: Reducer] {
	reducer.base in type.universe
}

pred applyFrame [type: GCDT, frame: Frame, reducer: Reducer, result: Operand] {
	typeFrame[type, frame]
	typeReducer[type, reducer]
	result in type.universe
	result = reducer.fold[frame.op.fn[reducer.base][frame.right]]
}

fun wrapFold [frame: Frame, fold: Operand one->one Operand]: Operand one->one Operand {
	{lhs, rhs : Operand |
		rhs = fold[frame.op.fn[lhs][frame.right]]
	}
}

pred applyFold [type: GCDT, frame: Frame, reducer, result: Reducer] {
	typeFrame[type, frame]
	typeReducer[type, reducer]
	typeReducer[type, result]
	(frame.op in PseudoCommutative) => result.fold = wrapFold[frame, reducer.fold]
	else (frame.op in Commutative) => result.fold = reducer.fold
}

fun reduceOnce[type: GCDT, frame: Frame, reducer: Reducer]: Reducer {
	{ result: Reducer |
		   typeReducer[type, result]
		&& applyFrame[type, frame, reducer, result.base]
		&& applyFold[type, frame, reducer, result]
		&& typeFrame[type, frame]
		&& typeReducer[type, reducer]
	}
}