From 2912f2da4753f40405a57ad833a779c2d9b8601f Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Fri, 24 Nov 2023 21:03:42 -0500 Subject: [PATCH] has and get and docs --- docs/src/content/docs/docs/api/dusa.md | 14 +- .../src/content/docs/docs/api/dusasolution.md | 134 +++++++++++++++++- docs/src/content/docs/docs/api/terms.md | 65 ++++++++- package-lock.json | 4 +- package.json | 2 +- src/client.test.ts | 58 ++++++++ src/client.ts | 20 ++- src/datastructures/datamap.ts | 6 + src/engine/forwardengine.ts | 20 +++ 9 files changed, 310 insertions(+), 13 deletions(-) diff --git a/docs/src/content/docs/docs/api/dusa.md b/docs/src/content/docs/docs/api/dusa.md index 29f8ce2..b9a991d 100644 --- a/docs/src/content/docs/docs/api/dusa.md +++ b/docs/src/content/docs/docs/api/dusa.md @@ -50,8 +50,8 @@ const dusa = new Dusa(` path X Y :- edge X Y. path X Z :- edge X Y, path Y Z.`); dusa.solution; // Object of type DusaSolution -[...dusa.solution.lookup('path', 'a')]; // [ ["b"], ["c"], ["d"] ] -[...dusa.solution.lookup('path', 'd')]; // [] +[...dusa.solution.lookup('path', 'b')]; // [['c', null], ['d', null]] +[...dusa.solution.lookup('path', 'c')]; // [['d', null]] ``` If no solutions exist, the `solution` getter will return `null`. @@ -87,8 +87,8 @@ Each call to `sample()` re-computes the program, so even if there are only a fin const dusa = new Dusa(`name is { "one", "two" }.`); for (let i = 0; i < 1000; i++) { - for (const { args } of dusa.sample().lookup('name')) { - console.log(args[0]); + for (const [name] of dusa.sample().lookup('name')) { + console.log(name); } } ``` @@ -101,7 +101,7 @@ will print `"two"` about 500 times. The `solutions` getter iterates through all the possible distinct solutions of a Dusa program. The iterator works in an arbitrary order: this program will either print -`"one"` and then `"two"` or else it will print `"two"` and then `"one"`. +`[["one"]]` and then `[["two"]]` or else it will print `[["two"]]` and then `[["one"]]`. ```javascript const dusa = new Dusa(`name is { "one", "two" }.`); @@ -134,11 +134,11 @@ const dusa = new Dusa(` [...dusa.solution.lookup('path', 'a')]; // [] dusa.assert({ name: 'edge', args: ['a', 'b'] }); -[...dusa.solution.lookup('path', 'a')]; // [ { args: ['b'] } ] +[...dusa.solution.lookup('path', 'a')]; // [['b', null]] dusa.assert( { name: 'edge', args: ['b', 'c'] }, { name: 'edge', args: ['e', 'b'] }, { name: 'edge', args: ['d', 'e'] }, ); -[...dusa.solution.lookup('path', 'a')]; // [ { args: ['b'] }, { args: ['c'] } ] +[...dusa.solution.lookup('path', 'a')]; // [['b', null], ['c', null]] ``` diff --git a/docs/src/content/docs/docs/api/dusasolution.md b/docs/src/content/docs/docs/api/dusasolution.md index 48ca650..2f20e64 100644 --- a/docs/src/content/docs/docs/api/dusasolution.md +++ b/docs/src/content/docs/docs/api/dusasolution.md @@ -2,4 +2,136 @@ title: class DusaSolution --- -TODO +A `DusaSolution` is a queryable solution to a Dusa program returned by +[solving a `Dusa` instance](docs/api/dusa/#solving-a-dusa-instance). + +## `facts` getter + +The `facts` getter provides an iterator over all the [facts](/docs/api/terms/#fact) +in a solution. + +```javascript +const dusa = new Dusa(` + #builtin INT_MINUS minus + digit 9. + digit (minus N 1) :- digit N, N != 0.`); + +for (const fact of dusa.solution.facts) { + console.log(fact); +} +``` + +## `has()` and `get()` + +The `has()` method is intended to check whether a relational proposition +exists in the database, and the `get()` method is intended to check the value +of a functional proposition. (But since [these are actually the same +thing](/docs/language/facts/#everythings-secretly-functional), either can be used +for either one.) The `has()` method checks for the presence of an attribute (with +any value), returning a `boolean`. The `get()` method checks for the value +associated with an attribute, returning the value or `undefined`. + +Both methods take a string as the first argument, and then one additional +[`InputTerm`](/docs/api/terms/#inputterm) argument for every non-value +argument for the predicate. + +### Example + +In a database with propositions of the form, `node _`, `edge _ _`, and +`color _ is _`, the implied Typescript types for `has()` and `get()` are as follows: + +```typescript +has(name: 'node', arg1: InputTerm): boolean; +has(name: 'edge', arg1: InputTerm, arg2: InputTerm): boolean; +has(name: 'color', arg1: InputTerm): boolean; +get(name: 'node', arg1: InputTerm): undefined | null; +get(name: 'edge', arg1: InputTerm, arg2: InputTerm): undefined | null; +get(name: 'color', arg1: InputTerm): undefined | Term; +``` + +These can be used like this: + +```javascript +const dusa = new Dusa(` + edge 1 2. + node 1. + node 2. + node 3. + color 1 is "blue". + color 2 is "red".`); + +dusa.solution.has('node', 1); // === true +dusa.solution.has('node', 7); // === false +dusa.solution.get('node', 3); // === null, () in Dusa +dusa.solution.get('node', 9); // === undefined + +dusa.solution.has('edge', 1, 2); // === true +dusa.solution.has('edge', 2, 1); // === false + +dusa.solution.get('color', 1); // === "blue" +dusa.solution.get('color', 9); // === undefined +``` + +## `lookup()` method + +The `lookup()` method on solutions is a powerful query mechanism. If your program +has a relational proposition `path _ _`, then given only the first argument +`'path'`, `lookup()` will return an iterator over all the paths. + +```javascript +const dusa = new Dusa(` + edge 1 2. + edge 2 3. + edge 3 4. + path X Y :- edge X Y. + path X Z :- edge X Y, path Y Z.`); +for (const [a, b] of dusa.solution.lookup('path')) { + console.log(`Path from ${a} to ${b}`); +} +``` + +This will print the following: + + Path from 1 to 2 + Path from 1 to 3 + Path from 1 to 4 + Path from 2 to 3 + Path from 2 to 4 + Path from 3 to 4 + +Given the first argument `'path'` and the second argument `2n`, `lookup` will +return an iterator over all the second arguments `B` such that there is a fact +`path 2 B`. + +```javascript +const dusa = new Dusa(` + edge 1 2. + edge 2 3. + edge 3 4. + path X Y :- edge X Y. + path X Z :- edge X Y, path Y Z.`); +for (const [b] of dusa.solution.lookup('path', 2n)) { + console.log(`Path from 2 to ${b}`); +} +``` + +This will print the following: + + Path from 2 to 3 + Path from 2 to 4 + +In Typescript terms, the `lookup()` method has the following type: + +```typescript +lookup(name: 'path'): IterableIterator<[Term, Term, null]>; +lookup(name: 'path', arg1: InputTerm): IterableIterator<[Term, null]>; +lookup(name: 'path', arg1: InputTerm, arg2: InputTerm): IterableIterator<[null]>; +``` + +For a functional proposition like `name _ is _`, the effective type of the +`lookup()` method is: + +```typescript +lookup(name: 'name'): IterableIterator<[Term, Term]>; +lookup(name: 'name', arg1: InputTerm): IterableIterator<[Term]>; +``` diff --git a/docs/src/content/docs/docs/api/terms.md b/docs/src/content/docs/docs/api/terms.md index dbf2a1b..0b9ca91 100644 --- a/docs/src/content/docs/docs/api/terms.md +++ b/docs/src/content/docs/docs/api/terms.md @@ -2,4 +2,67 @@ title: Terms --- -TODO +## Output types + +All Dusa terms have a correspondence with JavaScript types: + +- The trivial type `()` in Dusa corresponds to `null` in JavaScript. +- The string type in Dusa corresponds to the string type in JavaScript. +- The integer and natural number types in Dusa correspond to the + [BigInt](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/BigInt) + type in JavaScript. The JavaScript BigInt four is written as `4n`, not `4`. +- Constants like `a`, `tt`, or `bob` in Dusa correspond to objects `{ name: 'a' }`, + `{ name: 'tt' }`, or `{ name: 'bob' }` in JavaScript. +- An uninterpreted function with arguments like `h 9 "fish"` in Dusa corresponds + to an object `{ name: 'h', args: [9n, 'fish'] }` in JavaScript. + +### `Term` + +```typescript +export type Term = + | null // Trivial type () + | bigint // Natural numbers and integers + | string // Strings + | { name: string } // Constants + | { name: string; args: [Term, ...Term[]] }; +``` + +### `Fact` + +```typescript +export interface Fact { + name: string; + args: Term[]; + value: Term; +} +``` + +## Input types + +The Dusa and DusaSolution methods that take terms and facts as argument accept +inputs that are more flexible than the outputs that Dusa will return (see the +[Robustness Principle](https://en.wikipedia.org/wiki/Robustness_principle)). + +### `InputTerm` + +Dusa will accept numbers of type `number` and convert them to +[BigInt](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/BigInt) +values. This will raise a `RangeError` if you try to pass a non-integer `number` +to Dusa. + +An input constant like `a` can also be given as `{ name: 'a', args: [] }`, even +though that constant will always be output as `{ name: 'a' }`. + +### `InputFact` + +```typescript +export interface InputFact { + name: string; + args: InputTerm[]; + value?: InputTerm; +} +``` + +The `value` field is optional when giving a fact as an argument (for example, to +the [`assert()` method](/docs/api/dusa/#assert-method).), and a missing value +field will be interpreted as the trivial Dusa value `()`. diff --git a/package-lock.json b/package-lock.json index 94e083b..93d0f1a 100644 --- a/package-lock.json +++ b/package-lock.json @@ -1,12 +1,12 @@ { "name": "dusa", - "version": "0.0.6", + "version": "0.0.7", "lockfileVersion": 3, "requires": true, "packages": { "": { "name": "dusa", - "version": "0.0.6", + "version": "0.0.7", "license": "GPL-3.0-only", "devDependencies": { "@codemirror/commands": "^6.3.0", diff --git a/package.json b/package.json index 504233b..dc2e36c 100644 --- a/package.json +++ b/package.json @@ -1,6 +1,6 @@ { "name": "dusa", - "version": "0.0.6", + "version": "0.0.7", "type": "module", "main": "lib/client.js", "types": "lib/client.d.ts", diff --git a/src/client.test.ts b/src/client.test.ts index b26d6c8..807a806 100644 --- a/src/client.test.ts +++ b/src/client.test.ts @@ -43,4 +43,62 @@ test('Client fundamentals', () => { [3n, null], [7n, null], ]); + + expect(dusa.solution!.get('path', 0, -5)).toEqual(null); + expect(dusa.solution!.get('path', 0, 99)).toEqual(undefined); + expect(dusa.solution!.has('path', 0, 1)).toEqual(true); + expect(dusa.solution!.has('path', 0, 4)).toEqual(false); +}); + +test('Fact enumeration', () => { + const singleton = new Dusa(`fact 1 2 3 is "yo".`); + expect(singleton.solution).not.toBeNull(); + expect([...singleton.solution!.facts]).toEqual([ + { name: 'fact', args: [1n, 2n, 3n], value: 'yo' }, + ]); + + const digits = new Dusa(` + #builtin INT_MINUS minus + digit 9. + digit (minus N 1) :- digit N, N != 0.`); + + expect(digits.solution).not.toBeNull(); + expect([...digits.solution!.facts]).toEqual([ + { name: 'digit', args: [0n], value: null }, + { name: 'digit', args: [1n], value: null }, + { name: 'digit', args: [2n], value: null }, + { name: 'digit', args: [3n], value: null }, + { name: 'digit', args: [4n], value: null }, + { name: 'digit', args: [5n], value: null }, + { name: 'digit', args: [6n], value: null }, + { name: 'digit', args: [7n], value: null }, + { name: 'digit', args: [8n], value: null }, + { name: 'digit', args: [9n], value: null }, + ]); +}); + +test('Has and get', () => { + const dusa = new Dusa(` + edge 1 2. + node 1. + node 2. + node 3. + color 1 is "blue". + color 2 is "red".`); + + expect(dusa.solution!.has('node', 1)).toBeTruthy(); + expect(dusa.solution!.has('node', 7)).toBeFalsy(); + expect(dusa.solution!.has('node', null)).toBeFalsy(); + expect(dusa.solution!.get('node', 3)).toBeNull(); + expect(dusa.solution!.get('node', 'hello')).toBeUndefined(); + + expect(dusa.solution!.has('edge', 1, 2)).toBeTruthy(); + expect(dusa.solution!.has('edge', 2, 1)).toBeFalsy(); + expect(dusa.solution!.get('edge', 1, 2)).toBeNull(); + expect(dusa.solution!.get('edge', 2, 1)).toBeUndefined(); + + expect(dusa.solution!.has('color', 1)).toBeTruthy(); + expect(dusa.solution!.has('color', 4)).toBeFalsy(); + expect(dusa.solution!.get('color', 2)).toEqual('red'); + expect(dusa.solution!.get('color', 5)).toBeUndefined(); }); diff --git a/src/client.ts b/src/client.ts index 0451c38..9c3c8cd 100644 --- a/src/client.ts +++ b/src/client.ts @@ -6,7 +6,14 @@ import { pathToString, stepTreeRandomDFS, } from './engine/choiceengine.js'; -import { Database, insertFact, listFacts, lookup, makeInitialDb } from './engine/forwardengine.js'; +import { + Database, + get, + insertFact, + listFacts, + lookup, + makeInitialDb, +} from './engine/forwardengine.js'; import { compile } from './language/compile.js'; import { parse } from './language/dusa-parser.js'; import { IndexedProgram } from './language/indexize.js'; @@ -85,6 +92,17 @@ export class DusaSolution { } return map(lookup(this.db, name, args.map(termToData))); } + + get(name: string, ...args: InputTerm[]): Term | undefined { + const value = get(this.db, name, args.map(termToData)); + if (value === undefined) return undefined; + return dataToTerm(value); + } + + has(name: string, ...args: InputTerm[]): boolean { + const value = get(this.db, name, args.map(termToData)); + return value !== undefined; + } } function* solutionGenerator( diff --git a/src/datastructures/datamap.ts b/src/datastructures/datamap.ts index b9097db..d4800cd 100644 --- a/src/datastructures/datamap.ts +++ b/src/datastructures/datamap.ts @@ -422,6 +422,12 @@ export class TrieMap { return new TrieMap(null); } + arity(name: string): number | null { + const trie = lookup(this.t, name); + if (trie === null) return null; + return trie.depth; + } + set(name: string, args: K[], value: V) { const trie = lookup(this.t, name); if (trie !== null && args.length !== (trie.depth ?? 0)) { diff --git a/src/engine/forwardengine.ts b/src/engine/forwardengine.ts index 12dea0e..603199b 100644 --- a/src/engine/forwardengine.ts +++ b/src/engine/forwardengine.ts @@ -294,6 +294,12 @@ export function* lookup( name: string, args: Data[], ): IterableIterator<{ args: Data[]; value: Data }> { + const arity = db.factValues.arity(name); + if (arity !== null && arity < args.length) { + throw new TypeError( + `${name} takes ${arity} argument${arity === 1 ? '' : 's'}, but ${args.length} were given`, + ); + } for (const { keys, value } of db.factValues.lookup(name, args)) { if (value.type === 'is') { yield { args: keys, value: value.value }; @@ -301,6 +307,20 @@ export function* lookup( } } +export function get(db: Database, name: string, args: Data[]): undefined | Data { + const arity = db.factValues.arity(name); + if (arity === null) return undefined; + if (args.length !== arity) { + throw new TypeError( + `${name} takes ${arity} argument${arity === 1 ? '' : 's'}, but ${args.length} were given`, + ); + } + for (const { value } of db.factValues.lookup(name, args)) { + if (value.type === 'is') return value.value; + } + return undefined; +} + function argsetToString(args: Data[]) { return `[ ${args.map((v) => dataToString(v)).join(', ')} ]`; }