Control.Unification.Ranked.STVar

A ranked variant of Control.Unification.STVar.

Documentation

data STRVar s t

A ranked unification variable implemented by STRefs. In addition to the STRef for the term itself, we also track the variable's ID (to support visited-sets) and rank (to support weighted path compression).

Instances

Unifiable t => RankedBindingMonad t (STRVar s t) (STRBinding s)

Defined in Control.Unification.Ranked.STVar

Methods

lookupRankVar :: STRVar s t -> STRBinding s (Rank t (STRVar s t))

incrementRank :: STRVar s t -> STRBinding s ()

incrementBindVar :: STRVar s t -> UTerm t (STRVar s t) -> STRBinding s ()

Unifiable t => BindingMonad t (STRVar s t) (STRBinding s)

Defined in Control.Unification.Ranked.STVar

Methods

lookupVar :: STRVar s t -> STRBinding s (Maybe (UTerm t (STRVar s t)))

freeVar :: STRBinding s (STRVar s t)

newVar :: UTerm t (STRVar s t) -> STRBinding s (STRVar s t)

bindVar :: STRVar s t -> UTerm t (STRVar s t) -> STRBinding s ()

Eq (STRVar s t)

Defined in Control.Unification.Ranked.STVar

Methods

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

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

Show (STRVar s t)

Defined in Control.Unification.Ranked.STVar

Methods

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

show :: STRVar s t -> String

showList :: [STRVar s t] -> ShowS

Variable (STRVar s t)

Defined in Control.Unification.Ranked.STVar

Methods

getVarID :: STRVar s t -> Int

data STRBinding s a

A monad for handling STRVar bindings.

Instances

Unifiable t => RankedBindingMonad t (STRVar s t) (STRBinding s)

Defined in Control.Unification.Ranked.STVar

Methods

lookupRankVar :: STRVar s t -> STRBinding s (Rank t (STRVar s t))

incrementRank :: STRVar s t -> STRBinding s ()

incrementBindVar :: STRVar s t -> UTerm t (STRVar s t) -> STRBinding s ()

Unifiable t => BindingMonad t (STRVar s t) (STRBinding s)

Defined in Control.Unification.Ranked.STVar

Methods

lookupVar :: STRVar s t -> STRBinding s (Maybe (UTerm t (STRVar s t)))

freeVar :: STRBinding s (STRVar s t)

newVar :: UTerm t (STRVar s t) -> STRBinding s (STRVar s t)

bindVar :: STRVar s t -> UTerm t (STRVar s t) -> STRBinding s ()

Monad (STRBinding s)

Defined in Control.Unification.Ranked.STVar

Methods

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

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

return :: a -> STRBinding s a

Functor (STRBinding s)

Defined in Control.Unification.Ranked.STVar

Methods

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

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

Applicative (STRBinding s)

Defined in Control.Unification.Ranked.STVar

Methods

pure :: a -> STRBinding s a

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

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

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

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

runSTRBinding :: (forall s. STRBinding s a) -> a

Run the ST ranked binding monad. N.B., because STRVar 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.