GeezerVison

Copy link

Copy Markdown

Collaborator

rcosta358 requested a review from CatarinaGamboa March 19, 2026 13:42

CatarinaGamboa approved these changes Mar 27, 2026

View reviewed changes

Sorry, something went wrong.

Uh oh!

There was an error while loading. Please reload this page.

1 check passed

rcosta358 deleted the expand-aliases branch March 30, 2026 12:22

Closes #295.

A refinement error now says what the aliases in Found and Expected mean,
both as structured data for the IDE and as text in the CLI.

## CLI
The message keeps the alias names. Under it, one `where` line per alias
the message uses, in order of appearance (Found first, then Expected),
each alias once. The definition is printed as the spec wrote it:
parameter names and named constants unchanged, whitespace collapsed to
one line.

**Nested aliases.** When a definition uses another alias, that alias
gets its own `where` line after the one that uses it, and so on down.
Recursive aliases are not expanded again.

### Repro 1: minimal, aliases in both Found and Expected
```java
@RefinementAlias("Positive(int x) { x > 0 }")
@RefinementAlias("Nat(int x) { x >= 0 }")
public class Probe {
    static void need(@refinement("Positive(_)") int v) {}
    static void run(@refinement("Nat(_)") int n) { need(n); }
}
```
Before:
```
Refinement Error: Nat(n) is not a subtype of Positive(n)
```
After:
```
Refinement Error: Nat(n) is not a subtype of Positive(n)
  where Nat(x) = x >= 0
  where Positive(x) = x > 0
```

### Repro 2: external spec with named constants
The `x_e_oss_a1_01_sliderecoder` exercise, with the `ImageWriteMode`
alias from the issue on the `javax.imageio.ImageWriteParam` spec,
`setCompressionMode(@refinement("ImageWriteMode(_)") int mode)`, and
`wParam.setCompressionMode(4);` after `getDefaultWriteParam()`.

Before:
```
Refinement Error: mode³⁰⁶ == 4 is not a subtype of ImageWriteMode(mode³⁰⁶)
```
After:
```
Refinement Error: mode³⁰⁶ == 4 is not a subtype of ImageWriteMode(mode³⁰⁶)
  where ImageWriteMode(m) = m == ImageWriteParam.MODE_DISABLED || m == ImageWriteParam.MODE_DEFAULT || m == ImageWriteParam.MODE_EXPLICIT || m == ImageWriteParam.MODE_COPY_FROM_METADATA
```

### Repro 3: `Port` alias
The `y_e_oss_a2_04_vmwarecimprobe` exercise plus `static
InetSocketAddress agentAt(String host, int port) { return new
InetSocketAddress(host, port); }`.

Before:
```
Refinement Error: expected Port(port⁶⁵) but could not prove it
 --> Counterexample: port⁶⁵ == 65536
```
After:
```
Refinement Error: expected Port(port⁶⁵) but could not prove it
  where Port(p) = 0 <= p && p <= 65535
 --> Counterexample: port⁶⁵ == 65536
```
The exercise's other error (`expected timeout >= 0 but could not prove
it`) uses no alias and is unchanged.

### Nested aliases and argument order
```
Refinement Error: expected Small(n) but could not prove it
  where Small(x) = Nat(x) && x < 10
  where Nat(x) = x >= 0

Refinement Error: Below(3, b) is not a subtype of Below(b, 5)
  where Below(a, b) = a < b
```

## Structured data for the IDE
`RefinementError` has two new accessors:
- `getFoundAliases()`: one entry per distinct alias invocation in the
final simplified Found VC chain, the chain the extension renders as
Found.
- `getExpectedAliases()`: the same for Expected.

Each returns a `List<liquidjava.diagnostics.AliasExpansion>`. Entries
come in order of appearance, followed by the aliases their definitions
use. `AliasExpansion` is a record:

| field | example | meaning |
|---|---|---|
| `invocation` | `Nat(n)` | the invocation as the diagnostic displays
it, so the client can find it in the Found/Expected text |
| `expansion` | `n >= 0` | the definition with the parameters replaced
by the arguments (all at once). Nested alias invocations are kept and
have their own entry |
| `alias` | `Nat` | alias name |
| `parameters` | `["x"]` | parameter names |
| `definition` | `x >= 0` | definition as written in the
`@RefinementAlias` |
| `declarationPosition` | `SourcePosition` | the `@RefinementAlias`
annotation value, for go-to-definition |

`declaration()` gives `Nat(x) = x >= 0`. `getMessageNotes()`, new on
`LJDiagnostic` and empty by default, returns the CLI `where` lines.

The extension would need to add these to `RefinementErrorDTO`, e.g.
`foundAliases` / `expectedAliases` built from a small
`AliasExpansionDTO`, with `declarationPosition` converted via
`SourcePositionDTO.from`. For repro 1 that gives:
```json
"foundAliases": [
  { "invocation": "Nat(n)", "expansion": "n >= 0", "alias": "Nat", "parameters": ["x"],
    "definition": "x >= 0", "declarationPosition": { "file": ".../Probe.java", "lineStart": …, "colStart": …, "lineEnd": …, "colEnd": … } }
],
"expectedAliases": [
  { "invocation": "Positive(n)", "expansion": "n > 0", "alias": "Positive", "parameters": ["x"],
    "definition": "x > 0", "declarationPosition": { "file": ".../Probe.java", "lineStart": …, "colStart": …, "lineEnd": …, "colEnd": … } }
]
```
Positions are elided above; they are the `@RefinementAlias` value range
in the extension's 0-based `SourcePositionDTO` form. With that DTO, the
webview can show each invocation's expansion next to Found and Expected
(hover or an expandable row) and link `alias` to `declarationPosition`.
The extension is not changed in this PR.

## Changes
- `AliasWrapper` keeps the definition text as written (whitespace
collapsed to one line, except inside string and char literals) and the
declaration position. `AliasDTO` exposes the raw text it already parsed.
- `AliasExpansion` (new) collects and substitutes the invocations.
- `RefinementError` takes the context aliases (from `VCChecker`) and
computes the expansions and the `where` lines.
- `LJDiagnostic.toString` prints the message notes under the message.

The earlier derivation-based expansion from #184, removed in #261,
attached alias bodies as origins in the expression derivation tree. The
VC chain has no such per-node origins, so this PR records the expansions
alongside the chain instead. It reuses the old approach of substituting
the arguments into the alias body.

`StateRefinementError` is not covered. Its Expected is states, and it
has its own Found shape.

## Tests
`TestAliasExpansions` (2 tests, existing fixtures, no new ones):
- `ErrorAlias`: Found and Expected each record their substituted
`InRange` invocation, with parameters and declaration line.
- `ErrorStaticFinalInAlias`: one `where` line with the constants as
written, printed right under the message.

Full verifier module (rebased on main): 708 tests, 0 failures.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 5.5 <[email protected]>