{-# OPTIONS_GHC -fno-cse -fno-full-laziness #-}

-- | This module provides three primitive functions that use
-- 'unsafePerformIO'. These functions are only safe if used correctly.
-- How to use each function correctly is specified in its documentation.
--
-- This module exposes implementation details of the Nominal library,
-- and should not normally be imported. Users of the library should
-- only import the top-level module "Nominal".

module Nominal.Unsafe where

import Data.IORef
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Unique
import System.IO.Unsafe (unsafePerformIO)

import Nominal.ConcreteNames

-- | A global variable holding a set of strings already used for free
-- names.
-- 
-- The use of 'unsafePerformIO' in this function is safe, because it
-- is only called once and serves to create a unique global reference
-- cell.
{-# NOINLINE global_used #-}
global_used :: IORef (Set String)
global_used :: IORef (Set String)
global_used = IO (IORef (Set String)) -> IORef (Set String)
forall a. IO a -> a
unsafePerformIO (IO (IORef (Set String)) -> IORef (Set String))
-> IO (IORef (Set String)) -> IORef (Set String)
forall a b. (a -> b) -> a -> b
$ do
  Set String -> IO (IORef (Set String))
forall a. a -> IO (IORef a)
newIORef Set String
forall a. Set a
Set.empty

-- | Create a globally new concrete name based on the given name
-- suggestion. This ensures that fresh names have distinct names when
-- they are not bound.
global_new_io :: NameGen -> IO String
global_new_io :: NameGen -> IO String
global_new_io NameGen
ng = do
  Set String
used <- IORef (Set String) -> IO (Set String)
forall a. IORef a -> IO a
readIORef IORef (Set String)
global_used
  let n :: String
n = Set String -> NameGen -> String
rename_fresh Set String
used NameGen
ng
  IORef (Set String) -> Set String -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (Set String)
global_used (String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.insert String
n Set String
used)
  String -> IO String
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return String
n

-- | Create a globally new concrete name based on the given name
-- suggestion.
-- 
-- The use of 'unsafePerformIO' in this function is safe, provided
-- that the user only uses API functions and respects Pitts's
-- freshness condition.
{-# NOINLINE global_new #-}
global_new :: NameGen -> String
global_new :: NameGen -> String
global_new NameGen
ng = IO String -> String
forall a. IO a -> a
unsafePerformIO (NameGen -> IO String
global_new_io NameGen
ng)

-- | Perform a subcomputation in the presence of a globally unique
-- value. This is similar to 'newUnique', but uses a continuation
-- monad instead of the 'IO' monad. To ensure referential
-- transparency, the unique value must not escape the function body.
--
-- The use of 'unsafePerformIO' in this function is safe, provided
-- that the user only uses API functions and respects Pitts's
-- freshness condition.
{-# NOINLINE with_unique #-}
with_unique :: (Unique -> a) -> a
with_unique :: forall a. (Unique -> a) -> a
with_unique Unique -> a
k = IO a -> a
forall a. IO a -> a
unsafePerformIO (IO a -> a) -> IO a -> a
forall a b. (a -> b) -> a -> b
$ do
  Unique
x <- IO Unique
newUnique
  a -> IO a
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Unique -> a
k Unique
x)

-- | Unsafely embed the 'IO' monad in a continuation monad.
--
-- The use of 'unsafePerformIO' in this function is safe, provided
-- that the user only uses API functions and respects Pitts's
-- freshness condition.
unsafe_with :: IO a -> (a -> b) -> b
unsafe_with :: forall a b. IO a -> (a -> b) -> b
unsafe_with IO a
comp a -> b
k = IO b -> b
forall a. IO a -> a
unsafePerformIO (IO b -> b) -> IO b -> b
forall a b. (a -> b) -> a -> b
$ do
  a
a <- IO a
comp
  b -> IO b
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> b
k a
a)