unbound-0.5.0: Generic support for programming with names and binders

LicenseBSD-like (see LICENSE)
MaintainerStephanie Weirich <sweirich@cis.upenn.edu>
PortabilityGHC only (-XKitchenSink)
Safe HaskellNone
LanguageHaskell2010

Unbound.LocallyNameless.Alpha

Description

 

Synopsis

Documentation

class Rep1 AlphaD a => Alpha a where Source #

The Alpha type class is for types which may contain names. The Rep1 constraint means that we can only make instances of this class for types that have generic representations (which can be automatically derived by RepLib.)

Note that the methods of Alpha should almost never be called directly. Instead, use other methods provided by this module which are defined in terms of Alpha methods.

Most of the time, the default definitions of these methods will suffice, so you can make an instance for your data type by simply declaring

instance Alpha MyType

Occasionally, however, it may be useful to override the default implementations of one or more Alpha methods for a particular type. For example, consider a type like

data Term = ...
          | Annotation Stuff Term

where the Annotation constructor of Term associates some sort of annotation with a term --- say, information obtained from a parser about where in an input file the term came from. This information is needed to produce good error messages, but should not be taken into consideration when, say, comparing two Terms for alpha-equivalence. In order to make aeq ignore annotations, you can override the implementation of aeq' like so:

instance Alpha Term where
  aeq' c (Annotation _ t1) t2 = aeq' c t1 t2
  aeq' c t1 (Annotation _ t2) = aeq' c t1 t2
  aeq' c t1 t2 = aeqR1 rep1 t1 t2

Note how the call to aeqR1 handles all the other cases generically.

If you use Abstract types (i.e. those with representations derived via derive_abstract) then you must provide a definition of aeq' and acompare'. In these cases, Unbound has no information about the structure of the type and cannot do anything sensible.

Methods

swaps' :: AlphaCtx -> Perm AnyName -> a -> a Source #

See swaps.

fv' :: Collection f => AlphaCtx -> a -> f AnyName Source #

See fv.

lfreshen' :: LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b Source #

See lfreshen.

freshen' :: Fresh m => AlphaCtx -> a -> m (a, Perm AnyName) Source #

See freshen.

aeq' :: AlphaCtx -> a -> a -> Bool Source #

See aeq.

acompare' :: AlphaCtx -> a -> a -> Ordering Source #

See acompare.

close :: Alpha b => AlphaCtx -> b -> a -> a Source #

Replace free names by bound names.

open :: Alpha b => AlphaCtx -> b -> a -> a Source #

Replace bound names by free names.

isPat :: a -> Maybe [AnyName] Source #

isPat x dynamically checks whether x can be used as a valid pattern. The default instance returns Just if at all possible. If successful, returns a list of names bound by the pattern.

isTerm :: a -> Bool Source #

isTerm x dynamically checks whether x can be used as a valid term. The default instance returns True if at all possible.

isEmbed :: a -> Bool Source #

isEmbed is needed internally for the implementation of isPat. isEmbed is true for terms wrapped in Embed and zero or more occurrences of Shift. The default implementation simply returns False.

nthpatrec :: a -> NthCont Source #

nthpatrec p n looks up the nth name in the pattern p (zero-indexed), returning the number of names encountered if not found.

findpatrec :: a -> AnyName -> FindResult Source #

Find the (first) index of the name in the pattern if one exists; otherwise, return the number of names encountered instead.

Instances

Alpha Bool Source # 
Alpha Char Source # 
Alpha Double Source # 
Alpha Float Source # 
Alpha Int Source # 
Alpha Integer Source # 
Alpha () Source # 

Methods

swaps' :: AlphaCtx -> Perm AnyName -> () -> () Source #

fv' :: Collection f => AlphaCtx -> () -> f AnyName Source #

lfreshen' :: LFresh m => AlphaCtx -> () -> (() -> Perm AnyName -> m b) -> m b Source #

freshen' :: Fresh m => AlphaCtx -> () -> m ((), Perm AnyName) Source #

