Repository navigation
Expand Aliases - #184
Merged
Merged
Expand Aliases#184
Conversation
rcosta358
added
enhancement
CatarinaGamboa
approved these changes
Mar 27, 2026
CatarinaGamboa
left a comment
CatarinaGamboa
left a comment
Collaborator
There was a problem hiding this comment.
Great! As we discussed passing the context can be kinda weird. We can see if we can change the codebase to always use the ctx as a singleton (since it actually is a singleton) instead of as an argument in so many methods
CatarinaGamboa
added a commit
that referenced
this pull request
Nov 5, 2026
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 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #160. Adds a new alias expansion pass in the simplification that adds the alias body as an origin of an alias invocation, substituting its parameters with the provided arguments. Works by extracting the aliases from the context and passing them to the simplification logic and reusing the
ValDerivationNodeto represent alias expansions, which is enough for this purpose and avoids requiring changes to the VS Code extension.Example
When we invoke the alias
Byte(int b) { b >= -128 && b <= 127 }")withByte(#v_8), we get:{ "value": "Byte(#v_8)", "origin": { "value": "#v_8 >= -128 && #v_8 <= 127" } }