{-# LANGUAGE UndecidableInstances, TemplateHaskell, FlexibleContexts, FlexibleInstances #-}
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 x. GTerm v ast -> Rep (GTerm v ast) x)
-> (forall x. Rep (GTerm v ast) x -> GTerm v ast)
-> Generic (GTerm v ast)
forall x. Rep (GTerm v ast) x -> GTerm v ast
forall x. GTerm v ast -> Rep (GTerm v ast) x
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 :: HWitness (HFlip GTerm a) n -> Proxy c -> (c n => r) -> r
hLiftConstraint (HWitness HWitnessType (HFlip GTerm a) n
HRecSelf) = (r -> r) -> Proxy c -> r -> r
forall a b. a -> b -> a
const r -> r
forall a. a -> a
id
hLiftConstraint (HWitness (HRecSub c n)) = HWitness a c -> HRecWitness c n -> Proxy c -> (c n => r) -> r
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 :: 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 =
Dict (HNodesConstraint a RNodes)
-> (HNodesConstraint a RNodes => r) -> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy (RNodes a) -> Dict (HNodesConstraint a RNodes)
forall (c :: (AHyperType -> *) -> Constraint)
(h :: AHyperType -> *) (proxy :: Constraint -> *).
(Recursive c, HNodes h, c h) =>
proxy (c h) -> Dict (HNodesConstraint h c)
recurse (Proxy (RNodes a)
forall k (t :: k). Proxy t
Proxy @(RNodes a))) ((HNodesConstraint a RNodes => r) -> r)
-> (HNodesConstraint a RNodes => r) -> r
forall a b. (a -> b) -> a -> b
$
Dict (HNodesConstraint a c) -> (HNodesConstraint a c => r) -> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy (c a) -> Dict (HNodesConstraint a c)
forall (c :: (AHyperType -> *) -> Constraint)
(h :: AHyperType -> *) (proxy :: Constraint -> *).
(Recursive c, HNodes h, c h) =>
proxy (c h) -> Dict (HNodesConstraint h c)
recurse (Proxy (c a)
forall k (t :: k). Proxy t
Proxy @(c a))) ((HNodesConstraint a c => r) -> r)
-> (HNodesConstraint a c => r) -> r
forall a b. (a -> b) -> a -> b
$
HWitness a b -> Proxy RNodes -> (RNodes b => r) -> r
forall (h :: AHyperType -> *)
(c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
HWitness h n -> Proxy c -> (c n => r) -> r
hLiftConstraint HWitness a b
c (Proxy RNodes
forall k (t :: k). Proxy t
Proxy @RNodes)
( HWitness a b -> Proxy c -> (c b => r) -> r
forall (h :: AHyperType -> *)
(c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
HWitness h n -> Proxy c -> (c n => r) -> r
hLiftConstraint HWitness a b
c Proxy c
p
(HWitness (HFlip GTerm b) n -> Proxy c -> (c n => r) -> r
forall (h :: AHyperType -> *)
(c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
HWitness h n -> Proxy c -> (c n => r) -> r
hLiftConstraint (HWitnessType (HFlip GTerm b) n -> HWitness (HFlip GTerm b) n
forall (h :: AHyperType -> *) (n :: AHyperType -> *).
HWitnessType h n -> HWitness h n
HWitness @(HFlip GTerm _) HWitnessType (HFlip GTerm b) n
HRecWitness b n
n) Proxy c
p c n => r
f)
)
instance Recursively HFunctor ast => HFunctor (HFlip GTerm ast) where
{-# INLINE hmap #-}
hmap :: (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 =
((GTerm p # ast) -> Identity (GTerm q # ast))
-> (HFlip GTerm ast # p) -> Identity (HFlip GTerm ast # q)
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 (((GTerm p # ast) -> Identity (GTerm q # ast))
-> (HFlip GTerm ast # p) -> Identity (HFlip GTerm ast # q))
-> ((GTerm p # ast) -> GTerm q # ast)
-> (HFlip GTerm ast # p)
-> HFlip GTerm ast # q
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~
\case
GMono p ('AHyperType ast)
x -> HWitness (HFlip GTerm ast) ast -> p ('AHyperType ast) -> q # ast
forall (n :: AHyperType -> *).
HWitness (HFlip GTerm ast) n -> (p # n) -> q # n
f (HWitnessType (HFlip GTerm ast) ast
-> HWitness (HFlip GTerm ast) ast
forall (h :: AHyperType -> *) (n :: AHyperType -> *).
HWitnessType h n -> HWitness h n
HWitness HWitnessType (HFlip GTerm ast) ast
forall (h :: AHyperType -> *). HRecWitness h h
HRecSelf) p ('AHyperType ast)
x (q # ast) -> ((q # ast) -> GTerm q # ast) -> GTerm q # ast
forall a b. a -> (a -> b) -> b
& (q # ast) -> GTerm q # ast
forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GMono
GPoly p ('AHyperType ast)
x -> HWitness (HFlip GTerm ast) ast -> p ('AHyperType ast) -> q # ast
forall (n :: AHyperType -> *).
HWitness (HFlip GTerm ast) n -> (p # n) -> q # n
f (HWitnessType (HFlip GTerm ast) ast
-> HWitness (HFlip GTerm ast) ast
forall (h :: AHyperType -> *) (n :: AHyperType -> *).
HWitnessType h n -> HWitness h n
HWitness HWitnessType (HFlip GTerm ast) ast
forall (h :: AHyperType -> *). HRecWitness h h
HRecSelf) p ('AHyperType ast)
x (q # ast) -> ((q # ast) -> GTerm q # ast) -> GTerm q # ast
forall a b. a -> (a -> b) -> b
& (q # ast) -> GTerm q # ast
forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GPoly
GBody 'AHyperType ast :# GTerm p
x ->
Dict (HFunctor ast, HNodesConstraint ast (Recursively HFunctor))
-> ((HFunctor ast, HNodesConstraint ast (Recursively HFunctor)) =>
GTerm q # ast)
-> GTerm q # ast
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy (HFunctor ast)
-> Dict (HFunctor ast, HNodesConstraint ast (Recursively HFunctor))
forall (c :: (AHyperType -> *) -> Constraint)
(h :: AHyperType -> *) (proxy :: Constraint -> *).
Recursively c h =>
proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))
recursively (Proxy (HFunctor ast)
forall k (t :: k). Proxy t
Proxy @(HFunctor ast))) (((HFunctor ast, HNodesConstraint ast (Recursively HFunctor)) =>
GTerm q # ast)
-> GTerm q # ast)
-> ((HFunctor ast, HNodesConstraint ast (Recursively HFunctor)) =>
GTerm q # ast)
-> GTerm q # ast
forall a b. (a -> b) -> a -> b
$
(forall (n :: AHyperType -> *).
HWitness ast n -> (GTerm p # n) -> GTerm q # n)
-> (ast # GTerm p) -> ast # GTerm q
forall (h :: AHyperType -> *) (p :: AHyperType -> *)
(q :: AHyperType -> *).
HFunctor h =>
(forall (n :: AHyperType -> *). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap
( \HWitness ast n
cw ->
HWitness ast n
-> Proxy (Recursively HFunctor)
-> (Recursively HFunctor n => (GTerm p # n) -> GTerm q # n)
-> (GTerm p # n)
-> GTerm q # n
forall (h :: AHyperType -> *)
(c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
HWitness h n -> Proxy c -> (c n => r) -> r
hLiftConstraint HWitness ast n
cw (Proxy (Recursively HFunctor)
forall k (t :: k). Proxy t
Proxy @(Recursively HFunctor)) ((Recursively HFunctor n => (GTerm p # n) -> GTerm q # n)
-> (GTerm p # n) -> GTerm q # n)
-> (Recursively HFunctor n => (GTerm p # n) -> GTerm q # n)
-> (GTerm p # n)
-> GTerm q # n
forall a b. (a -> b) -> a -> b
$
((HFlip GTerm n # p) -> Identity (HFlip GTerm n # q))
-> (GTerm p # n) -> Identity (GTerm q # n)
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 (((HFlip GTerm n # p) -> Identity (HFlip GTerm n # q))
-> (GTerm p # n) -> Identity (GTerm q # n))
-> ((HFlip GTerm n # p) -> HFlip GTerm n # q)
-> (GTerm p # n)
-> GTerm q # n
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~
(forall (n :: AHyperType -> *).
HWitness (HFlip GTerm n) n -> (p # n) -> q # n)
-> (HFlip GTerm n # p) -> HFlip GTerm n # q
forall (h :: AHyperType -> *) (p :: AHyperType -> *)
(q :: AHyperType -> *).
HFunctor h =>
(forall (n :: AHyperType -> *). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap (HWitness (HFlip GTerm ast) n -> (p # n) -> q # n
forall (n :: AHyperType -> *).
HWitness (HFlip GTerm ast) n -> (p # n) -> q # n
f (HWitness (HFlip GTerm ast) n -> (p # n) -> q # n)
-> (HWitness (HFlip GTerm n) n -> HWitness (HFlip GTerm ast) n)
-> HWitness (HFlip GTerm n) n
-> (p # n)
-> q # n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(HWitness HWitnessType (HFlip GTerm n) n
nw) -> HWitnessType (HFlip GTerm ast) n -> HWitness (HFlip GTerm ast) n
forall (h :: AHyperType -> *) (n :: AHyperType -> *).
HWitnessType h n -> HWitness h n
HWitness (HWitness ast n -> HRecWitness n n -> HRecWitness ast n
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
HRecWitness n n
nw)))
) ast # GTerm p
'AHyperType ast :# GTerm p
x
(ast # GTerm q)
-> ((ast # GTerm q) -> GTerm q # ast) -> GTerm q # ast
forall a b. a -> (a -> b) -> b
& (ast # GTerm q) -> GTerm q # ast
forall (v :: AHyperType -> *) (ast :: AHyperType).
(ast :# GTerm v) -> GTerm v ast
GBody
instance Recursively HFoldable ast => HFoldable (HFlip GTerm ast) where
{-# INLINE hfoldMap #-}
hfoldMap :: (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 -> HWitness (HFlip GTerm ast) ast -> p ('AHyperType ast) -> a
forall (n :: AHyperType -> *).
HWitness (HFlip GTerm ast) n -> (p # n) -> a
f (HWitnessType (HFlip GTerm ast) ast
-> HWitness (HFlip GTerm ast) ast
forall (h :: AHyperType -> *) (n :: AHyperType -> *).
HWitnessType h n -> HWitness h n
HWitness HWitnessType (HFlip GTerm ast) ast
forall (h :: AHyperType -> *). HRecWitness h h
HRecSelf) p ('AHyperType ast)
x
GPoly p ('AHyperType ast)
x -> HWitness (HFlip GTerm ast) ast -> p ('AHyperType ast) -> a
forall (n :: AHyperType -> *).
HWitness (HFlip GTerm ast) n -> (p # n) -> a
f (HWitnessType (HFlip GTerm ast) ast
-> HWitness (HFlip GTerm ast) ast
forall (h :: AHyperType -> *) (n :: AHyperType -> *).
HWitnessType h n -> HWitness h n
HWitness HWitnessType (HFlip GTerm ast) ast
forall (h :: AHyperType -> *). HRecWitness h h
HRecSelf) p ('AHyperType ast)
x
GBody 'AHyperType ast :# GTerm p
x ->
Dict (HFoldable ast, HNodesConstraint ast (Recursively HFoldable))
-> ((HFoldable ast,
HNodesConstraint ast (Recursively HFoldable)) =>
a)
-> a
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy (HFoldable ast)
-> Dict
(HFoldable ast, HNodesConstraint ast (Recursively HFoldable))
forall (c :: (AHyperType -> *) -> Constraint)
(h :: AHyperType -> *) (proxy :: Constraint -> *).
Recursively c h =>
proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))
recursively (Proxy (HFoldable ast)
forall k (t :: k). Proxy t
Proxy @(HFoldable ast))) (((HFoldable ast, HNodesConstraint ast (Recursively HFoldable)) =>
a)
-> a)
-> ((HFoldable ast,
HNodesConstraint ast (Recursively HFoldable)) =>
a)
-> a
forall a b. (a -> b) -> a -> b
$
(forall (n :: AHyperType -> *).
HWitness ast n -> (GTerm p # n) -> a)
-> (ast # GTerm p) -> a
forall (h :: AHyperType -> *) a (p :: AHyperType -> *).
(HFoldable h, Monoid a) =>
(forall (n :: AHyperType -> *). HWitness h n -> (p # n) -> a)
-> (h # p) -> a
hfoldMap
( \HWitness ast n
cw ->
HWitness ast n
-> Proxy (Recursively HFoldable)
-> (Recursively HFoldable n => (GTerm p # n) -> a)
-> (GTerm p # n)
-> a
forall (h :: AHyperType -> *)
(c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
HWitness h n -> Proxy c -> (c n => r) -> r
hLiftConstraint HWitness ast n
cw (Proxy (Recursively HFoldable)
forall k (t :: k). Proxy t
Proxy @(Recursively HFoldable)) ((Recursively HFoldable n => (GTerm p # n) -> a)
-> (GTerm p # n) -> a)
-> (Recursively HFoldable n => (GTerm p # n) -> a)
-> (GTerm p # n)
-> a
forall a b. (a -> b) -> a -> b
$
(forall (n :: AHyperType -> *).
HWitness (HFlip GTerm n) n -> (p # n) -> a)
-> (HFlip GTerm n # p) -> a
forall (h :: AHyperType -> *) a (p :: AHyperType -> *).
(HFoldable h, Monoid a) =>
(forall (n :: AHyperType -> *). HWitness h n -> (p # n) -> a)
-> (h # p) -> a
hfoldMap (HWitness (HFlip GTerm ast) n -> (p # n) -> a
forall (n :: AHyperType -> *).
HWitness (HFlip GTerm ast) n -> (p # n) -> a
f (HWitness (HFlip GTerm ast) n -> (p # n) -> a)
-> (HWitness (HFlip GTerm n) n -> HWitness (HFlip GTerm ast) n)
-> HWitness (HFlip GTerm n) n
-> (p # n)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(HWitness HWitnessType (HFlip GTerm n) n
nw) -> HWitnessType (HFlip GTerm ast) n -> HWitness (HFlip GTerm ast) n
forall (h :: AHyperType -> *) (n :: AHyperType -> *).
HWitnessType h n -> HWitness h n
HWitness (HWitness ast n -> HRecWitness n n -> HRecWitness ast n
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
HRecWitness n n
nw)))
((HFlip GTerm n # p) -> a)
-> ((GTerm p # n) -> HFlip GTerm n # p) -> (GTerm p # n) -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Tagged (GTerm p # n) (Identity (GTerm p # n))
-> Tagged (HFlip GTerm n # p) (Identity (HFlip GTerm n # p))
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 (Tagged (GTerm p # n) (Identity (GTerm p # n))
-> Tagged (HFlip GTerm n # p) (Identity (HFlip GTerm n # p)))
-> (GTerm p # n) -> HFlip GTerm n # p
forall t b. AReview t b -> b -> t
#)
) ast # GTerm p
'AHyperType ast :# GTerm p
x
(GTerm p ('AHyperType ast) -> a)
-> ((HFlip GTerm ast # p) -> GTerm p ('AHyperType ast))
-> (HFlip GTerm ast # p)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((HFlip GTerm ast # p)
-> Getting
(GTerm p ('AHyperType ast))
(HFlip GTerm ast # p)
(GTerm p ('AHyperType ast))
-> GTerm p ('AHyperType ast)
forall s a. s -> Getting a s a -> a
^. Getting
(GTerm p ('AHyperType ast))
(HFlip GTerm ast # p)
(GTerm p ('AHyperType ast))
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 :: (HFlip GTerm ast # ContainedH f p) -> f (HFlip GTerm ast # p)
hsequence =
\case
GMono ContainedH f p ('AHyperType ast)
x -> ContainedH f p ('AHyperType ast) -> f (p ('AHyperType ast))
forall (f :: * -> *) (p :: AHyperType -> *) (h :: AHyperType).
ContainedH f p h -> f (p h)
runContainedH ContainedH f p ('AHyperType ast)
x f (p ('AHyperType ast))
-> (p ('AHyperType ast) -> GTerm p ('AHyperType ast))
-> f (GTerm p ('AHyperType ast))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> p ('AHyperType ast) -> GTerm p ('AHyperType ast)
forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GMono
GPoly ContainedH f p ('AHyperType ast)
x -> ContainedH f p ('AHyperType ast) -> f (p ('AHyperType ast))
forall (f :: * -> *) (p :: AHyperType -> *) (h :: AHyperType).
ContainedH f p h -> f (p h)
runContainedH ContainedH f p ('AHyperType ast)
x f (p ('AHyperType ast))
-> (p ('AHyperType ast) -> GTerm p ('AHyperType ast))
-> f (GTerm p ('AHyperType ast))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> p ('AHyperType ast) -> GTerm p ('AHyperType ast)
forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GPoly
GBody 'AHyperType ast :# GTerm (ContainedH f p)
x ->
Dict (HNodesConstraint ast RTraversable)
-> (HNodesConstraint ast RTraversable =>
f (GTerm p ('AHyperType ast)))
-> f (GTerm p ('AHyperType ast))
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy (RTraversable ast)
-> Dict (HNodesConstraint ast RTraversable)
forall (c :: (AHyperType -> *) -> Constraint)
(h :: AHyperType -> *) (proxy :: Constraint -> *).
(Recursive c, HNodes h, c h) =>
proxy (c h) -> Dict (HNodesConstraint h c)
recurse (Proxy (RTraversable ast)
forall k (t :: k). Proxy t
Proxy @(RTraversable ast))) ((HNodesConstraint ast RTraversable =>
f (GTerm p ('AHyperType ast)))
-> f (GTerm p ('AHyperType ast)))
-> (HNodesConstraint ast RTraversable =>
f (GTerm p ('AHyperType ast)))
-> f (GTerm p ('AHyperType ast))
forall a b. (a -> b) -> a -> b
$
(forall (n :: AHyperType -> *).
HWitness ast n -> (GTerm (ContainedH f p) # n) -> f (GTerm p # n))
-> (ast # GTerm (ContainedH f p)) -> f (ast # GTerm p)
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 (Proxy RTraversable
forall k (t :: k). Proxy t
Proxy @RTraversable Proxy RTraversable
-> (RTraversable n =>
(GTerm (ContainedH f p) # n) -> f (GTerm p # n))
-> HWitness ast n
-> (GTerm (ContainedH f p) # n)
-> f (GTerm p # n)
forall (h :: AHyperType -> *)
(c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> ((HFlip GTerm n # ContainedH f p) -> f (HFlip GTerm n # p))
-> (GTerm (ContainedH f p) # n) -> f (GTerm p # n)
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 (HFlip GTerm n # ContainedH f p) -> f (HFlip GTerm n # p)
forall (h :: AHyperType -> *) (f :: * -> *) (p :: AHyperType -> *).
(HTraversable h, Applicative f) =>
(h # ContainedH f p) -> f (h # p)
hsequence) ast # GTerm (ContainedH f p)
'AHyperType ast :# GTerm (ContainedH f p)
x
f (ast # GTerm p)
-> ((ast # GTerm p) -> GTerm p ('AHyperType ast))
-> f (GTerm p ('AHyperType ast))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (ast # GTerm p) -> GTerm p ('AHyperType ast)
forall (v :: AHyperType -> *) (ast :: AHyperType).
(ast :# GTerm v) -> GTerm v ast
GBody
(GTerm (ContainedH f p) ('AHyperType ast)
-> f (GTerm p ('AHyperType ast)))
-> ((GTerm (ContainedH f p) ('AHyperType ast)
-> f (GTerm p ('AHyperType ast)))
-> (HFlip GTerm ast # ContainedH f p) -> f (HFlip GTerm ast # p))
-> (HFlip GTerm ast # ContainedH f p)
-> f (HFlip GTerm ast # p)
forall a b. a -> (a -> b) -> b
& (GTerm (ContainedH f p) ('AHyperType ast)
-> f (GTerm p ('AHyperType ast)))
-> (HFlip GTerm ast # ContainedH f p) -> f (HFlip GTerm ast # p)
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 :: (UVarOf m # t) -> m (GTerm (UVarOf m) # t)
generalize UVarOf m # t
v0 =
do
(UVarOf m # t
v1, UTerm (UVarOf m) ('AHyperType t)
u) <- (UVarOf m # t)
-> m (UVarOf m # t, UTerm (UVarOf m) ('AHyperType t))
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 <- Proxy t -> m (TypeConstraintsOf t)
forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
Proxy t -> m (TypeConstraintsOf t)
scopeConstraints (Proxy t
forall k (t :: k). Proxy t
Proxy @t)
case UTerm (UVarOf m) ('AHyperType t)
u of
UUnbound TypeConstraintsOf (GetHyperType ('AHyperType t))
l | TypeConstraintsOf t -> TypeConstraintsOf t
forall c. TypeConstraints c => c -> c
toScopeConstraints TypeConstraintsOf t
TypeConstraintsOf (GetHyperType ('AHyperType t))
l TypeConstraintsOf t -> TypeConstraintsOf t -> Bool
forall a. PartialOrd a => a -> a -> Bool
`leq` TypeConstraintsOf t
c ->
(UVarOf m # t) -> GTerm (UVarOf m) # t
forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GPoly UVarOf m # t
v1 (GTerm (UVarOf m) # t) -> m () -> m (GTerm (UVarOf m) # t)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$
BindingDict (UVarOf m) m t
-> (UVarOf m # t) -> UTerm (UVarOf m) ('AHyperType t) -> m ()
forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (v # t) -> (UTerm v # t) -> m ()
bindVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
v1 (TypeConstraintsOf (GetHyperType ('AHyperType t))
-> UTerm (UVarOf m) ('AHyperType t)
forall (v :: AHyperType -> *) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
USkolem (TypeConstraintsOf t -> TypeConstraintsOf t
forall c. TypeConstraints c => c -> c
generalizeConstraints TypeConstraintsOf t
TypeConstraintsOf (GetHyperType ('AHyperType t))
l))
USkolem TypeConstraintsOf (GetHyperType ('AHyperType t))
l | TypeConstraintsOf t -> TypeConstraintsOf t
forall c. TypeConstraints c => c -> c
toScopeConstraints TypeConstraintsOf t
TypeConstraintsOf (GetHyperType ('AHyperType t))
l TypeConstraintsOf t -> TypeConstraintsOf t -> Bool
forall a. PartialOrd a => a -> a -> Bool
`leq` TypeConstraintsOf t
c -> (GTerm (UVarOf m) # t) -> m (GTerm (UVarOf m) # t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((UVarOf m # t) -> GTerm (UVarOf m) # t
forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GPoly UVarOf m # t
v1)
UTerm UTermBody (UVarOf m) ('AHyperType t)
t ->
Dict (HNodesConstraint t (UnifyGen m))
-> (HNodesConstraint t (UnifyGen m) => m (GTerm (UVarOf m) # t))
-> m (GTerm (UVarOf m) # t)
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy m -> Proxy t -> Dict (HNodesConstraint t (UnifyGen m))
forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
Proxy m -> Proxy t -> Dict (HNodesConstraint t (UnifyGen m))
unifyGenRecursive (Proxy m
forall k (t :: k). Proxy t
Proxy @m) (Proxy t
forall k (t :: k). Proxy t
Proxy @t)) ((HNodesConstraint t (UnifyGen m) => m (GTerm (UVarOf m) # t))
-> m (GTerm (UVarOf m) # t))
-> (HNodesConstraint t (UnifyGen m) => m (GTerm (UVarOf m) # t))
-> m (GTerm (UVarOf m) # t)
forall a b. (a -> b) -> a -> b
$
do
BindingDict (UVarOf m) m t
-> (UVarOf m # t) -> UTerm (UVarOf m) ('AHyperType t) -> m ()
forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (v # t) -> (UTerm v # t) -> m ()
bindVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
v1 (UTermBody (UVarOf m) ('AHyperType t)
-> UTerm (UVarOf m) ('AHyperType t)
forall (v :: AHyperType -> *) (ast :: AHyperType).
UTermBody v ast -> UTerm v ast
UResolving UTermBody (UVarOf m) ('AHyperType t)
t)
t # GTerm (UVarOf m)
r <- (forall (n :: AHyperType -> *).
HWitness t n -> (UVarOf m # n) -> m (GTerm (UVarOf m) # n))
-> (t # UVarOf m) -> m (t # GTerm (UVarOf m))
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 (Proxy (UnifyGen m)
forall k (t :: k). Proxy t
Proxy @(UnifyGen m) Proxy (UnifyGen m)
-> (UnifyGen m n => (UVarOf m # n) -> m (GTerm (UVarOf m) # n))
-> HWitness t n
-> (UVarOf m # n)
-> m (GTerm (UVarOf m) # n)
forall (h :: AHyperType -> *)
(c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> UnifyGen m n => (UVarOf m # n) -> m (GTerm (UVarOf m) # n)
forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
(UVarOf m # t) -> m (GTerm (UVarOf m) # t)
generalize) (UTermBody (UVarOf m) ('AHyperType t)
t UTermBody (UVarOf m) ('AHyperType t)
-> Getting
(t # UVarOf m)
(UTermBody (UVarOf m) ('AHyperType t))
(t # UVarOf m)
-> t # UVarOf m
forall s a. s -> Getting a s a -> a
^. Getting
(t # UVarOf m)
(UTermBody (UVarOf m) ('AHyperType t))
(t # UVarOf m)
forall (v1 :: AHyperType -> *) (ast :: AHyperType)
(v2 :: AHyperType -> *).
Lens (UTermBody v1 ast) (UTermBody v2 ast) (ast :# v1) (ast :# v2)
uBody)
t # GTerm (UVarOf m)
r (t # GTerm (UVarOf m)) -> m () -> m (t # GTerm (UVarOf m))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ BindingDict (UVarOf m) m t
-> (UVarOf m # t) -> UTerm (UVarOf m) ('AHyperType t) -> m ()
forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (v # t) -> (UTerm v # t) -> m ()
bindVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
v1 (UTermBody (UVarOf m) ('AHyperType t)
-> UTerm (UVarOf m) ('AHyperType t)
forall (v :: AHyperType -> *) (ast :: AHyperType).
UTermBody v ast -> UTerm v ast
UTerm UTermBody (UVarOf m) ('AHyperType t)
t)
m (t # GTerm (UVarOf m))
-> ((t # GTerm (UVarOf m)) -> GTerm (UVarOf m) # t)
-> m (GTerm (UVarOf m) # t)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
\t # GTerm (UVarOf m)
b ->
if (forall (n :: AHyperType -> *).
HWitness t n -> (GTerm (UVarOf m) # n) -> All)
-> (t # GTerm (UVarOf m)) -> All
forall (h :: AHyperType -> *) a (p :: AHyperType -> *).
(HFoldable h, Monoid a) =>
(forall (n :: AHyperType -> *). HWitness h n -> (p # n) -> a)
-> (h # p) -> a
hfoldMap (Proxy (UnifyGen m)
forall k (t :: k). Proxy t
Proxy @(UnifyGen m) Proxy (UnifyGen m)
-> (UnifyGen m n => (GTerm (UVarOf m) # n) -> All)
-> HWitness t n
-> (GTerm (UVarOf m) # n)
-> All
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 (Bool -> All)
-> ((GTerm (UVarOf m) # n) -> Bool)
-> (GTerm (UVarOf m) # n)
-> All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting Any (GTerm (UVarOf m) # n) (UVarOf m ('AHyperType n))
-> (GTerm (UVarOf m) # n) -> Bool
forall s a. Getting Any s a -> s -> Bool
Lens.has Getting Any (GTerm (UVarOf m) # n) (UVarOf m ('AHyperType n))
forall (v :: AHyperType -> *) (ast :: AHyperType).
Prism' (GTerm v ast) (v ast)
_GMono) t # GTerm (UVarOf m)
b All -> Getting Bool All Bool -> Bool
forall s a. s -> Getting a s a -> a
^. Getting Bool All Bool
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
Lens._Wrapped
then (UVarOf m # t) -> GTerm (UVarOf m) # t
forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GMono UVarOf m # t
v1
else ('AHyperType t :# GTerm (UVarOf m)) -> GTerm (UVarOf m) # t
forall (v :: AHyperType -> *) (ast :: AHyperType).
(ast :# GTerm v) -> GTerm v ast
GBody t # GTerm (UVarOf m)
'AHyperType t :# GTerm (UVarOf m)
b
UResolving UTermBody (UVarOf m) ('AHyperType t)
t -> (UVarOf m # t) -> GTerm (UVarOf m) # t
forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GMono UVarOf m # t
v1 (GTerm (UVarOf m) # t) -> m Any -> m (GTerm (UVarOf m) # t)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (UVarOf m # t) -> UTermBody (UVarOf m) ('AHyperType t) -> m Any
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)
_ -> (GTerm (UVarOf m) # t) -> m (GTerm (UVarOf m) # t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((UVarOf m # t) -> GTerm (UVarOf m) # t
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 :: (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 =
BindingDict (UVarOf m) m t
-> (UVarOf m # t) -> m (UTerm (UVarOf m) # t)
forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (v # t) -> m (UTerm v # t)
lookupVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
x m (UTerm (UVarOf m) # t)
-> (m (UTerm (UVarOf m) # t)
-> WriterT [m ()] m (UTerm (UVarOf m) # t))
-> WriterT [m ()] m (UTerm (UVarOf m) # t)
forall a b. a -> (a -> b) -> b
& m (UTerm (UVarOf m) # t) -> WriterT [m ()] m (UTerm (UVarOf m) # t)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
WriterT [m ()] m (UTerm (UVarOf m) # t)
-> ((UTerm (UVarOf m) # t) -> WriterT [m ()] m (UVarOf m # t))
-> WriterT [m ()] m (UVarOf m # t)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
\case
USkolem TypeConstraintsOf (GetHyperType ('AHyperType t))
l ->
do
[m ()] -> WriterT [m ()] m ()
forall (m :: * -> *) w. Monad m => w -> WriterT w m ()
tell [BindingDict (UVarOf m) m t
-> (UVarOf m # t) -> (UTerm (UVarOf m) # t) -> m ()
forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (v # t) -> (UTerm v # t) -> m ()
bindVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
x (TypeConstraintsOf (GetHyperType ('AHyperType t))
-> UTerm (UVarOf m) # t
forall (v :: AHyperType -> *) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
USkolem TypeConstraintsOf (GetHyperType ('AHyperType t))
l)]
UVarOf m # t
r <- Proxy t -> m (TypeConstraintsOf t)
forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
Proxy t -> m (TypeConstraintsOf t)
scopeConstraints (Proxy t
forall k (t :: k). Proxy t
Proxy @t) m (TypeConstraintsOf t)
-> (TypeConstraintsOf t -> TypeConstraintsOf t)
-> m (TypeConstraintsOf t)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (TypeConstraintsOf t -> TypeConstraintsOf t -> TypeConstraintsOf t
forall a. Semigroup a => a -> a -> a
<> TypeConstraintsOf t
TypeConstraintsOf (GetHyperType ('AHyperType t))
l) 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 :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (UTerm v # t) -> m (v # t)
newVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: AHyperType -> *).
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
cons m (UVarOf m # t)
-> (m (UVarOf m # t) -> WriterT [m ()] m (UVarOf m # t))
-> WriterT [m ()] m (UVarOf m # t)
forall a b. a -> (a -> b) -> b
& m (UVarOf m # t) -> WriterT [m ()] m (UVarOf m # t)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
(UVarOf m # t) -> UTerm (UVarOf m) # t
forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> UTerm v ast
UInstantiated UVarOf m # t
r (UTerm (UVarOf m) # t) -> ((UTerm (UVarOf m) # t) -> m ()) -> m ()
forall a b. a -> (a -> b) -> b
& BindingDict (UVarOf m) m t
-> (UVarOf m # t) -> (UTerm (UVarOf m) # t) -> m ()
forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (v # t) -> (UTerm v # t) -> m ()
bindVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
x m () -> (m () -> WriterT [m ()] m ()) -> WriterT [m ()] m ()
forall a b. a -> (a -> b) -> b
& m () -> WriterT [m ()] m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
(UVarOf m # t) -> WriterT [m ()] m (UVarOf m # t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure UVarOf m # t
r
UInstantiated UVarOf m # t
v -> (UVarOf m # t) -> WriterT [m ()] m (UVarOf m # t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure UVarOf m # t
v
UTerm (UVarOf m) # t
_ -> String -> WriterT [m ()] m (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 (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 # t
x) = (UVarOf m # t) -> WriterT [m ()] m (UVarOf m # t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure UVarOf m # t
x
instantiateH forall (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n
cons (GPoly UVarOf m # t
x) = (TypeConstraintsOf t -> UTerm (UVarOf m) # t)
-> (UVarOf m # t) -> WriterT [m ()] m (UVarOf m # t)
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
forall (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n
cons UVarOf m # t
x
instantiateH forall (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n
cons (GBody 'AHyperType t :# GTerm (UVarOf m)
x) =
Dict (HNodesConstraint t (UnifyGen m))
-> (HNodesConstraint t (UnifyGen m) =>
WriterT [m ()] m (UVarOf m # t))
-> WriterT [m ()] m (UVarOf m # t)
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy m -> Proxy t -> Dict (HNodesConstraint t (UnifyGen m))
forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
Proxy m -> Proxy t -> Dict (HNodesConstraint t (UnifyGen m))
unifyGenRecursive (Proxy m
forall k (t :: k). Proxy t
Proxy @m) (Proxy t
forall k (t :: k). Proxy t
Proxy @t)) ((HNodesConstraint t (UnifyGen m) =>
WriterT [m ()] m (UVarOf m # t))
-> WriterT [m ()] m (UVarOf m # t))
-> (HNodesConstraint t (UnifyGen m) =>
WriterT [m ()] m (UVarOf m # t))
-> WriterT [m ()] m (UVarOf m # t)
forall a b. (a -> b) -> a -> b
$
(forall (n :: AHyperType -> *).
HWitness t n
-> (GTerm (UVarOf m) # n) -> WriterT [m ()] m (UVarOf m # n))
-> (t # GTerm (UVarOf m)) -> WriterT [m ()] m (t # UVarOf m)
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 (Proxy (UnifyGen m)
forall k (t :: k). Proxy t
Proxy @(UnifyGen m) Proxy (UnifyGen m)
-> (UnifyGen m n =>
(GTerm (UVarOf m) # n) -> WriterT [m ()] m (UVarOf m # n))
-> HWitness t n
-> (GTerm (UVarOf m) # n)
-> WriterT [m ()] m (UVarOf m # n)
forall (h :: AHyperType -> *)
(c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> (forall (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n)
-> (GTerm (UVarOf m) # n) -> WriterT [m ()] m (UVarOf m # n)
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) t # GTerm (UVarOf m)
'AHyperType t :# GTerm (UVarOf m)
x WriterT [m ()] m (t # UVarOf m)
-> ((t # UVarOf m) -> WriterT [m ()] m (UVarOf m # t))
-> WriterT [m ()] m (UVarOf m # t)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= m (UVarOf m # t) -> WriterT [m ()] m (UVarOf m # t)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (UVarOf m # t) -> WriterT [m ()] m (UVarOf m # t))
-> ((t # UVarOf m) -> m (UVarOf m # t))
-> (t # UVarOf m)
-> WriterT [m ()] m (UVarOf m # t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (t # UVarOf m) -> m (UVarOf m # t)
forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
(t # UVarOf m) -> m (UVarOf m # t)
newTerm
{-# 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 :: 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 (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n)
-> (GTerm (UVarOf m) # t) -> WriterT [m ()] m (UVarOf m # t)
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
WriterT [m ()] m (UVarOf m # t)
-> (WriterT [m ()] m (UVarOf m # t) -> m (UVarOf m # t, [m ()]))
-> m (UVarOf m # t, [m ()])
forall a b. a -> (a -> b) -> b
& WriterT [m ()] m (UVarOf m # t) -> m (UVarOf m # t, [m ()])
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT
m a
action m a -> m () -> m a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* [m ()] -> m ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [m ()]
recover m a -> (a -> (UVarOf m # t, a)) -> m (UVarOf m # t, a)
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 :: (GTerm (UVarOf m) # t) -> m (UVarOf m # t)
instantiate GTerm (UVarOf m) # t
g = m ()
-> (forall (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n)
-> (GTerm (UVarOf m) # t)
-> m (UVarOf m # t, ())
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 ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) forall (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n
forall (v :: AHyperType -> *) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
UUnbound GTerm (UVarOf m) # t
g m (UVarOf m # t, ())
-> ((UVarOf m # t, ()) -> UVarOf m # t) -> m (UVarOf m # t)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> ((UVarOf m # t, ())
-> Getting (UVarOf m # t) (UVarOf m # t, ()) (UVarOf m # t)
-> UVarOf m # t
forall s a. s -> Getting a s a -> a
^. Getting (UVarOf m # t) (UVarOf m # t, ()) (UVarOf m # t)
forall s t a b. Field1 s t a b => Lens s t a b
Lens._1)