diff options
Diffstat (limited to '')
| -rw-r--r-- | src/index.ts | 39 | ||||
| -rw-r--r-- | src/tests.ts | 148 |
2 files changed, 110 insertions, 77 deletions
diff --git a/src/index.ts b/src/index.ts index 5164412..575c446 100644 --- a/src/index.ts +++ b/src/index.ts @@ -1,21 +1,41 @@ import { Op, Rewrite, ChainRewrites, Flip } from './util'; export type Add<A extends Op, B extends Op> = { op: '+'; a: A; b: B }; +export type Succ<A extends Op> = Add<'1', A>; 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>>; export interface Assoc0<A extends Op, B extends Op> { type: 'rewrite', - left: Add<Add<'0', A>, B>; + left: Add<Add<'0', A>, B>; // (0 + a) + b right: ChainRewrites<[ - Commutativity<'0', A>, - Identity<A>, - Flip<Identity<Add<A, B>>>, - Commutativity<Add<A, B>, '0'>, + Commutativity<'0', A>, // = (a + 0) + b + Identity<A>, // = a + b + Flip<Identity<Add<A, B>>>, // = (a + b) + 0 + Commutativity<Add<A, B>, '0'>, // = 0 + (a + b) ], this['left']>; }; +export type Assoc1<A extends Op, B extends Op> = Rewrite<Add<Succ<A>, B>, Succ<Add<A, B>>>; + +export interface Assoc<A extends Op, B extends Op, C extends Op> { + type: 'rewrite', + left: Add<Add<A, B>, C>; // (a + b) + c + right: ChainRewrites<[ + Rewrite<A, Succ<A>>, // = CHEATING + Assoc1<A, B>, // = succ(a + b) + c + Assoc1<Add<A, B>, C>, // = succ(a + b + c) + Rewrite<A, '0'>, // CHEATING. TODO: figure out recursion + Assoc0<B, C>, // Induction base case + Rewrite<'0', A>, // CHEATING + Flip<Assoc1<A, Add<B, C>>>, // = succ(a) + (b + c) + Rewrite<Succ<A>, A>, // = CHEATING + ], this['left']>; +}; + +// type _x = ApplyRewrite<Add<Add<'A', 'B'>, 'C'>, AssocN<'A', 'B', 'C'>> + /* Assoc: (a + b) + c = a + (b + c) @@ -26,7 +46,12 @@ For a = 0, = (b + c) + 0 -- flip id = 0 + (b + c) -- comm -For a = succ(), - +For a' = succ(a), +(succ(a) + b) + c += succ(a + b) + c += succ((a + b) + c) +----- rec += succ(a + (b + c)) += succ(a) + (b + c) */ 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'>> - >>, - ], -}; |