{-# LANGUAGE UndecidableInstances, TemplateHaskell, FlexibleInstances #-}
module Hyper.Type.AST.TypeSig
( TypeSig(..), tsType, tsTerm, W_TypeSig(..)
) where
import Generics.Constraints (Constraints)
import Hyper
import Hyper.Infer
import Hyper.Type.AST.Scheme
import Hyper.Unify (UnifyGen, unify)
import Hyper.Unify.Generalize (instantiateWith)
import Hyper.Unify.Term (UTerm(..))
import Text.PrettyPrint ((<+>))
import qualified Text.PrettyPrint as Pretty
import Text.PrettyPrint.HughesPJClass (Pretty(..), maybeParens)
import Hyper.Internal.Prelude
data TypeSig vars term h = TypeSig
{ TypeSig vars term h -> h :# term
_tsTerm :: h :# term
, TypeSig vars term h -> h :# Scheme vars (TypeOf term)
_tsType :: h :# Scheme vars (TypeOf term)
} deriving (forall x. TypeSig vars term h -> Rep (TypeSig vars term h) x)
-> (forall x. Rep (TypeSig vars term h) x -> TypeSig vars term h)
-> Generic (TypeSig vars term h)
forall x. Rep (TypeSig vars term h) x -> TypeSig vars term h
forall x. TypeSig vars term h -> Rep (TypeSig vars term h) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (vars :: AHyperType -> *) (term :: AHyperType -> *)
(h :: AHyperType) x.
Rep (TypeSig vars term h) x -> TypeSig vars term h
forall (vars :: AHyperType -> *) (term :: AHyperType -> *)
(h :: AHyperType) x.
TypeSig vars term h -> Rep (TypeSig vars term h) x
$cto :: forall (vars :: AHyperType -> *) (term :: AHyperType -> *)
(h :: AHyperType) x.
Rep (TypeSig vars term h) x -> TypeSig vars term h
$cfrom :: forall (vars :: AHyperType -> *) (term :: AHyperType -> *)
(h :: AHyperType) x.
TypeSig vars term h -> Rep (TypeSig vars term h) x
Generic
makeLenses ''TypeSig
makeCommonInstances [''TypeSig]
makeHTraversableApplyAndBases ''TypeSig
instance
Constraints (TypeSig vars term h) Pretty =>
Pretty (TypeSig vars term h) where
pPrintPrec :: PrettyLevel -> Rational -> TypeSig vars term h -> Doc
pPrintPrec PrettyLevel
lvl Rational
p (TypeSig h :# term
term h :# Scheme vars (TypeOf term)
typ) =
PrettyLevel -> Rational -> (h :# term) -> Doc
forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
1 h :# term
term Doc -> Doc -> Doc
<+> String -> Doc
Pretty.text String
":" Doc -> Doc -> Doc
<+> PrettyLevel -> Rational -> (h :# Scheme vars (TypeOf term)) -> Doc
forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
1 h :# Scheme vars (TypeOf term)
typ
Doc -> (Doc -> Doc) -> Doc
forall a b. a -> (a -> b) -> b
& Bool -> Doc -> Doc
maybeParens (Rational
p Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Rational
1)
type instance InferOf (TypeSig _ t) = InferOf t
instance
( MonadScopeLevel m
, HasInferredType term
, HasInferredValue (TypeOf term)
, HTraversable vars
, HTraversable (InferOf term)
, HNodesConstraint (InferOf term) (UnifyGen m)
, HNodesConstraint vars (MonadInstantiate m)
, UnifyGen m (TypeOf term)
, Infer m (TypeOf term)
, Infer m term
) =>
Infer m (TypeSig vars term) where
inferBody :: (TypeSig vars term # InferChild m h)
-> m (TypeSig vars term # h,
InferOf (TypeSig vars term) # UVarOf m)
inferBody (TypeSig 'AHyperType (InferChild m h) :# term
x 'AHyperType (InferChild m h) :# Scheme vars (TypeOf term)
s) =
do
InferredChild h ('AHyperType term)
xI InferOf (GetHyperType ('AHyperType term)) # UVarOf m
xR <- InferChild m h ('AHyperType term)
-> m (InferredChild (UVarOf m) h ('AHyperType term))
forall (m :: * -> *) (h :: AHyperType -> *) (t :: AHyperType).
InferChild m h t -> m (InferredChild (UVarOf m) h t)
inferChild 'AHyperType (InferChild m h) :# term
InferChild m h ('AHyperType term)
x
InferredChild h ('AHyperType (Scheme vars (TypeOf term)))
sI InferOf (GetHyperType ('AHyperType (Scheme vars (TypeOf term))))
# UVarOf m
sR <- InferChild m h ('AHyperType (Scheme vars (TypeOf term)))
-> m (InferredChild
(UVarOf m) h ('AHyperType (Scheme vars (TypeOf term))))
forall (m :: * -> *) (h :: AHyperType -> *) (t :: AHyperType).
InferChild m h t -> m (InferredChild (UVarOf m) h t)
inferChild 'AHyperType (InferChild m h) :# Scheme vars (TypeOf term)
InferChild m h ('AHyperType (Scheme vars (TypeOf term)))
s
(UVarOf m # TypeOf term
t, ()) <- m ()
-> (forall (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n)
-> (GTerm (UVarOf m) # TypeOf term)
-> m (UVarOf m # TypeOf term, ())
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
USkolem (HFlip GTerm (TypeOf term) ('AHyperType (UVarOf m))
InferOf (GetHyperType ('AHyperType (Scheme vars (TypeOf term))))
# UVarOf m
sR HFlip GTerm (TypeOf term) ('AHyperType (UVarOf m))
-> Getting
(GTerm (UVarOf m) # TypeOf term)
(HFlip GTerm (TypeOf term) ('AHyperType (UVarOf m)))
(GTerm (UVarOf m) # TypeOf term)
-> GTerm (UVarOf m) # TypeOf term
forall s a. s -> Getting a s a -> a
^. Getting
(GTerm (UVarOf m) # TypeOf term)
(HFlip GTerm (TypeOf term) ('AHyperType (UVarOf m)))
(GTerm (UVarOf m) # TypeOf term)
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)
InferOf term # UVarOf m
InferOf (GetHyperType ('AHyperType term)) # UVarOf m
xR (InferOf term # UVarOf m)
-> ((InferOf term # UVarOf m) -> m (InferOf term # UVarOf m))
-> m (InferOf term # UVarOf m)
forall a b. a -> (a -> b) -> b
& Proxy term
-> ((UVarOf m # TypeOf term)
-> Pretext
(->)
(UVarOf m # TypeOf term)
(UVarOf m # TypeOf term)
(UVarOf m # TypeOf term))
-> (InferOf term # UVarOf m)
-> Pretext
(->)
(UVarOf m # TypeOf term)
(UVarOf m # TypeOf term)
(InferOf term # UVarOf m)
forall (t :: AHyperType -> *) (v :: AHyperType -> *).
HasInferredType t =>
Proxy t -> ALens' (InferOf t # v) (v # TypeOf t)
inferredType (Proxy term
forall k (t :: k). Proxy t
Proxy @term) (((UVarOf m # TypeOf term)
-> Pretext
(->)
(UVarOf m # TypeOf term)
(UVarOf m # TypeOf term)
(UVarOf m # TypeOf term))
-> (InferOf term # UVarOf m)
-> Pretext
(->)
(UVarOf m # TypeOf term)
(UVarOf m # TypeOf term)
(InferOf term # UVarOf m))
-> ((UVarOf m # TypeOf term) -> m (UVarOf m # TypeOf term))
-> (InferOf term # UVarOf m)
-> m (InferOf term # UVarOf m)
forall (f :: * -> *) s t a b.
Functor f =>
ALens s t a b -> (a -> f b) -> s -> f t
#%%~ (UVarOf m # TypeOf term)
-> (UVarOf m # TypeOf term) -> m (UVarOf m # TypeOf term)
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
(UVarOf m # t) -> (UVarOf m # t) -> m (UVarOf m # t)
unify UVarOf m # TypeOf term
t
m (InferOf term # UVarOf m)
-> ((InferOf term # UVarOf m)
-> (TypeSig vars term # h, InferOf term # UVarOf m))
-> m (TypeSig vars term # h, InferOf term # UVarOf m)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (('AHyperType h :# term)
-> ('AHyperType h :# Scheme vars (TypeOf term))
-> TypeSig vars term # h
forall (vars :: AHyperType -> *) (term :: AHyperType -> *)
(h :: AHyperType).
(h :# term)
-> (h :# Scheme vars (TypeOf term)) -> TypeSig vars term h
TypeSig h ('AHyperType term)
'AHyperType h :# term
xI h ('AHyperType (Scheme vars (TypeOf term)))
'AHyperType h :# Scheme vars (TypeOf term)
sI, )
m (TypeSig vars term # h, InferOf term # UVarOf m)
-> (m (TypeSig vars term # h, InferOf term # UVarOf m)
-> m (TypeSig vars term # h, InferOf term # UVarOf m))
-> m (TypeSig vars term # h, InferOf term # UVarOf m)
forall a b. a -> (a -> b) -> b
& m (TypeSig vars term # h, InferOf term # UVarOf m)
-> m (TypeSig vars term # h, InferOf term # UVarOf m)
forall (m :: * -> *) a. MonadScopeLevel m => m a -> m a
localLevel