unbound-generics-0.4.3: Support for programming with names and binders using GHC Generics
Copyright(c) 2014 Aleksey Kliger
LicenseBSD3 (See LICENSE)
MaintainerAleksey Kliger
Stabilityexperimental
Safe HaskellSafe-Inferred
LanguageHaskell2010

Unbound.Generics.LocallyNameless.Subst

Description

A typeclass for types that may participate in capture-avoiding substitution

The minimal definition is empty, provided your type is an instance of Generic

type Var = Name Factor
data Expr = SumOf [Summand]
          deriving (Show, Generic)
data Summand = ProductOf [Factor]
          deriving (Show, Generic)
instance Subst Var Expr
instance Subst Var Summand

The default instance just propagates the substitution into the constituent factors.

If you identify the variable occurrences by implementing the isvar function, the derived subst function will be able to substitute a factor for a variable.

data Factor = V Var
            | C Int
            | Subexpr Expr
          deriving (Show, Generic)
instance Subst Var Factor where
  isvar (V v) = Just (SubstName v)
  isvar _     = Nothing
Synopsis

Documentation

data SubstName a b where Source #

See isVar

Constructors

SubstName :: a ~ b => Name a -> SubstName a b 

data SubstCoerce a b where Source #

Constructors

SubstCoerce :: Name b -> (b -> Maybe a) -> SubstCoerce a b 

class Subst b a where Source #

Instances of Subst b a are terms of type a that may contain variables of type b that may participate in capture-avoiding substitution.

Minimal complete definition

Nothing

Methods

isvar :: a -> Maybe (SubstName a b) Source #

This is the only method that must be implemented

isCoerceVar :: a -> Maybe (SubstCoerce a b) Source #

This is an alternative version to isvar, useable in the case that the substituted argument doesn't have *exactly* the same type as the term it should be substituted into. The default implementation always returns Nothing.

subst :: Name b -> b -> a -> a Source #

subst nm e tm substitutes e for nm in tm. It has a default generic implementation in terms of isvar

default subst :: (Generic a, GSubst b (Rep a)) => Name b -> b -> a -> a Source #

substs :: [(Name b, b)] -> a -> a Source #

default substs :: (Generic a, GSubst b (Rep a)) => [(Name b, b)] -> a -> a Source #

substBvs :: AlphaCtx -> [b] -> a -> a Source #

default substBvs :: (Generic a, GSubst b (Rep a)) => AlphaCtx -> [b] -> a -> a Source #

Instances

Instances details
Subst b AnyName Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Subst

Subst b Integer Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Subst

Subst b () Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

isvar :: () -> Maybe (SubstName () b) Source #

isCoerceVar :: () -> Maybe (SubstCoerce () b) Source #

subst :: Name b -> b -> () -> () Source #

substs :: [(Name b, b)] -> () -> () Source #

substBvs :: AlphaCtx -> [b] -> () -> () Source #

Subst b Bool Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

isvar :: Bool -> Maybe (SubstName Bool b) Source #

isCoerceVar :: Bool -> Maybe (SubstCoerce Bool b) Source #

subst :: Name b -> b -> Bool -> Bool Source #

substs :: [(Name b, b)] -> Bool -> Bool Source #

substBvs :: AlphaCtx -> [b] -> Bool -> Bool Source #

Subst b Char Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

isvar :: Char -> Maybe (SubstName Char b) Source #

isCoerceVar :: Char -> Maybe (SubstCoerce Char b) Source #

subst :: Name b -> b -> Char -> Char Source #

substs :: [(Name b, b)] -> Char -> Char Source #

substBvs :: AlphaCtx -> [b] -> Char -> Char Source #

Subst b Double Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Subst

Subst b Float Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Subst

Subst b Int Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

isvar :: Int -> Maybe (SubstName Int b) Source #

isCoerceVar :: Int -> Maybe (SubstCoerce Int b) Source #

subst :: Name b -> b -> Int -> Int Source #

substs :: [(Name b, b)] -> Int -> Int Source #

substBvs :: AlphaCtx -> [b] -> Int -> Int Source #

Subst a (Ignore b) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

