Unbound.LocallyNameless.Alpha

Documentation

class 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.

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

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

Defined in Unbound.LocallyNameless.Alpha

Methods

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

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

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

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

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

acompare' :: AlphaCtx -> Bool -> Bool -> Ordering

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

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

isPat :: Bool -> Maybe [AnyName]

isTerm :: Bool -> Bool

isEmbed :: Bool -> Bool

nthpatrec :: Bool -> NthCont

findpatrec :: Bool -> AnyName -> FindResult

Alpha Char

Defined in Unbound.LocallyNameless.Alpha

Methods

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

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

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

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

aeq' :: AlphaCtx -> Char -> Char -> Bool

acompare' :: AlphaCtx -> Char -> Char -> Ordering

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

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

isPat :: Char -> Maybe [AnyName]

isTerm :: Char -> Bool

isEmbed :: Char -> Bool

nthpatrec :: Char -> NthCont

findpatrec :: Char -> AnyName -> FindResult

Alpha Double

Defined in Unbound.LocallyNameless.Alpha

Methods

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

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

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

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

aeq' :: AlphaCtx -> Double -> Double -> Bool

acompare' :: AlphaCtx -> Double -> Double -> Ordering

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

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

isPat :: Double -> Maybe [AnyName]

isTerm :: Double -> Bool

isEmbed :: Double -> Bool

nthpatrec :: Double -> NthCont

findpatrec :: Double -> AnyName -> FindResult

Alpha Float

Defined in Unbound.LocallyNameless.Alpha

Methods

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

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

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

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

aeq' :: AlphaCtx -> Float -> Float -> Bool

acompare' :: AlphaCtx -> Float -> Float -> Ordering

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

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

isPat :: Float -> Maybe [AnyName]

isTerm :: Float -> Bool

isEmbed :: Float -> Bool

nthpatrec :: Float -> NthCont

findpatrec :: Float -> AnyName -> FindResult

Alpha Int

Defined in Unbound.LocallyNameless.Alpha

Methods

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

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

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

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

aeq' :: AlphaCtx -> Int -> Int -> Bool

acompare' :: AlphaCtx -> Int -> Int -> Ordering

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

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

isPat :: Int -> Maybe [AnyName]

isTerm :: Int -> Bool

isEmbed :: Int -> Bool

nthpatrec :: Int -> NthCont

findpatrec :: Int -> AnyName -> FindResult

Alpha Integer

Defined in Unbound.LocallyNameless.Alpha

Methods

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

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

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

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

aeq' :: AlphaCtx -> Integer -> Integer -> Bool

acompare' :: AlphaCtx -> Integer -> Integer -> Ordering

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

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

isPat :: Integer -> Maybe [AnyName]

isTerm :: Integer -> Bool

isEmbed :: Integer -> Bool

nthpatrec :: Integer -> NthCont

findpatrec :: Integer -> AnyName -> FindResult

Alpha ()

Defined in Unbound.LocallyNameless.Alpha

Methods

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

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

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

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

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

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

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

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

isPat :: () -> Maybe [AnyName]

isTerm :: () -> Bool

isEmbed :: () -> Bool

nthpatrec :: () -> NthCont

findpatrec :: () -> AnyName -> FindResult

Alpha AnyName

Defined in Unbound.LocallyNameless.Alpha

Methods

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

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

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

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

aeq' :: AlphaCtx -> AnyName -> AnyName -> Bool

acompare' :: AlphaCtx -> AnyName -> AnyName -> Ordering

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

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

isPat :: AnyName -> Maybe [AnyName]

isTerm :: AnyName -> Bool

isEmbed :: AnyName -> Bool

nthpatrec :: AnyName -> NthCont

findpatrec :: AnyName -> AnyName -> FindResult

Alpha a => Alpha [a]

Defined in Unbound.LocallyNameless.Alpha

Methods

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

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

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

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

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

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

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

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

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

isTerm :: [a] -> Bool

isEmbed :: [a] -> Bool

nthpatrec :: [a] -> NthCont

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

Alpha a => Alpha (Maybe a)

Defined in Unbound.LocallyNameless.Alpha

Methods

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

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

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

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

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

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

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

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

isPat :: Maybe a -> Maybe [AnyName]

isTerm :: Maybe a -> Bool

isEmbed :: Maybe a -> Bool

nthpatrec :: Maybe a -> NthCont

findpatrec :: Maybe a -> AnyName -> FindResult

Rep a => Alpha (R a)

Defined in Unbound.LocallyNameless.Alpha

Methods

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

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

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

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

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

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

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

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

isPat :: R a -> Maybe [AnyName]

isTerm :: R a -> Bool

isEmbed :: R a -> Bool

nthpatrec :: R a -> NthCont

findpatrec :: R a -> AnyName -> FindResult

Rep a => Alpha (Name a)

Defined in Unbound.LocallyNameless.Alpha

Methods

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

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

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

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

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

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

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

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

isPat :: Name a -> Maybe [AnyName]

isTerm :: Name a -> Bool

isEmbed :: Name a -> Bool

nthpatrec :: Name a -> NthCont

findpatrec :: Name a -> AnyName -> FindResult

Alpha a => Alpha (Shift a)

Defined in Unbound.LocallyNameless.Alpha

Methods

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

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

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

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

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

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

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

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

isPat :: Shift a -> Maybe [AnyName]

isTerm :: Shift a -> Bool

isEmbed :: Shift a -> Bool

nthpatrec :: Shift a -> NthCont

findpatrec :: Shift a -> AnyName -> FindResult

Alpha t => Alpha (Embed t)

Defined in Unbound.LocallyNameless.Alpha

Methods

swaps' :: AlphaCtx -> Perm AnyName -> Embed t -> Embed t

