Start reworking GCDT alloy theory

alloy/gcdt2.als

@@ -0,0 +1,72 @@
+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]
+	}
+}

alloy/gcdt2_int.als

@@ -0,0 +1,12 @@
+open gcdt2[Int]
+
+fun plusFn [n: Int]: Int one->one Int {
+	{lhs, rhs: Int | rhs = lhs + n}
+}
+
+fun plusOp [n: Int]: Commutative {
+	{c: Commutative |
+		c.fn = {lhs: Int, rhs: (Int one->one Int) | rhs = plusFn[lhs]}
+	}
+}
+