From 8ae8d7ab84d2ee38ee7cea4ff41598d135a9dc25 Mon Sep 17 00:00:00 2001 From: Akshay Nair Date: Fri, 15 Dec 2023 18:17:43 +0530 Subject: refactor: add support for imperative rewrites to make Refl more generic --- src/index.ts | 30 +++++++++++++++--------------- src/util.ts | 45 +++++++++++++++++++++++++++++---------------- 2 files changed, 44 insertions(+), 31 deletions(-) (limited to 'src') diff --git a/src/index.ts b/src/index.ts index 7a3f717..75e97be 100644 --- a/src/index.ts +++ b/src/index.ts @@ -17,7 +17,7 @@ export namespace addition { right: ChainRewrites<[ IdentityR, // b = b + 0 Sym>, // b + 0 = b + 0 - Refl>, // true + Refl, ], this['left']>; }; export interface Comm_Inductive_Proof { @@ -27,7 +27,7 @@ export namespace addition { SumSucc, // succ(a + b) = b + succ(a) Commutativity, // succ(b + a) = b + succ(a) SumSuccR, // succ(b + a) = succ(b + a) - Refl>>, // true + Refl, ], this['left']>; }; export namespace spec { @@ -46,7 +46,7 @@ export namespace addition { Commutativity<_0, B>, // (b + 0) + c = 0 + (b + c) Identity, // b + c = 0 + (b + c) IdentityR>, // b + c = b + c - Refl>, // true + Refl, ], this['left']>; }; export interface Assoc_Inductive_Proof { @@ -57,7 +57,7 @@ export namespace addition { SumSucc>, // succ(a + b) + c = succ(a + (b + c)) SumSucc, C>, // succ((a + b) + c) = succ(a + (b + c)) Associativity, // succ(a + (b + c)) = succ(a + (b + c)) - Refl>>>, // true + Refl, ], this['left']>; }; @@ -85,7 +85,7 @@ export namespace multiplication { right: ChainRewrites<[ IdentityR, // b = b * 1 Identity, // b = b - Refl, // true + Refl, ], this['left']>; }; export interface Comm_Inductive_Proof { @@ -95,7 +95,7 @@ export namespace multiplication { MulSucc, // b + a*b = b*succ(a) MulSuccR, // b + a*b = b + b*a Commutativity, // b + a*b = b + a*b - Refl>>, // true + Refl, ], this['left']>; }; export namespace spec { @@ -116,19 +116,19 @@ export namespace multiplication { addition.SumSucc<_0, B>, // succ(0 + b)*c = c + b*c addition.IdentityR, // succ(b)*c = c + b*c MulSucc, // c + b*c = c + b*c - Refl>>, // true + 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.SumSucc, // succ(a + b)*c = succ(a)*c + b*c + addition.SumSucc, // succ(a + b)*c = succ(a)*c + b*c MulSucc, C>, // c + (a + b)*c = succ(a)*c + b*c MulSucc, // 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, Multiply>>>, // true + Refl, ], this['left']>; }; export namespace spec { @@ -147,18 +147,18 @@ export namespace multiplication { right: ChainRewrites<[ IdentityR, // b*c = 1*(b*c) IdentityR>, // b*c = b*c - Refl>, // true + 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<[ - MulSucc, // (b + a*b)*c = succ(a) * (b*c) - Distributivity, C>, // b*c + (a*b)*c = succ(a) * (b*c) - MulSucc>, // b*c + (a*b)*c = b*c + a*(b*c) - Associativity, // b*c + a*(b*c) = b*c + a*(b*c) - Refl, Multiply>>>, // true + MulSucc, // (b + a*b)*c = succ(a) * (b*c) + Distributivity, C>, // b*c + (a*b)*c = succ(a) * (b*c) + MulSucc>, // 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 { diff --git a/src/util.ts b/src/util.ts index 1bed44b..c78c12c 100644 --- a/src/util.ts +++ b/src/util.ts @@ -1,15 +1,24 @@ export type Op = string | { op: string; a: Op; b: Op }; -export type Rewrite = { - type: 'rewrite'; +type RwType = 'rewrite' | 'imperative'; + +export interface RewriteBase { + type: RwType; + left: Op; + right: Op; +} + +export interface Rewrite extends RewriteBase { + type: Typ; left: left; right: right; }; -export type Sym> = Rewrite; +export type Sym = Rewrite; -export type ApplyRewrite> = - O extends R['left'] ? R['right'] +export type ApplyRewrite = + R['type'] extends 'imperative' ? (R & { left: O })['right'] + : O extends R['left'] ? R['right'] : O extends string ? O : O extends { a: Op, b: Op, op: string } ? ( ApplyRewrite extends O['a'] @@ -19,25 +28,29 @@ export type ApplyRewrite> = ) : never; -export interface Kind { - _: V; - return: R; -} -export type Ap = (K & { _: V })['return']; - -export type ChainRewrites[], O extends Op> = +export type ChainRewrites = Rws extends [] ? O - : Rws extends [infer R extends Rewrite, ...infer Rs extends Rewrite[]] + : Rws extends [infer R extends RewriteBase, ...infer Rs extends RewriteBase[]] ? ChainRewrites> : never; -export type VerifyEquation> = +export type VerifyEquation = Eq['right'] extends 'true' ? true : false & Eq['right']; -export type Evaluate> = ApplyRewrite; +export type Evaluate = ApplyRewrite; export type assert = 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 type Refl = Rewrite, 'true'>; + +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