------------------------------------------------------------------------------
--  Copyright (C) 2020 by Heisenbug Ltd. (gh+spat@heisenbug.eu)
--
--  This work is free. You can redistribute it and/or modify it under the
--  terms of the Do What The Fuck You Want To Public License, Version 2,
--  as published by Sam Hocevar. See the LICENSE file for more details.
------------------------------------------------------------------------------
pragma License (Unrestricted);

------------------------------------------------------------------------------
--
--  SPARK Proof Analysis Tool
--
--  S.P.A.T. - Read .spark files
--
--  Collect file contents.
--
--  Please note that Read is parallelized and uses background threads, hence
--  you need to call Shutdown once you're done, otherwise the application will
--  hang.
--
------------------------------------------------------------------------------

limited with Ada.Containers.Hashed_Maps;
limited with SPAT.Strings;

package SPAT.Spark_Files is

   --  .spark files are stored in a Hash map with the file name as key and the
   --  JSON reading result as value.
   package File_Maps is new Ada.Containers.Hashed_Maps
     (Key_Type        => SPARK_File_Name,
      Element_Type    => GNATCOLL.JSON.Read_Result,
      Hash            => Hash,
      Equivalent_Keys => "=",
      "="             => GNATCOLL.JSON."=");

   --
   --  Some renames for commonly used File_Maps.Cursor operations.
   --
   No_Element : File_Maps.Cursor renames File_Maps.No_Element;
   subtype Cursor is File_Maps.Cursor;

   ---------------------------------------------------------------------------
   --  Key
   ---------------------------------------------------------------------------
   function Key (C : in Cursor) return SPARK_File_Name renames File_Maps.Key;

   --
   --  Data collection and operations defined on it.
   --

   type T is new File_Maps.Map with private;
   --  Stores all data collected from SPARK files for analysis.

   ---------------------------------------------------------------------------
   --  Read
   ---------------------------------------------------------------------------
   not overriding
   procedure Read (This  : in out T;
                   Names : in     Strings.SPARK_File_Names);
   --  Reads the list of files, and parses and stores their content in This.

   ---------------------------------------------------------------------------
   --  Num_Workers
   --
   --  Report the number of tasks used for parallel file reads.
   ---------------------------------------------------------------------------
   function Num_Workers return Positive;

   ---------------------------------------------------------------------------
   --  Shutdown
   --
   --  Terminates all worker tasks.
   ---------------------------------------------------------------------------
   procedure Shutdown;

private

   type T is new File_Maps.Map with null record;

end SPAT.Spark_Files;