{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TemplateHaskell #-}

-- | Load serialized a binding state to 'Control.Monad.ST.ST' based bindings
module Hyper.Unify.Binding.ST.Load
    ( load
    ) where

import qualified Control.Lens as Lens
import Control.Monad.ST.Class (MonadST (..))
import Data.Array.ST (STArray, newArray, readArray, writeArray)
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.Binding.ST (STUVar)
import Hyper.Unify.Term (UTerm (..), uBody)

import Hyper.Internal.Prelude

newtype ConvertState s t = ConvertState (STArray s Int (Maybe (STUVar s t)))
makePrisms ''ConvertState

makeConvertState :: MonadST m => Binding # t -> m (ConvertState (World m) # t)
makeConvertState :: forall (m :: * -> *) (t :: HyperType).
MonadST m =>
(Binding # t) -> m (ConvertState (World m) # t)
makeConvertState (Binding Seq (UTerm UVar ('AHyperType t))
x) =
    forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> e -> m (a i e)
newArray (Int
0, forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq (UTerm UVar ('AHyperType t))
x) forall a. Maybe a
Nothing 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).
STArray s Int (Maybe (STUVar s t)) -> ConvertState s t
ConvertState

loadUTerm ::
    forall m typeVars t.
    ( MonadST m
    , UVarOf m ~ STUVar (World m)
    , Unify m t
    , Recursively (HNodeLens typeVars) t
    ) =>
    typeVars # Binding ->
    typeVars # ConvertState (World m) ->
    UTerm UVar # t ->
    m (UTerm (STUVar (World m)) # t)
loadUTerm :: forall (m :: * -> *) (typeVars :: HyperType) (t :: HyperType).
(MonadST m, UVarOf m ~ STUVar (World m), Unify m t,
 Recursively (HNodeLens typeVars) t) =>
(typeVars # Binding)
-> (typeVars # ConvertState (World m))
-> (UTerm UVar # t)
-> m (UTerm (STUVar (World m)) # t)
loadUTerm typeVars # Binding
_ typeVars # ConvertState (World m)
_ (UUnbound TypeConstraintsOf (GetHyperType ('AHyperType t))
c) = forall (v :: HyperType) (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
loadUTerm typeVars # Binding
_ typeVars # ConvertState (World m)
_ (USkolem TypeConstraintsOf (GetHyperType ('AHyperType t))
c) = forall (v :: HyperType) (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
loadUTerm typeVars # Binding
src typeVars # ConvertState (World m)
conv (UToVar UVar ('AHyperType t)
v) = forall (m :: * -> *) (t :: HyperType) (typeVars :: HyperType).
(MonadST m, UVarOf m ~ STUVar (World m), Unify m t,
 Recursively (HNodeLens typeVars) t) =>
(typeVars # Binding)
-> (typeVars # ConvertState (World m))
-> (UVar # t)
-> m (STUVar (World m) # t)
loadVar typeVars # Binding
src typeVars # ConvertState (World m)
conv UVar ('AHyperType t)
v forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> forall (v :: HyperType) (ast :: AHyperType). v ast -> UTerm v ast
UToVar
loadUTerm typeVars # Binding
src typeVars # ConvertState (World m)
conv (UTerm UTermBody UVar ('AHyperType t)
u) = forall (v1 :: HyperType) (ast :: AHyperType) (v2 :: HyperType).
Lens (UTermBody v1 ast) (UTermBody v2 ast) (ast :# v1) (ast :# v2)
uBody (forall (m :: * -> *) (typeVars :: HyperType) (t :: HyperType).
(MonadST m, UVarOf m ~ STUVar (World m), Unify m t,
 Recursively (HNodeLens typeVars) t) =>
(typeVars # Binding)
-> (typeVars # ConvertState (World m))
-> (t # UVar)
-> m (t # STUVar (World m))
loadBody typeVars # Binding
src typeVars # ConvertState (World m)
conv) UTermBody UVar ('AHyperType t)
u forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> forall (v :: HyperType) (ast :: AHyperType).
UTermBody v ast -> UTerm v ast
UTerm
loadUTerm typeVars # Binding
_ typeVars # ConvertState (World m)
_ UResolving{} = forall a. HasCallStack => [Char] -> a
error [Char]
"converting bindings after resolution"
loadUTerm typeVars # Binding
_ typeVars # ConvertState (World m)
_ UResolved{} = forall a. HasCallStack => [Char] -> a
error [Char]
"converting bindings after resolution"
loadUTerm typeVars # Binding
_ typeVars # ConvertState (World m)
_ UConverted{} = forall a. HasCallStack => [Char] -> a
error [Char]
"loading while saving?"
loadUTerm typeVars # Binding
_ typeVars # ConvertState (World m)
_ UInstantiated{} = forall a. HasCallStack => [Char] -> a
error [Char]
"loading during instantiation"

loadVar ::
    forall m t typeVars.
    ( MonadST m
    , UVarOf m ~ STUVar (World m)
    , Unify m t
    , Recursively (HNodeLens typeVars) t
    ) =>
    typeVars # Binding ->
    typeVars # ConvertState (World m) ->
    UVar # t ->
    m (STUVar (World m) # t)
loadVar :: forall (m :: * -> *) (t :: HyperType) (typeVars :: HyperType).
(MonadST m, UVarOf m ~ STUVar (World m), Unify m t,
 Recursively (HNodeLens typeVars) t) =>
(typeVars # Binding)
-> (typeVars # ConvertState (World m))
-> (UVar # t)
-> m (STUVar (World m) # t)
loadVar typeVars # Binding
src typeVars # ConvertState (World m)
conv (UVar Int
v) =
    forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (c :: HyperType -> Constraint) (h :: HyperType)
       (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))) forall a b. (a -> b) -> a -> b
$
        let tConv :: STArray (World m) Int (Maybe (STUVar (World m) # t))
tConv = typeVars # ConvertState (World m)
conv forall s a. s -> Getting a s a -> a
^. forall (s :: HyperType) (a :: HyperType) (h :: HyperType).
HNodeLens s a =>
Lens' (s # h) (h # a)
hNodeLens forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s (t :: AHyperType) s (t :: AHyperType).
Iso
  (ConvertState s t)
  (ConvertState s t)
  (STArray s Int (Maybe (STUVar s t)))
  (STArray s Int (Maybe (STUVar s t)))
_ConvertState
        in  forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> m e
readArray STArray (World m) Int (Maybe (STUVar (World m) # t))
tConv Int
v
                forall a b. a -> (a -> b) -> b
& forall (m :: * -> *) a. MonadST m => ST (World m) a -> m a
liftST
                forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                    Just STUVar (World m) # t
x -> forall (f :: * -> *) a. Applicative f => a -> f a
pure STUVar (World m) # t
x
                    Maybe (STUVar (World m) # t)
Nothing ->
                        do
                            UTerm (STUVar (World m)) # t
u <-
                                forall (m :: * -> *) (typeVars :: HyperType) (t :: HyperType).
(MonadST m, UVarOf m ~ STUVar (World m), Unify m t,
 Recursively (HNodeLens typeVars) t) =>
(typeVars # Binding)
-> (typeVars # ConvertState (World m))
-> (UTerm UVar # t)
-> m (UTerm (STUVar (World m)) # t)
loadUTerm
                                    typeVars # Binding
src
                                    typeVars # ConvertState (World m)
conv
                                    (typeVars # Binding
src forall s a. HasCallStack => s -> Getting (Endo a) s a -> a
^?! forall (s :: HyperType) (a :: HyperType) (h :: HyperType).
HNodeLens s a =>
Lens' (s # h) (h # a)
hNodeLens forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t1 :: AHyperType) (t2 :: AHyperType).
Iso
  (Binding t1)
  (Binding t2)
  (Seq (UTerm UVar t1))
  (Seq (UTerm UVar t2))
_Binding forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. Ixed m => Index m -> Traversal' m (IxValue m)
Lens.ix Int
v)
                            STUVar (World m) # t
r <- forall (v :: HyperType) (m :: * -> *) (t :: HyperType).
BindingDict v m t -> (UTerm v # t) -> m (v # t)
newVar forall (m :: * -> *) (t :: HyperType).
Unify m t =>
BindingDict (UVarOf m) m t
binding UTerm (STUVar (World m)) # t
u
                            STUVar (World m) # t
r forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *) a. MonadST m => ST (World m) a -> m a
liftST (forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray STArray (World m) Int (Maybe (STUVar (World m) # t))
tConv Int
v (forall a. a -> Maybe a
Just STUVar (World m) # t
r))

loadBody ::
    forall m typeVars t.
    ( MonadST m
    , UVarOf m ~ STUVar (World m)
    , Unify m t
    , Recursively (HNodeLens typeVars) t
    ) =>
    typeVars # Binding ->
    typeVars # ConvertState (World m) ->
    t # UVar ->
    m (t # STUVar (World m))
loadBody :: forall (m :: * -> *) (typeVars :: HyperType) (t :: HyperType).
(MonadST m, UVarOf m ~ STUVar (World m), Unify m t,
 Recursively (HNodeLens typeVars) t) =>
(typeVars # Binding)
-> (typeVars # ConvertState (World m))
-> (t # UVar)
-> m (t # STUVar (World m))
loadBody typeVars # Binding
src typeVars # ConvertState (World m)
conv =
    forall (f :: * -> *) (h :: HyperType) (p :: HyperType)
       (q :: HyperType).
(Applicative f, HTraversable h) =>
(forall (n :: HyperType). 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 :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) 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 :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#>
                forall (m :: * -> *) (t :: HyperType) (typeVars :: HyperType).
(MonadST m, UVarOf m ~ STUVar (World m), Unify m t,
 Recursively (HNodeLens typeVars) t) =>
(typeVars # Binding)
-> (typeVars # ConvertState (World m))
-> (UVar # t)
-> m (STUVar (World m) # t)
loadVar typeVars # Binding
src typeVars # ConvertState (World m)
conv
        )
        forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (c :: HyperType -> Constraint) (h :: HyperType)
       (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 :: HyperType -> Constraint) (h :: HyperType)
       (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))

-- | Load a given serialized unification
-- and a value with serialized unification variable identifiers
-- to a value with 'Control.Monad.ST.ST' unification variables.
load ::
    ( MonadST m
    , UVarOf m ~ STUVar (World m)
    , HTraversable typeVars
    , Unify m t
    , Recursively (HNodeLens typeVars) t
    ) =>
    typeVars # Binding ->
    t # UVar ->
    m (t # STUVar (World m))
load :: forall (m :: * -> *) (typeVars :: HyperType) (t :: HyperType).
(MonadST m, UVarOf m ~ STUVar (World m), HTraversable typeVars,
 Unify m t, Recursively (HNodeLens typeVars) t) =>
(typeVars # Binding) -> (t # UVar) -> m (t # STUVar (World m))
load typeVars # Binding
src t # UVar
collection =
    do
        typeVars # ConvertState (World m)
conv <- forall (f :: * -> *) (h :: HyperType) (p :: HyperType)
       (q :: HyperType).
(Applicative f, HTraversable h) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> f (q # n))
-> (h # p) -> f (h # q)
htraverse (forall a b. a -> b -> a
const forall (m :: * -> *) (t :: HyperType).
MonadST m =>
(Binding # t) -> m (ConvertState (World m) # t)
makeConvertState) typeVars # Binding
src
        forall (m :: * -> *) (typeVars :: HyperType) (t :: HyperType).
(MonadST m, UVarOf m ~ STUVar (World m), Unify m t,
 Recursively (HNodeLens typeVars) t) =>
(typeVars # Binding)
-> (typeVars # ConvertState (World m))
-> (t # UVar)
-> m (t # STUVar (World m))
loadBody typeVars # Binding
src typeVars # ConvertState (World m)
conv t # UVar
collection