{-# LANGUAGE TemplateHaskell, UndecidableInstances, FlexibleInstances #-} module Hyper.Type.AST.TypedLam ( TypedLam(..), tlIn, tlInType, tlOut, W_TypedLam(..), MorphWitness(..) ) where import Generics.Constraints (Constraints) import Hyper import Hyper.Class.Optic (HNodeLens(..), HSubset(..), HSubset') import Hyper.Infer import Hyper.Type.AST.FuncType (FuncType(..)) import Hyper.Unify (UnifyGen, UVarOf) import Hyper.Unify.New (newTerm) import qualified Text.PrettyPrint as P import Text.PrettyPrint.HughesPJClass (Pretty(..), maybeParens) import Hyper.Internal.Prelude data TypedLam var typ expr h = TypedLam { TypedLam var typ expr h -> var _tlIn :: var , TypedLam var typ expr h -> h :# typ _tlInType :: h :# typ , TypedLam var typ expr h -> h :# expr _tlOut :: h :# expr } deriving (forall x. TypedLam var typ expr h -> Rep (TypedLam var typ expr h) x) -> (forall x. Rep (TypedLam var typ expr h) x -> TypedLam var typ expr h) -> Generic (TypedLam var typ expr h) forall x. Rep (TypedLam var typ expr h) x -> TypedLam var typ expr h forall x. TypedLam var typ expr h -> Rep (TypedLam var typ expr h) x forall a. (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a forall var (typ :: HyperType) (expr :: HyperType) (h :: AHyperType) x. Rep (TypedLam var typ expr h) x -> TypedLam var typ expr h forall var (typ :: HyperType) (expr :: HyperType) (h :: AHyperType) x. TypedLam var typ expr h -> Rep (TypedLam var typ expr h) x $cto :: forall var (typ :: HyperType) (expr :: HyperType) (h :: AHyperType) x. Rep (TypedLam var typ expr h) x -> TypedLam var typ expr h $cfrom :: forall var (typ :: HyperType) (expr :: HyperType) (h :: AHyperType) x. TypedLam var typ expr h -> Rep (TypedLam var typ expr h) x Generic makeLenses ''TypedLam makeCommonInstances [''TypedLam] makeHTraversableApplyAndBases ''TypedLam makeZipMatch ''TypedLam makeHContext ''TypedLam makeHMorph ''TypedLam instance (RNodes t, RNodes e) => RNodes (TypedLam v t e) instance (c (TypedLam v t e), Recursively c t, Recursively c e) => Recursively c (TypedLam v t e) instance (RTraversable t, RTraversable e) => RTraversable (TypedLam v t e) instance Constraints (TypedLam var typ expr h) Pretty => Pretty (TypedLam var typ expr h) where pPrintPrec :: PrettyLevel -> Rational -> TypedLam var typ expr h -> Doc pPrintPrec PrettyLevel lvl Rational p (TypedLam var i h :# typ t h :# expr o) = ( String -> Doc P.text String "λ" Doc -> Doc -> Doc forall a. Semigroup a => a -> a -> a <> PrettyLevel -> Rational -> var -> Doc forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc pPrintPrec PrettyLevel lvl Rational 0 var i Doc -> Doc -> Doc forall a. Semigroup a => a -> a -> a <> String -> Doc P.text String ":" Doc -> Doc -> Doc forall a. Semigroup a => a -> a -> a <> PrettyLevel -> Rational -> (h :# typ) -> Doc forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc pPrintPrec PrettyLevel lvl Rational 0 h :# typ t ) Doc -> Doc -> Doc P.<+> String -> Doc P.text String "→" Doc -> Doc -> Doc P.<+> PrettyLevel -> Rational -> (h :# expr) -> Doc forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc pPrintPrec PrettyLevel lvl Rational 0 h :# expr o 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 0) type instance InferOf (TypedLam _ _ e) = ANode (TypeOf e) instance ( Infer m t , Infer m e , HasInferredType e , UnifyGen m (TypeOf e) , HSubset' (TypeOf e) (FuncType (TypeOf e)) , HNodeLens (InferOf t) (TypeOf e) , LocalScopeType v (UVarOf m # TypeOf e) m ) => Infer m (TypedLam v t e) where {-# INLINE inferBody #-} inferBody :: (TypedLam v t e # InferChild m h) -> m (TypedLam v t e # h, InferOf (TypedLam v t e) # UVarOf m) inferBody (TypedLam v p 'AHyperType (InferChild m h) :# t t 'AHyperType (InferChild m h) :# e r) = do InferredChild h ('AHyperType t) tI InferOf (GetHyperType ('AHyperType t)) # UVarOf m tR <- InferChild m h ('AHyperType t) -> m (InferredChild (UVarOf m) h ('AHyperType t)) forall (m :: * -> *) (h :: HyperType) (t :: AHyperType). InferChild m h t -> m (InferredChild (UVarOf m) h t) inferChild 'AHyperType (InferChild m h) :# t InferChild m h ('AHyperType t) t let tT :: UVarOf m # TypeOf e tT = InferOf t ('AHyperType (UVarOf m)) InferOf (GetHyperType ('AHyperType t)) # UVarOf m tR InferOf t ('AHyperType (UVarOf m)) -> Getting (UVarOf m # TypeOf e) (InferOf t ('AHyperType (UVarOf m))) (UVarOf m # TypeOf e) -> UVarOf m # TypeOf e forall s a. s -> Getting a s a -> a ^. Getting (UVarOf m # TypeOf e) (InferOf t ('AHyperType (UVarOf m))) (UVarOf m # TypeOf e) forall (s :: HyperType) (a :: HyperType) (h :: HyperType). HNodeLens s a => Lens' (s # h) (h # a) hNodeLens InferredChild h ('AHyperType e) rI InferOf (GetHyperType ('AHyperType e)) # UVarOf m rR <- InferChild m h ('AHyperType e) -> m (InferredChild (UVarOf m) h ('AHyperType e)) forall (m :: * -> *) (h :: HyperType) (t :: AHyperType). InferChild m h t -> m (InferredChild (UVarOf m) h t) inferChild 'AHyperType (InferChild m h) :# e InferChild m h ('AHyperType e) r m (InferredChild (UVarOf m) h ('AHyperType e)) -> (m (InferredChild (UVarOf m) h ('AHyperType e)) -> m (InferredChild (UVarOf m) h ('AHyperType e))) -> m (InferredChild (UVarOf m) h ('AHyperType e)) forall a b. a -> (a -> b) -> b & v -> (UVarOf m # TypeOf e) -> m (InferredChild (UVarOf m) h ('AHyperType e)) -> m (InferredChild (UVarOf m) h ('AHyperType e)) forall var scheme (m :: * -> *) a. LocalScopeType var scheme m => var -> scheme -> m a -> m a localScopeType v p UVarOf m # TypeOf e tT Tagged (FuncType (TypeOf e) # UVarOf m) (Identity (FuncType (TypeOf e) # UVarOf m)) -> Tagged (TypeOf e # UVarOf m) (Identity (TypeOf e # UVarOf m)) forall (s :: HyperType) (t :: HyperType) (a :: HyperType) (b :: HyperType) (h :: HyperType). HSubset s t a b => Prism (s # h) (t # h) (a # h) (b # h) hSubset (Tagged (FuncType (TypeOf e) # UVarOf m) (Identity (FuncType (TypeOf e) # UVarOf m)) -> Tagged (TypeOf e # UVarOf m) (Identity (TypeOf e # UVarOf m))) -> (FuncType (TypeOf e) # UVarOf m) -> TypeOf e # UVarOf m forall t b. AReview t b -> b -> t # ('AHyperType (UVarOf m) :# TypeOf e) -> ('AHyperType (UVarOf m) :# TypeOf e) -> FuncType (TypeOf e) # UVarOf m forall (typ :: HyperType) (h :: AHyperType). (h :# typ) -> (h :# typ) -> FuncType typ h FuncType 'AHyperType (UVarOf m) :# TypeOf e UVarOf m # TypeOf e tT (InferOf e ('AHyperType (UVarOf m)) InferOf (GetHyperType ('AHyperType e)) # UVarOf m rR InferOf e ('AHyperType (UVarOf m)) -> ALens (InferOf e ('AHyperType (UVarOf m))) (InferOf e ('AHyperType (UVarOf m))) (UVarOf m # TypeOf e) (UVarOf m # TypeOf e) -> UVarOf m # TypeOf e forall s t a b. s -> ALens s t a b -> a ^# Proxy e -> ALens (InferOf e ('AHyperType (UVarOf m))) (InferOf e ('AHyperType (UVarOf m))) (UVarOf m # TypeOf e) (UVarOf m # TypeOf e) forall (t :: HyperType) (v :: HyperType). HasInferredType t => Proxy t -> ALens' (InferOf t # v) (v # TypeOf t) inferredType (Proxy e forall k (t :: k). Proxy t Proxy @e)) (TypeOf e # UVarOf m) -> ((TypeOf e # UVarOf m) -> m (UVarOf m # TypeOf e)) -> m (UVarOf m # TypeOf e) forall a b. a -> (a -> b) -> b & (TypeOf e # UVarOf m) -> m (UVarOf m # TypeOf e) forall (m :: * -> *) (t :: HyperType). UnifyGen m t => (t # UVarOf m) -> m (UVarOf m # t) newTerm m (UVarOf m # TypeOf e) -> ((UVarOf m # TypeOf e) -> ANode (TypeOf e) ('AHyperType (UVarOf m))) -> m (ANode (TypeOf e) ('AHyperType (UVarOf m))) forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b <&> (UVarOf m # TypeOf e) -> ANode (TypeOf e) ('AHyperType (UVarOf m)) forall (c :: HyperType) (h :: AHyperType). (h :# c) -> ANode c h MkANode m (ANode (TypeOf e) ('AHyperType (UVarOf m))) -> (ANode (TypeOf e) ('AHyperType (UVarOf m)) -> (TypedLam v t e # h, ANode (TypeOf e) ('AHyperType (UVarOf m)))) -> m (TypedLam v t e # h, ANode (TypeOf e) ('AHyperType (UVarOf m))) forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b <&> (v -> ('AHyperType h :# t) -> ('AHyperType h :# e) -> TypedLam v t e # h forall var (typ :: HyperType) (expr :: HyperType) (h :: AHyperType). var -> (h :# typ) -> (h :# expr) -> TypedLam var typ expr h TypedLam v p h ('AHyperType t) 'AHyperType h :# t tI h ('AHyperType e) 'AHyperType h :# e rI,)