Unbound.LocallyNameless.Alpha

Documentation

class (Show a, Rep1 AlphaD a) => Alpha a where

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.

Minimal complete definition

Nothing

Methods

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

See swaps.

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

See fv.

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

See lfreshen.

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

See freshen.

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

See aeq.

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

See acompare.

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

Replace free names by bound names.

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

Replace bound names by free names.

isPat :: a -> Maybe [AnyName]

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

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

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

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

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

Instances

Alpha Bool

Alpha Char

Alpha Double

Alpha Float

Alpha Int

Alpha Integer

Alpha ()

Alpha AnyName

Alpha a => Alpha [a]

Rep a => Alpha (R a)

Alpha a => Alpha (Maybe a)

Rep a => Alpha (Name a)

Alpha a => Alpha (Shift a)

Alpha t => Alpha (Embed t)

Alpha p => Alpha (Rec p)

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

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

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

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

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

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

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

class IsEmbed e where

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

Associated Types

type Embedded e :: *

Methods

embed :: Embedded e -> e

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

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)

IsEmbed (Embed t)

data FindResult

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

Ord FindResult

Show FindResult

Monoid FindResult

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

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

data NthResult

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

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

Fields

runNthCont :: Integer -> NthResult

Instances

Monoid NthCont

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

nthName :: AnyName -> NthCont

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

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

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

mode :: Mode

level :: Integer

initial :: AlphaCtx

incr :: AlphaCtx -> AlphaCtx

decr :: AlphaCtx -> AlphaCtx

pat :: AlphaCtx -> AlphaCtx

term :: AlphaCtx -> AlphaCtx

data Mode

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

Instances

Eq Mode

Read Mode

Show Mode

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

Open a term using the given pattern.

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

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

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

Close a term using the given pattern.

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

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

data AlphaD a

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

isPatD :: a -> Maybe [AnyName]

isTermD :: a -> Bool

isEmbedD :: a -> Bool

swapsD :: AlphaCtx -> Perm AnyName -> a -> a

fvD :: forall f. Collection f => AlphaCtx -> a -> f AnyName

freshenD :: forall m. Fresh m => AlphaCtx -> a -> m (a, Perm AnyName)

lfreshenD :: forall m b. LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b

aeqD :: AlphaCtx -> a -> a -> Bool

acompareD :: AlphaCtx -> a -> a -> Ordering

closeD :: forall b. Alpha b => AlphaCtx -> b -> a -> a

openD :: forall b. Alpha b => AlphaCtx -> b -> a -> a

findpatD :: a -> AnyName -> FindResult

nthpatD :: a -> NthCont

Instances

Alpha a => Sat (AlphaD a)

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

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

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

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

fv1 :: Collection f => MTup AlphaD l -> AlphaCtx -> l -> f AnyName

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

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

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

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

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

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

findpatR1 :: R1 AlphaD b -> b -> AnyName -> FindResult

findpatL :: MTup AlphaD l -> l -> AnyName -> FindResult

nthpatR1 :: R1 AlphaD b -> b -> NthCont

nthpatL :: MTup AlphaD l -> l -> NthCont

combine :: Maybe [AnyName] -> Maybe [AnyName] -> Maybe [AnyName]

isPatR1 :: R1 AlphaD b -> b -> Maybe [AnyName]

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

acompareR1 :: R1 AlphaD a -> AlphaCtx -> a -> a -> Ordering

compareTupM :: MTup AlphaD l -> AlphaCtx -> l -> l -> Ordering