From 5d84fedd89c64110dadb76b1cc370a14edbb39a9 Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Tue, 27 Oct 2026 16:09:15 +0000 Subject: [PATCH 1/2] fix(runtime): hold a namespace-level feature read in its effective multiplicity Co-Authored-By: jason.han --- .../namespace-read-multiplicity.fixed.md | 1 + docs/project/spec-compliance.md | 2 +- internal/exec/runtime/eval.go | 6 +- internal/exec/runtime/function_value.go | 7 +- internal/exec/runtime/instance.go | 34 ++++++---- .../runtime/robustness_usage_members_test.go | 5 +- internal/exec/runtime/set_feature.go | 22 ++----- .../frontend/repl/namespace_shape_test.go | 64 +++++++++++++++++++ ...mespace_feature_multiplicity.expected.json | 5 ++ ...luate_namespace_feature_multiplicity.sysml | 6 ++ ..._object_feature_multiplicity.expected.json | 5 ++ ...evaluate_object_feature_multiplicity.sysml | 6 ++ 12 files changed, 130 insertions(+), 33 deletions(-) create mode 100644 changes/unreleased/namespace-read-multiplicity.fixed.md create mode 100644 internal/frontend/repl/namespace_shape_test.go create mode 100644 tests/grpc/testdata/conformance/evaluate_namespace_feature_multiplicity.expected.json create mode 100644 tests/grpc/testdata/conformance/evaluate_namespace_feature_multiplicity.sysml create mode 100644 tests/grpc/testdata/conformance/evaluate_object_feature_multiplicity.expected.json create mode 100644 tests/grpc/testdata/conformance/evaluate_object_feature_multiplicity.sysml diff --git a/changes/unreleased/namespace-read-multiplicity.fixed.md b/changes/unreleased/namespace-read-multiplicity.fixed.md new file mode 100644 index 0000000000..6ea7922d78 --- /dev/null +++ b/changes/unreleased/namespace-read-multiplicity.fixed.md @@ -0,0 +1 @@ +- A feature read at namespace level (`sysml -e P::xs`, a bare expression or `%eval` in the REPL, gRPC `Evaluate`) now holds its value in the feature's effective multiplicity, as the same feature read on an object already did: a `[0..*]` attribute valued `= 4` reads `[4]` on both, where the model-level read printed the bare `4`. An at-most-one feature (`[1]`, `[0..1]`, a bare `attribute x : Integer`) still reads its one value bare, and arithmetic and comparison over the read (`P::xs + 1`, `P::xs == 4`) are unchanged. A parameter stating no multiplicity is held to `[0..*]`, so its one default reads as a one-element sequence too, and a call of a calc-typed parameter applies the one function it holds. diff --git a/docs/project/spec-compliance.md b/docs/project/spec-compliance.md index 01003020a0..2e8d677a8f 100644 --- a/docs/project/spec-compliance.md +++ b/docs/project/spec-compliance.md @@ -838,7 +838,7 @@ remain one-shot. | Nested action invocation (`action call : Callee;`, `action call = Callee(3, 4);`, `action call = Callee(a = 3);`, `perform action call : Callee;`) | `runtime/action_frame.go` `bindArguments`, `performInvocation`, `checkInputsBound`; `runtime/state_statements.go` `stateStmtHost.performNode`; `runtime/invoke_action.go` `invocationArguments`, `bindArgumentList`, `Context.actionParametersOf` (over `semantics.Model.BehaviorParametersOf`, so inherited and redefined parameters keep their effective order); `action_executor.go` `stepNestedAction` | `invoke_action_test.go:TestInvokeActionPassesParametersBothWays`, `:TestInvokeActionBindsPositionalArguments`, `:TestInvokeActionBindsNamedArguments`, `:TestInvokeActionRejectsBadArguments`; `conformance/action_node_invocation_positional`, `action_node_invocation_named`, `action_node_typed_body_inputs`, `action_node_inherited_parameters`, `action_node_invocation_empty`, `action_inherited_typed_node_scope`, `action_node_arguments_before_defaults`, `state_block_flow_node_arguments_before_defaults` | ✅ Faithful (arguments bind the callee's inputs by the callee's parameter order and names, never by what the caller happens to name alike; they bind the node's pins before the defaults it declares are evaluated, so a default an argument replaces is never evaluated and one the node keeps reads the argument's value, in an action's flow and in a state's body alike; the callee is resolved where the node was declared, so a node a derived action inherits still finds a callee visible only to the general action; a surplus, missing, unknown or repeated argument is `errActionArity`, `errUnboundParameter`, `errUnknownParameter` or `errDuplicateArgument` before the callee runs — a surplus one is also reported statically by `passes/typecheck_expr.go`, so no conformance fixture states it. The row above states the compatibility by-name fallback a bare usage keeps) | | Assignment statement in a body (`assign x := `) | `lower/action_graph.go` lowerStatement Assign; `runtime/action_statements.go` execStatement | `action_send_accept.sysml`, `lower/action_body_test.go:TestActionBodyLowering` | ✅ Faithful | | A value written to a feature conforms to that feature's declared type, by the relation that governs binding an initial value: `Actions::AssignmentAction :> FeatureWritePerformance, Action` "updates the `accessedFeature` of its `target` Occurrence with the given `replacementValues`" and `FeatureReferencingPerformances::FeatureWritePerformance` "assigns the values of a feature on an occurrence to the given `replacementValues`", so what is written are values *of that feature* and answer to its type. The values of a feature are instances of all its types (KerML 1.1 §8.3.3.3.4), so a feature holds a value exactly when `istype` would affirm the feature's type of it — the one shared `runtime/classification.go` `classifyValue`, so a write and a classification never judge the same value and type differently. Specialization widens (a subtype value where a supertype is declared), the scalar lattice widens by representation (`Integer ⊑ Rational ⊑ Real ⊑ Complex`: an integer is held by a `Rational` or `Real` feature, a finite real — a `Rational`, §8.4.4.9.2 — by a `Real` one, and neither the whole real `2.0` nor the quotient `4 / 2` by an `Integer` or `Natural` feature, whatever number it is; `RationalFunctions::ToInteger`, `RealFunctions::ToInteger` and `IntegerFunctions::ToNatural` convert), a target the value's types leave open holds it (`Natural = 7`, `Even :> Integer = 4`, `Cost :> Real = 250.0` — the declaration being what states which of the supertype's values it is — while the bounds of `Natural` and `Positive` refuse `-1` and `0`), and an untyped or `Anything`-typed target holds anything. Statically, an expression's type only bounds its values, so the type pass refuses a value only for a disjoint type (`String` to `Integer`), when the value is a literal, whose type is exact (`2.5` to `Natural`), or when it is a quotient, a `Rational` however whole (`IntegerFunctions::'/'`, §9.4.11.1: `Integer = 7 / 2`, `Natural = i / 2`, an argument `add(4 / 2)` to an `Integer` parameter); a call or a `Real` feature bound to an `Integer` is the run time's to judge, since a `Real` feature may hold an integer, and the run time judges every binding it holds a value for: a default a declaration binds (folded ahead of time or evaluated on first read), a value read through a declaration, an argument or default bound to a calc parameter (inherited or redefined), and a calc's result. A calc parameter or result is held in the shape its declared multiplicity gives it, the one decision as for an action parameter: a stated `[0..*]` or `[n]` holds a sequence (one computed value becomes a one-element sequence), a stated `[1]` or `[0..1]` the sole value, and one stating no multiplicity what the body computed; a condition, `==` and `===` read a one-element collection as the value it holds, and a generated Go or C program (`codegen.Held`) holds and reads its parameters and result the same way (`calc_param_multiplicity_many_consumers.sysml`, `TestCompiledCalcsAgreeWithInterpreter`). A value's element count answers to the applicable multiplicity: a non-parameter feature is judged against the multiplicity it states or inherits — its own, the one it redefines, or, abstract, the intersection of what it subsets (the redefinition-and-subsetting row of the Instantiation map) — and against the implicit `[1..1]` where SysML v2 §7.6.3 declares it (`attribute z : Real;` on a part, action or state def refuses `(3.0, 4.0)` whether a nested action, the definition's own body or an entry action writes it); one that states and inherits none has the usual default `0..*` (KerML 1.1 §7.4.12; the default-multiplicity and representative-object rows of the Instantiation map), so a write of several values to it is held on every path — `attribute x : Real :> many;` written `(3.0, 4.0)` holds both whether a part def's nested action writes the part's feature (`Instance.SetFeatureValue` → `Context.checkAdmits`, no count judged where `MultiplicityDefaulted`) or the action or state def declaring it writes its own (`ActionExecutor.setFeature`, `StateExecutor.assignAttribute` → `Context.checkNamedWriteHeld`, whose `writeTarget.countJudged` is the same `featureRange` decision) — and writes and declarations of an action parameter are judged against its effective parameter range (`EffectiveParameterRange`, SysML v2 §7.6.3), so a bare action parameter is `[0..*]` and an explicitly stated `[*]`, `[0..1]` or `[1..2]` parameter holds what it declares — and a count-judged write holds its value in the shape that multiplicity gives it, as the performance occurrence already did (`Context.admitted`): a `[1]` target the sole element, a multi-valued one a sequence (a set where declared), so the frame, the occurrence's slots, the gRPC `FeatureValue`, `%action` and `-json` agree, and the shape no longer depends on the order the body read a pin in (the Action row on pin shape); `action_param_default_scalar_count.sysml` now explicitly declares `[1]`, and `robustness_performed_action_inputs_test.go:testNestedActionParameterMultiplicity` covers bare nested parameters and explicit required inner and outer parameters; a null holds none and so reaches a `[0..1]` parameter's `??` but not a `[1..1]` one — and a Complex is one value (`ValComplex`) against any feature's multiplicity: a Complex feature holds it, a Real feature refuses one off the real axis by type, and a numeric pair `(1.0, 2.0)` is two values whatever the feature's type | `passes/typecheck_assign.go` `assignWalker` → `passes/typecheck_expr.go` `exprChecker.checkBoundValue` and `bindable` (the initial-value rule, reached with the target's declaration); `runtime/write_conformance.go` `Context.writeTargetIn` → `writeTargetOf` (the target's multiplicity and whether a write's count is judged are `runtime/shape.go` `featureRange`'s, the one decision `effectiveFeature` gives an object's feature and `Context.checkAdmits` judges: a parameter's effective range, a stated or inherited multiplicity or the implicit `[1..1]` judge the count, a defaulted feature's representative range judges none; `writeTarget.stated` carries the declaration rule below), `Context.checkTargetAs` → `shapeForTarget` (the shape a count-judged write is held in) and `shapeDeclared` (a root default binding, `runtime/action_frame.go` `registerRootBindings`), `Context.checkWrite`/`checkWriteType`/`valueConforms`, reached from `runtime/instance.go` `Instance.SetFeatureValue`, `Context.checkDefault` (at `materialize` for a folded default and `materializeFeatureValueIntrinsic` for a deferred one), `runtime/binding.go` `assignBindingEndpoint`, `runtime/eval.go` `EvalContext.declaredValue`, `runtime/write_conformance.go` `Context.checkBodyDeclaration` → `checkTarget` with `admitDeclared` (a declaration local to a calc, action or constraint body, a `{ }` block or a collection-expression body — `lower.Declare` in `runtime/statements.go`, an action node's own feature seeded by `runtime/action_frame.go` `seedDeclaredValues`, and the compiled statement tier's `runtime/compiled_stmts.go` — is judged once when its initial value is bound, by the namespace-level rule: its type with declared admission, so an enumeration-typed local holds the enumerated value; its multiplicity only where the declaration states one, an omitted multiplicity holding the count the initializer has; its uniqueness where it declares more than one value; KerML 1.1 §7.3.4, "the values of a feature are instances of its types"; a local declaring no type holds anything), the statement hosts' `assignData`/`assignOuter`, `ActionExecutor.setFeature` and `StateExecutor.assignAttribute`; `runtime/invoke_calc.go` `bindCalcParameters` and `runtime/calc_statements.go` `calcStmtHost.acceptReturn` and `runtime/calc_usage.go` `calcRun.value` (an output a declaration binds rather than a body assigns, and a result a `bind result = ...` binds, which `calcShape.designatedOutput` keeps the declared result's declaration for) through `calcMemberDecl.check` (the parameter's effective declaration: `calcMemberDecl.redeclaring` keeps the type and multiplicity a redeclaration states none of from the parameter, output or result it redeclares, per KerML 1.1 §7.3.4.5; the compiled calc tier's `runtime/compile.go` `scalarCheck.accepts` decides the same declaration on the lattice, `least` being the `Positive` bound, and hands every value it declines to `calcMemberDecl.check`) and `Context.writeCountRefusal` (`runtime/write_conformance.go`, shared with `checkWrite` and `checkDefault`; `elementCount` in `runtime/collections.go` counts a scalar, a Complex included, without materializing a sequence); `runtime/state_statements.go` `stateStmtHost.assignStateAttribute` for an attribute held in a state's own frame | `passes/typecheck_assign_test.go` (state entry/do bodies, action bodies, calc bodies, transition effects, numeric widening, silence on an unknown type); `passes/typecheck_expr_test.go:TestExprQuotientDoesNotBindToWholeNumberFeature` (`Integer = 4 / 2` refused, `Rational = 7 / 2` and `Integer = RationalFunctions::ToInteger(4 / 2)` accepted), `:TestExprInvocationArgumentNarrowerThanExpression` (`add(7 / 2, 1)` refused, `add(RationalFunctions::ToInteger(7 / 2), w)` accepted), `:TestExprBindWiderTypedReferenceToNarrowerFeatureOK`, `:TestExprBindDecimalLiteralToNaturalRejected`, `:TestExprBindStringToIntegerAttribute`; `runtime/value_conformance_test.go:TestDefaultValueMustConformAtMaterialization` (`whole : Integer = 4 / 2`, `nat : Natural = 4 / 2`, `fromReal : Integer = two` and `computed : Integer = seven - two` are `ErrTypeMismatch`; `wholeRational : Rational = 4 / 2` holds `2.0` and `wholeConverted : Integer = ToInteger(4 / 2)` holds `2`), `:TestRestatedDefaultConformsByItsOwnValue`, `:TestDeclaredValueReadChecksItsType`, `:TestUserDeclaredScalarTypeDefersToTheBinding`, `:TestCalcParameterAndResultMustConform` (`Half(4 / 2)` and `Half(two)` refused, `Half(ToInteger(4 / 2))` accepted), `runtime/compile_test.go:TestCompiledCalcErrorParity` (`Natural1(-1)`, `Positive1(0)` and a `Positive` or `Rank :> Positive` result of `0` are the interpreter's `ErrTypeMismatch` on the compiled tier too), `sweep/sweep_test.go` (a sweep range over a `Natural`/`Positive` parameter admits what the parameter holds, in the interpreter and compiled alike), `conformance/value_classification_shared_rule` (`e : Even = 4`, `q : Rational = 6 / 3`, `none : Integer[0..1]`), a feature typed by an enumeration admits exactly the enumerated values (SysML v2 §8.3.7, the classification row) — `held : Level = three` for `three : Integer = 3` is held as `Level::high` (`checkWriteType` → `holdAsEnumerated`, so `held hastype Level` is `true`) and `= two` is the write-conformance `ErrTypeMismatch`, and a calc parameter, output or result declared by an enumeration holds its argument the same way (`calcMemberDecl.check` → `holdForDeclared`; `runtime/compile.go` `scalarCheckFor` declines an enumeration-typed declaration, so the compiled tier hands it to the same checker), so `asLevel(3) hastype Level` is `true` for `calc def asLevel { in n : Integer; return : Level = n; }`; where the value is constant the checker refuses it at its spelling (`passes/typecheck_value.go` `checkEnumeratedValue`: `Level = 2` is `cannot bind 2 (an Integer) to a feature typed by Level, whose values are Level::low = 1, Level::high = 3`, while a value of another kind stays the scalar lattice's one diagnostic) — `classify_test.go:TestEnumerationTypedFeatureAdmitsOnlyEnumeratedValues`, `robustness_classification_test.go:enumeration_typed_feature_holding_an_unenumerated_value`, `passes/typecheck_value_test.go:TestValueScalarConstantToScalarValuedEnumeration`, `:TestCalcParameterAndResultMultiplicity`, `:TestCalcMultiplicityViolationNamesTheBinding`, `:TestComplexCountsAsOneValue`, conformance `calc_body_local_declared_type` (`BodyOnly(3)` is `3` with `l` held as `Level::high`, `BodyOnly(2)` is the write's `ErrTypeMismatch`, `attribute xs : Integer[2] = (n, n + 1, n + 2)` `ErrMultiplicityViolation`, `attribute xs : Integer[*] = (n, n + 1, n)` `ErrUniquenessViolation`, an untyped local and one stating no multiplicity hold what they are given, a local in an `if` block and in a `->collect` body is judged the same), `action_body_local_declared_type`, `constraint_body_local_declared_type`, `constraint_body_local_count` (a condition reads its body's declaration through `eval.go` `conformBodyDeclared`, a stated multiplicity judging the count, determined or open, and an omitted one keeping it — `undetermined_test.go:TestBodyLocalKeepsOpenInitializerCount`), `constraint_param_scalar_count` (the unchanged constraint-parameter case), `action_param_default_scalar_count.sysml` (now explicitly `[1]`, preserving its two-value `ErrMultiplicityViolation` expectation), `robustness_performed_action_inputs_test.go:testNestedActionParameterMultiplicity` (bare nested action parameters admit no input, while explicit `[1]` inner and outer parameters preserve their typed errors), `constraint_body_local_redefined_type` and `constraint_body_local_redefined_count` (a local inheriting its initializer from the declaration it redefines is held to the redefinition, `shape.go` `statedMultiplicity` walking the same redefinition, positional-parameter and abstract-subsetting chain as the effective multiplicity — `undetermined_test.go:TestBodyLocalIntersectsRedefinedMultiplicities`, `TestBodyLocalInheritsImplicitParameterMultiplicity`), `constraint_body_local_redefined_unique` and `action_body_local_redefined_count` (the inherited bound also gates uniqueness and the lowered `checkBodyDeclaration` path), `robustness_body_locals_test.go:body_local_outside_its_declaration`, `tests/codegen/compiled_calcs_test.go:TestCompiledCalcsAgreeWithInterpreter` (`PosLoc`, `Seq::LocM1`, `Seq::LocN`, `Seq::LocAny2`: the native tier declares the local through `codegen/compile.go` `compileDeclare` → `bind` with the declared range and stated multiplicity, `codegen/ir.go` `Declare.Range`, and declines an enumeration-typed local and one redefining or subsetting another feature — `TestCompileRefusesWhatItCannotCompile` `SubsetLocal` — `not compilable`, rather than answer differently), pilot-exec-diff `body_local_conformance` (the pilot binds a body-local value unchecked, so the accepted case agrees and the refused ones are ours-error against its answer), `invoke_calc_body_test.go:TestCalcForLoopOverParameterSequence` (`in xs[*];`), `conformance/calc_null_coalesce.sysml` (`in n : Integer[0..1];`), `conformance/calc_result_multiplicity_many`, `_named_many`, `_body_many` and `_fixed` (`return : Real[0..*] = x`, `return r : Real[0..*] = x`, a `[0..*]` result the trailing expression binds and `return : Real[2]` hold sequences), `_one` and `_optional` (`[1]` and `[0..1]` hold the bare value), `_unstated` and `_unstated_named` (a bare `return : Real` keeps the computed scalar) and `verification_result_multiplicity_many` (a `VerdictKind[0..*]` verdict is read from its one element — `verification_run.go` `verdictOf` reads through `soleElement`), `conformance/calc_library_feature_imaginary_unit.sysml` (`return : Complex = i;`), pilot-exec-diff `intdiv` (deliberately `ours-error`, now refused by the checker: the reference answers `3.5` for `return : Integer = 7 / 2`, checking nothing against the parameter's type) and `rational-feature-hastype-integer` (`rat : Rational = 4` holds the `Integer` `4`); `conformance/assign_write_conforms_to_target_type.sysml`, `assign_write_violates_target_type.sysml`, `assign_write_through_chain_violates_target_type.sysml`; `robustness_typed_writes_test.go:write_of_a_wrong_typed_value_leaves_the_feature`, `:state_entry_write_of_a_wrong_typed_value`, `:chained_write_of_a_wrong_typed_value`, `robustness_calc_invocation_test.go:calc_output_write_of_a_wrong_typed_value`, `:action_local_write_of_a_wrong_typed_value`, `:action_output_write_of_a_wrong_typed_value`, `:performer_feature_write_of_a_wrong_typed_value`, `:performance_occurrence_write_of_a_wrong_typed_value`, `robustness_calc_usage_test.go:calc_output_binding_violates_declared_type`; `conformance/assign_write_to_state_attribute_violates_target_type.sysml` | ⚠️ Approximate (self-assessed: the pinned pilot implementation executes no action or state machine, so it cannot referee this. A quantity value carries its unit rather than the quantity value type measured in it, so the specialization relation between two quantity value types is not itself decided; the quantity kind such a target declares is judged dimensionally, by the row below. A model declaring its own scalar types gives the run time no value semantics for them, so there a value is refused only for a disjoint type, the binding rule's either-direction conformance standing in for a judgement by value. A Complex is a `Complex` on the real axis or off it — `rect(2.0, 0.0)` is refused by a `Real` or `Integer` feature, `re` of it is the `Real` — since `ComplexFunctions` return `Complex` and the specification fixes no finer classification of such a value. The fixtures that relied on a whole real or a quotient being held by an `Integer` feature were re-adjudicated by this rule rather than relaxed: an `Integer` or `Natural` feature or parameter a quotient or a whole real reaches is declared `Rational` or `Real` where the model computes such a value (`tests/codegen/testdata/compile_calcs.sysml`, `repl/choice_test.go`, `grpc/explore_test.go`, `lsp/library_invocation_test.go`, `passes/typecheck_value_test.go`, `runtime/classify_test.go`), converts with `ToInteger` where it means the integer (`runtime/value_conformance_test.go`, `passes/typecheck_expr_test.go`), or pins the typed error where the write is what the fixture probes (`runtime/value_conformance_test.go`, `robustness_quantities_test.go` coordinate-frame failure modes: a number written where a `ScalarMeasurementReference` or a `TranslationOrRotation` is declared is the write's `ErrTypeMismatch`), each by §8.3.3.3.4 and §9.4.11.1 above) | -| A performed action's parameter holds its values in the shape its effective multiplicity gives them from the moment it is bound, on every surface alike (KerML 1.1 §7.3.4 — the values of a feature are a sequence its multiplicity constrains; SysML v2 §7.6.3 — a parameter stating no multiplicity has no implied `1..1`, so a bare pin is `[0..*]`): a `[1]` pin holds its one value bare, a pin written without a multiplicity or `[0..*]` holds a one-element sequence, `[0..*]` holding several or none is that sequence or the empty one, and so for `in`, `out` and `inout` pins, the pins of a state's entry, do and exit actions, a nested performed action at every depth, a pin bound through `:>>` or through the same-position parameter of a specializing action def (which inherits the multiplicity it implicitly redefines unless it states its own), a pin the body reads twice, and the slots of the part performing the action — in the action's results, `-json`, the trace, the performing object's features and the gRPC `FeatureValue`. `bare_parameter_effective_multiplicity_action_bare` accordingly reads its bare `out n` as `[0]`: the count that case pins is unchanged, the shape now follows the multiplicity the case is about rather than being printed as computed. A calculation's `return` and a case's verdict take the same rule (`runtime/invoke_calc.go` `calcMemberDeclFor` resolves a parameter stating no multiplicity to `semantics.EffectiveParameterRange`): a bare `return : Real` is a one-element sequence, `[1]` or `[0..1]` the bare value (SysML v2 §7.6.3 — no implicit `[1..1]` for a reference usage; §7.19.2 — a `return` redefines the `[0..*]` result it inherits; KerML §7.3.4.2 — an unspecified feature has only the default subsetting of `things`), and a `return attribute r : Real` is `[1..1]` by the attribute rule; a calc `out` parameter a body assigns is a body write and takes the rule. The case and analysis consumers of verdicts, selected alternatives, ranges, indexes, conditions and quantities read a one-element sequence as its element (KerML §7.4.8), and a feature reads a value bound from such a result in its own shape (`runtime/set_feature.go` `declaredCollection`) | `runtime/write_conformance.go` `shapeForTarget` (from `checkTargetAs`, so `checkNamedWriteAs` for `ActionExecutor.setFeature`, `checkBodyDeclarationAs` and `calcMemberDecl.check` share it) and `shapeDeclared` (`runtime/action_frame.go` `registerRootBindings`, a default the root binds with no body write); `runtime/instance.go` `Context.admitted` on the occurrence side; the one-value consumers of the sequence row above | conformance `performed_pin_shape_scalar`, `performed_pin_shape_bare`, `performed_pin_shape_multi`, `performed_pin_shape_inout`, `performed_pin_shape_nested`, `performed_pin_shape_redefined`, `performed_pin_shape_state_actions` (+ trace), `performed_pin_shape_part_scalar`, `performed_pin_shape_part_bare`; `robustness_pin_shape_test.go` (`TestRuntimeRobustnessPinShape`: a `[1]` pin bound to two values, a `[1]` output assigned from a two-valued pin, two values in a bare pin as an operand, a bare pin holding one object as a send target); `tests/grpc` `execute_action_pin_shape` (a `[1]` output as `int_value`, a bare one as a one-element `sequence`, a `[0..*]` one as the sequence); `client/opensysml` `pin_shape_helpers_test.go` `sole` over the client suites; the trace goldens whose bare-pin reads moved from `-> v` to `-> (v)` and the conformance expectations whose bare pins moved from `v` to `[v]` | ✅ Faithful | +| A performed action's parameter holds its values in the shape its effective multiplicity gives them from the moment it is bound, on every surface alike (KerML 1.1 §7.3.4 — the values of a feature are a sequence its multiplicity constrains; SysML v2 §7.6.3 — a parameter stating no multiplicity has no implied `1..1`, so a bare pin is `[0..*]`): a `[1]` pin holds its one value bare, a pin written without a multiplicity or `[0..*]` holds a one-element sequence, `[0..*]` holding several or none is that sequence or the empty one, and so for `in`, `out` and `inout` pins, the pins of a state's entry, do and exit actions, a nested performed action at every depth, a pin bound through `:>>` or through the same-position parameter of a specializing action def (which inherits the multiplicity it implicitly redefines unless it states its own), a pin the body reads twice, and the slots of the part performing the action — in the action's results, `-json`, the trace, the performing object's features and the gRPC `FeatureValue`. `bare_parameter_effective_multiplicity_action_bare` accordingly reads its bare `out n` as `[0]`: the count that case pins is unchanged, the shape now follows the multiplicity the case is about rather than being printed as computed. A calculation's `return` and a case's verdict take the same rule (`runtime/invoke_calc.go` `calcMemberDeclFor` resolves a parameter stating no multiplicity to `semantics.EffectiveParameterRange`): a bare `return : Real` is a one-element sequence, `[1]` or `[0..1]` the bare value (SysML v2 §7.6.3 — no implicit `[1..1]` for a reference usage; §7.19.2 — a `return` redefines the `[0..*]` result it inherits; KerML §7.3.4.2 — an unspecified feature has only the default subsetting of `things`), and a `return attribute r : Real` is `[1..1]` by the attribute rule; a calc `out` parameter a body assigns is a body write and takes the rule. The case and analysis consumers of verdicts, selected alternatives, ranges, indexes, conditions and quantities read a one-element sequence as its element (KerML §7.4.8), and a feature reads a value bound from such a result in its own shape (`runtime/set_feature.go` `declaredCollection`) | `runtime/write_conformance.go` `shapeForTarget` (from `checkTargetAs`, so `checkNamedWriteAs` for `ActionExecutor.setFeature`, `checkBodyDeclarationAs` and `calcMemberDecl.check` share it) and `shapeDeclared` (`runtime/action_frame.go` `registerRootBindings`, a default the root binds with no body write); `runtime/instance.go` `Context.heldShape`, the one shape predicate `Context.admitted` applies on the occurrence side and `runtime/set_feature.go` `declaredCollection` applies to a namespace-level read of a declared value (`-e P::xs`, the REPL, gRPC `Evaluate`), so a `[0..*]` attribute valued `= 4` reads `[4]` at model level as it does on an object; the one-value consumers of the sequence row above, `runtime/function_value.go` `boundFunction` and `declaredFunction` among them (a call applies the one function a calc-typed parameter holds) | conformance `performed_pin_shape_scalar`, `performed_pin_shape_bare`, `performed_pin_shape_multi`, `performed_pin_shape_inout`, `performed_pin_shape_nested`, `performed_pin_shape_redefined`, `performed_pin_shape_state_actions` (+ trace), `performed_pin_shape_part_scalar`, `performed_pin_shape_part_bare`; `robustness_pin_shape_test.go` (`TestRuntimeRobustnessPinShape`: a `[1]` pin bound to two values, a `[1]` output assigned from a two-valued pin, two values in a bare pin as an operand, a bare pin holding one object as a send target); `tests/grpc` `execute_action_pin_shape` (a `[1]` output as `int_value`, a bare one as a one-element `sequence`, a `[0..*]` one as the sequence); `client/opensysml` `pin_shape_helpers_test.go` `sole` over the client suites; the trace goldens whose bare-pin reads moved from `-> v` to `-> (v)` and the conformance expectations whose bare pins moved from `v` to `[v]`; `repl/namespace_shape_test.go` `TestEvalNamespaceReadHoldsEffectiveMultiplicity` (`[0..*]`, `[1]`, `[0..1]`, bare, `[2]`, empty and `(4)`-valued features at namespace and object level, `P::xs + 1`, `P::xs == 4`), `tests/grpc` `evaluate_namespace_feature_multiplicity`, `evaluate_object_feature_multiplicity`, `robustness_usage_members_test.go` (a constraint's bare `in limit = 100.0` reads `[100.0]`) | ✅ Faithful | | A constant is a value of the scalar type its representation states and of that type's supertypes, whatever number it holds: an integer is an `Integer` (and so a `Rational`, `Real`, `Complex`, `Number`) whether written `2` or computed as `ToInteger(4 / 2)`; a finite real is a `Rational` — `2.0`, `4 / 2` (which `IntegerFunctions::'/'` declares `Rational`, KerML 1.1 §9.4.11.1) and `3.5` alike, so none is held by an `Integer` feature and nothing is truncated to become one (§8.4.4.9.2: a `LiteralRational` is classified in `Rational`); an infinity is a `Real`; a Complex is a `Complex` on the real axis or off it; a NaN, real or complex, states no type at all and so is of none — `istype`, `hastype`, `@` and `as` answer nothing for it, a `Real` or `Rational` parameter refuses it as `ErrTypeMismatch` on both calc tiers and its direct type is `errUndeterminedValueType`, never `Rational` — while `*` is the `Positive` exceeding every bound (§9.3) and is placed on the lattice as one: a subtype a model declares of `Positive` (or of any type above it) holds it through a declared feature and leaves a bare cast undecided, exactly as `Even :> Integer` treats `4`, while `String`, `Boolean` and their subtypes exclude it; a sequence index is still the position a whole value names (`Value.WholeNumber`), which is arithmetic, not classification | `runtime/classification.go` `representationPrim`, `representationClassifies`, `scalarLibraryType`, `isNaN`; `runtime/eval.go` `directValueType`; `semantics/eval.go` `Value.WholeNumber` (a finite real with no fractional part within the `Integer` range, so NaN, an infinity and `1e19` are no whole numbers); `runtime/write_conformance.go` `valueConforms` over `classifyValue` | `semantics/eval_test.go:TestWholeNumberRefusesFractionsAndNonFinite`; `runtime/value_conformance_test.go`, `:TestNaNIsOfNoScalarType`, `runtime/compile_test.go:TestCompiledCalcErrorParity` (`SameReal(NaN)`, `SameRational(NaN)`), `runtime/infinity_test.go:TestInfinityDirectType`, `:TestUnboundedAgainstDeclaredSubtype`, `:TestComplexCountsAsOneValue`, `runtime/complex_test.go`; `runtime/eval_operator_test.go:TestTypeClassificationOperators` (a model's own `Integer`/`Natural` keep their declared relation); conformance `value_classification_shared_rule`; pilot-exec-diff `scalar_classification.cases` | ✅ Faithful | | A bound or written quantity is measured in the dimension its target's declared quantity value type fixes: `ScalarQuantityValue` declares `attribute :>> mRef: ScalarMeasurementReference`, `ScalarMeasurementReference` declares `attribute quantityDimension: QuantityDimension[1]`, and a quantity kind narrows that reference to one unit definition (`DurationValue :>> mRef: DurationUnit[1]`, whose `durationPF` states `quantity = isq.T`, `exponent = 1`), so the type states the dimension its values are measured in and a unit of another dimension is not one of them. Scale is not part of a dimension, so `5 [min]` and `250 [ms]` conform where `5 [s]` does, and a composed unit is judged by the dimension it reduces to (`10 [m] / 2 [s]` conforms to `SpeedValue`, not to `DurationValue`) | `semantics/dimension.go` `Model.DimensionOfType` (beside `DimensionOfFeature`, sharing `quantityValueTypeIn`), compared with `Model.DimensionOfUnit` by `UnitTerm.Commensurable`; `passes/typecheck_dimension.go` `exprChecker.checkValueDimension`, reached from `passes/typecheck_expr.go` `exprChecker.checkBoundValue` and so from `passes/typecheck_assign.go` `assignWalker`; `runtime/write_conformance.go` `Context.quantityConforms`, reached from `Context.valueConforms` so every write path inherits it | `semantics/dimension_type_test.go:TestDimensionOfTypeFixesTheDeclaredKind`, `:TestDimensionOfTypeThroughAnAlias`, `:TestDimensionOfTypeMatchesTheFeatureItTypes`; `passes/typecheck_dimension_test.go:TestBoundQuantityOfAnotherDimension`, `:TestBoundQuantityOfTheSameDimensionAtAnotherScale`, `:TestBoundQuantityComposedToItsDimension`, `:TestAssignedQuantityOfAnotherDimension`, `:TestBoundQuantityThroughAnAlias`, `:TestBoundDimensionlessQuantity`; `conformance/action_quantity_dimension_scaled.sysml`, `action_quantity_dimension_inferred_mismatch.sysml`, `instance_quantity_dimension_mismatch.sysml`; `robustness_quantities_test.go:quantity_write_of_another_dimension` | ⚠️ Approximate (self-assessed: the pinned pilot implementation executes no action or state machine, so it cannot referee this. the rule is stated as the existing type-mismatch error with a dimension-specific message rather than a new diagnostic kind, so `-validate`, the REPL and the LSP report it identically) | | Nothing a declaration does not determine is judged dimensionally: a target typed by a scalar (`Real`), an untyped target, and `ScalarQuantityValue` itself — whose `mRef` is any `ScalarMeasurementReference` — fix no dimension, and a unit the libraries determine none for is not judged either | `semantics/dimension.go` `Model.DimensionOfType` (`quantityValueTypeIn` skips `ScalarQuantityValue`), `Model.DimensionOfUnit` (unknown where a factor's dimension is unknown); `passes/typecheck_dimension.go` `exprChecker.checkValueDimension`; `runtime/write_conformance.go` `Context.quantityConforms` (a scalar target keeps the primitive judgement) | `semantics/dimension_type_test.go:TestDimensionOfTypeIsSilentWhereNothingIsFixed`; `passes/typecheck_dimension_test.go:TestBoundQuantityWhereTheTargetFixesNoDimension`, `:TestBoundBareNumberStatesNoDimension`; `robustness_quantities_test.go:quantity_write_of_another_dimension` (`a unit the target fixes no dimension against`) | ✅ Faithful | diff --git a/internal/exec/runtime/eval.go b/internal/exec/runtime/eval.go index 036f40ff5e..3351d8b1b6 100644 --- a/internal/exec/runtime/eval.go +++ b/internal/exec/runtime/eval.go @@ -1333,7 +1333,11 @@ func (ec *EvalContext) conformHeld(sym *symbols.Symbol, val Value, countJudged b if err := ec.ctx.classifyHeld(sym, val); err != nil { return Value{}, fmt.Errorf("%s: %w", what(), err) } - return ec.bindVariationOf(sym, ec.ctx.classifiedFrame(sym, ec.ctx.declaredCollection(sym, val))) + val, err := ec.ctx.declaredCollection(sym, val) + if err != nil { + return Value{}, fmt.Errorf("%s: %w", what(), err) + } + return ec.bindVariationOf(sym, ec.ctx.classifiedFrame(sym, val)) } // occurrenceReference evaluates a name denoting objects of its own — an occurrence, a diff --git a/internal/exec/runtime/function_value.go b/internal/exec/runtime/function_value.go index fc5a8369f6..772873ab49 100644 --- a/internal/exec/runtime/function_value.go +++ b/internal/exec/runtime/function_value.go @@ -182,12 +182,12 @@ func (ec *EvalContext) boundFunction(callee *symbols.Symbol, qn *ast.QualifiedNa return val, true, nil } // A calc-typed feature the element being evaluated binds (`in calc :>> f = g`) - // is called as the function it is bound to. + // is called as the function it is bound to: a call takes the one function it holds. if val, ok, err := ec.valuedFeatureValue(name); ok { if err != nil { return Value{}, true, err } - if val.Kind == ValFunction { + if val = soleElement(val); val.Kind == ValFunction { return val, true, nil } } @@ -196,7 +196,7 @@ func (ec *EvalContext) boundFunction(callee *symbols.Symbol, qn *ast.QualifiedNa if err != nil { return Value{}, true, err } - if ok && val.Kind == ValFunction { + if val = soleElement(val); ok && val.Kind == ValFunction { return val, true, nil } } @@ -218,6 +218,7 @@ func (ec *EvalContext) declaredFunction(callee *symbols.Symbol) (Value, bool, er if err != nil { return Value{}, true, err } + val = soleElement(val) return val, val.Kind == ValFunction, nil } diff --git a/internal/exec/runtime/instance.go b/internal/exec/runtime/instance.go index b612a24725..43f96b42ca 100644 --- a/internal/exec/runtime/instance.go +++ b/internal/exec/runtime/instance.go @@ -668,7 +668,7 @@ func (ctx *Context) denotedValue(sym *symbols.Symbol) (Value, error) { if tail != nil { return NewSequenceValue(&Sequence{elements: elements, required: tail}), nil } - return ctx.declaredCollection(sym, sequenceOf(elements)), nil + return ctx.declaredCollection(sym, sequenceOf(elements)) } // liveOccurrences is the objects recorded as what sym denotes, while every one of them lives. @@ -844,24 +844,36 @@ func (feat *EffectiveFeature) heldBy() *symbols.Symbol { return feat.Type } -// admitted is the value an admitted val is stored as: a collection for a multi-valued -// feature, its elements charged, the objects a declared value holds classified by the feature. -func (ctx *Context) admitted(feat *EffectiveFeature, val Value, how admission) (Value, error) { +// heldShape is val in the shape feat holds it: a feature's values are a sequence its +// multiplicity constrains (KerML 1.0 §7.3.4.1, §7.4.12), so a multi-valued feature holds a +// collection however the value was written, a single value being that collection's one +// element, and an at-most-one feature holds a one-element collection's element bare. +func (ctx *Context) heldShape(feat *EffectiveFeature, val Value) (Value, error) { if val.Kind == ValUndetermined { // A value the model leaves open is held as it is: it is of no fixed count to collect. return val, nil } - if !feat.Scalar() && (val.Kind != ValSequence && val.Kind != ValSet || feat.HoldsSet != (val.Kind == ValSet)) { - // A multi-valued feature holds a collection however it was written, so a - // single value written to one is that collection's one element. + if feat.Scalar() { + return soleElement(val), nil + } + if val.Kind != ValSequence && val.Kind != ValSet || feat.HoldsSet != (val.Kind == ValSet) { elements := elementsOf(val) if err := ctx.chargeElements(int64(len(elements))); err != nil { return Value{}, err } - val = ctx.collectionOf(feat, elements) - } else if feat.Scalar() { - val = soleElement(val) - } else if err := ctx.chargeShaped(val); err != nil { + return ctx.collectionOf(feat, elements), nil + } + if err := ctx.chargeShaped(val); err != nil { + return Value{}, err + } + return val, nil +} + +// admitted is the value an admitted val is stored as: a collection for a multi-valued +// feature, its elements charged, the objects a declared value holds classified by the feature. +func (ctx *Context) admitted(feat *EffectiveFeature, val Value, how admission) (Value, error) { + val, err := ctx.heldShape(feat, val) + if err != nil { return Value{}, err } if how == admitDeclared { diff --git a/internal/exec/runtime/robustness_usage_members_test.go b/internal/exec/runtime/robustness_usage_members_test.go index 3e11cd3acf..79e2e30de1 100644 --- a/internal/exec/runtime/robustness_usage_members_test.go +++ b/internal/exec/runtime/robustness_usage_members_test.go @@ -99,8 +99,9 @@ func testUsageMembersUnboundConstraintInput(t *testing.T) { if err != nil || val.Kind != ValUndetermined { t.Fatalf("Probe::rig.under.limit = %s, %v; want undetermined for the input nothing binds", FormatValue(val), err) } - if val, err := eval("Probe::rig.fits.limit"); err != nil || FormatValue(val) != "100.0" { - t.Fatalf("Probe::rig.fits.limit = %s, %v; want the default 100.0", FormatValue(val), err) + // A parameter stating no multiplicity is held to [0..*], so its one default is a one-element sequence. + if val, err := eval("Probe::rig.fits.limit"); err != nil || FormatValue(val) != "[100.0]" { + t.Fatalf("Probe::rig.fits.limit = %s, %v; want the default held as [100.0]", FormatValue(val), err) } if val, err := eval("Probe::rig.fits"); err != nil || FormatValue(val) != "true" { t.Fatalf("Probe::rig.fits = %s, %v; want the verdict", FormatValue(val), err) diff --git a/internal/exec/runtime/set_feature.go b/internal/exec/runtime/set_feature.go index 0e2f679859..50bdb98b0c 100644 --- a/internal/exec/runtime/set_feature.go +++ b/internal/exec/runtime/set_feature.go @@ -45,20 +45,12 @@ func (ctx *Context) collectionOf(feat *EffectiveFeature, elements []Value) Value return sequenceOf(elements) } -// declaredCollection is a collection read through a declaration, in the shape that -// declaration holds: one value held by an at-most-one multiplicity is held bare; a set -// flowing into a sequence is its canonical sequence, a sequence flowing into a set its -// distinct elements. -func (ctx *Context) declaredCollection(sym *symbols.Symbol, val Value) Value { - if val.Kind != ValSet && val.Kind != ValSequence { - return val - } +// declaredCollection is a value read through a declaration, in the shape that declaration +// holds it (heldShape): one value held by an at-most-one multiplicity is held bare, one held +// by a multi-valued feature is a one-element collection, a set flowing into a sequence is its +// canonical sequence, a sequence flowing into a set its distinct elements. +func (ctx *Context) declaredCollection(sym *symbols.Symbol, val Value) (Value, error) { mult := ctx.featureMultiplicity(sym, nil) - if !mult.Upper.Infinite && mult.Upper.Value <= 1 { - return soleElement(val) - } - if holds := ctx.holdsSet(sym, ctx.findOwnerType(sym), mult); holds != (val.Kind == ValSet) { - return ctx.collectionOf(&EffectiveFeature{HoldsSet: holds}, elementsOf(val)) - } - return val + feat := &EffectiveFeature{Symbol: sym, Multiplicity: mult, HoldsSet: ctx.holdsSet(sym, ctx.findOwnerType(sym), mult)} + return ctx.heldShape(feat, val) } diff --git a/internal/frontend/repl/namespace_shape_test.go b/internal/frontend/repl/namespace_shape_test.go new file mode 100644 index 0000000000..c66fbe3032 --- /dev/null +++ b/internal/frontend/repl/namespace_shape_test.go @@ -0,0 +1,64 @@ +package repl + +import ( + "strings" + "testing" +) + +// A feature's values are a sequence its multiplicity constrains, so a +// namespace-level read holds one value in the feature's effective multiplicity +// exactly as the same feature read on an object does: a `[0..*]` feature valued +// `4` is `[4]` on both, an at-most-one feature holds its one value bare. +func TestEvalNamespaceReadHoldsEffectiveMultiplicity(t *testing.T) { + s := NewSession() + res := s.Submit(`package P { + private import ScalarValues::*; + attribute xs : Integer[0..*] = 4; + attribute ys : Integer[0..*] = (1, 2); + attribute e : Integer[0..*]; + attribute one : Integer[1] = 4; + attribute opt : Integer[0..1] = 4; + attribute bare : Integer = 4; + attribute two : Integer[2] = (4, 5); + attribute seq : Integer[0..*] = (4); + part def D { + attribute xs : Integer[0..*] = 4; + attribute e : Integer[0..*]; + attribute one : Integer[1] = 4; + attribute opt : Integer[0..1] = 4; + attribute bare : Integer = 4; + attribute two : Integer[2] = (4, 5); + attribute seq : Integer[0..*] = (4); + } + part d : D; + }`) + if len(res.Diagnostics) > 0 { + t.Fatalf("fixture has diagnostics: %v", res.Diagnostics) + } + for expr, want := range map[string]string{ + "P::xs": "= [4]", + "P::d.xs": "= [4]", + "P::ys": "= [1, 2]", + "P::e": "= []", + "P::d.e": "= []", + "P::one": "= 4", + "P::d.one": "= 4", + "P::opt": "= 4", + "P::d.opt": "= 4", + "P::bare": "= 4", + "P::d.bare": "= 4", + "P::two": "= [4, 5]", + "P::d.two": "= [4, 5]", + "P::seq": "= [4]", + "P::d.seq": "= [4]", + "P::xs + 1": "= 5", + "P::xs == 4": "= true", + } { + wants(t, run(t, s, "%eval "+expr), want) + lines, err := s.EvalBare(expr) + if err != nil { + t.Fatalf("%s: %v", expr, err) + } + wants(t, strings.Join(lines, "\n"), want) + } +} diff --git a/tests/grpc/testdata/conformance/evaluate_namespace_feature_multiplicity.expected.json b/tests/grpc/testdata/conformance/evaluate_namespace_feature_multiplicity.expected.json new file mode 100644 index 0000000000..20f71dcbb5 --- /dev/null +++ b/tests/grpc/testdata/conformance/evaluate_namespace_feature_multiplicity.expected.json @@ -0,0 +1,5 @@ +{ + "rpc": "Evaluate", + "expression": "P::xs", + "expected_result": {"kind": "sequence", "elements": [{"kind": "int_value", "value": 4}]} +} diff --git a/tests/grpc/testdata/conformance/evaluate_namespace_feature_multiplicity.sysml b/tests/grpc/testdata/conformance/evaluate_namespace_feature_multiplicity.sysml new file mode 100644 index 0000000000..61bdd196b1 --- /dev/null +++ b/tests/grpc/testdata/conformance/evaluate_namespace_feature_multiplicity.sysml @@ -0,0 +1,6 @@ +package P { + private import ScalarValues::*; + attribute xs : Integer[0..*] = 4; + part def D { attribute xs : Integer[0..*] = 4; } + part d : D; +} diff --git a/tests/grpc/testdata/conformance/evaluate_object_feature_multiplicity.expected.json b/tests/grpc/testdata/conformance/evaluate_object_feature_multiplicity.expected.json new file mode 100644 index 0000000000..4a31913eb9 --- /dev/null +++ b/tests/grpc/testdata/conformance/evaluate_object_feature_multiplicity.expected.json @@ -0,0 +1,5 @@ +{ + "rpc": "Evaluate", + "expression": "P::d.xs", + "expected_result": {"kind": "sequence", "elements": [{"kind": "int_value", "value": 4}]} +} diff --git a/tests/grpc/testdata/conformance/evaluate_object_feature_multiplicity.sysml b/tests/grpc/testdata/conformance/evaluate_object_feature_multiplicity.sysml new file mode 100644 index 0000000000..61bdd196b1 --- /dev/null +++ b/tests/grpc/testdata/conformance/evaluate_object_feature_multiplicity.sysml @@ -0,0 +1,6 @@ +package P { + private import ScalarValues::*; + attribute xs : Integer[0..*] = 4; + part def D { attribute xs : Integer[0..*] = 4; } + part d : D; +} From d35698ce4597b360bfc2e68434bcf57082c99ee4 Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Tue, 27 Oct 2026 16:42:50 +0000 Subject: [PATCH 2/2] refactor(runtime): keep the hold-shape comments to two lines Co-Authored-By: jason.han --- internal/exec/runtime/instance.go | 6 ++---- internal/exec/runtime/set_feature.go | 4 +--- internal/frontend/repl/namespace_shape_test.go | 6 ++---- 3 files changed, 5 insertions(+), 11 deletions(-) diff --git a/internal/exec/runtime/instance.go b/internal/exec/runtime/instance.go index 43f96b42ca..c67c2a2742 100644 --- a/internal/exec/runtime/instance.go +++ b/internal/exec/runtime/instance.go @@ -844,10 +844,8 @@ func (feat *EffectiveFeature) heldBy() *symbols.Symbol { return feat.Type } -// heldShape is val in the shape feat holds it: a feature's values are a sequence its -// multiplicity constrains (KerML 1.0 §7.3.4.1, §7.4.12), so a multi-valued feature holds a -// collection however the value was written, a single value being that collection's one -// element, and an at-most-one feature holds a one-element collection's element bare. +// heldShape is val in the shape feat holds it (KerML 1.0 §7.3.4.1, §7.4.12): a multi-valued +// feature holds a charged collection, one value its one element; an at-most-one feature holds it bare. func (ctx *Context) heldShape(feat *EffectiveFeature, val Value) (Value, error) { if val.Kind == ValUndetermined { // A value the model leaves open is held as it is: it is of no fixed count to collect. diff --git a/internal/exec/runtime/set_feature.go b/internal/exec/runtime/set_feature.go index 50bdb98b0c..a422da4b3d 100644 --- a/internal/exec/runtime/set_feature.go +++ b/internal/exec/runtime/set_feature.go @@ -46,9 +46,7 @@ func (ctx *Context) collectionOf(feat *EffectiveFeature, elements []Value) Value } // declaredCollection is a value read through a declaration, in the shape that declaration -// holds it (heldShape): one value held by an at-most-one multiplicity is held bare, one held -// by a multi-valued feature is a one-element collection, a set flowing into a sequence is its -// canonical sequence, a sequence flowing into a set its distinct elements. +// holds it (heldShape), so a `[0..*]` feature valued `4` reads `[4]` at namespace level too. func (ctx *Context) declaredCollection(sym *symbols.Symbol, val Value) (Value, error) { mult := ctx.featureMultiplicity(sym, nil) feat := &EffectiveFeature{Symbol: sym, Multiplicity: mult, HoldsSet: ctx.holdsSet(sym, ctx.findOwnerType(sym), mult)} diff --git a/internal/frontend/repl/namespace_shape_test.go b/internal/frontend/repl/namespace_shape_test.go index c66fbe3032..25400f2d4c 100644 --- a/internal/frontend/repl/namespace_shape_test.go +++ b/internal/frontend/repl/namespace_shape_test.go @@ -5,10 +5,8 @@ import ( "testing" ) -// A feature's values are a sequence its multiplicity constrains, so a -// namespace-level read holds one value in the feature's effective multiplicity -// exactly as the same feature read on an object does: a `[0..*]` feature valued -// `4` is `[4]` on both, an at-most-one feature holds its one value bare. +// A namespace-level read holds its value in the feature's effective multiplicity as the +// same feature read on an object does: `[0..*]` valued `4` is `[4]` on both, at-most-one bare. func TestEvalNamespaceReadHoldsEffectiveMultiplicity(t *testing.T) { s := NewSession() res := s.Submit(`package P {