From f6e26212620de411e082cbd52379075ea5a99032 Mon Sep 17 00:00:00 2001 From: Akshay Nair Date: Sun, 10 Dec 2023 16:15:00 +0530 Subject: init commit rewriting shit --- .gitignore | 4 ++++ LICENSE | 21 +++++++++++++++++++++ README.md | 2 ++ package.json | 15 +++++++++++++++ src/index.ts | 43 +++++++++++++++++++++++++++++++++++++++++++ src/nat.ts | 16 ++++++++++++++++ src/tests.ts | 39 +++++++++++++++++++++++++++++++++++++++ tsconfig.json | 10 ++++++++++ yarn.lock | 8 ++++++++ 9 files changed, 158 insertions(+) create mode 100644 .gitignore create mode 100644 LICENSE create mode 100644 README.md create mode 100644 package.json create mode 100644 src/index.ts create mode 100644 src/nat.ts create mode 100644 src/tests.ts create mode 100644 tsconfig.json create mode 100644 yarn.lock diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..e5c664e --- /dev/null +++ b/.gitignore @@ -0,0 +1,4 @@ +node_modules +*.log +*.map +dist/ diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..ba5b8af --- /dev/null +++ b/LICENSE @@ -0,0 +1,21 @@ +MIT License + +Copyright (c) 2023 Akshay Nair + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. diff --git a/README.md b/README.md new file mode 100644 index 0000000..ee7b099 --- /dev/null +++ b/README.md @@ -0,0 +1,2 @@ +# Theorem prover in ts types +Experiment to use typescript's type system for theorem proving diff --git a/package.json b/package.json new file mode 100644 index 0000000..a7d7598 --- /dev/null +++ b/package.json @@ -0,0 +1,15 @@ +{ + "name": "brainfuck-ts-types", + "version": "0.0.0", + "description": "__", + "main": "index.js", + "repository": "__", + "author": "Akshay Nair ", + "license": "MIT", + "scripts": { + "test": "tsc --noEmit ./src/tests.ts" + }, + "dependencies": { + "typescript": "^5.3.3" + } +} diff --git a/src/index.ts b/src/index.ts new file mode 100644 index 0000000..bd93300 --- /dev/null +++ b/src/index.ts @@ -0,0 +1,43 @@ +export type Op = string | { op: string; a: Op; b: Op }; + +export type Rewrite = { + type: 'rewrite'; + left: left; + right: right; +}; +export type RewriteKind = Rewrite; + +export type Flip = Rewrite; + +export type ApplyRewrite = + O extends R['left'] ? R['right'] + : O extends string ? O + : O extends { a: Op, b: Op, op: string } ? ( + ApplyRewrite extends O['a'] + ? Omit & { b: ApplyRewrite } + : Omit & { a: ApplyRewrite } + ) + : never; + +export type Add = { op: '+'; a: a; b: b }; + +export type Identity = Rewrite, A>; +export type Commutativity = Rewrite, Add>; + +// type _x = ApplyRewrite, Identity<'0'>>; + +// type Assoc = + +/* + +Assoc: (a + b) + c = a + (b + c) + +For a = 0, +(0 + b) + c += b + c += 0 + (b + c) + +For a = succ(), + +*/ + diff --git a/src/nat.ts b/src/nat.ts new file mode 100644 index 0000000..86bd318 --- /dev/null +++ b/src/nat.ts @@ -0,0 +1,16 @@ +declare const prev: unique symbol + +export type _nat = number & { [prev]: _nat | null } +export type Succ = number & { [prev]: n } +export type Pred = n extends _0 ? n : n[typeof prev] +export type Nat = _0 | Succ<_nat> + +export type _0 = 0 & { [prev]: null } +export type _1 = Succ<_0> +export type _2 = Succ<_1> +export type _3 = Succ<_2> +export type _4 = Succ<_3> +export type _5 = Succ<_4> +export type _6 = Succ<_5> +export type _7 = Succ<_6> +export type _8 = Succ<_7> diff --git a/src/tests.ts b/src/tests.ts new file mode 100644 index 0000000..8c379e8 --- /dev/null +++ b/src/tests.ts @@ -0,0 +1,39 @@ +import { Add, ApplyRewrite, Commutativity, Flip, Identity } from './index'; + +type Eq = ([a] extends [b] ? ([b] extends [a] ? true : false) : false) & { a: a; b: b }; +type assert = T; + +export type _testCases = { + Identity: [ + assert>, Identity<'B'>>, + Add<'A', 'B'> + >>, + assert, '0'>, Identity>>, + Add<'A', 'B'> + >>, + assert, Flip>>>, + Add, '0'> + >>, + assert>>, Identity<'C'>>, + Add<'A', Add<'B', 'C'>> + >>, + ], + Commutativity: [ + assert, Commutativity<'A', 'B'>>, + Add<'B', 'A'> + >>, + assert, 'C'>, Commutativity<'A', 'B'>>, + Add, 'C'> + >>, + assert>, Commutativity<'B', 'C'>>, + Add<'A', Add<'C', 'B'>> + >>, + ], +}; diff --git a/tsconfig.json b/tsconfig.json new file mode 100644 index 0000000..3ffa57b --- /dev/null +++ b/tsconfig.json @@ -0,0 +1,10 @@ +{ + "compilerOptions": { + "target": "es2016", + "module": "commonjs", + "esModuleInterop": true, + "forceConsistentCasingInFileNames": true, + "strict": true, + "skipLibCheck": true + } +} diff --git a/yarn.lock b/yarn.lock new file mode 100644 index 0000000..cd07bce --- /dev/null +++ b/yarn.lock @@ -0,0 +1,8 @@ +# THIS IS AN AUTOGENERATED FILE. DO NOT EDIT THIS FILE DIRECTLY. +# yarn lockfile v1 + + +typescript@^5.3.3: + version "5.3.3" + resolved "https://registry.yarnpkg.com/typescript/-/typescript-5.3.3.tgz#b3ce6ba258e72e6305ba66f5c9b452aaee3ffe37" + integrity sha512-pXWcraxM0uxAS+tN0AG/BF2TyqmHO014Z070UsJ+pFvYuRSq8KH8DmWpnbXe0pEPDHXZV3FcAbJkijJ5oNEnWw== -- cgit v1.3.1