adds associativity for a=0

4 files changed, 88 insertions, 30 deletions

diff --git a/package.json b/package.json
index a7d7598..91f7ae3 100644
--- a/package.json
+++ b/package.json
@@ -1,5 +1,5 @@
 {
-  "name": "brainfuck-ts-types",
+  "name": "ts-theorem-provinator",
   "version": "0.0.0",
   "description": "__",
   "main": "index.js",
diff --git a/src/index.ts b/src/index.ts
index bd93300..5164412 100644
--- a/src/index.ts
+++ b/src/index.ts
@@ -1,41 +1,30 @@
-export type Op = string | { op: string; a: Op; b: Op };
+import { Op, Rewrite, ChainRewrites, Flip } from './util';
 
-export type Rewrite<left extends Op, right extends Op> = {
-  type: 'rewrite';
-  left: left;
-  right: right;
-};
-export type RewriteKind = Rewrite<Op, Op>;
-
-export type Flip<R extends RewriteKind> = Rewrite<R['right'], R['left']>;
-
-export type ApplyRewrite<O extends Op, R extends RewriteKind> =
-  O extends R['left'] ? R['right']
-  : O extends string ? O
-  : O extends { a: Op, b: Op, op: string } ? (
-    ApplyRewrite<O['a'], R> extends O['a']
-    ? Omit<O, 'b'> & { b: ApplyRewrite<O['b'], R> }
-    : Omit<O, 'a'> & { a: ApplyRewrite<O['a'], R> }
-  )
-  : never;
-
-export type Add<a extends Op, b extends Op> = { op: '+'; a: a; b: b };
+export type Add<A extends Op, B extends Op> = { op: '+'; a: A; b: B };
 
 export type Identity<A extends Op> = Rewrite<Add<A, '0'>, A>;
 export type Commutativity<A extends Op, B extends Op> = Rewrite<Add<A, B>, Add<B, A>>;
 
-// type _x = ApplyRewrite<Add<'A', '1'>, Identity<'0'>>;
-
-// type Assoc<A extends Op, B extends Op> =
+export interface Assoc0<A extends Op, B extends Op> {
+  type: 'rewrite',
+  left: Add<Add<'0', A>, B>;
+  right: ChainRewrites<[
+    Commutativity<'0', A>,
+    Identity<A>,
+    Flip<Identity<Add<A, B>>>,
+    Commutativity<Add<A, B>, '0'>,
+  ], this['left']>;
+};
 
 /*
-
 Assoc: (a + b) + c = a + (b + c)
 
 For a = 0,
 (0 + b) + c
-= b + c
-= 0 + (b + c)
+= (b + 0) + c -- comm
+= b + c -- id
+= (b + c) + 0 -- flip id
+= 0 + (b + c) -- comm
 
 For a = succ(),
 
diff --git a/src/tests.ts b/src/tests.ts
index 8c379e8..b4fc214 100644
--- a/src/tests.ts
+++ b/src/tests.ts
@@ -1,6 +1,7 @@
-import { Add, ApplyRewrite, Commutativity, Flip, Identity } from './index';
+import { Add, Assoc0, Commutativity, Identity } from './index';
+import { ApplyRewrite, ChainRewrites, Flip } from './util';
 
-type Eq<a, b> = ([a] extends [b] ? ([b] extends [a] ? true : false) : false) & { a: a; b: b };
+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 = {
@@ -22,6 +23,7 @@ export type _testCases = {
       Add<'A', Add<'B', 'C'>>
     >>,
   ],
+
   Commutativity: [
     assert<Eq<
       ApplyRewrite<Add<'A', 'B'>, Commutativity<'A', 'B'>>,
@@ -36,4 +38,40 @@ export type _testCases = {
       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'>>
+    >>,
+  ],
 };
diff --git a/src/util.ts b/src/util.ts
new file mode 100644
index 0000000..5556f70
--- /dev/null
+++ b/src/util.ts
@@ -0,0 +1,31 @@
+export type Op = string | { op: string; a: Op; b: Op };
+
+export type Rewrite<left extends Op, right extends Op> = {
+  type: 'rewrite';
+  left: left;
+  right: right;
+};
+
+export type Flip<R extends Rewrite<Op, Op>> = Rewrite<R['right'], R['left']>;
+
+export type ApplyRewrite<O extends Op, R extends Rewrite<Op, Op>> =
+  O extends R['left'] ? R['right']
+  : O extends string ? O
+  : O extends { a: Op, b: Op, op: string } ? (
+    ApplyRewrite<O['a'], R> extends O['a']
+    ? Omit<O, 'b'> & { b: ApplyRewrite<O['b'], R> }
+    : Omit<O, 'a'> & { a: ApplyRewrite<O['a'], R> }
+  )
+  : never;
+
+// interface Kind<V = unknown> {
+//   _: V;
+//   return: unknown;
+// }
+// type Ap<K extends Kind, V> = (K & { _: V })['return'];
+
+export type ChainRewrites<Rws extends Rewrite<Op, Op>[], O extends Op> =
+  Rws extends [] ? O
+   : Rws extends [infer R extends Rewrite<Op, Op>, ...infer Rs extends Rewrite<Op, Op>[]]
+   ? ChainRewrites<Rs, ApplyRewrite<O, R>>
+   : never;