--          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.
--
deferred class ASSERTION_LIST
   --
   -- To store a list of assertions (see ASSERTION).
   --
   -- See also : CLASS_INVARIANT, E_REQUIRE, E_ENSURE,
   --            LOOP_INVARIANT and CHECK_INVARIANT.
   --

inherit GLOBALS

feature

   is_require: BOOLEAN is
      deferred
      end

   name: STRING is
         -- "require", "ensure" or "invariant".
      deferred
      end

   start_position: POSITION
         -- If any, the position of the first letter of `name'.

   header_comment: COMMENT

feature {ASSERTION_LIST,E_CHECK,E_FEATURE}

   list: ARRAY[ASSERTION]

feature

   verify_scoop(allowed: FORMAL_ARG_LIST) is
      local
         i: INTEGER
      do
         from
            i := list.upper
         until
            i = 0
         loop
            list.item(i).verify_scoop(allowed)
            i := i - 1
         end
      end

feature

   current_type: E_TYPE
         -- Not Void when checked in.

feature {NONE}

   run_feature: RUN_FEATURE
         -- Corresponding one (if any) when runnable.
         -- Note: class invariant are not inside a RUN_FEATURE.

feature

   set_current_type(ct: like current_type) is
      do
         current_type := ct
      end

   afd_check is
      local
         i: INTEGER
      do
         if list /= Void then
            from
               i := list.upper
            until
               i = 0
            loop
               list.item(i).afd_check
               i := i - 1
            end
         end
      end

feature {NONE}

   is_always_true: BOOLEAN is
      local
         i: INTEGER
         assertion: ASSERTION
      do
         from
            i := list.upper
            Result := true
         until
            not Result or else i = 0
         loop
            assertion := list.item(i)
            Result := assertion.is_always_true
            i := i - 1
         end
      end

feature

   compile_to_c is
      local
         i: INTEGER
         assertion: ASSERTION
      do
         if is_always_true then
            cpp.increment_static_expression_count(list.count)
         else
            c_set_flag
            from
               i := 1
            until
               i > list.upper
            loop
               assertion := list.item(i)
               if not is_require or else not smart_eiffel.scoop or else not assertion.is_guard then
                  c_compile_assertion(assertion)
               end
               i := i + 1
            end
            c_clear_flag
         end
      end

   c_scoop is
         -- Make some C code if the assertion is a guard
      require
         smart_eiffel.scoop
         is_require
      local
         i: INTEGER
         assertion: ASSERTION
         flag_set: BOOLEAN
      do
         if not is_always_true then
            from
               i := 1
            until
               i > list.upper
            loop
               assertion := list.item(i)
               if assertion.is_guard then
                  if not flag_set then
                     c_set_flag
                     flag_set := true
                  end
                  c_compile_assertion(assertion)
               end
               i := i + 1
            end
            if flag_set then
               c_clear_flag
            end
         end
      end

   frozen compile_to_jvm(last_chance: BOOLEAN) is
         -- If `last_chance' is true, an error message is printed at
         -- run-time.
         -- The final result is always left a top of stack.
      local
         point_true, i: INTEGER
         ca: like code_attribute
      do
         ca := code_attribute
         ca.check_opening
         from
            failure.clear
            i := 1
         until
            i > list.upper
         loop
            list.item(i).compile_to_jvm(last_chance)
            failure.add_last(ca.opcode_ifeq)
            i := i + 1
         end
         ca.opcode_iconst_1
         point_true := ca.opcode_goto
         ca.resolve_with(failure)
         ca.opcode_iconst_0
         ca.resolve_u2_branch(point_true)
         ca.check_closing
      end

   is_pre_computable: BOOLEAN is
      local
         i: INTEGER
      do
         if list = Void then
            Result := true
         else
            from
               i := list.upper
               Result := true
            until
               not Result or else i = 0
            loop
               Result := list.item(i).is_pre_computable
               i := i - 1
            end
         end
      end

   use_current: BOOLEAN is
      local
         i: INTEGER
      do
         if list /= Void then
            from
               i := list.upper
            until
               Result or else i = 0
            loop
               Result := list.item(i).use_current
               i := i - 1
            end
         end
      end

