Skip to content

Commit

Permalink
has and get and docs
Browse files Browse the repository at this point in the history
  • Loading branch information
robsimmons committed Nov 25, 2023
1 parent 8a17377 commit 2912f2d
Show file tree
Hide file tree
Showing 9 changed files with 310 additions and 13 deletions.
14 changes: 7 additions & 7 deletions docs/src/content/docs/docs/api/dusa.md
Original file line number Diff line number Diff line change
Expand Up @@ -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`.
Expand Down Expand Up @@ -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);
}
}
```
Expand All @@ -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" }.`);
Expand Down Expand Up @@ -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]]
```
134 changes: 133 additions & 1 deletion docs/src/content/docs/docs/api/dusasolution.md
Original file line number Diff line number Diff line change
Expand Up @@ -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]>;
```
65 changes: 64 additions & 1 deletion docs/src/content/docs/docs/api/terms.md
Original file line number Diff line number Diff line change
Expand Up @@ -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 `()`.
4 changes: 2 additions & 2 deletions package-lock.json

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion package.json
Original file line number Diff line number Diff line change
@@ -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",
Expand Down
58 changes: 58 additions & 0 deletions src/client.test.ts
Original file line number Diff line number Diff line change
Expand Up @@ -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();
});
20 changes: 19 additions & 1 deletion src/client.ts
Original file line number Diff line number Diff line change
Expand Up @@ -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';
Expand Down Expand Up @@ -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(
Expand Down
6 changes: 6 additions & 0 deletions src/datastructures/datamap.ts
Original file line number Diff line number Diff line change
Expand Up @@ -422,6 +422,12 @@ export class TrieMap<K, V> {
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)) {
Expand Down
Loading

0 comments on commit 2912f2d

Please sign in to comment.