| Maintainer | bastiaan.heeren@ou.nl |
|---|---|
| Stability | provisional |
| Portability | portable (depends on ghc) |
| Safe Haskell | None |
| Language | Haskell98 |
Ideas.Common.Rewriting.Substitution
Description
Substitutions on terms. Substitutions are idempotent, and non-cyclic.
- data Substitution
- emptySubst :: Substitution
- singletonSubst :: Int -> Term -> Substitution
- dom :: Substitution -> IntSet
- lookupVar :: Int -> Substitution -> Maybe Term
- (@@) :: Substitution -> Substitution -> Substitution
- (|->) :: Substitution -> Term -> Term
- listToSubst :: [(Int, Term)] -> Substitution
- composable :: Substitution -> Substitution -> Bool
- (@+@) :: Substitution -> Substitution -> Maybe Substitution
- tests :: TestSuite
Documentation
data Substitution Source
Abstract data type for substitutions
emptySubst :: Substitution Source
Returns the empty substitution
singletonSubst :: Int -> Term -> Substitution Source
Returns a singleton substitution
dom :: Substitution -> IntSet Source
Returns the domain of a substitution (as a set)
lookupVar :: Int -> Substitution -> Maybe Term Source
Lookups a variable in a substitution. Nothing indicates that the variable is not in the domain of the substitution
(@@) :: Substitution -> Substitution -> Substitution infixr 6 Source
Combines two substitutions. The left-hand side substitution is first applied to the co-domain of the right-hand side substitution
(|->) :: Substitution -> Term -> Term infixr 5 Source
Apply the substitution
listToSubst :: [(Int, Term)] -> Substitution Source
Turns a list into a substitution
composable :: Substitution -> Substitution -> Bool Source
(@+@) :: Substitution -> Substitution -> Maybe Substitution infix 6 Source