Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
62f82e2
feat(runtime): evaluate cast expressions
devin-ai-integration[bot] Sep 8, 2026
e095bc6
fix(runtime): read a scalar's library type when casting
devin-ai-integration[bot] Sep 8, 2026
3fc1d81
fix(runtime): apply Positive's bound and keep an empty cast's unit
devin-ai-integration[bot] Sep 8, 2026
dc13cbe
feat(runtime): decide structured-value casts by the value
devin-ai-integration[bot] Sep 8, 2026
6cb6053
fix(runtime): read a scalar's type for a cast from the library
devin-ai-integration[bot] Sep 8, 2026
02e615f
feat(runtime): decide casts by a value's declared type
devin-ai-integration[bot] Sep 8, 2026
6032337
feat(runtime): classify casts by every declared type and by unions
devin-ai-integration[bot] Sep 8, 2026
203dc9b
feat(semantics): classify casts by intersections and differences too
devin-ai-integration[bot] Sep 8, 2026
5276eaf
fix(semantics): weigh every type a value is of against a composed target
devin-ai-integration[bot] Sep 8, 2026
1272097
fix(semantics): keep a subtracted type excluding a value through spec…
devin-ai-integration[bot] Sep 8, 2026
a1f24c1
fix(runtime): read a composed cast target through its operands
devin-ai-integration[bot] Sep 8, 2026
57bdab9
docs(runtime): shorten the composed cast comment
devin-ai-integration[bot] Sep 8, 2026
4b0a459
fix(semantics): weigh every declared type against a difference cast t…
devin-ai-integration[bot] Sep 8, 2026
da10d0b
fix(semantics): select from a composed cast target and judge each ele…
devin-ai-integration[bot] Sep 8, 2026
8d3bc94
fix(runtime): cast a written sequence entry by entry
devin-ai-integration[bot] Sep 8, 2026
0e7c20f
fix(runtime): let a composed cast's decisive operand settle an undeci…
devin-ai-integration[bot] Sep 8, 2026
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
6 changes: 3 additions & 3 deletions .agents/skills/testing-pilot-execution-referee/SKILL.md
Original file line number Diff line number Diff line change
Expand Up @@ -63,10 +63,10 @@ Use `-cases DIR` for another directory of `.cases` files, `-out DIR`,
lines followed by `id :: target :: expression` lines. Reports go to
`build/pilot-exec-diff/pilot-exec-diff.{txt,json}`.

