RepLib-0.2.1: Generic programming library with representation types Source code Contents Index

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 = String Source

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

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 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 where Source

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 where Source

Methods is_var :: b -> Maybe a Source var :: a -> b Source

class Subst a t t' where Source

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

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

Produced by Haddock version 2.4.2