How do you perform a check for safe type conversion?

Question

To preface: I'm programming in the newest version (as of writing) of SPARK Ada with GNAT Community.

I've been looking over the internet for a simple solution for this but all results seem to point to the same answer that isn't working for me. I have a new type Digit defined as TYPE Digit IS new Integer range 0 .. 9. I'd like to safely convert Integer to Digit. For the sake of this conversion I've also created a range DigitRange defined as TYPE DigitRange IS range 0 .. 9. I'm attempting to perform this conversion by checking whether or not Digit is in the range (IF InputInteger IN DigitRange) but this raises an incompatible types compilation error.

• Is it possible to refer to the range 0 .. 9 that defines the Digit type without specifically stating IF InputInteger IN Digit? Because there's no subtyping, IN will not produce helpful results and that if statement would be invalid. I'd like to explicitly write in code that my conversion isn't performed by checking compatibility with an arbitrary variable such as DigitRange.
• Is it possible to perform this type conversion at all without subtyping while maintaining safety and not receiving a range check might fail error from gnatprove?
• Alternatively, should I just perform no check initially, convert types and then perform Output'Valid as a last resort? As far as I understand, this would still give me a range check might fail for the type conversion itself.

I'm aware that the more ideal solution to achieve this is using subtypes but I'm not permitted to do that.

Thank you for your answers.

Answer 1

As with many things in Ada, there are multiple ways to do this in Ada, and while the use of 'Pos is an excellent solution, it may be useful to see some others.

Since Digit is derived from Integer, their base types have the same range, so you can write

Digit'Base (X) in Digit

You can also define a subtype of Integer with the desired range and use it for the comparison

subtype Digit_Range is Integer range Digit'First .. Digit'Last;

X in Digit_Range

The right side of [not] in can also be a subtype definition, so you can also use

X in Integer range Digit'First .. Digit'Last

Answer 2

Applying Integer'Pos to the Integer value "converts" it to a "universal integer", which you can then test for inclusion in the range of any integer type:

   X : Integer;
   ...
   if Integer'Pos(X) in Digit then ...