Generics.RepLib.Unify

Documentation

data Proxy a

type UnifyError = String

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

data UnifySubD n a b

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)

data UConstraint n a

Constructors

forall b . UC (UnifySubD n a b) b b

data UnificationState n a

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

Methods

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

Instances

(Eq n, Show n, Show a, HasVar n a, Rep1 (UnifySubD n a) a) => Unify n a a

(Eq n, Show n, Show a, Show b, HasVar n a, Rep1 (UnifySubD n a) b) => Unify n a b

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 ()

Generic unifyStep. almost identical to polymorphic equality

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

Methods

is_var :: b -> Maybe a

var :: a -> b

class Subst a t t' where

Methods

subst :: a -> t -> t' -> t'

Instances

(Eq a, HasVar a t, Rep1 (UnifySubD a t) t) => Subst a t t

Rep1 (UnifySubD a t) t' => Subst a t t'

substR1 :: Rep1 (UnifySubD a t) t' => R1 (UnifySubD a t) t' -> a -> t -> t' -> t'

class Occurs n a b where

Methods

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

Instances

(Eq n, HasVar n a, Rep1 (UnifySubD n a) a) => Occurs n a a

Rep1 (UnifySubD n a) b => Occurs n a b

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