From 8ae8d7ab84d2ee38ee7cea4ff41598d135a9dc25 Mon Sep 17 00:00:00 2001
From: Akshay Nair <phenax5@gmail.com>
Date: Fri, 15 Dec 2023 18:17:43 +0530
Subject: refactor: add support for imperative rewrites to make Refl more
 generic

---
 src/util.ts | 45 +++++++++++++++++++++++++++++----------------
 1 file changed, 29 insertions(+), 16 deletions(-)

(limited to 'src/util.ts')

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'>;
-- 
cgit v1.3.1