如何在私有类型上强制使用准确的索引

Question

我有一个内部使用二维数组的私有类型，同时在设置该数组的元素时进行额外处理。我的包裹看起来像这样：

with MyElements;
generic
    Width, Height : Positive;
package MyPackage is
    subtype MyXCoordinate is Positive range 1..Width;
    subtype MyYCoordinate is Positive range 1..height;
    type MyCoordinate is
        record
            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);
private
    type MyTypeData is array (MyXCoordinate,MyYCoordinate)
      of MyElements.MyElementType;
    type MyType is 
        record
            data       : MyTypeData;
            otherstuff : ThatIsActuallyInThePackageButNotRelevant;
        end record;
end MyPackage

然而，这会强制与 MyPackage 接口的包要么是通用的，要么使用正确的参数动态实例化一个新的 MyPackage。在执行过程中，这些参数很早就可用（它们是从命令行传入的文件中读取的），但似乎我仍然缺少可以为我执行此操作的语言元素。

我考虑过只对坐标使用未绑定的正值，删除泛型并允许在边界失败时生成运行时间越界错误，但我不禁觉得 Ada 必须有一些在编译时干净地执行此操作的方法。

我知道我可以使用 SPARK，但它对这个项目来说太过分了（这个项目是一个游戏，用 Ada 编写以展示其品质）并且有点违背了它的目的（展示 Ada 的编译时错误检查！）。

我的通用实例化解决方案是处理这个问题的正确方法吗，还是有更好的方法？

到目前为止，我的尝试没有奏效，但感觉它们可能很接近：

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

并用 'generator' 包包装通用包，该包将 width/height 作为函数和过程的参数，然后调用包。（很多代码，不起作用，不会在这里浪费 space）。

Answer 1

看来您需要阅读判别式、无约束数组和不定类型。

这是一个通用包，它解决了您实际遇到的问题：

generic
   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;

private
   type Element_Matrix is array (Integer range <>,
                                 Integer range <>) of Element_Type;

   type Instance (Width, Height : Positive) is tagged
      record
         Elements : Element_Matrix (1 .. Width, 1 .. Height);
      end record;
end Dynamic_Matrix;

下面是一个使用包将布尔矩阵加载到变量中的示例：

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;
begin
   Get (Width);
   Get (Height);
   Skip_Line;

   declare
      Matrix : Boolean_Matrix.Instance (Width  => Width,
                                        Height => Height);
      Value  : Boolean;
   begin
      for Y in 1 .. Height loop
         for X in 1 .. Width loop
            Get (Value);
            Matrix.Set (X, Y, Value);
         end loop;
         Skip_Line;
      end loop;
   end;
end Dynamic_Matrix_Demo;

如何在私有类型上强制使用准确的索引

How to force accurate indices on a private type

generics

compilation

ada