|
| Data.TermLanguage.AutoTermLanguage | | Portability | portable | | Stability | experimental | | Maintainer | jba @ di . uminho . pt |
|
|
|
|
|
| Description |
A generic implementations for Substitutions and Unification in
a TermLanguage.
Some conventions used in this module:
- ) functions with suffix _ are default methods that will instanciate
the corresponding methods on the TermLanguage class.
- ) generic functions have prefix g.
- ) in generic transversals with two arguments, a single g in the
prefix means that both arguments have the same (generic) type, and
two ggs in the prefix mean a trully generic variant.
|
|
| Synopsis |
|
|
|
|
| Classes |
|
| class (Ord a, Data a, Data (t a)) => AutoTermLanguage t a |
| Main class for this module. The only method that does not have a default
definition is the varConstr method. This method specifies the constructor
for variables in the TermLanguage | | | Instances | |
|
|
| varConstr :: AutoTermLanguage t a => a -> t a |
| varConstr is the name for the constructor that injects
Variables in Terms. |
|
| gVarsIn :: AutoTermLanguage t a => t a -> GenericQ [a] |
| gVarsIn _ t is a generic function that computes the list of
variables in t. The first argument is dummy. |
|
| gGetVar :: AutoTermLanguage t a => t a -> GenericQ (Maybe a) |
| gGetVar _ x is a generic function that extracts a variable
from a Term. That is, it returns Just v when x==(Var v) and
Nothing otherwise.
The first argument for gGetVar is a dummy argument used to
establish the intended Term type. It can be instanciated with
undefined. |
|
| gAppS :: AutoTermLanguage t a => Subst a t -> GenericT |
| Generic application of a substitution |
|
| gUnifyT :: (AutoTermLanguage t a, Data x) => t a -> x -> x -> Maybe (Subst a t) |
| Generic unification (first argument is dummy) |
|
| ggUnifyT :: AutoTermLanguage t a => t a -> GenericQ (GenericQ (Maybe (Subst a t))) |
| Generic unification (first argument is dummy) |
|
| gMatchT :: (AutoTermLanguage t a, Data x) => t a -> x -> x -> Maybe (Subst a t) |
| Generic matching (first argument is dummy) |
|
| ggMatchT :: AutoTermLanguage t a => t a -> GenericQ (GenericQ (Maybe (Subst a t))) |
| Generic matching (first argument is dummy) |
|
| Types |
|
| data Subst a t |
| Substitutions are implemented as FiniteMaps. | | Instances | |
|
|
| Reexported Modules |
|
| The end-user will be interessed in using the functions from the TermLanguage
module. |
|
| module Data.TermLanguage |
|
| Reexports from Data.Generics to avoid extra imports clauses... |
|
Typeable,Data |
|
| Usage |
|
To use the class AutoTermLanguage it is necessary:
- Define term constructor data type with the variable type has parameter
and make it instance of the Data and Typeable classes (include these
classes in the deriving clause).
- Intanciate the class AutoTermLanguage specifying the
var-constructor.
EXAMPLE OF USE:
import Data.TermLanguage.AutoTermLanguage
data Term a = Var a | Const String | BOp String (Term a) (Term a)
deriving (Eq, Show, Data, Typeable)
instance AutoTermLanguage Term Int
where varConstr = Var
t1,t2 :: Term Int
...
mgu = unifyT t1 t2 --computes the most general unifier
|
|
| Produced by Haddock version 0.6 |
