commit c1af7bda259979388446a10afbbccf6398fd2adf Author: cannorin Date: Sat Feb 15 01:50:40 2025 +0900 Initial commit diff --git a/.editorconfig b/.editorconfig new file mode 100644 index 0000000..c6c8b36 --- /dev/null +++ b/.editorconfig @@ -0,0 +1,9 @@ +root = true + +[*] +indent_style = space +indent_size = 2 +end_of_line = lf +charset = utf-8 +trim_trailing_whitespace = true +insert_final_newline = true diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..9b1ee42 --- /dev/null +++ b/.gitignore @@ -0,0 +1,175 @@ +# Based on https://raw.githubusercontent.com/github/gitignore/main/Node.gitignore + +# Logs + +logs +_.log +npm-debug.log_ +yarn-debug.log* +yarn-error.log* +lerna-debug.log* +.pnpm-debug.log* + +# Caches + +.cache + +# Diagnostic reports (https://nodejs.org/api/report.html) + +report.[0-9]_.[0-9]_.[0-9]_.[0-9]_.json + +# Runtime data + +pids +_.pid +_.seed +*.pid.lock + +# Directory for instrumented libs generated by jscoverage/JSCover + +lib-cov + +# Coverage directory used by tools like istanbul + +coverage +*.lcov + +# nyc test coverage + +.nyc_output + +# Grunt intermediate storage (https://gruntjs.com/creating-plugins#storing-task-files) + +.grunt + +# Bower dependency directory (https://bower.io/) + +bower_components + +# node-waf configuration + +.lock-wscript + +# Compiled binary addons (https://nodejs.org/api/addons.html) + +build/Release + +# Dependency directories + +node_modules/ +jspm_packages/ + +# Snowpack dependency directory (https://snowpack.dev/) + +web_modules/ + +# TypeScript cache + +*.tsbuildinfo + +# Optional npm cache directory + +.npm + +# Optional eslint cache + +.eslintcache + +# Optional stylelint cache + +.stylelintcache + +# Microbundle cache + +.rpt2_cache/ +.rts2_cache_cjs/ +.rts2_cache_es/ +.rts2_cache_umd/ + +# Optional REPL history + +.node_repl_history + +# Output of 'npm pack' + +*.tgz + +# Yarn Integrity file + +.yarn-integrity + +# dotenv environment variable files + +.env +.env.development.local +.env.test.local +.env.production.local +.env.local + +# parcel-bundler cache (https://parceljs.org/) + +.parcel-cache + +# Next.js build output + +.next +out + +# Nuxt.js build / generate output + +.nuxt +dist + +# Gatsby files + +# Comment in the public line in if your project uses Gatsby and not Next.js + +# https://nextjs.org/blog/next-9-1#public-directory-support + +# public + +# vuepress build output + +.vuepress/dist + +# vuepress v2.x temp and cache directory + +.temp + +# Docusaurus cache and generated files + +.docusaurus + +# Serverless directories + +.serverless/ + +# FuseBox cache + +.fusebox/ + +# DynamoDB Local files + +.dynamodb/ + +# TernJS port file + +.tern-port + +# Stores VSCode versions used for testing VSCode extensions + +.vscode-test + +# yarn v2 + +.yarn/cache +.yarn/unplugged +.yarn/build-state.yml +.yarn/install-state.gz +.pnp.* + +# IntelliJ based IDEs +.idea + +# Finder (MacOS) folder config +.DS_Store diff --git a/.vscode/settings.json b/.vscode/settings.json new file mode 100644 index 0000000..915c8bc --- /dev/null +++ b/.vscode/settings.json @@ -0,0 +1,16 @@ +{ + "editor.formatOnSave": true, + "typescript.tsdk": "node_modules/typescript/lib", + "[typescript]": { + "editor.defaultFormatter": "biomejs.biome" + }, + "[javascript]": { + "editor.defaultFormatter": "biomejs.biome" + }, + "[json]": { + "editor.defaultFormatter": "biomejs.biome" + }, + "[jsonc]": { + "editor.defaultFormatter": "biomejs.biome" + } +} diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..026ea12 --- /dev/null +++ b/LICENSE @@ -0,0 +1,21 @@ +MIT License + +Copyright (c) 2024 cannorin + +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..fcbcd10 --- /dev/null +++ b/README.md @@ -0,0 +1,90 @@ +# KRIPKE + +## Setup + +To install dependencies: + +```bash +bun install +``` + +To run: + +```bash +bun run index.ts +``` + +This project was created using `bun init` in bun v1.1.33. [Bun](https://bun.sh) is a fast all-in-one JavaScript runtime. + +## Rules + +* A Kripke frame with 4 worlds are generated, +* You have a total of 10 moves. In each move you can do one of the following: + - Enter a modal formula. + - The game tells you in how many worlds the formula is valid (for every valuation). + - Guess the Kripke frame. + - If your frame is equal or isomorphic to the secret frame, you win. +* You lose when you run out of moves. + +A typical gameplay looks like this: +``` +Run !help for available commands. +A new Kripke frame is created! It has 4 worlds and 4 relations. +[10] Lp -> p +valid in 1 worlds, invalid in the rest. +[9] ~L0 +valid in 3 worlds, invalid in the rest. +[8] ML0 +valid in 1 worlds, invalid in the rest. +[7] (Lp -> p) & ML0 +invalid. +[6] M(Lp -> p) & ML0 +invalid. +[5] M(Lp -> p) +valid in 2 worlds, invalid in the rest. +[4] !guess aRa, bRc, bRd, dRa +incorrect. +[3] !guess aRa, bRc, dRa, dRb +incorrect. +[2] !guess aRa, bRc, dRa, dRc +incorrect. +[1] !guess aRa, bRc, dRa, aRd +correct! congratuations!! +id: 389 +a ==> a +a ==> c +b ==> d +c ==> a +``` + +## Syntax + +See `syntax.ts` for details. + +### Formulae + +You may use the following symbols: +* propositional variables, `p`, `q`, `r`, `s` (four are enough) +* verum: `T`, `⊤`, `1`, `\top` +* falsum: `F`, `⊥`, `0`, `\bot` +* negation: `~`, `¬`, `\neg`, `\lnot` +* box modality: `[]`, `□`, `L`, `\Box` +* diamond modality: `<>`, `⋄`, `M`, `\Diamond` +* conjunction: `&`, `^`, `∧`, `\wedge`, `\land` +* disjunction: `|`, `v`, `∨`, `\vee`, `\lor` +* implication: `->`, `→`, `\rightarrow`, `\to`, `\implies` +* equivalence: `<->`, `↔`, `\leftrightarrow`, `\iff` +* parentheses: `(`, `)` + +All operators are right associative. + +### Frames + +You may use the following symbols: +* worlds: `a`, `b`, `c`, `d` +* accessibility relation: `R`, `<`, `≺`, `\prec` +* comma: `,` (to separate relations) + +## License + +MIT diff --git a/biome.json b/biome.json new file mode 100644 index 0000000..c5ca063 --- /dev/null +++ b/biome.json @@ -0,0 +1,49 @@ +{ + "$schema": "https://biomejs.dev/schemas/1.9.1/schema.json", + "vcs": { + "enabled": true, + "clientKind": "git", + "useIgnoreFile": true + }, + "files": { + "ignoreUnknown": false, + "ignore": [".env", ".env.*", ".yarn/**/*", "*.*css"] + }, + "formatter": { + "enabled": true, + "indentStyle": "space" + }, + "organizeImports": { + "enabled": true + }, + "linter": { + "enabled": true, + "rules": { + "recommended": true + } + }, + "javascript": { + "formatter": { + "quoteStyle": "double" + } + }, + "overrides": [ + { + "include": ["*.svelte", "*.md"], + "linter": { + "rules": { + "correctness": { + "noUnusedLabels": "off" + }, + "suspicious": { + "noConfusingLabels": "off" + }, + "style": { + "useConst": "off", + "useImportType": "off" + } + } + } + } + ] +} diff --git a/bun.lockb b/bun.lockb new file mode 100755 index 0000000..2a11a3e Binary files /dev/null and b/bun.lockb differ diff --git a/global.d.ts b/global.d.ts new file mode 100644 index 0000000..5912f19 --- /dev/null +++ b/global.d.ts @@ -0,0 +1,36 @@ +interface String { + startsWith(searchString: S): this is `${S}${string}`; + endsWith(searchString: S): this is `${string}${S}`; + includes( + searchString: S, + position?: number, + ): this is `${string}${S}${string}`; +} + +type LiteralUnionLike = T extends string + ? T extends "" + ? T + : T extends `${T}${T}` + ? never + : T + : T extends number + ? `${T}0` extends `${number}` + ? T + : never + : T extends null | undefined + ? T + : never; + +interface Array { + includes( + searchElement: T extends LiteralUnionLike ? unknown : never, + fromIndex?: number, + ): searchElement is T extends LiteralUnionLike ? T : never; +} + +interface ReadonlyArray { + includes( + searchElement: T extends LiteralUnionLike ? unknown : never, + fromIndex?: number, + ): searchElement is T extends LiteralUnionLike ? T : never; +} diff --git a/index.ts b/index.ts new file mode 100644 index 0000000..247f322 --- /dev/null +++ b/index.ts @@ -0,0 +1,107 @@ +import { parse, parseFrame } from "./parser"; +import { + type Frame, + canonicals, + getFrame, + getId, + left, + mapping, + right, + validWorlds, + worlds, +} from "./semantics"; +import { sample } from "./utils"; + +import { stdin, stdout } from "node:process"; +import * as readline from "node:readline"; + +let frame: Frame = { relations: new Set() }; +let count = 0; + +const reset = () => { + frame = getFrame(sample(canonicals, 1)[0]); + count = 10; + console.log( + `A new Kripke frame is created! It has 4 worlds and ${frame.relations.size} relations.`, + ); +}; + +const show = () => { + console.log(`id: ${getId(frame)}`); + for (const rel of frame.relations) { + console.log(`${left(rel)} ==> ${right(rel)}`); + } +}; + +const query = (expr: string) => { + const fml = parse(expr); + return validWorlds(frame, fml).length; +}; + +const guess = (expr: string) => { + const relations = parseFrame(expr); + const id = mapping[getId({ relations })]; + return id === getId(frame); +}; + +const gameover = () => { + console.log("game over!"); + show(); + reset(); +}; + +const help = () => { + console.log(" ... check if the formula is valid in the frame"); + console.log("!guess ... guess the frame"); + console.log("!reset ... abandon this frame and start over"); + console.log("!show ... see the frame (CHEAT)"); + console.log("!help ... show this"); + console.log("!exit ... bye bye"); +}; + +const rl = readline.createInterface({ input: stdin, output: stdout }); +console.log("Run !help for available commands."); +reset(); +rl.setPrompt(`[${count}] `); +rl.on("line", (line) => { + const input = line.trim(); + if (input.startsWith("!reset")) reset(); + else if (input.startsWith("!show")) show(); + else if (input.startsWith("!exit")) rl.close(); + else if (input.startsWith("!help")) help(); + else if (input.startsWith("!guess")) { + const expr = input.replace("!guess", "").trim(); + try { + if (guess(expr)) { + console.log("correct! congratuations!!"); + show(); + reset(); + } else { + console.log("incorrect."); + count = count - 1; + } + } catch (e) { + console.log("invalid frame expression."); + console.log("example: aRa, aRb, bRb"); + } + } else { + try { + const num = query(input); + if (num === 0) { + console.log("invalid."); + } else if (num < worlds.length) { + console.log(`valid in ${num} worlds, invalid in the rest.`); + } else { + console.log("valid!"); + } + count = count - 1; + } catch (e) { + console.log("invalid formula"); + console.log("example: Mp -> LMp"); + } + } + if (count === 0) gameover(); + rl.setPrompt(`[${count}] `); + rl.prompt(); +}).on("close", () => process.exit(0)); +rl.prompt(); diff --git a/package.json b/package.json new file mode 100644 index 0000000..f8b9ba3 --- /dev/null +++ b/package.json @@ -0,0 +1,19 @@ +{ + "name": "kripke", + "module": "index.ts", + "devDependencies": { + "@types/bun": "latest" + }, + "peerDependencies": { + "typescript": "^5.0.0" + }, + "scripts": { + "lint": "biome check", + "fix": "biome check --fix" + }, + "type": "module", + "dependencies": { + "@biomejs/biome": "^1.9.4", + "typescript-parsec": "^0.3.4" + } +} diff --git a/parser.ts b/parser.ts new file mode 100644 index 0000000..c05a9da --- /dev/null +++ b/parser.ts @@ -0,0 +1,184 @@ +import { + type Token, + alt, + apply, + buildLexer, + expectEOF, + expectSingleResult, + kmid, + lrec_sc, + rule, + seq, + tok, +} from "typescript-parsec"; +import { type Relation, worlds } from "./semantics"; +import { + type Formula, + and, + bot, + box, + diamond, + iff, + not, + or, + propVars, + propvar, + to, + top, +} from "./syntax"; + +enum TokenKind { + PropVar = 0, + Top = 1, + Bot = 2, + Not = 3, + Box = 4, + Diamond = 5, + And = 6, + Or = 7, + To = 8, + Iff = 9, + LParen = 10, + RParen = 11, + Space = 12, +} + +const lexer = buildLexer([ + [true, /^[pqrs]/g, TokenKind.PropVar], + [true, /^(T|⊤|1|\\top)/g, TokenKind.Top], + [true, /^(F|⊥|0|\\bot)/g, TokenKind.Bot], + [true, /^(~|¬|\\neg|\\lnot)/g, TokenKind.Not], + [true, /^(\[\]|□|L|\\Box)/g, TokenKind.Box], + [true, /^(<>|⋄|M|\\Diamond)/g, TokenKind.Diamond], + [true, /^(&|\^|∧|\\wedge|\\land)/g, TokenKind.And], + [true, /^(\||v|∨|\\vee|\\lor)/g, TokenKind.Or], + [true, /^(->|→|\\rightarrow|\\to|\\implies)/g, TokenKind.To], + [true, /^(<->|↔|\\leftrightarrow|\\iff)/g, TokenKind.Iff], + [true, /^(\(|\\left\()/g, TokenKind.LParen], + [true, /^(\)|\\right\))/g, TokenKind.RParen], + [false, /^\s+/g, TokenKind.Space], +]); + +function atom( + value: Token, +): Formula { + switch (value.kind) { + case TokenKind.PropVar: { + if (propVars.includes(value.text)) { + return propvar(value.text); + } + throw new Error(`Unknown atom: ${value.text}`); + } + case TokenKind.Top: + return top; + case TokenKind.Bot: + return bot; + default: + throw new Error(`Unknown atom: ${value.text}`); + } +} + +function unary([op, value]: [ + Token, + Formula, +]): Formula { + switch (op.kind) { + case TokenKind.Not: + return not(value); + case TokenKind.Box: + return box(value); + case TokenKind.Diamond: + return diamond(value); + default: + throw new Error(`Unknown unary operator: ${op.text}`); + } +} + +function binary( + left: Formula, + [op, right]: [ + Token, + Formula, + ], +): Formula { + switch (op.kind) { + case TokenKind.And: + return and(left, right); + case TokenKind.Or: + return or(left, right); + case TokenKind.To: + return to(left, right); + case TokenKind.Iff: + return iff(left, right); + default: + throw new Error(`Unknown binary operator: ${op.text}`); + } +} + +const TERM = rule(); +const ANDOR = rule(); +const EXP = rule(); + +TERM.setPattern( + alt( + apply( + alt(tok(TokenKind.PropVar), tok(TokenKind.Top), tok(TokenKind.Bot)), + atom, + ), + apply( + seq( + alt(tok(TokenKind.Not), tok(TokenKind.Box), tok(TokenKind.Diamond)), + TERM, + ), + unary, + ), + kmid(tok(TokenKind.LParen), EXP, tok(TokenKind.RParen)), + ), +); + +ANDOR.setPattern( + lrec_sc(TERM, seq(alt(tok(TokenKind.And), tok(TokenKind.Or)), ANDOR), binary), +); + +EXP.setPattern( + lrec_sc(ANDOR, seq(alt(tok(TokenKind.To), tok(TokenKind.Iff)), EXP), binary), +); + +export function parse(expr: string): Formula { + return expectSingleResult(expectEOF(EXP.parse(lexer.parse(expr)))); +} + +const frameLexer = buildLexer([ + [true, /^[abcd]/g, "world" as const], + [true, /^(R|<|≺|\\prec)/g, "relation" as const], + [true, /^,/g, "separator" as const], + [false, /^\s+/g, "spaces" as const], +]); + +const RELATION = rule< + "world" | "relation" | "separator" | "spaces", + Set +>(); +RELATION.setPattern( + apply(seq(tok("world"), tok("relation"), tok("world")), ([x, _r, y]) => { + const w1 = x.text; + const w2 = y.text; + if (!worlds.includes(w1) || !worlds.includes(w2)) throw new Error(); + return new Set([`${w1}${w2}`]); + }), +); +const RELATIONS = rule< + "world" | "relation" | "separator" | "spaces", + Set +>(); +RELATIONS.setPattern( + lrec_sc( + RELATION, + seq(tok("separator"), RELATIONS), + (l, [_s, r]) => new Set([...l, ...r]), + ), +); + +export function parseFrame(expr: string): Set { + return expectSingleResult(expectEOF(RELATIONS.parse(frameLexer.parse(expr)))); +} diff --git a/semantics.ts b/semantics.ts new file mode 100644 index 0000000..cb96c4a --- /dev/null +++ b/semantics.ts @@ -0,0 +1,168 @@ +import { type Formula, type PropVar, and, propVars, vars } from "./syntax"; +import { decode, encode, permutations, power } from "./utils"; + +export const worlds = ["a", "b", "c", "d"] as const; + +export type World = (typeof worlds)[number]; + +export type Relation = `${World}${World}`; +export const left = (rel: Relation) => rel[0] as World; +export const right = (rel: Relation) => rel[1] as World; + +export const relation: Relation[] = worlds.flatMap((w) => + worlds.map((x) => `${w}${x}` as const), +); + +export interface Frame { + relations: Set; +} + +export interface Model extends Frame { + valuations: Set<`${World}${PropVar}`>; +} + +export function valuation(fml?: Formula): `${World}${PropVar}`[] { + const vs = fml ? Array.from(vars(fml)) : propVars; + return worlds.flatMap((w) => vs.map((p) => `${w}${p}` as const)); +} + +export function satisfy(m: Model, w: World, fml: Formula): boolean { + switch (fml.type) { + case "top": + return true; + case "bot": + return false; + case "propvar": + return m.valuations.has(`${w}${fml.name}`); + case "not": + return !satisfy(m, w, fml.fml); + case "box": { + for (const rel of m.relations.values()) { + if (left(rel) !== w) continue; + if (!satisfy(m, right(rel), fml.fml)) return false; + } + return true; + } + case "diamond": { + for (const rel of m.relations.values()) { + if (left(rel) !== w) continue; + if (satisfy(m, right(rel), fml.fml)) return true; + } + return false; + } + case "to": { + if (!satisfy(m, w, fml.left)) return true; + return satisfy(m, w, fml.right); + } + case "or": { + if (satisfy(m, w, fml.left)) return true; + return satisfy(m, w, fml.right); + } + case "and": { + if (!satisfy(m, w, fml.left)) return false; + return satisfy(m, w, fml.right); + } + case "iff": { + return satisfy(m, w, fml.left) === satisfy(m, w, fml.right); + } + } +} + +export const validInModel = (m: Model, fml: Formula) => + worlds.every((w) => satisfy(m, w, fml)); + +export function validInFrame(f: Frame, fml: Formula) { + for (const valuations of power(valuation(fml))) { + if (!validInModel({ ...f, valuations }, fml)) return false; + } + return true; +} + +export function validWorlds(f: Frame, fml: Formula) { + const result: World[] = []; + for (const w of worlds) { + let valid = true; + for (const valuations of power(valuation(fml))) { + if (!satisfy({ ...f, valuations }, w, fml)) { + valid = false; + break; + } + } + if (valid) result.push(w); + } + return result; +} + +export function getFrame(id: number): Frame { + return { relations: decode(relation, id) }; +} + +export function getId(frame: Frame) { + return encode(relation, frame.relations); +} + +const worldPermutations = permutations(worlds).map( + (perm) => new Map(worlds.map((k, i) => [k, perm[i]])), +); + +function applyPermutation( + frame: T, + permutation: Map, +) { + const relations = new Set(); + for (const rel of frame.relations) { + const l = left(rel); + const r = right(rel); + relations.add( + `${permutation.get(l) ?? l}${permutation.get(r) ?? r}` as Relation, + ); + } + return { ...frame, relations } as T; +} + +export function generateAllFrames() { + const canonicals: number[] = []; + const map = new Map(); + + const stats = { + equivalentPerRelations: new Uint16Array(relation.length), + }; + stats.equivalentPerRelations.fill(0); + + const total = 2 ** relation.length; + for (let id = 0; id < total; id++) { + if (map.has(id)) continue; + + const relations = decode(relation, id); + const frame = { relations }; + const equivalentIds: number[] = []; + + let canonicalId = id; + for (const perm of worldPermutations) { + const permuted = applyPermutation(frame, perm); + const permutedId = encode(relation, permuted.relations); + equivalentIds.push(permutedId); + if (canonicalId === null || permutedId < canonicalId) { + canonicalId = permutedId; + } + } + + canonicals.push(canonicalId); + for (const equivalentId of equivalentIds) { + map.set(equivalentId, canonicalId); + } + stats.equivalentPerRelations[relations.size]++; + } + + const mapping: Uint16Array = new Uint16Array(total); + for (let id = 0; id < total; id++) { + const value = map.get(id); + if (value === undefined) throw Error(`impossible (${id})`); + mapping[id] = value; + } + + return { canonicals, mapping, stats }; +} + +const { canonicals, mapping } = generateAllFrames(); +export { canonicals, mapping }; diff --git a/syntax.ts b/syntax.ts new file mode 100644 index 0000000..df01341 --- /dev/null +++ b/syntax.ts @@ -0,0 +1,53 @@ +export type PropVar = "p" | "q" | "r" | "s"; + +export const propVars: PropVar[] = ["p", "q", "r", "s"]; + +export type Formula = + | { type: "top" | "bot" } + | { type: "propvar"; name: PropVar } + | { type: "not" | "box" | "diamond"; fml: Formula } + | { + type: "to" | "or" | "and" | "iff"; + left: Formula; + right: Formula; + }; + +export function vars(fml: Formula): Set { + switch (fml.type) { + case "top": + case "bot": + return new Set(); + case "box": + case "diamond": + case "not": + return vars(fml.fml); + case "to": + case "or": + case "and": + case "iff": + return new Set([...vars(fml.left), ...vars(fml.right)]); + case "propvar": + return new Set([fml.name]); + } +} + +export const propvar = (name: PropVar) => ({ type: "propvar", name }) as const; + +export const top = { type: "top" } as const satisfies Formula; +export const bot = { type: "bot" } as const satisfies Formula; + +export const box = (fml: Formula) => + ({ type: "box", fml }) as const satisfies Formula; +export const diamond = (fml: Formula) => + ({ type: "diamond", fml }) as const satisfies Formula; +export const not = (fml: Formula) => + ({ type: "not", fml }) as const satisfies Formula; + +export const to = (left: Formula, right: Formula) => + ({ type: "to", left, right }) as const satisfies Formula; +export const and = (left: Formula, right: Formula) => + ({ type: "and", left, right }) as const satisfies Formula; +export const or = (left: Formula, right: Formula) => + ({ type: "or", left, right }) as const satisfies Formula; +export const iff = (left: Formula, right: Formula) => + ({ type: "iff", left, right }) as const satisfies Formula; diff --git a/tsconfig.json b/tsconfig.json new file mode 100644 index 0000000..2bb153e --- /dev/null +++ b/tsconfig.json @@ -0,0 +1,24 @@ +{ + "compilerOptions": { + // Enable latest features + "lib": ["ESNext", "DOM"], + "target": "ESNext", + "module": "ESNext", + "moduleDetection": "force", + "jsx": "react-jsx", + "allowJs": true, + // Bundler mode + "moduleResolution": "bundler", + "allowImportingTsExtensions": true, + "verbatimModuleSyntax": true, + "noEmit": true, + // Best practices + "strict": true, + "skipLibCheck": true, + "noFallthroughCasesInSwitch": true, + // Some stricter flags (disabled by default) + "noUnusedLocals": false, + "noUnusedParameters": false, + "noPropertyAccessFromIndexSignature": false + } +} diff --git a/utils.ts b/utils.ts new file mode 100644 index 0000000..ae09ddb --- /dev/null +++ b/utils.ts @@ -0,0 +1,51 @@ +const bitIsSet = (num: number, pos: number) => (num & (1 << pos)) !== 0; + +export function encode(all: readonly T[], set: Set): number { + let flags = 0; + for (let i = 0; i < all.length; i++) { + if (set.has(all[i])) { + flags |= 1 << i; + } + } + return flags; +} + +export function decode(all: readonly T[], flags: number): Set { + const total = 2 ** all.length; + if (flags < 0 || flags >= total) throw Error("invalid flags"); + const decoded = new Set(); + for (let j = 0; j < all.length; j++) { + if (bitIsSet(flags, j)) decoded.add(all[j]); + } + return decoded; +} + +export function* power(xs: readonly T[]) { + const total = 2 ** xs.length; + for (let i = 0; i < total; i++) { + yield decode(xs, i); + } +} + +export function permutations(arr: readonly T[]): T[][] { + if (arr.length === 0) return [[]]; + const result: T[][] = []; + for (let i = 0; i < arr.length; i++) { + const current = arr[i]; + const remaining = [...arr.slice(0, i), ...arr.slice(i + 1)]; + for (const perm of permutations(remaining)) { + result.push([current, ...perm]); + } + } + return result; +} + +export function sample(arr: readonly T[], n: number = arr.length): T[] { + if (n > arr.length) return sample(arr, arr.length); + const copy = [...arr]; + for (let i = 0; i < n; i++) { + const j = i + Math.floor(Math.random() * (copy.length - i)); + [copy[i], copy[j]] = [copy[j] as T, copy[i] as T]; + } + return copy.slice(0, n); +}