| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Nominal.NominalSupport
Contents
Description
This module provides the NominalSupport type class. It consists
of those types for which the support can be calculated. With the
exception of function types, most Nominal types are also
in NominalSupport.
We also provide some generic programming so that instances of
NominalSupport can be automatically derived in most cases.
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.
Synopsis
- newtype Literal = Literal String
- data Avoidee
- newtype Support = Support (Set Avoidee)
- support_empty :: Support
- support_unions :: [Support] -> Support
- support_union :: Support -> Support -> Support
- support_insert :: Atom -> Support -> Support
- support_atom :: Atom -> Support
- support_delete :: Atom -> Support -> Support
- support_deletes :: [Atom] -> Support -> Support
- support_string :: String -> Support
- strings_of_support :: Support -> Set String
- class Nominal t => NominalSupport t where
- atom_open_for_printing :: Nominal t => Support -> BindAtom t -> (Atom -> t -> Support -> s) -> s
- basic_support :: t -> Support
- class GNominalSupport f where
Literal strings
A wrapper around strings. This is used to denote any literal
strings whose values should not clash with the names of bound
variables. For example, if a term contains a constant symbol c,
the name c should not also be used as the name of a bound
variable. This can be achieved by marking the string with
Literal, like this
data Term = Var Atom | Const (Literal String) | ...
Another way to use Literal is in the definition of custom
NominalSupport instances. See
"Defining custom instances" for an example.
Instances
| Show Literal Source # | |
| Nominal Literal Source # | |
Defined in Nominal.NominalSupport | |
| NominalSupport Literal Source # | |
| NominalShow Literal Source # | |
Defined in Nominal.NominalShow | |
| Bindable Literal Source # | |
Defined in Nominal.Bindable | |
Support
Something to be avoided can be an atom or a string.
support_empty :: Support Source #
The empty support.
support_unions :: [Support] -> Support Source #
The union of a list of supports.
support_atom :: Atom -> Support Source #
A singleton support.
support_string :: String -> Support Source #
Add a literal string to the support.
The NominalSupport class
class Nominal t => NominalSupport t where Source #
NominalSupport is a subclass of Nominal consisting of those
types for which the support can be calculated. With the notable
exception of function types, most Nominal types are also
instances of NominalSupport.
In most cases, instances of NominalSupport can be automatically
derived. See "Deriving generic instances" for
information on how to do so, and
"Defining custom instances" for how to write custom
instances.
Minimal complete definition
Nothing
Methods
support :: t -> Support Source #
Compute a set of atoms and strings that should not be used as the names of bound variables.
support :: (Generic t, GNominalSupport (Rep t)) => t -> Support Source #
Compute a set of atoms and strings that should not be used as the names of bound variables.
Instances
Open for printing
atom_open_for_printing :: Nominal t => Support -> BindAtom t -> (Atom -> t -> Support -> s) -> s Source #
A variant of open which moreover chooses a name for the bound
atom that does not clash with any free name in its scope. This
function is mostly useful for building custom pretty-printers for
nominal terms. Except in pretty-printers, it is equivalent to
open.
Usage:
open_for_printing sup t (\x s sup' -> body)
Here, sup = support t. For printing to be efficient (roughly
O(n)), the support must be pre-computed in a bottom-up fashion,
and then passed into each subterm in a top-down fashion (rather
than re-computing it at each level, which would be O(n²)). For
this reason, open_for_printing takes the support of t as an
additional argument, and provides sup', the support of s, as an
additional parameter to the body.
The correct use of this function is subject to Pitts's freshness condition.
NominalSupport instances
Most of the time, instances of NominalSupport should be derived using
deriving (Generic, NominalSupport), as in this example:
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveAnyClass #-}
data Term = Var Atom | App Term Term | Abs (Bind Atom Term)
deriving (Generic, NominalSupport)In the case of non-nominal types (typically base types such as
Double), a NominalSupport instance can be defined using
basic_support:
instance NominalSupport MyType where support = basic_support
basic_support :: t -> Support Source #
A helper function for defining NominalSupport instances
for non-nominal types.
Generic programming for NominalSupport
class GNominalSupport f where Source #
A version of the NominalSupport class suitable for generic programming.
Instances
| GNominalSupport (V1 :: Type -> Type) Source # | |
| GNominalSupport (U1 :: Type -> Type) Source # | |
| NominalSupport a => GNominalSupport (K1 i a :: Type -> Type) Source # | |
| (GNominalSupport a, GNominalSupport b) => GNominalSupport (a :+: b) Source # | |
| (GNominalSupport a, GNominalSupport b) => GNominalSupport (a :*: b) Source # | |
| GNominalSupport a => GNominalSupport (M1 i c a) Source # | |