Safe Haskell	None
Language	Haskell2010

Generics.RepLib.Unify

Synopsis

data Proxy a
type UnifyError = String
type UM n a b = ExceptT UnifyError (State (UnificationState n a)) b
throwError :: UnifyError -> UM 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 = 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
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 ()
unifyStepEq :: (Eq b, Show b) => b -> b -> 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
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

data Proxy a Source #

type UnifyError = String Source #

type UM n a b = ExceptT UnifyError (State (UnificationState n a)) b Source #

throwError :: UnifyError -> UM n a b Source #

data UnifySubD n a b Source #

Constructors

UnifySubD
Fields unifyStepD :: Proxy (n, a) -> b -> b -> UM n a () substD :: n -> a -> b -> b occursCheckD :: n -> Proxy a -> b -> Bool

Instances

(Unify n a b, Subst n a b, Occurs n a b) => Sat (UnifySubD n a b) Source #
Instance details Defined in Generics.RepLib.Unify Methods dict :: UnifySubD n a b Source #

data UConstraint n a Source #

Constructors

UC (UnifySubD n a b) b b

data UnificationState n a Source #

Constructors

UState
Fields uConstraints :: [UConstraint n a] uSubst :: [(n, a)]

class (Eq n, Show n, Show a, Show b, HasVar n a) => Unify n a b where Source #

Minimal complete definition

unifyStep

Methods

unifyStep :: Proxy (n, a) -> b -> b -> UM n a () Source #

Instances

(Eq n, Show n, Show a, HasVar n a, Rep1 (UnifySubD n a) a) => Unify n a a Source #
Instance details Defined in Generics.RepLib.Unify Methods unifyStep :: Proxy (n, a) -> a -> a -> UM n a () Source #
(Eq n, Show n, Show a, Show b, HasVar n a, Rep1 (UnifySubD n a) b) => Unify n a b Source #
Instance details Defined in Generics.RepLib.Unify 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 #

unifyStepEq :: (Eq b, Show b) => b -> b -> 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 where Source #

Minimal complete definition

is_var, var

Methods

is_var :: b -> Maybe a Source #

var :: a -> b Source #

class Subst a t t' where Source #

Minimal complete definition

subst

Methods

subst :: a -> t -> t' -> t' Source #

Instances

(Eq a, HasVar a t, Rep1 (UnifySubD a t) t) => Subst a t t Source #
Instance details Defined in Generics.RepLib.Unify Methods subst :: a -> t -> t -> t Source #
Rep1 (UnifySubD a t) t' => Subst a t t' Source #
Instance details Defined in Generics.RepLib.Unify 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 where Source #

Minimal complete definition

occursCheck

Methods

occursCheck :: n -> Proxy a -> b -> Bool Source #

Instances

(Eq n, HasVar n a, Rep1 (UnifySubD n a) a) => Occurs n a a Source #
Instance details Defined in Generics.RepLib.Unify Methods occursCheck :: n -> Proxy a -> a -> Bool Source #
Rep1 (UnifySubD n a) b => Occurs n a b Source #
Instance details Defined in Generics.RepLib.Unify Methods occursCheck :: n -> Proxy a -> b -> Bool Source #

occursCheckR1 :: Rep1 (UnifySubD n a) b => R1 (UnifySubD n a) b -> n -> Proxy a -> b -> Bool Source #