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

PortabilityGHC only (-XKitchenSink)
MaintainerBrent Yorgey <byorgey@cis.upenn.edu>
Safe HaskellSafe-Infered

Unbound.LocallyNameless.Alpha

Description

 

Synopsis

Documentation

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

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.

Methods

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

See swaps.

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

See fv.

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

See lfreshen.

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

See freshen.

aeq' :: AlphaCtx -> a -> a -> BoolSource

See aeq.

acompare' :: AlphaCtx -> a -> a -> OrderingSource

See acompare.

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

Replace free names by bound names.

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

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 -> BoolSource

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

isEmbed :: a -> BoolSource

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 -> NthContSource

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 -> FindResultSource

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 whereSource

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

Associated Types

type Embedded e :: *Source

Methods

embed :: Embedded e -> eSource

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 eSource

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

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

and so on.

Instances

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 
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 IntegerSource

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

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

nthName :: AnyName -> NthContSource

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 -> AnyNameSource

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

mode :: Mode
 
level :: Integer
 

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 

Instances

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

Open a term using the given pattern.

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

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

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

Close a term using the given pattern.

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

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

isPatD :: a -> Maybe [AnyName]
 
isTermD :: a -> Bool
 
isEmbedD :: a -> Bool
 
swapsD :: AlphaCtx -> Perm AnyName -> a -> a
 
fvD :: Collection f => AlphaCtx -> a -> f AnyName
 
freshenD :: Fresh m => AlphaCtx -> a -> m (a, Perm AnyName)
 
lfreshenD :: LFresh m => AlphaCtx -> a -> (a -> Perm AnyName -> m b) -> m b
 
aeqD :: AlphaCtx -> a -> a -> Bool
 
acompareD :: AlphaCtx -> a -> a -> Ordering
 
closeD :: Alpha b => AlphaCtx -> b -> a -> a
 
openD :: 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 -> aSource

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

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

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

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

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

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

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