Unbound.Nominal.Internal

Documentation

(<>) :: Monoid m => m -> m -> m

rR1 :: forall ctx[a5EE] a[a1FY]. Rep a[a1FY] => R1 ctx[a5EE] (R a[a1FY])

rR :: forall a[a1FY]. Rep a[a1FY] => R (R a[a1FY])

data Bind a b

Type of a binding. Morally, the type a should be in the class Pattern and the type b should be in the class Alpha. The Pattern class contains the constructor and a safe destructor for these types. We can Bind an a object in a b object if we can create fresh a objects, and Names can be swapped in b objects. Often a is Name but that need not be the case.

Constructors

B a b

Instances

(Rep a[a5FT], Rep b[a5FU], Sat (ctx[a5QY] a[a5FT]), Sat (ctx[a5QY] b[a5FU])) => Rep1 ctx[a5QY] (Bind a[a5FT] b[a5FU])

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

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

(Show a, Show b) => Show (Bind a b)

(Rep a[a5FT], Rep b[a5FU]) => Rep (Bind a[a5FT] b[a5FU])

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

newtype Embed a

An annotation is a hole in a pattern where variables can be used, but not bound. For example patterns may include type annotations, and those annotations can reference variables without binding them. Annotations do nothing special when they appear elsewhere in terms

Constructors

Embed a

Instances

(Rep a[a5FS], Sat (ctx[a5QD] a[a5FS])) => Rep1 ctx[a5QD] (Embed a[a5FS])

Subst c a => Subst c (Embed a)

Eq a => Eq (Embed a)

Read a => Read (Embed a)

Show a => Show (Embed a)

Rep a[a5FS] => Rep (Embed a[a5FS])

(Eq a, Alpha a) => Alpha (Embed a)

newtype Shift a

Shift the scope of an embedded term one level outwards.

Constructors

Shift a

Instances

(Rep a[a5FR], Sat (ctx[a5Qa] a[a5FR])) => Rep1 ctx[a5Qa] (Shift a[a5FR])

Eq a => Eq (Shift a)

Rep a[a5FR] => Rep (Shift a[a5FR])

data Rebind a b

Rebinding is for telescopes --- i.e. to support patterns that also bind variables that appear later

Constructors

R a (Bind [AnyName] b)

Instances

(Rep a[a5FP], Rep b[a5FQ], Sat (ctx[a5Qq] a[a5FP]), Sat (ctx[a5Qq] (Bind [AnyName] b[a5FQ]))) => Rep1 ctx[a5Qq] (Rebind a[a5FP] b[a5FQ])

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

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

(Rep a[a5FP], Rep b[a5FQ]) => Rep (Rebind a[a5FP] b[a5FQ])

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

data Rec a

