From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!.POSTED!not-for-mail
From: Simon Wright <simon@pushface.org>
Newsgroups: comp.lang.ada
Subject: Re: matrix manipulation
Date: Sat, 27 Apr 2019 23:45:07 +0100
Organization: A noiseless patient Spider
Message-ID: <lyh8ajm5jg.fsf@pushface.org>
References: <4b46fe61-45af-4700-967c-503a4dafcee5@googlegroups.com>
Mime-Version: 1.0
Content-Type: text/plain
Injection-Info: reader02.eternal-september.org;
 posting-host="21682f1489c99ccb4937726047263d7e";
	logging-data="8687"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1+7q5WwhKPa95w5p4WTvNyDbgv4rYJtj5I="
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/26.1 (darwin)
Cancel-Lock: sha1:w4EHFJrqkNXsBwPHnGg/y7JjSLE=
	sha1:It2LGhxtX1Wh87f2IltbteDaUVU=
Xref: reader01.eternal-september.org comp.lang.ada:56202
Date: 2019-04-27T23:45:07+01:00
List-Id: <comp.lang.ada>

hnptz@yahoo.de writes:

> Hi,
>
> I would like to solve the following Ada-Programming demand:
>
> bk :=3; Dv := 4;
>
> H : Real_Matrix(1..bk*Dv,1..bk*Dv);
>
> type Block_Matrix
>    is array (Positive range <>, Positive range <>) of Real_Matrix(1..Dv,1..Dv);
>
> HB : Block_Matrix(1..bk,1..bk);
>
> Now, there are 12 Block_Matrices which make up H. After calculation of
> all HB's I want to place them into H and ended up in coding of 8
> different for loops. Is there a more elegant solution? I noticed that
> slicing would only work with a definition of linear arrays of a linear
> array, which does not fit for the rest of my program.

You might find this package helpful. I haven't been able to prove the
postconditions, due to lack of SPARK smarts, but see the demo.

--

package Block_Matrices
  with SPARK_Mode
is

   pragma Assertion_Policy (Check);

   type Matrix is array (Positive range <>, Positive range <>) of Integer;

   function Submatrix (Of_Matrix : Matrix;
                       At_Row    : Positive;
                       At_Column : Positive;
                       Rows      : Natural;
                       Columns   : Natural) return Matrix
   with
     Pre => At_Row in Of_Matrix'Range (1)
            and At_Column in Of_Matrix'Range (2)
            and At_Row + (Rows - 1) in Of_Matrix'Range (1)
            and At_Column + (Columns - 1) in Of_Matrix'Range (2),
     Post => Submatrix'Result'First (1) = At_Row
             and Submatrix'Result'Length (1) = Rows
             and Submatrix'Result'First (2) = At_Column
             and Submatrix'Result'Length (2) = Columns
             and (for all J in Submatrix'Result'Range (1) =>
                    (for all K in Submatrix'Result'Range (2) =>
                       Submatrix'Result (J, K) = Of_Matrix (J, K)));

   procedure Assign (Submatrix : Matrix; To : in out Matrix)
   with
     Pre => Submatrix'First (1) in To'Range (1)
            and Submatrix'Last (1) in To'Range (1)
            and Submatrix'First (2) in To'Range (2)
            and Submatrix'Last (2) in To'Range (2),
     Post => (for all J in Submatrix'Range (1) =>
                (for all K in Submatrix'Range (2) =>
                   To (J, K) = Submatrix (J, K)));

end Block_Matrices;

package body Block_Matrices
with SPARK_Mode
is

   function Submatrix (Of_Matrix : Matrix;
                       At_Row    : Positive;
                       At_Column : Positive;
                       Rows      : Natural;
                       Columns   : Natural) return Matrix
   is
   begin
      return Result : Matrix
        (At_Row .. At_Row - 1 + Rows, At_Column .. At_Column - 1 + Columns) do
         for J in Result'Range (1) loop
            for K in Result'Range (2) loop
               Result (J, K) := Of_Matrix (J, K);
            end loop;
         end loop;
      end return;
   end Submatrix;

   procedure Assign (Submatrix : Matrix; To : in out Matrix)
   is
   begin
      for J in Submatrix'Range (1) loop
         for K in Submatrix'Range (2) loop
            To (J, K) := Submatrix (J, K);
         end loop;
      end loop;
   end Assign;

end Block_Matrices;

with Ada.Text_IO; use Ada.Text_IO;
procedure Block_Matrices.Test
is

   procedure Print (M : Matrix) is
   begin
      for R in M'Range (1) loop
         for C in M'Range (2) loop
            Put (" " & M (R, C)'Image);
         end loop;
         New_Line;
      end loop;
   end Print;

   M : Matrix (1 .. 8, 1 .. 8);

begin

   for J in M'Range (1) loop
      for K in M'Range (2) loop
         M (J, K) := J * K;
      end loop;
   end loop;

   declare
      S : Matrix := Submatrix (M, 3, 5, 2, 3);
   begin
      Print (S);
      New_Line;
      for El of S loop
         El := - El;
      end loop;
      Assign (S, M);
      Print (M);
   end;

end Block_Matrices.Test;