diff options
| author | Akshay Nair <phenax5@gmail.com> | 2023-12-10 17:33:01 +0530 |
|---|---|---|
| committer | Akshay Nair <phenax5@gmail.com> | 2023-12-10 17:33:01 +0530 |
| commit | f724285d1d3cea85128069bcdf04e4c6af9c7a39 (patch) | |
| tree | ee73c1b85a4af63f6e553bbc8c3379d406e8e3ee /src/util.ts | |
| parent | f6e26212620de411e082cbd52379075ea5a99032 (diff) | |
| download | ts-theorem-provinator-f724285d1d3cea85128069bcdf04e4c6af9c7a39.tar.gz ts-theorem-provinator-f724285d1d3cea85128069bcdf04e4c6af9c7a39.zip | |
adds associativity for a=0
Diffstat (limited to 'src/util.ts')
| -rw-r--r-- | src/util.ts | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/src/util.ts b/src/util.ts new file mode 100644 index 0000000..5556f70 --- /dev/null +++ b/src/util.ts @@ -0,0 +1,31 @@ +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 Flip<R extends Rewrite<Op, Op>> = Rewrite<R['right'], R['left']>; + +export type ApplyRewrite<O extends Op, R extends Rewrite<Op, Op>> = + 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; + +// interface Kind<V = unknown> { +// _: V; +// return: unknown; +// } +// type Ap<K extends Kind, V> = (K & { _: V })['return']; + +export type ChainRewrites<Rws extends Rewrite<Op, Op>[], O extends Op> = + Rws extends [] ? O + : Rws extends [infer R extends Rewrite<Op, Op>, ...infer Rs extends Rewrite<Op, Op>[]] + ? ChainRewrites<Rs, ApplyRewrite<O, R>> + : never; |
