From 4987fce65a75c4aae31c89ecd62a3f4ecf1f98ac Mon Sep 17 00:00:00 2001 From: "Robert J. Simmons" <442315+robsimmons@users.noreply.github.com> Date: Wed, 27 Nov 2024 16:39:52 -0500 Subject: [PATCH] Adjust API (#78) A number of changes for backwards compatibility in the API and for usability in other situations - add a UMD export - (backwards incompatible) move `get` and `lookup` in solutions to return numbers for integers, and add `getBig` and `lookupBig` which return bigint. - (backwards incompatible) turn `solutions` back into a getter with a deprecation warning, and make `solve()` mimic the behavior of the old solutions getter and the current `[Symbol.iterator]` method. - add `all()` to the solution iterator, which returns all remaining solutions as an array --- .gitignore | 1 + package.json | 6 +- src/cli.ts | 5 +- src/client.test.ts | 2 +- src/client.ts | 215 +++++++++++++++++++++++++++++------------- src/global.ts | 16 ++++ src/termoutput.ts | 38 ++++++-- src/web/Inspector.tsx | 10 +- src/web/worker.ts | 5 +- 9 files changed, 209 insertions(+), 89 deletions(-) create mode 100644 src/global.ts diff --git a/.gitignore b/.gitignore index 6637ab1..4d1ca5c 100644 --- a/.gitignore +++ b/.gitignore @@ -13,6 +13,7 @@ dist-ssr *.local coverage lib/ +dusa.umd.js # Editor directories and files .vscode/* diff --git a/package.json b/package.json index cfba399..2149058 100644 --- a/package.json +++ b/package.json @@ -1,8 +1,10 @@ { "name": "dusa", - "version": "0.1.1", + "version": "0.1.2", "type": "module", "main": "lib/client.js", + "unpkg": "./dusa.umd.js", + "jsdelivr": "./dus.umd.js", "types": "lib/client.d.ts", "exports": { "require": "./lib/client.cjs", @@ -32,7 +34,7 @@ "build": "tsc && vite build", "coverage": "vitest run --coverage", "dev": "vite", - "lib": "tsc --project tsconfig.package.json && rollup lib/client.js --file lib/client.cjs --format cjs", + "lib": "tsc --project tsconfig.package.json && rollup lib/client.js --file lib/client.cjs && rollup lib/global.js --file dusa.umd.js --format umd --name Dusa", "lint": "eslint . --report-unused-disable-directives --max-warnings 0", "prettier": "prettier --ignore-path .prettierignore --write *.ts *.json *.html *.md **/*.ts* **/*.json **/*.css **/*.html **/*.md", "prettier:check": "prettier --ignore-path .prettierignore --check .", diff --git a/src/cli.ts b/src/cli.ts index 3409eb3..fa42c56 100644 --- a/src/cli.ts +++ b/src/cli.ts @@ -6,7 +6,6 @@ import { InputFact, InputTerm, Term, - termToJson, } from './client.js'; import { parseArgs, ParseArgsConfig } from 'util'; @@ -299,9 +298,7 @@ export function runDusaCli( if (verbose >= 2) log(`Answer: ${num_solutions}`); const answer: { [pred: string]: Term[][] | number } = {}; for (const pred of [...count, ...query]) { - answer[pred] = [ - ...solution.value.lookup(pred).map((terms) => terms.map(termToJson)), - ].toSorted(compareTerms); + answer[pred] = [...solution.value.lookup(pred)].toSorted(compareTerms); if (count.includes(pred)) { answer[pred] = answer[pred].length; } diff --git a/src/client.test.ts b/src/client.test.ts index 91f4c9f..9ee6bec 100644 --- a/src/client.test.ts +++ b/src/client.test.ts @@ -1,5 +1,5 @@ import { test, expect } from 'vitest'; -import { Dusa, termToString, compareTerms, DusaError } from './client.js'; +import { compareTerms, termToString, Dusa, DusaError } from './client.js'; function solutions(dusa: Dusa, pred: string = 'res') { const sols: string[] = []; diff --git a/src/client.ts b/src/client.ts index 1892d1c..52858a9 100644 --- a/src/client.ts +++ b/src/client.ts @@ -1,5 +1,5 @@ import { ProgramN as BytecodeProgramN } from './bytecode.js'; -import { Data, HashCons } from './datastructures/data.js'; +import { Data } from './datastructures/data.js'; import { Database } from './datastructures/database.js'; import { ascendToRoot, @@ -18,7 +18,10 @@ import { parse } from './language/dusa-parser.js'; import { Issue } from './parsing/parser.js'; import { bytecodeToJSON } from './serialize.js'; import { + BigFact, + BigTerm, compareTerms, + dataToBigTerm, dataToTerm, Fact, InputFact, @@ -29,9 +32,8 @@ import { export type { ProgramN as BytecodeProgramN } from './bytecode.js'; export type { Issue } from './parsing/parser.js'; -export type { InputFact, InputTerm, Fact, Term } from './termoutput.js'; +export type { InputFact, InputTerm, Fact, BigFact, BigTerm, Term } from './termoutput.js'; export { compareTerm, compareTerms, termToString } from './termoutput.js'; -export { termToJson } from './serialize.js'; export class DusaError extends Error { issues: Issue[]; @@ -47,30 +49,91 @@ export class DusaRuntimeError extends Error { } } +export interface DusaSolution { + get(name: string, ...args: InputTerm[]): Term | undefined; + getBig(name: string, ...args: InputTerm[]): BigTerm | undefined; + has(name: string, ...args: InputTerm[]): boolean; + lookup(name: string, ...args: InputTerm[]): Generator; + lookupBig(name: string, ...args: InputTerm[]): Generator; + facts(): Fact[]; + factsBig(): BigFact[]; +} + +export interface DusaIterator extends Iterator { + /** + * Takes at most `limit` steps of the choice engine's `step` function, + * stopping early if a solution is reached or if no more steps can be taken. + * + * Returns true iff next() can return without doing any work. + */ + advance(limit?: number): boolean; + + /** + * Information about the progress towards solutions. + */ + stats(): { deductions: number; rejected: number; choices: number; nonPos: number }; + + /** + * Run the iterator all the way to the end + */ + all(): DusaSolution[]; +} + export class Dusa { private prog: InternalProgram; private state: SearchState | null; - private cachedSolution: null | 'conflict' | DusaSolution = null; + private cachedSolution: 'unknown' | null | DusaSolution = 'unknown'; get relations(): string[] { return [...Object.keys(this.prog.arities)]; } - get solution() { - if (this.cachedSolution === null) { - const solution = this[Symbol.iterator]().next(); - if (!solution.done) { - this.cachedSolution = solution.value; - } else { - this.cachedSolution = 'conflict'; - } + [Symbol.iterator]() { + return new DusaIteratorImpl(this.prog, this.state); + } + + /** + * Returns an iterator to enumerate solutions with a for-if statement. + * + * The `solve()` method and the `[Symbol.iterator]()` do the same thing; if + * you want to enumerate the solutions with a `for...of` loop, just use the + * `dusa` object directly instead of calling `solve()`. + * + * const dusa = new Dusa(`num is { 1, 2, 18, 22 }.`); + * console.log(dusa.solve().next().value.get('num)); // 1, 2, 18, or 22 + * for (const solution of dusa) { + * console.log(solution.get('num')); // in some order: 1, 2, 18, 22 + * } + */ + solve(): DusaIterator { + return new DusaIteratorImpl(this.prog, this.state); + } + + /** + * Get a single arbitrary solution for the program, or null if we can be + * sure that no solutions exist. This is equivalent to calling sample() once + * and remembering the DusaSolution that it returns. + */ + get solution(): DusaSolution | null { + if (this.cachedSolution === 'unknown') { + this.cachedSolution = this.sample(); } - if (this.cachedSolution === 'conflict') return null; return this.cachedSolution; } - [Symbol.iterator]() { - return new DusaIteratorImpl(this.prog, this.state); + /** + * Get an arbitrary solution for the program, or null if we can be sure no + * solutions exist. + */ + sample(): DusaSolution | null { + const sample = this.solve().next(); + if (sample.done) return null; + return sample.value; + } + + get solutions(): DusaIterator { + console.warn(`Dusa.solutions is deprecated, use Dusa.solve() instead`); + return this.solve(); } constructor(source: string | BytecodeProgramN) { @@ -132,7 +195,7 @@ export class Dusa { assert(...facts: InputFact[]) { if (this.state === null) return; this.state = { ...this.state }; - this.cachedSolution = null; + this.cachedSolution = 'unknown'; let conflict = null; for (const fact of facts) { const { name, args, value } = this.inputFact(fact); @@ -171,13 +234,6 @@ export class Dusa { } } -export interface DusaSolution { - get(name: string, ...args: InputTerm[]): Term | undefined; - has(name: string, ...args: InputTerm[]): boolean; - lookup(name: string, ...args: InputTerm[]): Generator; - facts(): Fact[]; -} - class DusaSolutionImpl implements DusaSolution { private solution: Database; private prog: InternalProgram; @@ -186,7 +242,7 @@ class DusaSolutionImpl implements DusaSolution { this.solution = solution; } - get(name: string, ...args: InputTerm[]) { + private getImpl(name: string, ...args: InputTerm[]) { const arity = this.prog.arities[name]; if (!arity) return undefined; if (!arity.value) { @@ -204,7 +260,19 @@ class DusaSolutionImpl implements DusaSolution { args.map((arg) => termToData(this.prog.data, arg)), ); if (constraint === null) return undefined; - return dataToTerm(this.prog.data, (constraint as { just: Data }).just); + return (constraint as { just: Data }).just; + } + + get(name: string, ...args: InputTerm[]) { + const result = this.getImpl(name, ...args); + if (result === undefined) return undefined; + return dataToTerm(this.prog.data, result); + } + + getBig(name: string, ...args: InputTerm[]) { + const result = this.getImpl(name, ...args); + if (result === undefined) return undefined; + return dataToBigTerm(this.prog.data, result); } has(name: string, ...args: InputTerm[]) { @@ -223,59 +291,62 @@ class DusaSolutionImpl implements DusaSolution { ); } - lookup(name: string, ...args: InputTerm[]) { - function* loop( - data: HashCons, - arity: undefined | { args: number; value: boolean }, - solution: Database, - ) { - if (!arity) return; - const depth = (arity.value ? arity.args + 1 : arity.args) - args.length; - for (const result of solution.visit( - name, - args.map((arg) => termToData(data, arg)), - args.length, - depth, - )) { - yield result.map((arg) => dataToTerm(data, arg)); - } + *lookupImpl(name: string, args: InputTerm[]): Generator { + const arity = this.prog.arities[name]; + if (!arity) return; + const depth = (arity.value ? arity.args + 1 : arity.args) - args.length; + yield* this.solution.visit( + name, + args.map((arg) => termToData(this.prog.data, arg)), + args.length, + depth, + ); + } + + *lookup(name: string, ...args: InputTerm[]) { + for (const result of this.lookupImpl(name, args)) { + yield result.map((arg) => dataToTerm(this.prog.data, arg)); } - return loop(this.prog.data, this.prog.arities[name], this.solution); } - facts(): Fact[] { + *lookupBig(name: string, ...args: InputTerm[]) { + for (const result of this.lookupImpl(name, args)) { + yield result.map((arg) => dataToBigTerm(this.prog.data, arg)); + } + } + + factsImpl() { return [...Object.entries(this.prog.arities)] .toSorted((a, b) => (a[0] > b[0] ? 1 : a[0] < b[0] ? -1 : 0)) - .flatMap(([pred, arity]): Fact[] => { - const rows = [...this.lookup(pred)].toSorted(compareTerms); - if (arity.value) { - return rows.map((args) => { - const value = args.pop()!; - return { name: pred, args, value }; - }); - } else { - return rows.map((args) => ({ name: pred, args, value: null })); - } + .map(([pred, arity]) => { + return { pred, rows: [...this.lookupImpl(pred, [])], hasValue: arity.value }; }); } -} -export interface DusaIterator extends Iterator { - /** - * Takes at most `limit` steps of the choice engine's `step` function, - * stopping early if a solution is reached or if no more steps can be taken. - * - * Returns true iff next() can return without doing any work. - */ - advance(limit?: number): boolean; + facts(): Fact[] { + return this.factsImpl().flatMap(({ pred, rows, hasValue }) => { + return rows + .map((row) => row.map((tm) => dataToTerm(this.prog.data, tm))) + .toSorted(compareTerms) + .map((args) => + hasValue ? { name: pred, args, value: args.pop()! } : { name: pred, args }, + ); + }); + } - /** - * Information about the progress towards solutions. - */ - stats(): { deductions: number; rejected: number; choices: number; nonPos: number }; + factsBig(): BigFact[] { + return this.factsImpl().flatMap(({ pred, rows, hasValue }) => { + return rows + .map((row) => row.map((tm) => dataToBigTerm(this.prog.data, tm))) + .toSorted(compareTerms) + .map((args) => + hasValue ? { name: pred, args, value: args.pop()! } : { name: pred, args }, + ); + }); + } } -class DusaIteratorImpl implements Iterator { +class DusaIteratorImpl implements DusaIterator { private state: | { type: 'parent'; state: SearchState } | { type: 'tree'; path: ChoiceZipper; tree: ChoiceTree | null }; @@ -302,6 +373,16 @@ class DusaIteratorImpl implements Iterator { }; } + all() { + const results: DusaSolution[] = []; + let next: IteratorResult = this.next(); + for (;;) { + if (next.done) return results; + results.push(next.value); + next = this.next(); + } + } + stepState( prog: InternalProgram, state: SearchState, diff --git a/src/global.ts b/src/global.ts new file mode 100644 index 0000000..37f4a53 --- /dev/null +++ b/src/global.ts @@ -0,0 +1,16 @@ +import { + compareTerm, + compareTerms, + Dusa as DusaClient, + DusaError, + DusaRuntimeError, + termToString, +} from './client.js'; + +export default class Dusa extends DusaClient { + static termToString = termToString; + static compareTerm = compareTerm; + static compareTerms = compareTerms; + static DusaError = DusaError; + static DusaRuntimeError = DusaRuntimeError; +} diff --git a/src/termoutput.ts b/src/termoutput.ts index 936b6d7..fcd3cd6 100644 --- a/src/termoutput.ts +++ b/src/termoutput.ts @@ -2,7 +2,7 @@ import { Data, escapeString, HashCons } from './datastructures/data.js'; export type Term = | null // Trivial type () - | bigint // Natural numbers and integers + | number // Natural numbers and integers | string // Strings | boolean | { name: null; value: number } // JSON refs @@ -10,8 +10,21 @@ export type Term = export interface Fact { name: string; args: Term[]; - value: Term; + value?: Term; +} +export type BigTerm = + | null // Trivial type () + | bigint // Natural numbers and integers + | string // Strings + | boolean + | { name: null; value: number } // JSON refs + | { name: string; args?: [BigTerm, ...BigTerm[]] }; +export interface BigFact { + name: string; + args: BigTerm[]; + value?: BigTerm; } + export type InputTerm = | null | number @@ -29,7 +42,7 @@ export interface InputFact { export function dataToTerm(data: HashCons, t: Data): Term { const view = data.expose(t); if (view.type === 'trivial') return null; - if (view.type === 'int') return view.value; + if (view.type === 'int') return Number(view.value); if (view.type === 'bool') return view.value; if (view.type === 'string') return view.value; if (view.type === 'ref') return { name: null, value: view.value }; @@ -37,6 +50,17 @@ export function dataToTerm(data: HashCons, t: Data): Term { const args = view.args.map((arg) => dataToTerm(data, arg)) as [Term, ...Term[]]; return { name: view.name, args }; } +export function dataToBigTerm(data: HashCons, t: Data): BigTerm { + const view = data.expose(t); + if (view.type === 'trivial') return null; + if (view.type === 'int') return view.value; + if (view.type === 'bool') return view.value; + if (view.type === 'string') return view.value; + if (view.type === 'ref') return { name: null, value: view.value }; + if (view.args.length === 0) return { name: view.name }; + const args = view.args.map((arg) => dataToBigTerm(data, arg)) as [BigTerm, ...BigTerm[]]; + return { name: view.name, args }; +} export function termToData(data: HashCons, t: InputTerm): Data { if (t === null) return HashCons.TRIVIAL; @@ -54,11 +78,11 @@ export function termToData(data: HashCons, t: InputTerm): Data { return data.hide({ type: 'int', value: BigInt(t) }); } -export function termToString(tm: Term, parens = false): string { +export function termToString(tm: BigTerm | Term, parens = false): string { if (tm === null) return '()'; if (typeof tm === 'boolean') return `bool#${tm}`; if (typeof tm === 'string') return `"${escapeString(tm)}"`; - if (typeof tm === 'bigint') return `${tm}`; + if (typeof tm === 'bigint' || typeof tm === 'number') return `${tm}`; if (tm.name === null) return `ref#${tm.value}`; if (!tm.args) return tm.name; const tmStr = `${tm.name} ${tm.args.map((arg) => termToString(arg, true)).join('')}`; @@ -66,7 +90,7 @@ export function termToString(tm: Term, parens = false): string { return `(${tmStr})`; } -export function compareTerms(t: Term[], s: Term[]): number { +export function compareTerms(t: (Term | BigTerm)[], s: (Term | BigTerm)[]): number { for (let i = 0; i < Math.min(t.length, s.length); i++) { const c = compareTerm(t[i], s[i]); if (c !== 0) return c; @@ -74,7 +98,7 @@ export function compareTerms(t: Term[], s: Term[]): number { return s.length - t.length; } -export function compareTerm(t1: Term, t2: Term): number { +export function compareTerm(t1: Term | BigTerm, t2: Term | BigTerm): number { if (t1 === null) return t2 === null ? 0 : -1; if (t2 === null) return 1; if (typeof t1 === 'boolean') { diff --git a/src/web/Inspector.tsx b/src/web/Inspector.tsx index bb93459..a01ff15 100644 --- a/src/web/Inspector.tsx +++ b/src/web/Inspector.tsx @@ -2,7 +2,7 @@ import { DOCUMENT } from 'sketchzone'; import React from 'react'; import type { WorkerStats, AppToWorkerMsg, WorkerToAppMsg } from './worker.js'; import { Dusa, DusaError, type Issue } from '../client.js'; -import type { Fact, Term } from '../termoutput.js'; +import type { BigFact, BigTerm } from '../termoutput.js'; import { ChevronLeftIcon, ChevronRightIcon, @@ -21,7 +21,7 @@ interface Props { const ICON_SIZE = '24px'; -function Term({ term }: { term: Term }) { +function Term({ term }: { term: BigTerm }) { if (term === null) return '()'; if (typeof term === 'string') return `"${escapeString(term)}"`; if (typeof term === 'bigint') return `${term}`; @@ -42,7 +42,7 @@ function Term({ term }: { term: Term }) { ); } -function Solution({ facts }: { facts: Fact[] }) { +function Solution({ facts }: { facts: BigFact[] }) { return (
    {facts.map((fact, i) => ( @@ -54,7 +54,7 @@ function Solution({ facts }: { facts: Fact[] }) { ))} - {fact.value !== null && ( + {fact.value !== undefined && ( <> {' '} is @@ -77,7 +77,7 @@ export default function Inspector({ doc, visible }: Props) { // solutionIndex === solutions.length means we're "following" the latest state const [solutionIndex, setSolutionIndex] = React.useState(null); - const [solutions, setSolutions] = React.useState([]); + const [solutions, setSolutions] = React.useState([]); const [state, setState] = React.useState<'running' | 'paused' | 'done'>('running'); React.useEffect(() => { diff --git a/src/web/worker.ts b/src/web/worker.ts index 0cc2152..6779af9 100644 --- a/src/web/worker.ts +++ b/src/web/worker.ts @@ -1,6 +1,5 @@ -import { Fact as OutputFact } from '../termoutput.js'; import { ProgramN } from '../bytecode.js'; -import { Dusa, DusaIterator } from '../client.js'; +import { Dusa, DusaIterator, BigFact as OutputFact } from '../client.js'; export type WorkerQuery = { type: 'list'; @@ -62,7 +61,7 @@ function loop(): true { state = 'done'; return true; } else { - post({ type: 'solution', facts: next.value.facts() }); + post({ type: 'solution', facts: next.value.factsBig() }); } } } catch (e) {