-- | Generate new unification variables
{-# LANGUAGE FlexibleContexts #-}
module Hyper.Unify.New
    ( newUnbound, newTerm, unfreeze
    ) where

import Hyper
import Hyper.Class.Unify (Unify(..), UnifyGen(..), UVarOf, BindingDict(..))
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 :: m (UVarOf m # t)
newUnbound = Proxy t -> m (TypeConstraintsOf t)
forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
Proxy t -> m (TypeConstraintsOf t)
scopeConstraints (Proxy t
forall k (t :: k). Proxy t
Proxy @t) m (TypeConstraintsOf t)
-> (TypeConstraintsOf t -> m (UVarOf m # t)) -> m (UVarOf m # t)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= BindingDict (UVarOf m) m t
-> (UTerm (UVarOf m) # t) -> m (UVarOf m # t)
forall (v :: HyperType) (m :: * -> *) (t :: HyperType).
BindingDict v m t -> (UTerm v # t) -> m (v # t)
newVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
BindingDict (UVarOf m) m t
binding ((UTerm (UVarOf m) # t) -> m (UVarOf m # t))
-> (TypeConstraintsOf t -> UTerm (UVarOf m) # t)
-> TypeConstraintsOf t
-> m (UVarOf m # t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeConstraintsOf t -> UTerm (UVarOf m) # t
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 :: (t # UVarOf m) -> m (UVarOf m # t)
newTerm t # UVarOf m
x = Proxy t -> m (TypeConstraintsOf t)
forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
Proxy t -> m (TypeConstraintsOf t)
scopeConstraints (Proxy t
forall k (t :: k). Proxy t
Proxy @t) m (TypeConstraintsOf t)
-> (TypeConstraintsOf t -> m (UVarOf m # t)) -> m (UVarOf m # t)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= BindingDict (UVarOf m) m t
-> (UTerm (UVarOf m) # t) -> m (UVarOf m # t)
forall (v :: HyperType) (m :: * -> *) (t :: HyperType).
BindingDict v m t -> (UTerm v # t) -> m (v # t)
newVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
BindingDict (UVarOf m) m t
binding ((UTerm (UVarOf m) # t) -> m (UVarOf m # t))
-> (TypeConstraintsOf t -> UTerm (UVarOf m) # t)
-> TypeConstraintsOf t
-> m (UVarOf m # t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UTermBody (UVarOf m) ('AHyperType t) -> UTerm (UVarOf m) # t
forall (v :: HyperType) (ast :: AHyperType).
UTermBody v ast -> UTerm v ast
UTerm (UTermBody (UVarOf m) ('AHyperType t) -> UTerm (UVarOf m) # t)
-> (TypeConstraintsOf t -> UTermBody (UVarOf m) ('AHyperType t))
-> TypeConstraintsOf t
-> UTerm (UVarOf m) # t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeConstraintsOf (GetHyperType ('AHyperType t))
-> ('AHyperType t :# UVarOf m)
-> UTermBody (UVarOf m) ('AHyperType t)
forall (v :: HyperType) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast)
-> (ast :# v) -> UTermBody v ast
`UTermBody` t # UVarOf m
'AHyperType 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 :: (Pure # t) -> m (UVarOf m # t)
unfreeze = (forall (n :: HyperType).
 HRecWitness t n -> (n # UVarOf m) -> m (UVarOf m # n))
-> (Pure # t) -> m (UVarOf m # t)
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 (Proxy (UnifyGen m)
forall k (t :: k). Proxy t
Proxy @(UnifyGen m) Proxy (UnifyGen m)
-> (UnifyGen m n => (n # UVarOf m) -> m (UVarOf m # n))
-> HRecWitness t n
-> (n # UVarOf m)
-> m (UVarOf m # n)
forall (c :: HyperType -> Constraint) (h :: HyperType)
       (n :: HyperType) r.
(Recursive c, c h, RNodes h) =>
Proxy c -> (c n => r) -> HRecWitness h n -> r
#>> UnifyGen m n => (n # UVarOf m) -> m (UVarOf m # n)
forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
(t # UVarOf m) -> m (UVarOf m # t)
newTerm)