{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TemplateHaskell #-}
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 ::
( 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