diff --git a/.agents/skills/testing-pilot-execution-referee/SKILL.md b/.agents/skills/testing-pilot-execution-referee/SKILL.md index 640defd2e..3710fae56 100644 --- a/.agents/skills/testing-pilot-execution-referee/SKILL.md +++ b/.agents/skills/testing-pilot-execution-referee/SKILL.md @@ -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 diff --git a/changes/unreleased/cast-expression-evaluation.added.md b/changes/unreleased/cast-expression-evaluation.added.md new file mode 100644 index 000000000..627af89bc --- /dev/null +++ b/changes/unreleased/cast-expression-evaluation.added.md @@ -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`. diff --git a/cmd/pilot-exec-diff/testdata/cases/cast_expressions.cases b/cmd/pilot-exec-diff/testdata/cases/cast_expressions.cases new file mode 100644 index 000000000..1fee5a6be --- /dev/null +++ b/cmd/pilot-exec-diff/testdata/cases/cast_expressions.cases @@ -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 diff --git a/cmd/pilot-exec-diff/testdata/models/cast_expressions.sysml b/cmd/pilot-exec-diff/testdata/models/cast_expressions.sysml new file mode 100644 index 000000000..d828d44bb --- /dev/null +++ b/cmd/pilot-exec-diff/testdata/models/cast_expressions.sysml @@ -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; +} diff --git a/docs/project/pilot-execution-referee.md b/docs/project/pilot-execution-referee.md index 5cd990651..e0f7960c6 100644 --- a/docs/project/pilot-execution-referee.md +++ b/docs/project/pilot-execution-referee.md @@ -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 ``` @@ -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 diff --git a/docs/project/spec-compliance.md b/docs/project/spec-compliance.md index 8cb37da0a..1c846c30d 100644 --- a/docs/project/spec-compliance.md +++ b/docs/project/spec-compliance.md @@ -227,8 +227,9 @@ Each row documents one behavioral semantic feature: | A calc usage's outputs are evaluation results, not feature values of an object | `runtime/calc_usage.go` (no instance materialization) | `calc_usage_instance_slots.sysml` (the features fed by the outputs are feature values; the usage itself is not), pilot-exec-diff `w6d:calc-usage` | ⚠️ Approximate (unrefereeable: the pinned artifact answers a `CalculationUsage` node rather than an output value. `%instances` and export show the features valued from outputs, not the usage's outputs themselves) | | Boolean operators evaluated at runtime (`and`, `or`, `xor`, `implies`, short-circuiting where they can) | `eval.go` `evalLogical` | `calc_boolean_operators.sysml` | ✅ Faithful | | Identity (`===`, `!==`), null coalescing (`??`, lazy) and remainder (`%`) evaluated at runtime | `eval.go` `evalIdentity`/`evalNullCoalesce`/`evalArithmetic` | `calc_identity_operators.sysml`, `calc_null_coalesce.sysml`, `calc_modulo_operator.sysml` | ✅ Faithful | -| Value classification evaluated at runtime (`istype`, `hastype`, and `x @ T` with a value subject and an ordinary type, the third `ClassificationTestOperator` of the KerML 1.0 ClassificationExpression grammar beside `hastype` and `istype`, which the reference evaluates as `istype`; SysML v2 8.4.4.2 ClassificationExpression) | `eval.go` `evalTypeClassification`, `valueHasType`, `directValueType`, and `evalOperator` routing `OpAt` there through `classifiesValue` — `x @ T` is a value test when a subject is written and T resolves to a type that is not a metadata definition or metaclass (`semantics.IsMetadataType`), and the metadata test of the next row otherwise — a value's *direct* type is derived from what the value already holds (a scalar constant's value kind, a string's `String`, an object's classifier, a selected variant, an enumeration literal's enumeration, a quantity's numeric value), so no type field was added to `runtime.Value`; `istype` is `semantics.Model.Conforms` of that type to the operand and `hastype` is identity with it, and a sequence or set is classified elementwise | `eval_operator_test.go:TestTypeClassificationOperators` (the reference's 20-case truth table case by case), `:TestTypeClassificationFollowsSelectedVariant`, `conformance/w7d_type_classification.sysml` + `.expected.json` (the same table over the library scalar types), `robustness_test.go:type_classification_unresolved_type`, `:type_classification_undetermined_value_type`, `conformance/value_classification_at.sysml` + `.expected.json` (`n3 @ Integer`, `n3 @ Real`, `n3 @ String`, `seqInt @ Integer`, `car @ Vehicle` beside the same subjects under `hastype` and the metadata forms `belt @ Safety`, `belt @@ SysML::PartUsage`), pilot-exec-diff `w6d:istype-*`, `:hastype-*`, `at-*`, `real-at-integer`, `seq-at-integer`, `car-at-*` | ✅ Faithful — **externally refereed**: all 20 cases agree with the pinned reference, which they did not before (they were `ours-error`; the execution report moved from 31 to 51 agreeing of 94 cases), and the ten `@` cases agree too (65 agreeing of 104): `a : Integer = 3` answers `a @ Integer` and `a @ Real` `true`, `a @ String` `false`, and `car : Car` answers `car @ Vehicle` `true`, where before `a @ Integer` was reported as classifying no element. The referee settles what the direct type is: `nat3 : Natural = 3` answers `hastype Integer` `true`, so it is the value's type and not the declaring feature's, while `car : Car` answers `istype Vehicle` `true` and `hastype Vehicle` `false`. A mixed sequence is `false` and an empty one is `true`. A type operand that does not resolve is `ErrUnresolvedType` and a value whose direct type cannot be determined is `ErrUndeterminedValueType` — reported, never answered `false`. One local rule the referee does not cover: a feature declared `[0..1]` with no value classifies as the empty collection, because the evaluator otherwise reports it as valueless | -| An operator with no runtime evaluation (cast, `all`, bitwise complement, and the two the runtime evaluates from their own expression node) reports why | `eval.go` `unimplementedOperators` (`ErrUnsupportedOperator`) | `eval_operator_test.go:TestUnimplementedOperatorReportsWhy` | ❌ Not implemented (a cast needs a value to carry the type it was cast to, which `runtime.Value` does not model; `all` needs the extent of a type, which the runtime does not enumerate; bitwise complement is declared by no function library the runtime applies; `OpMeta` and `OpIndex` are evaluated from a MetadataAccessExpression and an IndexExpression rather than as operators, so reaching them as operators says that. Classification `istype`/`hastype` and metadata `@`/`@@` **are** evaluated — see the rows around this one) | +| Value classification evaluated at runtime (`istype`, `hastype`, and `x @ T` with a value subject and an ordinary type, the third `ClassificationTestOperator` of the KerML 1.0 ClassificationExpression grammar beside `hastype` and `istype`, which the reference evaluates as `istype`; SysML v2 8.4.4.2 ClassificationExpression) | `eval.go` `evalTypeClassification`, `valueHasType`, `directValueType`, and `evalOperator` routing `OpAt` there through `classifiesValue` — `x @ T` is a value test when a subject is written and T resolves to a type that is not a metadata definition or metaclass (`semantics.IsMetadataType`), and the metadata test of the next row otherwise — a value's *direct* type is derived from what the value already holds (a scalar constant's value kind, a string's `String`, an object's classifier, a selected variant, an enumeration literal's enumeration, a quantity's numeric value), so no type field was added to `runtime.Value`; `istype` is `semantics.Model.Classifies` — the operand's type conforming to the target or classifying it as a composed type does, the same relation a cast asks — and `hastype` is identity with it, and a sequence or set is classified elementwise | `eval_operator_test.go:TestTypeClassificationOperators` (the reference's 20-case truth table case by case), `:TestTypeClassificationFollowsSelectedVariant`, `conformance/w7d_type_classification.sysml` + `.expected.json` (the same table over the library scalar types), `robustness_test.go:type_classification_unresolved_type`, `:type_classification_undetermined_value_type`, `conformance/value_classification_at.sysml` + `.expected.json` (`n3 @ Integer`, `n3 @ Real`, `n3 @ String`, `seqInt @ Integer`, `car @ Vehicle` beside the same subjects under `hastype` and the metadata forms `belt @ Safety`, `belt @@ SysML::PartUsage`), pilot-exec-diff `w6d:istype-*`, `:hastype-*`, `at-*`, `real-at-integer`, `seq-at-integer`, `car-at-*` | ✅ Faithful — **externally refereed**: all 20 cases agree with the pinned reference, which they did not before (they were `ours-error`; the execution report moved from 31 to 51 agreeing of 94 cases), and the ten `@` cases agree too (65 agreeing of 104): `a : Integer = 3` answers `a @ Integer` and `a @ Real` `true`, `a @ String` `false`, and `car : Car` answers `car @ Vehicle` `true`, where before `a @ Integer` was reported as classifying no element. The referee settles what the direct type is: `nat3 : Natural = 3` answers `hastype Integer` `true`, so it is the value's type and not the declaring feature's, while `car : Car` answers `istype Vehicle` `true` and `hastype Vehicle` `false`. A mixed sequence is `false` and an empty one is `true`. A type operand that does not resolve is `ErrUnresolvedType` and a value whose direct type cannot be determined is `ErrUndeterminedValueType` — reported, never answered `false`. One local rule the referee does not cover: a feature declared `[0..1]` with no value classifies as the empty collection, because the evaluator otherwise reports it as valueless | +| Cast expressions evaluated at runtime (`x as T`; KerML 1.1 8.3.4.9 CastExpression, whose result is the values of `x` that `T` classifies, so it selects values and converts none — `ToInteger` and its siblings stay the library functions that convert) | `runtime/cast.go` `evalCast`, `castValue`, `castKeeps`, `castTypes`, `declaredCastTypes`, `castNarrowerKeeps`, `quantityCastKeeps` over `semantics/cast.go` `Model.ClassifiesTypes` and `semantics/exprtype.go` `Model.ScalarLatticeElement` — the types a value is of decide the cast where they are enough, and where `T` is narrower than all of them the value's own content does: a scalar by its magnitude against the ScalarValues lattice (`PrimTypeOfValue`, `PrimConforms`), a quantity by whether its unit is commensurable with the dimension `T` fixes, an object and an enumeration literal by the types they carry, a structured value (an array, a vector, a vector or tensor quantity, a measurement reference, a coordinate frame, a coordinate transformation) by the shape, units and frame reading `write_conformance.go` `valueConforms` already applies to a value written to a feature of that type — so a vector quantity of three axes is not a `ScalarQuantityValue`; `Positive` shares `Natural`'s lattice element, so its own bound is applied on top of it (`Model.PositiveScalar`); the ScalarValues type a scalar is of is read from the library rather than resolved by name in the scope reading it (`scalarLibraryType`), so a declaration wearing one of those names changes no cast's verdict; the type a value's own feature is declared with is a type it is of as well (`declaredCastTypes`), so a custom scalar subtype and a scalar-valued enumeration keep the values declared with them, and a written sequence is cast entry by entry (`castEntries`), each entry judged by the types its own expression is declared with and none by another's, at any nesting depth and whatever number of values an entry holds, while `Base::Anything` — which every declaration implicitly specializes — states nothing and is left out (`semantics.IsAnything`); an expression written as a value is of the evaluation type the model reads it as (`semantics/valuetype.go` `Model.ExprResultType`, so a boolean body is a `BooleanEvaluation`); and a quantity type stating a measurement reference of its own measures every value of its dimension while one narrowing lengths by something else does not (`semantics/dimension.go` `Model.FixesMeasurementReference`); *every* type an operand is declared with counts and not only the first (`semantics/operator_conformance.go` `Model.ExprResultTypes`), so a cast to a feature's second type and a cast of a selection keep their values; a type composed of others classifies as those types do (KerML 1.0 §8.3.3): 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, at any nesting depth and cycle-safely (`semantics/cast.go` `Model.Classifies` over `classifiesComposed`, `semantics/model.go` `UnioningTypes`/`IntersectingTypes`/`DifferencingTypes`, applied alike by the cast, by the static cast check `Model.CastConformance` and by an object's write conformance `runtime/classify.go` `instanceConforms`, so a cast to a composed type neither warns nor is refused by the feature it is written to); a composed target weighs all the types a value is of together (`Model.ClassifiesTypes` over `instanceConforms` and `runtime/eval.go` `valueHasType`), so an object held as a type a difference subtracts is none of its values and `istype` answers so too, whether that difference is the target, a type it specializes or one an intersection of it reaches (`excludes`), while `hastype` stays on identity with one of them; the static check asks whether the two types may share a value at all (`Model.MayShareValues`, which reads a source difference as the values of the first type that are none of the rest), weighing every type the operand is declared with together, so an operand typed by both a difference's first type and one it subtracts is called unrelated, so casting a union-typed operand to one of its members is not called unrelated either, while casting to a type composed of one the operand relates to — a member of a union, a type an intersection intersects, at any nesting depth — is not called unrelated; a composed target that the types a value is of leave open is read through its operands by the cast itself (`castComposedKeeps`), so a bare quantity is kept by the union operand whose measurement reference its unit matches and dropped by one that fixes another, and an operand the value settles nothing about is reported as undecided only where no other operand excludes the value outright, whatever order the operands are written in; and a complex value arithmetic left on the real axis is the real number it holds where an ordering bound is applied (`positiveValue`) | conformance `calc_cast_scalar_values`, `calc_cast_sequence_elementwise`, `calc_cast_enumeration`, `calc_cast_quantity`, `calc_cast_structured`, `calc_cast_instances`, `calc_cast_qualified_target`, `calc_cast_declared_types`, `calc_cast_expression_value`, `calc_cast_complex_real_axis`; `semantics/cast_classification_test.go:TestClassifiesComposedTargets`, `:TestSubtractedTypeExcludesADeclaredValue`, `:TestMayShareValuesOfComposedTypes`; `passes/typecheck_operator_test.go:TestCastConformanceRelatedTypes`, `:TestCastConformanceUnrelatedTypes`; `runtime/eval_operator_test.go:TestClassificationWeighsEveryTypeOfAnObject`; `robustness_test.go:cast_to_an_unresolved_type`, `:cast_undecided_by_the_value`, `:cast_of_a_quantity_to_a_constrained_subtype`, `:difference_typed_feature_holding_a_subtracted_object`; `passes/w8d_metadata_usage_test.go:TestW8DMetadataClassificationValuesAreModelLevelEvaluable`; pilot-exec-diff `integer-as-real`, `integer-as-natural`, `fraction-as-integer`, `whole-as-integer`, `sequence-as-integer`, `car-as-vehicle`, `car-as-car` | ✅ Faithful (a value `T` classifies is answered unchanged, one it does not is the empty sequence, and a sequence is filtered element-wise in order — `4.0 as Integer` is `4.0`, `2.5 as Integer` is `()`, `(1, 2.5, 3) as Integer` is `(1, 3)`. A target no value's type and no value content settles — a user-defined specialization of a scalar or quantity type, such as `Even :> Integer` or `RoomLength :> LengthValue`, whose membership a bare `5` or `5 [m]` does not state — is `ErrUndecidedClassification`, reported rather than answered as the empty sequence; read from a feature declared with that type (`attribute e : Even = 4`, `attribute room : RoomLength = 4 [m]`) the same value is kept, the declaration being what states which of the supertype's values it is. Classifying a value is model-level evaluable, so `x = 1 as Integer` in a metadata body is accepted (`semantics/evaluable.go` `evaluableOperator` reads the named type instead of folding the operand, as it does for `istype`/`hastype`), while an unresolved target or an operand that is not evaluable there is still refused. Judging a scalar by its magnitude is the rule the runtime already applies to a binding — a constant is an instance of the narrowest scalar type that holds it (`semantics.PrimTypeOfValue`), so an `Integer` feature holds `4 / 2` — and it is *narrower* than the direct type the classification row above reads, which is the literal's own type: `n : Integer = 7` answers `n istype Natural` `false` while `n as Natural` keeps `7`, and `r : Real = 4.0` answers `r istype Integer` `false` while `r as Integer` keeps `4.0`. The pinned reference settles the classification reading — `nat3 : Natural = 3` answers `hastype Integer` `true` — and draws no output at all for either cast, so it settles nothing here; the two readings are recorded as they stand rather than one being aligned to the other on no evidence. A scalar's own type is read from the library (`castTypes`, `scalarLibraryType`), so a cast decides the same way in a scope that writes `ScalarValues::Integer` out in full and imports nothing. An empty result is a result: it keeps the unit the source's elements measure in (`sequenceFrom`), so `sum((5 [m], 2 [m]) as DurationValue)` is `0 [m]`; a feature the cast may drop everything from needs multiplicity `[0..1]`, and `return : Integer = r as Integer` reports a multiplicity violation for `r = 2.5` because a lower bound of 1 is unsatisfiable by `()`) | +| An operator with no runtime evaluation (`all`, bitwise complement, and the two the runtime evaluates from their own expression node) reports why | `eval.go` `unimplementedOperators` (`ErrUnsupportedOperator`) | `eval_operator_test.go:TestUnimplementedOperatorReportsWhy` | ❌ Not implemented (`all` needs the extent of a type, which the runtime does not enumerate; bitwise complement is declared by no function library the runtime applies; `OpMeta` and `OpIndex` are evaluated from a MetadataAccessExpression and an IndexExpression rather than as operators, so reaching them as operators says that. Classification `istype`/`hastype`, metadata `@`/`@@` and the `as` cast **are** evaluated — see the rows around this one) | | Metadata classification evaluated at runtime (`p @ Safety`, `p @@ SysML::PartUsage`, in a constraint, a calc body or an `%eval`; SysML v2 7.9.4 metadata, 8.4.4.2 ClassificationExpression) | `eval.go` `EvalContext.evalClassification` — reached by `@@`, by `@` with no subject, and by `x @ T` when T is a metadata definition or metaclass (`semantics.IsMetadataType`), since only an annotation has such a type; `x @ T` with an ordinary type is the value test of the row above — over `semantics/filter.go` `Model.EvalClassification` (the same compiled predicate and `Model.AllSupertypes` conformance an element filter is decided by, so the two paths cannot disagree); `eval.go` `classifiedElement` settles the element the subject denotes — the object being evaluated for an implicit subject or `self`, the element a name names, or an object's classifier, a selected variant or an enumeration literal | `runtime/eval_classification_test.go` (`TestEvalClassificationOverNamedSubjects`, `TestEvalClassificationMetaVersusAnnotation`, `TestEvalClassificationInACalcBody`, `TestEvalClassificationOfTheObjectBeingEvaluated`, `TestEvalClassificationAgreesWithAnElementFilter` — the verdicts of the two paths pinned equal); `conformance/filter_classification_annotation_forms.sysml`, `filter_classification_meta_versus_annotation.sysml`, `filter_classification_implicit_subject.sysml`, `view_exposed_element_classification.sysml`; `robustness_test.go` `classification_outside_the_evaluable_subset`; `semantics/classification_test.go` (the shared predicate itself) | ✅ Faithful (`@T` holds for metadata annotating the subject in every form the parser accepts, inherited conformance included, and for the subject's own metaclass; `@@T` holds for the metaclass alone. A subject that denotes no element, or a metadata type that does not resolve, is `semantics.ErrFilterUnevaluable` — reported, never answered false) | | `lower..upper` is the ordered sequence of integers the library declares it to be (`IntegerFunctions::'..'` returns `Integer[0..*] ordered`, and `SequenceFunctions::subsequence` maps over it), so every sequence operation, index and `for` applies to it unchanged. A descending range is empty, a bound that is not an Integer is a type error, and each element generated costs a step and an element of the budgets, so a range wider than either — including one whose width overflows — is `ErrStepLimitExceeded` or `ErrElementLimitExceeded` rather than an allocation | `runtime/range.go` `evalRange`/`rangeSequence`/`rangeBound`/`builtinIntegerRange` (`ErrTypeMismatch`), registered in `builtins.go` | `calc_integer_range.sysml`, `range_test.go:TestIntegerRange`, `:TestIntegerRangeSequenceOperations`, `:TestIntegerRangeNonIntegerBound`, `:TestIntegerRangeSpendsTheStepBudget`, `:TestIntegerRangeExtremeBounds`, `:TestForOverIntegerRange`, `robustness_test.go:testRangeBoundIsNotAnInteger`, `:testRangeSpendsTheStepBudget` | ✅ Faithful | | Unary operators (not, -, +) | `eval.go` `evalUnary` | `calc_unary_operators.sysml` | ✅ Faithful | @@ -353,7 +354,7 @@ same declarations through `analysis.go` and is unchanged. |--------------|----------------|-----------|--------| | A redefining feature's declared type need not conform to the redefined feature's type: a redefinition is a subsetting (KerML 1.0, formal/2026-03-01, §8.3.3.3.6), so the redefining feature is typed by its own typings *and* the redefined feature's types (§8.3.3.3.4), and neither §8.3.3.3.6 nor SysML v2 §8.3.x declares a type-conformance constraint (the normative redefinition constraints are `validateRedefinitionDirectionConformance`, `validateRedefinitionEndConformance`, `validateRedefinitionFeaturingTypes` and `validateRedefinitionMultiplicityConformance`). The pinned pilot validator is silent on `part :>> p : B` under `part p : A` with `A`, `B` unrelated, and on `attribute :>> q : String` under `q : Integer`, and `ShapeItems.sysml` relies on it (`item :>> faces : Polygon` and `item :>> faces : PlanarSurface` under `faces : StructuredSurface`). OpenSysML still reports the unrelated-type case as `redefinition-type-mismatch`, an extension, because a redefinition typed by two unrelated types is almost always a slip — but as a **warning**, so no conforming model is rejected | `passes/constraint.go` `checkRedefinition` | `passes/constraint_test.go:TestConstraint_RedefinitionTypeMismatch`, `:TestConstraint_RedefinitionConformingTypeStaysSilent`, `:TestConstraint_ShapeItemsRedefinitionsAreNotErrors`; `passes/constraint_unions_test.go` | ⚠️ approximate (advisory warning where the specification and the reference have no rule) | | A usage that redefines an inherited usage (`part derived :> base { part :>> inner { … } }`) specializes what it redefines, so it keeps every nested member the redefined usage declared and overrides only what it restates | `semantics/model.go` `NewModel` (attaches the model to `resolve.Resolver`, so a redefinition target reachable only through inheritance resolves and the redefining usage gains it as a supertype), consumed by `runtime/shape.go` `FeaturesOf` over `Model.MembersOf` | `redefinition_inherited_nested_values.sysml`, `ballandchain_variant_configuration.sysml`, `robustness_test.go:deep_specialization_chain_of_redefinitions`, `conflicting_redefinitions_at_several_levels` | ✅ Faithful (multi-level chains, a redefinition of a redefinition, and conflicting restatements where the innermost wins; the merge is the inherited-member view, not a feature value-level merge in the instantiator) | -| A union's instances are exactly those of its unioning types (KerML §8.3.3), so a type declared `classifier MyWheel unions MyWheel1, MyWheel2` conforms to every type all of its unioning types conform to, and `feature redefines rollsOn : MyWheel` redefining `rollsOn : Wheel` is well-formed. Unioning is not a generalization edge — a union inherits nothing from its members — so it is resolved separately from `DirectSupertypes` | `semantics/model.go` `Model.Conforms` → `unionConforms`, `UnioningTypes` | `passes/constraint_unions_test.go:TestConstraintRedefinitionConformsThroughUnion`, `:TestConstraintRedefinitionUnionMemberDoesNotConform`, `:TestConstraintRedefinitionUnionCycleTerminates` | ✅ Faithful (conformance only: a union's *members* are not computed, and `intersects`/`differences` are not read) | +| A union's instances are exactly those of its unioning types (KerML §8.3.3), so a type declared `classifier MyWheel unions MyWheel1, MyWheel2` conforms to every type all of its unioning types conform to, and `feature redefines rollsOn : MyWheel` redefining `rollsOn : Wheel` is well-formed. Unioning is not a generalization edge — a union inherits nothing from its members — so it is resolved separately from `DirectSupertypes` | `semantics/model.go` `Model.Conforms` → `unionConforms`, `UnioningTypes` | `passes/constraint_unions_test.go:TestConstraintRedefinitionConformsThroughUnion`, `:TestConstraintRedefinitionUnionMemberDoesNotConform`, `:TestConstraintRedefinitionUnionCycleTerminates` | ✅ Faithful (conformance only: a union's *members* are not computed. `intersects` and `differences` are read for classification rather than conformance — see the cast row — so a type is not made to conform through them) | | The type a redefinition must inherit the redefined feature from is the feature's *featuring* type where it declares one (`member feature CC1_snapshots :>> Occurrences::Occurrence::snapshots featured by CC1;` is featured by `CC1`, not by the feature it is written inside — KerML §7.4.5, §8.3.4.3), and a bare `feature` owned by a package has no featuring type, so nothing can inherit it and the rule does not apply; a target that is not an inherited member may still be *accessible* through the featuring context — a context conforming to the target's own featuring context, or one that redefines a common feature whose own contexts conform (the variable-feature snapshot encoding; the pilot checks accessibility, `FeatureUtil.canAccess`, not inherited membership) | `passes/constraint.go` `checkRedefinition` over `featuringOwners` (the declared `featured by` targets, else the lexical owner), `isInheritedMember`, `isPackageLevelFeature`, and the accessibility fallback `redefinedAccessible`/`featuringContexts`/`featuredWithin`/`featuringContextConforms` | `passes/constraint_test.go:TestConstraint_RedefinitionUsesFeaturingType`, `:TestConstraint_PackageLevelRedefinitionHasNoInheritedOwner`, `:TestConstraint_PackageLevelUnfeaturedRedefinitionExemptsNoInheritedRule`, `passes/f100_redefinition_featuring_test.go` (a `featured by` context inheriting the target, the snapshot-style pair, and the unrelated-context/no-common-target/unrelated-typing negatives) | ⚠️ Approximate (`TimeVaryingCarDriver.kerml:93` is accepted, an unrelated `featured by` context still rejected; the accessibility walk approximates the pilot's `canAccess` — only a *declared* `featured by` is read, the featuring a nested feature implies is not computed. The package-level exemption is decided by the absence of a `featured by` relationship, so a package-level feature that declares one is still checked) | | A redefinition removes the redefined feature from the type owning the redefining one, so none of its names — primary, short, or an alias binding it — is visible there, transitively along a redefinition chain; masking is keyed by element, so an inherited namesake nobody redefines keeps its name, a redefinition taking the redefined name masks nothing, and a member the type declares itself is never masked (KerML §7.4.7, §8.3.3.3) | `semantics/masking.go` `RedefinedFeatures`, `redefinitionMask`, `buildMask`, `InheritanceMasked`; `semantics/members.go` `MembersOf` / `MembersOfDeclaring` (the redefinition-anchor view, KerML §8.3.3.3.6) / `MembersOfIncludingRedefined` (the unmasked view the runtime shape needs so a redefinition shares its target's feature value), consumed by `model/scope_names.go` | `semantics/w8b_masking_test.go`, `model/scope_names_test.go` (redefinition-anchor cases), pilot-xpect `scope` class `extra-names` 31 → 3 on the merged tree | ⚠️ Approximate (masking governs enumeration: `x.a` still *resolves* through `resolve.lookupMember`'s unmasked `LookupContributedMember` fallback, and under multiple inheritance a qualified path binds the masked namesake; visibility, 8A's filter, composes after the masked view in the same enumeration) | | A subsetting feature's declared type need not conform to the subsetted feature's type, and no diagnostic reports one that does not: a feature's types are derived from its own typings *and* the types of the features it subsets (KerML 1.0, formal/2026-03-01, §8.3.3.3.4; the 1.1 draft the pinned 2026-07 pilot implements states the same), so `feature f : B subsets g;` under `feature g : A;` makes `f` typed by both `A` and `B` — subsetting "adds additional feature types" (KerML §7.3.4.4) and the co-domain rule (§8.3.3.3.10) holds by construction. The OMG training corpus relies on this (`Model Library Example.sysml`: `occurrence causes : Cause[*] nonunique :> situations;` with `situations : Situation[*]`, `Cause` unrelated to `Situation`), and the pinned pilot validator reports nothing for the unrelated-type case. Neither §8.3.3.3.10 nor §8.3.3.3.8 declares a type-conformance constraint (the normative subsetting constraints are `validateSubsettingConstantConformance`, `validateSubsettingFeaturingTypes` and `validateSubsettingUniquenessConformance`; multiplicity conformance is a warning). Redefinition, a kind of subsetting, derives a feature's types the same way, so `redefinition-type-mismatch` is an OpenSysML extension reported as an advisory **warning**, never an error (see the redefinition row below) | `passes/constraint.go` `checkRedefinition` (no subsetting counterpart, by design) | `passes/constraint_test.go:TestConstraintSubsettingUnrelatedTypeOK`, `:TestConstraintSubsettingOccurrenceUnrelatedTypeOK`, `:TestConstraintSubsettingConformingTypeOK`; training-corpus gate over `Model Library Example.sysml` | ✅ Faithful (no rule, matching the specification and the reference) | @@ -1035,8 +1036,10 @@ the flat sequence of its elements: inherits as a same-named one does (`subsetting.go` `sharedRedefinitionName`, `declarationValues`; `TestRenamedRedefinitionBodyGovernsAnInheritedValue`), while that example's component frames, whose `mRefs` default to - `(that.that as SpatialItem).coordinateFrame.mRefs`, stay the `as` cast's typed - error — the runtime does not evaluate `as` (`eval.go` `ast.OpAs`). The value + `(that.that as SpatialItem).coordinateFrame.mRefs`, stay a typed error: the + `as` cast is evaluated now (`cast.go` `evalCast`), but `that.that` is not — an + object features no `that`, so the chain reports itself before the cast sees a + value. The value carries the declaration, its type, the `dimensions` the type fixes (`'3dCoordinateFrame'` states `3`; a scalar reference `()`, one axis), one `ValMeasurementRef` per axis read from `mRefs` (the flattened size of `dimensions` gates the count: a @@ -1257,7 +1260,7 @@ reports itself by name rather than answering: | `MatrixFunctions` | The vendored Kernel Function Library declares no such package — only `docs/` mention it — so there is nothing to dispatch. Not implemented rather than invented. | | `ComplexFunctions::ToString`/`ToComplex`, `BaseFunctions::ToString` of a Complex | No string notation for a Complex value is defined; inventing a rendering would make `ToComplex(ToString(x))` a value nothing else in the library agrees on. | | `BaseFunctions::'['` | Declared abstract, and the operator notation `a[i, j]` is the quantity notation `num [unit]` to the parser and the evaluator (`evalIndexExpr`): over an operand whose bracket names no unit the error (`ErrNotAQuantity`, `notAQuantityError`) says so, and when the operand is declared an Array, a vector or a feature of more than one value (`declaredCollection`, from the declaration alone — the operand is not evaluated to diagnose it) points at `a#(i, j)`, which `CollectionFunctions::'array#'` and `BaseFunctions::'#'` evaluate. Reading `a[i, j]` as indexing by the operand's static type would be a checker rule as well as a runtime one, and is not made here. | -| `BaseFunctions::all`, `as`, `meta`, `istype`, `hastype`, `'@'`, `'@@'`; `ControlFunctions::'.'` | The operator notations `x istype T`, `x @ M`, `x.f` **are** evaluated, from their own expression nodes (`istype`/`hastype`/`@`/`@@` take a *type*, which the function form would have to receive as a value); `as` needs the type a value was cast to, which `runtime.Value` does not carry; `all` needs the extent of a type, which the runtime does not enumerate. The function forms report themselves rather than pretend. | +| `BaseFunctions::all`, `as`, `meta`, `istype`, `hastype`, `'@'`, `'@@'`; `ControlFunctions::'.'` | The operator notations `x istype T`, `x as T`, `x @ M`, `x.f` **are** evaluated, from their own expression nodes (`as`/`istype`/`hastype`/`@`/`@@` take a *type*, which the function form would have to receive as a value); `all` needs the extent of a type, which the runtime does not enumerate. The function forms report themselves rather than pretend. | | `DataFunctions::'~'`, `ScalarFunctions::'~'` | Declared abstract and specialized by no concrete library function, so the complement denotes no operation on any value type — reported as the `~` operator is. | | `QuantityCalculations::ConvertQuantity` to or from a measurement scale that states neither a `CoordinateFramePlacement` nor a `quantityValueMapping` — `Time::UTC`, every `OrdinalScale`, `CyclicRatioScale`, `LogarithmicScale` in the vendored library | The scale is a value (`ValCoordinateFrame`, *Structured values* above) and a quantity on it reads, but the library gives its points no relation to any other reference, so a conversion has nothing to compute by; the reason names the scale and the missing transformation or mapping. `SI::'°C_abs'`, placed on `K`, converts. | | `VectorCalculations::transform` over a `CoordinateTransformation` that is none of `CoordinateFramePlacement`, `TranslationRotationSequence`, `AffineTransformationMatrix3d`, `NullTransformation` | Those four are the shapes the library documents; a user-defined subtype states no origin, basis, steps or matrix the runtime could apply, so the reason names the declaration and the four shapes. | diff --git a/internal/core/passes/typecheck_operator_test.go b/internal/core/passes/typecheck_operator_test.go index 62ec37b83..7caff3857 100644 --- a/internal/core/passes/typecheck_operator_test.go +++ b/internal/core/passes/typecheck_operator_test.go @@ -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 @@ -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") @@ -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;`) @@ -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 diff --git a/internal/core/passes/w8d_metadata_usage_test.go b/internal/core/passes/w8d_metadata_usage_test.go index 1127d1e8c..77a1f01ea 100644 --- a/internal/core/passes/w8d_metadata_usage_test.go +++ b/internal/core/passes/w8d_metadata_usage_test.go @@ -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) +} diff --git a/internal/core/runtime/cast.go b/internal/core/runtime/cast.go new file mode 100644 index 000000000..22b0c9076 --- /dev/null +++ b/internal/core/runtime/cast.go @@ -0,0 +1,374 @@ +package runtime + +import ( + "fmt" + + "github.com/Open-MBEE/OpenSysML/internal/core/ast" + "github.com/Open-MBEE/OpenSysML/internal/core/semantics" + "github.com/Open-MBEE/OpenSysML/internal/core/symbols" +) + +// evaluationTypeFQN types a deferred expression: the functions computing a result. +const evaluationTypeFQN = "Performances::Evaluation" + +// evalCast evaluates `x as T`: a CastExpression's result is the values of x that +// the type T classifies, so it selects values and never converts one (KerML 1.1 +// §8.3.4.9). Converting between types is what the library functions do. +func (ec *EvalContext) evalCast(n *ast.OperatorExpr) (Value, error) { + if len(n.Operands) != 1 || n.TypeRef == nil { + return Value{}, fmt.Errorf("%w: '%s' requires one value and one type", + ErrTypeMismatch, n.Operator) + } + target, ok := ec.resolveClassificationType(n.TypeRef) + if !ok { + return Value{}, fmt.Errorf("%w: %s", ErrUnresolvedType, + qualifiedNameToString(n.TypeRef)) + } + // A written sequence is cast entry by entry, each judged by its own types. + if _, ok := n.Operands[0].(*ast.SequenceExpr); ok { + kept, sources, err := ec.castEntries(n.Operands[0], target) + if err != nil { + return Value{}, err + } + return ec.sequenceFrom(kept, sources...) + } + value, err := ec.Eval(n.Operands[0]) + if err != nil { + return Value{}, err + } + return ec.castValue(value, target, ec.declaredCastTypes(n.Operands[0])) +} + +// castEntries casts one entry of a written sequence, answering the values target +// keeps of it and the values it holds, whose unit an empty result keeps. A KerML +// sequence is flat, so a nested one contributes its own entries. +func (ec *EvalContext) castEntries( + entry ast.Node, target *symbols.Symbol, +) (kept, sources []Value, err error) { + if seq, ok := entry.(*ast.SequenceExpr); ok { + for _, element := range seq.Elements { + elementKept, elementSources, err := ec.castEntries(element, target) + if err != nil { + return nil, nil, err + } + kept = append(kept, elementKept...) + sources = append(sources, elementSources...) + } + return kept, sources, nil + } + value, err := ec.Eval(entry) + if err != nil { + return nil, nil, err + } + out, err := ec.castValue(value, target, ec.declaredCastTypes(entry)) + if err != nil { + return nil, nil, err + } + return elementsOf(out), []Value{value}, nil +} + +// declaredCastTypes names every type the cast's operand is declared with, which +// classifies its values where their own content does not state their type. +func (ec *EvalContext) declaredCastTypes(operand ast.Node) []*symbols.Symbol { + // An enumeration literal is of its enumeration however its value is written. + if sym, ok := ec.ctx.resolver.ResolveTarget(ec.scope, operand); ok && sym != nil { + if canonical, aliased := ec.ctx.resolver.ResolveAliasTarget(sym); aliased { + sym = canonical + } + if enum := semantics.EnumerationOwning(sym); enum != nil { + return []*symbols.Symbol{enum} + } + } + var declared []*symbols.Symbol + for _, typ := range ec.ctx.model.ExprResultTypes(ec.scope, operand) { + // A feature typed Anything states nothing about the values it holds. + if typ != nil && !semantics.IsAnything(typ) { + declared = append(declared, typ) + } + } + return declared +} + +// castValue keeps the values of value that target classifies: element-wise and in +// order for a collection, the value itself or the empty sequence for one value. +func (ec *EvalContext) castValue( + value Value, target *symbols.Symbol, declared []*symbols.Symbol, +) (Value, error) { + switch value.Kind { + case ValNull, ValInvalid: + return sequenceOf(nil), nil + case ValSequence, ValSet: + elements := elementsOf(value) + kept := make([]Value, 0, len(elements)) + for _, element := range elements { + keep, err := ec.castKeeps(element, target, declared) + if err != nil { + return Value{}, err + } + if keep { + kept = append(kept, element) + } + } + if value.Kind == ValSet { + set := NewSet() + for _, element := range kept { + set.Add(element) + } + if err := ec.ctx.chargeElements(int64(set.Size())); err != nil { + return Value{}, err + } + return NewSetValue(set), nil + } + return ec.sequenceFrom(kept, value) + } + keep, err := ec.castKeeps(value, target, declared) + if err != nil { + return Value{}, err + } + if !keep { + return ec.sequenceFrom(nil, value) + } + return value, nil +} + +// castKeeps reports whether target classifies one value. The types the value is +// of decide it wherever they are enough; where target is narrower than all of +// them, the value's own content does (castNarrowerKeeps). +func (ec *EvalContext) castKeeps( + value Value, target *symbols.Symbol, declared []*symbols.Symbol, +) (bool, error) { + return ec.castKeepsReading(value, target, declared, nil) +} + +// castKeepsReading answers castKeeps; reading holds the composed targets being +// read, so a composition naming itself does not recur. +func (ec *EvalContext) castKeepsReading( + value Value, target *symbols.Symbol, declared []*symbols.Symbol, reading map[*symbols.Symbol]bool, +) (bool, error) { + types, err := ec.castTypes(value) + if err != nil && len(declared) == 0 { + return false, err + } + known := append(append([]*symbols.Symbol{}, declared...), types...) + switch ec.ctx.model.ClassifiesTypes(known, target) { + case semantics.ClassifiesAll: + return true, nil + case semantics.ClassifiesNone: + return false, nil + } + if keep, composed, err := ec.castComposedKeeps(value, target, declared, reading); composed { + return keep, err + } + return ec.castNarrowerKeeps(value, target) +} + +// castComposedKeeps decides a value by a composed target's operands — any of a +// union, all of an intersection, the first of a difference and none of the rest — +// and reports second whether the target is composed at all. +func (ec *EvalContext) castComposedKeeps( + value Value, target *symbols.Symbol, declared []*symbols.Symbol, reading map[*symbols.Symbol]bool, +) (bool, bool, error) { + unions := ec.ctx.model.UnioningTypes(target) + intersects := ec.ctx.model.IntersectingTypes(target) + differences := ec.ctx.model.DifferencingTypes(target) + if len(unions)+len(intersects)+len(differences) == 0 || reading[target] { + return false, false, nil + } + if reading == nil { + reading = make(map[*symbols.Symbol]bool) + } + reading[target] = true + defer delete(reading, target) + + keeps := func(operand *symbols.Symbol) (bool, error) { + return ec.castKeepsReading(value, operand, declared, reading) + } + // An operand no type of the value settles leaves the cast undecided, but only + // where no other operand excludes the value outright. + var undecided error + if len(unions) > 0 { + kept, err := anyKeeps(unions, keeps) + switch { + case err != nil: + undecided = err + case !kept: + return false, true, nil + } + } + for _, operand := range intersects { + kept, err := keeps(operand) + switch { + case err != nil: + undecided = err + case !kept: + return false, true, nil + } + } + for i, operand := range differences { + kept, err := keeps(operand) + switch { + case err != nil: + undecided = err + case kept != (i == 0): + return false, true, nil + } + } + if undecided != nil { + return false, true, undecided + } + return true, true, nil +} + +// anyKeeps reports whether any operand keeps the value, reporting an operand's +// error only when no other one keeps it. +func anyKeeps(operands []*symbols.Symbol, keeps func(*symbols.Symbol) (bool, error)) (bool, error) { + var undecided error + for _, operand := range operands { + kept, err := keeps(operand) + if err != nil { + undecided = err + continue + } + if kept { + return true, nil + } + } + return false, undecided +} + +// castTypes names the types a value is of for a cast: a quantity value is the +// quantity type it is, whose dimension castNarrowerKeeps then judges, and every +// other value is of the types a classification reads it as. +func (ec *EvalContext) castTypes(value Value) ([]*symbols.Symbol, error) { + // A deferred expression is of the evaluation type the model reads it as, in + // the scope it closes over. + if value.Kind == ValExpr { + if typ := ec.ctx.model.ExprResultType(value.exprEnv(ec).scope, value.Expr()); typ != nil { + return []*symbols.Symbol{typ}, nil + } + evaluation, err := ec.ctx.loadedLibraryType(evaluationTypeFQN) + if err != nil { + return nil, err + } + return []*symbols.Symbol{evaluation}, nil + } + if value.Kind == ValQuantity { + quantity, err := ec.ctx.loadedLibraryType(scalarQuantityTypeFQN) + if err != nil { + return nil, err + } + return []*symbols.Symbol{quantity}, nil + } + // A scalar is of its ScalarValues type whatever a declaration of that name in + // the reading scope says, so the library symbol answers ahead of a lookup. + if scalar := ec.scalarLibraryType(value); scalar != nil { + return []*symbols.Symbol{scalar}, nil + } + return ec.ctx.directValueTypes(ec.scope, value) +} + +// scalarLibraryType is the ScalarValues type a literal value is of, independent of +// what the reading scope imports or declares under that type's name. +func (ec *EvalContext) scalarLibraryType(value Value) *symbols.Symbol { + var prim semantics.PrimType + switch value.Kind { + case ValString: + prim = semantics.PrimString + case ValComplex: + prim = semantics.PrimComplex + case ValConst: + switch value.Const.Kind { + case semantics.ValInt: + prim = semantics.PrimInteger + case semantics.ValReal: + prim = semantics.PrimReal + case semantics.ValBool: + prim = semantics.PrimBoolean + default: + return nil + } + default: + return nil + } + return ec.ctx.model.ScalarSymbol(prim) +} + +// positiveValue reports whether a numeric value is greater than zero; a complex +// value off the real axis is not on the ordering Positive bounds. +func positiveValue(value Value) bool { + if value.Kind == ValComplex { + return imag(value.Complex()) == 0 && real(value.Complex()) > 0 + } + switch value.Const.Kind { + case semantics.ValInt: + return value.Const.Int > 0 + case semantics.ValReal: + return value.Const.Real > 0 + } + return false +} + +// castNarrowerKeeps decides a target narrower than every type the value is of, +// which only the value itself settles: a scalar by its own magnitude against the +// ScalarValues lattice, a quantity by the dimension the target fixes, an object +// and an enumeration literal by the types they carry — which already said no. +func (ec *EvalContext) castNarrowerKeeps(value Value, target *symbols.Symbol) (bool, error) { + switch value.Kind { + case ValConst, ValComplex, ValString: + prim, ok := ec.ctx.model.ScalarLatticeElement(target) + got := valuePrimType(&value) + if !ok || got == semantics.PrimUnknown { + return false, ec.undecidedCast(value, target) + } + if !semantics.PrimConforms(got, prim) { + return false, nil + } + // Positive shares Natural's lattice element but not its zero. + return !ec.ctx.model.PositiveScalar(target) || positiveValue(value), nil + case ValQuantity: + return ec.quantityCastKeeps(value, target) + case ValArray, ValVector, ValVectorQuantity, ValTensorQuantity, + ValMeasurementRef, ValCoordinateFrame, ValCoordinateTransformation: + // A structured value's own shape, units and frame decide it, as they do + // for a value written to a feature of the target type. + keep, _, err := ec.ctx.valueConforms(ec.scope, &value, target, admitWritten) + return keep, err + case ValEnumLiteral, ValVariant: + return false, nil + } + if _, isObject := value.Object(); isObject { + // An object is classified by the types it was declared and classified by; + // a specialization of those does not classify it. + return false, nil + } + return false, ec.undecidedCast(value, target) +} + +// quantityCastKeeps judges a quantity against a narrower target by dimension: an +// incommensurable target measures none of its values, and a target stating its own +// measurement reference measures every value of that dimension. Anything else a +// magnitude and a unit do not state, so it is undecided. +func (ec *EvalContext) quantityCastKeeps(value Value, target *symbols.Symbol) (bool, error) { + want, ok := ec.ctx.model.DimensionOfType(target) + if !ok || value.Quantity() == nil { + return false, ec.undecidedCast(value, target) + } + got, ok := ec.ctx.model.DimensionOfUnit(value.Quantity().Unit.Term) + if !ok { + return false, ec.undecidedCast(value, target) + } + if !want.Term.Commensurable(got.Term) { + return false, nil + } + if !ec.ctx.model.FixesMeasurementReference(target) { + return false, ec.undecidedCast(value, target) + } + return true, nil +} + +// undecidedCast reports a cast whose verdict the value does not settle, so the +// cast fails rather than dropping a value that may well be one of the target's. +func (ec *EvalContext) undecidedCast(value Value, target *symbols.Symbol) error { + return fmt.Errorf("%w: whether %s (%s) is a value of %s is not stated by the value", + ErrUndecidedClassification, FormatValue(value), describeValue(value), symbolText(target)) +} diff --git a/internal/core/runtime/classify.go b/internal/core/runtime/classify.go index 23653f355..8f0952f99 100644 --- a/internal/core/runtime/classify.go +++ b/internal/core/runtime/classify.go @@ -13,15 +13,8 @@ import ( // instanceConforms reports whether an object is an instance of typ by its declaration or by // a feature it was held as a value of (KerML 1.0 §7.3.4.1: a feature's values are instances of its types). func (ctx *Context) instanceConforms(inst *Instance, typ *symbols.Symbol) bool { - if ctx.model.Conforms(inst.Type, typ) { - return true - } - for _, c := range inst.classifiers { - if ctx.model.Conforms(c, typ) { - return true - } - } - return false + // All of the object's types at once: a difference reads the types it subtracts too. + return ctx.model.ClassifiesTypes(inst.types(), typ) == semantics.ClassifiesAll } // isDirectTypeOf reports whether typ is already a direct type of an object: one it was diff --git a/internal/core/runtime/errors.go b/internal/core/runtime/errors.go index 1b73ba84a..acff6309a 100644 --- a/internal/core/runtime/errors.go +++ b/internal/core/runtime/errors.go @@ -106,6 +106,11 @@ var ( // direct runtime type to compare. ErrUndeterminedValueType = errors.New("value type cannot be determined") + // ErrUndecidedClassification is returned when a cast reaches a value whose + // classification by a type narrower than the value's own the value does not + // settle, so the cast fails rather than dropping a value that may be one. + ErrUndecidedClassification = errors.New("classification of a value cannot be decided") + // ErrCalcNoReturn is returned when a calc body runs to its end without // returning: it computed no result, which is not the same as a null one. ErrCalcNoReturn = errors.New("calculation returned no value") diff --git a/internal/core/runtime/eval.go b/internal/core/runtime/eval.go index c2911178d..e6133437e 100644 --- a/internal/core/runtime/eval.go +++ b/internal/core/runtime/eval.go @@ -1261,7 +1261,6 @@ func (ctx *Context) enumerationSummary(enum *symbols.Symbol) string { // says what each would need, so reaching one reports why rather than "unsupported". var unimplementedOperators = map[ast.OperatorKind]string{ ast.OpBitNot: "bitwise complement is declared by no function library the runtime applies", - ast.OpAs: "a cast needs the runtime type of a value, which values do not carry yet", ast.OpMeta: "metadata access is evaluated from a MetadataAccessExpression, not this operator", ast.OpAll: "'all' needs the extent of a type, which the runtime does not enumerate", ast.OpIndex: "indexing is evaluated from an IndexExpression, not this operator", @@ -1305,6 +1304,8 @@ func (ec *EvalContext) evalOperator(n *ast.OperatorExpr) (Value, error) { return ec.evalClassification(n) case ast.OpHasType, ast.OpIsType: return ec.evalTypeClassification(n) + case ast.OpAs: + return ec.evalCast(n) default: if why, ok := unimplementedOperators[n.Operator]; ok { return Value{}, fmt.Errorf("%w: '%s': %s", ErrUnsupportedOperator, n.Operator, why) @@ -1394,12 +1395,12 @@ func (ec *EvalContext) valueHasType(value Value, target *symbols.Symbol, exact b if err != nil { return false, err } - for _, typ := range direct { - if (exact && typ == target) || (!exact && ec.ctx.model.Conforms(typ, target)) { - return true, nil - } + // istype reads a composed target as a cast does, weighing the value's types + // together; hastype stays on identity with one of them. + if !exact { + return ec.ctx.model.ClassifiesTypes(direct, target) == semantics.ClassifiesAll, nil } - return false, nil + return slices.Contains(direct, target), nil } // directValueTypes names the types a value is of, resolved in the scope reading it: diff --git a/internal/core/runtime/eval_operator_test.go b/internal/core/runtime/eval_operator_test.go index d7673fb49..7e7460c09 100644 --- a/internal/core/runtime/eval_operator_test.go +++ b/internal/core/runtime/eval_operator_test.go @@ -13,18 +13,18 @@ import ( // TestUnimplementedOperatorReportsWhy requires an operator the runtime does not // evaluate to say what it would need, rather than failing as "unsupported". func TestUnimplementedOperatorReportsWhy(t *testing.T) { - const src = `calc def classify { in n : Integer; return : Boolean = n as Integer; }` + const src = `calc def complement { in n : Integer; return : Integer = ~n; }` model, resolver, root := parseAndBuildModel(t, src) ctx := NewContext(model, resolver, 1000) - classify := resolveSymbol(t, root, "classify") + complement := resolveSymbol(t, root, "complement") - _, err := ctx.InvokeCalc(classify, []Value{constInt(1)}, root) + _, err := ctx.InvokeCalc(complement, []Value{constInt(1)}, root) if !errors.Is(err, ErrUnsupportedOperator) { t.Fatalf("InvokeCalc: got %v, want ErrUnsupportedOperator", err) } - if !strings.Contains(err.Error(), "runtime type") { - t.Fatalf("InvokeCalc: %v does not say what classification would need", err) + if !strings.Contains(err.Error(), "function library") { + t.Fatalf("InvokeCalc: %v does not say what the complement would need", err) } } @@ -139,6 +139,51 @@ func TestTypeClassificationFollowsSelectedVariant(t *testing.T) { } } +// TestClassificationWeighsEveryTypeOfAnObject requires a difference to read the +// classifiers an object gained beside its own type: a Car held as an ElectricCar +// is a value of Electric, so it is none of Vehicle minus Electric. +func TestClassificationWeighsEveryTypeOfAnObject(t *testing.T) { + const src = ` + part def Vehicle; + part def Car :> Vehicle; + part def Electric; + part def ElectricCar :> Car, Electric; + part def CombustionVehicle differences Vehicle, Electric; + part sedan : Car; + part def Shop { + part retrofit : ElectricCar = sedan; + } + part shop : Shop; + attribute burner = shop.retrofit istype CombustionVehicle; + attribute vehicle = shop.retrofit istype Vehicle; + attribute burnerCast = (shop.retrofit as CombustionVehicle) == (); + ` + model, resolver, root := parseAndBuildModel(t, src) + ctx := NewContext(model, resolver, 10000) + for _, tt := range []struct { + name string + want bool + }{ + {name: "burner", want: false}, + {name: "vehicle", want: true}, + {name: "burnerCast", want: true}, + } { + t.Run(tt.name, func(t *testing.T) { + sym := resolveSymbol(t, root, tt.name) + value, err := ctx.Eval(sym.Decl.(*ast.Usage).Value) + if err != nil { + t.Fatalf("Eval: %v", err) + } + if value.Kind != ValConst || value.Const.Kind != semantics.ValBool { + t.Fatalf("value = %v, want Boolean", value) + } + if value.Const.Bool != tt.want { + t.Errorf("%s = %v, want %v", tt.name, value.Const.Bool, tt.want) + } + }) + } +} + // strValue is a String runtime value, the representation of a string literal. func strValue(s string) Value { return NewStringValue(s) } @@ -289,3 +334,27 @@ package test { } } } + +// TestComposedCastUndecidedWhenNoOperandExcludes: an intersection or difference +// no operand settles is still the typed undecidable-classification error. +func TestComposedCastUndecidedWhenNoOperandExcludes(t *testing.T) { + const src = ` + attribute def Integer; + attribute def Even :> Integer; + attribute def EvenInteger intersects Even, Integer; + attribute def OddInteger differences Integer, Even; + attribute intersected = 5 as EvenInteger; + attribute subtracted = 5 as OddInteger; + ` + model, resolver, root := parseAndBuildModel(t, src) + ctx := NewContext(model, resolver, 10000) + for _, name := range []string{"intersected", "subtracted"} { + t.Run(name, func(t *testing.T) { + sym := resolveSymbol(t, root, name) + if _, err := ctx.Eval(sym.Decl.(*ast.Usage).Value); !errors.Is( + err, ErrUndecidedClassification) { + t.Fatalf("expected ErrUndecidedClassification, got: %v", err) + } + }) + } +} diff --git a/internal/core/runtime/robustness_test.go b/internal/core/runtime/robustness_test.go index 684a380a4..0d556282e 100644 --- a/internal/core/runtime/robustness_test.go +++ b/internal/core/runtime/robustness_test.go @@ -238,6 +238,10 @@ func TestRuntimeRobustness(t *testing.T) { t.Run("routed_send_receiver_name_mismatch_deadlock", testRoutedSendReceiverNameMismatchDeadlock) t.Run("type_classification_unresolved_type", testTypeClassificationUnresolvedType) t.Run("type_classification_undetermined_value_type", testTypeClassificationUndeterminedValueType) + t.Run("cast_to_an_unresolved_type", testCastToAnUnresolvedType) + t.Run("cast_undecided_by_the_value", testCastUndecidedByTheValue) + t.Run("cast_of_a_quantity_to_a_constrained_subtype", testCastOfAQuantityToAConstrainedSubtype) + t.Run("difference_typed_feature_holding_a_subtracted_object", testDifferenceTypedFeatureHoldingASubtractedObject) t.Run("send_addressed_through_several_occurrences", testSendAddressedThroughSeveralOccurrences) t.Run("send_addressed_to_an_object_that_cannot_be_built", testSendAddressedToAnObjectThatCannotBeBuilt) t.Run("send_addressed_to_a_part_no_sibling_takes", testSendAddressedToAPartNoSiblingTakes) @@ -4321,6 +4325,93 @@ func testTypeClassificationUndeterminedValueType(t *testing.T) { } } +func testCastToAnUnresolvedType(t *testing.T) { + model, resolver, root := parseAndBuildModel(t, `package P { + item def Integer; + calc narrow { return : Integer = 1 as MissingType; } + }`) + pkg := resolveSymbol(t, root, "P") + calc := resolveSymbol(t, pkg.Scope, "narrow") + _, err := NewContext(model, resolver, 1000).InvokeCalc(calc, nil, pkg.Scope) + if err == nil { + t.Fatal("expected a cast to an unresolved type to fail") + } + if !errors.Is(err, ErrUnresolvedType) { + t.Fatalf("expected ErrUnresolvedType, got: %v", err) + } + if !strings.Contains(err.Error(), "MissingType") { + t.Errorf("error = %v, want unresolved type name", err) + } +} + +// testCastUndecidedByTheValue: a target narrower than the value's own type that +// the value does not settle — 5 states nothing about being an Even — fails +// rather than dropping a value that may well be one of the target's. +func testCastUndecidedByTheValue(t *testing.T) { + model, resolver, root := parseAndBuildModel(t, `package P { + attribute def Integer; + attribute def Even :> Integer; + calc narrow { return : Even = 5 as Even; } + }`) + pkg := resolveSymbol(t, root, "P") + calc := resolveSymbol(t, pkg.Scope, "narrow") + _, err := NewContext(model, resolver, 1000).InvokeCalc(calc, nil, pkg.Scope) + if err == nil { + t.Fatal("expected an undecidable cast to fail") + } + if !errors.Is(err, ErrUndecidedClassification) { + t.Fatalf("expected ErrUndecidedClassification, got: %v", err) + } + if !strings.Contains(err.Error(), "Even") { + t.Errorf("error = %v, want the target type named", err) + } +} + +// testDifferenceTypedFeatureHoldingASubtractedObject: a feature typed by a +// difference refuses an object one of the subtracted types classifies, whether +// the object was declared by it or classified by it since. +func testDifferenceTypedFeatureHoldingASubtractedObject(t *testing.T) { + model, resolver, root := parseAndBuildModel(t, ` + part def Vehicle; + part def Car :> Vehicle; + part def Electric; + part def ElectricCar :> Car, Electric; + part def CombustionVehicle differences Vehicle, Electric; + part sedan : Car; + part def Shop { part retrofit : ElectricCar = sedan; } + part shop : Shop; + part def Depot { part burner : CombustionVehicle = shop.retrofit; } + part depot : Depot; + attribute held = depot.burner istype Vehicle; + `) + sym := resolveSymbol(t, root, "held") + _, err := NewContext(model, resolver, 10000).Eval(sym.Decl.(*ast.Usage).Value) + if !errors.Is(err, ErrTypeMismatch) { + t.Fatalf("expected ErrTypeMismatch, got: %v", err) + } + if !strings.Contains(err.Error(), "CombustionVehicle") { + t.Errorf("error = %v, want the feature's type named", err) + } +} + +// testCastOfAQuantityToAConstrainedSubtype: a quantity subtype inheriting its +// measurement reference narrows lengths by something a magnitude and a unit do +// not state, so a bare length is undecided rather than kept by its dimension. +func testCastOfAQuantityToAConstrainedSubtype(t *testing.T) { + err := calcErrorWithLibraries(t, ` + package test { + private import SI::*; + attribute def RoomLength :> ISQBase::LengthValue; + calc narrow { return : RoomLength = 5 [m] as RoomLength; } + }`, "narrow", nil, 1000) + if !errors.Is(err, ErrUndecidedClassification) { + t.Fatalf("expected ErrUndecidedClassification, got: %v", err) + } + if !strings.Contains(err.Error(), "RoomLength") { + t.Errorf("error = %v, want the target type named", err) + } +} + // testSendAddressedToAnUnreachableTarget: a target reaching no port of an object // the sender can address is reported where it was written rather than delivered // to whatever else carries the last segment's name. diff --git a/internal/core/runtime/testdata/conformance/calc_cast_complex_real_axis.expected.json b/internal/core/runtime/testdata/conformance/calc_cast_complex_real_axis.expected.json new file mode 100644 index 000000000..269b7f023 --- /dev/null +++ b/internal/core/runtime/testdata/conformance/calc_cast_complex_real_axis.expected.json @@ -0,0 +1,10 @@ +{ + "libraries": true, + "type": "calcUsage", + "evaluate": "test::c", + "outputs": { + "onAxisAsPositive": {"type": "Complex", "value": 4.0, "im": 0.0}, + "negativeOnAxisAsPositive": {"type": "Sequence", "elements": []}, + "offAxisAsPositive": {"type": "Sequence", "elements": []} + } +} diff --git a/internal/core/runtime/testdata/conformance/calc_cast_complex_real_axis.sysml b/internal/core/runtime/testdata/conformance/calc_cast_complex_real_axis.sysml new file mode 100644 index 000000000..4d689c0da --- /dev/null +++ b/internal/core/runtime/testdata/conformance/calc_cast_complex_real_axis.sysml @@ -0,0 +1,15 @@ +// A complex value that arithmetic left on the real axis is the real number it +// holds, so the ordering scalar types classify it by that number; one off the +// axis is on no ordering bound (KerML 1.1 §8.3.4.9). +package test { + private import ScalarValues::*; + private import ComplexFunctions::*; + + calc def ComplexCasts { + out onAxisAsPositive : Positive[0..1] = (rect(3.0, 1.0) + rect(1.0, -1.0)) as Positive; + out negativeOnAxisAsPositive : Positive[0..1] = (rect(-3.0, 1.0) + rect(-1.0, -1.0)) as Positive; + out offAxisAsPositive : Positive[0..1] = (rect(3.0, 1.0) + rect(1.0, 1.0)) as Positive; + } + + calc c : ComplexCasts; +} diff --git a/internal/core/runtime/testdata/conformance/calc_cast_composed_operands.expected.json b/internal/core/runtime/testdata/conformance/calc_cast_composed_operands.expected.json new file mode 100644 index 000000000..7a73c9c43 --- /dev/null +++ b/internal/core/runtime/testdata/conformance/calc_cast_composed_operands.expected.json @@ -0,0 +1,11 @@ +{ + "libraries": true, + "type": "calcUsage", + "evaluate": "test::c", + "outputs": { + "fractionalUndecidedFirst": {"type": "Sequence", "elements": []}, + "fractionalDecidedFirst": {"type": "Sequence", "elements": []}, + "integralSubtractedLast": {"type": "Sequence", "elements": []}, + "integralSubtractedFirst": {"type": "Sequence", "elements": []} + } +} diff --git a/internal/core/runtime/testdata/conformance/calc_cast_composed_operands.sysml b/internal/core/runtime/testdata/conformance/calc_cast_composed_operands.sysml new file mode 100644 index 000000000..48d85656a --- /dev/null +++ b/internal/core/runtime/testdata/conformance/calc_cast_composed_operands.sysml @@ -0,0 +1,21 @@ +// A composed target keeps a value only where all of its operands do, so an +// operand nothing states about does not hide one the value's own content +// excludes it by, whichever is written first (KerML 1.1 §8.3.4.9). +package test { + private import ScalarValues::*; + + attribute def Even :> Integer; + attribute def EvenInteger intersects Even, Integer; + attribute def IntegerEven intersects Integer, Even; + attribute def NonIntegralLast differences Real, Even, Integer; + attribute def NonIntegralFirst differences Real, Integer, Even; + + calc def ComposedCasts { + out fractionalUndecidedFirst : EvenInteger[0..*] = 5.5 as EvenInteger; + out fractionalDecidedFirst : IntegerEven[0..*] = 5.5 as IntegerEven; + out integralSubtractedLast : NonIntegralLast[0..*] = 5.0 as NonIntegralLast; + out integralSubtractedFirst : NonIntegralFirst[0..*] = 5.0 as NonIntegralFirst; + } + + calc c : ComposedCasts; +} diff --git a/internal/core/runtime/testdata/conformance/calc_cast_declared_types.expected.json b/internal/core/runtime/testdata/conformance/calc_cast_declared_types.expected.json new file mode 100644 index 000000000..53e4bd2ad --- /dev/null +++ b/internal/core/runtime/testdata/conformance/calc_cast_declared_types.expected.json @@ -0,0 +1,38 @@ +{ + "libraries": true, + "type": "calcUsage", + "evaluate": "test::c", + "outputs": { + "asDeclaredSubtype": {"type": "Integer", "value": 4}, + "asScalarSupertype": {"type": "Integer", "value": 4}, + "asOwnEnumeration": {"type": "Real", "value": 4.0}, + "literalAsEnumeration": {"type": "Real", "value": 4.0}, + "asEnumerationSupertype": {"type": "Real", "value": 4.0}, + "asOtherScalar": {"type": "Sequence", "elements": []}, + "asSecondDeclaredType": {"type": "Integer", "value": 6}, + "selectedAsSubtype": {"type": "Sequence", "elements": [ + {"type": "Integer", "value": 4}, + {"type": "Integer", "value": 6} + ]}, + "literalsAsEnumeration": {"type": "Sequence", "elements": [ + {"type": "Real", "value": 4.0}, + {"type": "Real", "value": 3.0} + ]}, + "mixedAsEnumeration": {"type": "Sequence", "elements": [ + {"type": "Real", "value": 4.0} + ]}, + "declaredWithLiteral": {"type": "Sequence", "elements": [ + {"type": "Integer", "value": 4} + ]}, + "nestedAsEnumeration": {"type": "Sequence", "elements": [ + {"type": "Real", "value": 4.0}, + {"type": "Real", "value": 3.0}, + {"type": "Real", "value": 4.0} + ]}, + "multiValuedEntry": {"type": "Sequence", "elements": [ + {"type": "Integer", "value": 2}, + {"type": "Integer", "value": 4}, + {"type": "Integer", "value": 6} + ]} + } +} diff --git a/internal/core/runtime/testdata/conformance/calc_cast_declared_types.sysml b/internal/core/runtime/testdata/conformance/calc_cast_declared_types.sysml new file mode 100644 index 000000000..ab38c0b19 --- /dev/null +++ b/internal/core/runtime/testdata/conformance/calc_cast_declared_types.sysml @@ -0,0 +1,39 @@ +// A value is kept by the type its feature is declared with as well as by the +// types its own content states: a custom scalar subtype keeps the values of the +// feature declared with it, and a scalar-valued enumeration keeps its literals +// (KerML 1.1 §8.3.4.9). +package test { + private import ScalarValues::*; + + attribute def Even :> Integer; + attribute def Counted :> Integer; + + enum def GradePoints :> Real { + enum a = 4.0; + enum b = 3.0; + } + + attribute e : Even = 4; + attribute g : GradePoints = GradePoints::a; + attribute both : Even, Counted = 6; + attribute evens : Even[0..*] = (2, 4, 6); + + calc def DeclaredCasts { + out asDeclaredSubtype : Even[0..1] = e as Even; + out asScalarSupertype : Integer[0..1] = e as Integer; + out asOwnEnumeration : GradePoints[0..1] = g as GradePoints; + out literalAsEnumeration : GradePoints[0..1] = GradePoints::a as GradePoints; + out asEnumerationSupertype : Real[0..1] = g as Real; + out asOtherScalar : Boolean[0..1] = e as Boolean; + out asSecondDeclaredType : Counted[0..1] = both as Counted; + out selectedAsSubtype : Even[0..*] = (evens.?{in x; x > 2}) as Even; + out literalsAsEnumeration : GradePoints[0..*] = (GradePoints::a, GradePoints::b) as GradePoints; + out mixedAsEnumeration : GradePoints[0..*] = (GradePoints::a, true) as GradePoints; + out declaredWithLiteral : Even[0..*] = (e, false) as Even; + out nestedAsEnumeration : GradePoints[0..*] = + ((GradePoints::a, GradePoints::b), GradePoints::a) as GradePoints; + out multiValuedEntry : Even[0..*] = (evens, false) as Even; + } + + calc c : DeclaredCasts; +} diff --git a/internal/core/runtime/testdata/conformance/calc_cast_enumeration.expected.json b/internal/core/runtime/testdata/conformance/calc_cast_enumeration.expected.json new file mode 100644 index 000000000..1c1038f43 --- /dev/null +++ b/internal/core/runtime/testdata/conformance/calc_cast_enumeration.expected.json @@ -0,0 +1,11 @@ +{ + "libraries": true, + "type": "calcUsage", + "evaluate": "test::c", + "outputs": { + "asOwnEnumeration": {"type": "EnumLiteral", "value": "Signal::on"}, + "asSupertype": {"type": "EnumLiteral", "value": "Signal::on"}, + "asDataValue": {"type": "EnumLiteral", "value": "Signal::on"}, + "asSibling": {"type": "Sequence", "elements": []} + } +} diff --git a/internal/core/runtime/testdata/conformance/calc_cast_enumeration.sysml b/internal/core/runtime/testdata/conformance/calc_cast_enumeration.sysml new file mode 100644 index 000000000..40ef66f27 --- /dev/null +++ b/internal/core/runtime/testdata/conformance/calc_cast_enumeration.sysml @@ -0,0 +1,26 @@ +// An enumeration value is kept by the enumeration that declares it and by every +// type that enumeration specializes, and dropped by a sibling enumeration whose +// values it is not one of (KerML 1.1 §8.3.4.9). +package test { + private import ScalarValues::*; + + attribute def Mode; + + enum def Signal :> Mode { + on; + off; + } + + enum def Other :> Mode { + idle; + } + + calc def EnumerationCasts { + out asOwnEnumeration : Signal[0..1] = Signal::on as Signal; + out asSupertype : Mode[0..1] = Signal::on as Mode; + out asDataValue : Base::DataValue[0..1] = Signal::on as Base::DataValue; + out asSibling : Mode[0..1] = Signal::on as Other; + } + + calc c : EnumerationCasts; +} diff --git a/internal/core/runtime/testdata/conformance/calc_cast_expression_value.expected.json b/internal/core/runtime/testdata/conformance/calc_cast_expression_value.expected.json new file mode 100644 index 000000000..fb5ff10b3 --- /dev/null +++ b/internal/core/runtime/testdata/conformance/calc_cast_expression_value.expected.json @@ -0,0 +1,13 @@ +{ + "libraries": true, + "type": "calcUsage", + "evaluate": "test::c", + "outputs": { + "selectedByKeptBody": {"type": "Sequence", "elements": [ + {"type": "Integer", "value": 2}, + {"type": "Integer", "value": 3} + ]}, + "keptAsEvaluation": {"type": "Integer", "value": 1}, + "droppedByScalarType": {"type": "Integer", "value": 0} + } +} diff --git a/internal/core/runtime/testdata/conformance/calc_cast_expression_value.sysml b/internal/core/runtime/testdata/conformance/calc_cast_expression_value.sysml new file mode 100644 index 000000000..9da25d4f3 --- /dev/null +++ b/internal/core/runtime/testdata/conformance/calc_cast_expression_value.sysml @@ -0,0 +1,20 @@ +// An expression written as a value is kept by the evaluation type it is read as +// — a boolean body by BooleanEvaluation — and dropped by a type whose values it +// is not one of, so the cast selects a body still applicable afterwards +// (KerML 1.1 §8.3.4.9). +package test { + private import ScalarValues::*; + private import ControlFunctions::*; + private import SequenceFunctions::*; + + calc def ExpressionCasts { + out selectedByKeptBody : Integer[0..*] = + select((1, 2, 3), { in v; v > 1 } as Performances::BooleanEvaluation); + out keptAsEvaluation : Integer = + size(({ in v; v > 1 }) as Performances::Evaluation); + out droppedByScalarType : Integer = + size(({ in v; v > 1 }) as Integer); + } + + calc c : ExpressionCasts; +} diff --git a/internal/core/runtime/testdata/conformance/calc_cast_instances.expected.json b/internal/core/runtime/testdata/conformance/calc_cast_instances.expected.json new file mode 100644 index 000000000..d90cc9222 --- /dev/null +++ b/internal/core/runtime/testdata/conformance/calc_cast_instances.expected.json @@ -0,0 +1,26 @@ +{ + "type": "calcUsage", + "evaluate": "test::c", + "outputs": { + "carAsCar": {"type": "Instance"}, + "carAsVehicle": {"type": "Instance"}, + "carAsTruck": {"type": "Sequence", "elements": []}, + "carsOfFleet": {"type": "Sequence", "elements": [ + {"type": "Instance"} + ]}, + "vehiclesOfFleet": {"type": "Sequence", "elements": [ + {"type": "Instance"}, + {"type": "Instance"} + ]}, + "carAsUnion": {"type": "Instance"}, + "truckAsUnion": {"type": "Instance"}, + "carAsNestedUnion": {"type": "Instance"}, + "unionHeldAsCar": {"type": "Instance"}, + "plugInAsIntersection": {"type": "Instance"}, + "carAsIntersection": {"type": "Sequence", "elements": []}, + "carAsDifference": {"type": "Instance"}, + "plugInAsDifference": {"type": "Sequence", "elements": []}, + "hybridAsDifference": {"type": "Sequence", "elements": []}, + "hybridAsIntersection": {"type": "Instance"} + } +} diff --git a/internal/core/runtime/testdata/conformance/calc_cast_instances.sysml b/internal/core/runtime/testdata/conformance/calc_cast_instances.sysml new file mode 100644 index 000000000..67b964968 --- /dev/null +++ b/internal/core/runtime/testdata/conformance/calc_cast_instances.sysml @@ -0,0 +1,42 @@ +// An object is kept by every classifier it is an instance of, its type's +// generalizations included, and dropped by a specialization it is not an +// instance of (KerML 1.1 §8.3.4.9). A union's instances are those of the types +// it unions (KerML 1.0 §8.3.3), so it keeps each of them however deeply nested; +// an intersection's are the objects of every type it intersects and a +// difference's those of the first type that are none of the rest. +package test { + part def Vehicle; + part def Car :> Vehicle; + part def Truck :> Vehicle; + part def Wheeled unions Car, Truck; + part def Registered unions Wheeled; + part def Electric; + part def ElectricCar :> Car, Electric; + part def ElectricVehicle intersects Vehicle, Electric; + part def CombustionVehicle differences Vehicle, Electric; + + part car : Car; + part truck : Truck; + part plugIn : ElectricCar; + part hybrid : Car, Electric; + + calc def InstanceCasts { + out carAsCar : Car[0..1] = car as Car; + out carAsVehicle : Vehicle[0..1] = car as Vehicle; + out carAsTruck : Truck[0..1] = car as Truck; + out carsOfFleet : Car[0..*] = (car, truck) as Car; + out vehiclesOfFleet : Vehicle[0..*] = (car, truck) as Vehicle; + out carAsUnion : Wheeled[0..1] = car as Wheeled; + out truckAsUnion : Wheeled[0..1] = truck as Wheeled; + out carAsNestedUnion : Registered[0..1] = car as Registered; + out unionHeldAsCar : Car[0..1] = carAsUnion as Car; + out plugInAsIntersection : ElectricVehicle[0..1] = plugIn as ElectricVehicle; + out carAsIntersection : ElectricVehicle[0..1] = car as ElectricVehicle; + out carAsDifference : CombustionVehicle[0..1] = car as CombustionVehicle; + out plugInAsDifference : CombustionVehicle[0..1] = plugIn as CombustionVehicle; + out hybridAsDifference : CombustionVehicle[0..1] = hybrid as CombustionVehicle; + out hybridAsIntersection : ElectricVehicle[0..1] = hybrid as ElectricVehicle; + } + + calc c : InstanceCasts; +} diff --git a/internal/core/runtime/testdata/conformance/calc_cast_qualified_target.expected.json b/internal/core/runtime/testdata/conformance/calc_cast_qualified_target.expected.json new file mode 100644 index 000000000..b026decb3 --- /dev/null +++ b/internal/core/runtime/testdata/conformance/calc_cast_qualified_target.expected.json @@ -0,0 +1,13 @@ +{ + "libraries": true, + "type": "calcUsage", + "evaluate": "test::c", + "outputs": { + "wholeAsInteger": {"type": "Real", "value": 4.0}, + "fractionAsInteger": {"type": "Sequence", "elements": []}, + "fractionAsReal": {"type": "Real", "value": 2.5}, + "stringAsString": {"type": "String", "value": "kept"}, + "shadowedInteger": {"type": "Integer", "value": 3}, + "localInteger": {"type": "Sequence", "elements": []} + } +} diff --git a/internal/core/runtime/testdata/conformance/calc_cast_qualified_target.sysml b/internal/core/runtime/testdata/conformance/calc_cast_qualified_target.sysml new file mode 100644 index 000000000..b7954aa83 --- /dev/null +++ b/internal/core/runtime/testdata/conformance/calc_cast_qualified_target.sysml @@ -0,0 +1,21 @@ +// A cast reads the value's own type from the library, so `x as T` decides the +// same way in a scope that writes every ScalarValues name out in full and +// imports none of them (KerML 1.1 §8.3.4.9). +package test { + // Declarations wearing the ScalarValues names, which classify no scalar. + attribute def Integer; + attribute def String; + + calc def QualifiedCasts { + in whole : ScalarValues::Real = 4.0; + in fraction : ScalarValues::Real = 2.5; + out wholeAsInteger : ScalarValues::Integer[0..1] = whole as ScalarValues::Integer; + out fractionAsInteger : ScalarValues::Integer[0..1] = fraction as ScalarValues::Integer; + out fractionAsReal : ScalarValues::Real[0..1] = fraction as ScalarValues::Real; + out stringAsString : ScalarValues::String[0..1] = "kept" as ScalarValues::String; + out shadowedInteger : ScalarValues::Integer[0..1] = 3 as ScalarValues::Integer; + out localInteger : Integer[0..1] = 3 as Integer; + } + + calc c : QualifiedCasts; +} diff --git a/internal/core/runtime/testdata/conformance/calc_cast_quantity.expected.json b/internal/core/runtime/testdata/conformance/calc_cast_quantity.expected.json new file mode 100644 index 000000000..b96603fdb --- /dev/null +++ b/internal/core/runtime/testdata/conformance/calc_cast_quantity.expected.json @@ -0,0 +1,21 @@ +{ + "libraries": true, + "type": "calcUsage", + "evaluate": "test::c", + "outputs": { + "asLength": {"type": "Quantity", "value": 5, "unit": "m"}, + "asScalarQuantity": {"type": "Quantity", "value": 5, "unit": "m"}, + "asDuration": {"type": "Sequence", "elements": []}, + "lengthsOfMixed": {"type": "Sequence", "elements": [ + {"type": "Quantity", "value": 5, "unit": "m"}, + {"type": "Quantity", "value": 2, "unit": "m"} + ]}, + "sumOfNoDurations": {"type": "Quantity", "value": 0, "unit": "m"}, + "declaredAsSubtype": {"type": "Quantity", "value": 4, "unit": "m"}, + "declaredAsBaseQuantity": {"type": "Quantity", "value": 4, "unit": "m"}, + "declaredAsDuration": {"type": "Sequence", "elements": []}, + "bareAsUnion": {"type": "Quantity", "value": 5, "unit": "m"}, + "bareSecondsAsUnion": {"type": "Quantity", "value": 3, "unit": "s"}, + "bareMassAsUnion": {"type": "Sequence", "elements": []} + } +} diff --git a/internal/core/runtime/testdata/conformance/calc_cast_quantity.sysml b/internal/core/runtime/testdata/conformance/calc_cast_quantity.sysml new file mode 100644 index 000000000..b2f616a46 --- /dev/null +++ b/internal/core/runtime/testdata/conformance/calc_cast_quantity.sysml @@ -0,0 +1,37 @@ +// A quantity is kept by the quantity value type whose measurement reference its +// unit is one of, and by that type's supertypes; a length is not a duration +// (KerML 1.1 §8.3.4.9). +package test { + private import ScalarValues::*; + private import SI::*; + private import ISQ::*; + private import QuantityCalculations::*; + + // A subtype narrowing lengths by something a magnitude and a unit do not state. + attribute def RoomLength :> ISQBase::LengthValue; + + // A union of quantity types states no measurement reference of its own. + attribute def LengthOrDuration unions ISQBase::LengthValue, ISQBase::DurationValue; + + attribute room : RoomLength = 4 [m]; + + calc def QuantityCasts { + in length : ISQBase::LengthValue = 5 [m]; + out asLength : ISQBase::LengthValue[0..1] = length as ISQBase::LengthValue; + out asScalarQuantity : Quantities::ScalarQuantityValue[0..1] = length as Quantities::ScalarQuantityValue; + out asDuration : ISQBase::DurationValue[0..1] = length as ISQBase::DurationValue; + out lengthsOfMixed : ISQBase::LengthValue[0..*] = (5 [m], 3 [s], 2 [m]) as ISQBase::LengthValue; + // Nothing kept still measures in the source's unit, so an aggregate of it does. + out sumOfNoDurations = sum((5 [m], 2 [m]) as ISQBase::DurationValue); + // The declaring type says which of its dimension's values these are. + out declaredAsSubtype : RoomLength[0..1] = room as RoomLength; + out declaredAsBaseQuantity : ISQBase::LengthValue[0..1] = room as ISQBase::LengthValue; + out declaredAsDuration : ISQBase::DurationValue[0..1] = room as ISQBase::DurationValue; + // A union is read through its operands, each of which fixes a reference. + out bareAsUnion : LengthOrDuration[0..1] = 5 [m] as LengthOrDuration; + out bareSecondsAsUnion : LengthOrDuration[0..1] = 3 [s] as LengthOrDuration; + out bareMassAsUnion : LengthOrDuration[0..1] = 2 [kg] as LengthOrDuration; + } + + calc c : QuantityCasts; +} diff --git a/internal/core/runtime/testdata/conformance/calc_cast_scalar_values.expected.json b/internal/core/runtime/testdata/conformance/calc_cast_scalar_values.expected.json new file mode 100644 index 000000000..8d683f31b --- /dev/null +++ b/internal/core/runtime/testdata/conformance/calc_cast_scalar_values.expected.json @@ -0,0 +1,25 @@ +{ + "libraries": true, + "type": "calcUsage", + "evaluate": "test::c", + "outputs": { + "wholeAsInteger": {"type": "Real", "value": 4.0}, + "fractionAsInteger": {"type": "Sequence", "elements": []}, + "fractionAsRational": {"type": "Real", "value": 2.5}, + "integerAsReal": {"type": "Integer", "value": 7}, + "integerAsNatural": {"type": "Integer", "value": 7}, + "negativeAsNatural": {"type": "Sequence", "elements": []}, + "zeroAsNatural": {"type": "Integer", "value": 0}, + "oneAsPositive": {"type": "Integer", "value": 1}, + "zeroAsPositive": {"type": "Sequence", "elements": []}, + "negativeAsPositive": {"type": "Sequence", "elements": []}, + "positivesOfMixed": {"type": "Sequence", "elements": [ + {"type": "Integer", "value": 2}, + {"type": "Integer", "value": 3} + ]}, + "integerAsNumber": {"type": "Integer", "value": 7}, + "realAsScalarValue": {"type": "Real", "value": 2.5}, + "booleanAsBoolean": {"type": "Boolean", "value": true}, + "stringAsString": {"type": "String", "value": "kept"} + } +} diff --git a/internal/core/runtime/testdata/conformance/calc_cast_scalar_values.sysml b/internal/core/runtime/testdata/conformance/calc_cast_scalar_values.sysml new file mode 100644 index 000000000..10826becf --- /dev/null +++ b/internal/core/runtime/testdata/conformance/calc_cast_scalar_values.sysml @@ -0,0 +1,28 @@ +// `x as T` selects, it does not convert (KerML 1.1 §8.3.4.9): a scalar is kept +// where T classifies the value it is — the ScalarValues types are nested value +// sets, so a whole Real is an Integer and 2.5 is not — and is dropped otherwise. +package test { + private import ScalarValues::*; + + calc def ScalarCasts { + in whole : Real = 4.0; + in fraction : Real = 2.5; + out wholeAsInteger : Integer[0..1] = whole as Integer; + out fractionAsInteger : Integer[0..1] = fraction as Integer; + out fractionAsRational : Rational[0..1] = fraction as Rational; + out integerAsReal : Real[0..1] = 7 as Real; + out integerAsNatural : Natural[0..1] = 7 as Natural; + out negativeAsNatural : Natural[0..1] = -7 as Natural; + out zeroAsNatural : Natural[0..1] = 0 as Natural; + out oneAsPositive : Positive[0..1] = 1 as Positive; + out zeroAsPositive : Positive[0..1] = 0 as Positive; + out negativeAsPositive : Positive[0..1] = -1 as Positive; + out positivesOfMixed : Positive[0..*] = (2, 0, -1, 3) as Positive; + out integerAsNumber : Number[0..1] = 7 as Number; + out realAsScalarValue : ScalarValue[0..1] = fraction as ScalarValue; + out booleanAsBoolean : Boolean[0..1] = true as Boolean; + out stringAsString : String[0..1] = "kept" as String; + } + + calc c : ScalarCasts; +} diff --git a/internal/core/runtime/testdata/conformance/calc_cast_sequence_elementwise.expected.json b/internal/core/runtime/testdata/conformance/calc_cast_sequence_elementwise.expected.json new file mode 100644 index 000000000..1583d7f75 --- /dev/null +++ b/internal/core/runtime/testdata/conformance/calc_cast_sequence_elementwise.expected.json @@ -0,0 +1,24 @@ +{ + "libraries": true, + "type": "calcUsage", + "evaluate": "test::c", + "outputs": { + "integersOfMixed": {"type": "Sequence", "elements": [ + {"type": "Integer", "value": 1}, + {"type": "Integer", "value": 3}, + {"type": "Real", "value": 4.0} + ]}, + "rationalsOfMixed": {"type": "Sequence", "elements": [ + {"type": "Integer", "value": 1}, + {"type": "Real", "value": 2.5}, + {"type": "Integer", "value": 3}, + {"type": "Real", "value": 4.0} + ]}, + "naturalsOfSigned": {"type": "Sequence", "elements": [ + {"type": "Integer", "value": 2}, + {"type": "Integer", "value": 4} + ]}, + "noneConform": {"type": "Sequence", "elements": []}, + "emptyStaysEmpty": {"type": "Sequence", "elements": []} + } +} diff --git a/internal/core/runtime/testdata/conformance/calc_cast_sequence_elementwise.sysml b/internal/core/runtime/testdata/conformance/calc_cast_sequence_elementwise.sysml new file mode 100644 index 000000000..2aedfc883 --- /dev/null +++ b/internal/core/runtime/testdata/conformance/calc_cast_sequence_elementwise.sysml @@ -0,0 +1,16 @@ +// Casting a sequence is element-wise: the elements the target classifies are +// kept in their original order, and a sequence none of whose elements it +// classifies casts to the empty sequence (KerML 1.1 §8.3.4.9). +package test { + private import ScalarValues::*; + + calc def SequenceCasts { + out integersOfMixed : Integer[0..*] = (1, 2.5, 3, 4.0) as Integer; + out rationalsOfMixed : Rational[0..*] = (1, 2.5, 3, 4.0) as Rational; + out naturalsOfSigned : Natural[0..*] = (-1, 2, -3, 4) as Natural; + out noneConform : Natural[0..*] = (-1, -2) as Natural; + out emptyStaysEmpty : Integer[0..*] = () as Integer; + } + + calc c : SequenceCasts; +} diff --git a/internal/core/runtime/testdata/conformance/calc_cast_structured.expected.json b/internal/core/runtime/testdata/conformance/calc_cast_structured.expected.json new file mode 100644 index 000000000..4fa4094a0 --- /dev/null +++ b/internal/core/runtime/testdata/conformance/calc_cast_structured.expected.json @@ -0,0 +1,19 @@ +{ + "libraries": true, + "type": "calcUsage", + "evaluate": "test::c", + "outputs": { + "asVectorQuantity": {"type": "VectorQuantity", "elements": [ + {"type": "Quantity", "value": 2.0, "unit": "m"}, + {"type": "Quantity", "value": 4.0, "unit": "m"}, + {"type": "Quantity", "value": 6.0, "unit": "m"} + ]}, + "asTensorQuantity": {"type": "VectorQuantity", "elements": [ + {"type": "Quantity", "value": 2.0, "unit": "m"}, + {"type": "Quantity", "value": 4.0, "unit": "m"}, + {"type": "Quantity", "value": 6.0, "unit": "m"} + ]}, + "asScalarQuantity": {"type": "Sequence", "elements": []}, + "asNumber": {"type": "Sequence", "elements": []} + } +} diff --git a/internal/core/runtime/testdata/conformance/calc_cast_structured.sysml b/internal/core/runtime/testdata/conformance/calc_cast_structured.sysml new file mode 100644 index 000000000..446cb9eec --- /dev/null +++ b/internal/core/runtime/testdata/conformance/calc_cast_structured.sysml @@ -0,0 +1,20 @@ +// A structured value is kept by a target its own shape, units and frame fit — +// the same reading a write to a feature of that type applies: a vector quantity +// of three axes is no scalar quantity (KerML 1.1 §8.3.4.9). +package test { + private import ScalarValues::*; + private import VectorValues::*; + private import Quantities::*; + private import SI::*; + + attribute d : VectorQuantityValue = 2 [m] * VectorFunctions::VectorOf((1.0, 2.0, 3.0)); + + calc def StructuredCasts { + out asVectorQuantity : VectorQuantityValue[0..*] = d as VectorQuantityValue; + out asTensorQuantity : TensorQuantityValue[0..*] = d as TensorQuantityValue; + out asScalarQuantity : ScalarQuantityValue[0..*] = d as ScalarQuantityValue; + out asNumber : NumericalValue[0..*] = d as NumericalValue; + } + + calc c : StructuredCasts; +} diff --git a/internal/core/runtime/testdata/conformance/w7d_type_classification.expected.json b/internal/core/runtime/testdata/conformance/w7d_type_classification.expected.json index 307871504..fb0aae07c 100644 --- a/internal/core/runtime/testdata/conformance/w7d_type_classification.expected.json +++ b/internal/core/runtime/testdata/conformance/w7d_type_classification.expected.json @@ -24,6 +24,10 @@ {"type": "Boolean", "value": true}, {"type": "Boolean", "value": true}, {"type": "Boolean", "value": true}, + {"type": "Boolean", "value": false}, + {"type": "Boolean", "value": true}, + {"type": "Boolean", "value": true}, + {"type": "Boolean", "value": false}, {"type": "Boolean", "value": false} ] } diff --git a/internal/core/runtime/testdata/conformance/w7d_type_classification.sysml b/internal/core/runtime/testdata/conformance/w7d_type_classification.sysml index 6c3af6172..327211e07 100644 --- a/internal/core/runtime/testdata/conformance/w7d_type_classification.sysml +++ b/internal/core/runtime/testdata/conformance/w7d_type_classification.sysml @@ -3,6 +3,9 @@ private import ScalarValues::*; package W7D { part def Vehicle; part def Car :> Vehicle; + part def Truck :> Vehicle; + part def Wheeled unions Car, Truck; + part def Registered unions Wheeled; part def Sys; attribute n7 : Integer = 7; @@ -35,7 +38,11 @@ package W7D { W7D::none istype Integer, W7D::car istype Car, W7D::car istype Vehicle, - W7D::sys istype Car + W7D::sys istype Car, + W7D::car istype Wheeled, + W7D::car istype Registered, + W7D::car hastype Wheeled, + W7D::sys istype Wheeled ); } } diff --git a/internal/core/semantics/cast.go b/internal/core/semantics/cast.go new file mode 100644 index 000000000..322dd6072 --- /dev/null +++ b/internal/core/semantics/cast.go @@ -0,0 +1,254 @@ +package semantics + +import ( + "github.com/Open-MBEE/OpenSysML/internal/core/ast" + "github.com/Open-MBEE/OpenSysML/internal/core/symbols" +) + +// TypeClassification is how far the types a value is of settle whether a target +// type classifies it, the question a CastExpression asks (KerML 1.1 §8.3.4.9). +type TypeClassification uint8 + +const ( + // ClassifiesNone is a target disjoint from every type the value is of, so no + // value of those types is one of the target's. + ClassifiesNone TypeClassification = iota + // ClassifiesAll is a type of the value specializing the target, so every + // value of that type is one of the target's. + ClassifiesAll + // ClassifiesSome is a target specializing a type of the value: some values of + // that type are the target's and the value itself decides which. + ClassifiesSome +) + +// ClassifiesTypes reports how target classifies a value known to be of types. +func (m *Model) ClassifiesTypes(types []*symbols.Symbol, target *symbols.Symbol) TypeClassification { + return m.classifiesTypes(types, target, nil) +} + +// Classifies reports whether every value of typ is one of target's. +func (m *Model) Classifies(target, typ *symbols.Symbol) bool { + return m.ClassifiesTypes([]*symbols.Symbol{typ}, target) == ClassifiesAll +} + +// classifiesTypes answers ClassifiesTypes; composing holds the composed targets +// being read, so a composition naming itself does not recur. +func (m *Model) classifiesTypes( + types []*symbols.Symbol, target *symbols.Symbol, composing map[*symbols.Symbol]bool, +) TypeClassification { + if m == nil || target == nil { + return ClassifiesNone + } + verdict := ClassifiesNone + for _, typ := range types { + if typ == nil { + continue + } + if m.Conforms(typ, target) { + // A type subtracted somewhere in the target still excludes the value. + if m.excludes(types, target, composing) { + return ClassifiesNone + } + return ClassifiesAll + } + if m.Conforms(target, typ) { + verdict = ClassifiesSome + } + } + composed, ok := m.classifiesComposed(types, target, composing) + if !ok || composed == ClassifiesNone { + return verdict + } + if composed == ClassifiesAll || verdict == ClassifiesNone { + return composed + } + return verdict +} + +// classifiesComposed reads a target composed of other types — a union, an +// intersection or a difference (KerML 1.0 §8.3.3) — as those types classify: the +// values of a union are those of any of its types, of an intersection those of +// every type, of a difference those of the first that are none of the rest. +func (m *Model) classifiesComposed( + types []*symbols.Symbol, target *symbols.Symbol, composing map[*symbols.Symbol]bool, +) (TypeClassification, bool) { + unions, intersects, differences := m.UnioningTypes(target), + m.IntersectingTypes(target), m.DifferencingTypes(target) + if len(unions)+len(intersects)+len(differences) == 0 || composing[target] { + return ClassifiesNone, false + } + if composing == nil { + composing = make(map[*symbols.Symbol]bool) + } + composing[target] = true + defer delete(composing, target) + + // Every composition of a type constrains its values, so all of them must hold. + constraints := make([]TypeClassification, 0, 3) + if len(unions) > 0 { + constraints = append(constraints, classifiesAny(m.classifiesEach(types, unions, composing))) + } + if len(intersects) > 0 { + constraints = append(constraints, classifiesAll(m.classifiesEach(types, intersects, composing))) + } + if len(differences) > 0 { + constraints = append(constraints, classifiesExcept(m.classifiesEach(types, differences, composing))) + } + return classifiesAll(constraints), true +} + +// excludes reports whether target or a type it is one of the values of subtracts a +// type the value is of: a difference subtracts it, an intersection or a +// specialization is of a type that does, a union is of nothing else. reading holds +// the targets being read so a cycle terminates. +func (m *Model) excludes( + types []*symbols.Symbol, target *symbols.Symbol, reading map[*symbols.Symbol]bool, +) bool { + if m == nil || target == nil || reading[target] { + return false + } + if reading == nil { + reading = make(map[*symbols.Symbol]bool) + } + reading[target] = true + defer delete(reading, target) + + differences := m.DifferencingTypes(target) + for _, subtracted := range differences[min(1, len(differences)):] { + if m.classifiesTypes(types, subtracted, reading) == ClassifiesAll { + return true + } + } + for _, group := range [][]*symbols.Symbol{m.DirectSupertypes(target), m.IntersectingTypes(target)} { + for _, super := range group { + if m.excludes(types, super, reading) { + return true + } + } + } + unions := m.UnioningTypes(target) + for _, operand := range unions { + if !m.excludes(types, operand, reading) { + return false + } + } + return len(unions) > 0 +} + +// classifiesEach classifies types by each of a composition's operands in order. +func (m *Model) classifiesEach( + types, operands []*symbols.Symbol, composing map[*symbols.Symbol]bool, +) []TypeClassification { + out := make([]TypeClassification, 0, len(operands)) + for _, operand := range operands { + out = append(out, m.classifiesTypes(types, operand, composing)) + } + return out +} + +// classifiesAny is how a union of the classified types classifies: a value one of +// them classifies is one of the union's. +func classifiesAny(verdicts []TypeClassification) TypeClassification { + out := ClassifiesNone + for _, v := range verdicts { + if v == ClassifiesAll { + return ClassifiesAll + } + if v == ClassifiesSome { + out = ClassifiesSome + } + } + return out +} + +// classifiesAll is how an intersection of the classified types classifies: only a +// value every one of them classifies is one of the intersection's. +func classifiesAll(verdicts []TypeClassification) TypeClassification { + out := ClassifiesAll + for _, v := range verdicts { + if v == ClassifiesNone { + return ClassifiesNone + } + if v == ClassifiesSome { + out = ClassifiesSome + } + } + return out +} + +// classifiesExcept is how a difference of the classified types classifies: a value +// of the first that none of the rest classifies. +func classifiesExcept(verdicts []TypeClassification) TypeClassification { + if len(verdicts) == 0 || verdicts[0] == ClassifiesNone { + return ClassifiesNone + } + out := verdicts[0] + for _, v := range verdicts[1:] { + if v == ClassifiesAll { + return ClassifiesNone + } + if v == ClassifiesSome { + out = ClassifiesSome + } + } + return out +} + +// MayShareValues reports whether a cast from a value of typ to target can select +// anything: either type classifies values of the other, or one is composed of a +// type that does — a value of `Wheeled unions Car, Truck` may well be a Car. +func (m *Model) MayShareValues(target, typ *symbols.Symbol) bool { + return m.mayShareValues(target, typ, nil) +} + +func (m *Model) mayShareValues( + target, typ *symbols.Symbol, reading map[[2]*symbols.Symbol]bool, +) bool { + if m == nil || target == nil || typ == nil || reading[[2]*symbols.Symbol{target, typ}] { + return false + } + if m.ClassifiesTypes([]*symbols.Symbol{typ}, target) != ClassifiesNone { + return true + } + if reading == nil { + reading = make(map[[2]*symbols.Symbol]bool) + } + pair := [2]*symbols.Symbol{target, typ} + reading[pair] = true + defer delete(reading, pair) + for _, kind := range []ast.RelationshipKind{ast.RelUnions, ast.RelIntersects} { + for _, operand := range m.composedOperands(typ, kind) { + if m.mayShareValues(target, operand, reading) { + return true + } + } + // A type composed of one the source relates to may hold its values too. + for _, operand := range m.composedOperands(target, kind) { + if m.mayShareValues(operand, typ, reading) { + return true + } + } + } + if subtracted := m.DifferencingTypes(target); len(subtracted) > 0 { + if m.mayShareValues(subtracted[0], typ, reading) { + return true + } + } + return m.differenceMayShareValues(target, m.DifferencingTypes(typ), reading) +} + +// differenceMayShareValues reads a source difference: only the first type's values +// are its own, and none of them is a value of the types it subtracts. +func (m *Model) differenceMayShareValues( + target *symbols.Symbol, operands []*symbols.Symbol, reading map[[2]*symbols.Symbol]bool, +) bool { + if len(operands) == 0 || !m.mayShareValues(target, operands[0], reading) { + return false + } + for _, subtracted := range operands[1:] { + if m.Classifies(subtracted, target) { + return false + } + } + return true +} diff --git a/internal/core/semantics/cast_classification_test.go b/internal/core/semantics/cast_classification_test.go new file mode 100644 index 000000000..6e7d16657 --- /dev/null +++ b/internal/core/semantics/cast_classification_test.go @@ -0,0 +1,156 @@ +package semantics_test + +import ( + "testing" + + "github.com/Open-MBEE/OpenSysML/internal/core/libs" + "github.com/Open-MBEE/OpenSysML/internal/core/parser" + "github.com/Open-MBEE/OpenSysML/internal/core/resolve" + "github.com/Open-MBEE/OpenSysML/internal/core/semantics" + "github.com/Open-MBEE/OpenSysML/internal/core/source" + "github.com/Open-MBEE/OpenSysML/internal/core/symbols" +) + +// composedModel is a model of composed types — unions (one nested, one its own +// union), an intersection and a difference — with ordinary specializations to +// compare against. +func composedModel(t *testing.T) (*semantics.Model, *symbols.Index) { + t.Helper() + idx := libs.NewModelIndex() + idx.AddDocument("", parser.New(source.New("", []byte(`package T { + part def Vehicle; + part def Car :> Vehicle; + part def Coupe :> Car; + part def Truck :> Vehicle; + part def Boat; + part def Wheeled unions Car, Truck; + part def Registered unions Wheeled; + part def Looped unions Looped, Boat; + part def Electric; + part def ElectricCar :> Car, Electric; + part def ElectricVehicle intersects Vehicle, Electric; + part def CombustionVehicle differences Vehicle, Electric; + part def CycleA intersects CycleB, Vehicle; + part def CycleB intersects CycleA, Electric; + part def Burner :> CombustionVehicle; + part def RoadBurner intersects Burner, Vehicle; + part def Ping differences Ping, Pong; + part def Pong differences Pong, Ping; + }`))).ParseFile()) + idx.ExpandWildcardImports() + return semantics.NewModel(resolve.New(idx)), idx +} + +// TestClassifiesComposedTargets: a composed target classifies as its types do — +// any of a union at any nesting depth, every one of an intersection, the first of +// a difference and none of the rest — and a cyclic one neither loops nor lies. +func TestClassifiesComposedTargets(t *testing.T) { + m, idx := composedModel(t) + cases := []struct { + target, typ string + want bool + }{ + {"Wheeled", "Car", true}, + {"Wheeled", "Truck", true}, + {"Wheeled", "Coupe", true}, + {"Wheeled", "Vehicle", false}, + {"Wheeled", "Boat", false}, + {"Registered", "Car", true}, + {"Registered", "Truck", true}, + {"Registered", "Boat", false}, + {"Looped", "Boat", true}, + {"Looped", "Car", false}, + {"Vehicle", "Car", true}, + {"Car", "Vehicle", false}, + // An intersection's values are those of every type it intersects. + {"ElectricVehicle", "ElectricCar", true}, + {"ElectricVehicle", "Car", false}, + {"ElectricVehicle", "Boat", false}, + {"CycleA", "ElectricCar", false}, + {"CycleB", "Boat", false}, + // A difference's are those of the first type that are none of the rest. + {"CombustionVehicle", "Car", true}, + {"CombustionVehicle", "ElectricCar", false}, + {"CombustionVehicle", "Boat", false}, + } + for _, c := range cases { + target := dimensionSymbol(t, idx, "T::"+c.target) + typ := dimensionSymbol(t, idx, "T::"+c.typ) + if got := m.Classifies(target, typ); got != c.want { + t.Errorf("Classifies(%s, %s) = %v, want %v", c.target, c.typ, got, c.want) + } + verdict := m.ClassifiesTypes([]*symbols.Symbol{typ}, target) + if c.want && verdict != semantics.ClassifiesAll { + t.Errorf("ClassifiesTypes(%s, %s) = %v, want all", c.typ, c.target, verdict) + } + if !c.want && verdict == semantics.ClassifiesAll { + t.Errorf("ClassifiesTypes(%s, %s) = all, want less", c.typ, c.target) + } + } +} + +// TestSubtractedTypeExcludesADeclaredValue: a value whose declared type +// specializes a difference is still none of its values when another type it is of +// is one the difference subtracts, however the difference is reached. +func TestSubtractedTypeExcludesADeclaredValue(t *testing.T) { + m, idx := composedModel(t) + sym := func(name string) *symbols.Symbol { return dimensionSymbol(t, idx, "T::"+name) } + for _, c := range []struct { + name string + types []string + target string + want semantics.TypeClassification + }{ + {"declared burner", []string{"Burner"}, "CombustionVehicle", semantics.ClassifiesAll}, + {"burner held as electric", []string{"Burner", "Electric"}, "CombustionVehicle", semantics.ClassifiesNone}, + {"burner held as an electric car", []string{"Burner", "ElectricCar"}, "CombustionVehicle", semantics.ClassifiesNone}, + {"through an intersection", []string{"RoadBurner", "Electric"}, "RoadBurner", semantics.ClassifiesNone}, + {"cyclic differences terminate", []string{"Ping"}, "Ping", semantics.ClassifiesAll}, + } { + types := make([]*symbols.Symbol, 0, len(c.types)) + for _, name := range c.types { + types = append(types, sym(name)) + } + if got := m.ClassifiesTypes(types, sym(c.target)); got != c.want { + t.Errorf("%s: ClassifiesTypes(%v, %s) = %v, want %v", c.name, c.types, c.target, got, c.want) + } + } +} + +// TestMayShareValuesOfComposedTypes: a cast between a composed type and a type +// one of its operands relates to selects rather than being unrelated. +func TestMayShareValuesOfComposedTypes(t *testing.T) { + m, idx := composedModel(t) + cases := []struct { + target, typ string + want bool + }{ + {"Car", "Wheeled", true}, + {"Coupe", "Wheeled", true}, + {"Car", "Registered", true}, + {"Boat", "Wheeled", false}, + {"Boat", "Looped", true}, + {"Car", "Looped", false}, + {"Electric", "ElectricVehicle", true}, + {"Boat", "ElectricVehicle", false}, + // A cast to a composed type selects from a type it is composed of. + {"ElectricVehicle", "Vehicle", true}, + {"ElectricVehicle", "Car", true}, + {"ElectricVehicle", "Boat", false}, + {"CycleA", "Electric", true}, + {"CycleA", "Boat", false}, + {"Wheeled", "Boat", false}, + // A difference holds values of the first type it names and none of the rest, + // so a type the rest classify shares nothing with it. + {"Car", "CombustionVehicle", true}, + {"Electric", "CombustionVehicle", false}, + {"ElectricCar", "CombustionVehicle", false}, + } + for _, c := range cases { + target := dimensionSymbol(t, idx, "T::"+c.target) + typ := dimensionSymbol(t, idx, "T::"+c.typ) + if got := m.MayShareValues(target, typ); got != c.want { + t.Errorf("MayShareValues(%s, %s) = %v, want %v", c.target, c.typ, got, c.want) + } + } +} diff --git a/internal/core/semantics/dimension.go b/internal/core/semantics/dimension.go index ed557d642..72b258890 100644 --- a/internal/core/semantics/dimension.go +++ b/internal/core/semantics/dimension.go @@ -262,6 +262,30 @@ func (m *Model) dimensionOfQuantityType(typ *symbols.Symbol) (Dimension, bool) { return Dimension{Term: term, Unit: leafName(typ.Name)}, true } +// FixesMeasurementReference reports whether a quantity type states a measurement +// reference of its own, so its values are exactly the quantities that reference +// measures; a subtype inheriting one narrows it by something else. +func (m *Model) FixesMeasurementReference(sym *symbols.Symbol) bool { + if m == nil || sym == nil || m.resolver == nil { + return false + } + if target, ok := m.resolver.ResolveAliasTarget(sym); ok { + sym = target + } + if _, ok := m.resolver.LocalBinding(sym.Scope, memberMRef); ok { + return true + } + if sym.Scope != nil { + return false + } + for _, child := range m.resolver.Index().LookupDirectChildrenNamed(sym.Name, memberMRef) { + if leafName(child.Name) == memberMRef { + return true + } + } + return false +} + // quantityValueTypeOf returns the nearest supertype of sym that is a // ScalarQuantityValue definition, or nil. func (m *Model) quantityValueTypeOf(sym *symbols.Symbol) *symbols.Symbol { diff --git a/internal/core/semantics/evaluable.go b/internal/core/semantics/evaluable.go index e95330e21..4a0a98cb1 100644 --- a/internal/core/semantics/evaluable.go +++ b/internal/core/semantics/evaluable.go @@ -52,7 +52,7 @@ func (m *Model) evaluable(scope *symbols.Scope, expr ast.Node, depth int) bool { case *ast.FeatureChainExpr: return m.evaluable(scope, e.Operand, depth+1) } - // A cast, a body and anything else read the instance the expression runs on. + // A body and anything else read the instance the expression runs on. return false } @@ -81,6 +81,12 @@ func (m *Model) evaluableOperator(scope *symbols.Scope, e *ast.OperatorExpr, dep if !m.allEvaluable(scope, e.Operands, depth) { return false } + switch e.Operator { + case ast.OpAs, ast.OpIsType, ast.OpHasType: + // Classifying a value reads the named type, which the model holds, rather + // than folding the operation over its operand. + return m.namedType(scope, e.TypeRef) != nil + } if !allConstant(e.Operands) { return true } diff --git a/internal/core/semantics/exprtype.go b/internal/core/semantics/exprtype.go index 81e731493..7af3a831a 100644 --- a/internal/core/semantics/exprtype.go +++ b/internal/core/semantics/exprtype.go @@ -152,6 +152,38 @@ func (m *Model) scalarTable() map[*symbols.Symbol]PrimType { return table } +// ScalarLatticeElement is the lattice element sym is, as opposed to one it +// specializes; false for any type outside ScalarValues. +func (m *Model) ScalarLatticeElement(sym *symbols.Symbol) (PrimType, bool) { + if m == nil || sym == nil { + return PrimUnknown, false + } + prim, ok := m.scalarTable()[sym] + return prim, ok +} + +// PositiveScalar reports whether sym is `ScalarValues::Positive`, whose values +// exclude zero — a bound the lattice element it shares with Natural cannot carry. +func (m *Model) PositiveScalar(sym *symbols.Symbol) bool { + if m == nil || sym == nil { + return false + } + for _, positive := range m.scalarSymbols("ScalarValues::Positive") { + if positive == sym { + return true + } + } + return false +} + +// scalarSymbols are the library symbols the given qualified name indexes. +func (m *Model) scalarSymbols(fqn string) []*symbols.Symbol { + if m.resolver == nil || m.resolver.Index() == nil { + return nil + } + return m.resolver.Index().LookupQualified(fqn) +} + // ScalarSymbol returns the library definition a lattice element stands for // (`ScalarValues::Natural` for PrimNatural), or nil when none is loaded. func (m *Model) ScalarSymbol(prim PrimType) *symbols.Symbol { diff --git a/internal/core/semantics/invocation.go b/internal/core/semantics/invocation.go index 338dfa6cf..dad2d737d 100644 --- a/internal/core/semantics/invocation.go +++ b/internal/core/semantics/invocation.go @@ -426,7 +426,7 @@ func (m *Model) signatureOf(sym *symbols.Symbol) invocationSignature { optional: m.OptionalParameter(p.Symbol), } switch { - case isAnything(param.typ): + case IsAnything(param.typ): param.typ, param.untyped = nil, true case param.typ == nil && param.prim == PrimUnknown && !m.declaresType(p.Symbol): param.untyped = true diff --git a/internal/core/semantics/model.go b/internal/core/semantics/model.go index ab6ae5550..dc4903630 100644 --- a/internal/core/semantics/model.go +++ b/internal/core/semantics/model.go @@ -48,7 +48,7 @@ type Model struct { // typingArgs holds the calls whose arguments are being typed, so an argument // whose type leads back to its own call is not typed again. typingArgs map[*ast.InvocationExpr]bool - unioning map[*symbols.Symbol][]*symbols.Symbol + composed map[composedKey][]*symbols.Symbol ends map[*symbols.Symbol][]connectorEnd superEdgeCache map[*symbols.Symbol][]superEdge // generalization edges with conjugation @@ -112,7 +112,7 @@ func NewModel(resolver *resolve.Resolver) *Model { params: make(map[*symbols.Symbol]behaviorParameters), invocations: make(map[invocationKey]*InvocationSelection), typingArgs: make(map[*ast.InvocationExpr]bool), - unioning: make(map[*symbols.Symbol][]*symbols.Symbol), + composed: make(map[composedKey][]*symbols.Symbol), ends: make(map[*symbols.Symbol][]connectorEnd), superEdgeCache: make(map[*symbols.Symbol][]superEdge), @@ -653,7 +653,7 @@ func (m *Model) conforms(a, b *symbols.Symbol, unioning map[*symbols.Symbol]bool if a == nil || b == nil { return false } - if symbols.SameElement(a, b) || isAnything(b) { + if symbols.SameElement(a, b) || IsAnything(b) { return true } for _, s := range m.AllSupertypes(a) { @@ -813,23 +813,51 @@ func (m *Model) featureTypes(sym *symbols.Symbol, visiting map[*symbols.Symbol]b return types } +// composedKey names one kind of type composition of one type, the key its +// resolved operands are memoized under. +type composedKey struct { + sym *symbols.Symbol + kind ast.RelationshipKind +} + // UnioningTypes returns the resolved targets of sym's `unions` relationships: // the types sym is declared to be the union of (KerML 1.0 §8.3.3). Unioning is // not a generalization edge — a union is constrained by its members rather than // inheriting from them — so it is resolved on its own. The result is memoized. func (m *Model) UnioningTypes(sym *symbols.Symbol) []*symbols.Symbol { + return m.composedOperands(sym, ast.RelUnions) +} + +// IntersectingTypes returns the targets of sym's `intersects` relationships: the +// types whose common values are sym's (KerML 1.0 §8.3.3), memoized. +func (m *Model) IntersectingTypes(sym *symbols.Symbol) []*symbols.Symbol { + return m.composedOperands(sym, ast.RelIntersects) +} + +// DifferencingTypes returns the targets of sym's `differences` relationships: the +// values of the first that are none of the rest are sym's (KerML 1.0 §8.3.3). +func (m *Model) DifferencingTypes(sym *symbols.Symbol) []*symbols.Symbol { + return m.composedOperands(sym, ast.RelDifferences) +} + +// composedOperands resolves the targets of sym's relationships of one composition +// kind, in declaration order and without repetition. The result is memoized. +func (m *Model) composedOperands( + sym *symbols.Symbol, kind ast.RelationshipKind, +) []*symbols.Symbol { if sym == nil { return nil } - if cached, ok := m.unioning[sym]; ok { + key := composedKey{sym: sym, kind: kind} + if cached, ok := m.composed[key]; ok { return cached } - m.unioning[sym] = nil + m.composed[key] = nil var out []*symbols.Symbol seen := make(map[*symbols.Symbol]bool) for _, rel := range RelationshipsOf(sym) { - if rel == nil || rel.Target == nil || rel.Kind != ast.RelUnions { + if rel == nil || rel.Target == nil || rel.Kind != kind { continue } targetNode := rel.Target @@ -856,7 +884,7 @@ func (m *Model) UnioningTypes(sym *symbols.Symbol) []*symbols.Symbol { out = append(out, target) } - m.unioning[sym] = out + m.composed[key] = out return out } @@ -872,9 +900,9 @@ func IsElementType(sym *symbols.Symbol) bool { return sym != nil && symbols.FQNOf(sym) == "KerML::Root::Element" } -// isAnything reports whether sym is Base::Anything, the classifier every type +// IsAnything reports whether sym is Base::Anything, the classifier every type // specializes (KerML 8.3.2.1), whether or not the chain to it is declared. -func isAnything(sym *symbols.Symbol) bool { +func IsAnything(sym *symbols.Symbol) bool { return sym != nil && (sym.Name == "Base::Anything" || (sym.Name == "Anything" && sym.OwnerScope != nil && sym.OwnerScope.Owner() != nil && sym.OwnerScope.Owner().Name == "Base")) diff --git a/internal/core/semantics/operator_conformance.go b/internal/core/semantics/operator_conformance.go index 63f032646..7b8fe6aa7 100644 --- a/internal/core/semantics/operator_conformance.go +++ b/internal/core/semantics/operator_conformance.go @@ -7,8 +7,10 @@ import ( "github.com/Open-MBEE/OpenSysML/internal/core/symbols" ) -// CastConformance judges `x as T`: sound when a type of x and T specialize one -// another in either direction (KerML validateOperatorExpressionCastConformance). +// CastConformance judges `x as T`: sound when a type of x and T may share values +// (KerML validateOperatorExpressionCastConformance), which they do when either +// specializes the other or a type either is composed of does, and no type the +// operand is declared with is one the target subtracts. func (m *Model) CastConformance(scope *symbols.Scope, e *ast.OperatorExpr) Conformance { if m == nil || m.resolver == nil || e == nil || e.Operator != ast.OpAs || len(e.Operands) != 1 { return conformanceUnknown() @@ -21,9 +23,12 @@ func (m *Model) CastConformance(scope *symbols.Scope, e *ast.OperatorExpr) Confo if len(types) == 0 { return conformanceUnknown() } - for _, typ := range types { - if m.Conforms(typ, target) || m.Conforms(target, typ) { - return Conformance{Known: true, Holds: true} + // A type the target subtracts leaves it none of the operand's values. + if !m.excludes(types, target, nil) { + for _, typ := range types { + if m.MayShareValues(target, typ) { + return Conformance{Known: true, Holds: true} + } } } names := make([]string, 0, len(types))