Rec supports recursive patterns --- that is, patterns where any variables anywhere in the pattern are bound in the pattern itself. Useful for lectrec (and Agda's dot notation).

Constructors

Rec a

Instances

(Rep a[a5FO], Sat (ctx[a5Qi] a[a5FO])) => Rep1 ctx[a5Qi] (Rec a[a5FO])

Show a => Show (Rec a)

Rep a[a5FO] => Rep (Rec a[a5FO])

rBind1 :: forall ctx[a5QY] a[a5FT] b[a5FU]. (Rep a[a5FT], Rep b[a5FU]) => ctx[a5QY] a[a5FT] -> ctx[a5QY] b[a5FU] -> R1 ctx[a5QY] (Bind a[a5FT] b[a5FU])

rBind :: forall a[a5FT] b[a5FU]. (Rep a[a5FT], Rep b[a5FU]) => R (Bind a[a5FT] b[a5FU])

rName1 :: forall ctx[a5QL] a[a1Ev]. Rep a[a1Ev] => ctx[a5QL] (R a[a1Ev]) -> ctx[a5QL] (String, Integer) -> R1 ctx[a5QL] (Name a[a1Ev])

rName :: forall a[a1Ev]. Rep a[a1Ev] => R (Name a[a1Ev])

rEmbed1 :: forall ctx[a5QD] a[a5FS]. Rep a[a5FS] => ctx[a5QD] a[a5FS] -> R1 ctx[a5QD] (Embed a[a5FS])

rEmbed :: forall a[a5FS]. Rep a[a5FS] => R (Embed a[a5FS])

rRebind1 :: forall ctx[a5Qq] a[a5FP] b[a5FQ]. (Rep a[a5FP], Rep b[a5FQ]) => ctx[a5Qq] a[a5FP] -> ctx[a5Qq] (Bind [AnyName] b[a5FQ]) -> R1 ctx[a5Qq] (Rebind a[a5FP] b[a5FQ])

rRebind :: forall a[a5FP] b[a5FQ]. (Rep a[a5FP], Rep b[a5FQ]) => R (Rebind a[a5FP] b[a5FQ])

rRec1 :: forall ctx[a5Qi] a[a5FO]. Rep a[a5FO] => ctx[a5Qi] a[a5FO] -> R1 ctx[a5Qi] (Rec a[a5FO])

rRec :: forall a[a5FO]. Rep a[a5FO] => R (Rec a[a5FO])

rShift1 :: forall ctx[a5Qa] a[a5FR]. Rep a[a5FR] => ctx[a5Qa] a[a5FR] -> R1 ctx[a5Qa] (Shift a[a5FR])

rShift :: forall a[a5FR]. Rep a[a5FR] => R (Shift a[a5FR])

bind :: (Alpha b, Alpha c) => b -> c -> Bind b c

Smart constructor for binders

unsafeUnbind :: Bind a b -> (a, b)

A destructor for binders that does not guarantee fresh names for the binders.

rebind :: (Alpha a, Alpha b) => a -> b -> Rebind a b

Constructor for binding in patterns

reopen :: (Alpha a, Alpha b) => Rebind a b -> (a, b)

destructor for binding patterns, the external names should have already been freshen'ed. We swap the internal names so that they use the external names

rec :: Alpha a => a -> Rec a

unrec :: Alpha a => Rec a -> a

aeq :: Alpha a => a -> a -> Bool

fv :: (Rep b, Alpha a) => a -> Set (Name b)

calculate the free variables of the term

binders :: (Rep b, Alpha b) => b -> [AnyName]

List the binding variables in a pattern

patfv :: (Rep a, Alpha b) => b -> Set (Name a)

Set of variables that occur freely in annotations (not binding)

swaps :: Alpha a => Perm AnyName -> a -> a

The method swaps applys a permutation to all free variables in the term.

swapsBinders :: Alpha a => Perm AnyName -> a -> a

Apply a permutation to the binding variables in a pattern. Embedded terms are left alone by the permutation.

swapsEmbeds :: Alpha a => Perm AnyName -> a -> a

Apply a permutation to the annotations in a pattern. Binding names are left alone by the permutation.

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

Locally freshen an object

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

A pattern of type b can be freshened if a new copy of b can be produced where all old *binding* Names in b are replaced with new fresh Names, and the permutation reports which Names were swapped by others.

match :: Alpha a => a -> a -> Maybe (Perm AnyName)

Match compares two data structures and produces a permutation of their Names that will make them alpha-equivalent to eachother. (Names that appear in annotations must match exactly.) Also note that two terms are alpha-equivalent when the empty permutation is returned.

matchEmbeds :: Alpha a => a -> a -> Maybe (Perm AnyName)

Compare two patterns, ignoring the names of binders, and produce a permutation of their annotations to make them alpha-equivalent to eachother. Return Nothing if no such renaming is possible.

matchBinders :: Alpha a => a -> a -> Maybe (Perm AnyName)

Compare two patterns for equality and produce a permutation of their binding Names to make them alpha-equivalent to each other (Names that appear in annotations must match exactly). Return Nothing if no such renaming is possible.

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

Term

Pat

Instances

Eq AlphaCtx

Read AlphaCtx

Show AlphaCtx

initial :: AlphaCtx

pat :: AlphaCtx -> AlphaCtx

term :: AlphaCtx -> AlphaCtx

mode :: AlphaCtx -> AlphaCtx

class Rep1 AlphaD a => Alpha a where

The Alpha class is for all terms that may contain binders The Rep1 class constraint means that we can only make instances of this class for types that have generic representations. (Derive these using TH and RepLib.)

Methods

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

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

swap everything, including bound and free variables, parts in annots, etc.

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

The method swaps' applys a compound permutation

fv' :: AlphaCtx -> a -> Set AnyName

calculate the free variables (aka support)

binders' :: AlphaCtx -> a -> [AnyName]

list the binding variables in a pattern, in order

match' :: AlphaCtx -> a -> a -> Maybe (Perm AnyName)

Match' compares two data structures and produces a permutation of their free variables that will make them alpha-equivalent to eachother.

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

An object of type a can be freshened if a new copy of a can be produced where all old Names in a are replaced with new fresh Names, and the permutation reports which names were swapped by others.

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

See lfreshen

Instances

Alpha Bool

Alpha Char

Alpha Double

Alpha Float

Alpha Int

Alpha Integer

Alpha ()

Alpha AnyName

Alpha Exp

Alpha a => Alpha [a]

Rep a => Alpha (R a)

Alpha a => Alpha (Maybe a)

Rep a => Alpha (Name a)

(Eq a, Alpha a) => Alpha (Embed a)

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

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

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

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

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

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

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

data AlphaD a

Constructors

AlphaD

Fields

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

swapallD :: AlphaCtx -> Perm AnyName -> a -> a

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

fvD :: AlphaCtx -> a -> Set AnyName

bindersD :: AlphaCtx -> a -> [AnyName]

matchD :: AlphaCtx -> a -> a -> Maybe (Perm AnyName)

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

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

Instances

Alpha a => Sat (AlphaD a)

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

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

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

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

fvR1 :: R1 AlphaD a -> AlphaCtx -> a -> Set AnyName

fv1 :: MTup AlphaD l -> AlphaCtx -> l -> Set AnyName

bindersR1 :: R1 AlphaD a -> AlphaCtx -> a -> [AnyName]

binders1 :: MTup AlphaD l -> AlphaCtx -> l -> [AnyName]

matchR1 :: R1 AlphaD a -> AlphaCtx -> a -> a -> Maybe (Perm AnyName)

match1 :: MTup AlphaD l -> AlphaCtx -> l -> l -> Maybe (Perm AnyName)

freshenR1 :: R1 AlphaD a -> Fresh m => 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

class Monad m => HasNext m where

A monad m supports the nextInteger operation if it can generate new fresh integers

Methods

nextInteger :: m Integer

resetNext :: Integer -> m ()

class (Monad m, HasNext m) => Fresh m where

A monad m supports the fresh operation if it can generate a new unique names.

Methods

fresh :: Name a -> m (Name a)

Instances

HasNext m => Fresh m

unbind :: (Alpha b, Fresh m, Alpha c) => Bind b c -> m (b, c)

Unbind is the destructor of a binding. It ensures that the names in the binding b are fresh.

unbind2 :: (Fresh m, Alpha b, Alpha c, Alpha d) => Bind b c -> Bind b d -> m (Maybe (b, c, d))

Destruct two bindings simultanously, if they match, using the same list of fresh names

unbind3 :: (Fresh m, Alpha b, Alpha c, Alpha d, Alpha e) => Bind b c -> Bind b d -> Bind b e -> m (Maybe (b, c, d, e))

class Monad m => LFresh m where

Locally fresh monad This is the class of monads that support freshness in an (implicit) local scope. Names drawn are fresh for this particular scope, but not globally fresh. This class has a basic instance based on the reader monad.

Methods

lfresh :: Rep a => Name a -> m (Name a)

pick a new name that is fresh for the current (implicit) scope.

avoid :: [AnyName] -> m a -> m a

avoid these names when freshening in the subcomputation.

Instances

LFresh (Reader Integer)

Reader monad instance for local freshness class.

lunbind :: (LFresh m, Alpha a, Alpha b) => Bind a b -> m (a, b)

Destruct a binding in the LFresh monad.

lunbind2 :: (LFresh m, Alpha b, Alpha c, Alpha d) => Bind b c -> Bind b d -> m (Maybe (b, c, d))

lunbind3 :: (LFresh m, Alpha b, Alpha c, Alpha d, Alpha e) => Bind b c -> Bind b d -> Bind b e -> m (Maybe (b, c, d, e))

subst :: (Alpha a, Alpha b, Subst b a) => Name b -> b -> a -> a

Capture-avoiding substitution, in a monad so that we can rename variables at binding locations and avoid capture

substs :: (Alpha a, Alpha b, Subst b a) => [Name b] -> [b] -> a -> a

class Rep1 (SubstD b) a => Subst b a where

Methods

isvar :: a -> Maybe (Name b, b -> a)

lsubst :: LFresh m => Name b -> b -> a -> m a

lsubsts :: LFresh m => [Name b] -> [b] -> a -> m a

Instances

Subst b Double

Subst b Float

Subst b Integer

Subst b Char

Subst b ()

Subst b Bool

Subst b Int

Subst c AnyName

Subst Exp Exp

Subst c a => Subst c (Embed a)

Rep a => Subst b (Name a)

Rep a => Subst b (R a)

Subst c a => Subst c (Maybe a)

Subst c a => Subst c [a]

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

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

(Subst c a, Subst c b) => Subst c (Either a b)

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

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

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

(Subst c a, Subst c b, Subst c d, Subst c e, Subst c f) => Subst c (a, b, d, e, f)

data SubstD b a

Constructors

SubstD

Fields

substD :: LFresh m => Name b -> b -> a -> m a

substsD :: LFresh m => [Name b] -> [b] -> a -> m a

Instances

Subst b a => Sat (SubstD b a)

substR1 :: LFresh m => R1 (SubstD b) a -> Name b -> b -> a -> m a

substsR1 :: LFresh m => R1 (SubstD b) a -> [Name b] -> [b] -> a -> m a

data Exp

Constructors

V (Name Exp)

A Exp Exp

L (Bind (Name Exp) Exp)

Instances

Show Exp

Rep Exp

Alpha Exp

(Sat (ctx[a6TR] (Name Exp)), Sat (ctx[a6TR] Exp), Sat (ctx[a6TR] (Bind (Name Exp) Exp))) => Rep1 ctx[a6TR] Exp

Subst Exp Exp

rExp1 :: forall ctx[a6TR]. ctx[a6TR] (Name Exp) -> ctx[a6TR] Exp -> ctx[a6TR] (Bind (Name Exp) Exp) -> R1 ctx[a6TR] Exp

rExp :: R Exp

nameB :: Name Exp

nameC :: Name Exp

nameA :: Name Exp

assert :: String -> Bool -> IO ()

do_tests :: ()

emptyNE :: Set (Name Exp)

mkbig :: [Name Exp] -> Exp -> Exp