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

Defined in Nominal.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.

Defined in Nominal.Atom

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

Defined in Nominal.Atom

Methods

showsPrec :: Int -> Atom -> ShowS

show :: Atom -> String

showList :: [Atom] -> ShowS

Nominal Atom

Defined in Nominal.Nominal

Methods

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

NominalSupport Atom

Defined in Nominal.NominalSupport

Methods

support :: Atom -> Support

NominalShow Atom

Defined in Nominal.NominalShow

Methods

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

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

Bindable Atom

Defined in Nominal.Bindable

Methods

binding :: Atom -> NominalBinder Atom

Atomic Atom

Defined in Nominal.Atomic

Methods

to_atom :: Atom -> Atom

from_atom :: Atom -> Atom

names :: Atom -> NameGen

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.