RepLib-0.5.4.1: Generic programming library with representation types

Safe HaskellNone
LanguageHaskell2010

Generics.RepLib.Unify

Synopsis

Documentation

data Proxy a Source #

data UnifySubD n a b Source #

Constructors

UnifySubD 

Fields

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

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 #

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 #