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

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

    module System.Random.Primitive where

    open import Agda.Builtin.IO using (IO)
    open import Agda.Builtin.Char using (Char)
    open import Agda.Builtin.Float using (Float)
    open import Agda.Builtin.Int using (Int)
    open import Agda.Builtin.Nat using (Nat)
    open import Agda.Builtin.Word using (Word64)
    open import Foreign.Haskell.Pair using (Pair)

    postulate
      randomIO-Char : IO Char
      randomRIO-Char : Pair Char Char → IO Char
      randomIO-Int : IO Int
      randomRIO-Int : Pair Int Int → IO Int
      randomIO-Float : IO Float
      randomRIO-Float : Pair Float Float → IO Float
      randomIO-Nat : IO Nat
      randomRIO-Nat : Pair Nat Nat → IO Nat
      randomIO-Word64 : IO Word64
      randomRIO-Word64 : Pair Word64 Word64 → IO Word64

    {-# FOREIGN GHC import System.Random #-}

    {-# COMPILE GHC randomIO-Char = randomIO #-}
    {-# COMPILE GHC randomRIO-Char = randomRIO #-}
    {-# COMPILE GHC randomIO-Int = randomIO #-}
    {-# COMPILE GHC randomRIO-Int = randomRIO #-}
    {-# COMPILE GHC randomIO-Float = randomIO #-}
    {-# COMPILE GHC randomRIO-Float = randomRIO #-}
    {-# COMPILE GHC randomIO-Nat = abs <$> randomIO #-}
    {-# COMPILE GHC randomRIO-Nat = randomRIO #-}
    {-# COMPILE GHC randomIO-Word64 = randomIO #-}
    {-# COMPILE GHC randomRIO-Word64 = randomRIO #-}