aeq' :: AlphaCtx -> () -> () -> Bool Source #

acompare' :: AlphaCtx -> () -> () -> Ordering Source #

close :: Alpha b => AlphaCtx -> b -> () -> () Source #

open :: Alpha b => AlphaCtx -> b -> () -> () Source #

isPat :: () -> Maybe [AnyName] Source #

isTerm :: () -> Bool Source #

isEmbed :: () -> Bool Source #

nthpatrec :: () -> NthCont Source #

findpatrec :: () -> AnyName -> FindResult Source #

Alpha AnyName Source # 
Alpha a => Alpha [a] Source # 

Methods

swaps' :: AlphaCtx -> Perm AnyName -> [a] -> [a] Source #

fv' :: Collection f => AlphaCtx -> [a] -> f AnyName Source #

lfreshen' :: LFresh m => AlphaCtx -> [a] -> ([a] -> Perm AnyName -> m b) -> m b Source #

freshen' :: Fresh m => AlphaCtx -> [a] -> m ([a], Perm AnyName) Source #

aeq' :: AlphaCtx -> [a] -> [a] -> Bool Source #

acompare' :: AlphaCtx -> [a] -> [a] -> Ordering Source #

close :: Alpha b => AlphaCtx -> b -> [a] -> [a] Source #

open :: Alpha b => AlphaCtx -> b -> [a] -> [a] Source #

isPat :: [a] -> Maybe [AnyName] Source #

isTerm :: [a] -> Bool Source #

isEmbed :: [a] -> Bool Source #

nthpatrec :: [a] -> NthCont Source #

findpatrec :: [a] -> AnyName -> FindResult Source #

Alpha a => Alpha (Maybe a) Source # 
Rep a => Alpha (R a) Source # 

Methods

swaps' :: AlphaCtx -> Perm AnyName -> R a -> R a Source #

fv' :: Collection f => AlphaCtx -> R a -> f AnyName Source #

lfreshen' :: LFresh m => AlphaCtx -> R a -> (R a -> Perm AnyName -> m b) -> m b Source #

freshen' :: Fresh m => AlphaCtx -> R a -> m (R a, Perm AnyName) Source #

aeq' :: AlphaCtx -> R a -> R a -> Bool Source #

acompare' :: AlphaCtx -> R a -> R a -> Ordering Source #

close :: Alpha b => AlphaCtx -> b -> R a -> R a Source #

open :: Alpha b => AlphaCtx -> b -> R a -> R a Source #

isPat :: R a -> Maybe [AnyName] Source #

isTerm :: R a -> Bool Source #

isEmbed :: R a -> Bool Source #

nthpatrec :: R a -> NthCont Source #

findpatrec :: R a -> AnyName -> FindResult Source #

Rep a => Alpha (Name a) Source # 

Methods

swaps' :: AlphaCtx -> Perm AnyName -> Name a -> Name a Source #

fv' :: Collection f => AlphaCtx -> Name a -> f AnyName Source #

lfreshen' :: LFresh m => AlphaCtx -> Name a -> (Name a -> Perm AnyName -> m b) -> m b Source #

freshen' :: Fresh m => AlphaCtx -> Name a -> m (Name a, Perm AnyName) Source #

aeq' :: AlphaCtx -> Name a -> Name a -> Bool Source #

acompare' :: AlphaCtx -> Name a -> Name a -> Ordering Source #

close :: Alpha b => AlphaCtx -> b -> Name a -> Name a Source #

open :: Alpha b => AlphaCtx -> b -> Name a -> Name a Source #

isPat :: Name a -> Maybe [AnyName] Source #

isTerm :: Name a -> Bool Source #

isEmbed :: Name a -> Bool Source #

nthpatrec :: Name a -> NthCont Source #

findpatrec :: Name a -> AnyName -> FindResult Source #

Alpha a => Alpha (Shift a) Source # 
Alpha t => Alpha (Embed t) Source # 
Alpha p => Alpha (Rec p) Source # 

