Skip to content
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
124 changes: 124 additions & 0 deletions ts/docs/architecture/actionGrammar.md
Original file line number Diff line number Diff line change
@@ -1,5 +1,13 @@
# Action Grammar — Architecture & Design

> **Scope:** This document is the implementation reference for the
> `actionGrammar` package — the grammar language (`.agr` syntax,
> entities, spacing modes, value expressions), the compilation pipeline,
> and the matching algorithms (full matching and completion matching).
> For the cross-layer completion pipeline (cache → dispatcher → shell →
> CLI), metadata contracts, and correctness invariants, see
> `completion.md`.

## Overview

The `action-grammar` package is TypeAgent's natural language understanding
Expand Down Expand Up @@ -610,6 +618,122 @@ input `"play"`:
separator, so `directionSensitive` is always `true` when any word has
been fully matched — trailing spaces do not commit.

### Forward/backward equivalence analysis

Given `input` and `matchPrefixLength` P, does
`completion(input[0..P], "forward")` produce the same result as
`completion(input[0..P], "backward")`?

The answer depends on **where P lands** in the grammar structure, the
**separator mode**, and whether there is a **trailing separator** after
the last matched item.

**Terminology:**

- **Committed:** a separator character follows the last matched
word/wildcard in `input[0..P]`
(i.e. `nextNonSeparatorIndex(input[0..P], endIndex) > endIndex`).
- **Uncommitted:** the last matched item runs to end-of-string with no
trailing separator.

#### P at a keyword boundary (between parts)

| Mode / Trailing sep | Fwd = Bwd? | Why |
| ------------------------------------- | ---------- | ------------------------------------------------------- |
| `required`/`auto` — committed | **Yes** | Separator commits; nothing to reconsider |
| `required`/`auto` — uncommitted (EOI) | **No** | Backward re-offers keyword; forward offers next part |
| `optional`/`auto` (CJK) — committed | **Yes** | Separator commits |
| `optional`/`auto` (CJK) — uncommitted | **No** | Backward backs up; forward advances |
| `none` | **No** | `couldBackUp` always true when `spacingMode === "none"` |

#### P inside a multi-word keyword (between words of one keyword)

| Mode / Trailing sep | Fwd = Bwd? | Why |
| ------------------------------------- | ---------- | ----------------------------------- |
| `required`/`auto` — committed | **Yes** | Separator commits word K |
| `required`/`auto` — uncommitted (EOI) | **No** | Backward backs up to `prevEndIndex` |
| `optional` — committed | **Yes** | Separator commits |
| `optional` — uncommitted | **No** | Backward reconsiders word K |
| `none` | **No** | `couldBackUp` always true |

#### P at a wildcard-keyword boundary (wildcard finalized at EOI, next part is string)

Wildcard boundaries are always ambiguous — the wildcard could absorb
more text, moving the boundary forward. The grammar matcher sets
`openWildcard=true` and `directionSensitive=true` unconditionally for
these positions. The table below explains _why_ the directions always
differ at these boundaries.

| Mode / Partial keyword? | Fwd = Bwd? | Why |
| ------------------------------------------------ | ---------- | ----------------------------------------------------------------- |
| non-`none` — no partial keyword | **No** | Forward defers to Phase B; backward backs up to wildcard start |
| non-`none` — partial at Q < P | **No** | Both find partial at Q, but backward can also back up — ambiguous |
| non-`none` — partial at Q = P (full word at EOI) | **No** | Forward uses it; backward rejects (Q < `state.index` required) |
| `none` — any | **No** | `couldBackUp` always true |

#### P inside a wildcard (no keyword boundary reached)

| What follows P? | Fwd = Bwd? | Why |
| ------------------------------------------- | ---------- | ---------------------------------------------------------------- |
| Non-separator text (Cat 3a) | **No** | Forward: property completion; backward: backs up to last keyword |
| Separator / nothing (wildcard just started) | **No**\* | Backward reconsiders preceding keyword |

\* When `lastMatchedPartInfo` exists.

#### P = 0 (nothing matched)

