{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}
module Hyper.Syntax.Scheme
( Scheme (..)
, sForAlls
, sTyp
, W_Scheme (..)
, QVars (..)
, _QVars
, HasScheme (..)
, loadScheme
, saveScheme
, MonadInstantiate (..)
, inferType
, QVarInstances (..)
, _QVarInstances
, makeQVarInstances
) where
import qualified Control.Lens as Lens
import Control.Monad.Trans.Class (MonadTrans (..))
import Control.Monad.Trans.State (StateT (..))
import qualified Data.Map as Map
import Hyper
import Hyper.Class.Optic (HNodeLens (..))
import Hyper.Infer
import Hyper.Recurse
import Hyper.Unify
import Hyper.Unify.Generalize
import Hyper.Unify.New (newTerm)
import Hyper.Unify.QuantifiedVar (HasQuantifiedVar (..), MonadQuantify (..), OrdQVar)
import Hyper.Unify.Term (UTerm (..), uBody)
import Text.PrettyPrint ((<+>))
import qualified Text.PrettyPrint as Pretty
import Text.PrettyPrint.HughesPJClass (Pretty (..), maybeParens)
import Hyper.Internal.Prelude
data Scheme varTypes typ h = Scheme
{ forall (varTypes :: AHyperType -> *) (typ :: AHyperType -> *)
(h :: AHyperType).
Scheme varTypes typ h -> varTypes # QVars
_sForAlls :: varTypes # QVars
, forall (varTypes :: AHyperType -> *) (typ :: AHyperType -> *)
(h :: AHyperType).
Scheme varTypes typ h -> h :# typ
_sTyp :: h :# typ
}
deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (varTypes :: AHyperType -> *) (typ :: AHyperType -> *)
(h :: AHyperType) x.
Rep (Scheme varTypes typ h) x -> Scheme varTypes typ h
forall (varTypes :: AHyperType -> *) (typ :: AHyperType -> *)
(h :: AHyperType) x.
Scheme varTypes typ h -> Rep (Scheme varTypes typ h) x
$cto :: forall (varTypes :: AHyperType -> *) (typ :: AHyperType -> *)
(h :: AHyperType) x.
Rep (Scheme varTypes typ h) x -> Scheme varTypes typ h
$cfrom :: forall (varTypes :: AHyperType -> *) (typ :: AHyperType -> *)
(h :: AHyperType) x.
Scheme varTypes typ h -> Rep (Scheme varTypes typ h) x
Generic)
newtype QVars typ
= QVars
(Map (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ)))
deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (typ :: AHyperType) x. Rep (QVars typ) x -> QVars typ
forall (typ :: AHyperType) x. QVars typ -> Rep (QVars typ) x
$cto :: forall (typ :: AHyperType) x. Rep (QVars typ) x -> QVars typ
$cfrom :: forall (typ :: AHyperType) x. QVars typ -> Rep (QVars typ) x
Generic)
newtype QVarInstances h typ = QVarInstances (Map (QVar (GetHyperType typ)) (h typ))
deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (h :: AHyperType -> *) (typ :: AHyperType) x.
Rep (QVarInstances h typ) x -> QVarInstances h typ
forall (h :: AHyperType -> *) (typ :: AHyperType) x.
QVarInstances h typ -> Rep (QVarInstances h typ) x
$cto :: forall (h :: AHyperType -> *) (typ :: AHyperType) x.
Rep (QVarInstances h typ) x -> QVarInstances h typ
$cfrom :: forall (h :: AHyperType -> *) (typ :: AHyperType) x.
QVarInstances h typ -> Rep (QVarInstances h typ) x
Generic)
makeLenses ''Scheme
makePrisms ''QVars
makePrisms ''QVarInstances
makeCommonInstances [''Scheme, ''QVars, ''QVarInstances]
makeHTraversableApplyAndBases ''Scheme
instance RNodes t => RNodes (Scheme v t)
instance (c (Scheme v t), Recursively c t) => Recursively c (Scheme v t)
instance (HTraversable (Scheme v t), RTraversable t) => RTraversable (Scheme v t)
instance
( Ord (QVar (GetHyperType typ))
, Semigroup (TypeConstraintsOf (GetHyperType typ))
) =>
Semigroup (QVars typ)
where
QVars Map
(QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ))
m <> :: QVars typ -> QVars typ -> QVars typ
<> QVars Map
(QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ))
n = forall (typ :: AHyperType).
Map
(QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ))
-> QVars typ
QVars (forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith forall a. Semigroup a => a -> a -> a
(<>) Map
(QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ))
m Map
(QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ))
n)
instance
( Ord (QVar (GetHyperType typ))
, Semigroup (TypeConstraintsOf (GetHyperType typ))
) =>
Monoid (QVars typ)
where
mempty :: QVars typ
mempty = forall (typ :: AHyperType).
Map
(QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ))
-> QVars typ
QVars forall a. Monoid a => a
mempty
instance
(Pretty (varTypes # QVars), Pretty (h :# typ)) =>
Pretty (Scheme varTypes typ h)
where
pPrintPrec :: PrettyLevel -> Rational -> Scheme varTypes typ h -> Doc
pPrintPrec PrettyLevel
lvl Rational
p (Scheme varTypes # QVars
forAlls h :# typ
typ)
| Doc -> Bool
Pretty.isEmpty Doc
f = forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
p h :# typ
typ
| Bool
otherwise = Doc
f Doc -> Doc -> Doc
<+> forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
0 h :# typ
typ forall a b. a -> (a -> b) -> b
& Bool -> Doc -> Doc
maybeParens (Rational
p forall a. Ord a => a -> a -> Bool
> Rational
0)
where
f :: Doc
f = forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
0 varTypes # QVars
forAlls
instance
(Pretty (TypeConstraintsOf typ), Pretty (QVar typ)) =>
Pretty (QVars # typ)
where
pPrint :: (QVars # typ) -> Doc
pPrint (QVars Map
(QVar (GetHyperType ('AHyperType typ)))
(TypeConstraintsOf (GetHyperType ('AHyperType typ)))
qvars) =
Map
(QVar (GetHyperType ('AHyperType typ)))
(TypeConstraintsOf (GetHyperType ('AHyperType typ)))
qvars forall s i a. s -> IndexedGetting i (Endo [(i, a)]) s a -> [(i, a)]
^@.. forall i (t :: * -> *) a b.
TraversableWithIndex i t =>
IndexedTraversal i (t a) (t b) a b
Lens.itraversed
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (forall a. Semigroup a => a -> a -> a
<> String -> Doc
Pretty.text String
".") forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Doc
Pretty.text String
"∀" forall a. Semigroup a => a -> a -> a
<>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a} {a}. (Pretty a, Pretty a) => (a, a) -> Doc
printVar
forall a b. a -> (a -> b) -> b
& [Doc] -> Doc
Pretty.hsep
where
printVar :: (a, a) -> Doc
printVar (a
q, a
c)
| Doc
cP forall a. Eq a => a -> a -> Bool
== forall a. Monoid a => a
mempty = forall a. Pretty a => a -> Doc
pPrint a
q
| Bool
otherwise = forall a. Pretty a => a -> Doc
pPrint a
q forall a. Semigroup a => a -> a -> a
<> String -> Doc
Pretty.text String
"(" forall a. Semigroup a => a -> a -> a
<> Doc
cP forall a. Semigroup a => a -> a -> a
<> String -> Doc
Pretty.text String
")"
where
cP :: Doc
cP = forall a. Pretty a => a -> Doc
pPrint a
c
type instance Lens.Index (QVars typ) = QVar (GetHyperType typ)
type instance Lens.IxValue (QVars typ) = TypeConstraintsOf (GetHyperType typ)
instance Ord (QVar (GetHyperType typ)) => Lens.Ixed (QVars typ)
instance Ord (QVar (GetHyperType typ)) => Lens.At (QVars typ) where
at :: Index (QVars typ)
-> Lens' (QVars typ) (Maybe (IxValue (QVars typ)))
at Index (QVars typ)
h = forall (typ :: AHyperType) (typ :: AHyperType).
Iso
(QVars typ)
(QVars typ)
(Map
(QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ)))
(Map
(QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ)))
_QVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
Lens.at Index (QVars typ)
h
type instance InferOf (Scheme _ t) = HFlip GTerm t
class UnifyGen m t => MonadInstantiate m t where
localInstantiations ::
QVarInstances (UVarOf m) # t ->
m a ->
m a
lookupQVar :: QVar t -> m (UVarOf m # t)
instance
( HasInferredValue typ
, UnifyGen m typ
, HTraversable varTypes
, HNodesConstraint varTypes (MonadInstantiate m)
, Infer m typ
) =>
Infer m (Scheme varTypes typ)
where
{-# INLINE inferBody #-}
inferBody :: forall (h :: AHyperType -> *).
(Scheme varTypes typ # InferChild m h)
-> m (Scheme varTypes typ # h,
InferOf (Scheme varTypes typ) # UVarOf m)
inferBody (Scheme varTypes # QVars
vars 'AHyperType (InferChild m h) :# typ
typ) =
do
varTypes # QVarInstances (UVarOf m)
foralls <- 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 @(MonadInstantiate 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 :: * -> *) (typ :: AHyperType -> *).
Unify m typ =>
(QVars # typ) -> m (QVarInstances (UVarOf m) # typ)
makeQVarInstances) varTypes # QVars
vars
let withForalls :: m (InferredChild (UVarOf m) h ('AHyperType typ))
-> m (InferredChild (UVarOf m) h ('AHyperType typ))
withForalls =
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 @(MonadInstantiate 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 a. a -> [a] -> [a]
: []) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) (t :: AHyperType -> *) a.
MonadInstantiate m t =>
(QVarInstances (UVarOf m) # t) -> m a -> m a
localInstantiations)
varTypes # QVarInstances (UVarOf m)
foralls
forall a b. a -> (a -> b) -> b
& forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) forall a. a -> a
id
InferredChild h ('AHyperType typ)
typI InferOf (GetHyperType ('AHyperType typ)) # UVarOf m
typR <- forall (m :: * -> *) (h :: AHyperType -> *) (t :: AHyperType).
InferChild m h t -> m (InferredChild (UVarOf m) h t)
inferChild 'AHyperType (InferChild m h) :# typ
typ forall a b. a -> (a -> b) -> b
& m (InferredChild (UVarOf m) h ('AHyperType typ))
-> m (InferredChild (UVarOf m) h ('AHyperType typ))
withForalls
forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
(UVarOf m # t) -> m (GTerm (UVarOf m) # t)
generalize (InferOf (GetHyperType ('AHyperType typ)) # UVarOf m
typR forall s a. s -> Getting a s a -> a
^. forall (t :: AHyperType -> *) (v :: AHyperType -> *).
HasInferredValue t =>
Lens' (InferOf t # v) (v # t)
inferredValue)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (forall (varTypes :: AHyperType -> *) (typ :: AHyperType -> *)
(h :: AHyperType).
(varTypes # QVars) -> (h :# typ) -> Scheme varTypes typ h
Scheme varTypes # QVars
vars h ('AHyperType typ)
typI,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: (AHyperType -> *) -> AHyperType -> *)
(x :: AHyperType -> *) (h :: AHyperType).
(f (GetHyperType h) # x) -> HFlip f x h
MkHFlip
inferType ::
( InferOf t ~ ANode t
, HNodesConstraint t HasInferredValue
, MonadInstantiate m t
) =>
t # InferChild m h ->
m (t # h, InferOf t # UVarOf m)
inferType :: forall (t :: AHyperType -> *) (m :: * -> *) (h :: AHyperType -> *).
(InferOf t ~ ANode t, HNodesConstraint t HasInferredValue,
MonadInstantiate m t) =>
(t # InferChild m h) -> m (t # h, InferOf t # UVarOf m)
inferType t # InferChild m h
x =
case t # InferChild m h
x forall s a. s -> Getting (First a) s a -> Maybe a
^? forall (t :: AHyperType -> *) (f :: AHyperType).
HasQuantifiedVar t =>
Prism' (t f) (QVar t)
quantifiedVar of
Just QVar t
q -> forall (m :: * -> *) (t :: AHyperType -> *).
MonadInstantiate m t =>
QVar t -> m (UVarOf m # t)
lookupQVar QVar t
q forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (forall (t :: AHyperType -> *) (f :: AHyperType).
HasQuantifiedVar t =>
Prism' (t f) (QVar t)
quantifiedVar forall t b. AReview t b -> b -> t
# QVar t
q,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: AHyperType -> *) (h :: AHyperType).
(h :# c) -> ANode c h
MkANode
Maybe (QVar t)
Nothing ->
do
t # InferredChild (UVarOf m) h
xI <- 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 a b. a -> b -> a
const forall (m :: * -> *) (h :: AHyperType -> *) (t :: AHyperType).
InferChild m h t -> m (InferredChild (UVarOf m) h t)
inferChild) t # InferChild m h
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 @HasInferredValue forall (h :: AHyperType -> *)
(c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> (forall s a. s -> Getting a s a -> a
^. forall (v1 :: AHyperType -> *) (h :: AHyperType -> *)
(t :: AHyperType) (v2 :: AHyperType -> *).
Lens
(InferredChild v1 h t)
(InferredChild v2 h t)
(InferOf (GetHyperType t) # v1)
(InferOf (GetHyperType t) # v2)
inType forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: AHyperType -> *) (v :: AHyperType -> *).
HasInferredValue t =>
Lens' (InferOf t # v) (v # t)
inferredValue)) t # InferredChild (UVarOf m) h
xI
forall a b. a -> (a -> b) -> b
& forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
(t # UVarOf m) -> m (UVarOf m # t)
newTerm
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (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 a b. a -> b -> a
const (forall s a. s -> Getting a s a -> a
^. forall (v :: AHyperType -> *) (h1 :: AHyperType -> *)
(t :: AHyperType) (h2 :: AHyperType -> *).
Lens (InferredChild v h1 t) (InferredChild v h2 t) (h1 t) (h2 t)
inRep)) t # InferredChild (UVarOf m) h
xI,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: AHyperType -> *) (h :: AHyperType).
(h :# c) -> ANode c h
MkANode
{-# INLINE makeQVarInstances #-}
makeQVarInstances ::
Unify m typ =>
QVars # typ ->
m (QVarInstances (UVarOf m) # typ)
makeQVarInstances :: forall (m :: * -> *) (typ :: AHyperType -> *).
Unify m typ =>
(QVars # typ) -> m (QVarInstances (UVarOf m) # typ)
makeQVarInstances (QVars Map
(QVar (GetHyperType ('AHyperType typ)))
(TypeConstraintsOf (GetHyperType ('AHyperType typ)))
foralls) =
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (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
. forall (v :: AHyperType -> *) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
USkolem) Map
(QVar (GetHyperType ('AHyperType typ)))
(TypeConstraintsOf (GetHyperType ('AHyperType typ)))
foralls forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> forall (h :: AHyperType -> *) (typ :: AHyperType).
Map (QVar (GetHyperType typ)) (h typ) -> QVarInstances h typ
QVarInstances
{-# INLINE loadBody #-}
loadBody ::
( UnifyGen m typ
, HNodeLens varTypes typ
, Ord (QVar typ)
) =>
varTypes # QVarInstances (UVarOf m) ->
typ # GTerm (UVarOf m) ->
m (GTerm (UVarOf m) # typ)
loadBody :: forall (m :: * -> *) (typ :: AHyperType -> *)
(varTypes :: AHyperType -> *).
(UnifyGen m typ, HNodeLens varTypes typ, Ord (QVar typ)) =>
(varTypes # QVarInstances (UVarOf m))
-> (typ # GTerm (UVarOf m)) -> m (GTerm (UVarOf m) # typ)
loadBody varTypes # QVarInstances (UVarOf m)
foralls typ # GTerm (UVarOf m)
x =
case typ # GTerm (UVarOf m)
x forall s a. s -> Getting (First a) s a -> Maybe a
^? forall (t :: AHyperType -> *) (f :: AHyperType).
HasQuantifiedVar t =>
Prism' (t f) (QVar t)
quantifiedVar forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= QVar typ -> Maybe (UVarOf m ('AHyperType typ))
getForAll of
Just UVarOf m ('AHyperType typ)
r -> forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GPoly UVarOf m ('AHyperType typ)
r forall a b. a -> (a -> b) -> b
& forall (f :: * -> *) a. Applicative f => a -> f a
pure
Maybe (UVarOf m ('AHyperType typ))
Nothing ->
case 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 a b. a -> b -> a
const (forall s a. s -> Getting (First a) s a -> Maybe a
^? forall (v :: AHyperType -> *) (ast :: AHyperType).
Prism' (GTerm v ast) (v ast)
_GMono)) typ # GTerm (UVarOf m)
x of
Just typ # UVarOf m
xm -> forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
(t # UVarOf m) -> m (UVarOf m # t)
newTerm typ # UVarOf m
xm forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GMono
Maybe (typ # UVarOf m)
Nothing -> forall (v :: AHyperType -> *) (ast :: AHyperType).
(ast :# GTerm v) -> GTerm v ast
GBody typ # GTerm (UVarOf m)
x forall a b. a -> (a -> b) -> b
& forall (f :: * -> *) a. Applicative f => a -> f a
pure
where
getForAll :: QVar typ -> Maybe (UVarOf m ('AHyperType typ))
getForAll QVar typ
v = varTypes # QVarInstances (UVarOf m)
foralls forall s a. s -> Getting (First a) s a -> Maybe a
^? forall (s :: AHyperType -> *) (a :: AHyperType -> *)
(h :: AHyperType -> *).
HNodeLens s a =>
Lens' (s # h) (h # a)
hNodeLens forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h :: AHyperType -> *) (typ :: AHyperType)
(h :: AHyperType -> *) (typ :: AHyperType).
Iso
(QVarInstances h typ)
(QVarInstances h typ)
(Map (QVar (GetHyperType typ)) (h typ))
(Map (QVar (GetHyperType typ)) (h typ))
_QVarInstances forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. Ixed m => Index m -> Traversal' m (IxValue m)
Lens.ix QVar typ
v
class
(UnifyGen m t, HNodeLens varTypes t, Ord (QVar t)) =>
HasScheme varTypes m t
where
hasSchemeRecursive :: Proxy varTypes -> Proxy m -> RecMethod (HasScheme varTypes m) t
{-# INLINE hasSchemeRecursive #-}
default hasSchemeRecursive ::
HNodesConstraint t (HasScheme varTypes m) =>
Proxy varTypes ->
Proxy m ->
RecMethod (HasScheme varTypes m) t
hasSchemeRecursive Proxy varTypes
_ Proxy m
_ Proxy t
_ = forall (a :: Constraint). a => Dict a
Dict
instance Recursive (HasScheme varTypes m) where
recurse :: forall (h :: AHyperType -> *) (proxy :: Constraint -> *).
(HNodes h, HasScheme varTypes m h) =>
proxy (HasScheme varTypes m h)
-> Dict (HNodesConstraint h (HasScheme varTypes m))
recurse = forall (varTypes :: AHyperType -> *) (m :: * -> *)
(t :: AHyperType -> *).
HasScheme varTypes m t =>
Proxy varTypes -> Proxy m -> RecMethod (HasScheme varTypes m) t
hasSchemeRecursive (forall {k} (t :: k). Proxy t
Proxy @varTypes) (forall {k} (t :: k). Proxy t
Proxy @m) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (proxy :: Constraint -> *)
(f :: (AHyperType -> *) -> Constraint) (h :: AHyperType -> *).
proxy (f h) -> Proxy h
proxyArgument
{-# INLINE loadScheme #-}
loadScheme ::
forall m varTypes typ.
( HTraversable varTypes
, HNodesConstraint varTypes (UnifyGen m)
, HasScheme varTypes m typ
) =>
Pure # Scheme varTypes typ ->
m (GTerm (UVarOf m) # typ)
loadScheme :: forall (m :: * -> *) (varTypes :: AHyperType -> *)
(typ :: AHyperType -> *).
(HTraversable varTypes, HNodesConstraint varTypes (UnifyGen m),
HasScheme varTypes m typ) =>
(Pure # Scheme varTypes typ) -> m (GTerm (UVarOf m) # typ)
loadScheme (Pure (Scheme varTypes # QVars
vars 'AHyperType Pure :# typ
typ)) =
do
varTypes # QVarInstances (UVarOf m)
foralls <- 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 :: * -> *) (typ :: AHyperType -> *).
Unify m typ =>
(QVars # typ) -> m (QVarInstances (UVarOf m) # typ)
makeQVarInstances) varTypes # QVars
vars
forall (m :: * -> *) (h :: AHyperType -> *) (w :: AHyperType -> *).
(Monad m, RTraversable h) =>
(forall (n :: AHyperType -> *).
HRecWitness h n -> (n # w) -> m (w # n))
-> (Pure # h) -> m (w # h)
wrapM (forall {k} (t :: k). Proxy t
Proxy @(HasScheme varTypes m) forall (c :: (AHyperType -> *) -> Constraint)
(h :: AHyperType -> *) (n :: AHyperType -> *) r.
(Recursive c, c h, RNodes h) =>
Proxy c -> (c n => r) -> HRecWitness h n -> r
#>> forall (m :: * -> *) (typ :: AHyperType -> *)
(varTypes :: AHyperType -> *).
(UnifyGen m typ, HNodeLens varTypes typ, Ord (QVar typ)) =>
(varTypes # QVarInstances (UVarOf m))
-> (typ # GTerm (UVarOf m)) -> m (GTerm (UVarOf m) # typ)
loadBody varTypes # QVarInstances (UVarOf m)
foralls) 'AHyperType Pure :# typ
typ
saveH ::
forall typ varTypes m.
HasScheme varTypes m typ =>
GTerm (UVarOf m) # typ ->
StateT (varTypes # QVars, [m ()]) m (Pure # typ)
saveH :: forall (typ :: AHyperType -> *) (varTypes :: AHyperType -> *)
(m :: * -> *).
HasScheme varTypes m typ =>
(GTerm (UVarOf m) # typ)
-> StateT (varTypes # QVars, [m ()]) m (Pure # typ)
saveH (GBody 'AHyperType typ :# 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 @(HasScheme varTypes 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 (typ :: AHyperType -> *) (varTypes :: AHyperType -> *)
(m :: * -> *).
HasScheme varTypes m typ =>
(GTerm (UVarOf m) # typ)
-> StateT (varTypes # QVars, [m ()]) m (Pure # typ)
saveH) 'AHyperType typ :# GTerm (UVarOf m)
x
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (forall (h :: AHyperType -> *) (j :: AHyperType -> *).
Iso (Pure # h) (Pure # j) (h # Pure) (j # Pure)
_Pure forall t b. AReview t b -> b -> t
#)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (varTypes :: AHyperType -> *) (m :: * -> *)
(t :: AHyperType -> *).
HasScheme varTypes m t =>
Proxy varTypes -> Proxy m -> RecMethod (HasScheme varTypes m) t
hasSchemeRecursive (forall {k} (t :: k). Proxy t
Proxy @varTypes) (forall {k} (t :: k). Proxy t
Proxy @m) (forall {k} (t :: k). Proxy t
Proxy @typ)
saveH (GMono UVarOf m ('AHyperType typ)
x) =
forall (m :: * -> *) (h :: AHyperType -> *) (w :: AHyperType -> *).
(Monad m, RTraversable h) =>
(forall (n :: AHyperType -> *).
HRecWitness h n -> (w # n) -> m (n # w))
-> (w # h) -> m (Pure # h)
unwrapM (forall {k} (t :: k). Proxy t
Proxy @(HasScheme varTypes m) forall (c :: (AHyperType -> *) -> Constraint)
(h :: AHyperType -> *) (n :: AHyperType -> *) r.
(Recursive c, c h, RNodes h) =>
Proxy c -> (c n => r) -> HRecWitness h n -> r
#>> forall {f :: * -> *} {t :: AHyperType -> *}.
Unify f t =>
(UVarOf f # t) -> f (t # UVarOf f)
f) UVarOf m ('AHyperType typ)
x forall a b. a -> (a -> b) -> b
& forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
where
f :: (UVarOf f # t) -> f (t # UVarOf f)
f UVarOf f # t
v =
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
(UVarOf m # t) -> m (UVarOf m # t, UTerm (UVarOf m) # t)
semiPruneLookup UVarOf f # t
v
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
(UVarOf f # t
_, UTerm UTermBody (UVarOf f) ('AHyperType t)
t) -> UTermBody (UVarOf f) ('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
(UVarOf f # t
_, UUnbound{}) -> forall a. HasCallStack => String -> a
error String
"saveScheme of non-toplevel scheme!"
(UVarOf f # t, UTerm (UVarOf f) ('AHyperType t))
_ -> forall a. HasCallStack => String -> a
error String
"unexpected state at saveScheme of monomorphic part"
saveH (GPoly UVarOf m ('AHyperType typ)
x) =
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 ('AHyperType typ)
x
forall a b. a -> (a -> b) -> b
& forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
USkolem TypeConstraintsOf (GetHyperType ('AHyperType typ))
l ->
do
QVar typ
r <-
forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
Proxy t -> m (TypeConstraintsOf t)
scopeConstraints (forall {k} (t :: k). Proxy t
Proxy @typ)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (forall a. Semigroup a => a -> a -> a
<> TypeConstraintsOf (GetHyperType ('AHyperType typ))
l)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall typeConstraints q (m :: * -> *).
MonadQuantify typeConstraints q m =>
typeConstraints -> m q
newQuantifiedVariable
forall a b. a -> (a -> b) -> b
& forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
forall s t a b. Field1 s t a b => Lens s t a b
Lens._1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: AHyperType -> *) (a :: AHyperType -> *)
(h :: AHyperType -> *).
HNodeLens s a =>
Lens' (s # h) (h # a)
hNodeLens
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= (\QVars # typ
v -> QVars # typ
v forall a b. a -> (a -> b) -> b
& forall (typ :: AHyperType) (typ :: AHyperType).
Iso
(QVars typ)
(QVars typ)
(Map
(QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ)))
(Map
(QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ)))
_QVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
Lens.at QVar typ
r forall s t a b. ASetter s t a (Maybe b) -> b -> s -> t
?~ forall c. TypeConstraints c => c -> c
generalizeConstraints TypeConstraintsOf (GetHyperType ('AHyperType typ))
l :: QVars # typ)
forall s t a b. Field2 s t a b => Lens s t a b
Lens._2 forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= (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 ('AHyperType typ)
x (forall (v :: AHyperType -> *) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
USkolem TypeConstraintsOf (GetHyperType ('AHyperType typ))
l) forall a. a -> [a] -> [a]
:)
let result :: Pure # typ
result = forall (h :: AHyperType -> *) (j :: AHyperType -> *).
Iso (Pure # h) (Pure # j) (h # Pure) (j # Pure)
_Pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: AHyperType -> *) (f :: AHyperType).
HasQuantifiedVar t =>
Prism' (t f) (QVar t)
quantifiedVar forall t b. AReview t b -> b -> t
# QVar typ
r
forall (v :: AHyperType -> *) (ast :: AHyperType).
Pure ast -> UTerm v ast
UResolved Pure # typ
result 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 ('AHyperType typ)
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 Pure # typ
result
UResolved Pure # typ
v -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Pure # typ
v
UTerm (UVarOf m) # typ
_ -> forall a. HasCallStack => String -> a
error String
"unexpected state at saveScheme's forall"
saveScheme ::
( HNodesConstraint varTypes OrdQVar
, HPointed varTypes
, HasScheme varTypes m typ
) =>
GTerm (UVarOf m) # typ ->
m (Pure # Scheme varTypes typ)
saveScheme :: forall (varTypes :: AHyperType -> *) (m :: * -> *)
(typ :: AHyperType -> *).
(HNodesConstraint varTypes OrdQVar, HPointed varTypes,
HasScheme varTypes m typ) =>
(GTerm (UVarOf m) # typ) -> m (Pure # Scheme varTypes typ)
saveScheme GTerm (UVarOf m) # typ
x =
do
(Pure # typ
t, (varTypes # QVars
v, [m ()]
recover)) <-
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT
(forall (typ :: AHyperType -> *) (varTypes :: AHyperType -> *)
(m :: * -> *).
HasScheme varTypes m typ =>
(GTerm (UVarOf m) # typ)
-> StateT (varTypes # QVars, [m ()]) m (Pure # typ)
saveH GTerm (UVarOf m) # typ
x)
( forall (h :: AHyperType -> *) (p :: AHyperType -> *).
HPointed h =>
(forall (n :: AHyperType -> *). HWitness h n -> p # n) -> h # p
hpure (forall {k} (t :: k). Proxy t
Proxy @OrdQVar forall (h :: AHyperType -> *)
(c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> forall (typ :: AHyperType).
Map
(QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ))
-> QVars typ
QVars forall a. Monoid a => a
mempty)
, []
)
forall (h :: AHyperType -> *) (j :: AHyperType -> *).
Iso (Pure # h) (Pure # j) (h # Pure) (j # Pure)
_Pure forall t b. AReview t b -> b -> t
# forall (varTypes :: AHyperType -> *) (typ :: AHyperType -> *)
(h :: AHyperType).
(varTypes # QVars) -> (h :# typ) -> Scheme varTypes typ h
Scheme varTypes # QVars
v Pure # typ
t forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [m ()]
recover