feat(runtime): evaluate the unbounded value * and elem.metadata - #113
feat(runtime): evaluate the unbounded value * and elem.metadata#113devin-ai-integration[bot] wants to merge 11 commits into
* and elem.metadata#113Conversation
🤖 Devin AI EngineerI'll be helping with this pull request! Here's what you should know: ✅ I will automatically:
Note: I can only respond to comments from users who have write access to this repository. ⚙️ Control Options:
|
|
Runtime-verified by hand through the REPL and through the gRPC service with the Python client, beside the suite. Verified: That pass found the prompt answering Not exercised by hand: the Java, Node and Rust clients, and the capability-withholding path (both covered by tests only). Ordering note: mixed inline and |
5f77ae5 to
f1e7e7e
Compare
`*` in expression position now evaluates to a dedicated unbounded scalar that orders above every finite number, equals itself, prints as `*` in values, traces and solver output, crosses the wire in its own Value arm behind the infinity_value capability, and is refused with a typed error naming the operation in every arithmetic form. `elem.metadata` reads the annotation side table and answers an ordered sequence of materialized metadata instances, including features bound in an annotation body and the metadata type's own defaults, an empty sequence for an unannotated element, and a typed error for a non-element operand. Co-Authored-By: jason.han <hanhuijun@gmail.com>
The `about` index keys the annotated element by symbol, but the prompt evaluates against a scope tree re-indexed from the same declarations, so its twin of the element missed every annotation stated about it — `elem.metadata` and package metadata read as empty there while the same document answered them over gRPC. The index now also keys the annotations by the annotated element's declaration, which identifies it across both trees. Co-Authored-By: jason.han <hanhuijun@gmail.com>
…ty arm Review found two paths. A metadata access that failed part-way left the objects of the annotations already read registered in the context, so a retried access accumulated unreachable objects; one access now materializes every annotation or none. And the infinity arm arriving as false read as the unbounded value, letting a malformed request execute with a value it never supplied; the arm is the value itself, so only true carries it and false is refused. Co-Authored-By: jason.han <hanhuijun@gmail.com>
A metadata annotation body can read an object whose classifier behavior starts, so abandoning only the objects left that behavior attached to the context, able to run after the object it belongs to is gone. The access now rolls back from the behavior boundary as well. Co-Authored-By: jason.han <hanhuijun@gmail.com>
…ded value Metadata body values resolve in the body's own scope, nested body declarations bind through the object their feature holds, a ValInfinity constant answers ScalarValues::Positive as its direct type, and every client decoder refuses an infinity arm that is not asserted. Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
f145243 to
0b78ad5
Compare
A body declaration with a name of its own writes to the feature it redefines, so `severity :>> level = 3` binds level rather than being refused. A body value naming a sibling feature reads it off the object being bound. Co-Authored-By: jason.han <hanhuijun@gmail.com>
… access An annotation denotes one object, so a second `elem.metadata` answers what the first made rather than a fresh identity. The access is bracketed by a journal, so a failing annotation also undoes writes made while reading the ones before it, not only the objects and behaviors they left. Co-Authored-By: jason.han <hanhuijun@gmail.com>
A metadata annotation is named by the element it annotates and its place among that element's annotations rather than by its syntax node, so a carry-over rebinds it and a later read of a carried metadata object answers that object instead of making a second one. Co-Authored-By: jason.han <hanhuijun@gmail.com>
…read A carry-over compares what the annotation at that place states, type and text, before taking over the object made for it, so an annotation edited, reordered or retyped between analyses is read again rather than answered with a stale object. Co-Authored-By: jason.han <hanhuijun@gmail.com>
An `about` annotation is stated away from the element it annotates, so its digest now reads the annotating document rather than the annotated element's, which an edit there did not change and an unrelated edit here did. Co-Authored-By: jason.han <hanhuijun@gmail.com>
What and why
Two value forms the runtime could not produce are now evaluated.
*as a value. Expression-position*was parsed but not evaluable, so a body stating itwas reported as an unevaluable expression. It now evaluates to a dedicated unbounded scalar,
semantics.Value{Kind: ValInfinity}, carried as aValConstruntime value. It is a semantickind of its own rather than an IEEE infinity, so it can never be mistaken for a number:
<,<=,>and>=all answer consistently (semantics.UnboundedOrder/OrderSatisfies);*everywhere — value formatting, trace formatting, the REPL's document queries andthe solver's pinned values, which previously spelled it
∞, a spelling no SysML source uses;ErrTypeMismatchnaming theoperation, for
+,-,*,/,%,**and both unary forms, e.g.type mismatch: operator '+' is not defined for the unbounded value '*': * + 1. No panic, noNaN, no silently narrowed finite answer;
Valueoneof arm (bool infinity = 16) rather than the string"*", whichstays an ordinary string. The arm is advertised as the
infinity_valuecapability and behaveslike the other value-arm capabilities — withheld as an
unsupportednull in a response, andrefused with
UNIMPLEMENTEDin an input — with the Go, Java, Python, Node and Rust clientsand the wire contract updated for it.
The checker types the literal as
ScalarValues::Positive, which the standard library declares asthe natural number exceeding every other, so conformance of
attribute n : Natural = *;followsfrom the library rather than from a runtime special case.
elem.metadata.ref.metadatanow parses as a metadata access rather than a feature chainthrough a member named
metadata, and evaluates from the annotation side table the@@classification already reads — no re-derivation and no reparsing of declarations. The semantic
layer materializes that table into
semantics.ElementMetadata(type, node, scope, and thefeatures bound in the annotation body, in declaration order); the runtime turns each entry into
a metadata instance through the existing instance materialization, so a feature the body binds
answers that value and one it does not answers the metadata type's default. An element with no
metadata answers the empty sequence. A non-element operand (
1.metadata) is anErrTypeMismatch, an unresolved name anErrUnresolvedReference, and a body binding naming afeature the metadata type does not have an
ErrTypeMismatchnaming both — never a droppedvalue.
Specification basis
*in expression position: KerML 8.4.4.6 (unbounded natural), typed throughScalarValues::Positiveas the library declares it.features of the referenced element.
Both add rows to the Expression Evaluation table in
docs/project/spec-compliance.md(✅), andthe new wire arm is documented in
docs/reference/wire-contract.mdanddocs/reference/service-transports.md.How it was verified
New coverage:
value_unbounded_comparison,value_unbounded_arithmetic_refused(every refusedoperation) and
metadata_access_annotations(bound body values, defaults,aboutmetadata,several annotations in order, and an element with none), plus an
Infinityexpected-value typein the conformance schema and its README;
internal/core/parser/testdata/parse/unbounded_and_metadata_access.sysml;*,*compared with a string,.metadataon a value, and.metadataon an unresolved name — each a typed error;internal/core/runtime/infinity_test.go,metadata_test.goandinternal/grpc/convert_infinity_test.go(round trip of the arm, of*nested in a sequence,the withheld null and the refused input without the capability, and
"*"still an ordinarystring).
One existing test changed intentionally.
TestUnevaluableResultIsNotReportedAsMissingusedFoo.metadataand*as its two expressions the evaluator has no value kind for; both are nowevaluable, so the model states
~nandn as Fooinstead — two formsunimplementedOperatorsstill declares unevaluated. The test's contract (an unevaluable resultis reported as such, not as a missing result) is unchanged.
internal/repl/runtime_commands_test.gomoved from
∞to*with the formatter.A follow-up commit fixes a difference the prompt showed against the same document over gRPC:
the
aboutindex keys the annotated element by symbol, while the prompt evaluates against ascope tree re-indexed from the same declarations, so its twin of the element reached none of the
annotations stated about it —
elem.metadataand a package's metadata read as empty at theprompt while gRPC answered them. The index now keys those annotations by the annotated element's
declaration as well, which identifies it across both trees
(
internal/repl/metadata_about_eval_test.go).Known limitation:
*is a value and an ordering bound only — no arithmetic over it is defined,by design, since KerML gives none.
Checklist
make testandmake lintpass locallychanges/unreleased/<slug>.<section>.md, not as an edit toCHANGELOG.mdmake docs-countsrun if a gate count moved (compliance rows need nothing: the census is counted at docs build)F4,K5) in the body, docs, or changelog