term-rewriting-0.3.0.1: Term Rewriting Library

Safe HaskellNone
LanguageHaskell98

Data.Rewriting.Substitution

Contents

Synopsis

Documentation

data GSubst v f v' Source #

A generalised? substitution: a finite, partial map from variables to terms with a different variable type.

Instances
(Show v, Show v', Show f) => Show (GSubst v f v') Source # 
Instance details

Defined in Data.Rewriting.Substitution.Type

Methods

showsPrec :: Int -> GSubst v f v' -> ShowS #

show :: GSubst v f v' -> String #

showList :: [GSubst v f v'] -> ShowS #

(Pretty v, Pretty f, Pretty v') => Pretty (GSubst v f v') # 
Instance details

Defined in Data.Rewriting.Substitution.Pretty

Methods

pretty :: GSubst v f v' -> Doc #

prettyList :: [GSubst v f v'] -> Doc #

type Subst f v = GSubst v f v Source #

A substitution, mapping variables to terms. Substitutions are equal to the identity almost everywhere.

Important operations

gApply :: Ord v => GSubst v f v' -> Term f v -> Maybe (Term f v') Source #

Apply a substitution, assuming that it's total. If the term contains a variable not defined by the substitution, return Nothing.

apply :: Ord v => Subst f v -> Term f v -> Term f v Source #

Apply a substitution, assuming that it's the identity on variables not mentionend in the substitution.

compose :: Ord v => Subst f v -> Subst f v -> Subst f v Source #

Compose substitutions. We have

(s1 `compose` s2) `apply` t = s1 `apply` (s2 `apply` t).

Reexported modules

data GSubst v f v' Source #

A generalised? substitution: a finite, partial map from variables to terms with a different variable type.

Instances
(Show v, Show v', Show f) => Show (GSubst v f v') Source # 
Instance details

Defined in Data.Rewriting.Substitution.Type

Methods

showsPrec :: Int -> GSubst v f v' -> ShowS #

show :: GSubst v f v' -> String #

showList :: [GSubst v f v'] -> ShowS #

(Pretty v, Pretty f, Pretty v') => Pretty (GSubst v f v') # 
Instance details

Defined in Data.Rewriting.Substitution.Pretty

Methods

pretty :: GSubst v f v' -> Doc #

prettyList :: [GSubst v f v'] -> Doc #

type Subst f v = GSubst v f v Source #

A substitution, mapping variables to terms. Substitutions are equal to the identity almost everywhere.