    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Primitive System.Clock simple bindings to Haskell functions
    ------------------------------------------------------------------------

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

    module System.Clock.Primitive where

    open import Agda.Builtin.Nat using (Nat)
    open import IO.Primitive.Core using (IO)
    open import Foreign.Haskell using (Pair)

    data Clock : Set where
      monotonic realTime processCPUTime : Clock
      threadCPUTime monotonicRaw bootTime : Clock
      monotonicCoarse realTimeCoarse : Clock

    {-# COMPILE GHC Clock = data Clock (Monotonic | Realtime | ProcessCPUTime
                                       | ThreadCPUTime | MonotonicRaw | Boottime
                                       | MonotonicCoarse | RealtimeCoarse )
    #-}

    postulate getTime : Clock → IO (Pair Nat Nat)

    {-# FOREIGN GHC import System.Clock  #-}
    {-# FOREIGN GHC import Data.Function #-}
    {-# COMPILE GHC getTime = fmap (\ (TimeSpec a b) -> ((,) `on` fromIntegral) a b) . getTime #-}