{-# LANGUAGE TemplateHaskell #-}

-- | Unification variables binding in the 'Control.Monad.ST.ST' monad
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

-- | A unification variable in the 'Control.Monad.ST.ST' monad
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

-- | A 'BindingDict' for 'STUVar's
{-# 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
        }