with Ada.Real_Time, Display;
use type Ada.Real_Time.Time;

package body Timer with
  SPARK_Mode,
  Refined_State => (Control => Run_State)
is

   protected Run_State is
      pragma Priority (TuningData.UserPriority);

      procedure Start;

      procedure Stop;

      procedure Add_Time_If_Running
        with Global => (In_Out => Display.LCD);

      entry Wait_Until_Start;
   private
      Running : Boolean := False;
   end Run_State;

   protected body Run_State is
      procedure Start is
      begin
         Running := True;
      end Start;

      procedure Stop is
      begin
         Running := False;
      end Stop;

      procedure Add_Time_If_Running is
      begin
         if Running then
            Display.AddSecond;
         end if;
      end Add_Time_If_Running;

      pragma Warnings (Off, "statement has no effect",
                       Reason => "We use this just to block the task until" &
                                 " it is ready to run.");
      entry Wait_Until_Start when Running is
      begin
         null;
      end Wait_Until_Start;
      pragma Warnings (On, "statement has no effect");

   end Run_State;

   task body Timer with
     Refined_Depends => (Display.LCD => Run_State,
                         Run_State   => Run_State,
                         null        => Ada.Real_Time.Clock_Time)

   is
      Release_Time : Ada.Real_Time.Time := Ada.Real_Time.Clock;
      Period : Ada.Real_Time.Time_Span renames TuningData.TimerPeriod;
   begin
      Display.Initialize; -- ensure we get 0 on the screen at start up
      loop
         --  Wait until user allows clock to run...
         Run_State.Wait_Until_Start;

         --  Once running, count the seconds.
         Release_Time := Release_Time + Period;
         delay until Release_Time;

         --  Each time period, update the display. We check if we're
         --  still running to not *always* round up to the next second
         --  when we stop the clock.
         Run_State.Add_Time_If_Running;
      end loop;
   end Timer;

   procedure StartClock with
     Refined_Global  => (In_Out => Run_State),
     Refined_Depends => (Run_State => Run_State)
   is
   begin
      Run_State.Start;
   end StartClock;

   procedure StopClock with
     Refined_Global  => (In_Out => Run_State),
     Refined_Depends => (Run_State => Run_State)
   is
   begin
      Run_State.Stop;
   end StopClock;

end Timer;