fv' :: Collection f => AlphaCtx -> Embed t -> f AnyName

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

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

aeq' :: AlphaCtx -> Embed t -> Embed t -> Bool

acompare' :: AlphaCtx -> Embed t -> Embed t -> Ordering

close :: Alpha b => AlphaCtx -> b -> Embed t -> Embed t

open :: Alpha b => AlphaCtx -> b -> Embed t -> Embed t

isPat :: Embed t -> Maybe [AnyName]

isTerm :: Embed t -> Bool

isEmbed :: Embed t -> Bool

nthpatrec :: Embed t -> NthCont

findpatrec :: Embed t -> AnyName -> FindResult

Alpha p => Alpha (Rec p)

Defined in Unbound.LocallyNameless.Alpha

Methods

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

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

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

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

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

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

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

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

isPat :: Rec p -> Maybe [AnyName]

isTerm :: Rec p -> Bool

isEmbed :: Rec p -> Bool

nthpatrec :: Rec p -> NthCont

findpatrec :: Rec p -> AnyName -> FindResult

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

Defined in Unbound.LocallyNameless.Alpha

Methods

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

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

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

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

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

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

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

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

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

isTerm :: Either a b -> Bool

isEmbed :: Either a b -> Bool

nthpatrec :: Either a b -> NthCont

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

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

Defined in Unbound.LocallyNameless.Alpha

Methods

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

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

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

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

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

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

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

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

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

isTerm :: (a, b) -> Bool

isEmbed :: (a, b) -> Bool

nthpatrec :: (a, b) -> NthCont

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

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

Defined in Unbound.LocallyNameless.Alpha

Methods

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

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

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

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

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

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

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

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

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

isTerm :: Rebind p q -> Bool

isEmbed :: Rebind p q -> Bool

nthpatrec :: Rebind p q -> NthCont

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

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

Defined in Unbound.LocallyNameless.Alpha

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Defined in Unbound.LocallyNameless.Alpha

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Defined in Unbound.LocallyNameless.Alpha

Methods

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

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

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

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

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

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

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

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

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

isTerm :: GenBind order card p t -> Bool

isEmbed :: GenBind order card p t -> Bool

nthpatrec :: GenBind order card p t -> NthCont

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

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

Defined in Unbound.LocallyNameless.Alpha

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

class IsEmbed e where

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

Minimal complete definition

embed, unembed

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)

Defined in Unbound.LocallyNameless.Alpha

Associated Types

type Embedded (Shift e) :: *

Methods

embed :: Embedded (Shift e) -> Shift e

unembed :: Shift e -> Embedded (Shift e)

IsEmbed (Embed t)

Defined in Unbound.LocallyNameless.Alpha

Associated Types

type Embedded (Embed t) :: *

Methods

embed :: Embedded (Embed t) -> Embed t

unembed :: Embed t -> Embedded (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

Defined in Unbound.LocallyNameless.Alpha

Methods

(==) :: FindResult -> FindResult -> Bool

(/=) :: FindResult -> FindResult -> Bool

Ord FindResult

Defined in Unbound.LocallyNameless.Alpha

Methods

compare :: FindResult -> FindResult -> Ordering

(<) :: FindResult -> FindResult -> Bool

(<=) :: FindResult -> FindResult -> Bool

(>) :: FindResult -> FindResult -> Bool

(>=) :: FindResult -> FindResult -> Bool

max :: FindResult -> FindResult -> FindResult

min :: FindResult -> FindResult -> FindResult

Semigroup FindResult

Defined in Unbound.LocallyNameless.Alpha

Methods

(<>) :: FindResult -> FindResult -> FindResult

sconcat :: NonEmpty FindResult -> FindResult

stimes :: Integral b => b -> FindResult -> 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.

Defined in Unbound.LocallyNameless.Alpha

Methods

mempty :: FindResult

mappend :: FindResult -> FindResult -> FindResult

mconcat :: [FindResult] -> FindResult

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

Semigroup NthCont

Defined in Unbound.LocallyNameless.Alpha

Methods

(<>) :: NthCont -> NthCont -> NthCont

sconcat :: NonEmpty NthCont -> NthCont

stimes :: Integral b => b -> NthCont -> NthCont

Monoid NthCont

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

Defined in Unbound.LocallyNameless.Alpha

Methods

mempty :: NthCont

mappend :: NthCont -> NthCont -> NthCont

mconcat :: [NthCont] -> NthCont

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

Toplevel alpha-contexts

incr :: AlphaCtx -> AlphaCtx

Call when going under a binder

decr :: AlphaCtx -> AlphaCtx

Call when going in an embedding

pat :: AlphaCtx -> AlphaCtx

Call when entering a pattern

term :: AlphaCtx -> AlphaCtx

Call when entering a term embedded in a pattern

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

Defined in Unbound.LocallyNameless.Alpha

Methods

(==) :: Mode -> Mode -> Bool

(/=) :: Mode -> Mode -> Bool

Read Mode

Defined in Unbound.LocallyNameless.Alpha

Methods

readsPrec :: Int -> ReadS Mode

readList :: ReadS [Mode]

readPrec :: ReadPrec Mode

readListPrec :: ReadPrec [Mode]

Show Mode

Defined in Unbound.LocallyNameless.Alpha

Methods

showsPrec :: Int -> Mode -> ShowS

show :: Mode -> String

showList :: [Mode] -> ShowS

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)

Defined in Unbound.LocallyNameless.Alpha

Methods

dict :: AlphaD a

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

Generic version of close

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

Generic version of open

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

Generic version of swaps

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

Generic version of fv

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

Generic version of aeq

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

Generic list version of aeq

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

Generic version of freshen

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

Generic list version of freshen

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