Reference values at the current implementation (147 cases, all eight default
Reference values at the current implementation (154 cases, all nine default
fixtures):
`agree 69 · kind-only 1 · order-only 0 · disagree 4 · pilot-unevaluated 57 ·
pilot-silent 4 · pilot-error 2 · ours-error 2 · both-error 8 ·
`agree 71 · kind-only 1 · order-only 0 · disagree 4 · pilot-unevaluated 59 ·
pilot-silent 7 · pilot-error 2 · ours-error 2 · both-error 8 ·
nondeterministic 0`.
All four `disagree` are unrefereeable rather than verdicts against us:
`w6d:complex-is-zero-qualified`, where the pilot answers `false` for
Expand Down
33 changes: 33 additions & 0 deletions changes/unreleased/cast-expression-evaluation.added.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
- **`x as T` is evaluated.** A cast selects the values of `x` that `T` classifies, in order, and
answers the empty sequence when none does, so `4.0 as Integer` is `4.0`, `2.5 as Integer` is
`()` and `(1, 2.5, 3) as Integer` is `(1, 3)`. Scalars are judged by their magnitude against
the `ScalarValues` hierarchy, quantities by whether their unit is commensurable with the
dimension the target fixes, arrays, vectors, vector and tensor quantities, measurement
references, frames and transformations by their shape, units and frame, and objects and
enumeration literals by the types they carry.
A type composed of others classifies as they do — the values of a union are those of any of the
types it unions, of an intersection those of every type it intersects, of a difference those of
the first that are none of the rest, however deeply nested — so a cast to one keeps them, the
feature it is written to holds them, and `istype` answers for them; casting a value of a union to
one of its members is not reported as unrelated either, nor is casting a value to a type composed
of one it relates to.
A composed target a value's types leave open is read through its operands, so a bare quantity
cast to a union of quantity types is kept by the operand whose reference its unit matches, and an
operand the value settles nothing about is reported as undecided only where no other operand
excludes the value outright.
A composed type weighs all the types a value is of at once, whether they are the types a runtime
value carries or those its feature is declared with, so an object held as a type a
difference subtracts is none of its values, whether the difference is the target, one it
specializes, or one an intersection of it reaches.
Every type a value's feature is declared with counts among the types it is of, so a custom scalar
subtype (`attribute e : Even = 4`) and a scalar-valued enumeration keep the values declared with
them — a written sequence entry by entry, each judged by its own declaration however many values
it holds and however deeply nested, so `(GradePoints::a, GradePoints::b) as GradePoints` keeps
both and no entry is judged by another's type — and a quantity subtype narrowing its dimension by something a magnitude and a unit do not
state keeps a value declared with it. An expression written as a value is kept by the evaluation
type it is read as, a boolean body by `BooleanEvaluation`.
A cast converts nothing: `ToInteger` and its siblings remain the library functions that do.
A target that neither a value's types nor its content settles is reported rather than silently
dropping the value.
- **Classifying a value is model-level evaluable.** `as`, `istype` and `hastype` read the type they
name rather than folding their operand, so a metadata body may bind `x = 1 as Integer`.
14 changes: 14 additions & 0 deletions cmd/pilot-exec-diff/testdata/cases/cast_expressions.cases
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
model: cmd/pilot-exec-diff/testdata/models/cast_expressions.sysml

# `x as T` selects the values of x that T classifies and converts nothing
# (KerML CastExpression): a whole Real is an Integer, 2.5 is not, and a
# sequence is filtered element-wise. As with the classification cases, the
# pilot cannot resolve ScalarValues names inside a bare %eval, so each case
# reads a model-level attribute bound to the cast.
integer-as-real :: :: Cast::integerAsReal
integer-as-natural :: :: Cast::integerAsNatural
fraction-as-integer :: :: Cast::fractionAsInteger
whole-as-integer :: :: Cast::wholeAsInteger
sequence-as-integer :: :: Cast::sequenceAsInteger
car-as-vehicle :: :: Cast::carAsVehicle
car-as-car :: :: Cast::carAsCar
20 changes: 20 additions & 0 deletions cmd/pilot-exec-diff/testdata/models/cast_expressions.sysml
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
package Cast {
private import ScalarValues::*;

part def Vehicle;
part def Car :> Vehicle;

attribute n : Integer = 7;
attribute r : Real = 2.5;
attribute whole : Real = 4.0;
attribute seq : Real[*] = (1, 2.5, 3);
part car : Car;

attribute integerAsReal = n as Real;
attribute integerAsNatural = n as Natural;
attribute fractionAsInteger = r as Integer;
attribute wholeAsInteger = whole as Integer;
attribute sequenceAsInteger = seq as Integer;
ref part carAsVehicle = car as Vehicle;
ref part carAsCar = car as Car;
}
20 changes: 15 additions & 5 deletions docs/project/pilot-execution-referee.md
Original file line number Diff line number Diff line change
Expand Up @@ -211,15 +211,15 @@ Run it with `go run ./cmd/pilot-exec-diff` after `./scripts/download-pilot-evalu
execution artifact absent it prints a provisioning instruction, exits 0 and writes nothing, so
`cmd/pilot-diff` and its committed baseline are untouched. The bucket counts below are as measured
when this record was last updated and are not the current baseline — `go run ./cmd/pilot-exec-diff`
prints the current ones. State of the 147 committed cases, the original 32, the 62 the
prints the current ones. State of the 154 committed cases, the original 32, the 62 the
expression round added, the 10 of `value_classification.cases`, the 3 of `contextual_names.cases`,
the 14 of `rational_terms.cases`, the 5 the empty-aggregate and subsetting round added to
`w6d_expr_depth.cases` the 12 of `tensor_quantities.cases` and the 9 of
`coordinate_frames.cases`:
`w6d_expr_depth.cases` the 12 of `tensor_quantities.cases`, the 9 of
`coordinate_frames.cases` and the 7 of `cast_expressions.cases`:

```
agree: 69 · kind-only: 1 · order-only: 0 · disagree: 4
pilot-unevaluated: 57 · pilot-silent: 4 · pilot-error: 2 · ours-error: 2 · both-error: 8
agree: 71 · kind-only: 1 · order-only: 0 · disagree: 4
pilot-unevaluated: 59 · pilot-silent: 7 · pilot-error: 2 · ours-error: 2 · both-error: 8
nondeterministic: 0
```

Expand Down Expand Up @@ -262,6 +262,16 @@ metadata reading, which the pilot does not share (its `@` is `istype` throughout
`false`); no committed case probes it, since the corpus was written model-level and the
annotation forms are pinned by the runtime conformance fixtures instead.

The seven `cast_expressions.cases` probe `x as T`, added with the evaluation they referee. Two
agree: `n as Real` on `n : Integer = 7` answers `7` on both sides, and `(1, 2.5, 3) as Integer`
answers `(1, 3)` on both — the cast selects element-wise and converts nothing. Three are
`pilot-silent`: `n as Natural`, `2.5 as Integer` and `4.0 as Integer` draw no output at all from
the pilot, so its reading of a value the target does not classify (we answer the empty sequence
for `2.5 as Integer`) and of an integral `Real` cast to `Integer` (we keep `4.0`) is unobservable
here. The two part cases, `car as Vehicle` and `car as Car`, land in `pilot-unevaluated`: the
pilot answers with the unevaluated `PartUsage car`, which names the same value we select but is
not an evaluation of the cast.

The three `contextual_names.cases` all agree, and they were added with the parser fix they
referee: `chain` is the feature chain modifier only when a name follows it, so `attribute chain =
1;` declares a feature named `chain` and `chain + 1` reads it — where before the parser took the
Expand Down
15 changes: 9 additions & 6 deletions docs/project/spec-compliance.md

Large diffs are not rendered by default.

15 changes: 13 additions & 2 deletions internal/core/passes/typecheck_operator_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -107,7 +107,7 @@ const castFixture = `package P {
function F { return r : A; }
classifier Q; classifier R :> Q; classifier CQ ~ Q; feature cq : CQ;
feature xs : A[*];
feature d : D;
feature d : D; feature b : B; datatype U unions B, C; datatype I intersects A, C; datatype NI intersects I, B; datatype Diff differences A, C; feature u : U; feature dd : Diff;
feature untyped;
feature valued = 3;
%s
Expand Down Expand Up @@ -136,6 +136,13 @@ func TestCastConformanceUnrelatedTypes(t *testing.T) {
castDiags(t, "", `feature bad = (1 < 2) as Integer;`, "16:16 cast argument is typed by Boolean, unrelated to the target Integer")
castDiags(t, "", `feature bad = xs.?{in x; true} as C;`, "16:16 cast argument is typed by A, unrelated to the target C")
castDiags(t, "", `feature bad = a#(1) as C;`, "16:16 cast argument is typed by A, unrelated to the target C")
castDiags(t, "", `feature bad = u as String;`, "16:16 cast argument is typed by U, unrelated to the target String")
castDiags(t, "", `feature bad = s as I;`, "16:16 cast argument is typed by String, unrelated to the target I")
// Every value of D is one of C's, which the difference subtracts.
castDiags(t, "", `feature bad = d as Diff;`, "16:16 cast argument is typed by D, unrelated to the target Diff")
castDiags(t, "", `feature bad = dd as C;`, "16:16 cast argument is typed by Diff, unrelated to the target C")
// A value of C as well as of A is none of the values A minus C holds.
castDiags(t, "", `feature bad = ab as Diff;`, "16:16 cast argument is typed by A and C, unrelated to the target Diff")
castDiags(t, "", `feature bad = a as s;`, "16:16 cast argument is typed by A, unrelated to the target s")
castDiags(t, "", `feature bad = cq as R;`, "16:16 cast argument is typed by CQ, unrelated to the target R")
castDiags(t, `feature bad = base as String;`, "", "9:59 cast argument is typed by A, unrelated to the target String")
Expand All @@ -145,7 +152,8 @@ func TestCastConformanceUnrelatedTypes(t *testing.T) {
}

// A cast up, down, or sideways through one of several types conforms; so does
// one whose argument's type is not statically known, or is Anything.
// one whose argument's type is not statically known, or is Anything, and one
// between a composed type and a type it is composed of.
func TestCastConformanceRelatedTypes(t *testing.T) {
castDiags(t, "", `feature up = a as Base::Anything; feature down = a as B; feature same = a as A; feature self = a as a;`)
castDiags(t, "", `feature one = ab as B; feature other = ab as C; feature viaD = d as C;`)
Expand All @@ -155,6 +163,9 @@ func TestCastConformanceRelatedTypes(t *testing.T) {
castDiags(t, "", `feature wide = untyped as String; feature nothing = null as A; feature real = 3 as Real;`)
castDiags(t, "", `feature data = (1 + 2) as String; feature seq = (1, 2) as Integer; feature body = xs.{in x; x} as C;`)
castDiags(t, "", `feature cond = (if true ? a else a) as C; feature sel = xs.?{in x; true} as B;`)
castDiags(t, "", `feature union = a as U; feature member = u as B; feature wider = u as A;`)
castDiags(t, "", `feature meet = d as I; feature less = b as Diff; feature kept = dd as A;`)
castDiags(t, "", `feature operand = a as I; feature nestedOperand = a as NI;`)
}

// The rule is KerML's, but SysML declares the same operator: a usage cast to an
Expand Down
37 changes: 37 additions & 0 deletions internal/core/passes/w8d_metadata_usage_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -175,3 +175,40 @@ func TestW8DLegalMetadataAnnotationsStaySilent(t *testing.T) {
}
}
}

// Classifying a value is evaluated from the model: `as`, `istype` and `hastype`
// read the type they name rather than folding their operand, so a metadata value
// written with one is model-level evaluable — unless its operand is not.
func TestW8DMetadataClassificationValuesAreModelLevelEvaluable(t *testing.T) {
src := `package Test {
private import ScalarValues::*;
metadata def A {
attribute x : Integer[0..*];
attribute b : Boolean[0..*];
}
part def P { attribute own : Integer = 1; }
part p : P {
@A {
x = 1 as Integer;
b = (1 istype Integer, 1 hastype Real);
}
}
}
`
if lines := w8dLines(t, src, "metadata-value-not-evaluable"); len(lines) != 0 {
t.Fatalf("classification values reported at lines %v", lines)
}

src = `package Test {
private import ScalarValues::*;
metadata def A { attribute x : Integer[0..*]; }
part def P { attribute own : Integer = 1; }
part p : P {
@A {
x = own as Integer;
}
}
}
`
w8dWantLines(t, src, "metadata-value-not-evaluable", 7)
}
Loading
Loading