--
--  Copyright (c) 2022-2023, German Rivera
--
--
--  SPDX-License-Identifier: Apache-2.0
--

with HiRTOS.Memory_Protection;
with System.Storage_Elements;

package HiRTOS.Timer is

   type Timer_Expiration_Callback_Type is access
      procedure (Timer_Id : Valid_Timer_Id_Type;
                 Callback_Arg : System.Storage_Elements.Integer_Address)
          with Convention => C;

   function Timer_Running (Timer_Id : Valid_Timer_Id_Type) return Boolean;

   procedure Create_Timer (Timer_Id : out Valid_Timer_Id_Type);

   --
   --  NOTE: Due to a race condition with the tick timer ISR, the timer may have already expired
   --  when this subprogram returns to the caller. So we cannot assert in the post-condition that
   --  the timer is still running upon return.
   --
   procedure Start_Timer (Timer_Id : Valid_Timer_Id_Type;
                          Expiration_Time_Us : Relative_Time_Us_Type;
                          Expiration_Callback : Timer_Expiration_Callback_Type;
                          Expiration_Callback_Arg : System.Storage_Elements.Integer_Address;
                          Periodic : Boolean := False)
      with Pre => not Timer_Running (Timer_Id)
                  and then
                  Expiration_Time_Us /= 0
                  and then
                  Expiration_Time_Us mod HiRTOS_Config_Parameters.Tick_Timer_Period_Us = 0
                  and then
                  HiRTOS.Memory_Protection.Valid_Code_Address (Expiration_Callback.all'Address);

   --
   --  NOTE: Due to a race condition with the tick timer ISR, the timer may have already expired
   --  may have already expired when this subprogram is invoked. So we cannot assert in the
   --  pre-condition that the timer is still running upon entry.
   --
   procedure Stop_Timer (Timer_Id : Valid_Timer_Id_Type)
      with Post => not Timer_Running (Timer_Id);

   function Get_Timestamp_Us return Absolute_Time_Us_Type;

end HiRTOS.Timer;