Nominal.Atom

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.

Atoms

data Atom

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

Methods

(==) :: Atom -> Atom -> Bool

(/=) :: Atom -> Atom -> Bool

Ord Atom

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 Sets and Maps.

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

Methods

showsPrec :: Int -> Atom -> ShowS

show :: Atom -> String

showList :: [Atom] -> ShowS

Nominal Atom

Methods

(•) :: NominalPermutation -> Atom -> Atom

NominalSupport Atom

Methods

support :: Atom -> Support

Bindable Atom

Methods

binding :: Atom -> NominalBinder Atom

Atomic Atom

Methods

to_atom :: Atom -> Atom

from_atom :: Atom -> Atom

names :: Atom -> NameGen

NominalShow Atom

Methods

showsPrecSup :: Support -> Int -> Atom -> ShowS

nominal_showList :: Support -> [Atom] -> ShowS

Basic operations on atoms

atom_show :: Atom -> String

Return the name of an atom.

atom_names :: Atom -> NameGen

Return the suggested names of an atom.

Creation of fresh atoms globally

fresh_atom_named :: String -> NameGen -> IO Atom

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

fresh_atom :: NameGen -> IO Atom

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

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 :: NameGen -> (Atom -> a) -> a

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.