isvar :: Ignore b -> Maybe (SubstName (Ignore b) a) Source #

isCoerceVar :: Ignore b -> Maybe (SubstCoerce (Ignore b) a) Source #

subst :: Name a -> a -> Ignore b -> Ignore b Source #

substs :: [(Name a, a)] -> Ignore b -> Ignore b Source #

substBvs :: AlphaCtx -> [a] -> Ignore b -> Ignore b Source #

Subst b (Name a) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

isvar :: Name a -> Maybe (SubstName (Name a) b) Source #

isCoerceVar :: Name a -> Maybe (SubstCoerce (Name a) b) Source #

subst :: Name b -> b -> Name a -> Name a Source #

substs :: [(Name b, b)] -> Name a -> Name a Source #

substBvs :: AlphaCtx -> [b] -> Name a -> Name a Source #

Subst c a => Subst c (Embed a) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

isvar :: Embed a -> Maybe (SubstName (Embed a) c) Source #

isCoerceVar :: Embed a -> Maybe (SubstCoerce (Embed a) c) Source #

subst :: Name c -> c -> Embed a -> Embed a Source #

substs :: [(Name c, c)] -> Embed a -> Embed a Source #

substBvs :: AlphaCtx -> [c] -> Embed a -> Embed a Source #

Subst c p => Subst c (Rec p) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

isvar :: Rec p -> Maybe (SubstName (Rec p) c) Source #

isCoerceVar :: Rec p -> Maybe (SubstCoerce (Rec p) c) Source #

subst :: Name c -> c -> Rec p -> Rec p Source #

substs :: [(Name c, c)] -> Rec p -> Rec p Source #

substBvs :: AlphaCtx -> [c] -> Rec p -> Rec p Source #

(Alpha p, Subst c p) => Subst c (TRec p) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

isvar :: TRec p -> Maybe (SubstName (TRec p) c) Source #

isCoerceVar :: TRec p -> Maybe (SubstCoerce (TRec p) c) Source #

subst :: Name c -> c -> TRec p -> TRec p Source #

substs :: [(Name c, c)] -> TRec p -> TRec p Source #

substBvs :: AlphaCtx -> [c] -> TRec p -> TRec p Source #

Subst c e => Subst c (Shift e) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

isvar :: Shift e -> Maybe (SubstName (Shift e) c) Source #

isCoerceVar :: Shift e -> Maybe (SubstCoerce (Shift e) c) Source #

subst :: Name c -> c -> Shift e -> Shift e Source #

substs :: [(Name c, c)] -> Shift e -> Shift e Source #

substBvs :: AlphaCtx -> [c] -> Shift e -> Shift e Source #

Subst c a => Subst c (Maybe a) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

isvar :: Maybe a -> Maybe (SubstName (Maybe a) c) Source #

isCoerceVar :: Maybe a -> Maybe (SubstCoerce (Maybe a) c) Source #

subst :: Name c -> c -> Maybe a -> Maybe a Source #

substs :: [(Name c, c)] -> Maybe a -> Maybe a Source #

substBvs :: AlphaCtx -> [c] -> Maybe a -> Maybe a Source #

Subst c a => Subst c [a] Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

isvar :: [a] -> Maybe (SubstName [a] c) Source #

isCoerceVar :: [a] -> Maybe (SubstCoerce [a] c) Source #

subst :: Name c -> c -> [a] -> [a] Source #

substs :: [(Name c, c)] -> [a] -> [a] Source #

substBvs :: AlphaCtx -> [c] -> [a] -> [a] Source #

(Subst c a, Subst c b) => Subst c (Either a b) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

isvar :: Either a b -> Maybe (SubstName (Either a b) c) Source #

isCoerceVar :: Either a b -> Maybe (SubstCoerce (Either a b) c) Source #

subst :: Name c -> c -> Either a b -> Either a b Source #

substs :: [(Name c, c)] -> Either a b -> Either a b Source #

substBvs :: AlphaCtx -> [c] -> Either a b -> Either a b Source #

(Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Bind a b) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

isvar :: Bind a b -> Maybe (SubstName (Bind a b) c) Source #

