-------------------------------------------------------------------------------
-- (C) Altran Praxis Limited
-------------------------------------------------------------------------------
--
-- The SPARK toolset is free software; you can redistribute it and/or modify it
-- under terms of the GNU General Public License as published by the Free
-- Software Foundation; either version 3, or (at your option) any later
-- version. The SPARK toolset is distributed in the hope that it will be
-- useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
-- Public License for more details. You should have received a copy of the GNU
-- General Public License distributed with the SPARK toolset; see file
-- COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of
-- the license.
--
--=============================================================================

--------------------------------------------------------------------------------
--  SeqAlgebra
--
--  Implementation Details:
--
--  A Seq object represents a sequence or a set.
--  Seqs are implemented as linked lists of Heap.Atoms using the storage
--  facilities provided by package Heap.  A linked list is a good representation
--  for sequences but is a less than ideal but simple representation for
--  general sets.
--
--   An object which is a member of a Seq is type MemberOfSeq.  [Actually, they
--  are both simply numbers (Heap.Atoms), indexes of atoms on the
--  heap currently being used.]
--
--  The atoms of a Seq are allocated from the Heap package but only use the
--  "A" values and pointers of Heap.Atoms.  An "A" pointer P is the
--  index of the following member of the Seq, or is Heap.IsNullPointer (P)
--  to represent the end of the Seq.
--
--  Note: In the current implementation of Heap.IsNullPointer (P) <=> P = 0 and
--  there are instances where this implementation dependent equivalence is
--  used directly in the code.  Such implementation dependent code needs to be
--  factored out in future revisions.
--
--  A Seq object representing a sequence has an implied order and
--  may have elements with duplicate values, whereas a set has no implied
--  order and does not have elements with duplicate values.
--
--  To represent a set within a Seq object the members of a set are kept in
--  numerical order of the element value (lowest first).  This allows
--  detection of duplicate values and more efficient algorithms for the set
--  operations.
--  All is well if the operation Add member is used to add elements to a set as
--  the ordering is maintained. Use AppendAfter (intended for sequences)
--  and all bets are off.  The ordering will be destroyed and the set operations
--  will not work correctly.
--  Use the AppendAfter operation to add members to a sequence but not a set.
--------------------------------------------------------------------------------

