RepLib-0.2.1: Generic programming library with representation typesSource codeContentsIndex
Data.RepLib.Unify
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 {
unifyStepD :: Proxy (n, a) -> b -> b -> UM n a ()
substD :: n -> a -> b -> b
occursCheckD :: n -> Proxy a -> b -> Bool
}
data UConstraint n a = forall b . UC (UnifySubD n a b) b b
data UnificationState n a = UState {
uConstraints :: [UConstraint n a]
uSubst :: [(n, a)]
}
class (Eq n, Show n, Show a, Show b, HasVar n a) => Unify n a b where
unifyStep :: Proxy (n, a) -> b -> b -> UM n a ()
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
is_var :: b -> Maybe a
var :: a -> b
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
occursCheck :: n -> Proxy a -> b -> Bool
occursCheckR1 :: Rep1 (UnifySubD n a) b => R1 (UnifySubD n a) b -> n -> Proxy a -> b -> Bool
Documentation
data Proxy a Source
type UnifyError = StringSource
type UM n a b = ErrorT UnifyError (State (UnificationState n a)) bSource
data UnifySubD n a b Source
Constructors
UnifySubD
unifyStepD :: Proxy (n, a) -> b -> b -> UM n a ()
substD :: n -> a -> b -> b
occursCheckD :: n -> Proxy a -> b -> Bool
show/hide Instances
(Unify n a b, Subst n a b, Occurs n a b) => Sat (UnifySubD n a b)
data UConstraint n a Source
Constructors
forall b . UC (UnifySubD n a b) b b
data UnificationState n a Source
Constructors
UState
uConstraints :: [UConstraint n a]
uSubst :: [(n, a)]
class (Eq n, Show n, Show a, Show b, HasVar n a) => Unify n a b whereSource
Methods
unifyStep :: Proxy (n, a) -> b -> b -> UM n a ()Source
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 ()Source
Generic unifyStep. almost identical to polymorphic equality
addConstraintsRL1 :: MTup (UnifySubD n a) l -> Proxy (n, a) -> l -> l -> UM n a ()Source
dequeueConstraint :: UM n a (Maybe (UConstraint n a))Source
queueConstraint :: UConstraint n a -> UM n a ()Source
extendSubstitution :: (HasVar n a, Eq n, Show n, Show a, Rep1 (UnifySubD n a) a) => (n, a) -> UM n a ()Source
solveUnification :: (HasVar n a, Eq n, Show n, Show a, Rep1 (UnifySubD n a) a) => [(a, a)] -> Maybe [(n, a)]Source
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)]Source
class HasVar a b whereSource
Methods
is_var :: b -> Maybe aSource
var :: a -> bSource
class Subst a t t' whereSource
Methods
subst :: a -> t -> t' -> t'Source
substR1 :: Rep1 (UnifySubD a t) t' => R1 (UnifySubD a t) t' -> a -> t -> t' -> t'Source
class Occurs n a b whereSource
Methods
occursCheck :: n -> Proxy a -> b -> BoolSource
occursCheckR1 :: Rep1 (UnifySubD n a) b => R1 (UnifySubD n a) b -> n -> Proxy a -> b -> BoolSource
Produced by Haddock version 2.4.2