{-# LANGUAGE TemplateHaskell #-}
module Hyper.Unify.Binding.ST
( STUVar (..)
, _STUVar
, stBinding
) where
import Control.Monad.ST.Class (MonadST (..))
import Data.STRef (STRef, newSTRef, readSTRef, writeSTRef)
import Hyper.Class.Unify (BindingDict (..))
import Hyper.Unify.Term (UTerm (..))
import Hyper.Internal.Prelude
newtype STUVar s t = STUVar (STRef s (UTerm (STUVar s) t))
deriving stock (STUVar s t -> STUVar s t -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall s (t :: AHyperType). STUVar s t -> STUVar s t -> Bool
/= :: STUVar s t -> STUVar s t -> Bool
$c/= :: forall s (t :: AHyperType). STUVar s t -> STUVar s t -> Bool
== :: STUVar s t -> STUVar s t -> Bool
$c== :: forall s (t :: AHyperType). STUVar s t -> STUVar s t -> Bool
Eq)
makePrisms ''STUVar
{-# INLINE stBinding #-}
stBinding ::
MonadST m =>
BindingDict (STUVar (World m)) m t
stBinding :: forall (m :: * -> *) (t :: HyperType).
MonadST m =>
BindingDict (STUVar (World m)) m t
stBinding =
BindingDict
{ lookupVar :: (STUVar (World m) # t) -> m (UTerm (STUVar (World m)) # t)
lookupVar = forall (m :: * -> *) a. MonadST m => ST (World m) a -> m a
liftST forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s a. STRef s a -> ST s a
readSTRef forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall s a. s -> Getting a s a -> a
^. forall s (t :: AHyperType) s (t :: AHyperType).
Iso
(STUVar s t)
(STUVar s t)
(STRef s (UTerm (STUVar s) t))
(STRef s (UTerm (STUVar s) t))
_STUVar)
, newVar :: (UTerm (STUVar (World m)) # t) -> m (STUVar (World m) # t)
newVar = \UTerm (STUVar (World m)) # t
t -> forall a s. a -> ST s (STRef s a)
newSTRef UTerm (STUVar (World m)) # t
t forall a b. a -> (a -> b) -> b
& forall (m :: * -> *) a. MonadST m => ST (World m) a -> m a
liftST forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> forall s (t :: AHyperType).
STRef s (UTerm (STUVar s) t) -> STUVar s t
STUVar
, bindVar :: (STUVar (World m) # t) -> (UTerm (STUVar (World m)) # t) -> m ()
bindVar = \STUVar (World m) # t
v UTerm (STUVar (World m)) # t
t -> forall s a. STRef s a -> a -> ST s ()
writeSTRef (STUVar (World m) # t
v forall s a. s -> Getting a s a -> a
^. forall s (t :: AHyperType) s (t :: AHyperType).
Iso
(STUVar s t)
(STUVar s t)
(STRef s (UTerm (STUVar s) t))
(STRef s (UTerm (STUVar s) t))
_STUVar) UTerm (STUVar (World m)) # t
t forall a b. a -> (a -> b) -> b
& forall (m :: * -> *) a. MonadST m => ST (World m) a -> m a
liftST
}