|
|
|
|
Synopsis |
|
data Proxy a | | type UnifyError = String | | type UM n a b = ErrorT UnifyError (State (UnificationState n a)) b | | data UnifySubD n a b = UnifySubD {} | | data UConstraint n a = forall b . UC (UnifySubD n a b) b b | | data UnificationState n a = UState {} | | class (Eq n, Show n, Show a, Show b, HasVar n a) => Unify n a b where | | | unifyStepR1 :: (Eq n, Show n, Show a, Show b, HasVar n a) => R1 (UnifySubD n a) b -> Proxy (n, a) -> b -> b -> UM n a () | | addConstraintsRL1 :: MTup (UnifySubD n a) l -> Proxy (n, a) -> l -> l -> UM n a () | | dequeueConstraint :: UM n a (Maybe (UConstraint n a)) | | queueConstraint :: UConstraint n a -> UM n a () | | extendSubstitution :: (HasVar n a, Eq n, Show n, Show a, Rep1 (UnifySubD n a) a) => (n, a) -> UM n a () | | solveUnification :: (HasVar n a, Eq n, Show n, Show a, Rep1 (UnifySubD n a) a) => [(a, a)] -> Maybe [(n, a)] | | solveUnification' :: (HasVar n a, Eq n, Show n, Show a, Show b, Rep1 (UnifySubD n a) b) => Proxy (n, a) -> [(b, b)] -> Maybe [(n, a)] | | class HasVar a b where | | | class Subst a t t' where | subst :: a -> t -> t' -> t' |
| | substR1 :: Rep1 (UnifySubD a t) t' => R1 (UnifySubD a t) t' -> a -> t -> t' -> t' | | class Occurs n a b where | | | occursCheckR1 :: Rep1 (UnifySubD n a) b => R1 (UnifySubD n a) b -> n -> Proxy a -> b -> Bool |
|
|
Documentation |
|
|
|
|
|
|
|
|
Constructors | UnifySubD | | unifyStepD :: Proxy (n, a) -> b -> b -> UM n a () | | substD :: n -> a -> b -> b | | occursCheckD :: n -> Proxy a -> b -> Bool | |
|
| Instances | |
|
|
|
|
|
data UnificationState n a | Source |
|
|
|
|
|
|
|
Generic unifyStep. almost identical to polymorphic equality
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
class Subst a t t' where | Source |
|
| Methods | subst :: a -> t -> t' -> t' | Source |
|
|
|
|
|
|
class Occurs n a b where | Source |
|
|
|
|
|
Produced by Haddock version 2.4.2 |