--          This file is part of SmartEiffel The GNU Eiffel Compiler.
--       Copyright (C) 1994-2002 LORIA - INRIA - U.H.P. Nancy 1 - FRANCE
--          Dominique COLNET and Suzanne COLLIN - SmartEiffel@loria.fr
--                       http://SmartEiffel.loria.fr
-- SmartEiffel is  free  software;  you can  redistribute it and/or modify it
-- under the terms of the GNU General Public License as published by the Free
-- Software  Foundation;  either  version  2, or (at your option)  any  later
-- version. SmartEiffel 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  along  with  SmartEiffel;  see the file COPYING.  If not,
-- write to the  Free Software Foundation, Inc., 59 Temple Place - Suite 330,
-- Boston, MA 02111-1307, USA.
--
class CLIENT_LIST
   --
   -- To store a list of clients class like : {FOO,BAR}
   --

inherit GLOBALS

creation make, omitted, merge

feature

   start_position: POSITION
         -- Of the the opening bracket when list is really written.

   is_omitted: BOOLEAN is
      do
         Result := start_position.is_unknown
      end

   pretty_print is
      do
         if is_omitted then
            if pretty_printer.zen_mode then
            else
               pretty_printer.put_string(once "{ANY} ")
            end
         else
            if list = Void then
               if pretty_printer.zen_mode then
                  pretty_printer.put_string(once "{} ")
               else
                  pretty_printer.put_string(once "{NONE} ")
               end
            else
               pretty_printer.put_character('{')
               pretty_printer.set_indent_level(2)
               list.pretty_print
               pretty_printer.put_character('}')
               pretty_printer.put_character(' ')
            end
         end
      end

   gives_permission_to(cn: CLASS_NAME): BOOLEAN is
         -- Check whether the `cn' class is a member (or a subclass as
         -- well) of the `Current' client list. (No error report done here
         -- in `error_handler').
      require
         cn /= Void
	 error_handler.is_empty
      do
         if is_omitted then
            -- It is equivalent to {ANY}:
            Result := true
         elseif list = Void then
            -- Because it is equivalent to {NONE}.
         else
            Result := list.gives_permission_to(cn)
         end
      ensure
	 error_handler.is_empty
      end

   gives_permission_to_any: BOOLEAN is
         -- Check whether the `Current' client list gives permission to all
         -- classes. (No error report done here in `error_handler').
      require
	 error_handler.is_empty
      do
         if is_omitted then
            Result := true
            -- Because it is as : {ANY}.
         elseif list = Void then
            -- Because it is as : {NONE}.
         else
            Result := list.gives_permission_to_any
         end
      ensure
	 error_handler.is_empty
      end

feature {BASE_CLASS, CLIENT_LIST}

   eiffel_view: STRING is
	 -- The Eiffel view of the allowed classe(s) list. (Because of
	 -- clients list merging, the `Current' clients list may be located
	 -- on many Eiffel source files. This function is also useful to
	 -- remind default abbreviated notation as omited list or empty
	 -- list.)
      local
	 i: INTEGER
      do
	 if eiffel_view_memory = Void then
	    if is_omitted then
	       eiffel_view_memory := once "{ANY}"
	    elseif list = Void then
	       eiffel_view_memory := once "{NONE}"
	    else
	       create eiffel_view_memory.make(64)
	       eiffel_view_memory.extend('{')
	       from
		  i := 1
	       until
		  i > list.count
	       loop
		  eiffel_view_memory.append(list.item(i).to_string)
		  i := i + 1
		  if i <= list.count then
		     eiffel_view_memory.extend(',')
		     eiffel_view_memory.extend(' ')
		  end
	       end
	       eiffel_view_memory.extend('}')
	    end
	 end
	 Result := eiffel_view_memory
      ensure
	 Result /= Void
      end

   locate_in_error_handler is
	 -- Add one or more related positions in the `error_handler'.
      do
	 if list = Void then
	    error_handler.add_position(start_position)
	 else
	    list.locate_in_error_handler
	 end
      end

feature {EXPORT_LIST}

   merge_with(other: like Current): like current is
      require
         other /= Void
      local
         sp: POSITION
      do
         if gives_permission_to_any then
            Result := Current
         elseif other.gives_permission_to_any then
            Result := other
         else
            sp := start_position
            if sp.is_unknown then
               sp := other.start_position
            end
            create Result.merge(sp,list,other.list)
         end
      end

feature {PARENT_LIST}

   append(other: like Current): like Current is
      require
         other /= Void
      do
         if Current = other or else is_omitted then
            Result := Current
         elseif gives_permission_to_any then
	    Result := Current
	 elseif other.is_omitted then
	    Result := other
	 elseif other.gives_permission_to_any then
	    Result := other
	 else
	    create Result.merge(start_position,list,other.list)
	 end
	 debug
	    eiffel_view_memory := Void
	    if eiffel_view /= Void then end
	 end
      end

feature {RUN_FEATURE}

   vape_check(enclosing: RUN_FEATURE; call_site: POSITION;
	      other: like Current) is
         -- To enforce the VAPE rule. The `Current' client list is the one of
         -- the `enclosing' feature and the `other' is the one of the
	 -- `call_site' which is inside the require assertion.
      require
         other /= Void
      local
         vape: BOOLEAN; i: INTEGER; cn: CLASS_NAME
      do
         if is_omitted then
            -- It is as {ANY}:
            vape := other.gives_permission_to_any
         elseif list = Void then
            -- It is {NONE}:
            vape := true
         else
            from
               vape := true
               i := list.count
            until
               not vape or else i = 0
            loop
               cn := list.item(i)
               vape := other.gives_permission_to(cn)
               i := i - 1
            end
         end
         if not vape then
            error_handler.append("(VAPE): The content of a require assertion must %
		      %also be visible by the caller of the routine (i.e. %
		      %the client must be able to check the require %
		      %assertion before calling the routine). See next %
		      %two following reports for details.")
            error_handler.print_as_error
	    --
            error_handler.add_position(call_site)
            error_handler.append("This call which is inside the require assertion is %
		       %exported to ")
	    error_handler.append(other.eiffel_view)
	    other.locate_in_error_handler
	    error_handler.extend('.')
            error_handler.print_as_error
	    --
            error_handler.add_position(enclosing.start_position)
            error_handler.append("This routine, is exported to ")
	    error_handler.append(Current.eiffel_view)
	    Current.locate_in_error_handler
            error_handler.append(" (when the type of Current is ")
            error_handler.append(enclosing.current_type.run_time_mark)
            error_handler.append(" ).")
            if cn /= Void then
	       error_handler.append(" (Class ")
	       error_handler.append(cn.to_string)
	       error_handler.append(" is not allowed to use the code inside the %
			 %require assertion.)")
            end
            error_handler.print_as_fatal_error
         end
      end

feature {CLIENT_LIST}

   list: CLASS_NAME_LIST

feature {NONE}

   make(sp: like start_position; l: like list) is
         -- When the client list is really written.
         --
         -- Note : {NONE} has the same meaning as {}.
      require
         not sp.is_unknown
      do
         start_position := sp
         list := l
	 debug
	    if eiffel_view /= Void then end
	 end
      ensure
         start_position = sp
         list = l
      end

   omitted is
         -- When the client list is omitted. (Remind that when the
         -- client list is omitted, it is like {ANY}.)
      do
      end

   merge(sp: like start_position; l1, l2: like list) is
      require
         not sp.is_unknown
      do
         start_position := sp
         create list.merge(l1,l2)
	 debug
	    eiffel_view_memory := Void
	    if eiffel_view /= Void then end
	 end
      end

   eiffel_view_memory: STRING
	 -- To cache the Result of `eiffel_view'.

end -- CLIENT_LIST