AdaCore / RecordFlux

Formal specification and generation of verifiable binary parsers, message generators and protocol state machines
Apache License 2.0
104 stars 6 forks source link

RFLX.RFLX_Types.Operators package #1126

Closed jklmnn closed 2 years ago

jklmnn commented 2 years ago

The operators for the types defined in RFLX.RFLX_Types are currently also defined in this package. As the types in this package are only subtypes the operators are not primitive functions of these types and therefore not visible by using use type. To use these operators the whole package has to be used. Additionally the use type is still required for the default operators of these types. The reason is that they're defined in the package that provides the types for the generic types implementation. It seems there is no way around using use and use type.

To avoid withing the whole RFLX_Types package I suggest to implement the operators in RFLX.RFLX_Types.Operators so only this package has to be used completely. This avoids all the visibility and ambiguity issues that come by using RFLX_Types. To ensure backwards compatibility one could also think of only renaming the operators in the Operators child package.

treiher commented 2 years ago

To avoid withing the whole RFLX_Types package I suggest to implement the operators in RFLX.RFLX_Types.Operators so only this package has to be used completely. This avoids all the visibility and ambiguity issues that come by using RFLX_Types.

Sounds reasonable to me.

To ensure backwards compatibility one could also think of only renaming the operators in the Operators child package.

What exactly do you mean with backward compatibility here?

jklmnn commented 2 years ago

If we move the operator definitions to the child package I think we will get errors in the currently generated code as it doesn't know about the operators and therefor cannot use the types as intended. So we would have to add with RFLX.RFLX_Types.Operators; use RFLX.RFLX_Types.Operators to all units that make use of the operators. The same applies to any external code that uses the operators. We should also keep the abstract operators in the original package as otherwise afaict if you don't use the child package you can just use them as the compiler doesn't know they're overridden.

treiher commented 2 years ago

I think that would be a good thing. I don't see a good reason to allow the old/default operator behavior.