{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}

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