aboutsummaryrefslogtreecommitdiff
path: root/src/tests.ts
diff options
context:
space:
mode:
Diffstat (limited to 'src/tests.ts')
-rw-r--r--src/tests.ts148
1 files changed, 78 insertions, 70 deletions
diff --git a/src/tests.ts b/src/tests.ts
index b4fc214..d56cb30 100644
--- a/src/tests.ts
+++ b/src/tests.ts
@@ -1,77 +1,85 @@
-import { Add, Assoc0, Commutativity, Identity } from './index';
-import { ApplyRewrite, ChainRewrites, Flip } from './util';
+import { Add, Assoc, Assoc0, Assoc1, Commutativity, Identity, Succ } from './index';
+import { ApplyRewrite, ChainRewrites, Flip, Rewrite } from './util';
type Eq<a, b> = ([a] extends [b] ? ([b] extends [a] ? true : false & { a: a; b: b }) : 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'>>
- >>,
- ],
+export type specIdentity = [
+ 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'>>
+ >>,
+]
+
+export type specCommutativity = [
+ 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'>>
+ >>,
+]
+
+export type specChainRewrites = [
+ assert<Eq<
+ ChainRewrites<
+ [
+ Commutativity<'0', 'B'>,
+ Identity<'B'>,
+ ],
+ Add<Add<'0', 'B'>, 'C'>
+ >,
+ Add<'B', 'C'>
+ >>,
+ assert<Eq<
+ ChainRewrites<
+ [
+ Commutativity<'0', 'B'>,
+ Identity<'B'>,
+ Flip<Identity<Add<'B', 'C'>>>,
+ Commutativity<Add<'B', 'C'>, '0'>,
+ ],
+ Add<Add<'0', 'B'>, 'C'>
+ >,
+ Add<'0', Add<'B', 'C'>>
+ >>,
+]
+
+export type specAssoc0 = [
+ assert<Eq<
+ ApplyRewrite<Add<Add<'0', 'B'>, 'C'>, Assoc0<'B', 'C'>>,
+ Add<'0', Add<'B', 'C'>>
+ >>,
+ assert<Eq<
+ ApplyRewrite<Add<Add<'0', Add<'A', 'B'>>, 'C'>, Assoc0<Add<'A', 'B'>, 'C'>>,
+ Add<'0', Add<Add<'A', 'B'>, 'C'>>
+ >>,
+]
+
+export type specAssocN = [
+ assert<Eq<
+ ApplyRewrite<Add<Add<'A', 'B'>, 'C'>, Assoc<'A', 'B', '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'>>
- >>,
- ],
- ChainRewrites: [
- assert<Eq<
- ChainRewrites<
- [
- Commutativity<'0', 'B'>,
- Identity<'B'>,
- ],
- Add<Add<'0', 'B'>, 'C'>
- >,
- Add<'B', 'C'>
- >>,
- assert<Eq<
- ChainRewrites<
- [
- Commutativity<'0', 'B'>,
- Identity<'B'>,
- Flip<Identity<Add<'B', 'C'>>>,
- Commutativity<Add<'B', 'C'>, '0'>,
- ],
- Add<Add<'0', 'B'>, 'C'>
- >,
- Add<'0', Add<'B', 'C'>>
- >>,
- ],
- Assoc0: [
- assert<Eq<
- ApplyRewrite<Add<Add<'0', 'B'>, 'C'>, Assoc0<'B', 'C'>>,
- Add<'0', Add<'B', 'C'>>
- >>,
- assert<Eq<
- ApplyRewrite<Add<Add<'0', Add<'A', 'B'>>, 'C'>, Assoc0<Add<'A', 'B'>, 'C'>>,
- Add<'0', Add<Add<'A', 'B'>, 'C'>>
- >>,
- ],
-};