{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE UndecidableInstances #-} module Hyper.Syntax.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.Syntax.FuncType (FuncType (..)) import Hyper.Unify (UVarOf, UnifyGen) 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 { forall var (typ :: HyperType) (expr :: HyperType) (h :: AHyperType). TypedLam var typ expr h -> var _tlIn :: var , forall var (typ :: HyperType) (expr :: HyperType) (h :: AHyperType). TypedLam var typ expr h -> h :# typ _tlInType :: h :# typ , forall var (typ :: HyperType) (expr :: HyperType) (h :: AHyperType). TypedLam var typ expr h -> h :# expr _tlOut :: h :# expr } deriving (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 GetHyperType h ('AHyperType typ) t GetHyperType h ('AHyperType expr) o) = ( String -> Doc P.text String "λ" forall a. Semigroup a => a -> a -> a <> forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc pPrintPrec PrettyLevel lvl Rational 0 var i forall a. Semigroup a => a -> a -> a <> String -> Doc P.text String ":" forall a. Semigroup a => a -> a -> a <> forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc pPrintPrec PrettyLevel lvl Rational 0 GetHyperType h ('AHyperType typ) t ) Doc -> Doc -> Doc P.<+> String -> Doc P.text String "→" Doc -> Doc -> Doc P.<+> forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc pPrintPrec PrettyLevel lvl Rational 0 GetHyperType h ('AHyperType expr) o forall a b. a -> (a -> b) -> b & Bool -> Doc -> Doc maybeParens (Rational p 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 :: forall (h :: HyperType). (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 <- forall (m :: * -> *) (h :: HyperType) (t :: AHyperType). InferChild m h t -> m (InferredChild (UVarOf m) h t) inferChild 'AHyperType (InferChild m h) :# t t let tT :: UVarOf m # TypeOf e tT = InferOf (GetHyperType ('AHyperType t)) # UVarOf m tR forall s a. s -> Getting a s a -> a ^. 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 <- forall (m :: * -> *) (h :: HyperType) (t :: AHyperType). InferChild m h t -> m (InferredChild (UVarOf m) h t) inferChild 'AHyperType (InferChild m h) :# e r forall a b. a -> (a -> b) -> b & forall var scheme (m :: * -> *) a. LocalScopeType var scheme m => var -> scheme -> m a -> m a localScopeType v p UVarOf m # TypeOf e tT 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 forall t b. AReview t b -> b -> t # forall (typ :: HyperType) (h :: AHyperType). (h :# typ) -> (h :# typ) -> FuncType typ h FuncType UVarOf m # TypeOf e tT (InferOf (GetHyperType ('AHyperType e)) # UVarOf m rR forall s t a b. s -> ALens s t a b -> a ^# forall (t :: HyperType) (v :: HyperType). HasInferredType t => Proxy t -> ALens' (InferOf t # v) (v # TypeOf t) inferredType (forall {k} (t :: k). Proxy t Proxy @e)) forall a b. a -> (a -> b) -> b & forall (m :: * -> *) (t :: HyperType). UnifyGen m t => (t # UVarOf m) -> m (UVarOf m # t) newTerm forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b <&> (forall var (typ :: HyperType) (expr :: HyperType) (h :: AHyperType). var -> (h :# typ) -> (h :# expr) -> TypedLam var typ expr h TypedLam v p h ('AHyperType t) tI h ('AHyperType e) rI,) forall b c a. (b -> c) -> (a -> b) -> a -> c . forall (c :: HyperType) (h :: AHyperType). (h :# c) -> ANode c h MkANode