lingenic_text-file_io

--  Copyright © 2026 Lingenic LLC. All rights reserved.
--  Licensed under the Lingenic Source-Available License v2.3.
--  Production use requires a separate license from Licensor.
--  See LICENSE.md and COPYRIGHT in the project root.
--

-------------------------------------------------------------------------------
--  Lingenic-Text — File I/O body
--
--  SPARK_Mode(Off): uses Ada.Streams.Stream_IO to read files.
--  This is the only unproved code in the library.
-------------------------------------------------------------------------------

with Ada.Streams.Stream_IO;

package body Lingenic_Text.File_IO
   with SPARK_Mode => Off
is

   procedure Read_File
     (Name    : String;
      Buffer  : out File_Byte_Array;
      Length  : out File_Size;
      Success : out Boolean)
   is
      use Ada.Streams.Stream_IO;
      use Ada.Streams;

      File : File_Type;
      Size : Stream_Element_Count;
   begin
      --  Zero buffer element-by-element to avoid stack temporaries
      for I in Buffer'Range loop
         Buffer (I) := 0;
      end loop;
      Length := 0;
      Success := False;

      begin
         Open (File, In_File, Name);
      exception
         when others =>
            return;
      end;

      Size := Stream_Element_Count (Ada.Streams.Stream_IO.Size (File));

      if Size > Stream_Element_Count (Max_File_Size) or Size = 0 then
         Close (File);
         return;
      end if;

      --  Read in chunks to avoid allocating a multi-megabyte
      --  Stream_Element_Array on the stack.
      declare
         Chunk_Size : constant := 8192;
         Chunk      : Stream_Element_Array (1 .. Chunk_Size);
         Last       : Stream_Element_Offset;
         Remaining  : Stream_Element_Count := Size;
         Buf_Pos    : Positive := 1;
      begin
         while Remaining > 0 loop
            declare
               Want : constant Stream_Element_Count :=
                 Stream_Element_Count'Min (Remaining, Chunk_Size);
            begin
               Read (Stream (File).all, Chunk (1 .. Want), Last);
               if Last < 1 then
                  Close (File);
                  return;
               end if;

               for I in 1 .. Last loop
                  Buffer (Buf_Pos) := Byte (Chunk (I));
                  Buf_Pos := Buf_Pos + 1;
               end loop;

               Remaining := Remaining - Last;
            end;
         end loop;

         Close (File);
         Length := File_Size (Size);
         Success := True;
      end;

   exception
      when others =>
         if Is_Open (File) then
            Close (File);
         end if;
         Length := 0;
         Success := False;
   end Read_File;

end Lingenic_Text.File_IO;