Methods

swaps' :: AlphaCtx -> Perm AnyName -> Rec p -> Rec p Source #

fv' :: Collection f => AlphaCtx -> Rec p -> f AnyName Source #

lfreshen' :: LFresh m => AlphaCtx -> Rec p -> (Rec p -> Perm AnyName -> m b) -> m b Source #

freshen' :: Fresh m => AlphaCtx -> Rec p -> m (Rec p, Perm AnyName) Source #

aeq' :: AlphaCtx -> Rec p -> Rec p -> Bool Source #

acompare' :: AlphaCtx -> Rec p -> Rec p -> Ordering Source #

close :: Alpha b => AlphaCtx -> b -> Rec p -> Rec p Source #

open :: Alpha b => AlphaCtx -> b -> Rec p -> Rec p Source #

isPat :: Rec p -> Maybe [AnyName] Source #

isTerm :: Rec p -> Bool Source #

isEmbed :: Rec p -> Bool Source #

nthpatrec :: Rec p -> NthCont Source #

findpatrec :: Rec p -> AnyName -> FindResult Source #

(Alpha a, Alpha b) => Alpha (Either a b) Source # 

Methods

swaps' :: AlphaCtx -> Perm AnyName -> Either a b -> Either a b Source #

fv' :: Collection f => AlphaCtx -> Either a b -> f AnyName Source #

lfreshen' :: LFresh m => AlphaCtx -> Either a b -> (Either a b -> Perm AnyName -> m b) -> m b Source #

freshen' :: Fresh m => AlphaCtx -> Either a b -> m (Either a b, Perm AnyName) Source #

aeq' :: AlphaCtx -> Either a b -> Either a b -> Bool Source #

acompare' :: AlphaCtx -> Either a b -> Either a b -> Ordering Source #

close :: Alpha b => AlphaCtx -> b -> Either a b -> Either a b Source #

open :: Alpha b => AlphaCtx -> b -> Either a b -> Either a b Source #

isPat :: Either a b -> Maybe [AnyName] Source #

isTerm :: Either a b -> Bool Source #

isEmbed :: Either a b -> Bool Source #

nthpatrec :: Either a b -> NthCont Source #

findpatrec :: Either a b -> AnyName -> FindResult Source #

(Alpha a, Alpha b) => Alpha (a, b) Source # 

Methods

swaps' :: AlphaCtx -> Perm AnyName -> (a, b) -> (a, b) Source #

fv' :: Collection f => AlphaCtx -> (a, b) -> f AnyName Source #

lfreshen' :: LFresh m => AlphaCtx -> (a, b) -> ((a, b) -> Perm AnyName -> m b) -> m b Source #

freshen' :: Fresh m => AlphaCtx -> (a, b) -> m ((a, b), Perm AnyName) Source #

aeq' :: AlphaCtx -> (a, b) -> (a, b) -> Bool Source #

acompare' :: AlphaCtx -> (a, b) -> (a, b) -> Ordering Source #

close :: Alpha b => AlphaCtx -> b -> (a, b) -> (a, b) Source #

open :: Alpha b => AlphaCtx -> b -> (a, b) -> (a, b) Source #

isPat :: (a, b) -> Maybe [AnyName] Source #

isTerm :: (a, b) -> Bool Source #

isEmbed :: (a, b) -> Bool Source #

nthpatrec :: (a, b) -> NthCont Source #

findpatrec :: (a, b) -> AnyName -> FindResult Source #

(Alpha p, Alpha q) => Alpha (Rebind p q) Source # 

Methods

swaps' :: AlphaCtx -> Perm AnyName -> Rebind p q -> Rebind p q Source #

fv' :: Collection f => AlphaCtx -> Rebind p q -> f AnyName Source #

lfreshen' :: LFresh m => AlphaCtx -> Rebind p q -> (Rebind p q -> Perm AnyName -> m b) -> m b Source #

freshen' :: Fresh m => AlphaCtx -> Rebind p q -> m (Rebind p q, Perm AnyName) Source #

