{-# 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
(STUVar s t -> STUVar s t -> Bool)
-> (STUVar s t -> STUVar s t -> Bool) -> Eq (STUVar s t)
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 :: BindingDict (STUVar (World m)) m t
stBinding =
BindingDict :: forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
((v # t) -> m (UTerm v # t))
-> ((UTerm v # t) -> m (v # t))
-> ((v # t) -> (UTerm v # t) -> m ())
-> BindingDict v m t
BindingDict
{ lookupVar :: (STUVar (World m) # t) -> m (UTerm (STUVar (World m)) # t)
lookupVar = ST (World m) (UTerm (STUVar (World m)) # t)
-> m (UTerm (STUVar (World m)) # t)
forall (m :: * -> *) a. MonadST m => ST (World m) a -> m a
liftST (ST (World m) (UTerm (STUVar (World m)) # t)
-> m (UTerm (STUVar (World m)) # t))
-> ((STUVar (World m) # t)
-> ST (World m) (UTerm (STUVar (World m)) # t))
-> (STUVar (World m) # t)
-> m (UTerm (STUVar (World m)) # t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STRef (World m) (UTerm (STUVar (World m)) # t)
-> ST (World m) (UTerm (STUVar (World m)) # t)
forall s a. STRef s a -> ST s a
readSTRef (STRef (World m) (UTerm (STUVar (World m)) # t)
-> ST (World m) (UTerm (STUVar (World m)) # t))
-> ((STUVar (World m) # t)
-> STRef (World m) (UTerm (STUVar (World m)) # t))
-> (STUVar (World m) # t)
-> ST (World m) (UTerm (STUVar (World m)) # t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((STUVar (World m) # t)
-> Getting
(STRef (World m) (UTerm (STUVar (World m)) # t))
(STUVar (World m) # t)
(STRef (World m) (UTerm (STUVar (World m)) # t))
-> STRef (World m) (UTerm (STUVar (World m)) # t)
forall s a. s -> Getting a s a -> a
^. Getting
(STRef (World m) (UTerm (STUVar (World m)) # t))
(STUVar (World m) # t)
(STRef (World m) (UTerm (STUVar (World m)) # t))
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 -> (UTerm (STUVar (World m)) # t)
-> ST (World m) (STRef (World m) (UTerm (STUVar (World m)) # t))
forall a s. a -> ST s (STRef s a)
newSTRef UTerm (STUVar (World m)) # t
t ST (World m) (STRef (World m) (UTerm (STUVar (World m)) # t))
-> (ST (World m) (STRef (World m) (UTerm (STUVar (World m)) # t))
-> m (STRef (World m) (UTerm (STUVar (World m)) # t)))
-> m (STRef (World m) (UTerm (STUVar (World m)) # t))
forall a b. a -> (a -> b) -> b
& ST (World m) (STRef (World m) (UTerm (STUVar (World m)) # t))
-> m (STRef (World m) (UTerm (STUVar (World m)) # t))
forall (m :: * -> *) a. MonadST m => ST (World m) a -> m a
liftST m (STRef (World m) (UTerm (STUVar (World m)) # t))
-> (STRef (World m) (UTerm (STUVar (World m)) # t)
-> STUVar (World m) # t)
-> m (STUVar (World m) # t)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> STRef (World m) (UTerm (STUVar (World m)) # t)
-> STUVar (World m) # t
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 -> STRef (World m) (UTerm (STUVar (World m)) # t)
-> (UTerm (STUVar (World m)) # t) -> ST (World m) ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef (STUVar (World m) # t
v (STUVar (World m) # t)
-> Getting
(STRef (World m) (UTerm (STUVar (World m)) # t))
(STUVar (World m) # t)
(STRef (World m) (UTerm (STUVar (World m)) # t))
-> STRef (World m) (UTerm (STUVar (World m)) # t)
forall s a. s -> Getting a s a -> a
^. Getting
(STRef (World m) (UTerm (STUVar (World m)) # t))
(STUVar (World m) # t)
(STRef (World m) (UTerm (STUVar (World m)) # t))
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 ST (World m) () -> (ST (World m) () -> m ()) -> m ()
forall a b. a -> (a -> b) -> b
& ST (World m) () -> m ()
forall (m :: * -> *) a. MonadST m => ST (World m) a -> m a
liftST
}