{-# 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
(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

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