{-# LANGUAGE FlexibleContexts #-}

-- | Generate new unification variables
module Hyper.Unify.New
    ( newUnbound
    , newTerm
    , unfreeze
    ) where

import Hyper
import Hyper.Class.Unify (BindingDict (..), UVarOf, Unify (..), UnifyGen (..))
import Hyper.Recurse
import Hyper.Unify.Term (UTerm (..), UTermBody (..))

import Prelude.Compat

-- | Create a new unbound unification variable in the current scope
{-# INLINE newUnbound #-}
newUnbound :: forall m t. UnifyGen m t => m (UVarOf m # t)
newUnbound :: forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
m (UVarOf m # t)
newUnbound = forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
Proxy t -> m (TypeConstraintsOf t)
scopeConstraints (forall {k} (t :: k). Proxy t
Proxy @t) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (v :: HyperType) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
UUnbound

-- | Create a new unification term with a given body
{-# INLINE newTerm #-}
newTerm :: forall m t. UnifyGen m t => t # UVarOf m -> m (UVarOf m # t)
newTerm :: forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
(t # UVarOf m) -> m (UVarOf m # t)
newTerm t # UVarOf m
x = forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
Proxy t -> m (TypeConstraintsOf t)
scopeConstraints (forall {k} (t :: k). Proxy t
Proxy @t) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (v :: HyperType) (ast :: AHyperType).
UTermBody v ast -> UTerm v ast
UTerm forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (v :: HyperType) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast)
-> (ast :# v) -> UTermBody v ast
`UTermBody` t # UVarOf m
x)

-- | Embed a pure term as a unification term
{-# INLINE unfreeze #-}
unfreeze :: forall m t. UnifyGen m t => Pure # t -> m (UVarOf m # t)
unfreeze :: forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
(Pure # t) -> m (UVarOf m # t)
unfreeze = forall (m :: * -> *) (h :: HyperType) (w :: HyperType).
(Monad m, RTraversable h) =>
(forall (n :: HyperType). HRecWitness h n -> (n # w) -> m (w # n))
-> (Pure # h) -> m (w # h)
wrapM (forall {k} (t :: k). Proxy t
Proxy @(UnifyGen m) forall (c :: HyperType -> Constraint) (h :: HyperType)
       (n :: HyperType) r.
(Recursive c, c h, RNodes h) =>
Proxy c -> (c n => r) -> HRecWitness h n -> r
#>> forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
(t # UVarOf m) -> m (UVarOf m # t)
newTerm)