-- | This module provides a type of atoms. An atom is a globally
-- unique identifier that also has a concrete name, as well as
-- additional name suggestions (in case it must be renamed).
--
-- 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.Atom where

import Data.Unique

import Nominal.Unsafe
import Nominal.ConcreteNames

-- ----------------------------------------------------------------------
-- * Atoms

-- | An atom is a globally unique, opaque value.
data Atom =
  -- | An atom consists of a unique identifier, a concrete name, and
  -- some optional name suggestions.
  Atom Unique String NameGen


instance Eq Atom where
  -- We only compare the unique identifier, because the name
  -- suggestions may be large or even infinite.
  Atom Unique
x String
n NameGen
ng == :: Atom -> Atom -> Bool
== Atom Unique
x' String
n' NameGen
ng' = Unique
x Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== Unique
x'

-- | User code should /not/ explicitly compare atoms for relative
-- ordering, because this is not referentially transparent (can be
-- unsound).  However, we define an 'Ord' instance for atoms anyway,
-- because it permits atoms to be used as keys in 'Set's and 'Map's.
instance Ord Atom where
  -- We only compare the unique identifier, because the name
  -- suggestions may be large or even infinite.
  compare :: Atom -> Atom -> Ordering
compare (Atom Unique
x String
n NameGen
ng) (Atom Unique
x' String
n' NameGen
ng') = Unique -> Unique -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Unique
x Unique
x'

instance Show Atom where
  show :: Atom -> String
show = Atom -> String
atom_show

-- ----------------------------------------------------------------------
-- ** Basic operations on atoms

-- | Return the name of an atom.
atom_show :: Atom -> String
atom_show :: Atom -> String
atom_show (Atom Unique
x String
n NameGen
ng) = String
n

-- | Return the suggested names of an atom.
atom_names :: Atom -> NameGen
atom_names :: Atom -> NameGen
atom_names (Atom Unique
x String
n NameGen
ng) = NameGen
ng

-- ----------------------------------------------------------------------
-- ** Creation of fresh atoms globally

-- | Globally create a fresh atom with the given name and name
-- suggestions.
fresh_atom_named :: String -> NameGen -> IO Atom
fresh_atom_named :: String -> NameGen -> IO Atom
fresh_atom_named String
n NameGen
ng = do
  Unique
x <- IO Unique
newUnique
  Atom -> IO Atom
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Unique -> String -> NameGen -> Atom
Atom Unique
x String
n NameGen
ng)

-- | Globally create a fresh atom with the given name suggestions.
fresh_atom :: NameGen -> IO Atom
fresh_atom :: NameGen -> IO Atom
fresh_atom NameGen
ng = do
  String
n <- NameGen -> IO String
global_new_io NameGen
ng
  String -> NameGen -> IO Atom
fresh_atom_named String
n NameGen
ng

-- ----------------------------------------------------------------------
-- ** Creation of fresh atoms in a scope

-- | Create a fresh atom with the given name and name suggestions.
--
-- The correct use of this function is subject to
-- Pitts's freshness condition.
with_fresh_atom_named :: String -> NameGen -> (Atom -> a) -> a
with_fresh_atom_named :: forall a. String -> NameGen -> (Atom -> a) -> a
with_fresh_atom_named String
n NameGen
ng Atom -> a
k =
  (Unique -> a) -> a
forall a. (Unique -> a) -> a
with_unique (\Unique
x -> Atom -> a
k (Unique -> String -> NameGen -> Atom
Atom Unique
x String
n NameGen
ng))

-- | Create a fresh atom with the given name suggestion.
--
-- Here, the call to 'global_new' is performed lazily (outside of the
-- 'IO' monad), so an actual concrete name will only be computed on
-- demand.
--
-- The correct use of this function is subject to
-- Pitts's freshness condition.
with_fresh_atom :: NameGen -> (Atom -> a) -> a
with_fresh_atom :: forall a. NameGen -> (Atom -> a) -> a
with_fresh_atom NameGen
ng Atom -> a
k =
  String -> NameGen -> (Atom -> a) -> a
forall a. String -> NameGen -> (Atom -> a) -> a
with_fresh_atom_named (NameGen -> String
global_new NameGen
ng) NameGen
ng Atom -> a
k