From 17cea620eae066ce989d41ea12718d33369f9b5e Mon Sep 17 00:00:00 2001 From: "Robert J. Simmons" <442315+robsimmons@users.noreply.github.com> Date: Fri, 22 Nov 2024 15:58:54 -0500 Subject: [PATCH 1/2] Dusa v0.1 followup (#64) Docs, coverage, and some fact assertion errors --- docs/src/content/docs/docs/api/dusa.md | 90 +++----- .../src/content/docs/docs/api/dusasolution.md | 105 +++------ docs/src/content/docs/docs/api/terms.md | 20 +- docs/src/content/docs/docs/index.md | 13 +- src/cli.test.ts | 204 +++++++++++++++++- src/cli.ts | 45 +++- src/client.ts | 4 +- src/datastructures/data.test.ts | 6 +- src/termoutput.ts | 2 +- 9 files changed, 328 insertions(+), 161 deletions(-) diff --git a/docs/src/content/docs/docs/api/dusa.md b/docs/src/content/docs/docs/api/dusa.md index 3ff172c..60eab6b 100644 --- a/docs/src/content/docs/docs/api/dusa.md +++ b/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) diff --git a/docs/src/content/docs/docs/api/dusasolution.md b/docs/src/content/docs/docs/api/dusasolution.md index 2cdeac3..18ce742 100644 --- a/docs/src/content/docs/docs/api/dusasolution.md +++ b/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) diff --git a/docs/src/content/docs/docs/api/terms.md b/docs/src/content/docs/docs/api/terms.md index a2df64b..7ff908e 100644 --- a/docs/src/content/docs/docs/api/terms.md +++ b/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).). diff --git a/docs/src/content/docs/docs/index.md b/docs/src/content/docs/docs/index.md index 3053642..6716a2f 100644 --- a/docs/src/content/docs/docs/index.md +++ b/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). diff --git a/src/cli.test.ts b/src/cli.test.ts index c48914c..6f0e02a 100644 --- a/src/cli.test.ts +++ b/src/cli.test.ts @@ -1,13 +1,17 @@ import { test, expect } from 'vitest'; import { runDusaCli } from './cli.js'; +import { InputFact } from './termoutput.js'; -function testCli(args: string[]) { +function testCli(args: (string | InputFact)[]) { const outs: string[] = []; const errs: string[] = []; return { code: runDusaCli( - args, + args.map((arg) => { + if (typeof arg === 'string') return arg; + return JSON.stringify(arg); + }), (msg) => outs.push(`${msg}`), (msg) => errs.push(`${msg}`), ), @@ -37,6 +41,18 @@ test('Readme examples: mutual exclusion', () => { '{"p":[[{"name":"ff"}]],"q":[[{"name":"tt"}]]}', '{"p":[[{"name":"tt"}]],"q":[[{"name":"ff"}]]}', ]); + + result = testCli(['examples/mutual-exclusion.dusa', '-n0', '-cp', '-qq']); + expect(result.code).toBe(0); + expect(result.errs).toStrictEqual([]); + expect(result.outs.toSorted()).toStrictEqual([ + 'Answer: 1', + 'Answer: 2', + 'SATISFIABLE (2 models)', + 'Solving...', + '{"p":1,"q":[[{"name":"ff"}]]}', + '{"p":1,"q":[[{"name":"tt"}]]}', + ]); }); test('Readme examples: character creation', () => { @@ -68,3 +84,187 @@ test('Readme examples: canonical reps', () => { expect(JSON.parse(result.outs[2])?.isRep?.[5]).toStrictEqual([30]); expect(result.outs[3]).toBe('SATISFIABLE (1+ model)'); }); + +test('CLI argument validation', () => { + result = testCli(['-z']); + expect(result.code).toBe(1); + expect(result.errs[0].slice(0, 20)).toStrictEqual("\nUnknown option '-z'"); + expect(result.outs).toStrictEqual([]); + + result = testCli(['--help']); + expect(result.code).toBe(0); + expect(result.errs[0].split('\n')[1]).toStrictEqual('usage: dusa [options]'); + expect(result.outs).toStrictEqual([]); + + result = testCli(['/dev/null', '-vX']); + expect(result.code).toBe(1); + expect(result.errs[0]).toStrictEqual('--verbose must be an integer'); + expect(result.outs).toStrictEqual([]); + + result = testCli(['/dev/null', '-nX']); + expect(result.code).toBe(1); + expect(result.errs[0]).toStrictEqual("Number of models 'X' not an natural number"); + expect(result.outs).toStrictEqual([]); + + result = testCli(['__invalid__']); + expect(result.code).toBe(1); + expect(result.errs[0].slice(0, 27)).toStrictEqual('Could not read Dusa program'); + expect(result.outs).toStrictEqual([]); + + result = testCli([]); + expect(result.code).toBe(1); + expect(result.errs[0]).toStrictEqual( + '\nA single positional argument, a filename containing a Dusa program, is required.\n', + ); + expect(result.outs).toStrictEqual([]); +}); + +test('Inputs and term validation', () => { + expect(testCli(['/dev/null', '-a', { name: 'p' }])).toStrictEqual({ + code: 0, + errs: [], + outs: ['Solving...', 'Answer: 1', '{"p":[[]]}', 'SATISFIABLE (1+ model)'], + }); + + expect( + testCli(['/dev/null', '-a', { name: 'p', value: 1 }, '-a', { name: 'p', value: 2 }]), + ).toStrictEqual({ + code: 1, + errs: [], + outs: ['Solving...', 'UNSATISFIABLE'], + }); + + expect( + testCli(['/dev/null', '-a', { name: 'p', value: 0 }, '-a', { name: 'p', value: 1 }]), + ).toStrictEqual({ + code: 1, + errs: [], + outs: ['Solving...', 'UNSATISFIABLE'], + }); + + expect( + testCli(['/dev/null', '-a', { name: 'p', value: 1 }, '-a', { name: 'p', value: 1 }]), + ).toStrictEqual({ + code: 0, + errs: [], + outs: ['Solving...', 'Answer: 1', '{"p":[[1]]}', 'SATISFIABLE (1+ model)'], + }); + + expect( + testCli(['/dev/null', '-a', { name: 'p', value: 0 }, '-a', { name: 'p', value: 0 }]), + ).toStrictEqual({ + code: 0, + errs: [], + outs: ['Solving...', 'Answer: 1', '{"p":[[0]]}', 'SATISFIABLE (1+ model)'], + }); + + expect( + testCli(['/dev/null', '-a', { name: 'p', value: 1 }, '-a', { name: 'p', value: 0 }]), + ).toStrictEqual({ + code: 1, + errs: [], + outs: ['Solving...', 'UNSATISFIABLE'], + }); + + expect(testCli(['/dev/null', '-f', '/dev/null'])).toStrictEqual({ + code: 1, + errs: ['Invalid JSON in /dev/null: Unexpected end of JSON input'], + outs: [], + }); + + expect(testCli(['/dev/null', '-a', '/'])).toStrictEqual({ + code: 1, + errs: [`Invalid JSON in command-line fact #1: Unexpected token '/', "/" is not valid JSON`], + outs: [], + }); + + expect(testCli(['/dev/null', '-a', { name: 'p' }, '-a', { name: 'p', args: [1] }])).toStrictEqual( + { + code: 1, + errs: ['Predicate p should have 0 arguments, but the asserted fact has 1'], + outs: [], + }, + ); + + expect(testCli(['/dev/null', '-a', '4'])).toStrictEqual({ + code: 1, + errs: ['Error in command-line fact #1: not an object'], + outs: [], + }); + + expect(testCli(['/dev/null', '-a', '{"name":4}'])).toStrictEqual({ + code: 1, + errs: ["Error in command-line fact #1: 'name' field in fact object not a string"], + outs: [], + }); + + expect(testCli(['/dev/null', '-a', '{"name":"p","args":null}'])).toStrictEqual({ + code: 1, + errs: ["Error in command-line fact #1: 'args' field in fact object not an array"], + outs: [], + }); + + expect(testCli(['/dev/null', '-a', '{"name":"p","args":[{}]}'])).toStrictEqual({ + code: 1, + errs: ["Error in command-line fact #1: no 'name' field in term object"], + outs: [], + }); + + expect(testCli(['/dev/null', '-a', '{"name":"p","args":[{"name":4}]}'])).toStrictEqual({ + code: 1, + errs: ["Error in command-line fact #1: 'name' field in term object not a string"], + outs: [], + }); + + expect(testCli(['/dev/null', '-a', '{"name":"p","args":[{"name":"s","args":0}]}'])).toStrictEqual( + { + code: 1, + errs: ["Error in command-line fact #1: 'args' field in term object not an array"], + outs: [], + }, + ); + + expect( + testCli(['/dev/null', '-a', '{"name":"p","args":[{"name":"s","args":null}]}']), + ).toStrictEqual({ + code: 1, + errs: ["Error in command-line fact #1: 'args' field in term object not an array"], + outs: [], + }); + + expect(testCli(['/dev/null', '-a', { name: 'p' }, '-a', '{}'])).toStrictEqual({ + code: 1, + errs: ["Error in command-line fact #2: no 'name' field in fact object"], + outs: [], + }); + + expect( + testCli( + [ + '/dev/null', + '-v1', + ['-a', { name: 'p', args: [4] }], + ['-a', { name: 'p', args: ['Hello'] }], + ['-a', { name: 'p', args: [{ name: 'c' }] }], + ['-a', { name: 'p', args: [{ name: 's', args: [{ name: 'z' }] }] }], + ['-a', { name: 'p', args: [true] }], + ['-a', { name: 'p', args: [false] }], + ].flat(), + ), + ).toStrictEqual({ + code: 0, + errs: [], + outs: [ + JSON.stringify({ + p: [ + [false], + [true], + ['Hello'], + [4], + [{ name: 'c' }], + [{ name: 's', args: [{ name: 'z' }] }], + ], + }), + ], + }); +}); diff --git a/src/cli.ts b/src/cli.ts index 7113a83..3409eb3 100644 --- a/src/cli.ts +++ b/src/cli.ts @@ -66,17 +66,20 @@ function validateTerm(term: any): term is InputTerm { if (typeof term === 'number') return true; if (typeof term === 'string') return true; if (typeof term === 'boolean') return true; + /* istanbul ignore next -- not possible for json inputs @preserve */ if (typeof term !== 'object') { - throw new Error('term not number, string, boolean, or term object'); + throw new Error( + '(unexpected internal error, please report) term not number, string, boolean, or term object', + ); } - if (!term.name) { + if (term.name === undefined) { throw new Error("no 'name' field in term object"); } if (typeof term.name !== 'string') { throw new Error("'name' field in term object not a string"); } - if (!term.args) return true; - if (typeof term.args !== 'object' || typeof term.args.length !== 'number') { + if (term.args === undefined) return true; + if (!Array.isArray(term.args)) { throw new Error("'args' field in term object not an array"); } return term.args.every(validateTerm); @@ -86,7 +89,7 @@ function validateFact(fact: any): fact is InputFact { if (typeof fact !== 'object') { throw new Error('not an object'); } - if (!fact.name) { + if (fact.name === undefined) { throw new Error("no 'name' field in fact object"); } if (typeof fact.name !== 'string') { @@ -109,7 +112,31 @@ function validateFact(fact: any): fact is InputFact { } } -function validateJsonString(source: string, str: string): InputFact[] { +function validateJsonFact(arg: number, str: string): InputFact { + let input: any; + try { + input = JSON.parse(str); + } catch (e) { + if (e instanceof Error) { + throw new Error(`Invalid JSON in command-line fact #${arg}: ${e.message}`); + } else { + throw e; + } + } + + try { + validateFact(input); + return input; + } catch (e) { + if (e instanceof Error) { + throw new Error(`Error in command-line fact #${arg}: ${e.message}`); + } else { + throw e; + } + } +} + +function validateJsonFacts(source: string, str: string): InputFact[] { let input: any; try { input = JSON.parse(str); @@ -232,8 +259,8 @@ export function runDusaCli( const assertArgs = args.values.assert as string[]; try { for (let i = 0; i < assertArgs.length; i++) { - const facts = validateJsonString(`command-line fact #${i + 1}`, `[${assertArgs[i]}]`); - dusa.assert(...facts); + const fact = validateJsonFact(i + 1, assertArgs[i]); + dusa.assert(fact); } } catch (e) { if (e instanceof Error) err(e.message); @@ -243,7 +270,7 @@ export function runDusaCli( const assertFileArgs = args.values.facts as string[]; try { for (let i = 0; i < assertFileArgs.length; i++) { - const facts = validateJsonString( + const facts = validateJsonFacts( assertFileArgs[i], readFileSync(assertFileArgs[i]).toString('utf-8'), ); diff --git a/src/client.ts b/src/client.ts index ad77a82..1892d1c 100644 --- a/src/client.ts +++ b/src/client.ts @@ -96,7 +96,7 @@ export class Dusa { private inputFact(fact: InputFact): { name: string; args: Data[]; value: Data | null } { const nArgs = fact.args?.length ?? 0; - const hasValue = !!fact.value; + const hasValue = fact.value !== undefined; let arity = this.prog.arities[fact.name]; if (!arity) { @@ -125,7 +125,7 @@ export class Dusa { return { name: fact.name, args: (fact.args ?? []).map((arg) => termToData(this.prog.data, arg)), - value: fact.value ? termToData(this.prog.data, fact.value) : null, + value: fact.value !== undefined ? termToData(this.prog.data, fact.value) : null, }; } diff --git a/src/datastructures/data.test.ts b/src/datastructures/data.test.ts index d2f4727..7682eeb 100644 --- a/src/datastructures/data.test.ts +++ b/src/datastructures/data.test.ts @@ -8,6 +8,8 @@ test('Internalizing basic types', () => { { type: 'int', value: 123n }, { type: 'int', value: 123456789012345678901234567890123456762354n }, { type: 'int', value: 0n }, + { type: 'int', value: 1n }, + { type: 'int', value: -1n }, { type: 'string', value: 'abc' }, { type: 'string', value: '"🦊"' }, { type: 'string', value: "'\n\t\x9DĦ\0\\" }, @@ -31,11 +33,13 @@ test('Internalizing basic types', () => { } expect(data.hide({ type: 'trivial' })).toEqual(data.hide({ type: 'trivial' })); - expect(testData.slice(0, 15).map((d) => data.toString(data.hide(d)))).toStrictEqual([ + expect(testData.slice(0, 17).map((d) => data.toString(data.hide(d)))).toStrictEqual([ '()', '123', '123456789012345678901234567890123456762354', '0', + '1', + '-1', '"abc"', '"\\"\\u{1f98a}\\""', '"\'\\n\\x09\\x9d\\u{126}\\x00\\\\"', diff --git a/src/termoutput.ts b/src/termoutput.ts index 0d84f3e..936b6d7 100644 --- a/src/termoutput.ts +++ b/src/termoutput.ts @@ -90,7 +90,7 @@ export function compareTerm(t1: Term, t2: Term): number { if (typeof t1 === 'bigint' || typeof t1 === 'number') { return typeof t2 === 'bigint' || typeof t2 === 'number' ? Number(t1) - Number(t2) : -1; } - if (typeof t2 === 'bigint') return 1; + if (typeof t2 === 'bigint' || typeof t2 === 'number') return 1; if (t1.name !== null) { if (t2.name === null) return -1; From 1e7a342887a13e61e22dd9f7bbb167747aa22de0 Mon Sep 17 00:00:00 2001 From: "Robert J. Simmons" <442315+robsimmons@users.noreply.github.com> Date: Fri, 22 Nov 2024 16:58:04 -0500 Subject: [PATCH 2/2] Update index.md (#65) --- docs/src/content/docs/docs/index.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/src/content/docs/docs/index.md b/docs/src/content/docs/docs/index.md index 6716a2f..458a51f 100644 --- a/docs/src/content/docs/docs/index.md +++ b/docs/src/content/docs/docs/index.md @@ -24,6 +24,6 @@ the first implementation of finite-choice logic programming. [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 +The easiest way to use Dusa is in our [https://dusa.rocks/](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).