From 85a315ee5a9f7e33e65ae082a49c601ef7643920 Mon Sep 17 00:00:00 2001
From: Garrett Mills <gmills@allofe.com>
Date: Tue, 13 Dec 2022 11:28:43 -0600
Subject: [PATCH] Start example GCDT for Int

---
 alloy/gcdt2_int.als | 39 +++++++++++++++++++++++++++++++++++----
 1 file changed, 35 insertions(+), 4 deletions(-)

diff --git a/alloy/gcdt2_int.als b/alloy/gcdt2_int.als
index 4d9f7a6..dd1f99b 100644
--- a/alloy/gcdt2_int.als
+++ b/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 plusFn []: Int one->one (Int one->one Int) {
+	{opl, opr, res: Int |
+		res = opl + opr
+	}
 }
 
-fun plusOp [n: Int]: Commutative {
+fun plusOp []: Commutative {
 	{c: Commutative |
-		c.fn = {lhs: Int, rhs: (Int one->one Int) | rhs = plusFn[lhs]}
+		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