------------------------------------------------------------------------------
--                                                                          --
--                           OCARINA COMPONENTS                             --
--                                                                          --
--              O C A R I N A . C H E C K E R . Q U E R I E S               --
--                                                                          --
--                                 S p e c                                  --
--                                                                          --
--                 Copyright (C) 2007, GET-Telecom Paris.                   --
--                                                                          --
-- Ocarina  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 2, or (at your option) any      --
-- later version. Ocarina 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 Ocarina; see file COPYING.   --
-- If not, write to the Free Software Foundation, 51 Franklin Street, Fifth --
-- Floor, Boston, MA 02111-1301, USA.                                       --
--                                                                          --
-- As a special exception,  if other files  instantiate  generics from this --
-- unit, or you link  this unit with other files  to produce an executable, --
-- this  unit  does not  by itself cause  the resulting  executable to be   --
-- covered  by the  GNU  General  Public  License. This exception does not  --
-- however invalidate  any other reasons why the executable file might be   --
-- covered by the GNU Public License.                                       --
--                                                                          --
--                 Ocarina is maintained by the Ocarina team                --
--                       (ocarina-users@listes.enst.fr)                     --
--                                                                          --
------------------------------------------------------------------------------

--  This package contains definition and manipulation subprograms for
--  instances set, in order to perform property adequacy verification.

with Types;

package Ocarina.Checker.Queries is

   type Result_Set is private;
   --  A Result set, on which all elementary set operation
   --  will be defined.

   type Instance_Type is
     (C_Data,
      C_Subprogram,
      C_Subprogram_Call,
      C_Sequence_Call,
      C_Thread,
      C_Threadgroup,
      C_Process,
      C_Memory,
      C_Processor,
      C_Bus,
      C_Connection,
      C_Device,
      C_System,
      C_Unknown);

   type Predicates_Search_Options is
     (PSO_Direct,      --  Non-recursive search
      PSO_Recursive);  --  Recursive search

   --  Set builder procedures

   function Get_Instances_Of_Component_Type
     (Component_T : Instance_Type)
     return Result_Set;
   --  Search in the Node table for instances a given type

   function Get_Instances_Of_Component_Type
     (E : Types.Node_Id)
     return Result_Set;
   --  Search in the Node table for instances a given type

   function Get_Instances_With_Property
     (Set           : Result_Set;
      Property_Name : String)
     return Result_Set;
   --  Search in the given set for instnces with the
   --  property_name property

   --  Set manipulation procedures

   function Union
     (Set_1    : Result_Set;
      Set_2    : Result_Set;
      Distinct : Boolean := False)
     return Result_Set;
   --  Returns all distincts elements of set_1 and set_2
   --  If an element is present in the intersection, it
   --  will be present only one time in the result_set if
   --  'distinct' is set to true, two times otherwise.

   function Intersection
     (Set_1  : Result_Set;
      Set_2  : Result_Set)
     return Result_Set;
   --  Returns all elements that are in both of set_1 and set_2
   --  each element is present only one time in the result_set.

   function Exclusion
     (Set_1  : Result_Set;
      Set_2  : Result_Set)
     return Result_Set;
   --  Returns all elements that are in set_1 and NOT in set_2

   function Includes
     (Set_1  : Result_Set;
      Set_2  : Result_Set)
     return Boolean;
   --  Does Set_1 includes set_2 ?

   function Mutual_Inclusion
     (Set_1  : Result_Set;
      Set_2  : Result_Set)
     return Boolean;
   --  Does Set_1 includes set_2 AND set_2 includes set_1 ?

   function Empty_Set return Result_Set;
   --  returns the empty set

   function Is_Empty
     (Set  : Result_Set)
     return Boolean;
   --  Is the set empty ?

   function Cardinal
     (Set  : Result_Set)
     return Natural;
   --  Return set's cardinality

   function Get (Set  : Result_Set; Index : Natural)
                return Types.Node_Id;

   procedure Add (Set : in out Result_Set;
                  E   : Types.Node_Id;
                  Distinct : Boolean := False);
   --  Add the element E in the result set.
   --  If distint is set to true and if E is already
   --  present in the set, E won't be added

   function Is_In (E   : Types.Node_Id;
                   Set : Result_Set)
                  return Boolean;
   --  Found whether E is present in the Set

   --  Testing procedures

   function Test_Dummy (C : Instance_Type) return Result_Set;

   function Test_Dummy_Sets return Result_Set;

   procedure Display_Set (Set  : Result_Set);

   --  Misc functions

   function Get_Property_Value
     (E : Types.Node_Id; Name : String)
     return Types.Node_Id;
   --  for a given set element, returns then Name property value
   --  if the property is absent, returns No_Node.

private
   Max_Cardinal : constant Natural := 1000;
   --  FIXME :
   --  check rules for the rules that guides generation
   --  of Node_Id table's size (currently 1000, seems hard-coded)

   type Cardinal_Size is new Natural range 0 .. Max_Cardinal;

   type Result_Array is array (Cardinal_Size) of Types.Node_Id;

   type Result_Set is
      record
         Elements : Result_Array;
         Cardinal : Cardinal_Size := 0;
      end record;

end Ocarina.Checker.Queries;