From f6e26212620de411e082cbd52379075ea5a99032 Mon Sep 17 00:00:00 2001
From: Akshay Nair <phenax5@gmail.com>
Date: Sun, 10 Dec 2023 16:15:00 +0530
Subject: init commit rewriting shit

---
 src/index.ts | 43 +++++++++++++++++++++++++++++++++++++++++++
 src/nat.ts   | 16 ++++++++++++++++
 src/tests.ts | 39 +++++++++++++++++++++++++++++++++++++++
 3 files changed, 98 insertions(+)
 create mode 100644 src/index.ts
 create mode 100644 src/nat.ts
 create mode 100644 src/tests.ts

(limited to 'src')

diff --git a/src/index.ts b/src/index.ts
new file mode 100644
index 0000000..bd93300
--- /dev/null
+++ b/src/index.ts
@@ -0,0 +1,43 @@
+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 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 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> =
+
+/*
+
+Assoc: (a + b) + c = a + (b + c)
+
+For a = 0,
+(0 + b) + c
+= b + c
+= 0 + (b + c)
+
+For a = succ(),
+
+*/
+
diff --git a/src/nat.ts b/src/nat.ts
new file mode 100644
index 0000000..86bd318
--- /dev/null
+++ b/src/nat.ts
@@ -0,0 +1,16 @@
+declare const prev: unique symbol
+
+export type _nat = number & { [prev]: _nat | null }
+export type Succ<n extends _nat> = number & { [prev]: n }
+export type Pred<n extends _nat> = n extends _0 ? n : n[typeof prev]
+export type Nat = _0 | Succ<_nat>
+
+export type _0 = 0 & { [prev]: null }
+export type _1 = Succ<_0>
+export type _2 = Succ<_1>
+export type _3 = Succ<_2>
+export type _4 = Succ<_3>
+export type _5 = Succ<_4>
+export type _6 = Succ<_5>
+export type _7 = Succ<_6>
+export type _8 = Succ<_7>
diff --git a/src/tests.ts b/src/tests.ts
new file mode 100644
index 0000000..8c379e8
--- /dev/null
+++ b/src/tests.ts
@@ -0,0 +1,39 @@
+import { Add, ApplyRewrite, Commutativity, Flip, Identity } from './index';
+
+type Eq<a, b> = ([a] extends [b] ? ([b] extends [a] ? true : false) : 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'>>
+    >>,
+  ],
+  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'>>
+    >>,
+  ],
+};
-- 
cgit v1.3.1