feature {NONE}

   make(sp: like start_position; hc: like header_comment; l: like list) is
      require
         l /= Void implies not l.is_empty
         hc /= Void or else l /= Void
      do
         start_position := sp
         header_comment := hc
         list := l
      ensure
         start_position = sp
         header_comment = hc
         list = l
      end

feature {NONE}

   make_runnable(sp: like start_position; l: like list
                 ct: like current_type; rf: like run_feature) is
      require
         not l.is_empty
         ct /= Void
      do
         start_position := sp
         list := l
         current_type := ct
         run_feature := rf
      ensure
         start_position = sp
         list = l
         current_type = ct
         run_feature = rf
      end

feature

   is_empty: BOOLEAN is
      do
         Result := list = Void
      end

   run_class: RUN_CLASS is
      do
         Result := current_type.run_class
      end

   frozen to_runnable(ct: E_TYPE): like Current is
      require
         ct.run_type = ct
      do
         if current_type = Void then
            current_type := ct
            run_feature := smart_eiffel.top_rf
            if list /= Void then
               list := assertion_collector.runnable(list,ct,run_feature,'_')
            end
            if nb_errors = 0 then
               Result := Current
            end
         else
            Result := twin
            Result.set_current_type(Void)
            Result := Result.to_runnable(ct)
         end
      ensure
         nb_errors = 0 implies Result /= Void
      end

   pretty_print is
      local
         i: INTEGER
      do
         pretty_printer.indent
         pretty_printer.keyword(name)
         pretty_printer.level_incr
         if header_comment /= Void then
            header_comment.pretty_print
         else
            pretty_printer.indent
         end
         if list /= Void then
            from
               i := 1
            until
               i > list.upper
            loop
               if pretty_printer.zen_mode and i = list.upper then
                  pretty_printer.set_semi_colon_flag(false)
               else
                  pretty_printer.set_semi_colon_flag(true)
               end
               pretty_printer.indent
               list.item(i).pretty_print
               i := i + 1
            end
         end
         pretty_printer.level_decr
         pretty_printer.indent
      ensure
         pretty_printer.indent_level = old pretty_printer.indent_level
      end

   set_header_comment(hc: like header_comment) is
      do
         header_comment := hc
      end

feature {E_FEATURE,RUN_CLASS,ASSERTION_COLLECTOR}

   add_into(collector: ARRAY[ASSERTION]) is
      local
         i: INTEGER
         a: ASSERTION
      do
         if list /= Void then
            from
               i := 1
            until
               i > list.upper
            loop
               a := list.item(i)
               if not collector.fast_has(a) then
                  collector.add_last(a)
               end
               i := i + 1
            end
         end
      end

feature {NONE}

   failure: FIXED_ARRAY[INTEGER] is
      once
         !!Result.with_capacity(12)
      end

   check_assertion_mode: STRING is
      deferred
      end

feature {ONCE_ROUTINE_POOL, RUN_REQUIRE}

   clear_run_feature is
      do
         run_feature := Void
      end

feature {NONE}

   c_compile_assertion(assertion: ASSERTION) is
      local
         need_se_tmp: BOOLEAN
      do
         if assertion.is_always_true then
         else
            assertion.collect_c_tmp
            need_se_tmp := cpp.se_tmp_open_declaration
            cpp.set_check_assertion_mode(check_assertion_mode)
            assertion.compile_to_c
            if need_se_tmp then
               cpp.se_tmp_close_declaration
            end
         end
      end

   c_set_flag is
      do
	 -- Remove the `assertion_flag' stuff in boost'ed SCOOP guards
	 if ace.no_check then
	    if run_feature = Void then
	       cpp.put_string
	       (once "if(ds.fd->assertion_flag){%Nds.fd->assertion_flag=0;%N")
	    else
	       cpp.put_string
	       (once "if(fd.assertion_flag){%Nfd.assertion_flag=0;%N")
	    end
	 end
      end

   c_clear_flag is
      do
	 -- Remove the `assertion_flag' stuff in boost'ed SCOOP guards
	 if ace.no_check then
	    if run_feature = Void then
	       cpp.put_string(once "ds.fd->assertion_flag=1;%N}%N")
	    else
	       cpp.put_string(once "fd.assertion_flag=1;%N}%N")
	    end
	 end
      end

invariant

   list /= Void implies (list.lower = 1 and not list.is_empty)

end -- ASSERTION_LIST