| Scenario | Fwd = Bwd? | Why |
| ------------------------------ | ---------- | -------------------------------------------------------- |
| Partial first keyword (Cat 3b) | **Yes** | `couldBackUp = false`; backward falls through to forward |

#### P = input.length, all parts matched (Category 1: exact match)

| Scenario | Fwd = Bwd? | Why |
| ------------------- | ---------- | ----------------------------------------------------------- |
| All parts satisfied | **Yes** | Both use `tryCollectBackwardCandidate` — direction-agnostic |

#### Decision tree

The `directionSensitive` flag is computed by the following decision tree,
evaluated once after all candidates are collected using the final
`maxPrefixLength` (P).

```
openWildcard?
└─ Yes → DIFFERENT (wildcard boundary is ambiguous;
backward can always reconsider)

P = minPrefixLength (or 0 if unset)?
└─ Yes → SAME (nothing matched beyond the caller's floor;
backward has nothing to reconsider)

P < input.length? (midPosition)
└─ Yes → DIFFERENT (truncated input ends at keyword boundary
with no trailing separator — backward always backs up)

P = input.length:
└─ Trailing separator advanced P past last matched item?
├─ Yes → SAME (separator commits the position)
└─ No → DIFFERENT (no separator — backward can reconsider)
```

**Key insight:** The separator is the universal "commit" mechanism.
Once `input[0..P]` ends with a separator after the last matched item,
the position is committed and both directions agree. Without that
separator (including `none` mode where separators don't exist),
backward has the option to reconsider — and the directions diverge.

**Design choice — openWildcard → always true:** Even when both
directions happen to find the same partial keyword at the same position
(e.g. "play Never b" where both find "b"→"by" at position 11), the
wildcard boundary is ambiguous. Truncating to `input[0..P]` removes
the content that established the anchor, so
`completion(input[0..P], "backward")` always diverges — confirming
that the position is genuinely direction-sensitive under the cross-query
definition (invariant #4 in `completion.md`). This also simplifies the
implementation (no `partialKeywordAgrees` tracking needed) and enables
unguarded cross-query invariant checking in tests.

**Metadata produced:**

- `matchedPrefixLength` — characters consumed; becomes `startIndex`
Expand Down
62 changes: 45 additions & 17 deletions ts/docs/architecture/completion.md
Original file line number Diff line number Diff line change
@@ -1,5 +1,14 @@
# Completion Architecture

> **Scope:** This document describes the cross-layer completion pipeline
> — how completions flow from the grammar matcher through the cache,
> dispatcher, agent SDK, shell, and CLI layers. It defines the metadata
> contract (`startIndex`, `separatorMode`, `closedSet`,
> `directionSensitive`, `openWildcard`), the shell state machine, and
> correctness invariants. For the grammar language, compilation
> pipeline, and grammar-level matching algorithms (categories, direction
> semantics, equivalence analysis), see `actionGrammar.md`.

## Overview

TypeAgent's completion system provides real-time, context-aware completions
Expand Down Expand Up @@ -546,25 +555,42 @@ wildcard and the results differ (→ `directionSensitive=true`).
See `actionGrammar.md` "When direction does _not_ matter" for the
full list, including the `[spacing=none]` exception.

The flag is a **biconditional**: `directionSensitive=true` if and only
if forward and backward produce different results. There are no false
positives (see invariant #3).
The flag is correct under the cross-query invariant definition:
`directionSensitive=true` if and only if
`completion(input[0..P], "backward")` differs from the forward result.
For `openWildcard` positions, truncating to `input[0..P]` removes the
content that established the anchor, so backward on the truncated input
always diverges — even when both directions happen to agree on the
original (longer) input. See invariant #4.

**Decision tree** (evaluated once after all candidates are collected):

```
openWildcard → true (ambiguous boundary; backward can reconsider)
P = minPrefixLength → false (nothing matched beyond caller's floor)
midPosition → true (keyword boundary, no trailing separator)
P = prefix.length → !trailingSepAdvanced
```

See the "Forward/backward equivalence analysis" section in
`actionGrammar.md` for the full position-by-position analysis.

**Examples:** The table below shows `directionSensitive` for various
inputs. The general pattern: `true` when a part is fully matched with
no trailing separator; `false` when partial, committed by whitespace,
or dirty.

| Rule | Input | `directionSensitive` | Why |
| ---------------------- | ------------ | -------------------- | ------------------------------------------------------------- |
| `play <song> by <a>` | `play` | `true` | `"play"` fully matched, backward can reconsider |
| `play <song> by <a>` | `play ` | `false` | Trailing space commits |
| `play <song> by <a>` | `play Never` | `true` | `"Never"` in wildcard, keyword `"by"` next; no trailing space |
| `play <song> by <a>` | `pla` | `false` | Only partial match (Category 3b) — nothing to back up to |
| `play music` | `play` | `true` | `"play"` fully matched, no trailing space |
| `play music` | `play ` | `false` | Trailing space commits |
| `(play \| player) now` | `play` | `true` | Backward: `["play","player"]` at mpl=0; forward: `["now"]` |
| `(play \| player) now` | `play ` | `false` | Trailing space commits |
| Rule | Input | `directionSensitive` | Why |
| ---------------------- | -------------- | -------------------- | ------------------------------------------------------------- |
| `play <song> by <a>` | `play` | `true` | `"play"` fully matched, backward can reconsider |
| `play <song> by <a>` | `play ` | `false` | Trailing space commits |
| `play <song> by <a>` | `play Never` | `true` | `"Never"` in wildcard, keyword `"by"` next; no trailing space |
| `play <song> by <a>` | `play Never b` | `true` | `openWildcard=true` — wildcard boundary ambiguous |
| `play <song> by <a>` | `pla` | `false` | Only partial match (Category 3b) — nothing to back up to |
| `play music` | `play` | `true` | `"play"` fully matched, no trailing space |
| `play music` | `play ` | `false` | Trailing space commits |
| `(play \| player) now` | `play` | `true` | Backward: `["play","player"]` at mpl=0; forward: `["now"]` |
| `(play \| player) now` | `play ` | `false` | Trailing space commits |

The dispatcher may additionally set `directionSensitive=true` at the
command level — for example, when a subcommand name is both a valid
Expand Down Expand Up @@ -749,20 +775,17 @@ _Impact:_ False negative → stale menu after backspace.
_#3b — Forward not direction-sensitive → backward on truncated agrees._
`!forward.directionSensitive` →
`forward === completion(input[0..fwd.mpl], "backward")`.
Skipped when `forward.openWildcard` (ambiguous boundary).
_Impact:_ False negative → stale menu; false positive → unnecessary
re-fetch.

_#3c — Backward not direction-sensitive → forward on truncated agrees._
`!backward.directionSensitive` →
`backward === completion(input[0..bwd.mpl], "forward")`.
Skipped when `backward.openWildcard` (ambiguous boundary).
_Impact:_ Same as #3b.

**#4 — Forward direction-sensitive → backward backs up.**
`forward.directionSensitive` →
`completion(input[0..fwd.mpl], "backward").matchedPrefixLength < fwd.mpl`.
Skipped when `forward.openWildcard`.
_Impact:_ Backspacing shows different completions than forward-typing to
the same position — the menu is inconsistent depending on how the user
arrived at that input.
Expand All @@ -771,10 +794,15 @@ arrived at that input.
When `fwd.mpl ≠ bwd.mpl` and `backward.directionSensitive`:
`completion(input[0..bwd.mpl], "forward").matchedPrefixLength ≥ bwd.mpl`.
Confirms that backward's backed-up position is reachable from forward.
Skipped when `backward.openWildcard`.
_Impact:_ User sees only one completion branch when backspacing at a fork —
other valid alternatives are silently lost.

Note: invariants #3b–#5 previously skipped `openWildcard` cases because
truncating to an ambiguous wildcard boundary removed the content that
established the anchor. With `openWildcard → directionSensitive=true`,
#3b/#3c never fire for openWildcard (the guard is `!directionSensitive`),
and #4/#5 validate correctly (backward on truncated does back up).

### Field-specific invariants

**#6 — `separatorMode` = `"none"` for `[spacing=none]` rules.**
Expand Down
Loading
Loading