| Copyright | (c) 2002 Wolfgang Lux |
|---|---|
| License | BSD-3-clause |
| Maintainer | bjp@informatik.uni-kiel.de |
| Stability | experimental |
| Portability | portable |
| Safe Haskell | Safe |
| Language | Haskell2010 |
Base.Subst
Description
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).
Synopsis
- data Subst a b = Subst Bool (Map a b)
- class IntSubst e where
- idSubst :: Subst a b
- singleSubst :: Ord v => v -> e -> Subst v e
- bindSubst :: Ord v => v -> e -> Subst v e -> Subst v e
- unbindSubst :: Ord v => v -> Subst v e -> Subst v e
- substToList :: Subst v e -> [(v, e)]
- compose :: Ord v => Subst v e -> Subst v e -> Subst v e
- substVar' :: Ord v => (v -> e) -> (Subst v e -> e -> e) -> Subst v e -> v -> e
- isubstVar :: IntSubst e => Subst Int e -> Int -> e
- restrictSubstTo :: Ord v => [v] -> Subst v e -> Subst v e
Documentation
Data type for substitution
singleSubst :: Ord v => v -> e -> Subst v e Source #
Create a substitution for a single replacement
bindSubst :: Ord v => v -> e -> Subst v e -> Subst v e Source #
Extend a substitution with a single replacement
unbindSubst :: Ord v => v -> Subst v e -> Subst v e Source #
Remove a single replacement from a substitution
substToList :: Subst v e -> [(v, e)] Source #
Convert a substitution to a list of replacements
substVar' :: Ord v => (v -> e) -> (Subst v e -> e -> e) -> Subst v e -> v -> e Source #
Apply a substitution to a variable
isubstVar :: IntSubst e => Subst Int e -> Int -> e Source #
Apply a substitution to a term with variables represented as Ints
restrictSubstTo :: Ord v => [v] -> Subst v e -> Subst v e Source #
The function restrictSubstTo implements the restriction of a
substitution to a given subset of its domain.