-- | A pure data structures implementation of unification variables state

{-# LANGUAGE UndecidableInstances, TemplateHaskell #-}

module Hyper.Unify.Binding
    ( UVar(..), _UVar
    , Binding(..), _Binding
    , emptyBinding
    , bindingDict
    ) where

import           Control.Lens (ALens')
import qualified Control.Lens as Lens
import           Control.Monad.State (MonadState(..))
import           Data.Sequence (Seq)
import           Hyper.Class.Unify (BindingDict(..))
import           Hyper.Type (AHyperType, type (#))
import           Hyper.Unify.Term

import           Hyper.Internal.Prelude

-- | A unification variable identifier pure state based unification
newtype UVar (t :: AHyperType) = UVar Int
    deriving stock ((forall x. UVar t -> Rep (UVar t) x)
-> (forall x. Rep (UVar t) x -> UVar t) -> Generic (UVar t)
forall x. Rep (UVar t) x -> UVar t
forall x. UVar t -> Rep (UVar t) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (t :: AHyperType) x. Rep (UVar t) x -> UVar t
forall (t :: AHyperType) x. UVar t -> Rep (UVar t) x
$cto :: forall (t :: AHyperType) x. Rep (UVar t) x -> UVar t
$cfrom :: forall (t :: AHyperType) x. UVar t -> Rep (UVar t) x
Generic, Int -> UVar t -> ShowS
[UVar t] -> ShowS
UVar t -> String
(Int -> UVar t -> ShowS)
-> (UVar t -> String) -> ([UVar t] -> ShowS) -> Show (UVar t)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (t :: AHyperType). Int -> UVar t -> ShowS
forall (t :: AHyperType). [UVar t] -> ShowS
forall (t :: AHyperType). UVar t -> String
showList :: [UVar t] -> ShowS
$cshowList :: forall (t :: AHyperType). [UVar t] -> ShowS
show :: UVar t -> String
$cshow :: forall (t :: AHyperType). UVar t -> String
showsPrec :: Int -> UVar t -> ShowS
$cshowsPrec :: forall (t :: AHyperType). Int -> UVar t -> ShowS
Show)
    deriving newtype (UVar t -> UVar t -> Bool
(UVar t -> UVar t -> Bool)
-> (UVar t -> UVar t -> Bool) -> Eq (UVar t)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (t :: AHyperType). UVar t -> UVar t -> Bool
/= :: UVar t -> UVar t -> Bool
$c/= :: forall (t :: AHyperType). UVar t -> UVar t -> Bool
== :: UVar t -> UVar t -> Bool
$c== :: forall (t :: AHyperType). UVar t -> UVar t -> Bool
Eq, Eq (UVar t)
Eq (UVar t)
-> (UVar t -> UVar t -> Ordering)
-> (UVar t -> UVar t -> Bool)
-> (UVar t -> UVar t -> Bool)
-> (UVar t -> UVar t -> Bool)
-> (UVar t -> UVar t -> Bool)
-> (UVar t -> UVar t -> UVar t)
-> (UVar t -> UVar t -> UVar t)
-> Ord (UVar t)
UVar t -> UVar t -> Bool
UVar t -> UVar t -> Ordering
UVar t -> UVar t -> UVar t
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall (t :: AHyperType). Eq (UVar t)
forall (t :: AHyperType). UVar t -> UVar t -> Bool
forall (t :: AHyperType). UVar t -> UVar t -> Ordering
forall (t :: AHyperType). UVar t -> UVar t -> UVar t
min :: UVar t -> UVar t -> UVar t
$cmin :: forall (t :: AHyperType). UVar t -> UVar t -> UVar t
max :: UVar t -> UVar t -> UVar t
$cmax :: forall (t :: AHyperType). UVar t -> UVar t -> UVar t
>= :: UVar t -> UVar t -> Bool
$c>= :: forall (t :: AHyperType). UVar t -> UVar t -> Bool
> :: UVar t -> UVar t -> Bool
$c> :: forall (t :: AHyperType). UVar t -> UVar t -> Bool
<= :: UVar t -> UVar t -> Bool
$c<= :: forall (t :: AHyperType). UVar t -> UVar t -> Bool
< :: UVar t -> UVar t -> Bool
$c< :: forall (t :: AHyperType). UVar t -> UVar t -> Bool
compare :: UVar t -> UVar t -> Ordering
$ccompare :: forall (t :: AHyperType). UVar t -> UVar t -> Ordering
$cp1Ord :: forall (t :: AHyperType). Eq (UVar t)
Ord)
makePrisms ''UVar

-- | The state of unification variables implemented in a pure data structure
newtype Binding t = Binding (Seq (UTerm UVar t))
    deriving stock (forall x. Binding t -> Rep (Binding t) x)
-> (forall x. Rep (Binding t) x -> Binding t)
-> Generic (Binding t)
forall x. Rep (Binding t) x -> Binding t
forall x. Binding t -> Rep (Binding t) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (t :: AHyperType) x. Rep (Binding t) x -> Binding t
forall (t :: AHyperType) x. Binding t -> Rep (Binding t) x
$cto :: forall (t :: AHyperType) x. Rep (Binding t) x -> Binding t
$cfrom :: forall (t :: AHyperType) x. Binding t -> Rep (Binding t) x
Generic

makePrisms ''Binding
makeCommonInstances [''Binding]

-- | An empty 'Binding'
emptyBinding :: Binding t
emptyBinding :: Binding t
emptyBinding = Seq (UTerm UVar t) -> Binding t
forall (t :: AHyperType). Seq (UTerm UVar t) -> Binding t
Binding Seq (UTerm UVar t)
forall a. Monoid a => a
mempty

-- | A 'BindingDict' for 'UVar's in a 'MonadState' whose state contains a 'Binding'
{-# INLINE bindingDict #-}
bindingDict ::
    MonadState s m =>
    ALens' s (Binding # t) ->
    BindingDict UVar m t
bindingDict :: ALens' s (Binding # t) -> BindingDict UVar m t
bindingDict ALens' s (Binding # t)
l =
    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 :: (UVar # t) -> m (UTerm UVar # t)
lookupVar =
        \(UVar Int
h) ->
        Getting (Seq (UTerm UVar # t)) s (Seq (UTerm UVar # t))
-> m (Seq (UTerm UVar # t))
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
Lens.use (ALens' s (Binding # t) -> Lens s s (Binding # t) (Binding # t)
forall s t a b. ALens s t a b -> Lens s t a b
Lens.cloneLens ALens' s (Binding # t)
l (((Binding # t) -> Const (Seq (UTerm UVar # t)) (Binding # t))
 -> s -> Const (Seq (UTerm UVar # t)) s)
-> ((Seq (UTerm UVar # t)
     -> Const (Seq (UTerm UVar # t)) (Seq (UTerm UVar # t)))
    -> (Binding # t) -> Const (Seq (UTerm UVar # t)) (Binding # t))
-> Getting (Seq (UTerm UVar # t)) s (Seq (UTerm UVar # t))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Seq (UTerm UVar # t)
 -> Const (Seq (UTerm UVar # t)) (Seq (UTerm UVar # t)))
-> (Binding # t) -> Const (Seq (UTerm UVar # t)) (Binding # t)
forall (t :: AHyperType) (t :: AHyperType).
Iso
  (Binding t) (Binding t) (Seq (UTerm UVar t)) (Seq (UTerm UVar t))
_Binding)
        m (Seq (UTerm UVar # t))
-> (Seq (UTerm UVar # t) -> UTerm UVar # t) -> m (UTerm UVar # t)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (Seq (UTerm UVar # t)
-> Getting
     (Endo (UTerm UVar # t)) (Seq (UTerm UVar # t)) (UTerm UVar # t)
-> UTerm UVar # t
forall s a. HasCallStack => s -> Getting (Endo a) s a -> a
^?! Index (Seq (UTerm UVar # t))
-> Traversal'
     (Seq (UTerm UVar # t)) (IxValue (Seq (UTerm UVar # t)))
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
Lens.ix Int
Index (Seq (UTerm UVar # t))
h)
    , newVar :: (UTerm UVar # t) -> m (UVar # t)
newVar =
        \UTerm UVar # t
x ->
        ALens' s (Binding # t) -> Lens s s (Binding # t) (Binding # t)
forall s t a b. ALens s t a b -> Lens s t a b
Lens.cloneLens ALens' s (Binding # t)
l (((Binding # t) -> (Seq (UTerm UVar # t), Binding # t))
 -> s -> (Seq (UTerm UVar # t), s))
-> ((Seq (UTerm UVar # t)
     -> (Seq (UTerm UVar # t), Seq (UTerm UVar # t)))
    -> (Binding # t) -> (Seq (UTerm UVar # t), Binding # t))
-> (Seq (UTerm UVar # t)
    -> (Seq (UTerm UVar # t), Seq (UTerm UVar # t)))
-> s
-> (Seq (UTerm UVar # t), s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Seq (UTerm UVar # t)
 -> (Seq (UTerm UVar # t), Seq (UTerm UVar # t)))
-> (Binding # t) -> (Seq (UTerm UVar # t), Binding # t)
forall (t :: AHyperType) (t :: AHyperType).
Iso
  (Binding t) (Binding t) (Seq (UTerm UVar t)) (Seq (UTerm UVar t))
_Binding ((Seq (UTerm UVar # t)
  -> (Seq (UTerm UVar # t), Seq (UTerm UVar # t)))
 -> s -> (Seq (UTerm UVar # t), s))
-> (Seq (UTerm UVar # t) -> Seq (UTerm UVar # t))
-> m (Seq (UTerm UVar # t))
forall (p :: * -> * -> *) s (m :: * -> *) a b.
(Strong p, MonadState s m) =>
Over p ((,) a) s s a b -> p a b -> m a
<<%= (Seq (UTerm UVar # t) -> (UTerm UVar # t) -> Seq (UTerm UVar # t)
forall s a. Snoc s s a a => s -> a -> s
Lens.|> UTerm UVar # t
x)
        m (Seq (UTerm UVar # t)) -> (Seq (UTerm UVar # t) -> Int) -> m Int
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> Seq (UTerm UVar # t) -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length m Int -> (Int -> UVar # t) -> m (UVar # t)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> Int -> UVar # t
forall (t :: AHyperType). Int -> UVar t
UVar
    , bindVar :: (UVar # t) -> (UTerm UVar # t) -> m ()
bindVar =
        \(UVar Int
h) UTerm UVar # t
v ->
        ALens' s (Binding # t) -> Lens s s (Binding # t) (Binding # t)
forall s t a b. ALens s t a b -> Lens s t a b
Lens.cloneLens ALens' s (Binding # t)
l (((Binding # t) -> Identity (Binding # t)) -> s -> Identity s)
-> (((UTerm UVar # t) -> Identity (UTerm UVar # t))
    -> (Binding # t) -> Identity (Binding # t))
-> ((UTerm UVar # t) -> Identity (UTerm UVar # t))
-> s
-> Identity s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Seq (UTerm UVar # t) -> Identity (Seq (UTerm UVar # t)))
-> (Binding # t) -> Identity (Binding # t)
forall (t :: AHyperType) (t :: AHyperType).
Iso
  (Binding t) (Binding t) (Seq (UTerm UVar t)) (Seq (UTerm UVar t))
_Binding ((Seq (UTerm UVar # t) -> Identity (Seq (UTerm UVar # t)))
 -> (Binding # t) -> Identity (Binding # t))
-> (((UTerm UVar # t) -> Identity (UTerm UVar # t))
    -> Seq (UTerm UVar # t) -> Identity (Seq (UTerm UVar # t)))
-> ((UTerm UVar # t) -> Identity (UTerm UVar # t))
-> (Binding # t)
-> Identity (Binding # t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (Seq (UTerm UVar # t))
-> Traversal'
     (Seq (UTerm UVar # t)) (IxValue (Seq (UTerm UVar # t)))
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
Lens.ix Int
Index (Seq (UTerm UVar # t))
h (((UTerm UVar # t) -> Identity (UTerm UVar # t))
 -> s -> Identity s)
-> (UTerm UVar # t) -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= UTerm UVar # t
v
    }