Base.Subst

The module Subst implements substitutions. A substitution sigma = {x_1 |-> t_1, ... ,x_n |-> t_n} is a finite mapping from (finitely many) variables x_1, ... ,x_n to some kind of expression or term.

In order to implement substitutions efficiently, composed substitutions are marked with a boolean flag (see below).

Documentation

data Subst a b

Data type for substitution

Constructors

Subst Bool (Map a b)

Instances

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

Defined in Base.Subst

Methods

showsPrec :: Int -> Subst a b -> ShowS

show :: Subst a b -> String

showList :: [Subst a b] -> ShowS

class IntSubst e where

Type class for terms where variables are represented as Ints

Methods

ivar :: Int -> e

Construct a variable from an Int

isubst :: Subst Int e -> e -> e

Apply a substitution to a term

idSubst :: Subst a b

Identity substitution

singleSubst :: Ord v => v -> e -> Subst v e

Create a substitution for a single replacement

bindSubst :: Ord v => v -> e -> Subst v e -> Subst v e

Extend a substitution with a single replacement

unbindSubst :: Ord v => v -> Subst v e -> Subst v e

Remove a single replacement from a substitution

substToList :: Subst v e -> [(v, e)]

Convert a substitution to a list of replacements

compose :: Ord v => Subst v e -> Subst v e -> Subst v e

Compose two substitutions

substVar' :: Ord v => (v -> e) -> (Subst v e -> e -> e) -> Subst v e -> v -> e

Apply a substitution to a variable

isubstVar :: IntSubst e => Subst Int e -> Int -> e

Apply a substitution to a term with variables represented as Ints

restrictSubstTo :: Ord v => [v] -> Subst v e -> Subst v e

The function restrictSubstTo implements the restriction of a substitution to a given subset of its domain.