-- This file is  free  software, which  comes  along  with  SmartEiffel. This
-- software  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. You can modify it as you want, provided
-- this header is kept unaltered, and a notification of the changes is added.
-- You  are  allowed  to  redistribute  it and sell it, alone or as a part of
-- another product.
--       Copyright (C) 1994-2002 LORIA - INRIA - U.H.P. Nancy 1 - FRANCE
--          Dominique COLNET and Suzanne COLLIN - SmartEiffel@loria.fr
--                       http://SmartEiffel.loria.fr
--
expanded class MICROSECOND_TIME
--
-- Date and time facilities (like TIME) plus an extra microsecond information.
--

inherit
   HASHABLE redefine is_equal end
   COMPARABLE redefine is_equal end

feature

   time: TIME
	 -- To store year, month, day, hour and seconds.

   microsecond: INTEGER
         -- Extra information in number of microseconds in range 0 .. 999999.
	 -- Note that the accuracy is system dependant.

   is_local_time: BOOLEAN is
         -- Is the local time in use? This information applies to all objects
         -- of class TIME and MICROSECOND_TIME.
      do
         Result := time.is_local_time
      ensure
         Result implies not is_universal_time
      end

   is_universal_time: BOOLEAN is
         -- Is Universal Time in use?  This information applies to all objects
         -- of class TIME and MICROSECOND_TIME.
      do
         Result := time.is_universal_time
      ensure
         Result implies not is_local_time
      end

   year: INTEGER is
         -- Number of the year.
      do
	 Result := time.year
      end

   month: INTEGER is
         -- Number of the month (1 for January, 2 for February, ...
         -- 12 for December).
      do
         Result := time.month
      ensure
         Result.in_range(1,12)
      end

   day: INTEGER is
         -- Day of the `month' in range 1 .. 31.
      do
         Result := time.day
      ensure
         Result.in_range(1,31)
      end

   hour: INTEGER is
         -- Hour in range 0..23.
      do
         Result := time.hour
      ensure
         Result.in_range(0,23)
      end

   minute: INTEGER is
         -- Minute in range 0 .. 59.
      do
         Result := time.minute
      ensure
         Result.in_range(0,59)
      end

   second: INTEGER is
         -- Second in range 0 .. 59.
      do
         Result := time.second
      ensure
         Result.in_range(0,59)
      end

   week_day: INTEGER is
         -- Number of the day in the week (Sunday is 0, Monday is 1, etc.).
      do
         Result := time.week_day
      ensure
         Result.in_range(0,6)
      end

   year_day: INTEGER is
         -- Number of the day in the year in range 0 .. 365.
      do
         Result := time.year_day
      end

   is_summer_time_used: BOOLEAN is
         -- Is summer time in effect? This information applies to all objects
         -- of class TIME and MICROSECOND_TIME.
      do
         Result := time.is_summer_time_used
      end

feature -- Setting:

   update is
         -- Update `Current' with the current system clock.
      do
         basic_microsecond_update
	 time.set_time_memory(basic_microsecond_time)
	 microsecond := basic_microsecond_microsecond
      end

   set(a_year, a_month, a_day, a_hour, a_min, sec: INTEGER): BOOLEAN is
         -- Try to set `Current' using the given information. If this input
         -- is not a valid date, the `Result' is false and `Current' is not updated.
      require
	 valid_month: a_month.in_range(1,12)
	 valid_day: a_day.in_range(1,31)
	 valid_hour: a_hour.in_range(0,23)
	 valid_minute: a_min.in_range(0,59)
	 valid_second: sec.in_range(0,59)
      do
	 Result := time.set(a_year,a_month,a_day,a_hour,a_min,sec)
      end

   set_microsecond(microsec: INTEGER) is
         -- To set `microsecond' in range 0 .. 999 999.
      require
	 microsec.in_range(0, 999_999)
      do
	 microsecond := microsec
      ensure
	 microsecond = microsec
      end

   infix "+" (s: DOUBLE): like Current is
	 -- Add `s' seconds (2.476 is 2 seconds and 476 milliseconds)
      require
	 s >= 0.0
      local
	 a, b: INTEGER
      do
	 a := s.truncated_to_integer
	 b := ((s - a) * 1_000_000).truncated_to_integer
	 Result := Current
	 Result.add_second(a)
	 Result.add_microsecond(b)
      end

   add_second(s: INTEGER) is
	 -- Add `s' seconds to `Current'.
      require
	 s >= 0
      do
	 time.add_second(s)
      ensure
	 Current >= old Current
      end

   add_millisecond(millisecond: INTEGER) is
	 -- Add `millisecond' milliseconds.
      require
	 millisecond.in_range(0, 999)
      do
	 add_microsecond(millisecond * 1000)
      ensure
	 Current >= old Current
      end

   add_microsecond(microsec: INTEGER) is
	 -- Add `microsec' microseconds
      require
	 microsec.in_range(0, 999_999)
      local
	 a: INTEGER
      do
	 a := microsec + microsecond
	 if a >= 1_000_000 then
	    add_second(1)
	    a := a - 1_000_000
	 end
	 microsecond := a
      ensure
	 Current >= old Current
      end

feature

   elapsed_seconds(other: like Current): INTEGER is
         -- Elapsed time in seconds from `Current' to `other'.
      do
         Result := time.elapsed_seconds(other.time)
	 if other.microsecond < microsecond then
	    Result := Result - 1
	 end
      end

   elapsed_with_subsecond (other: like Current): DOUBLE is
         -- Elapsed time in seconds from `Current' to `other' with sub-second
	 -- precision.
      require
         Current <= other
      local
	 tm1, tm2: DOUBLE
      do
	 tm1 := time.time_memory
	 tm2 := other.time.time_memory
         Result := basic_time_difftime(tm2,tm1)
	 Result := Result + ((other.microsecond - microsecond) / 1_000_000)
      ensure
         Result >= 0
      end

   is_equal(other: like Current): BOOLEAN is
      do
	 if microsecond = other.microsecond then
	    Result := time.is_equal(other.time)
	 end
      end

   infix "<" (other: like Current): BOOLEAN is
      local
	 tm1, tm2: DOUBLE; sec: INTEGER
      do
	 tm1 := time.time_memory
	 tm2 := other.time.time_memory
         sec := basic_time_difftime(tm2,tm1)
	 Result := sec > 0 or else 
			(sec = 0 and then microsecond < other.microsecond)
      ensure
	 Result implies (elapsed_with_subsecond(other) > 0)
      end

feature -- Setting common time mode (local or universal):

   set_universal_time is
      do
         time.set_universal_time
      ensure
         is_universal_time
      end

   set_local_time is
      do
         time.set_local_time
      ensure
         is_local_time
      end

feature -- Hashing:

   hash_code: INTEGER is
      do
         Result := time.hash_code
      end

feature {NONE}

   basic_microsecond_time: DOUBLE is
      external "SmartEiffel"
      end

   basic_microsecond_microsecond: INTEGER is
      external "SmartEiffel"
      end

   basic_microsecond_update is
      external "SmartEiffel"
      end

   basic_time_difftime(time2, time1: DOUBLE): INTEGER is
      external "SmartEiffel"
      end

invariant

   microsecond.in_range(0,999999)

end -- MICROSECOND_TIME