{-# LANGUAGE FlexibleContexts #-}

-- | Serialize the state of unification
module Hyper.Unify.Binding.Save
    ( save
    ) where

import qualified Control.Lens as Lens
import Control.Monad.Trans.Class (MonadTrans (..))
import Control.Monad.Trans.State (StateT (..))
import Hyper
import Hyper.Class.Optic (HNodeLens (..))
import Hyper.Class.Unify (BindingDict (..), UVarOf, Unify (..))
import Hyper.Recurse
import Hyper.Unify.Binding (Binding, UVar (..), _Binding)
import Hyper.Unify.Term (UTerm (..), uBody)

import Hyper.Internal.Prelude

saveUTerm ::
    forall m typeVars t.
    (Unify m t, Recursively (HNodeLens typeVars) t) =>
    UTerm (UVarOf m) # t ->
    StateT (typeVars # Binding, [m ()]) m (UTerm UVar # t)
saveUTerm :: forall (m :: * -> *) (typeVars :: AHyperType -> *)
       (t :: AHyperType -> *).
(Unify m t, Recursively (HNodeLens typeVars) t) =>
(UTerm (UVarOf m) # t)
-> StateT (typeVars # Binding, [m ()]) m (UTerm UVar # t)
saveUTerm (UUnbound TypeConstraintsOf (GetHyperType ('AHyperType t))
c) = forall (v :: AHyperType -> *) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
UUnbound TypeConstraintsOf (GetHyperType ('AHyperType t))
c forall a b. a -> (a -> b) -> b
& forall (f :: * -> *) a. Applicative f => a -> f a
pure
saveUTerm (USkolem TypeConstraintsOf (GetHyperType ('AHyperType t))
c) = forall (v :: AHyperType -> *) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
USkolem TypeConstraintsOf (GetHyperType ('AHyperType t))
c forall a b. a -> (a -> b) -> b
& forall (f :: * -> *) a. Applicative f => a -> f a
pure
saveUTerm (UToVar UVarOf m ('AHyperType t)
v) = forall (m :: * -> *) (t :: AHyperType -> *)
       (typeVars :: AHyperType -> *).
(Unify m t, Recursively (HNodeLens typeVars) t) =>
(UVarOf m # t) -> StateT (typeVars # Binding, [m ()]) m (UVar # t)
saveVar UVarOf m ('AHyperType t)
v forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> UTerm v ast
UToVar
saveUTerm (UTerm UTermBody (UVarOf m) ('AHyperType t)
u) = forall (v1 :: AHyperType -> *) (ast :: AHyperType)
       (v2 :: AHyperType -> *).
Lens (UTermBody v1 ast) (UTermBody v2 ast) (ast :# v1) (ast :# v2)
uBody forall (m :: * -> *) (typeVars :: AHyperType -> *)
       (t :: AHyperType -> *).
(Unify m t, Recursively (HNodeLens typeVars) t) =>
(t # UVarOf m) -> StateT (typeVars # Binding, [m ()]) m (t # UVar)
saveBody UTermBody (UVarOf m) ('AHyperType t)
u forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> forall (v :: AHyperType -> *) (ast :: AHyperType).
UTermBody v ast -> UTerm v ast
UTerm
saveUTerm UInstantiated{} = forall a. HasCallStack => [Char] -> a
error [Char]
"converting bindings during instantiation"
saveUTerm UResolving{} = forall a. HasCallStack => [Char] -> a
error [Char]
"converting bindings after resolution"
saveUTerm UResolved{} = forall a. HasCallStack => [Char] -> a
error [Char]
"converting bindings after resolution"
saveUTerm UConverted{} = forall a. HasCallStack => [Char] -> a
error [Char]
"converting variable again"

saveVar ::
    forall m t typeVars.
    (Unify m t, Recursively (HNodeLens typeVars) t) =>
    UVarOf m # t ->
    StateT (typeVars # Binding, [m ()]) m (UVar # t)
saveVar :: forall (m :: * -> *) (t :: AHyperType -> *)
       (typeVars :: AHyperType -> *).
(Unify m t, Recursively (HNodeLens typeVars) t) =>
(UVarOf m # t) -> StateT (typeVars # Binding, [m ()]) m (UVar # t)
saveVar UVarOf m # t
v =
    forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (v # t) -> m (UTerm v # t)
lookupVar forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
v
        forall a b. a -> (a -> b) -> b
& forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
        forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            UConverted Int
i -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (t :: AHyperType). Int -> UVar t
UVar Int
i)
            UTerm (UVarOf m) # t
srcBody ->
                do
                    Binding # t
pb <- forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
Lens.use (forall s t a b. Field1 s t a b => Lens s t a b
Lens._1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: AHyperType -> *) (a :: AHyperType -> *)
       (h :: AHyperType -> *).
HNodeLens s a =>
Lens' (s # h) (h # a)
hNodeLens)
                    let r :: Int
r = Binding # t
pb forall s a. s -> Getting a s a -> a
^. forall (t1 :: AHyperType) (t2 :: AHyperType).
Iso
  (Binding t1)
  (Binding t2)
  (Seq (UTerm UVar t1))
  (Seq (UTerm UVar t2))
_Binding forall a b. a -> (a -> b) -> b
& forall (t :: * -> *) a. Foldable t => t a -> Int
length
                    forall (v :: AHyperType -> *) (ast :: AHyperType).
Int -> UTerm v ast
UConverted Int
r forall a b. a -> (a -> b) -> b
& forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (v # t) -> (UTerm v # t) -> m ()
bindVar forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
v forall a b. a -> (a -> b) -> b
& forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
                    forall s t a b. Field2 s t a b => Lens s t a b
Lens._2 forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= (forall a. Semigroup a => a -> a -> a
<> [forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (v # t) -> (UTerm v # t) -> m ()
bindVar forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
v UTerm (UVarOf m) # t
srcBody])
                    UTerm UVar ('AHyperType t)
dstBody <- forall (m :: * -> *) (typeVars :: AHyperType -> *)
       (t :: AHyperType -> *).
(Unify m t, Recursively (HNodeLens typeVars) t) =>
(UTerm (UVarOf m) # t)
-> StateT (typeVars # Binding, [m ()]) m (UTerm UVar # t)
saveUTerm UTerm (UVarOf m) # t
srcBody
                    forall s t a b. Field1 s t a b => Lens s t a b
Lens._1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: AHyperType -> *) (a :: AHyperType -> *)
       (h :: AHyperType -> *).
HNodeLens s a =>
Lens' (s # h) (h # a)
hNodeLens forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= (Binding # t
pb forall a b. a -> (a -> b) -> b
& forall (t1 :: AHyperType) (t2 :: AHyperType).
Iso
  (Binding t1)
  (Binding t2)
  (Seq (UTerm UVar t1))
  (Seq (UTerm UVar t2))
_Binding forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (forall s a. Snoc s s a a => s -> a -> s
Lens.|> UTerm UVar ('AHyperType t)
dstBody))
                    forall (t :: AHyperType). Int -> UVar t
UVar Int
r forall a b. a -> (a -> b) -> b
& forall (f :: * -> *) a. Applicative f => a -> f a
pure
                    forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (c :: (AHyperType -> *) -> Constraint)
       (h :: AHyperType -> *) (proxy :: Constraint -> *).
Recursively c h =>
proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))
recursively (forall {k} (t :: k). Proxy t
Proxy @(HNodeLens typeVars t))

saveBody ::
    forall m typeVars t.
    (Unify m t, Recursively (HNodeLens typeVars) t) =>
    t # UVarOf m ->
    StateT (typeVars # Binding, [m ()]) m (t # UVar)
saveBody :: forall (m :: * -> *) (typeVars :: AHyperType -> *)
       (t :: AHyperType -> *).
(Unify m t, Recursively (HNodeLens typeVars) t) =>
(t # UVarOf m) -> StateT (typeVars # Binding, [m ()]) m (t # UVar)
saveBody =
    forall (f :: * -> *) (h :: AHyperType -> *) (p :: AHyperType -> *)
       (q :: AHyperType -> *).
(Applicative f, HTraversable h) =>
(forall (n :: AHyperType -> *).
 HWitness h n -> (p # n) -> f (q # n))
-> (h # p) -> f (h # q)
htraverse
        ( forall {k} (t :: k). Proxy t
Proxy @(Unify m) forall (h :: AHyperType -> *)
       (c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => HWitness h n -> r) -> HWitness h n -> r
#*#
            forall {k} (t :: k). Proxy t
Proxy @(Recursively (HNodeLens typeVars)) forall (h :: AHyperType -> *)
       (c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#>
                forall (m :: * -> *) (t :: AHyperType -> *)
       (typeVars :: AHyperType -> *).
(Unify m t, Recursively (HNodeLens typeVars) t) =>
(UVarOf m # t) -> StateT (typeVars # Binding, [m ()]) m (UVar # t)
saveVar
        )
        forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (c :: (AHyperType -> *) -> Constraint)
       (h :: AHyperType -> *) (proxy :: Constraint -> *).
(Recursive c, HNodes h, c h) =>
proxy (c h) -> Dict (HNodesConstraint h c)
recurse (forall {k} (t :: k). Proxy t
Proxy @(Unify m t))
        forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (c :: (AHyperType -> *) -> Constraint)
       (h :: AHyperType -> *) (proxy :: Constraint -> *).
Recursively c h =>
proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))
recursively (forall {k} (t :: k). Proxy t
Proxy @(HNodeLens typeVars t))

-- | Serialize the state of unification for
-- the unification variables in a given value,
-- and transform the value's unification variables
-- to their serialized identifiers.
save ::
    (Unify m t, Recursively (HNodeLens typeVars) t) =>
    t # UVarOf m ->
    StateT (typeVars # Binding) m (t # UVar)
save :: forall (m :: * -> *) (t :: AHyperType -> *)
       (typeVars :: AHyperType -> *).
(Unify m t, Recursively (HNodeLens typeVars) t) =>
(t # UVarOf m) -> StateT (typeVars # Binding) m (t # UVar)
save t # UVarOf m
collection =
    forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT forall a b. (a -> b) -> a -> b
$
        \typeVars # Binding
dstState ->
            do
                (t # UVar
r, (typeVars # Binding
finalState, [m ()]
recover)) <- forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (forall (m :: * -> *) (typeVars :: AHyperType -> *)
       (t :: AHyperType -> *).
(Unify m t, Recursively (HNodeLens typeVars) t) =>
(t # UVarOf m) -> StateT (typeVars # Binding, [m ()]) m (t # UVar)
saveBody t # UVarOf m
collection) (typeVars # Binding
dstState, [])
                (t # UVar
r, typeVars # Binding
finalState) forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [m ()]
recover