diff options
Diffstat (limited to 'src/tests.ts')
| -rw-r--r-- | src/tests.ts | 148 |
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'>> - >>, - ], -}; |
