How to force accurate indices on a private type


I have a private type that internally uses a 2 dimensional array, while doing additional processing whenever the elements of that array are set. My package looks something like this:

with MyElements;
    Width, Height : Positive;
package MyPackage is
    subtype MyXCoordinate is Positive range 1..Width;
    subtype MyYCoordinate is Positive range 1..height;
    type MyCoordinate is
            x : MyXCoordinate;
            y : MyYCoordinate;
        end record;
    type MyType is private;
    function Create return MyType;
    function Get (this  : in MyType;
                  coord : in MyCoordinate) return MyElements.MyElementType;
    procedure Set (this    :    out MyType;
                   coord   : in     MyCoordinate;
                   element : in    MyElements.MyElementType);
    type MyTypeData is array (MyXCoordinate,MyYCoordinate)
      of MyElements.MyElementType;
    type MyType is 
            data       : MyTypeData;
            otherstuff : ThatIsActuallyInThePackageButNotRelevant;
        end record;
end MyPackage

However this forces packages that interface with MyPackage to either be generic, or to dynamically instantiate a new MyPackage with the correct parameters. Granted in execution these parameters are available fairly early (they are read from a file which is passed in on command line), but it still seems like I'm missing a language element that would do this for me.

I considered just using unbound Positives for the coordinates, removing the generic and allowing a run-time outofbounds error to be generated if the bounds fail, but I can't help feeling like Ada must have some way to do this cleanly at compile time.

I know I could use SPARK, but its overkill for this project (this project is a game, written in Ada to showcase its qualities) and somewhat defeats its purpose (showcasing Ada's compile-time error checking!).

Is my generic instantiation solution the correct way to handle this, or is there something better?

My attempts so far, that don't work but feel like they might be close-ish:

type MyType is
        Width,Height : Positive;
        subtype XCoordinate is Positive 1..Width;
        subtype YCoordinate is Positive 1..Height;
        data : array (XCoordinate,YCoordinate) of MyElements.MyElementType;
    end record;

And wrapping the generic package with a 'generator' package that takes width/height as parameters to functions and procedures that then call-through to the package. (lots of code, doesn't work, wont waste space here with it).

Show source
| generics   | compilation   | ada   2016-09-30 17:09 1 Answers

Answers to How to force accurate indices on a private type ( 1 )

  1. 2016-10-02 09:10

    It looks like you need to read up on discriminants, unconstrained arrays and indefinite types.

    Here's a generic package, which solves what appears to be your actual problem:

       type Element_Type is private;
    package Dynamic_Matrix is
       type Instance (Width, Height : Positive) is tagged private;
       procedure Set (Item  : in out Instance;
                      X, Y  : in     Positive;
                      Value : in     Element_Type)
         with Pre => X <= Item.Width and Y <= Item.Height;
       function Element (Item : in     Instance;
                         X, Y : in     Positive) return Element_Type
         with Pre => X <= Item.Width and Y <= Item.Height;
       type Element_Matrix is array (Integer range <>,
                                     Integer range <>) of Element_Type;
       type Instance (Width, Height : Positive) is tagged
             Elements : Element_Matrix (1 .. Width, 1 .. Height);
          end record;
    end Dynamic_Matrix;

    Here's an example using the package to load a matrix of Booleans into a variable:

    with Ada.Text_IO;
    with Dynamic_Matrix;
    procedure Dynamic_Matrix_Demo is
       package Positive_IO is new Ada.Text_IO.Integer_IO     (Positive);
       package Boolean_IO  is new Ada.Text_IO.Enumeration_IO (Boolean);
       package Boolean_Matrix is new Dynamic_Matrix (Element_Type => Boolean);
       Width, Height : Positive;
       use Ada.Text_IO, Positive_IO, Boolean_IO;
       Get (Width);
       Get (Height);
          Matrix : Boolean_Matrix.Instance (Width  => Width,
                                            Height => Height);
          Value  : Boolean;
          for Y in 1 .. Height loop
             for X in 1 .. Width loop
                Get (Value);
                Matrix.Set (X, Y, Value);
             end loop;
          end loop;
    end Dynamic_Matrix_Demo;

Leave a reply to - How to force accurate indices on a private type

◀ Go back