--
-- Copyright (C) 2015-2016 secunet Security Networks AG
--
-- This program 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 of the License, or
-- (at your option) any later version.
--
-- This program 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.
--

with HW;
with HW.Time.Timer;

use type HW.Word64;

package body HW.Time
   with Refined_State => (State => (Timer.Timer_State, Timer.Abstract_Time))
is

   function Now return T
   with
      Refined_Global => (Input => Timer.Abstract_Time)
   is
      Current : constant T := Timer.Raw_Value_Min;
   begin
      return Current;
   end Now;

   function US_From_Now (US : Natural) return T
   with
      Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
   is
      Hz : constant T := Timer.Hz;
      Current : constant T := Timer.Raw_Value_Max;
   begin
      return Current + (T (US) * Hz + 999_999) / 1_000_000;
   end US_From_Now;

   function MS_From_Now (MS : Natural) return T
   with
      Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
   is
      Hz : constant T := Timer.Hz;
      Current : constant T := Timer.Raw_Value_Max;
   begin
      return Current + (T (MS) * Hz + 999) / 1_000;
   end MS_From_Now;

   function Now_US return Int64
   with
      Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
   is
      Hz : constant T := Timer.Hz;
      MHz : constant T := Hz / 1_000_000;
      Current : constant T := Timer.Raw_Value_Min;
   begin
      return Int64 (Current and (2 ** 63 - 1))
               / Int64 (if MHz = 0 then T'(1) else MHz);
   end Now_US;

   ----------------------------------------------------------------------------

   procedure Delay_Until (Deadline : T)
   with
      Refined_Global => (Input => (Timer.Abstract_Time))
   is
      Current : T;
   begin
      loop
         Current := Timer.Raw_Value_Min;
         exit when Current >= Deadline;
      end loop;
   end Delay_Until;

   procedure U_Delay (US : Natural)
   with
      Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
   is
      Deadline : constant T := US_From_Now (US);
   begin
      Delay_Until (Deadline);
   end U_Delay;

   procedure M_Delay (MS : Natural)
   with
      Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
   is
      Deadline : constant T := MS_From_Now (MS);
   begin
      Delay_Until (Deadline);
   end M_Delay;

   ----------------------------------------------------------------------------

   function Timed_Out (Deadline : T) return Boolean
   with
      Refined_Global => (Input => (Timer.Abstract_Time))
   is
      Current : constant T := Timer.Raw_Value_Min;
   begin
      return Current >= Deadline;
   end Timed_Out;

end HW.Time;

--  vim: set ts=8 sts=3 sw=3 et: