Safe Haskell	None
Language	Haskell2010

Nominal.Atom

Contents

Atoms

Description

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).

Synopsis

Atoms

data Atom Source #

An atom is a globally unique, opaque value.

Constructors

Atom Unique String NameGen

An atom consists of a unique identifier, a concrete name, and some optional name suggestions.

Instances

Eq Atom Source #
Methods (==) :: Atom -> Atom -> Bool # (/=) :: Atom -> Atom -> Bool #
Ord Atom Source #	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.
Methods compare :: Atom -> Atom -> Ordering # (<) :: Atom -> Atom -> Bool # (<=) :: Atom -> Atom -> Bool # (>) :: Atom -> Atom -> Bool # (>=) :: Atom -> Atom -> Bool # max :: Atom -> Atom -> Atom # min :: Atom -> Atom -> Atom #
Show Atom Source #
Methods showsPrec :: Int -> Atom -> ShowS # show :: Atom -> String # showList :: [Atom] -> ShowS #
Nominal Atom Source #
Methods (•) :: NominalPermutation -> Atom -> Atom Source #
NominalSupport Atom Source #
Methods support :: Atom -> Support Source #
Bindable Atom Source #
Methods binding :: Atom -> NominalPattern Atom Source #
Atomic Atom Source #
Methods to_atom :: Atom -> Atom Source # from_atom :: Atom -> Atom Source # names :: Atom -> NameGen Source #
NominalShow Atom Source #
Methods showsPrecSup :: Support -> Int -> Atom -> ShowS Source # nominal_showList :: Support -> [Atom] -> ShowS Source #

Basic operations on atoms

atom_show :: Atom -> String Source #

Return the name of an atom.

atom_names :: Atom -> NameGen Source #

Return the suggested names of an atom.

Creation of fresh atoms globally

fresh_atom_named :: String -> NameGen -> IO Atom Source #

Globally create a fresh atom with the given name and name suggestions.

fresh_atom :: NameGen -> IO Atom Source #

Globally create a fresh atom with the given name suggestions.

Creation of fresh atoms in a scope

with_fresh_atom_named :: String -> NameGen -> (Atom -> a) -> a Source #

Create a fresh atom with the given name and name suggestions. To ensure soundness, the created atom must not escape the body of the with_fresh block. Otherwise, referential transparency may be violated. For example,

with_fresh id != with_fresh id.

See the documentation of with_fresh for more information on the correctness criterion.

with_fresh_atom :: NameGen -> (Atom -> a) -> a Source #

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.