{-# 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,)