Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Doc tweak #84

Merged
merged 2 commits into from
Nov 29, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion docs/astro.config.mjs
Original file line number Diff line number Diff line change
Expand Up @@ -62,8 +62,8 @@ export default defineConfig({
label: 'JavaScript API',
items: [
{ label: 'class Dusa', link: '/docs/api/dusa/' },
{ label: 'class DusaSolution', link: '/docs/api/dusasolution/' },
{ label: 'Terms', link: '/docs/api/terms/' },
{ label: 'class DusaSolution', link: '/docs/api/dusasolution/' },
{ label: 'Helpers', link: '/docs/api/helpers/' },
{ label: 'Using Dusa in JS', link: '/docs/api/importing/' },
],
Expand Down
4 changes: 2 additions & 2 deletions docs/src/content/docs/docs/api/dusa.md
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ provide access to [`DusaSolution` objects](/docs/api/dusasolution/).
### `sample()` method and `solution` getter

Often all you need is to find a single solution (or to know that at least one
solution exists). The `sample()` method just returns a single solution, but
solution exists). The `sample()` method just returns a single solution, and
will potentially return a different solution every time it is called. The
`solution` getter will generate a sample the first time it is accessed and
will then remember that sample; from then on accessing `dusa.solution` will
Expand Down Expand Up @@ -102,7 +102,7 @@ steps, returning `true` if `next()` can return without any extra computation.
The `stats()` method reports how much work has been done by the iterator so
far, and `all()` returns all remaining solutions as an array.

```javascript
```typescript
advance(limit?: number): boolean;
stats(): { deductions: number; rejected: number; choices: number; nonPos: number };
all(): DusaSolution[];
Expand Down
3 changes: 2 additions & 1 deletion docs/src/content/docs/docs/api/dusasolution.md
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,8 @@ arguments that the proposition has.
### `get()` method

The `get()` method is intended to check the value assigned to a functional
proposition.
proposition. It returns the [term](/docs/api/terms/) associated with the
attribute.

```typescript
get(name: string, ...args: InputTerm): undefined | Term;
Expand Down
14 changes: 9 additions & 5 deletions docs/src/content/docs/docs/api/terms.md
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,11 @@ All Dusa terms have a correspondence with JavaScript types:
- An uninterpreted function with arguments like `h c "fish"` in Dusa
corresponds to an object `{ name: 'h', args: [{ name: 'c' }, 'fish'] }` in JavaScript.

### type `Term`
### type `Term` and `BigTerm`

The `Term` type is more convenient to use in JavaScript; `BigTerm` represents
integers with the `bigint` type and so will correctly represent very positive
or very negative large integers without rounding.

```typescript
export type Term =
Expand All @@ -44,8 +48,8 @@ export interface Fact {
}
export interface BigFact {
name: string;
args: Term[];
value?: Term;
args: BigTerm[];
value?: BigTerm;
}
```

Expand All @@ -59,8 +63,8 @@ inputs that are more flexible than the outputs that Dusa will return (see the

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.
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' }`.
Expand Down