nominal-0.1.0.0: Binders and alpha-equivalence made easy

Safe HaskellNone
LanguageHaskell2010

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.

Synopsis

Literal strings

newtype Literal Source #

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.

Constructors

Literal String 

Support

data Avoidee Source #

Something to be avoided can be an atom or a string.

Constructors

A Atom 
S String 

newtype Support Source #

This type provides an internal representation for the support of a nominal term, i.e., the set of atoms (and constants) occurring in it. This is an abstract type with no exposed structure. The only way to construct a value of type Support is to use the function support.

Constructors

Support (Set Avoidee) 

support_empty :: Support Source #

The empty support.

support_unions :: [Support] -> Support Source #

The union of a list of supports.

support_union :: Support -> Support -> Support Source #

The union of two supports.

support_insert :: Atom -> Support -> Support Source #

Add an atom to the support.

support_atom :: Atom -> Support Source #

A singleton support.

support_delete :: Atom -> Support -> Support Source #

Delete an atom from the support.

support_deletes :: [Atom] -> Support -> Support Source #

Delete a list of atoms from the support.

support_string :: String -> Support Source #

Add a literal string to the support.

strings_of_support :: Support -> Set String Source #

Convert the support to a list of strings.

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.

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

NominalSupport Bool Source # 

Methods

support :: Bool -> Support Source #

NominalSupport Char Source # 

Methods

support :: Char -> Support Source #

NominalSupport Double Source # 
NominalSupport Float Source # 
NominalSupport Int Source # 

Methods

support :: Int -> Support Source #

NominalSupport Integer Source # 
NominalSupport () Source # 

Methods

support :: () -> Support Source #

NominalSupport Atom Source # 

Methods

support :: Atom -> Support Source #

NominalSupport Literal Source # 
NominalSupport t => NominalSupport [t] Source # 

Methods

support :: [t] -> Support Source #

(Ord k, NominalSupport k) => NominalSupport (Set k) Source # 

Methods

support :: Set k -> Support Source #

NominalSupport (Basic t) Source # 

Methods

support :: Basic t -> Support Source #

NominalSupport t => NominalSupport (BindAtom t) Source # 
NominalSupport t => NominalSupport (Defer t) Source # 

Methods

support :: Defer t -> Support Source #

NominalSupport t => NominalSupport (NoBind t) Source # 

Methods

support :: NoBind t -> Support Source #

AtomKind a => NominalSupport (AtomOfKind a) Source # 
(NominalSupport t, NominalSupport s) => NominalSupport (t, s) Source # 

Methods

support :: (t, s) -> Support Source #

(Ord k, NominalSupport k, NominalSupport v) => NominalSupport (Map k v) Source # 

Methods

support :: Map k v -> Support Source #

(Bindable a, NominalSupport a, NominalSupport t) => NominalSupport (Bind a t) Source # 

Methods

support :: Bind a t -> Support Source #

(NominalSupport t, NominalSupport s, NominalSupport r) => NominalSupport (t, s, r) Source # 

Methods

support :: (t, s, r) -> Support Source #

(NominalSupport t, NominalSupport s, NominalSupport r, NominalSupport q) => NominalSupport (t, s, r, q) Source # 

Methods

support :: (t, s, r, q) -> Support Source #

(NominalSupport t, NominalSupport s, NominalSupport r, NominalSupport q, NominalSupport p) => NominalSupport (t, s, r, q, p) Source # 

Methods

support :: (t, s, r, q, p) -> Support Source #

(NominalSupport t, NominalSupport s, NominalSupport r, NominalSupport q, NominalSupport p, NominalSupport o) => NominalSupport (t, s, r, q, p, o) Source # 

Methods

support :: (t, s, r, q, p, o) -> Support Source #

(NominalSupport t, NominalSupport s, NominalSupport r, NominalSupport q, NominalSupport p, NominalSupport o, NominalSupport n) => NominalSupport (t, s, r, q, p, o, n) Source # 

Methods

support :: (t, s, r, q, p, o, n) -> Support Source #

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.

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.

Minimal complete definition

gsupport

Methods

gsupport :: f a -> Support Source #