From efc0358c1e2b52308d3df68aa713cef5dc6e6bfe Mon Sep 17 00:00:00 2001 From: Akshay Nair Date: Fri, 15 Dec 2023 22:36:03 +0530 Subject: refactor: moves stuff around --- package.json | 2 +- src/equation.ts | 51 ++++++++++ src/index.ts | 236 ---------------------------------------------- src/nat.ts | 10 -- src/natural-numbers.ts | 186 ++++++++++++++++++++++++++++++++++++ src/tests.ts | 85 ----------------- src/tests/nat.spec.ts | 60 ++++++++++++ src/tests/theorem.spec.ts | 28 ++++++ src/util.ts | 75 --------------- src/utils/nat.ts | 10 ++ src/utils/theorem.ts | 75 +++++++++++++++ 11 files changed, 411 insertions(+), 407 deletions(-) create mode 100644 src/equation.ts delete mode 100644 src/index.ts delete mode 100644 src/nat.ts create mode 100644 src/natural-numbers.ts delete mode 100644 src/tests.ts create mode 100644 src/tests/nat.spec.ts create mode 100644 src/tests/theorem.spec.ts delete mode 100644 src/util.ts create mode 100644 src/utils/nat.ts create mode 100644 src/utils/theorem.ts diff --git a/package.json b/package.json index 91f7ae3..7691cd2 100644 --- a/package.json +++ b/package.json @@ -7,7 +7,7 @@ "author": "Akshay Nair ", "license": "MIT", "scripts": { - "test": "tsc --noEmit ./src/tests.ts" + "test": "tsc --noEmit" }, "dependencies": { "typescript": "^5.3.3" diff --git a/src/equation.ts b/src/equation.ts new file mode 100644 index 0000000..0ec25d6 --- /dev/null +++ b/src/equation.ts @@ -0,0 +1,51 @@ +import { Op, Rewrite, ChainRewrites, Sym, Equation, VerifyEquation, assert, ApplyRewrite, Evaluate, OpToStr } from './utils/theorem'; + +export namespace equation { + type F = { op: 'F', a: X }; + + export type Reflexivity = Rewrite, 'true'>; + + export type Symmetry = Rewrite, Equation>; + + export type Congruence = Rewrite, Equation, F>>; + + export type SubstituteEq> = Rewrite + export interface SubstituteEq_Proof { + type: 'rewrite', + known: { + 'a = b': Equation, + }, + left: Equation, F>; // f(a) = f(b) + right: ChainRewrites<[ + Sym>, // a = b + SubstituteEq, // b = b + Reflexivity, + ], this['left']>; + }; + export namespace spec { + export type substitution = [ + assert>>, + ] + } + + export interface Transitivity_Proof { + type: 'rewrite', + known: { + 'a = b': Equation, + 'b = c': Equation, + }, + left: Equation, Equation>; // (a = b) = (b = c) + right: ChainRewrites<[ + SubstituteEq, // (b = b) = (b = c) + SubstituteEq>>, // (b = b) = (c = b) + Reflexivity, // true = (b = b) + Reflexivity, // true = true + Reflexivity<'true'>, + ], this['left']>; + }; + export namespace spec { + export type transitivity = [ + assert>>, + ] + } +} diff --git a/src/index.ts b/src/index.ts deleted file mode 100644 index 4a00438..0000000 --- a/src/index.ts +++ /dev/null @@ -1,236 +0,0 @@ -import { Add, Multiply, Succ, _0, _1, _3 } from './nat'; -import { Op, Rewrite, ChainRewrites, Sym, Equation, Refl, VerifyEquation, assert, Subst, ApplyRewrite, Evaluate, OpToStr } from './util'; - -export namespace addition { - // Identity - export type Identity = Rewrite, A>; - export type IdentityR = Rewrite, A>; - - export type SuccLemma = Rewrite, B>, Succ>> - export type SuccLemmaR = Rewrite>, Succ>> - - // Commutativity - export type Commutativity = Rewrite, Add>; - export interface Comm_Base_Proof { - type: 'rewrite', - left: Equation, Add>; // 0 + b = b + 0 - right: ChainRewrites<[ - IdentityR, // b = b + 0 - Sym>, // b + 0 = b + 0 - Refl, - ], this['left']>; - }; - export interface Comm_Inductive_Proof { - type: 'rewrite', - left: Equation, B>, Add>>; // succ(a) + b = b + succ(a) - right: ChainRewrites<[ - SuccLemma, // succ(a + b) = b + succ(a) - Commutativity, // succ(b + a) = b + succ(a) - SuccLemmaR, // succ(b + a) = succ(b + a) - Refl, - ], this['left']>; - }; - export namespace spec { - export type commutativity = [ - assert>>, - assert>>, - ] - } - - // Associativity - export type Associativity = Rewrite, C>, Add>>; - export interface Assoc_Base_Proof { - type: 'rewrite', - left: Equation, C>, Add<_0, Add>>; // (0 + b) + c = 0 + (b + c) - right: ChainRewrites<[ - Commutativity<_0, B>, // (b + 0) + c = 0 + (b + c) - Identity, // b + c = 0 + (b + c) - IdentityR>, // b + c = b + c - Refl, - ], this['left']>; - }; - export interface Assoc_Inductive_Proof { - type: 'rewrite', - left: Equation, B>, C>, Add, Add>>; // (succ(a) + b) + c = succ(a) + (b + c) - right: ChainRewrites<[ - SuccLemma, // succ(a + b) + c = succ(a) + (b + c) - SuccLemma>, // succ(a + b) + c = succ(a + (b + c)) - SuccLemma, C>, // succ((a + b) + c) = succ(a + (b + c)) - Associativity, // succ(a + (b + c)) = succ(a + (b + c)) - Refl, - ], this['left']>; - }; - - export namespace spec { - export type associativity = [ - assert>>, - assert>>, - ] - } - - // Rearrange - export interface Rearrange_Proof { - type: 'rewrite', - left: Equation, Add>, Add, D>>>; // (a + b) + (c + d) = a + ((b + c) + d) - right: ChainRewrites<[ - Associativity>, // a + (b + (c + d)) = a + ((b + c) + d) - Associativity, // a + (b + (c + d)) = a + (b + (c + d)) - Refl, - ], this['left']>; - }; - export namespace spec { - export type rearrange = [ - assert>>, - ] - } -} - -export namespace multiplication { - // Identity - export type Identity = Rewrite, A>; - export type IdentityR = Rewrite, A>; - - export type SuccLemma = Rewrite, B>, Add>>; - export type SuccLemmaR = Rewrite>, Add>>; - - // Commutativity - export type Commutativity = Rewrite, Multiply>; - export interface Comm_Base_Proof { - type: 'rewrite', - left: Equation, Multiply>; // 1 * b = b * 1 - right: ChainRewrites<[ - IdentityR, // b = b * 1 - Identity, // b = b - Refl, - ], this['left']>; - }; - export interface Comm_Inductive_Proof { - type: 'rewrite', - left: Equation, B>, Multiply>>; // succ(a)*b = b*succ(a) - right: ChainRewrites<[ - SuccLemma, // b + a*b = b*succ(a) - SuccLemmaR, // b + a*b = b + b*a - Commutativity, // b + a*b = b + a*b - Refl, - ], this['left']>; - }; - export namespace spec { - export type commutativity = [ - assert>>, - assert>>, - ] - } - - // Distributivity - export type Distributivity = - Rewrite, C>, Add, Multiply>>; - export interface Dist_Base_Proof { - type: 'rewrite', - left: Equation, C>, Add, Multiply>>; // (1 + b)*c = 1*c + b*c - right: ChainRewrites<[ - IdentityR, // (1 + b)*c = c + b*c - addition.SuccLemma<_0, B>, // succ(0 + b)*c = c + b*c - addition.IdentityR, // succ(b)*c = c + b*c - SuccLemma, // c + b*c = c + b*c - Refl, - ], this['left']>; - }; - export interface Dist_Inductive_Proof { - type: 'rewrite', - left: Equation, B>, C>, Add, C>, Multiply>>; // (succ(a) + b)*c = succ(a)*c + b*c - right: ChainRewrites<[ - addition.SuccLemma, // succ(a + b)*c = succ(a)*c + b*c - SuccLemma, C>, // c + (a + b)*c = succ(a)*c + b*c - SuccLemma, // c + (a + b)*c = (c + a*c) + b*c - Distributivity, // c + (a*c + b*c) = (c + a*c) + b*c - addition.Associativity, Multiply>, // (c + a*c) + b*c = (c + a*c) + b*c - Refl, - ], this['left']>; - }; - export namespace spec { - export type distributivity = [ - assert>>, - assert>>, - ] - } - - // Associativity - export type Associativity = - Rewrite, C>, Multiply>>; - export interface Assoc_Base_Proof { - type: 'rewrite', - left: Equation, C>, Multiply<_1, Multiply>>; // (1*b)*c = 1*(b*c) - right: ChainRewrites<[ - IdentityR, // b*c = 1*(b*c) - IdentityR>, // b*c = b*c - Refl, - ], this['left']>; - }; - export interface Assoc_Inductive_Proof { - type: 'rewrite', - left: Equation, B>, C>, Multiply, Multiply>>; // (succ(a)*b)*c = succ(a)*(b*c) - right: ChainRewrites<[ - SuccLemma, // (b + a*b)*c = succ(a) * (b*c) - Distributivity, C>, // b*c + (a*b)*c = succ(a) * (b*c) - SuccLemma>, // b*c + (a*b)*c = b*c + a*(b*c) - Associativity, // b*c + a*(b*c) = b*c + a*(b*c) - Refl, - ], this['left']>; - }; - export namespace spec { - export type associativity = [ - assert>>, - assert>>, - ] - } -} - -export namespace equation { - type F = { op: 'F', a: X }; - - export type Reflexivity = Rewrite, 'true'>; - - export type Symmetry = Rewrite, Equation>; - - export type Congruence = Rewrite, Equation, F>>; - - export type SubstituteEq> = Rewrite - export interface SubstituteEq_Proof { - type: 'rewrite', - known: { - 'a = b': Equation, - }, - left: Equation, F>; // f(a) = f(b) - right: ChainRewrites<[ - Sym>, // a = b - SubstituteEq, // b = b - Reflexivity, - ], this['left']>; - }; - export namespace spec { - export type substitution = [ - assert>>, - ] - } - - export interface Transitivity_Proof { - type: 'rewrite', - known: { - 'a = b': Equation, - 'b = c': Equation, - }, - left: Equation, Equation>; // (a = b) = (b = c) - right: ChainRewrites<[ - SubstituteEq, // (b = b) = (b = c) - SubstituteEq>>, // (b = b) = (c = b) - Reflexivity, // true = (b = b) - Reflexivity, // true = true - Reflexivity<'true'>, - ], this['left']>; - }; - export namespace spec { - export type transitivity = [ - assert>>, - ] - } -} diff --git a/src/nat.ts b/src/nat.ts deleted file mode 100644 index 7491e82..0000000 --- a/src/nat.ts +++ /dev/null @@ -1,10 +0,0 @@ -import { Op } from './util'; - -export type Add = { op: '+'; a: A; b: B }; -export type Multiply = { op: '*'; a: A; b: B }; -export type Succ = { op: 'succ', a: A }; - -export type _0 = '0' -export type _1 = Succ<_0> -export type _2 = Succ<_1> -export type _3 = Succ<_2> diff --git a/src/natural-numbers.ts b/src/natural-numbers.ts new file mode 100644 index 0000000..fa8a3ce --- /dev/null +++ b/src/natural-numbers.ts @@ -0,0 +1,186 @@ +import { Add, Multiply, Succ, _0, _1, _3 } from './utils/nat'; +import { Op, Rewrite, ChainRewrites, Sym, Equation, Refl, VerifyEquation, assert, Subst, ApplyRewrite, Evaluate, OpToStr } from './utils/theorem'; + +export namespace addition { + // Identity + export type Identity = Rewrite, A>; + export type IdentityR = Rewrite, A>; + + export type SuccLemma = Rewrite, B>, Succ>> + export type SuccLemmaR = Rewrite>, Succ>> + + // Commutativity + export type Commutativity = Rewrite, Add>; + export interface Comm_Base_Proof { + type: 'rewrite', + left: Equation, Add>; // 0 + b = b + 0 + right: ChainRewrites<[ + IdentityR, // b = b + 0 + Sym>, // b + 0 = b + 0 + Refl, + ], this['left']>; + }; + export interface Comm_Inductive_Proof { + type: 'rewrite', + left: Equation, B>, Add>>; // succ(a) + b = b + succ(a) + right: ChainRewrites<[ + SuccLemma, // succ(a + b) = b + succ(a) + Commutativity, // succ(b + a) = b + succ(a) + SuccLemmaR, // succ(b + a) = succ(b + a) + Refl, + ], this['left']>; + }; + export namespace spec { + export type commutativity = [ + assert>>, + assert>>, + ] + } + + // Associativity + export type Associativity = Rewrite, C>, Add>>; + export interface Assoc_Base_Proof { + type: 'rewrite', + left: Equation, C>, Add<_0, Add>>; // (0 + b) + c = 0 + (b + c) + right: ChainRewrites<[ + Commutativity<_0, B>, // (b + 0) + c = 0 + (b + c) + Identity, // b + c = 0 + (b + c) + IdentityR>, // b + c = b + c + Refl, + ], this['left']>; + }; + export interface Assoc_Inductive_Proof { + type: 'rewrite', + left: Equation, B>, C>, Add, Add>>; // (succ(a) + b) + c = succ(a) + (b + c) + right: ChainRewrites<[ + SuccLemma, // succ(a + b) + c = succ(a) + (b + c) + SuccLemma>, // succ(a + b) + c = succ(a + (b + c)) + SuccLemma, C>, // succ((a + b) + c) = succ(a + (b + c)) + Associativity, // succ(a + (b + c)) = succ(a + (b + c)) + Refl, + ], this['left']>; + }; + + export namespace spec { + export type associativity = [ + assert>>, + assert>>, + ] + } + + // Rearrange + export interface Rearrange_Proof { + type: 'rewrite', + left: Equation, Add>, Add, D>>>; // (a + b) + (c + d) = a + ((b + c) + d) + right: ChainRewrites<[ + Associativity>, // a + (b + (c + d)) = a + ((b + c) + d) + Associativity, // a + (b + (c + d)) = a + (b + (c + d)) + Refl, + ], this['left']>; + }; + export namespace spec { + export type rearrange = [ + assert>>, + ] + } +} + +export namespace multiplication { + // Identity + export type Identity = Rewrite, A>; + export type IdentityR = Rewrite, A>; + + export type SuccLemma = Rewrite, B>, Add>>; + export type SuccLemmaR = Rewrite>, Add>>; + + // Commutativity + export type Commutativity = Rewrite, Multiply>; + export interface Comm_Base_Proof { + type: 'rewrite', + left: Equation, Multiply>; // 1 * b = b * 1 + right: ChainRewrites<[ + IdentityR, // b = b * 1 + Identity, // b = b + Refl, + ], this['left']>; + }; + export interface Comm_Inductive_Proof { + type: 'rewrite', + left: Equation, B>, Multiply>>; // succ(a)*b = b*succ(a) + right: ChainRewrites<[ + SuccLemma, // b + a*b = b*succ(a) + SuccLemmaR, // b + a*b = b + b*a + Commutativity, // b + a*b = b + a*b + Refl, + ], this['left']>; + }; + export namespace spec { + export type commutativity = [ + assert>>, + assert>>, + ] + } + + // Distributivity + export type Distributivity = + Rewrite, C>, Add, Multiply>>; + export interface Dist_Base_Proof { + type: 'rewrite', + left: Equation, C>, Add, Multiply>>; // (1 + b)*c = 1*c + b*c + right: ChainRewrites<[ + IdentityR, // (1 + b)*c = c + b*c + addition.SuccLemma<_0, B>, // succ(0 + b)*c = c + b*c + addition.IdentityR, // succ(b)*c = c + b*c + SuccLemma, // c + b*c = c + b*c + Refl, + ], this['left']>; + }; + export interface Dist_Inductive_Proof { + type: 'rewrite', + left: Equation, B>, C>, Add, C>, Multiply>>; // (succ(a) + b)*c = succ(a)*c + b*c + right: ChainRewrites<[ + addition.SuccLemma, // succ(a + b)*c = succ(a)*c + b*c + SuccLemma, C>, // c + (a + b)*c = succ(a)*c + b*c + SuccLemma, // c + (a + b)*c = (c + a*c) + b*c + Distributivity, // c + (a*c + b*c) = (c + a*c) + b*c + addition.Associativity, Multiply>, // (c + a*c) + b*c = (c + a*c) + b*c + Refl, + ], this['left']>; + }; + export namespace spec { + export type distributivity = [ + assert>>, + assert>>, + ] + } + + // Associativity + export type Associativity = + Rewrite, C>, Multiply>>; + export interface Assoc_Base_Proof { + type: 'rewrite', + left: Equation, C>, Multiply<_1, Multiply>>; // (1*b)*c = 1*(b*c) + right: ChainRewrites<[ + IdentityR, // b*c = 1*(b*c) + IdentityR>, // b*c = b*c + Refl, + ], this['left']>; + }; + export interface Assoc_Inductive_Proof { + type: 'rewrite', + left: Equation, B>, C>, Multiply, Multiply>>; // (succ(a)*b)*c = succ(a)*(b*c) + right: ChainRewrites<[ + SuccLemma, // (b + a*b)*c = succ(a) * (b*c) + Distributivity, C>, // b*c + (a*b)*c = succ(a) * (b*c) + SuccLemma>, // b*c + (a*b)*c = b*c + a*(b*c) + Associativity, // b*c + a*(b*c) = b*c + a*(b*c) + Refl, + ], this['left']>; + }; + export namespace spec { + export type associativity = [ + assert>>, + assert>>, + ] + } +} diff --git a/src/tests.ts b/src/tests.ts deleted file mode 100644 index 7f331a6..0000000 --- a/src/tests.ts +++ /dev/null @@ -1,85 +0,0 @@ -import { addition, multiplication } from './index'; -import { Add, Multiply, Succ, _0 } from './nat'; -import { ApplyRewrite, ChainRewrites, Sym, Eq, VerifyEquation, Equation, assert, Evaluate } from './util'; - -export type specChainRewrites = [ - assert, - addition.Identity<'B'>, - ], - Add, 'C'> - >, - Add<'B', 'C'> - >>, - assert, - addition.Identity<'B'>, - Sym>>, - addition.Commutativity, _0>, - ], - Add, 'C'> - >, - Add<_0, Add<'B', 'C'>> - >>, -] - -export namespace spec_addition { - export type specIdentity = [ - assert>, addition.Identity<'B'>>, - Add<'A', 'B'> - >>, - assert, _0>, addition.Identity>>, - Add<'A', 'B'> - >>, - assert, Sym>>>, - Add, _0> - >>, - assert>>, addition.Identity<'C'>>, - Add<'A', Add<'B', 'C'>> - >>, - ] - - export type specCommutativity = [ - assert, addition.Commutativity<'A', 'B'>>, - Add<'B', 'A'> - >>, - assert, 'C'>, addition.Commutativity<'A', 'B'>>, - Add, 'C'> - >>, - assert>, addition.Commutativity<'B', 'C'>>, - Add<'A', Add<'C', 'B'>> - >>, - ] -} - -export namespace multiplication_spec { - export type specCommutativity = [ - assert, 'C'>, multiplication.Commutativity<'A', 'B'>>, - Multiply, 'C'> - >>, - ] - export type specDistributivity = [ - assert>, - Add, Multiply<'B', 'C'>> - >>, - ] - export type specAssociativity = [ - assert>, - Multiply<'A', Multiply<'B', 'C'>> - >>, - ] -} diff --git a/src/tests/nat.spec.ts b/src/tests/nat.spec.ts new file mode 100644 index 0000000..acade6f --- /dev/null +++ b/src/tests/nat.spec.ts @@ -0,0 +1,60 @@ +import { addition, multiplication } from '../natural-numbers'; +import { Add, Multiply, _0 } from '../utils/nat'; +import { ApplyRewrite, Sym, Eq, VerifyEquation, Equation, assert, Evaluate } from '../utils/theorem'; + +export namespace spec_addition { + export type specIdentity = [ + assert>, addition.Identity<'B'>>, + Add<'A', 'B'> + >>, + assert, _0>, addition.Identity>>, + Add<'A', 'B'> + >>, + assert, Sym>>>, + Add, _0> + >>, + assert>>, addition.Identity<'C'>>, + Add<'A', Add<'B', 'C'>> + >>, + ] + + export type specCommutativity = [ + assert, addition.Commutativity<'A', 'B'>>, + Add<'B', 'A'> + >>, + assert, 'C'>, addition.Commutativity<'A', 'B'>>, + Add, 'C'> + >>, + assert>, addition.Commutativity<'B', 'C'>>, + Add<'A', Add<'C', 'B'>> + >>, + ] +} + +export namespace multiplication_spec { + export type specCommutativity = [ + assert, 'C'>, multiplication.Commutativity<'A', 'B'>>, + Multiply, 'C'> + >>, + ] + export type specDistributivity = [ + assert>, + Add, Multiply<'B', 'C'>> + >>, + ] + export type specAssociativity = [ + assert>, + Multiply<'A', Multiply<'B', 'C'>> + >>, + ] +} diff --git a/src/tests/theorem.spec.ts b/src/tests/theorem.spec.ts new file mode 100644 index 0000000..4ab220a --- /dev/null +++ b/src/tests/theorem.spec.ts @@ -0,0 +1,28 @@ +import { addition } from '../natural-numbers'; +import { Add, _0 } from '../utils/nat'; +import { ApplyRewrite, ChainRewrites, Sym, Eq, VerifyEquation, Equation, assert, Evaluate } from '../utils/theorem'; + +export type specChainRewrites = [ + assert, + addition.Identity<'B'>, + ], + Add, 'C'> + >, + Add<'B', 'C'> + >>, + assert, + addition.Identity<'B'>, + Sym>>, + addition.Commutativity, _0>, + ], + Add, 'C'> + >, + Add<_0, Add<'B', 'C'>> + >>, +] diff --git a/src/util.ts b/src/util.ts deleted file mode 100644 index a4dd2e9..0000000 --- a/src/util.ts +++ /dev/null @@ -1,75 +0,0 @@ -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 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 DyadicOp, b: infer b extends string } ? `(${OpToStr} ${O['op']} ${b})` - : O extends { op: string, a: infer a extends string, b: infer b extends DyadicOp } ? `(${a} ${O['op']} ${OpToStr})` - : O extends { op: string, a: infer a extends DyadicOp, b: infer b extends DyadicOp } ? `(${OpToStr} ${O['op']} ${OpToStr})` - : O extends { op: string, a: infer a extends string } ? `${O['op']}(${a})` - : O extends { op: string, a: infer a extends DyadicOp } ? `${O['op']}(${OpToStr})` - : never; - -type RwType = 'rewrite' | 'imperative'; - -export interface RewriteBase { - type: RwType; - left: Op; - right: Op; - assume?: Record; -} - -export interface Rewrite extends RewriteBase { - type: Typ; - left: left; - right: right; -}; - -export type Sym = Rewrite; -export type Subst = Rewrite - -export type ApplyRewrite = - R['type'] extends 'imperative' ? (R & { left: O })['right'] - : O extends R['left'] ? R['right'] - : O extends string ? O - : O extends DyadicOp ? ( - ApplyRewrite extends O['a'] - ? (ApplyRewrite extends O['b'] ? O - : Omit & { b: ApplyRewrite }) - : Omit & { a: ApplyRewrite } - ) - : O extends MonadicOp ? ( - ApplyRewrite extends O['a'] ? O : Omit & { a: ApplyRewrite } - ) - : never; - -export type ChainRewrites = - Rws extends [] ? O - : Rws extends [infer R extends RewriteBase, ...infer Rs extends RewriteBase[]] - ? ChainRewrites> - : never; - -export type VerifyEquation = - Eq['right'] extends 'true' ? true : false & Eq['right']; - -export type Evaluate = ApplyRewrite; - -export type assert = T; -export type assertFalse = T; -export type Eq = ([a] extends [b] ? ([b] extends [a] ? true : false & { lhs: a; rhs: b }) : false & { lhs: a; rhs: b }); - -export type Equation = { op: '=', a: A, b: B }; - -export interface Refl extends RewriteBase { - type: 'imperative'; - left: Op; - right: this['left'] extends { op: '=', a: infer a, b: infer b } - ? (Eq extends true ? 'true' : this['left']) - : this['left']; -}; - -// Like Refl, but you have to specify the sides of the equation and this one works recursively -export type ReflR = Rewrite, 'true'>; diff --git a/src/utils/nat.ts b/src/utils/nat.ts new file mode 100644 index 0000000..af8f3da --- /dev/null +++ b/src/utils/nat.ts @@ -0,0 +1,10 @@ +import { Op } from './theorem'; + +export type Add = { op: '+'; a: A; b: B }; +export type Multiply = { op: '*'; a: A; b: B }; +export type Succ = { op: 'succ', a: A }; + +export type _0 = '0' +export type _1 = Succ<_0> +export type _2 = Succ<_1> +export type _3 = Succ<_2> diff --git a/src/utils/theorem.ts b/src/utils/theorem.ts new file mode 100644 index 0000000..a4dd2e9 --- /dev/null +++ b/src/utils/theorem.ts @@ -0,0 +1,75 @@ +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 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 DyadicOp, b: infer b extends string } ? `(${OpToStr} ${O['op']} ${b})` + : O extends { op: string, a: infer a extends string, b: infer b extends DyadicOp } ? `(${a} ${O['op']} ${OpToStr})` + : O extends { op: string, a: infer a extends DyadicOp, b: infer b extends DyadicOp } ? `(${OpToStr} ${O['op']} ${OpToStr})` + : O extends { op: string, a: infer a extends string } ? `${O['op']}(${a})` + : O extends { op: string, a: infer a extends DyadicOp } ? `${O['op']}(${OpToStr})` + : never; + +type RwType = 'rewrite' | 'imperative'; + +export interface RewriteBase { + type: RwType; + left: Op; + right: Op; + assume?: Record; +} + +export interface Rewrite extends RewriteBase { + type: Typ; + left: left; + right: right; +}; + +export type Sym = Rewrite; +export type Subst = Rewrite + +export type ApplyRewrite = + R['type'] extends 'imperative' ? (R & { left: O })['right'] + : O extends R['left'] ? R['right'] + : O extends string ? O + : O extends DyadicOp ? ( + ApplyRewrite extends O['a'] + ? (ApplyRewrite extends O['b'] ? O + : Omit & { b: ApplyRewrite }) + : Omit & { a: ApplyRewrite } + ) + : O extends MonadicOp ? ( + ApplyRewrite extends O['a'] ? O : Omit & { a: ApplyRewrite } + ) + : never; + +export type ChainRewrites = + Rws extends [] ? O + : Rws extends [infer R extends RewriteBase, ...infer Rs extends RewriteBase[]] + ? ChainRewrites> + : never; + +export type VerifyEquation = + Eq['right'] extends 'true' ? true : false & Eq['right']; + +export type Evaluate = ApplyRewrite; + +export type assert = T; +export type assertFalse = T; +export type Eq = ([a] extends [b] ? ([b] extends [a] ? true : false & { lhs: a; rhs: b }) : false & { lhs: a; rhs: b }); + +export type Equation = { op: '=', a: A, b: B }; + +export interface Refl extends RewriteBase { + type: 'imperative'; + left: Op; + right: this['left'] extends { op: '=', a: infer a, b: infer b } + ? (Eq extends true ? 'true' : this['left']) + : this['left']; +}; + +// Like Refl, but you have to specify the sides of the equation and this one works recursively +export type ReflR = Rewrite, 'true'>; -- cgit v1.3.1