aeq' :: AlphaCtx -> Rebind p q -> Rebind p q -> Bool Source #

acompare' :: AlphaCtx -> Rebind p q -> Rebind p q -> Ordering Source #

close :: Alpha b => AlphaCtx -> b -> Rebind p q -> Rebind p q Source #

open :: Alpha b => AlphaCtx -> b -> Rebind p q -> Rebind p q Source #

isPat :: Rebind p q -> Maybe [AnyName] Source #

isTerm :: Rebind p q -> Bool Source #

isEmbed :: Rebind p q -> Bool Source #

nthpatrec :: Rebind p q -> NthCont Source #

findpatrec :: Rebind p q -> AnyName -> FindResult Source #

(Alpha a, Alpha b, Alpha c) => Alpha (a, b, c) Source # 

Methods

swaps' :: AlphaCtx -> Perm AnyName -> (a, b, c) -> (a, b, c) Source #

fv' :: Collection f => AlphaCtx -> (a, b, c) -> f AnyName Source #

lfreshen' :: LFresh m => AlphaCtx -> (a, b, c) -> ((a, b, c) -> Perm AnyName -> m b) -> m b Source #

freshen' :: Fresh m => AlphaCtx -> (a, b, c) -> m ((a, b, c), Perm AnyName) Source #

aeq' :: AlphaCtx -> (a, b, c) -> (a, b, c) -> Bool Source #

acompare' :: AlphaCtx -> (a, b, c) -> (a, b, c) -> Ordering Source #

close :: Alpha b => AlphaCtx -> b -> (a, b, c) -> (a, b, c) Source #

open :: Alpha b => AlphaCtx -> b -> (a, b, c) -> (a, b, c) Source #

isPat :: (a, b, c) -> Maybe [AnyName] Source #

isTerm :: (a, b, c) -> Bool Source #

isEmbed :: (a, b, c) -> Bool Source #

nthpatrec :: (a, b, c) -> NthCont Source #

findpatrec :: (a, b, c) -> AnyName -> FindResult Source #

(Alpha a, Alpha b, Alpha c, Alpha d) => Alpha (a, b, c, d) Source # 

Methods

swaps' :: AlphaCtx -> Perm AnyName -> (a, b, c, d) -> (a, b, c, d) Source #

fv' :: Collection f => AlphaCtx -> (a, b, c, d) -> f AnyName Source #

lfreshen' :: LFresh m => AlphaCtx -> (a, b, c, d) -> ((a, b, c, d) -> Perm AnyName -> m b) -> m b Source #

freshen' :: Fresh m => AlphaCtx -> (a, b, c, d) -> m ((a, b, c, d), Perm AnyName) Source #

aeq' :: AlphaCtx -> (a, b, c, d) -> (a, b, c, d) -> Bool Source #

acompare' :: AlphaCtx -> (a, b, c, d) -> (a, b, c, d) -> Ordering Source #

close :: Alpha b => AlphaCtx -> b -> (a, b, c, d) -> (a, b, c, d) Source #

open :: Alpha b => AlphaCtx -> b -> (a, b, c, d) -> (a, b, c, d) Source #

isPat :: (a, b, c, d) -> Maybe [AnyName] Source #

isTerm :: (a, b, c, d) -> Bool Source #

isEmbed :: (a, b, c, d) -> Bool Source #

nthpatrec :: (a, b, c, d) -> NthCont Source #

findpatrec :: (a, b, c, d) -> AnyName -> FindResult Source #

(Rep order, Rep card, Alpha p, Alpha t) => Alpha (GenBind order card p t) Source # 

Methods

swaps' :: AlphaCtx -> Perm AnyName -> GenBind order card p t -> GenBind order card p t Source #

fv' :: Collection f => AlphaCtx -> GenBind order card p t -> f AnyName Source #

lfreshen' :: LFresh m => AlphaCtx -> GenBind order card p t -> (GenBind order card p t -> Perm AnyName -> m b) -> m b Source #

