Merge pull request #2900 from gallais/v2.0-joss-submission-mac

 [ re #2896 ] Restrict clock types

Author: JacquesCarette

src/System/Clock.agda

@@ -37,20 +37,13 @@ open import System.Clock.Primitive as Prim
         -- System-wide monotonic time since an arbitrary point in the past
         ; monotonic
         -- System-wide real time since the Epoch
-        ; realTime
+        ; 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
         )
 
 ------------------------------------------------------------------------
@@ -86,9 +79,9 @@ record Timed (A : Set a) : Set a where
 
 time : IO A → IO (Timed A)
 time io = do
-  start ← lift! $ getTime realTime
+  start ← lift! $ getTime realtime
   a     ← io
-  end   ← lift! $ getTime realTime
+  end   ← lift! $ getTime realtime
   pure $ mkTimed a $ diff (lower start) (lower end)
 
 time′ : IO {0ℓ} A → IO Time

src/System/Clock/Primitive.agda

@@ -13,17 +13,39 @@ open import IO.Primitive using (IO)
 open import Foreign.Haskell using (Pair)
 
 data Clock : Set where
-  monotonic realTime processCPUTime : Clock
-  threadCPUTime monotonicRaw bootTime : Clock
-  monotonicCoarse realTimeCoarse : Clock
+  monotonic realtime processCPUTime : Clock
+  threadCPUTime monotonicRaw : Clock
 
-{-# COMPILE GHC Clock = data Clock (Monotonic | Realtime | ProcessCPUTime
-                                   | ThreadCPUTime | MonotonicRaw | Boottime
-                                   | MonotonicCoarse | RealtimeCoarse )
+{-# FOREIGN GHC import System.Clock  #-}
+
+{-# FOREIGN GHC
+data AgdaClock
+  = AgdaMonotonic
+  | AgdaRealtime
+  | AgdaProcessCPUTime
+  | AgdaThreadCPUTime
+  | AgdaMonotonicRaw
+
+fromAgdaClock :: AgdaClock -> Clock
+fromAgdaClock ac = case ac of
+  AgdaMonotonic -> Monotonic
+  AgdaRealtime -> Realtime
+  AgdaProcessCPUTime -> ProcessCPUTime
+  AgdaThreadCPUTime -> ThreadCPUTime
+  AgdaMonotonicRaw -> MonotonicRaw
+#-}
+
+{-# COMPILE GHC Clock =
+  data AgdaClock
+  ( AgdaMonotonic
+  | AgdaRealtime
+  | AgdaProcessCPUTime
+  | AgdaThreadCPUTime
+  | AgdaMonotonicRaw
+  )
 #-}
 
 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 #-}
+{-# COMPILE GHC getTime = fmap (\ (TimeSpec a b) -> ((,) `on` fromIntegral) a b) . getTime . fromAgdaClock #-}