    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Measuring time
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --guardedness #-}

    module System.Clock where

    open import Level using (Level; 0ℓ; Lift; lower)
    open import Data.Bool.Base using (if_then_else_)
    open import Data.Fin.Base using (Fin; toℕ)
    open import Data.Nat.Base as ℕ using (ℕ; zero; suc; _+_; _∸_; _^_; _<ᵇ_)
    import Data.Nat.Show as ℕ using (show)
    open import Data.Nat.DivMod using (_/_)
    import Data.Nat.Properties as ℕ
    open import Data.String.Base using (String; _++_; padLeft)

    open import IO.Base
    open import Function.Base using (_$_; _∘′_)
    open import Foreign.Haskell using (_,_)

    open import Relation.Nullary.Decidable using (False; fromWitnessFalse; toWitnessFalse)

    private
      variable
        a : Level
        A : Set a

    ------------------------------------------------------------------------
    -- Re-exporting the Clock data structure

    open import System.Clock.Primitive as Prim
      public
      using ( Clock
            -- System-wide monotonic time since an arbitrary point in the past
            ; monotonic
            -- System-wide real time since the Epoch
            ; realTime
            -- Amount of execution time of the current process
            ; processCPUTime
            -- Amount of execution time of the current OS thread
            ; threadCPUTime
            -- A raw hardware version of Monotonic ignoring adjustments
            ; monotonicRaw
            -- Linux-specific clocks
            -- Similar to Monotonic, includes time spent suspended
            ; bootTime
            -- Faster but less precise alternative to Monotonic
            ; monotonicCoarse
            -- Faster but less precise alternative to RealTime
            ; realTimeCoarse
            )

    ------------------------------------------------------------------------
    -- Defining a more convenient representation

    record Time : Set where
      constructor mkTime
      field seconds     : ℕ
            nanoseconds : ℕ
    open Time public

    ------------------------------------------------------------------------
    -- Reading the clock

    getTime : Clock → IO Time
    getTime c = do
      (a , b) ← lift (Prim.getTime c)
      pure $ mkTime a b

    ------------------------------------------------------------------------
    -- Measuring time periods

    diff : Time → Time → Time
    diff (mkTime ss sns) (mkTime es ens) =
      if ens <ᵇ sns
      then mkTime (es ∸ suc ss) ((1000000000 + ens) ∸ sns)
      else mkTime (es ∸ ss) (ens ∸ sns)

    record Timed (A : Set a) : Set a where
      constructor mkTimed
      field value : A
            time  : Time

    time : IO A → IO (Timed A)
    time io = do
      start ← lift! $ getTime realTime
      a     ← io
      end   ← lift! $ getTime realTime
      pure $ mkTimed a $ diff (lower start) (lower end)

    time′ : IO {0ℓ} A → IO Time
    time′ io = Timed.time <$> time io

    ------------------------------------------------------------------------
    -- Showing time

    show : Time →   -- Time in seconds and nanoseconds
           Fin 10 → -- Number of decimals to show
                    -- (in [0,9] because we are using nanoseconds)
           String
    show (mkTime s ns) prec = secs ++ "s" ++ padLeft '0' decimals nsecs where
      decimals = toℕ prec
      secs     = ℕ.show s
      prf      = ℕ.m^n≢0 10 (9 ∸ decimals)
      nsecs    = ℕ.show ((ns / (10 ^ (9 ∸ decimals))) {{prf}})