package body SeqAlgebra is

   -------- Functions and operations for implementation of SeqAlgebra --------

   function Is_Null_Seq (S : Seq) return Boolean is
   begin
      return S = Null_Seq;
   end Is_Null_Seq;

   function IsNullMember (M : MemberOfSeq) return Boolean is
   begin
      return M.Member = 0;
   end IsNullMember;

   function FirstMember (TheHeap : Heap.HeapRecord;
                         S       : Seq) return MemberOfSeq is
   begin
      return MemberOfSeq'(Member  => Member_Range (Heap.APointer (TheHeap, Heap.Atom (S))),
                          The_Seq => S);
   end FirstMember;

   function NextMember (TheHeap : Heap.HeapRecord;
                        M       : MemberOfSeq) return MemberOfSeq is
   begin
      return MemberOfSeq'(Member  => Member_Range (Heap.APointer (TheHeap, Heap.Atom (M.Member))),
                          The_Seq => M.The_Seq);
   end NextMember;

   function Value_Of_Member (The_Heap : Heap.HeapRecord;
                             M        : MemberOfSeq) return Natural is
   begin
      return Heap.AValue (The_Heap, Heap.Atom (M.Member));
   end Value_Of_Member;

   -- Puts a marker atom (index S) onto TheHeap,
   -- with no members (A pointer is 0).
   procedure CreateSeq (TheHeap : in out Heap.HeapRecord;
                        S       :    out Seq) is
      A : Heap.Atom;
   begin
      Heap.CreateAtom (TheHeap, A);
      S := Seq (A);
   end CreateSeq;

   function AreEqual (TheHeap : Heap.HeapRecord;
                      S1, S2  : Seq) return Boolean is
      M1, M2 : MemberOfSeq;
      Result : Boolean;
   begin
      M1 := FirstMember (TheHeap, S1);
      M2 := FirstMember (TheHeap, S2);
      loop
         Result := IsNullMember (M1) and IsNullMember (M2);
         exit when Result; -- success, both lists finished at same time

         Result := not IsNullMember (M1);
         exit when not Result; -- fail case, first list finished before second

         Result := not IsNullMember (M2);
         exit when not Result; -- fail case, second list finished before first

         -- both list still have members, so compare them
         Result := Value_Of_Member (The_Heap => TheHeap,
                                    M        => M1) = Value_Of_Member (The_Heap => TheHeap,
                                                                       M        => M2);
         exit when not Result; --fail case, two different members found

         -- OK so far, still have values and equal so far, so compare next
         M1 := NextMember (TheHeap, M1);
         M2 := NextMember (TheHeap, M2);
      end loop;
      return Result;
   end AreEqual;

   function Length (TheHeap : Heap.HeapRecord;
                    S       : Seq) return Natural is
      Result : Natural := 0;
      M      : MemberOfSeq;
   begin
      M := FirstMember (TheHeap, S);
      while not IsNullMember (M) loop
         Result := Result + 1;
         M      := NextMember (TheHeap, M);
      end loop;
      return Result;
   end Length;

   function IsEmptySeq (TheHeap : Heap.HeapRecord;
                        S       : Seq) return Boolean is
   begin
      return IsNullMember (FirstMember (TheHeap, S));
   end IsEmptySeq;

   -- Frees all the atoms on the heap relating to
   --  sequence S.
   procedure DisposeOfSeq (TheHeap : in out Heap.HeapRecord;
                           S       : in     Seq) is
      M, N : MemberOfSeq;
   begin
      M := FirstMember (TheHeap, S);
      while not IsNullMember (M) loop
         N := NextMember (TheHeap, M);
         Heap.DisposeOfAtom (TheHeap, Heap.Atom (M.Member));
         M := N;
      end loop;
      Heap.DisposeOfAtom (TheHeap, Heap.Atom (S));
   end DisposeOfSeq;

   ---type conversion functions used in RefList------------

   function SeqToNatural (S : Seq) return Natural is
   begin
      return Natural (S);
   end SeqToNatural;

   function NaturalToSeq (N : Natural) return Seq is
   begin
      return Seq (N);
   end NaturalToSeq;

   -------- Functions and operations intended for sequences --------

   function BeforeFirstMember (S : Seq) return MemberOfSeq is
   begin
      return MemberOfSeq'(Member  => Member_Range (S),
                          The_Seq => S);
   end BeforeFirstMember;

   --  Note if this is used with a Seq representing a set this will
   --  destroy the numerical ordering of the set.
   procedure AppendAfter (TheHeap    : in out Heap.HeapRecord;
                          M          : in out MemberOfSeq;
                          GivenValue : in     Natural) is
      LastAtom, NewAtom : Heap.Atom;
   begin
      LastAtom := Heap.Atom (M.Member);
      Heap.CreateAtom (TheHeap, NewAtom);
      Heap.UpdateAValue (TheHeap, NewAtom, GivenValue);
      Heap.UpdateAPointer (TheHeap, NewAtom, Heap.APointer (TheHeap, LastAtom));
      Heap.UpdateAPointer (TheHeap, LastAtom, NewAtom);
      M.Member := Member_Range (NewAtom);
   end AppendAfter;

   --  Note frees the eliminated member from the heap
   procedure EliminateAfter (TheHeap : in out Heap.HeapRecord;
                             M       : in     MemberOfSeq) is
      LastAtom, OldAtom : Heap.Atom;
   begin
      LastAtom := Heap.Atom (M.Member);
      OldAtom  := Heap.APointer (TheHeap, LastAtom);
      Heap.UpdateAPointer (TheHeap, LastAtom, Heap.APointer (TheHeap, OldAtom));
      Heap.DisposeOfAtom (TheHeap, OldAtom);
   end EliminateAfter;

   -------- Functions and operations intended for sets ----------

   -- This operation uses the numerical ordering of a set.
   -- It might not find an element from a sequence even if the element exists.
   function IsMember
     (TheHeap    : Heap.HeapRecord;
      S          : Seq;
      GivenValue : Natural)
     return       Boolean
   is
      MemberPresent : Boolean;
      N             : MemberOfSeq;
      ValueOfN      : Natural;
   begin
      MemberPresent := False;
      N             := FirstMember (TheHeap, S);
      loop
         exit when IsNullMember (N);
         ValueOfN := Value_Of_Member (The_Heap => TheHeap,
                                      M        => N);
         if ValueOfN = GivenValue then
            MemberPresent := True;
         end if;
         exit when ValueOfN >= GivenValue;
         N := NextMember (TheHeap, N);
      end loop;
      return MemberPresent;
   end IsMember;

   -- Preserves the numerical ordering of the set.
   -- Do not use with a Seq representing a sequence it may
   -- destroy the sequence order.
   procedure AddMember (TheHeap    : in out Heap.HeapRecord;
                        S          : in     Seq;
                        GivenValue : in     Natural) is
      MemberPresent : Boolean;
      M, N          : MemberOfSeq;
      ValueOfN      : Natural;
   begin
      MemberPresent := False;
      M             := BeforeFirstMember (S);
      N             := FirstMember (TheHeap, S);
      loop
         exit when IsNullMember (N);
         ValueOfN := Value_Of_Member (The_Heap => TheHeap,
                                      M        => N);
         if ValueOfN = GivenValue then
            MemberPresent := True;
         end if;
         exit when ValueOfN >= GivenValue;
         M := N;
         N := NextMember (TheHeap, N);
      end loop;
      if not MemberPresent then
         -- we don't need the updated value of M in this case
         --# accept F, 10, M, "M unused here";
         AppendAfter (TheHeap, M, GivenValue);
         --# end accept;
      end if;
   end AddMember;

   -- This operation uses the numerical ordering of a set.
   -- It might not remove an element from a sequence even if the element exists.
   procedure RemoveMember (TheHeap    : in out Heap.HeapRecord;
                           S          : in     Seq;
                           GivenValue : in     Natural) is
      MemberPresent : Boolean;
      M, N          : MemberOfSeq;
      ValueOfN      : Natural;
   begin
      MemberPresent := False;
      M             := BeforeFirstMember (S);
      N             := FirstMember (TheHeap, S);
      loop
         exit when IsNullMember (N);
         ValueOfN := Value_Of_Member (The_Heap => TheHeap,
                                      M        => N);
         if ValueOfN = GivenValue then
            MemberPresent := True;
         end if;
         exit when ValueOfN >= GivenValue;
         M := N;
         N := NextMember (TheHeap, N);
      end loop;
      if MemberPresent then
         EliminateAfter (TheHeap, M);
      end if;
   end RemoveMember;

   -- Note this operation is intended for Seq objects representing sets.
   -- It currently also works for sequences because the comparison is commented out.
   -- The usefulness of the value returned is questionable
   -- because it will be the same if the last member has the given value
   -- or if no members match the given value.  It would be better if 0 was
   -- returned if no match is found.
   function MemberIndex
     (TheHeap    : Heap.HeapRecord;
      S          : Seq;
      GivenValue : Natural)
     return       Natural
   is
      N        : MemberOfSeq;
      ValueOfN : Natural;
      Index    : Natural;
   begin
      Index := 0;
      N     := FirstMember (TheHeap, S);
      loop
         exit when IsNullMember (N);
         ValueOfN := Value_Of_Member (The_Heap => TheHeap,
                                      M        => N);
         -- What should the value of index be if the GivenValue is not in the Seq
         --      exit when ValueOfN >= GivenValue;
         Index := Index + 1;
         exit when ValueOfN = GivenValue;
         N := NextMember (TheHeap, N);
      end loop;
      return Index;
   end MemberIndex;

   ----------- Set Operations on Seq representing Sets -----------

   --  Assumes A and B are in numerical order, i.e. a set, in which case
   --  C will be set too.
   --  The operation is meaningless for a Seq representing a sequence.
   procedure Union (TheHeap : in out Heap.HeapRecord;
                    A, B    : in     Seq;
                    C       :    out Seq) is
      LocalC             : Seq;
      M, N               : MemberOfSeq;
      ValueofM, ValueofN : Natural;
      LastC              : MemberOfSeq;
   begin
      CreateSeq (TheHeap, LocalC);
      LastC := BeforeFirstMember (LocalC);
      M     := FirstMember (TheHeap, A);
      N     := FirstMember (TheHeap, B);
      loop
         exit when IsNullMember (M) or IsNullMember (N);
         ValueofM := Value_Of_Member (The_Heap => TheHeap,
                                      M        => M);
         ValueofN := Value_Of_Member (The_Heap => TheHeap,
                                      M        => N);
         if ValueofM = ValueofN then
            AppendAfter (TheHeap, LastC, ValueofM);
            M := NextMember (TheHeap, M);
            N := NextMember (TheHeap, N);
         elsif ValueofM < ValueofN then
            AppendAfter (TheHeap, LastC, ValueofM);
            M := NextMember (TheHeap, M);
         else
            AppendAfter (TheHeap, LastC, ValueofN);
            N := NextMember (TheHeap, N);
         end if;
      end loop;
      loop
         exit when IsNullMember (M);
         AppendAfter (TheHeap, LastC, Value_Of_Member (The_Heap => TheHeap,
                                                       M        => M));
         M := NextMember (TheHeap, M);
      end loop;
      loop
         exit when IsNullMember (N);
         AppendAfter (TheHeap, LastC, Value_Of_Member (The_Heap => TheHeap,
                                                       M        => N));
         N := NextMember (TheHeap, N);
      end loop;
      C := LocalC;
   end Union;

   -- This operation uses the numerical ordering of a set.
   --  The operation is meaningless for a Seq representing a sequence.
   procedure AugmentSeq (TheHeap : in out Heap.HeapRecord;
                         A, B    : in     Seq) is
      M, N               : MemberOfSeq;
      ValueofM, ValueofN : Natural;
      LastM              : MemberOfSeq;
   begin
      M     := FirstMember (TheHeap, A);
      LastM := BeforeFirstMember (A);
      N     := FirstMember (TheHeap, B);
      loop
         exit when IsNullMember (M) or IsNullMember (N);
         ValueofM := Value_Of_Member (The_Heap => TheHeap,
                                      M        => M);
         ValueofN := Value_Of_Member (The_Heap => TheHeap,
                                      M        => N);
         if ValueofM = ValueofN then
            LastM := M;
            M     := NextMember (TheHeap, M);
            N     := NextMember (TheHeap, N);
         elsif ValueofM < ValueofN then
            LastM := M;
            M     := NextMember (TheHeap, M);
         else
            AppendAfter (TheHeap, LastM, ValueofN);
            N := NextMember (TheHeap, N);
         end if;
      end loop;
      loop
         exit when IsNullMember (N);
         AppendAfter (TheHeap, LastM, Value_Of_Member (The_Heap => TheHeap,
                                                       M        => N));
         N := NextMember (TheHeap, N);
      end loop;
   end AugmentSeq;

   -- This operation uses the numerical ordering of a set.
   -- C is created as a new Seq on TheHeap.
   -- The operation is meaningless for a Seq representing a sequence.
   procedure Intersection (TheHeap : in out Heap.HeapRecord;
                           A, B    : in     Seq;
                           C       :    out Seq) is
      LocalC             : Seq;
      LastC              : MemberOfSeq;
      M, N               : MemberOfSeq;
      ValueOfM, ValueOfN : Natural;
   begin
      CreateSeq (TheHeap, LocalC);
      LastC := BeforeFirstMember (LocalC);
      M     := FirstMember (TheHeap, A);
      N     := FirstMember (TheHeap, B);
      loop
         exit when IsNullMember (M) or IsNullMember (N);
         ValueOfM := Value_Of_Member (The_Heap => TheHeap,
                                      M        => M);
         ValueOfN := Value_Of_Member (The_Heap => TheHeap,
                                      M        => N);
         if ValueOfM < ValueOfN then
            M := NextMember (TheHeap, M);
         elsif ValueOfM > ValueOfN then
            N := NextMember (TheHeap, N);
         else
            AppendAfter (TheHeap, LastC, ValueOfM);
            M := NextMember (TheHeap, M);
            N := NextMember (TheHeap, N);
         end if;
      end loop;
      C := LocalC;
   end Intersection;

   -- This operation uses the numerical ordering of a set.
   -- C is created as a new Seq on TheHeap.
   -- The operation is meaningless for a Seq representing a sequence.
   procedure Complement (TheHeap : in out Heap.HeapRecord;
                         A, B    : in     Seq;
                         C       :    out Seq) is
      LocalC             : Seq;
      M, N               : MemberOfSeq;
      ValueOfM, ValueOfN : Natural;
      LastC              : MemberOfSeq;
   begin
      CreateSeq (TheHeap, LocalC);
      LastC := BeforeFirstMember (LocalC);
      M     := FirstMember (TheHeap, A);
      N     := FirstMember (TheHeap, B);
      loop
         exit when IsNullMember (M) or IsNullMember (N);
         ValueOfM := Value_Of_Member (The_Heap => TheHeap,
                                      M        => M);
         ValueOfN := Value_Of_Member (The_Heap => TheHeap,
                                      M        => N);
         if ValueOfM = ValueOfN then
            M := NextMember (TheHeap, M);
            N := NextMember (TheHeap, N);
         elsif ValueOfM < ValueOfN then
            AppendAfter (TheHeap, LastC, ValueOfM);
            M := NextMember (TheHeap, M);
         else
            N := NextMember (TheHeap, N);
         end if;
      end loop;
      loop
         exit when IsNullMember (M);
         AppendAfter (TheHeap, LastC, Value_Of_Member (The_Heap => TheHeap,
                                                       M        => M));
         M := NextMember (TheHeap, M);
      end loop;
      C := LocalC;
   end Complement;

   -- This operation uses the numerical ordering of a set.
   -- The operation is meaningless for a Seq representing a sequence.
   procedure Reduction (TheHeap : in out Heap.HeapRecord;
                        A, B    : in     Seq) is
      M, N               : MemberOfSeq;
      ValueOfM, ValueOfN : Natural;
      LastM              : MemberOfSeq;
   begin
      M     := FirstMember (TheHeap, A);
      LastM := BeforeFirstMember (A);
      N     := FirstMember (TheHeap, B);
      loop
         exit when IsNullMember (M) or IsNullMember (N);
         ValueOfM := Value_Of_Member (The_Heap => TheHeap,
                                      M        => M);
         ValueOfN := Value_Of_Member (The_Heap => TheHeap,
                                      M        => N);
         if ValueOfM = ValueOfN then
            M := NextMember (TheHeap, M);
            N := NextMember (TheHeap, N);
            EliminateAfter (TheHeap, LastM);
         elsif ValueOfM < ValueOfN then
            LastM := M;
            M     := NextMember (TheHeap, M);
         else
            N := NextMember (TheHeap, N);
         end if;
      end loop;
   end Reduction;

   function To_Atom (M : MemberOfSeq) return Heap.Atom is
   begin
      return Heap.Atom (M.Member);
   end To_Atom;

end SeqAlgebra;