From 60331b72ab37e581b0fb405c2eff862e16b52ac2 Mon Sep 17 00:00:00 2001
From: Akshay Nair <phenax5@gmail.com>
Date: Sun, 10 Dec 2023 19:24:31 +0530
Subject: cheated for associativity for a=n

---
 src/tests.ts | 148 +++++++++++++++++++++++++++++++----------------------------
 1 file changed, 78 insertions(+), 70 deletions(-)

(limited to 'src/tests.ts')

diff --git a/src/tests.ts b/src/tests.ts
index b4fc214..d56cb30 100644
--- a/src/tests.ts
+++ b/src/tests.ts
@@ -1,77 +1,85 @@
-import { Add, Assoc0, Commutativity, Identity } from './index';
-import { ApplyRewrite, ChainRewrites, Flip } from './util';
+import { Add, Assoc, Assoc0, Assoc1, Commutativity, Identity, Succ } from './index';
+import { ApplyRewrite, ChainRewrites, Flip, Rewrite } from './util';
 
 type Eq<a, b> = ([a] extends [b] ? ([b] extends [a] ? true : false & { a: a; b: b }) : false & { a: a; b: b });
 type assert<T extends true> = T;
 
-export type _testCases = {
-  Identity: [
-    assert<Eq<
-      ApplyRewrite<Add<'A', Add<'B', '0'>>, Identity<'B'>>,
-      Add<'A', 'B'>
-    >>,
-    assert<Eq<
-      ApplyRewrite<Add<Add<'A', 'B'>, '0'>, Identity<Add<'A', 'B'>>>,
-      Add<'A', 'B'>
-    >>,
-    assert<Eq<
-      ApplyRewrite<Add<'A', 'B'>, Flip<Identity<Add<'A', 'B'>>>>,
-      Add<Add<'A', 'B'>, '0'>
-    >>,
-    assert<Eq<
-      ApplyRewrite<Add<'A', Add<'B', Add<'C', '0'>>>, Identity<'C'>>,
-      Add<'A', Add<'B', 'C'>>
-    >>,
-  ],
+export type specIdentity = [
+  assert<Eq<
+    ApplyRewrite<Add<'A', Add<'B', '0'>>, Identity<'B'>>,
+    Add<'A', 'B'>
+  >>,
+  assert<Eq<
+    ApplyRewrite<Add<Add<'A', 'B'>, '0'>, Identity<Add<'A', 'B'>>>,
+    Add<'A', 'B'>
+  >>,
+  assert<Eq<
+    ApplyRewrite<Add<'A', 'B'>, Flip<Identity<Add<'A', 'B'>>>>,
+    Add<Add<'A', 'B'>, '0'>
+  >>,
+  assert<Eq<
+    ApplyRewrite<Add<'A', Add<'B', Add<'C', '0'>>>, Identity<'C'>>,
+    Add<'A', Add<'B', 'C'>>
+  >>,
+]
+
+export type specCommutativity = [
+  assert<Eq<
+    ApplyRewrite<Add<'A', 'B'>, Commutativity<'A', 'B'>>,
+    Add<'B', 'A'>
+  >>,
+  assert<Eq<
+    ApplyRewrite<Add<Add<'A', 'B'>, 'C'>, Commutativity<'A', 'B'>>,
+    Add<Add<'B', 'A'>, 'C'>
+  >>,
+  assert<Eq<
+    ApplyRewrite<Add<'A', Add<'B', 'C'>>, Commutativity<'B', 'C'>>,
+    Add<'A', Add<'C', 'B'>>
+  >>,
+]
+
+export type specChainRewrites = [
+  assert<Eq<
+    ChainRewrites<
+      [
+        Commutativity<'0', 'B'>,
+        Identity<'B'>,
+      ],
+      Add<Add<'0', 'B'>, 'C'>
+    >,
+    Add<'B', 'C'>
+  >>,
+  assert<Eq<
+    ChainRewrites<
+      [
+        Commutativity<'0', 'B'>,
+        Identity<'B'>,
+        Flip<Identity<Add<'B', 'C'>>>,
+        Commutativity<Add<'B', 'C'>, '0'>,
+      ],
+      Add<Add<'0', 'B'>, 'C'>
+    >,
+    Add<'0', Add<'B', 'C'>>
+  >>,
+]
+
+export type specAssoc0 = [
+  assert<Eq<
+    ApplyRewrite<Add<Add<'0', 'B'>, 'C'>, Assoc0<'B', 'C'>>,
+    Add<'0', Add<'B', 'C'>>
+  >>,
+  assert<Eq<
+    ApplyRewrite<Add<Add<'0', Add<'A', 'B'>>, 'C'>, Assoc0<Add<'A', 'B'>, 'C'>>,
+    Add<'0', Add<Add<'A', 'B'>, 'C'>>
+  >>,
+]
+
+export type specAssocN = [
+  assert<Eq<
+    ApplyRewrite<Add<Add<'A', 'B'>, 'C'>, Assoc<'A', 'B', 'C'>>,
+    Add<'A', Add<'B', 'C'>>
+  >>,
+]
 
-  Commutativity: [
-    assert<Eq<
-      ApplyRewrite<Add<'A', 'B'>, Commutativity<'A', 'B'>>,
-      Add<'B', 'A'>
-    >>,
-    assert<Eq<
-      ApplyRewrite<Add<Add<'A', 'B'>, 'C'>, Commutativity<'A', 'B'>>,
-      Add<Add<'B', 'A'>, 'C'>
-    >>,
-    assert<Eq<
-      ApplyRewrite<Add<'A', Add<'B', 'C'>>, Commutativity<'B', 'C'>>,
-      Add<'A', Add<'C', 'B'>>
-    >>,
-  ],
 
-  ChainRewrites: [
-    assert<Eq<
-      ChainRewrites<
-        [
-          Commutativity<'0', 'B'>,
-          Identity<'B'>,
-        ],
-        Add<Add<'0', 'B'>, 'C'>
-      >,
-      Add<'B', 'C'>
-    >>,
-    assert<Eq<
-      ChainRewrites<
-        [
-          Commutativity<'0', 'B'>,
-          Identity<'B'>,
-          Flip<Identity<Add<'B', 'C'>>>,
-          Commutativity<Add<'B', 'C'>, '0'>,
-        ],
-        Add<Add<'0', 'B'>, 'C'>
-      >,
-      Add<'0', Add<'B', 'C'>>
-    >>,
-  ],
 
-  Assoc0: [
-    assert<Eq<
-      ApplyRewrite<Add<Add<'0', 'B'>, 'C'>, Assoc0<'B', 'C'>>,
-      Add<'0', Add<'B', 'C'>>
-    >>,
-    assert<Eq<
-      ApplyRewrite<Add<Add<'0', Add<'A', 'B'>>, 'C'>, Assoc0<Add<'A', 'B'>, 'C'>>,
-      Add<'0', Add<Add<'A', 'B'>, 'C'>>
-    >>,
-  ],
-};
-- 
cgit v1.3.1