adds associativity for a=0

1 files changed, 16 insertions, 27 deletions

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(),