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