{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}
module Hyper.Unify.Generalize
( generalize
, instantiate
, GTerm (..)
, _GMono
, _GPoly
, _GBody
, W_GTerm (..)
, instantiateWith
, instantiateForAll
, instantiateH
) where
import Algebra.PartialOrd (PartialOrd (..))
import qualified Control.Lens as Lens
import Control.Monad.Trans.Class (MonadTrans (..))
import Control.Monad.Trans.Writer (WriterT (..), tell)
import Data.Monoid (All (..))
import Hyper
import Hyper.Class.Traversable
import Hyper.Class.Unify
import Hyper.Recurse
import Hyper.Unify.Constraints
import Hyper.Unify.New (newTerm)
import Hyper.Unify.Term (UTerm (..), uBody)
import Hyper.Internal.Prelude
data GTerm v ast
=
GMono (v ast)
|
GPoly (v ast)
|
GBody (ast :# GTerm v)
deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (v :: AHyperType -> *) (ast :: AHyperType) x.
Rep (GTerm v ast) x -> GTerm v ast
forall (v :: AHyperType -> *) (ast :: AHyperType) x.
GTerm v ast -> Rep (GTerm v ast) x
$cto :: forall (v :: AHyperType -> *) (ast :: AHyperType) x.
Rep (GTerm v ast) x -> GTerm v ast
$cfrom :: forall (v :: AHyperType -> *) (ast :: AHyperType) x.
GTerm v ast -> Rep (GTerm v ast) x
Generic)
makePrisms ''GTerm
makeCommonInstances [''GTerm]
makeHTraversableAndBases ''GTerm
instance RNodes a => HNodes (HFlip GTerm a) where
type HNodesConstraint (HFlip GTerm a) c = (c a, Recursive c)
type HWitnessType (HFlip GTerm a) = HRecWitness a
{-# INLINE hLiftConstraint #-}
hLiftConstraint :: forall (c :: (AHyperType -> *) -> Constraint)
(n :: AHyperType -> *) r.
HNodesConstraint (HFlip GTerm a) c =>
HWitness (HFlip GTerm a) n -> Proxy c -> (c n => r) -> r
hLiftConstraint (HWitness HWitnessType (HFlip GTerm a) n
HRecWitness a n
HRecSelf) = \Proxy c
_ c n => r
x -> c n => r
x
hLiftConstraint (HWitness (HRecSub HWitness a c
c HRecWitness c n
n)) = forall (a :: AHyperType -> *)
(c :: (AHyperType -> *) -> Constraint) (b :: AHyperType -> *)
(n :: AHyperType -> *) r.
(RNodes a, HNodesConstraint (HFlip GTerm a) c) =>
HWitness a b -> HRecWitness b n -> Proxy c -> (c n => r) -> r
hLiftConstraintH HWitness a c
c HRecWitness c n
n
hLiftConstraintH ::
forall a c b n r.
(RNodes a, HNodesConstraint (HFlip GTerm a) c) =>
HWitness a b ->
HRecWitness b n ->
Proxy c ->
(c n => r) ->
r
hLiftConstraintH :: forall (a :: AHyperType -> *)
(c :: (AHyperType -> *) -> Constraint) (b :: AHyperType -> *)
(n :: AHyperType -> *) r.
(RNodes a, HNodesConstraint (HFlip GTerm a) c) =>
HWitness a b -> HRecWitness b n -> Proxy c -> (c n => r) -> r
hLiftConstraintH HWitness a b
c HRecWitness b n
n Proxy c
p c n => r
f =
(forall {k} (t :: k). Proxy t
Proxy @RNodes forall (h :: AHyperType -> *)
(c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> (Proxy c
p forall (h :: AHyperType -> *)
(c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> (Proxy c
p forall (h :: AHyperType -> *)
(c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> c n => r
f) (forall (h :: AHyperType -> *) (n :: AHyperType -> *).
HWitnessType h n -> HWitness h n
HWitness @(HFlip GTerm _) HRecWitness b n
n)) HWitness a b
c) HWitness a b
c
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 @(c a))
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 @(RNodes a))
instance Recursively HFunctor ast => HFunctor (HFlip GTerm ast) where
{-# INLINE hmap #-}
hmap :: forall (p :: AHyperType -> *) (q :: AHyperType -> *).
(forall (n :: AHyperType -> *).
HWitness (HFlip GTerm ast) n -> (p # n) -> q # n)
-> (HFlip GTerm ast # p) -> HFlip GTerm ast # q
hmap forall (n :: AHyperType -> *).
HWitness (HFlip GTerm ast) n -> (p # n) -> q # n
f =
forall (f0 :: (AHyperType -> *) -> AHyperType -> *)
(x0 :: AHyperType -> *) (k0 :: AHyperType -> *)
(f1 :: (AHyperType -> *) -> AHyperType -> *)
(x1 :: AHyperType -> *) (k1 :: AHyperType -> *).
Iso (HFlip f0 x0 # k0) (HFlip f1 x1 # k1) (f0 k0 # x0) (f1 k1 # x1)
_HFlip
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ \case
GMono p ('AHyperType ast)
x -> forall (n :: AHyperType -> *).
HWitness (HFlip GTerm ast) n -> (p # n) -> q # n
f (forall (h :: AHyperType -> *) (n :: AHyperType -> *).
HWitnessType h n -> HWitness h n
HWitness forall (h :: AHyperType -> *). HRecWitness h h
HRecSelf) p ('AHyperType ast)
x forall a b. a -> (a -> b) -> b
& forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GMono
GPoly p ('AHyperType ast)
x -> forall (n :: AHyperType -> *).
HWitness (HFlip GTerm ast) n -> (p # n) -> q # n
f (forall (h :: AHyperType -> *) (n :: AHyperType -> *).
HWitnessType h n -> HWitness h n
HWitness forall (h :: AHyperType -> *). HRecWitness h h
HRecSelf) p ('AHyperType ast)
x forall a b. a -> (a -> b) -> b
& forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GPoly
GBody 'AHyperType ast :# GTerm p
x ->
forall (h :: AHyperType -> *) (p :: AHyperType -> *)
(q :: AHyperType -> *).
HFunctor h =>
(forall (n :: AHyperType -> *). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap
( forall {k} (t :: k). Proxy t
Proxy @(Recursively HFunctor) 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
#*#
\HWitness ast n
cw ->
forall (f0 :: (AHyperType -> *) -> AHyperType -> *)
(k0 :: AHyperType -> *) (x0 :: AHyperType -> *)
(f1 :: (AHyperType -> *) -> AHyperType -> *)
(k1 :: AHyperType -> *) (x1 :: AHyperType -> *).
Iso (f0 k0 # x0) (f1 k1 # x1) (HFlip f0 x0 # k0) (HFlip f1 x1 # k1)
hflipped
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ forall (h :: AHyperType -> *) (p :: AHyperType -> *)
(q :: AHyperType -> *).
HFunctor h =>
(forall (n :: AHyperType -> *). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap (forall (n :: AHyperType -> *).
HWitness (HFlip GTerm ast) n -> (p # n) -> q # n
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(HWitness HWitnessType (HFlip GTerm n) n
nw) -> forall (h :: AHyperType -> *) (n :: AHyperType -> *).
HWitnessType h n -> HWitness h n
HWitness (forall (h :: AHyperType -> *) (c :: AHyperType -> *)
(n :: AHyperType -> *).
HWitness h c -> HRecWitness c n -> HRecWitness h n
HRecSub HWitness ast n
cw HWitnessType (HFlip GTerm n) n
nw)))
)
'AHyperType ast :# GTerm p
x
forall a b. a -> (a -> b) -> b
& forall (v :: AHyperType -> *) (ast :: AHyperType).
(ast :# GTerm v) -> GTerm v ast
GBody
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 @(HFunctor ast))
instance Recursively HFoldable ast => HFoldable (HFlip GTerm ast) where
{-# INLINE hfoldMap #-}
hfoldMap :: forall a (p :: AHyperType -> *).
Monoid a =>
(forall (n :: AHyperType -> *).
HWitness (HFlip GTerm ast) n -> (p # n) -> a)
-> (HFlip GTerm ast # p) -> a
hfoldMap forall (n :: AHyperType -> *).
HWitness (HFlip GTerm ast) n -> (p # n) -> a
f =
\case
GMono p ('AHyperType ast)
x -> forall (n :: AHyperType -> *).
HWitness (HFlip GTerm ast) n -> (p # n) -> a
f (forall (h :: AHyperType -> *) (n :: AHyperType -> *).
HWitnessType h n -> HWitness h n
HWitness forall (h :: AHyperType -> *). HRecWitness h h
HRecSelf) p ('AHyperType ast)
x
GPoly p ('AHyperType ast)
x -> forall (n :: AHyperType -> *).
HWitness (HFlip GTerm ast) n -> (p # n) -> a
f (forall (h :: AHyperType -> *) (n :: AHyperType -> *).
HWitnessType h n -> HWitness h n
HWitness forall (h :: AHyperType -> *). HRecWitness h h
HRecSelf) p ('AHyperType ast)
x
GBody 'AHyperType ast :# GTerm p
x ->
forall (h :: AHyperType -> *) a (p :: AHyperType -> *).
(HFoldable h, Monoid a) =>
(forall (n :: AHyperType -> *). HWitness h n -> (p # n) -> a)
-> (h # p) -> a
hfoldMap
( forall {k} (t :: k). Proxy t
Proxy @(Recursively HFoldable) 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
#*#
\HWitness ast n
cw ->
forall (h :: AHyperType -> *) a (p :: AHyperType -> *).
(HFoldable h, Monoid a) =>
(forall (n :: AHyperType -> *). HWitness h n -> (p # n) -> a)
-> (h # p) -> a
hfoldMap (forall (n :: AHyperType -> *).
HWitness (HFlip GTerm ast) n -> (p # n) -> a
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(HWitness HWitnessType (HFlip GTerm n) n
nw) -> forall (h :: AHyperType -> *) (n :: AHyperType -> *).
HWitnessType h n -> HWitness h n
HWitness (forall (h :: AHyperType -> *) (c :: AHyperType -> *)
(n :: AHyperType -> *).
HWitness h c -> HRecWitness c n -> HRecWitness h n
HRecSub HWitness ast n
cw HWitnessType (HFlip GTerm n) n
nw)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (f0 :: (AHyperType -> *) -> AHyperType -> *)
(x0 :: AHyperType -> *) (k0 :: AHyperType -> *)
(f1 :: (AHyperType -> *) -> AHyperType -> *)
(x1 :: AHyperType -> *) (k1 :: AHyperType -> *).
Iso (HFlip f0 x0 # k0) (HFlip f1 x1 # k1) (f0 k0 # x0) (f1 k1 # x1)
_HFlip forall t b. AReview t b -> b -> t
#)
)
'AHyperType ast :# GTerm p
x
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 @(HFoldable ast))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall s a. s -> Getting a s a -> a
^. forall (f0 :: (AHyperType -> *) -> AHyperType -> *)
(x0 :: AHyperType -> *) (k0 :: AHyperType -> *)
(f1 :: (AHyperType -> *) -> AHyperType -> *)
(x1 :: AHyperType -> *) (k1 :: AHyperType -> *).
Iso (HFlip f0 x0 # k0) (HFlip f1 x1 # k1) (f0 k0 # x0) (f1 k1 # x1)
_HFlip)
instance RTraversable ast => HTraversable (HFlip GTerm ast) where
{-# INLINE hsequence #-}
hsequence :: forall (f :: * -> *) (p :: AHyperType -> *).
Applicative f =>
(HFlip GTerm ast # ContainedH f p) -> f (HFlip GTerm ast # p)
hsequence =
\case
GMono ContainedH f p ('AHyperType ast)
x -> forall (f :: * -> *) (p :: AHyperType -> *) (h :: AHyperType).
ContainedH f p h -> f (p h)
runContainedH ContainedH f p ('AHyperType ast)
x forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GMono
GPoly ContainedH f p ('AHyperType ast)
x -> forall (f :: * -> *) (p :: AHyperType -> *) (h :: AHyperType).
ContainedH f p h -> f (p h)
runContainedH ContainedH f p ('AHyperType ast)
x forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GPoly
GBody 'AHyperType ast :# GTerm (ContainedH f p)
x ->
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 @RTraversable forall (h :: AHyperType -> *)
(c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> forall (f0 :: (AHyperType -> *) -> AHyperType -> *)
(k0 :: AHyperType -> *) (x0 :: AHyperType -> *)
(f1 :: (AHyperType -> *) -> AHyperType -> *)
(k1 :: AHyperType -> *) (x1 :: AHyperType -> *).
Iso (f0 k0 # x0) (f1 k1 # x1) (HFlip f0 x0 # k0) (HFlip f1 x1 # k1)
hflipped forall (h :: AHyperType -> *) (f :: * -> *) (p :: AHyperType -> *).
(HTraversable h, Applicative f) =>
(h # ContainedH f p) -> f (h # p)
hsequence) 'AHyperType ast :# GTerm (ContainedH f p)
x
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 @(RTraversable ast))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> forall (v :: AHyperType -> *) (ast :: AHyperType).
(ast :# GTerm v) -> GTerm v ast
GBody
forall a b. a -> (a -> b) -> b
& forall (f0 :: (AHyperType -> *) -> AHyperType -> *)
(x0 :: AHyperType -> *) (k0 :: AHyperType -> *)
(f1 :: (AHyperType -> *) -> AHyperType -> *)
(x1 :: AHyperType -> *) (k1 :: AHyperType -> *).
Iso (HFlip f0 x0 # k0) (HFlip f1 x1 # k1) (f0 k0 # x0) (f1 k1 # x1)
_HFlip
generalize ::
forall m t.
UnifyGen m t =>
UVarOf m # t ->
m (GTerm (UVarOf m) # t)
generalize :: forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
(UVarOf m # t) -> m (GTerm (UVarOf m) # t)
generalize UVarOf m # t
v0 =
do
(UVarOf m # t
v1, UTerm (UVarOf m) ('AHyperType t)
u) <- forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
(UVarOf m # t) -> m (UVarOf m # t, UTerm (UVarOf m) # t)
semiPruneLookup UVarOf m # t
v0
TypeConstraintsOf t
c <- forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
Proxy t -> m (TypeConstraintsOf t)
scopeConstraints (forall {k} (t :: k). Proxy t
Proxy @t)
case UTerm (UVarOf m) ('AHyperType t)
u of
UUnbound TypeConstraintsOf (GetHyperType ('AHyperType t))
l
| forall c. TypeConstraints c => c -> c
toScopeConstraints TypeConstraintsOf (GetHyperType ('AHyperType t))
l forall a. PartialOrd a => a -> a -> Bool
`leq` TypeConstraintsOf t
c ->
forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GPoly UVarOf m # t
v1
forall (f :: * -> *) a b. Functor f => a -> f b -> f 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
v1 (forall (v :: AHyperType -> *) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
USkolem (forall c. TypeConstraints c => c -> c
generalizeConstraints TypeConstraintsOf (GetHyperType ('AHyperType t))
l))
USkolem TypeConstraintsOf (GetHyperType ('AHyperType t))
l | forall c. TypeConstraints c => c -> c
toScopeConstraints TypeConstraintsOf (GetHyperType ('AHyperType t))
l forall a. PartialOrd a => a -> a -> Bool
`leq` TypeConstraintsOf t
c -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GPoly UVarOf m # t
v1)
UTerm UTermBody (UVarOf m) ('AHyperType t)
t ->
do
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
v1 (forall (v :: AHyperType -> *) (ast :: AHyperType).
UTermBody v ast -> UTerm v ast
UResolving UTermBody (UVarOf m) ('AHyperType t)
t)
t # GTerm (UVarOf m)
b <- 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 @(UnifyGen m) 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 -> *).
UnifyGen m t =>
(UVarOf m # t) -> m (GTerm (UVarOf m) # t)
generalize) (UTermBody (UVarOf m) ('AHyperType t)
t forall s a. s -> Getting a s a -> a
^. forall (v1 :: AHyperType -> *) (ast :: AHyperType)
(v2 :: AHyperType -> *).
Lens (UTermBody v1 ast) (UTermBody v2 ast) (ast :# v1) (ast :# v2)
uBody)
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
v1 (forall (v :: AHyperType -> *) (ast :: AHyperType).
UTermBody v ast -> UTerm v ast
UTerm UTermBody (UVarOf m) ('AHyperType t)
t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
( if forall (h :: AHyperType -> *) a (p :: AHyperType -> *).
(HFoldable h, Monoid a) =>
(forall (n :: AHyperType -> *). HWitness h n -> (p # n) -> a)
-> (h # p) -> a
hfoldMap (forall {k} (t :: k). Proxy t
Proxy @(UnifyGen m) forall (h :: AHyperType -> *)
(c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> Bool -> All
All forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s a. Getting Any s a -> s -> Bool
Lens.has forall (v :: AHyperType -> *) (ast :: AHyperType).
Prism' (GTerm v ast) (v ast)
_GMono) t # GTerm (UVarOf m)
b forall s a. s -> Getting a s a -> a
^. forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
Lens._Wrapped
then forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GMono UVarOf m # t
v1
else forall (v :: AHyperType -> *) (ast :: AHyperType).
(ast :# GTerm v) -> GTerm v ast
GBody t # GTerm (UVarOf m)
b
)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
Proxy m -> RecMethod (UnifyGen m) t
unifyGenRecursive (forall {k} (t :: k). Proxy t
Proxy @m) (forall {k} (t :: k). Proxy t
Proxy @t)
UResolving UTermBody (UVarOf m) ('AHyperType t)
t -> forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GMono UVarOf m # t
v1 forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *) (t :: AHyperType -> *) a.
Unify m t =>
(UVarOf m # t) -> (UTermBody (UVarOf m) # t) -> m a
occursError UVarOf m # t
v1 UTermBody (UVarOf m) ('AHyperType t)
t
UTerm (UVarOf m) ('AHyperType t)
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GMono UVarOf m # t
v1)
{-# INLINE instantiateForAll #-}
instantiateForAll ::
forall m t.
UnifyGen m t =>
(TypeConstraintsOf t -> UTerm (UVarOf m) # t) ->
UVarOf m # t ->
WriterT [m ()] m (UVarOf m # t)
instantiateForAll :: forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
(TypeConstraintsOf t -> UTerm (UVarOf m) # t)
-> (UVarOf m # t) -> WriterT [m ()] m (UVarOf m # t)
instantiateForAll TypeConstraintsOf t -> UTerm (UVarOf m) # t
cons UVarOf m # t
x =
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (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
x)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
USkolem TypeConstraintsOf (GetHyperType ('AHyperType t))
l ->
do
forall (m :: * -> *) w. Monad m => w -> WriterT w m ()
tell [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
x (forall (v :: AHyperType -> *) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
USkolem TypeConstraintsOf (GetHyperType ('AHyperType t))
l)]
UVarOf m # t
r <- forall (m :: * -> *) (t :: AHyperType -> *).
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 :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (UTerm v # t) -> m (v # t)
newVar forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeConstraintsOf t -> UTerm (UVarOf m) # t
cons forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Semigroup a => a -> a -> a
<> TypeConstraintsOf (GetHyperType ('AHyperType t))
l) forall a b. a -> (a -> b) -> b
& forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> UTerm v ast
UInstantiated UVarOf m # t
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
x forall a b. a -> (a -> b) -> b
& forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
forall (f :: * -> *) a. Applicative f => a -> f a
pure UVarOf m # t
r
UInstantiated UVarOf m # t
v -> forall (f :: * -> *) a. Applicative f => a -> f a
pure UVarOf m # t
v
UTerm (UVarOf m) # t
_ -> forall a. HasCallStack => String -> a
error String
"unexpected state at instantiate's forall"
{-# INLINE instantiateH #-}
instantiateH ::
forall m t.
UnifyGen m t =>
(forall n. TypeConstraintsOf n -> UTerm (UVarOf m) # n) ->
GTerm (UVarOf m) # t ->
WriterT [m ()] m (UVarOf m # t)
instantiateH :: forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
(forall (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n)
-> (GTerm (UVarOf m) # t) -> WriterT [m ()] m (UVarOf m # t)
instantiateH forall (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n
_ (GMono UVarOf m ('AHyperType t)
x) = forall (f :: * -> *) a. Applicative f => a -> f a
pure UVarOf m ('AHyperType t)
x
instantiateH forall (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n
cons (GPoly UVarOf m ('AHyperType t)
x) = forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
(TypeConstraintsOf t -> UTerm (UVarOf m) # t)
-> (UVarOf m # t) -> WriterT [m ()] m (UVarOf m # t)
instantiateForAll forall (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n
cons UVarOf m ('AHyperType t)
x
instantiateH forall (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n
cons (GBody 'AHyperType t :# GTerm (UVarOf m)
x) =
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 @(UnifyGen m) 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 -> *).
UnifyGen m t =>
(forall (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n)
-> (GTerm (UVarOf m) # t) -> WriterT [m ()] m (UVarOf m # t)
instantiateH forall (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n
cons) 'AHyperType t :# GTerm (UVarOf m)
x
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
(t # UVarOf m) -> m (UVarOf m # t)
newTerm
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
Proxy m -> RecMethod (UnifyGen m) t
unifyGenRecursive (forall {k} (t :: k). Proxy t
Proxy @m) (forall {k} (t :: k). Proxy t
Proxy @t)
{-# INLINE instantiateWith #-}
instantiateWith ::
forall m t a.
UnifyGen m t =>
m a ->
(forall n. TypeConstraintsOf n -> UTerm (UVarOf m) # n) ->
GTerm (UVarOf m) # t ->
m (UVarOf m # t, a)
instantiateWith :: forall (m :: * -> *) (t :: AHyperType -> *) a.
UnifyGen m t =>
m a
-> (forall (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n)
-> (GTerm (UVarOf m) # t)
-> m (UVarOf m # t, a)
instantiateWith m a
action forall (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n
cons GTerm (UVarOf m) # t
g =
do
(UVarOf m # t
r, [m ()]
recover) <- forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
(forall (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n)
-> (GTerm (UVarOf m) # t) -> WriterT [m ()] m (UVarOf m # t)
instantiateH forall (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n
cons GTerm (UVarOf m) # t
g)
m a
action forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [m ()]
recover forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (UVarOf m # t
r,)
{-# INLINE instantiate #-}
instantiate ::
UnifyGen m t =>
GTerm (UVarOf m) # t ->
m (UVarOf m # t)
instantiate :: forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
(GTerm (UVarOf m) # t) -> m (UVarOf m # t)
instantiate GTerm (UVarOf m) # t
g = forall (m :: * -> *) (t :: AHyperType -> *) a.
UnifyGen m t =>
m a
-> (forall (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n)
-> (GTerm (UVarOf m) # t)
-> m (UVarOf m # t, a)
instantiateWith (forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) forall (v :: AHyperType -> *) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
UUnbound GTerm (UVarOf m) # t
g forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (forall s a. s -> Getting a s a -> a
^. forall s t a b. Field1 s t a b => Lens s t a b
Lens._1)