Control.Unification.STVar

This module defines an implementation of unification variables using the ST monad.

Documentation

data STVar s t

Unification variables implemented by STRefs. In addition to the STRef for the term itself, we also track the variable's ID (to support visited-sets).

Instances

Unifiable t => BindingMonad t (STVar s t) (STBinding s)

Defined in Control.Unification.STVar

Methods

lookupVar :: STVar s t -> STBinding s (Maybe (UTerm t (STVar s t)))

freeVar :: STBinding s (STVar s t)

newVar :: UTerm t (STVar s t) -> STBinding s (STVar s t)

bindVar :: STVar s t -> UTerm t (STVar s t) -> STBinding s ()

Eq (STVar s t)

Defined in Control.Unification.STVar

Methods

(==) :: STVar s t -> STVar s t -> Bool

(/=) :: STVar s t -> STVar s t -> Bool

Show (STVar s t)

Defined in Control.Unification.STVar

Methods

showsPrec :: Int -> STVar s t -> ShowS

show :: STVar s t -> String

showList :: [STVar s t] -> ShowS

Variable (STVar s t)

Defined in Control.Unification.STVar

Methods

getVarID :: STVar s t -> Int

data STBinding s a

A monad for handling STVar bindings.

Instances

Unifiable t => BindingMonad t (STVar s t) (STBinding s)

Defined in Control.Unification.STVar

Methods

lookupVar :: STVar s t -> STBinding s (Maybe (UTerm t (STVar s t)))

freeVar :: STBinding s (STVar s t)

newVar :: UTerm t (STVar s t) -> STBinding s (STVar s t)

bindVar :: STVar s t -> UTerm t (STVar s t) -> STBinding s ()

Monad (STBinding s)

Defined in Control.Unification.STVar

Methods

(>>=) :: STBinding s a -> (a -> STBinding s b) -> STBinding s b

(>>) :: STBinding s a -> STBinding s b -> STBinding s b

return :: a -> STBinding s a

Functor (STBinding s)

Defined in Control.Unification.STVar

Methods

fmap :: (a -> b) -> STBinding s a -> STBinding s b

(<$) :: a -> STBinding s b -> STBinding s a

Applicative (STBinding s)

Defined in Control.Unification.STVar

Methods

pure :: a -> STBinding s a

(<*>) :: STBinding s (a -> b) -> STBinding s a -> STBinding s b

liftA2 :: (a -> b -> c) -> STBinding s a -> STBinding s b -> STBinding s c

(*>) :: STBinding s a -> STBinding s b -> STBinding s b

(<*) :: STBinding s a -> STBinding s b -> STBinding s a

runSTBinding :: (forall s. STBinding s a) -> a

Run the ST ranked binding monad. N.B., because STVar are rank-2 quantified, this guarantees that the return value has no such references. However, in order to remove the references from terms, you'll need to explicitly apply the bindings and ground the term.