[ re agda#2896 ] Restrict clock types

Author: gallais

src/System/Clock/Primitive.agda

@@ -14,16 +14,38 @@ open import Foreign.Haskell using (Pair)
 
 data Clock : Set where
   monotonic realTime processCPUTime : Clock
-  threadCPUTime monotonicRaw bootTime : Clock
-  monotonicCoarse realTimeCoarse : 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 #-}