    ------------------------------------------------------------------------
    -- |
    -- Module           : Data.Parameterized.Nonce.Unsafe
    -- Description      : A counter in the ST monad.
    -- Copyright        : (c) Galois, Inc 2014
    -- Maintainer       : Joe Hendrix <jhendrix@galois.com>
    -- Stability        : provisional
    --
    -- This module provides a simple generator of new indexes in the ST monad.
    -- It is predictable and not intended for cryptographic purposes.
    --
    -- NOTE: the 'TestEquality' and 'OrdF' instances for the 'Nonce' type simply
    -- compare the generated nonce values and then assert to the compiler
    -- (via 'unsafeCoerce') that the types ascribed to the nonces are equal
    -- if their values are equal.  This is only OK because of the discipline
    -- by which nonces should be used: they should only be generated from
    -- a 'NonceGenerator' (i.e., should not be built directly), and nonces from
    -- different generators must never be compared!  Arranging to compare
    -- Nonces from different origins would allow users to build 'unsafeCoerce'
    -- via the 'testEquality' function.
    --
    -- This module is deprecated, and should not be used in new code.
    -- Clients of this module should migrate to use "Data.Parameterized.Nonce".
    -------------------------------------------------------------------------
    {-# LANGUAGE GeneralizedNewtypeDeriving #-}
    {-# LANGUAGE KindSignatures #-}
    {-# LANGUAGE PolyKinds #-}
    {-# LANGUAGE RoleAnnotations #-}
    {-# LANGUAGE Unsafe #-}
    module Data.Parameterized.Nonce.Unsafe
      {-# DEPRECATED "Migrate to use Data.Parameterized.Nonce instead, this module will be removed soon." #-}
      ( NonceGenerator
      , newNonceGenerator
      , freshNonce
      , atLimit
      , Nonce
      , indexValue
      ) where

    import Control.Monad.ST
    import Data.Hashable
    import Data.STRef
    import Data.Word
    import Unsafe.Coerce

    import Data.Parameterized.Axiom
    import Data.Parameterized.Classes

    -- | A simple type that for getting fresh indices in the 'ST' monad.
    -- The type parameter @s@ is used for the 'ST' monad parameter.
    newtype NonceGenerator s = NonceGenerator (STRef s Word64)

    -- | Create a new counter.
    newNonceGenerator :: ST s (NonceGenerator s)
    newNonceGenerator :: forall s. ST s (NonceGenerator s)
    newNonceGenerator = STRef s Word64 -> NonceGenerator s
    forall s. STRef s Word64 -> NonceGenerator s
    NonceGenerator (STRef s Word64 -> NonceGenerator s)
    -> ST s (STRef s Word64) -> ST s (NonceGenerator s)
    forall a b. (a -> b) -> ST s a -> ST s b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    `fmap` Word64 -> ST s (STRef s Word64)
    forall a s. a -> ST s (STRef s a)
    newSTRef (Int -> Word64
    forall a. Enum a => Int -> a
    toEnum Int
    0)

    -- | An index generated by the counter.
    newtype Nonce (tp :: k) = Nonce { forall k (tp :: k). Nonce tp -> Word64
    indexValue :: Word64 }
      deriving (Nonce tp -> Nonce tp -> Bool
    (Nonce tp -> Nonce tp -> Bool)
    -> (Nonce tp -> Nonce tp -> Bool) -> Eq (Nonce tp)
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    forall k (tp :: k). Nonce tp -> Nonce tp -> Bool
    $c== :: forall k (tp :: k). Nonce tp -> Nonce tp -> Bool
    == :: Nonce tp -> Nonce tp -> Bool
    $c/= :: forall k (tp :: k). Nonce tp -> Nonce tp -> Bool
    /= :: Nonce tp -> Nonce tp -> Bool
    Eq, Eq (Nonce tp)
    Eq (Nonce tp) =>
    (Nonce tp -> Nonce tp -> Ordering)
    -> (Nonce tp -> Nonce tp -> Bool)
    -> (Nonce tp -> Nonce tp -> Bool)
    -> (Nonce tp -> Nonce tp -> Bool)
    -> (Nonce tp -> Nonce tp -> Bool)
    -> (Nonce tp -> Nonce tp -> Nonce tp)
    -> (Nonce tp -> Nonce tp -> Nonce tp)
    -> Ord (Nonce tp)
    Nonce tp -> Nonce tp -> Bool
    Nonce tp -> Nonce tp -> Ordering
    Nonce tp -> Nonce tp -> Nonce tp
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    forall k (tp :: k). Eq (Nonce tp)
    forall k (tp :: k). Nonce tp -> Nonce tp -> Bool
    forall k (tp :: k). Nonce tp -> Nonce tp -> Ordering
    forall k (tp :: k). Nonce tp -> Nonce tp -> Nonce tp
    $ccompare :: forall k (tp :: k). Nonce tp -> Nonce tp -> Ordering
    compare :: Nonce tp -> Nonce tp -> Ordering
    $c< :: forall k (tp :: k). Nonce tp -> Nonce tp -> Bool
    < :: Nonce tp -> Nonce tp -> Bool
    $c<= :: forall k (tp :: k). Nonce tp -> Nonce tp -> Bool
    <= :: Nonce tp -> Nonce tp -> Bool
    $c> :: forall k (tp :: k). Nonce tp -> Nonce tp -> Bool
    > :: Nonce tp -> Nonce tp -> Bool
    $c>= :: forall k (tp :: k). Nonce tp -> Nonce tp -> Bool
    >= :: Nonce tp -> Nonce tp -> Bool
    $cmax :: forall k (tp :: k). Nonce tp -> Nonce tp -> Nonce tp
    max :: Nonce tp -> Nonce tp -> Nonce tp
    $cmin :: forall k (tp :: k). Nonce tp -> Nonce tp -> Nonce tp
    min :: Nonce tp -> Nonce tp -> Nonce tp
    Ord, Eq (Nonce tp)
    Eq (Nonce tp) =>
    (Int -> Nonce tp -> Int)
    -> (Nonce tp -> Int) -> Hashable (Nonce tp)
    Int -> Nonce tp -> Int
    Nonce tp -> Int
    forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
    forall k (tp :: k). Eq (Nonce tp)
    forall k (tp :: k). Int -> Nonce tp -> Int
    forall k (tp :: k). Nonce tp -> Int
    $chashWithSalt :: forall k (tp :: k). Int -> Nonce tp -> Int
    hashWithSalt :: Int -> Nonce tp -> Int
    $chash :: forall k (tp :: k). Nonce tp -> Int
    hash :: Nonce tp -> Int
    Hashable, Int -> Nonce tp -> ShowS
    [Nonce tp] -> ShowS
    Nonce tp -> String
    (Int -> Nonce tp -> ShowS)
    -> (Nonce tp -> String) -> ([Nonce tp] -> ShowS) -> Show (Nonce tp)
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    forall k (tp :: k). Int -> Nonce tp -> ShowS
    forall k (tp :: k). [Nonce tp] -> ShowS
    forall k (tp :: k). Nonce tp -> String
    $cshowsPrec :: forall k (tp :: k). Int -> Nonce tp -> ShowS
    showsPrec :: Int -> Nonce tp -> ShowS
    $cshow :: forall k (tp :: k). Nonce tp -> String
    show :: Nonce tp -> String
    $cshowList :: forall k (tp :: k). [Nonce tp] -> ShowS
    showList :: [Nonce tp] -> ShowS
    Show)

    --  Force the type role of Nonce to be nominal: this prevents Data.Coerce.coerce
    --  from casting the types of nonces, which it would otherwise be able to do
    --  because tp is a phantom type parameter.  This partially helps to protect
    --  the nonce abstraction.
    type role Nonce nominal

    instance EqF Nonce where
      eqF :: forall (a :: k). Nonce a -> Nonce a -> Bool
    eqF Nonce a
    x Nonce a
    y = Maybe (a :~: a) -> Bool
    forall a. Maybe a -> Bool
    isJust (Nonce a -> Nonce a -> Maybe (a :~: a)
    forall (a :: k) (b :: k). Nonce a -> Nonce b -> Maybe (a :~: b)
    forall {k} (f :: k -> *) (a :: k) (b :: k).
    TestEquality f =>
    f a -> f b -> Maybe (a :~: b)
    testEquality Nonce a
    x Nonce a
    y)

    instance TestEquality Nonce where
      testEquality :: forall (a :: k) (b :: k). Nonce a -> Nonce b -> Maybe (a :~: b)
    testEquality Nonce a
    x Nonce b
    y | Nonce a -> Word64
    forall k (tp :: k). Nonce tp -> Word64
    indexValue Nonce a
    x Word64 -> Word64 -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nonce b -> Word64
    forall k (tp :: k). Nonce tp -> Word64
    indexValue Nonce b
    y = (a :~: b) -> Maybe (a :~: b)
    forall a. a -> Maybe a
    Just a :~: b
    forall {k} (a :: k) (b :: k). a :~: b
    unsafeAxiom
                       | Bool
    otherwise = Maybe (a :~: b)
    forall a. Maybe a
    Nothing

    instance OrdF Nonce where
      compareF :: forall (x :: k) (y :: k). Nonce x -> Nonce y -> OrderingF x y
    compareF Nonce x
    x Nonce y
    y =
        case Word64 -> Word64 -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Nonce x -> Word64
    forall k (tp :: k). Nonce tp -> Word64
    indexValue Nonce x
    x) (Nonce y -> Word64
    forall k (tp :: k). Nonce tp -> Word64
    indexValue Nonce y
    y) of
          Ordering
    LT -> OrderingF x y
    forall {k} (x :: k) (y :: k). OrderingF x y
    LTF
          Ordering
    EQ -> OrderingF (ZonkAny 1) (ZonkAny 1) -> OrderingF x y
    forall a b. a -> b
    unsafeCoerce OrderingF (ZonkAny 1) (ZonkAny 1)
    forall {k} (x :: k). OrderingF x x
    EQF
          Ordering
    GT -> OrderingF x y
    forall {k} (x :: k) (y :: k). OrderingF x y
    GTF

    instance HashableF Nonce where
      hashWithSaltF :: forall (tp :: k). Int -> Nonce tp -> Int
    hashWithSaltF Int
    s (Nonce Word64
    x) = Int -> Word64 -> Int
    forall a. Hashable a => Int -> a -> Int
    hashWithSalt Int
    s Word64
    x

    instance ShowF Nonce

    {-# INLINE freshNonce #-}
    -- | Get a fresh index and increment the counter.
    freshNonce :: NonceGenerator s -> ST s (Nonce tp)
    freshNonce :: forall {k} s (tp :: k). NonceGenerator s -> ST s (Nonce tp)
    freshNonce (NonceGenerator STRef s Word64
    r) = do
      i <- STRef s Word64 -> ST s Word64
    forall s a. STRef s a -> ST s a
    readSTRef STRef s Word64
    r
      writeSTRef r $! succ i
      return (Nonce i)

    -- | Return true if counter has reached the limit, and can't be
    -- incremented without risk of error.
    atLimit :: NonceGenerator s -> ST s Bool
    atLimit :: forall s. NonceGenerator s -> ST s Bool
    atLimit (NonceGenerator STRef s Word64
    r) = do
      i <- STRef s Word64 -> ST s Word64
    forall s a. STRef s a -> ST s a
    readSTRef STRef s Word64
    r
      return (i == maxBound)