feat(runtime): evaluate cast expressions - #115
Open
devin-ai-integration[bot] wants to merge 16 commits into
Open
feat(runtime): evaluate cast expressions#115devin-ai-integration[bot] wants to merge 16 commits into
devin-ai-integration[bot] wants to merge 16 commits into
Conversation
A CastExpression selects the values of its operand that the target type classifies and converts none of them, element-wise and in order for a collection, the empty sequence when none is classified. Co-Authored-By: jason.han <hanhuijun@gmail.com>
Contributor
Author
🤖 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:
|
A cast derived the operand's own type name through the reading scope, so a cast whose target was written as a fully qualified ScalarValues name in a scope importing none of them failed instead of deciding. Co-Authored-By: jason.han <hanhuijun@gmail.com>
Contributor
Author
Positive shares Natural's lattice element, so a cast to it also checks the value is above zero; an empty cast result is built with sequenceFrom so it keeps the unit its source's elements measure in. Co-Authored-By: jason.han <hanhuijun@gmail.com>
An array, vector, vector or tensor quantity, measurement reference, frame or transformation is judged against a narrower target by the shape, units and frame reading a write to a feature of that type applies, rather than being reported undecidable. Co-Authored-By: jason.han <hanhuijun@gmail.com>
A declaration named Integer, Real, Boolean, String or Complex in the scope reading a value was taken as that value's type, so a cast to the ScalarValues type of the same name kept nothing. The library symbol now answers first. Co-Authored-By: jason.han <hanhuijun@gmail.com>
A cast now reads the type a value's feature is declared with alongside the types the value itself states, so a custom scalar subtype, a scalar-valued enumeration and a constrained quantity subtype keep the values declared with them, and an expression written as a value is kept by the evaluation type it is read as. Classification operators are model-level evaluable, reading the type they name rather than folding their operand, so a metadata body may bind 1 as Integer. Co-Authored-By: jason.han <hanhuijun@gmail.com>
A cast reads all of an operand's declared result types, a union classifies the values of the types it unions, and a complex value on the real axis is judged by the real number it holds. Co-Authored-By: jason.han <hanhuijun@gmail.com>
A composed type classifies as the types composing it do: any of a union, every one of an intersection, the first of a difference and none of the rest. istype asks the same relation, and the static cast check asks whether the two types may share a value at all, so a union-typed operand cast to a member is not warned about. Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
…ialization A value directly conforming to a difference target no longer bypasses the types the difference subtracts, reached through the target, its supertypes or an intersection. Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
…arget Co-Authored-By: jason.han <hanhuijun@gmail.com>
…ment by its own declaration Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
…ded one Co-Authored-By: jason.han <hanhuijun@gmail.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What and why
x as Thad no runtime evaluation:eval.golistedast.OpAsamong the unimplemented operatorsand reported that a cast would need a value to carry the type it was cast to. It does not — a cast
selects, so all it needs is what a value already is.
runtime/cast.goevaluates it.semantics/cast.goModel.ClassifiesTypesanswers, for the types avalue is of, whether the target classifies all of them, none of them, or is narrower than them; the
runtime only dispatches on
Valuekinds and asks that question:Where the target is narrower than every type the value is of, the value itself settles it: a scalar
by its magnitude against the
ScalarValueslattice (semantics.PrimTypeOfValue/PrimConforms, reached through the newModel.ScalarLatticeElement), a quantity by whether itsunit is commensurable with the dimension the target fixes, and an object or an enumeration literal
by the types it carries — which have already answered. A collection is filtered element-wise in
order; a kept value is answered unchanged; nothing kept is the empty sequence. No conversion is
performed and no library function is touched:
ToIntegerand its siblings remain the functionsthat convert.
The type a value's own feature is declared with is a type it is of as well (
declaredCastTypes),which is what settles a target the value's content cannot:
attribute e : Even = 4keepse as Evenand
attribute room : RoomLength = 4 [m]keepsroom as RoomLength, and a scalar-valuedenumeration keeps its literals (
GradePoints::a as GradePoints).Base::Anything, which everydeclaration implicitly specializes, states nothing about the values held and is left out
(
semantics.IsAnything). An expression written as a value is of the evaluation type the model readsit as (
Model.ExprResultType), so{ in v; v > 1 } as Performances::BooleanEvaluationis a bodystill applicable afterwards while the same body
as Integeris empty. A quantity type stating ameasurement reference of its own measures every value of its dimension
(
Model.FixesMeasurementReference); one narrowing lengths by something else does not, so a bare5 [m] as RoomLengthis undecided while the value read from aRoomLengthfeature is kept.Every type an operand's result is declared with counts, not only the first
(
Model.ExprResultTypes), so a feature typed by two types is classified by both and an expression theresolver names nothing for — a selection, an index, a chain — is classified by its operand's types. A
union classifies the values of every type it unions, however deeply nested:
Model.Classifiesis theone predicate for that, applied alike by the cast, by the static cast check (which otherwise warned
that the operand's type was unrelated) and by an object's write conformance (which otherwise refused
the kept object for the feature the result is written to). A complex value arithmetic left on the real
axis is judged by the real number it holds where an ordering bound applies, so a positive sum on the
axis is a
Positiveand one off the axis is not.A target that neither the value's types nor its content settles — a bare
5againstEven :> Integer, a bare5 [m]againstRoomLength :> LengthValue— is the typedErrUndecidedClassification, reported rather than answered as the empty sequence, so a value thatmay well be one of the target's is never dropped silently. An unresolved target is
ErrUnresolvedType.Classifying a value is model-level evaluable:
evaluableOperatorreads the typeas,istypeandhastypename instead of folding the operand, so a metadata body may bindx = 1 as Integer, whilean unresolved target or an operand that is not evaluable there is still refused.
A cast reads the operand's own scalar type from the library rather than through the reading scope
(
castTypes,scalarLibraryType), so it decides the same way in a scope that writesScalarValues::Integerout in full and imports nothing — where deriving the name through the scopealone reported that the value's type could not be determined. The classification operators keep
their scope-based derivation: moving them onto the library type changed how feature writes report a
type mismatch, which is not this change's subject.
An empty result is a result, so a feature a cast may drop everything from needs multiplicity
[0..1]:return : Integer = r as Integerreports a multiplicity violation forr = 2.5, becausea lower bound of 1 is unsatisfiable by
().The unsupported-operator row and its test keep their subject (
all, bitwise complement,OpMetaand
OpIndexreached as operators); the test'sasprobe is now bitwise complement.Specification basis
KerML 1.1 §8.3.4.9 CastExpression: the result is the values of the argument that the target type
classifies, so a cast selects values and converts none. The pinned grammar
(
build/pilot-grammars/KerMLExpressions.xtext,CastOperator) already gaveasits parse, so noparser change and no golden AST fixture were needed.
docs/project/spec-compliance.mdgains a Cast expressions row (✅ Faithful) and theno-runtime-evaluation row above it loses the cast. The Structured values note that said the
runtime does not evaluate
asnow says which part of the(that.that as SpatialItem)chain stillreports:
that.that, before the cast sees a value.One divergence is recorded rather than papered over. 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, so an
Integerfeature holds4 / 2), and it is narrower than the direct type theclassification operators read, which is the literal's own type:
n : Integer = 7answersn istype Naturalfalsewhilen as Naturalkeeps7, andr : Real = 4.0answersr istype Integerfalsewhiler as Integerkeeps4.0. The pinned reference settles theclassification reading (
nat3 : Natural = 3answershastype Integertrue) and draws no outputat all for either cast, so it settles nothing about the cast; aligning one reading to the other on
no evidence would move an externally refereed row, so both are documented as they stand.
How it was verified
Corpus gates, corpora present and required:
python3 scripts/changelog.py check,make docs-checkandmake docs-countspass; no measuredfigure moved.
New conformance cases under
internal/core/runtime/testdata/conformance/:calc_cast_qualified_target(fully qualified targets in a scope importing nothing),calc_cast_scalar_values(theScalarValueshierarchy, integral and non-integralReal,Boolean,String),calc_cast_enumeration(a literal against its enumeration, a supertype,Base::DataValue, and a sibling enumeration that keeps nothing),calc_cast_quantity(
ISQBase::LengthValue,Quantities::ScalarQuantityValue, an incommensurableISQBase::DurationValue, and a mixed length/duration sequence filtered),calc_cast_instances(classifier, superclass, a sibling part definition that keeps nothing),calc_cast_structured(a vector quantity kept as a vector and tensor quantity, refused by shape asa scalar quantity, refused as a plain
NumericalValue) andcalc_cast_sequence_elementwise(element-wise order, nothing kept, empty input). Robustness:cast_to_an_unresolved_type,cast_undecided_by_the_valueandcast_of_a_quantity_to_a_constrained_subtype, all typed errors.calc_cast_declared_types(a custom scalar subtype, its scalar supertype, a scalar-valuedenumeration and its supertype, a target of another kind that keeps nothing) and
calc_cast_expression_value(a boolean body kept as aBooleanEvaluationand applied byselect,a body kept as an
Evaluation, a body dropped by a scalar target) cover the declared-type andexpression-value readings;
calc_cast_quantitygains the declared quantity subtype; andpasses/w8d_metadata_usage_test.go:TestW8DMetadataClassificationValuesAreModelLevelEvaluablecovers the metadata tier both ways.
Two further points the review raised are fixed in the branch.
ScalarValues::PositivesharesNatural's lattice element but not its zero, so the cast applies the strict bound on top of lattice
conformance (
0 as Positiveand-1 as Positiveare empty, covered incalc_cast_scalar_values),and an empty filtered result keeps the source elements' unit so a following
sumstill answers aquantity (covered in
calc_cast_quantity). A structured value narrower than every type it is of isnow decided by
write_conformance.go'svalueConforms— the same shape, unit and frame reading awrite to a feature of the target type applies — rather than reported undecidable.
Pilot execution referee
./scripts/download-pilot-evaluator.shthengo run ./cmd/pilot-exec-diff, with the sevencast_expressions.casesadded — 154 cases:No new disagreement: relative to the previous 147 the seven cases are
agree +2,pilot-silent +3,pilot-unevaluated +2, and the four pre-existingdisagreeare unchanged.Case by case:
integer-as-real(n as Real)LiteralInteger 77sequence-as-integer((1, 2.5, 3) as Integer)LiteralInteger 1,LiteralInteger 3[1, 3]integer-as-natural7fraction-as-integer(2.5 as Integer)[]whole-as-integer(4.0 as Integer)4.0car-as-vehiclePartUsage carcar-as-carPartUsage carThe two agreeing cases are the substance of the feature: the selection is unchanged for a value the
target classifies, and element-wise for a sequence. The three
pilot-silentcases are the harnesslimit documented on
docs/project/pilot-execution-referee.md: the pilot prints nothing both for alegitimately empty result and for an expression it declines, so it neither confirms nor contradicts
2.5 as Integerbeing empty or4.0 as Integerkeeping4.0— this is where the divergence notedabove is unrefereeable, and it is stated in the record rather than read as agreement. The two part
cases get the unevaluated
PartUsage carback: it names the same value we select, but it is not anevaluation of the cast, so it is not counted as agreement either.
docs/project/pilot-execution-referee.mdand the referee skill record the new counts and thisadjudication.
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)