isCoerceVar :: Bind a b -> Maybe (SubstCoerce (Bind a b) c) Source #

subst :: Name c -> c -> Bind a b -> Bind a b Source #

substs :: [(Name c, c)] -> Bind a b -> Bind a b Source #

substBvs :: AlphaCtx -> [c] -> Bind a b -> Bind a b Source #

(Subst c p1, Subst c p2) => Subst c (Rebind p1 p2) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

isvar :: Rebind p1 p2 -> Maybe (SubstName (Rebind p1 p2) c) Source #

isCoerceVar :: Rebind p1 p2 -> Maybe (SubstCoerce (Rebind p1 p2) c) Source #

subst :: Name c -> c -> Rebind p1 p2 -> Rebind p1 p2 Source #

substs :: [(Name c, c)] -> Rebind p1 p2 -> Rebind p1 p2 Source #

substBvs :: AlphaCtx -> [c] -> Rebind p1 p2 -> Rebind p1 p2 Source #

(Subst c a, Subst c b) => Subst c (a, b) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

isvar :: (a, b) -> Maybe (SubstName (a, b) c) Source #

isCoerceVar :: (a, b) -> Maybe (SubstCoerce (a, b) c) Source #

subst :: Name c -> c -> (a, b) -> (a, b) Source #

substs :: [(Name c, c)] -> (a, b) -> (a, b) Source #

substBvs :: AlphaCtx -> [c] -> (a, b) -> (a, b) Source #

(Subst c a, Subst c b, Subst c d) => Subst c (a, b, d) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

isvar :: (a, b, d) -> Maybe (SubstName (a, b, d) c) Source #

isCoerceVar :: (a, b, d) -> Maybe (SubstCoerce (a, b, d) c) Source #

subst :: Name c -> c -> (a, b, d) -> (a, b, d) Source #

substs :: [(Name c, c)] -> (a, b, d) -> (a, b, d) Source #

substBvs :: AlphaCtx -> [c] -> (a, b, d) -> (a, b, d) Source #

(Subst c a, Subst c b, Subst c d, Subst c e) => Subst c (a, b, d, e) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

isvar :: (a, b, d, e) -> Maybe (SubstName (a, b, d, e) c) Source #

isCoerceVar :: (a, b, d, e) -> Maybe (SubstCoerce (a, b, d, e) c) Source #

subst :: Name c -> c -> (a, b, d, e) -> (a, b, d, e) Source #

substs :: [(Name c, c)] -> (a, b, d, e) -> (a, b, d, e) Source #

substBvs :: AlphaCtx -> [c] -> (a, b, d, e) -> (a, b, d, e) Source #

(Subst c a, Subst c b, Subst c d, Subst c e, Subst c f) => Subst c (a, b, d, e, f) Source # 
Instance details

Defined in Unbound.Generics.LocallyNameless.Subst

Methods

isvar :: (a, b, d, e, f) -> Maybe (SubstName (a, b, d, e, f) c) Source #

isCoerceVar :: (a, b, d, e, f) -> Maybe (SubstCoerce (a, b, d, e, f) c) Source #

subst :: Name c -> c -> (a, b, d, e, f) -> (a, b, d, e, f) Source #

substs :: [(Name c, c)] -> (a, b, d, e, f) -> (a, b, d, e, f) Source #

substBvs :: AlphaCtx -> [c] -> (a, b, d, e, f) -> (a, b, d, e, f) Source #

substBind :: Subst a t => Bind (Name a) t -> a -> t Source #

Specialized version of capture-avoiding substitution for that operates on a Bind (Name a) t term to unbind the bound name Name a and immediately subsitute a new term for its occurrences.

This is a specialization of instantiate :: Bind pat term -> [a] -> term where the Bind pat term has a pattern that is just a single Name a and there is a single substitution term of type a. Unlike instantiate, this function cannot fail at runtime.

instantiate :: (Alpha a, Alpha b, Alpha p, Subst a b) => Bind p b -> [a] -> b Source #

Immediately substitute for the bound variables of a pattern in a binder, without first naming the variables. NOTE: this operation does not check that the number of terms passed in match the number of variables in the pattern. (Or that they are of appropriate type.)