refactor: add support for imperative rewrites to make Refl more generic

2 files changed, 44 insertions, 31 deletions

diff --git a/src/index.ts b/src/index.ts
index 7a3f717..75e97be 100644
--- a/src/index.ts
+++ b/src/index.ts
@@ -17,7 +17,7 @@ export namespace addition {
     right: ChainRewrites<[
       IdentityR<B>,         // b = b + 0
       Sym<Identity<B>>,     // b + 0 = b + 0
-      Refl<Add<B, _0>>,     // true
+      Refl,
     ], this['left']>;
   };
   export interface Comm_Inductive_Proof<A extends Op, B extends Op> {
@@ -27,7 +27,7 @@ export namespace addition {
       SumSucc<A, B>,          // succ(a + b) = b + succ(a)
       Commutativity<A, B>,    // succ(b + a) = b + succ(a)
       SumSuccR<B, A>,         // succ(b + a) = succ(b + a)
-      Refl<Succ<Add<B, A>>>,  // true
+      Refl,
     ], this['left']>;
   };
   export namespace spec {
@@ -46,7 +46,7 @@ export namespace addition {
       Commutativity<_0, B>,   // (b + 0) + c = 0 + (b + c)
       Identity<B>,            // b + c = 0 + (b + c)
       IdentityR<Add<B, C>>,   // b + c = b + c
-      Refl<Add<B, C>>,        // true
+      Refl,
     ], this['left']>;
   };
   export interface Assoc_Inductive_Proof<A extends Op, B extends Op, C extends Op> {
@@ -57,7 +57,7 @@ export namespace addition {
       SumSucc<A, Add<B, C>>,           // succ(a + b) + c = succ(a + (b + c))
       SumSucc<Add<A, B>, C>,           // succ((a + b) + c) = succ(a + (b + c))
       Associativity<A, B, C>,          // succ(a + (b + c)) = succ(a + (b + c))
-      Refl<Succ<Add<A, Add<B, C>>>>,   // true
+      Refl,
     ], this['left']>;
   };
 
