{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}

module Hyper.Syntax.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.Syntax.FuncType
import Hyper.Unify (UVarOf, UnifyGen)
import Hyper.Unify.New (newTerm, newUnbound)
import qualified Text.PrettyPrint as P
import Text.PrettyPrint.HughesPJClass (Pretty (..), maybeParens)

import Hyper.Internal.Prelude

-- | A term for lambda abstractions.
--
-- @Lam v expr@s express lambda abstractions with @v@s as variable names and @expr@s for bodies.
--
-- Apart from the data type, an 'Infer' instance is also provided.
data Lam v expr h = Lam
    { forall v (expr :: HyperType) (h :: AHyperType). Lam v expr h -> v
_lamIn :: v
    , forall v (expr :: HyperType) (h :: AHyperType).
Lam v expr h -> h :# expr
_lamOut :: h :# expr
    }
    deriving (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 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 v
i)
            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 (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 :: forall (h :: HyperType).
(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 <- forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
m (UVarOf m # t)
newUnbound
            InferredChild h ('AHyperType t)
rI InferOf (GetHyperType ('AHyperType t)) # UVarOf m
rR <- forall (m :: * -> *) (h :: HyperType) (t :: AHyperType).
InferChild m h t -> m (InferredChild (UVarOf m) h t)
inferChild 'AHyperType (InferChild m h) :# t
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 t
varType
            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 t
varType (InferOf (GetHyperType ('AHyperType t)) # 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 @t))
                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 v (expr :: HyperType) (h :: AHyperType).
v -> (h :# expr) -> Lam v expr h
Lam v
p h ('AHyperType t)
rI,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: HyperType) (h :: AHyperType). (h :# c) -> ANode c h
MkANode