|
| Data.TermLanguage | | Portability | portable | | Stability | experimental | | Maintainer | jba @ di . uminho . pt |
|
|
|
|
|
| Description |
| A module for handling Terms, Variables and Substitutions.
|
|
| Synopsis |
|
|
|
| Documentation |
|
| class Eq a => TermLanguage t s a | t -> s where |
A class that handle terms (t a) with variables (a) and the
associated notion of substitution (s a t).
Note that a has kind *, t has kind *->* and s has
kind *->*->*. | | | Methods | | varT :: a -> t a | | Build a term from a variable | | | varsIn :: t a -> [a] | | Vars in a term | | | appS :: s a t -> t a -> t a | | Applies a substitution to a term | | | nullS :: s a t | | Null Substitution | | | unitS :: a -> t a -> s a t | | Singleton substitution | | | compS :: s a t -> s a t -> s a t | | Composition of two substitutions | | | domS :: s a t -> [a] | | Gets the Domain of a substitution | | | unifyT :: t a -> t a -> Maybe (s a t) | | unifyT t1 t2 computes the most general unifier for terms
t1 and t2 (if it exists).
That is, if unify t1 t2 returns Just s then
(appS s t1)==(appS s t2)
and, for every substitution s1 that equalizes both terms, it factors
through s (i.e. exists s2 such that s1==comp s s2). | | | matchT :: t a -> t a -> Maybe (s a t) | | matchT t1 t2 computes the matcher substitution for terms
t1 and t2 (if it exists).
That is, if match t1 t2 returns Just s then
(appS s t1)==t2. |
| | | Instances | |
|
|
| vRngS :: TermLanguage t s a => s a t -> [a] |
(s2 @@ s1) returns the substitution s2 AFTER s1.
It is the infix operator for substitution composition.
However, remember that the arguments are swaped when compared with
compS, that is compS s1 s2==s2 s1 Get all vars in the range of a substitution. |
|
| isIdempotentS :: TermLanguage t s a => s a t -> Bool |
| isIdempotentS s checks if s is an idempotent substitution. |
|
| isInstanceOfT :: TermLanguage t s a => t a -> t a -> Bool |
| isInstanceOfT t1 t2 checks if t1 is an instance of t2. |
|
| Produced by Haddock version 0.6 |
