Copyright	disco team and contributors
Maintainer	byorgey@gmail.com
Safe Haskell	Safe-Inferred
Language	Haskell2010

Disco.Subst

Contents

Substitutions
- Constructing/destructing substitutions
- Substitution operations

Description

The Disco.Subst module defines a generic type of substitutions that map variable names to values.

Synopsis

newtype Substitution a = Substitution {
- getSubst :: Map (Name a) a
}
dom :: Substitution a -> Set (Name a)
idS :: Substitution a
(|->) :: Name a -> a -> Substitution a
fromList :: [(Name a, a)] -> Substitution a
toList :: Substitution a -> [(Name a, a)]
(@@) :: Subst a a => Substitution a -> Substitution a -> Substitution a
compose :: (Subst a a, Foldable t) => t (Substitution a) -> Substitution a
applySubst :: Subst b a => Substitution b -> a -> a
lookup :: Name a -> Substitution a -> Maybe a

Substitutions

newtype Substitution a Source #

A value of type Substitution a is a substitution which maps some set of names (the domain, see dom) to values of type a. Substitutions can be applied to certain terms (see applySubst), replacing any free occurrences of names in the domain with their corresponding values. Thus, substitutions can be thought of as functions of type Term -> Term (for suitable Terms that contain names and values of the right type).

Concretely, substitutions are stored using a Map.

See also Disco.Types, which defines S as an alias for substitutions on types (the most common kind in the disco codebase).

Constructors

Substitution
Fields getSubst :: Map (Name a) a

Instances

Instances details

Functor Substitution Source #
Instance details Defined in Disco.Subst Methods fmap :: (a -> b) -> Substitution a -> Substitution b # (<$) :: a -> Substitution b -> Substitution a #
Show a => Show (Substitution a) Source #
Instance details Defined in Disco.Subst Methods showsPrec :: Int -> Substitution a -> ShowS # show :: Substitution a -> String # showList :: [Substitution a] -> ShowS #
Pretty a => Pretty (Substitution a) Source #
Instance details Defined in Disco.Subst Methods pretty :: forall (r :: EffectRow) ann. Members '[Reader PA, LFresh] r => Substitution a -> Sem r (Doc ann) Source #
Eq a => Eq (Substitution a) Source #
Instance details Defined in Disco.Subst Methods (==) :: Substitution a -> Substitution a -> Bool # (/=) :: Substitution a -> Substitution a -> Bool #
Ord a => Ord (Substitution a) Source #
Instance details Defined in Disco.Subst Methods compare :: Substitution a -> Substitution a -> Ordering # (<) :: Substitution a -> Substitution a -> Bool # (<=) :: Substitution a -> Substitution a -> Bool # (>) :: Substitution a -> Substitution a -> Bool # (>=) :: Substitution a -> Substitution a -> Bool # max :: Substitution a -> Substitution a -> Substitution a # min :: Substitution a -> Substitution a -> Substitution a #

dom :: Substitution a -> Set (Name a) Source #

The domain of a substitution is the set of names for which the substitution is defined.

Constructing/destructing substitutions

idS :: Substitution a Source #

The identity substitution, i.e. the unique substitution with an empty domain, which acts as the identity function on terms.

(|->) :: Name a -> a -> Substitution a Source #

Construct a singleton substitution, which maps the given name to the given value.

fromList :: [(Name a, a)] -> Substitution a Source #

Create a substitution from an association list of names and values.

toList :: Substitution a -> [(Name a, a)] Source #

Convert a substitution into an association list.

Substitution operations

(@@) :: Subst a a => Substitution a -> Substitution a -> Substitution a Source #

Compose two substitutions. Applying s1 @@ s2 is the same as applying first s2, then s1; that is, semantically, composition of substitutions corresponds exactly to function composition when they are considered as functions on terms.

As one would expect, composition is associative and has idS as its identity.

compose :: (Subst a a, Foldable t) => t (Substitution a) -> Substitution a Source #

Compose a whole container of substitutions. For example, compose [s1, s2, s3] = s1 @@ s2 @@ s3.

applySubst :: Subst b a => Substitution b -> a -> a Source #

Apply a substitution to a term, resulting in a new term in which any free variables in the domain of the substitution have been replaced by their corresponding values. Note this requires a Subst b a constraint, which intuitively means that values of type a contain variables of type b we can substitute for.

lookup :: Name a -> Substitution a -> Maybe a Source #

Look up the value a particular name maps to under the given substitution; or return Nothing if the name being looked up is not in the domain.