-------------------------------------------------------------------------------
-- (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.
--
--=============================================================================

with Ada.Command_Line, GNAT.OS_Lib, GNAT.IO_Aux, SPARK_IO;
use type SPARK_IO.File_Type;
use type SPARK_IO.File_Status;

--  Key layout concerns are summarised below:
-- --------------------------------------------------------------------
--  Column number:
--  123456789...
--
--                        The column beoynd which wrapping is desired>M
--                                                                    M
--                             V--split Characters-V----------V       M
--  SSSSSSSSSSSXXXXXXXXXXXXXXXXCXXXXXXXXXXXXXXXXXXXCXXXXXXXXXXXCYYYYYYYZZZZZZZZ...
--  ^Possible  ^Text for this line                             ^      M ^
--   start                           Text cut off for next line|      M Text
--   offset                                                           M beyond
--
-- --------------------
--  Note that, wrapped lines are prefixed with an indent. This is achieved by
--  modifying the text to include non-breaking space Characters.
-- --------------------------------------------------------------------
--
--  Key layout rules are summarised below:
--
--  The line fits:
--  Condition: start+line lies within the wrapping point.
--  Action: write out the line and finish. (Never insert a newline here.
--          Newlines are only added for wrapping purposes.)
--
--  The line does not fit:
--  Condition: Above condition is false.
--  Action: Compare start point and wrapping column.
--
--  Condition: The start point is beyond the wrapping column.
--  Action: Scan remaining text forwards until a split Character (that is not
--          the last Character!) is encountered.  Write out line up to and
--          including the split Character, and a newline. Collect remaining
--          line, and start again. An indent is now requested.
--          If a split Character is never found (or it's only found at the
--          last Character), write out the whole line and finish.
--
--  Condition: The start point is within the wrapping column.
--  Action: Scan backwards from the wrapping column. If a split Character is
--          encountered (that is not the first Character!), then write out the line
--          up to and including the split Character, and a newline.  Collect
--          remaining line, and start again. An indent is now requested.  If a split
--          Character is never found (or it's only found at the first Character),
--          write out the whole line, set offset to just after the wrapper column,
--          and start again.
--
-- Note: If the last line terminates with a new line, then the above rules hold.
-- If the last line does not terminate with a new line, then the above rules hold,
-- with an additional new line being added just before the end of the file.

package body WRAPS is

   -- CONSTANTS --
   maxlinelength    : constant Integer := 262143; -- 2**18 - 1 or 256k
   MaxCols          : constant Integer := 80;   -- Maximum no. of output columns normally permitted
   Indentation      : constant Integer := 10;   -- Columns to indent for 2nd. & subsequent wraps
   SpaceChar        : constant Integer := 32;   -- ' ' {assumption: ASCII, so space is chr(32)}
   OpenParenthesis  : constant Integer := 40;   -- '('
   CloseParenthesis : constant Integer := 41;   -- ')'
   OpenBracket      : constant Integer := 91;   -- '['
   CloseBracket     : constant Integer := 93;   -- ']'

   -- TYPES --
   type linelength is range 0 .. maxlinelength;
   subtype linearraypos is linelength range 1 .. linelength'Last;
   subtype charcode is Integer range 0 .. 255;   --assumption: ASCII range 0..255
   type linearray is array (linearraypos) of charcode;
   type line is record
      contents : linearray;
      length   : linelength;
   end record;  -- line

   procedure WRAP is
      infile, outfile : SPARK_IO.File_Type;
      STATUS          : SPARK_IO.File_Status;

      procedure DoRead (CH : out charcode)
      --# global in     infile;
      --#        in out SPARK_IO.File_Sys;
      --# derives CH,
      --#         SPARK_IO.File_Sys from infile,
      --#                                SPARK_IO.File_Sys;
      is
         C : Character;
      begin
         SPARK_IO.Get_Char (infile, C);
         CH := Character'Pos (C);
      end DoRead;

      procedure DoWrite (CH : in charcode)
      --# global in     outfile;
      --#        in out SPARK_IO.File_Sys;
      --# derives SPARK_IO.File_Sys from *,
      --#                                CH,
      --#                                outfile;
      is
      begin
         SPARK_IO.Put_Char (outfile, Character'Val (CH));
      end DoWrite;

      procedure DoReadln
      --# global in     infile;
      --#        in out SPARK_IO.File_Sys;
      --# derives SPARK_IO.File_Sys from *,
      --#                                infile;
      is
      begin
         SPARK_IO.Skip_Line (infile, 1);
      end DoReadln;

      procedure DoWriteln
      --# global in     outfile;
      --#        in out SPARK_IO.File_Sys;
      --# derives SPARK_IO.File_Sys from *,
      --#                                outfile;
      is
      begin
         SPARK_IO.New_Line (outfile, 1);
      end DoWriteln;

      function CheckFileExists (Name : String) return Boolean
      -- checks that we're not trying to open a non-existent file
      is
         --# hide CheckFileExists;
      begin
         return GNAT.IO_Aux.File_Exists (Name);
      end CheckFileExists;

      -- True if we were called with a filename argument
      function New_Wrap return Boolean is
         --# hide New_Wrap;
      begin
         return Ada.Command_Line.Argument_Count > 0;
      end New_Wrap;

      -- Return the input file.
      -- This will be either the first argument, or "WRAPS.IN" if there is no
      -- argument.
      function OpenInFile return  SPARK_IO.File_Type is
         --# hide OpenInFile;
         filename   : GNAT.OS_Lib.String_Access := new String'("WRAP.INP");
         filehandle : SPARK_IO.File_Type;
         STATUS     : SPARK_IO.File_Status;
      begin
         if New_Wrap then
            filename := new String'(Ada.Command_Line.Argument (1));
         end if;
         if CheckFileExists (filename.all) then
            SPARK_IO.Open (filehandle, SPARK_IO.In_File, filename'Length, filename.all, "", STATUS);

            if STATUS /= SPARK_IO.Ok then
               SPARK_IO.Put_Line (SPARK_IO.Standard_Output, "Open input failed with: " & SPARK_IO.File_Status'Image (STATUS), 0);
            end if;
         else
            filehandle := SPARK_IO.Null_File;
         end if;
         return filehandle;
      end OpenInFile;

      -- Return the output file.
      -- This will be either the first argument and ".tmp", or "WRAPS.OUT" if there is no
      -- argument.
      function OpenOutFile return  SPARK_IO.File_Type is
         --# hide OpenOutFile;
         filename   : GNAT.OS_Lib.String_Access := new String'("WRAP.OUT");
         filehandle : SPARK_IO.File_Type;
         STATUS     : SPARK_IO.File_Status;
      begin
         if New_Wrap then
            filename := new String'(Ada.Command_Line.Argument (1) & ".tmp");
         end if;

         SPARK_IO.Create (filehandle, filename'Length, filename.all, "", STATUS);
         if STATUS /= SPARK_IO.Ok then
            SPARK_IO.Put_Line (SPARK_IO.Standard_Output, "Create output failed with: " & SPARK_IO.File_Status'Image (STATUS), 0);
         end if;
         if filehandle = SPARK_IO.Null_File then
            SPARK_IO.Put_Line (SPARK_IO.Standard_Output, "Create output return Null_File", 0);
         end if;
         return filehandle;
      end OpenOutFile;

      procedure Initialise
      --# global out infile;
      --#        out outfile;
      --# derives infile,
      --#         outfile from ;
      is
      begin
         infile := OpenInFile;
         --# accept Flow, 22, "OpenInFile is hidden. Expression may actually change.";
         if infile = SPARK_IO.Null_File then
            --# end accept;
            outfile := SPARK_IO.Null_File;
         else
            outfile := OpenOutFile;
         end if;
      end Initialise;

      -- Delete the original file and rename the temporary file.
      procedure CleanUp
      --# derives ;
      is
         --# hide CleanUp;
         SUCCESS      : Boolean := False;
         infile_name  : GNAT.OS_Lib.String_Access;
         outfile_name : GNAT.OS_Lib.String_Access;
         newfile_name : GNAT.OS_Lib.String_Access;
      begin
         if New_Wrap then -- We have arguments

            infile_name  := new String'(Ada.Command_Line.Argument (1));
            outfile_name := new String'(Ada.Command_Line.Argument (1) & ".tmp");

            if Ada.Command_Line.Argument_Count = 2 then -- We have a destination filename
               newfile_name := new String'(Ada.Command_Line.Argument (2));
            else -- Replace the original file
               newfile_name := new String'(Ada.Command_Line.Argument (1));
            end if;

            -- Delete the original input file.
            GNAT.OS_Lib.Delete_File (infile_name.all, SUCCESS);

            if not SUCCESS then
               SPARK_IO.New_Line (SPARK_IO.Standard_Output, 1);
               SPARK_IO.Put_Line
                 (SPARK_IO.Standard_Output,
                  "*** ERROR - wrap_utility failed to delete input file failed with Errno=" & Integer'Image (GNAT.OS_Lib.Errno),
                  0);
               SPARK_IO.New_Line (SPARK_IO.Standard_Output, 1);
            end if;

            -- Move the output file to the destination name.
            GNAT.OS_Lib.Rename_File (outfile_name.all, newfile_name.all, SUCCESS);

            if not SUCCESS then
               SPARK_IO.New_Line (SPARK_IO.Standard_Output, 1);
               SPARK_IO.Put_Line (SPARK_IO.Standard_Output, "*** ERROR - wrap_utility failed to rename output file", 0);
               SPARK_IO.New_Line (SPARK_IO.Standard_Output, 1);
            end if;
         else
            null; -- We are behaving as the old wrap util, so do nothing.
         end if; -- New_Wrap
      end CleanUp;

      --------------------------------------------------------------------------------

      procedure ReadLine (L : out line)
      --# global in     infile;
      --#        in out SPARK_IO.File_Sys;
      --# derives L,
      --#         SPARK_IO.File_Sys from infile,
      --#                                SPARK_IO.File_Sys;
      --This routine reads a line of Character-codes into the line-buffer L.
      is
         CH       : charcode;
         lensofar : linelength;
      begin
         lensofar := 0;
         while not SPARK_IO.End_Of_Line (infile) and lensofar < linelength (maxlinelength) loop
            lensofar := lensofar + 1;
            DoRead (CH);
            --# accept Flow, 23, L.contents, "Array elements are initialised before use.";
            L.contents (lensofar) := CH;
            --# end accept;
         end loop;
         L.length := lensofar;
         DoReadln;

         --# accept Flow, 602, L, L.contents, "Array elements are initialised before use.";
      end ReadLine;

      procedure OutPartOfLine (L              : in line;
                               FromCol, ToCol : in linelength)
      --# global in     outfile;
      --#        in out SPARK_IO.File_Sys;
      --# derives SPARK_IO.File_Sys from *,
      --#                                FromCol,
      --#                                L,
      --#                                outfile,
      --#                                ToCol;
      --Writes out line-buffer L unchanged, without adding any single quotes.
      is
         index : linelength;
      begin
         index := FromCol;
         while index <= ToCol loop
            DoWrite (L.contents (index));
            index := index + 1;
         end loop;
      end OutPartOfLine;

      procedure OutUnchangedLine (L : in line)
      --# global in     outfile;
      --#        in out SPARK_IO.File_Sys;
      --# derives SPARK_IO.File_Sys from *,
      --#                                L,
      --#                                outfile;
      --Writes out line-buffer L unchanged, without any line-wrapping.
      is
      begin
         OutPartOfLine (L, 1, L.length);
         DoWriteln;
      end OutUnchangedLine;

      --Copies a line, wrapping if it appears to be necessary.
      procedure CopyAndMaybeWrapLine
      --# global in     infile;
      --#        in     outfile;
      --#        in out SPARK_IO.File_Sys;
      --# derives SPARK_IO.File_Sys from *,
      --#                                infile,
      --#                                outfile;
      is
         currentline : line;

         function IsALongLine (L : in line) return Boolean
         --True if we need to wrap the line around - i.e. more than MaxCols.
         is
         begin
            return L.length > linelength (MaxCols);
         end IsALongLine;

         --Write out line-buffer L, wrapping where necessary.
         procedure OutWrappedLine (L : in line)
         --# global in     outfile;
         --#        in out SPARK_IO.File_Sys;
         --# derives SPARK_IO.File_Sys from *,
         --#                                L,
         --#                                outfile;
         is
            OnCol, Width : linelength;

            procedure OutNextPartOfLine (L       : in     line;
                                         FromCol : in out linelength;
                                         InWidth : in     linelength)
            --# global in     outfile;
            --#        in out SPARK_IO.File_Sys;
            --# derives FromCol           from *,
            --#                                InWidth,
            --#                                L &
            --#         SPARK_IO.File_Sys from *,
            --#                                FromCol,
            --#                                InWidth,
            --#                                L,
            --#                                outfile;
            -- pre FromCol + InWidth <= L.length and InWidth > 1;
            is
               ToCol : linelength;

               function OKSplitChar (C : in charcode) return Boolean
               --Returns true if C is a space, parenthesis or bracket.
               is
               begin
                  return (C = SpaceChar)
                    or else (C = OpenParenthesis)
                    or else (C = CloseParenthesis)
                    or else (C = OpenBracket)
                    or else (C = CloseBracket);
               end OKSplitChar;

            begin --OutNextPartOfLine

               -- L:       The line under consideration.
               -- FromCol: Index the first portion of L that not has already been displayed.
               -- InWidth: The remaining width of the screen before MaxCols is reached.

               -- ToCol: Index the last portion of L to be displayed on this
               -- line. The correct value is calculated below.

               -- Assume that the line fits perfectly.
               ToCol := (FromCol + InWidth) - 1;

               if not OKSplitChar (L.contents (ToCol)) then
                  -- Cannot split at the ideal position.

                  -- Search backwards to find the next-best split point.
                  loop
                     ToCol := ToCol - 1;
                     exit when OKSplitChar (L.contents (ToCol)) or else (ToCol = FromCol);
                  end loop;

                  if ToCol = FromCol then
                     -- Could not find any split point looking backwards. The
                     -- line will need to wrap beyond MaxCols.

                     -- Search forwards to find the least-worst split point.
                     ToCol := (FromCol + InWidth) - 1;
                     loop
                        exit when (ToCol >= L.length) or else OKSplitChar (L.contents (ToCol));
                        ToCol := ToCol + 1;
                     end loop;
                  end if;
               end if;

               -- Display the selected portion of the line.
               OutPartOfLine (L, FromCol, ToCol);

               -- The index to first portion of L that not has already been displayed
               -- is adjusted accordingly.
               FromCol := ToCol + 1;
            end OutNextPartOfLine;

            procedure Indent (NoOfCols : in linelength)
            --# global in     outfile;
            --#        in out SPARK_IO.File_Sys;
            --# derives SPARK_IO.File_Sys from *,
            --#                                NoOfCols,
            --#                                outfile;
            -- pre NoOfCols >= 0;
            is
            begin
               for index in linelength range 1 .. NoOfCols loop
                  DoWrite (SpaceChar);
               end loop;
            end Indent;

         begin--OutWrappedLine

            --Start at column 1.
            OnCol := 1;

            -- To start with, have the width of the screen in which to place content.
            Width := linelength (MaxCols);

            while OnCol + Width <= L.length loop

               OutNextPartOfLine (L, OnCol, Width);

               -- Wrap and indent, only if there is more text to display for this line.
               if OnCol <= L.length then
                  DoWriteln;
                  Indent (linelength (Indentation));
               end if;

               -- Now, have the width of the screen (less indent) in which to place content.
               Width := linelength (MaxCols - Indentation);
            end loop;

            -- Display any residue.
            if OnCol <= L.length then
               OutPartOfLine (L, OnCol, L.length);
            end if;

            -- All done. Add final newline.
            DoWriteln;
         end OutWrappedLine;

      begin--CopyAndMaybeWrapLine
         ReadLine (currentline);
         if IsALongLine (currentline) then
            OutWrappedLine (currentline);
         else
            OutUnchangedLine (currentline);
         end if;
      end CopyAndMaybeWrapLine;

      procedure DisplayErrorMessage (Leader :    String;
                                     STATUS : in SPARK_IO.File_Status)
      --# global in out SPARK_IO.File_Sys;
      --# derives SPARK_IO.File_Sys from *,
      --#                                Leader,
      --#                                STATUS;
      is
         --# hide DisplayErrorMessage ;
      begin
         SPARK_IO.Put_Line (SPARK_IO.Standard_Output, (Leader & SPARK_IO.File_Status'Image (STATUS)), 0);
      end DisplayErrorMessage;

   begin -- WRAP

      --  GetFileNames;
      Initialise;

      --# accept Flow, 22, "Initialise hides behaviour. Expression may actually change.";
      if infile /= SPARK_IO.Null_File then
         --# end accept;

         -- Please note that End_Of_File (infile) will report true where:
         -- The next Character is: EOF
         -- The next Character sequence is: NL, EOF

         while not SPARK_IO.End_Of_File (infile) loop
            CopyAndMaybeWrapLine;
         end loop;
         -- This call to DoWriteln would appear to be totally unnecessary. However, it would
         -- correctly restore a NL if End_Of_File has really detected: NL, EOF. (Of course,
         -- it also adds an additional NL if End_Of_File actually detected: EOF.)
         DoWriteln;
         --# accept Flow, 10, infile, "May actually affect infile.";
         SPARK_IO.Close (infile, STATUS);
         --# end accept;

         if STATUS /= SPARK_IO.Ok then
            DisplayErrorMessage ("Close  In_File: ", STATUS);
         end if;

         --# accept Flow, 10, outfile, "May actually affect outfile.";
         SPARK_IO.Close (outfile, STATUS);
         --# end accept;

         if STATUS /= SPARK_IO.Ok then
            DisplayErrorMessage ("Close Out_File: ", STATUS);
         end if;

         CleanUp;
      end if;
   end WRAP;

end WRAPS;