freshen' :: Fresh m => AlphaCtx -> GenBind order card p t -> m (GenBind order card p t, Perm AnyName) Source #

aeq' :: AlphaCtx -> GenBind order card p t -> GenBind order card p t -> Bool Source #

acompare' :: AlphaCtx -> GenBind order card p t -> GenBind order card p t -> Ordering Source #

close :: Alpha b => AlphaCtx -> b -> GenBind order card p t -> GenBind order card p t Source #

open :: Alpha b => AlphaCtx -> b -> GenBind order card p t -> GenBind order card p t Source #

isPat :: GenBind order card p t -> Maybe [AnyName] Source #

isTerm :: GenBind order card p t -> Bool Source #

isEmbed :: GenBind order card p t -> Bool Source #

nthpatrec :: GenBind order card p t -> NthCont Source #

findpatrec :: GenBind order card p t -> AnyName -> FindResult Source #

(Alpha a, Alpha b, Alpha c, Alpha d, Alpha e) => Alpha (a, b, c, d, e) Source # 

Methods

swaps' :: AlphaCtx -> Perm AnyName -> (a, b, c, d, e) -> (a, b, c, d, e) Source #

fv' :: Collection f => AlphaCtx -> (a, b, c, d, e) -> f AnyName Source #

lfreshen' :: LFresh m => AlphaCtx -> (a, b, c, d, e) -> ((a, b, c, d, e) -> Perm AnyName -> m b) -> m b Source #

freshen' :: Fresh m => AlphaCtx -> (a, b, c, d, e) -> m ((a, b, c, d, e), Perm AnyName) Source #

aeq' :: AlphaCtx -> (a, b, c, d, e) -> (a, b, c, d, e) -> Bool Source #

acompare' :: AlphaCtx -> (a, b, c, d, e) -> (a, b, c, d, e) -> Ordering Source #

close :: Alpha b => AlphaCtx -> b -> (a, b, c, d, e) -> (a, b, c, d, e) Source #

open :: Alpha b => AlphaCtx -> b -> (a, b, c, d, e) -> (a, b, c, d, e) Source #

isPat :: (a, b, c, d, e) -> Maybe [AnyName] Source #

isTerm :: (a, b, c, d, e) -> Bool Source #

isEmbed :: (a, b, c, d, e) -> Bool Source #

nthpatrec :: (a, b, c, d, e) -> NthCont Source #

findpatrec :: (a, b, c, d, e) -> AnyName -> FindResult Source #

class IsEmbed e where Source #

Type class for embedded terms (either Embed or Shift).

Minimal complete definition

embed, unembed

Associated Types

type Embedded e :: * Source #

Methods

embed :: Embedded e -> e Source #

Construct an embedded term, which is an instance of Embed with any number of enclosing Shifts. That is, embed can have any of the types

  • t -> Embed t
  • t -> Shift (Embed t)
  • t -> Shift (Shift (Embed t))

and so on.

unembed :: e -> Embedded e Source #

Destruct an embedded term. unembed can have any of the types

  • Embed t -> t
  • Shift (Embed t) -> t

and so on.

Instances

IsEmbed e => IsEmbed (Shift e) Source # 

Associated Types

type Embedded (Shift e) :: * Source #

IsEmbed (Embed t) Source # 

Associated Types

type Embedded (Embed t) :: * Source #

data FindResult Source #

The result of a findpatrec operation.

Constructors

Index Integer

The (first) index of the name we sought

NamesSeen Integer

We haven't found the name (yet), but have seen this many others while looking for it

Instances

Eq FindResult Source # 
Ord FindResult Source # 
Monoid FindResult Source #

FindResult forms a monoid which combines information from several findpatrec operations. mappend takes the leftmost Index, and combines the number of names seen to the left of it so we can correctly compute its global index.

findpat :: Alpha a => a -> AnyName -> Maybe Integer Source #

Find the (first) index of the name in the pattern, if it exists.

data NthResult Source #

