Start example GCDT for Int

alloy/gcdt2_int.als

@@ -1,12 +1,43 @@
 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]}
+fun plusFn []: Int one->one (Int one->one Int) {
+	{opl, opr, res: Int |
+		res = opl + opr
 	}
 }
 
+fun plusOp []: Commutative {
+	{c: Commutative |
+		c.fn = plusFn[]
+	}
+}
+
+fun mulFn []: Int one->one (Int one->one Int) {
+	{opl, opr, res: Int |
+		res = mul[opl, opr]
+	}
+}
+
+fun mulOp []: PseudoCommutative {
+	{pc: PseudoCommutative |
+		pc.fn = mulFn[]
+	}
+}
+
+fun intType []: GCDT {
+	{dt: GCDT |
+		dt.universe = Int &&
+		dt.operations = {plusOp[] + mulOp[]}
+	}
+}
+
+run intType for 5
+
+basicReduction: check {
+	all dt: GCDT | all r0: Reducer | all f1, f2, f3: Frame |
+	(dt = intType[] && r0 = baseReducer[0]) =>
+	(f1.op = plusOp[] && f1.right = 1) =>
+	(f2.op = mulOp[] && f2.right = 2) =>
+	(f3.op = plusOp[] && f3.right = 2) =>
+		reduceOnce[dt, f3, reduceOnce[dt, f2, reduceOnce[dt, f1, r0]]].base = 6
+} for 20