@@ -85,7 +85,7 @@ export namespace multiplication {
     right: ChainRewrites<[
       IdentityR<B>,        // b = b * 1
       Identity<B>,         // b = b
-      Refl<B>,             // true
+      Refl,
     ], this['left']>;
   };
   export interface Comm_Inductive_Proof<A extends Op, B extends Op> {
@@ -95,7 +95,7 @@ export namespace multiplication {
       MulSucc<A, B>,                     // b + a*b = b*succ(a)
       MulSuccR<B, A>,                    // b + a*b = b + b*a
       Commutativity<B, A>,               // b + a*b = b + a*b
-      Refl<Add<B, Multiply<A, B>>>,      // true
+      Refl,
     ], this['left']>;
   };
   export namespace spec {
@@ -116,19 +116,19 @@ export namespace multiplication {
       addition.SumSucc<_0, B>,            // succ(0 + b)*c = c + b*c
       addition.IdentityR<B>,              // succ(b)*c = c + b*c
       MulSucc<B, C>,                      // c + b*c = c + b*c
-      Refl<Add<C, Multiply<B, C>>>,       // true
+      Refl,
     ], this['left']>;
   };
   export interface Dist_Inductive_Proof<A extends Op, B extends Op, C extends Op> {
     type: 'rewrite',
     left: Equation<Multiply<Add<Succ<A>, B>, C>, Add<Multiply<Succ<A>, C>, Multiply<B, C>>>; // (succ(a) + b)*c = succ(a)*c + b*c
     right: ChainRewrites<[
-      addition.SumSucc<A, B>,                                      // succ(a + b)*c = succ(a)*c + b*c
+      addition.SumSucc<A, B>,                                       // succ(a + b)*c = succ(a)*c + b*c
       MulSucc<Add<A, B>, C>,                                        // c + (a + b)*c = succ(a)*c + b*c
       MulSucc<A, C>,                                                // c + (a + b)*c = (c + a*c) + b*c
       Distributivity<A, B, C>,                                      // c + (a*c + b*c) = (c + a*c) + b*c
       addition.Associativity<C, Multiply<A, C>, Multiply<B, C>>,    // (c + a*c) + b*c = (c + a*c) + b*c
-      Refl<Add<C, Add<Multiply<A, C>, Multiply<B, C>>>>,            // true
+      Refl,
     ], this['left']>;
   };
   export namespace spec {
@@ -147,18 +147,18 @@ export namespace multiplication {
     right: ChainRewrites<[
       IdentityR<B>,                     // b*c = 1*(b*c)
       IdentityR<Multiply<B, C>>,        // b*c = b*c
-      Refl<Multiply<B, C>>,             // true
+      Refl,
     ], this['left']>;
   };
   export interface Assoc_Inductive_Proof<A extends Op, B extends Op, C extends Op> {
     type: 'rewrite',
     left: Equation<Multiply<Multiply<Succ<A>, B>, C>, Multiply<Succ<A>, Multiply<B, C>>>; // (succ(a)*b)*c = succ(a)*(b*c)
     right: ChainRewrites<[
-      MulSucc<A, B>,                                                   // (b + a*b)*c = succ(a) * (b*c)
-      Distributivity<B, Multiply<A, B>, C>,                            // b*c + (a*b)*c = succ(a) * (b*c)
-      MulSucc<A, Multiply<B, C>>,                                      // b*c + (a*b)*c = b*c + a*(b*c)
-      Associativity<A, B, C>,                                          // b*c + a*(b*c) = b*c + a*(b*c)
-      Refl<Add<Multiply<B, C>, Multiply<A, Multiply<B, C>>>>,          // true
+      MulSucc<A, B>,                            // (b + a*b)*c = succ(a) * (b*c)
+      Distributivity<B, Multiply<A, B>, C>,     // b*c + (a*b)*c = succ(a) * (b*c)
+      MulSucc<A, Multiply<B, C>>,               // b*c + (a*b)*c = b*c + a*(b*c)
+      Associativity<A, B, C>,                   // b*c + a*(b*c) = b*c + a*(b*c)
+      Refl,
     ], this['left']>;
   };
   export namespace spec {
diff --git a/src/util.ts b/src/util.ts
index 1bed44b..c78c12c 100644
--- a/src/util.ts
+++ b/src/util.ts
@@ -1,15 +1,24 @@
 export type Op = string | { op: string; a: Op; b: Op };
 
-export type Rewrite<left extends Op, right extends Op> = {
-  type: 'rewrite';
+type RwType = 'rewrite' | 'imperative';
+
+export interface RewriteBase {
+  type: RwType;
+  left: Op;
+  right: Op;
+}
+
+export interface Rewrite<left extends Op, right extends Op, Typ extends RwType = 'rewrite'> extends RewriteBase {
+  type: Typ;
   left: left;
   right: right;
 };
 
-export type Sym<R extends Rewrite<Op, Op>> = Rewrite<R['right'], R['left']>;
+export type Sym<R extends RewriteBase> = Rewrite<R['right'], R['left'], R['type']>;
 
-export type ApplyRewrite<O extends Op, R extends Rewrite<Op, Op>> =
-  O extends R['left'] ? R['right']
+export type ApplyRewrite<O extends Op, R extends RewriteBase> =
+  R['type'] extends 'imperative' ? (R & { left: O })['right']
+  : 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']
@@ -19,25 +28,29 @@ export type ApplyRewrite<O extends Op, R extends Rewrite<Op, Op>> =
   )
   : never;
 
-export interface Kind<V = unknown, R = unknown> {
-  _: V;
-  return: R;
-}
-export type Ap<K extends Kind, V> = (K & { _: V })['return'];
-
-export type ChainRewrites<Rws extends Rewrite<Op, Op>[], O extends Op> =
+export type ChainRewrites<Rws extends RewriteBase[], O extends Op> =
   Rws extends [] ? O
-  : Rws extends [infer R extends Rewrite<Op, Op>, ...infer Rs extends Rewrite<Op, Op>[]]
+  : Rws extends [infer R extends RewriteBase, ...infer Rs extends RewriteBase[]]
   ? ChainRewrites<Rs, ApplyRewrite<O, R>>
   : never;
 
-export type VerifyEquation<Eq extends Rewrite<Op, Op>> =
+export type VerifyEquation<Eq extends RewriteBase> =
   Eq['right'] extends 'true' ? true : false & Eq['right'];
 
-export type Evaluate<Eq extends Rewrite<Op, Op>> = ApplyRewrite<Eq['left'], Eq>;
+export type Evaluate<Eq extends RewriteBase> = ApplyRewrite<Eq['left'], Eq>;
 
 export type assert<T extends true> = T;
 export type Eq<a, b> = ([a] extends [b] ? ([b] extends [a] ? true : false & { lhs: a; rhs: b }) : false & { lhs: a; rhs: b });
 
 export type Equation<A extends Op, B extends Op> = { op: '=', a: A, b: B };
-export type Refl<A extends Op> = Rewrite<Equation<A, A>, 'true'>;
+
+export interface Refl extends RewriteBase {
+  type: 'imperative';
+  left: Op;
+  right: this['left'] extends { op: '=', a: infer a, b: infer b }
+  ? (Eq<a, b> extends true ? 'true' : this['left'])
+  : this['left'];
+};
+
+// Like Refl, but you have to specify the sides of the equation and this one works recursively
+export type ReflR<A extends Op> = Rewrite<Equation<A, A>, 'true'>;