feat: adds monadic/dyadic operators

3 files changed, 16 insertions, 10 deletions

diff --git a/src/index.ts b/src/index.ts
index 276bbe9..4a00438 100644
--- a/src/index.ts
+++ b/src/index.ts
@@ -1,5 +1,5 @@
 import { Add, Multiply, Succ, _0, _1, _3 } from './nat';
-import { Op, Rewrite, ChainRewrites, Sym, Equation, Refl, VerifyEquation, assert, RewriteBase, Subst, ApplyRewrite, Evaluate, ReflR, OpToStr } from './util';
+import { Op, Rewrite, ChainRewrites, Sym, Equation, Refl, VerifyEquation, assert, Subst, ApplyRewrite, Evaluate, OpToStr } from './util';
 
 export namespace addition {
   // Identity
@@ -186,7 +186,7 @@ export namespace multiplication {
 }
 
 export namespace equation {
-  type F<X extends Op> = { op: '<F>', a: _0, b: X };
+  type F<X extends Op> = { op: 'F', a: X };
 
   export type Reflexivity<A extends Op> = Rewrite<Equation<A, A>, 'true'>;
 
@@ -194,7 +194,7 @@ export namespace equation {
 
   export type Congruence<A extends Op, B extends Op> = Rewrite<Equation<A, B>, Equation<F<A>, F<B>>>;
 
-  export type SubstituteEq<O extends { op: '=', a: Op, b: Op }> = Rewrite<O['a'], O['b']>
+  export type SubstituteEq<O extends Equation<Op, Op>> = Rewrite<O['a'], O['b']>
   export interface SubstituteEq_Proof<A extends Op, B extends Op> {
     type: 'rewrite',
     known: {
diff --git a/src/nat.ts b/src/nat.ts
index 0017489..7491e82 100644
--- a/src/nat.ts
+++ b/src/nat.ts
@@ -2,7 +2,7 @@ import { Op } from './util';
 
 export type Add<A extends Op, B extends Op> = { op: '+'; a: A; b: B };
 export type Multiply<A extends Op, B extends Op> = { op: '*'; a: A; b: B };
-export type Succ<A extends Op> = Add<'1', A>;
+export type Succ<A extends Op> = { op: 'succ', a: A };
 
 export type _0 = '0'
 export type _1 = Succ<_0>
diff --git a/src/util.ts b/src/util.ts
index da6d637..a4dd2e9 100644
--- a/src/util.ts
+++ b/src/util.ts
@@ -1,13 +1,16 @@
-type COp = { op: string; a: Op; b: Op }
-export type Op = string | COp;
+type DyadicOp = { op: string; a: Op; b: Op }
+type MonadicOp = { op: string; a: Op }
+export type Op = string | MonadicOp | DyadicOp;
 
 export type OpToStr<O extends Op> =
   O extends string
   ? O
   : O extends { op: string, a: infer a extends string, b: infer b extends string } ? `(${a} ${O['op']} ${b})`
-  : O extends { op: string, a: infer a extends COp, b: infer b extends string } ? `(${OpToStr<a>} ${O['op']} ${b})`
-  : O extends { op: string, a: infer a extends string, b: infer b extends COp } ? `(${a} ${O['op']} ${OpToStr<b>})`
-  : O extends { op: string, a: infer a extends COp, b: infer b extends COp } ? `(${OpToStr<a>} ${O['op']} ${OpToStr<b>})`
+  : O extends { op: string, a: infer a extends DyadicOp, b: infer b extends string } ? `(${OpToStr<a>} ${O['op']} ${b})`
+  : O extends { op: string, a: infer a extends string, b: infer b extends DyadicOp } ? `(${a} ${O['op']} ${OpToStr<b>})`
+  : O extends { op: string, a: infer a extends DyadicOp, b: infer b extends DyadicOp } ? `(${OpToStr<a>} ${O['op']} ${OpToStr<b>})`
+  : O extends { op: string, a: infer a extends string } ? `${O['op']}(${a})`
+  : O extends { op: string, a: infer a extends DyadicOp } ? `${O['op']}(${OpToStr<a>})`
   : never;
 
 type RwType = 'rewrite' | 'imperative';
@@ -32,12 +35,15 @@ 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 } ? (
+  : O extends DyadicOp ? (
     ApplyRewrite<O['a'], R> extends O['a']
     ? (ApplyRewrite<O['b'], R> extends O['b'] ? O
       : Omit<O, 'b'> & { b: ApplyRewrite<O['b'], R> })
     : Omit<O, 'a'> & { a: ApplyRewrite<O['a'], R> }
   )
+  : O extends MonadicOp ? (
+    ApplyRewrite<O['a'], R> extends O['a'] ? O : Omit<O, 'a'> & { a: ApplyRewrite<O['a'], R> }
+  )
   : never;
 
 export type ChainRewrites<Rws extends RewriteBase[], O extends Op> =