Dusa v0.1 followup (#64)

Docs, coverage, and some fact assertion errors

docs/src/content/docs/docs/api/dusa.md

@@ -30,17 +30,16 @@ const dusa = new Dusa(`edge a X.`);
 
 ## Solving a Dusa instance
 
-Dusa programs can't be directly queried: they must first be solved. There are several
-different ways to direct Dusa to generate solutions, all of which provide access to
-[`DusaSolution` objects](/docs/api/dusasolution/).
+Dusa programs can't be directly queried: they must first be solved. There are
+several different ways to direct Dusa to generate solutions, all of which
+provide access to [`DusaSolution` objects](/docs/api/dusasolution/).
 
 ### `solution` getter
 
-If a Dusa program has at most one solution, that solution can be accessed with the
-`solution` getter. The first time this method is accessed it will cause some
-computation to happen (and it could even fail to terminate if there aren't finite
-solutions). The result is cached, so subsequent calls will not trigger additional
-computation.
+Often all you need is to find a single solution (or to know that know
+solutions exist). The first time you try to access `dusa.solution` some
+computation will happen (and this could even fail to terminate). But then the
+result is cached; subsequent calls will not trigger additional computation.
 
 ```javascript
 const dusa = new Dusa(`
@@ -50,11 +49,11 @@ 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', 'b')]; // [['c', null], ['d', null]]
-[...dusa.solution.lookup('path', 'c')]; // [['d', null]]
+[...dusa.solution.lookup('path', 'b')]; // [['c'], ['d']]
+[...dusa.solution.lookup('path', 'c')]; // [['d']]
 ```
 
-[Explore this example on StackBlitz](https://stackblitz.com/edit/node-kmrbac?file=index.js&view=editor)
+[Explore this example on val.town](https://www.val.town/v/robsimmons/solution_getter_yes)
 
 If no solutions exist, the `solution` getter will return `null`.
 
@@ -65,77 +64,50 @@ const dusa = new Dusa(`
 dusa.solution; // null
 ```
 
-[Explore this example on StackBlitz](https://stackblitz.com/edit/node-qmaf3y?file=index.js&view=editor)
+[Explore this example on val.town](htthttps://www.val.town/v/robsimmons/solution_getter_no)
 
-This getter can only be used if a single solution exists. Dusa will check for
-additional solutions when the `solution` getter is accessed, and will throw an
-exception if there are other solutions.
+If there are multiple solutions, the `solution` getter will pick one solution,
+and will always return that one.
 
 ```javascript
 const dusa = new Dusa(`name is { "one", "two" }.`);
 dusa.solution; // raises DusaError
 ```
 
-[Explore this example on StackBlitz](https://stackblitz.com/edit/node-ybvpcq?file=index.js&view=editor)
+[Explore this example on val.town](https://www.val.town/v/robsimmons/solution_getter_maybe)
 
-For programs with multiple solutions, use the `sample()` method or the `solutions`
-getter, which returns an iterator.
+### Getting all solutions
 
-### `sample()` method
-
-The `sample()` method will return an arbitrary solution to the Dusa program, or
-`null` if no solution exists.
-
-Each call to `sample()` re-computes the program, so even if there are only a finite
-(but nonzero) number of solutions, `sample()` can be called as many times as desired.
-
-```javascript
-const dusa = new Dusa(`name is { "one", "two" }.`);
-
-for (let i = 0; i < 1000; i++) {
-  for (const [name] of dusa.sample().lookup('name')) {
-    console.log(name);
-  }
-}
-```
-
-[Explore this example on StackBlitz](https://stackblitz.com/edit/node-dqe9g4?file=index.js&view=editor)
-
-The current Dusa interpreter does not have a well-defined probabilistic semantics for
-complex programs, but the simple program above will print `"one"` about 500 times and
-will print `"two"` about 500 times.
-
-### solutions getter
-
-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"]]`.
+To enumerate the solutions to a program, you can use the Javascript iterator
+notation. 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"]]`.
 
 ```javascript
 const dusa = new Dusa(`name is { "one", "two" }.`);
 
-for (const solution of dusa.solutions) {
+for (const solution of dusa) {
   console.log([...solution.lookup('name')]);
 }
 ```
 
-[Explore this example on StackBlitz](https://stackblitz.com/edit/node-cysbcb?file=index.js&view=editor)
+[Explore this example on val.town](https://www.val.town/v/robsimmons/solutions_enumerate)
 
-Each time the `dusa.solutions` getter is accessed, an iterator is returned that
-re-runs solution search, potentially returning solutions in a different order.
+Each time you invoke the iterator `dusa` getter is accessed, search is re-run,
+potentially returning solutions in a different order.
 
 ## Modifying a Dusa instance
 
-The Dusa implementation doesn't support adding and removing rules after a `Dusa`
-class instance has been created, but it does support adding additional **facts**,
-which can be just as powerful. This can be useful for applications where the actual
-set of facts isn't known ahead of time, but the desired analysis on those facts is
-known.
+The Dusa implementation doesn't support adding and removing rules after a
+`Dusa` class instance has been created, but it does support adding additional
+**facts**, which can be just as powerful. This can be useful for applications
+where the actual set of facts isn't known ahead of time, but the desired
+analysis on those facts is known.
 
 ### assert() method
 
-The `assert` method of a Dusa instance takes an arbitrary number of arguments, each
-one a Fact, and adds them to the database.
+The `assert` method of a Dusa instance takes an arbitrary number of arguments,
+each one a Fact, and adds them to the database.
 
 ```javascript
 const dusa = new Dusa(`
@@ -153,4 +125,4 @@ dusa.assert(
 [...dusa.solution.lookup('path', 'a')]; // [['b', null], ['c', null]]
 ```
 
-[Explore this example on StackBlitz](https://stackblitz.com/edit/node-7k1apl?file=index.js&view=editor)
+[Explore this example on val.town](https://www.val.town/v/robsimmons/dusa_assertion)

docs/src/content/docs/docs/api/dusasolution.md

@@ -29,78 +29,16 @@ get(name: string, ...args: InputTerm): undefined | Term;
 ```
 
 An error will be raised if the number of `args` is not equal to the number of
-arguments that the proposition has (not counting the value).
-
-### Example
-
-Since [functional and relational propositions are actually the same
-thing](/docs/language/facts/#everythings-secretly-functional), either `has()`
-or `get()` can be used with any proposition.
-
-In a solution 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
-```
-
-[Explore this example on StackBlitz](https://stackblitz.com/edit/node-kk2qno?file=index.js&view=editor)
-
-## Enumerating all facts
-
-### `facts` getter
-
-The `facts` getter provides an iterator over all the [facts](/docs/api/terms/#type-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);
-}
-```
-
-[Explore this example on StackBlitz](https://stackblitz.com/edit/node-4fvfea?file=index.js&view=editor)
+arguments that the proposition has (not counting the value), or if the
+predicate `name` is a Datalog predicate that does not have an `is` value.
 
 ## Querying solutions
 
 ### `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.
+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(`
@@ -114,9 +52,9 @@ for (const [a, b] of dusa.solution.lookup('path')) {
 }
 ```
 
-[Explore this example on StackBlitz](https://stackblitz.com/edit/node-xhjrt3?file=index.js&view=editor)
+[Explore this example on val.town](https://www.val.town/v/robsimmons/lookup_all)
 
-This will print the following:
+This will print the following in some order:
 
     Path from 1 to 2
     Path from 1 to 3
@@ -141,7 +79,7 @@ for (const [b] of dusa.solution.lookup('path', 2n)) {
 }
 ```
 
-[Explore this example on StackBlitz](https://stackblitz.com/edit/node-15xb9l?file=index.js&view=editor)
+[Explore this example on val.town](https://www.val.town/v/robsimmons/lookup_some)
 
 This will print the following:
 
@@ -151,9 +89,9 @@ This will print the following:
 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]>;
+lookup(name: 'path'): IterableIterator<[Term, Term]>;
+lookup(name: 'path', arg1: InputTerm): IterableIterator<[Term]>;
+lookup(name: 'path', arg1: InputTerm, arg2: InputTerm): IterableIterator<[]>;
 ```
 
 For a functional proposition like `name _ is _`, the effective type of the
@@ -163,3 +101,24 @@ For a functional proposition like `name _ is _`, the effective type of the
 lookup(name: 'name'): IterableIterator<[Term, Term]>;
 lookup(name: 'name', arg1: InputTerm): IterableIterator<[Term]>;
 ```
+
+## Enumerating all facts
+
+### `facts()`
+
+The `facts` method provides a list of all the
+[facts](/docs/api/terms/#type-fact) in a solution. The `lookup()` method
+is generally going to be preferable.
+
+```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);
+}
+```
+
+[Explore this example on val.town](https://www.val.town/v/robsimmons/list_the_facts)

docs/src/content/docs/docs/api/terms.md

@@ -11,10 +11,10 @@ All Dusa terms have a correspondence with JavaScript types:
 - 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.
+- 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.
 
 ### type `Term`
 
@@ -50,19 +50,19 @@ Dusa will accept numbers of type `number` and convert them to
 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' }`.
+An input constant like `a` can also be given as `{ name: 'a', args: [] }`,
+even though that constant will always be output as `{ name: 'a' }`.
 
 ### type `InputFact`
 
 ```typescript
 export interface InputFact {
   name: string;
-  args: InputTerm[];
+  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 `()`.
+Both the `args` field and the `value` field are is optional when giving a fact
+as an argument (for example, to the [`assert()`
+method](/docs/api/dusa/#assert-method).).

docs/src/content/docs/docs/index.md

@@ -14,11 +14,16 @@ the first implementation of finite-choice logic programming.
 - If you've heard of answer set programming (as implemented in systems
   like [Potassco](https://potassco.org/)), you may want to start by reading
   about how [Dusa is answer set programming](/docs/introductions/asp/).
-- If you have no familarity with either of these, that's okay too! You may want
-  to start by reading about how
+- If you have no familarity with either of these, that's okay too! You may
+  want to start by reading about how
   [Dusa is a graph exploration language](/docs/introductions/graph/).
   Then you can take a look at some of the other introductions, or
   [fiddle with some of the default examples](/).
-- If you're interested in the mathematics of finite-choice logic programming, the
-  paper [Finite-Choice Logic Programming](https://popl25.sigplan.org/details/POPL-2025-popl-research-papers/13/Finite-Choice-Logic-Programming)
+- If you're interested in the mathematics of finite-choice logic programming,
+  the paper
+  [Finite-Choice Logic Programming](https://popl25.sigplan.org/details/POPL-2025-popl-research-papers/13/Finite-Choice-Logic-Programming)
   by Martens, Simmons, and Michael Arntzenius may be of interest.
+
+The easiest way to use Dusa is in our [/](web editor). Dusa is also available
+as a command-line utility and JavaScript API via the
+[Node package manager](https://www.npmjs.com/package/dusa).