The result of an nthpatrec operation.

Constructors

Found AnyName

The name found at the given index.

CurIndex Integer

We haven't yet reached the required index; this is the index into the remainder of the pattern (which decreases as we traverse the pattern).

newtype NthCont Source #

A continuation which takes the remaining index and searches for that location in a pattern, yielding a name or a remaining index if the end of the pattern was reached too soon.

Constructors

NthCont 

Instances

Monoid NthCont Source #

NthCont forms a monoid: function composition which short-circuits once a result is found.

nthName :: AnyName -> NthCont Source #

If we see a name, check whether the index is 0: if it is, we've found the name we're looking for, otherwise continue with a decremented index.

nthpat :: Alpha a => a -> Integer -> AnyName Source #

nthpat b n looks up up the nth name in the pattern b (zero-indexed). PRECONDITION: the number of names in the pattern must be at least n.

data AlphaCtx Source #

Many of the operations in the Alpha class take an AlphaCtx: stored information about the iteration as it progresses. This type is abstract, as classes that override these operations should just pass the context on.

Constructors

AC 

Fields

initial :: AlphaCtx Source #

Toplevel alpha-contexts

incr :: AlphaCtx -> AlphaCtx Source #

Call when going under a binder

decr :: AlphaCtx -> AlphaCtx Source #

Call when going in an embedding

pat :: AlphaCtx -> AlphaCtx Source #

Call when entering a pattern

term :: AlphaCtx -> AlphaCtx Source #

Call when entering a term embedded in a pattern

data Mode Source #

A mode is basically a flag that tells us whether we should be looking at the names in the term, or if we are in a pattern and should only be looking at the names in the annotations. The standard mode is to use Term; many functions do this by default.

Constructors

Term 
Pat 

openT :: (Alpha p, Alpha t) => p -> t -> t Source #

Open a term using the given pattern.

openP :: (Alpha p1, Alpha p2) => p1 -> p2 -> p2 Source #

openP p1 p2 opens the pattern p2 using the pattern p1.

closeT :: (Alpha p, Alpha t) => p -> t -> t Source #

Close a term using the given pattern.

closeP :: (Alpha p1, Alpha p2) => p1 -> p2 -> p2 Source #

closeP p1 p2 closes the pattern p2 using the pattern p1.

data AlphaD a Source #

Class constraint hackery to allow us to override the default definitions for certain classes. AlphaD is essentially a reified dictionary for the Alpha class.

Constructors

AlphaD 

Fields

Instances

Alpha a => Sat (AlphaD a) Source # 

Methods

dict :: AlphaD a #

closeR1 :: Alpha b => R1 AlphaD a -> AlphaCtx -> b -> a -> a Source #

Generic version of close

openR1 :: Alpha b => R1 AlphaD a -> AlphaCtx -> b -> a -> a Source #

Generic version of open

swapsR1 :: R1 AlphaD a -> AlphaCtx -> Perm AnyName -> a -> a Source #

Generic version of swaps

fvR1 :: Collection f => R1 AlphaD a -> AlphaCtx -> a -> f AnyName Source #

Generic version of fv

aeqR1 :: R1 AlphaD a -> AlphaCtx -> a -> a -> Bool Source #

Generic version of aeq

aeq1 :: MTup AlphaD l -> AlphaCtx -> l -> l -> Bool Source #

Generic list version of aeq

freshenR1 :: Fresh m => R1 AlphaD a -> AlphaCtx -> a -> m (a, Perm AnyName) Source #

Generic version of freshen

freshenL :: Fresh m => MTup AlphaD l -> AlphaCtx -> l -> m (l, Perm AnyName) Source #

Generic list version of freshen

lfreshenR1 :: LFresh m => R1 AlphaD a -> AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b Source #

lfreshenL :: LFresh m => MTup AlphaD l -> AlphaCtx -> l -> (l -> Perm AnyName -> m b) -> m b Source #

isTermR1 :: R1 AlphaD b -> b -> Bool Source #