Lam.hs

{-# 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
    { _lamIn :: v
    , _lamOut :: h :# expr
    }
    deriving (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 lvl p (Lam i o) =
        (P.text "λ" <> pPrintPrec lvl 0 i)
            P.<+> P.text "→"
            P.<+> pPrintPrec lvl 0 o
            & maybeParens (p > 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 p r) =
        do
            varType <- newUnbound
            InferredChild rI rR <- inferChild r & localScopeType p varType
            hSubset # FuncType varType (rR ^# inferredType (Proxy @t))
                & newTerm
                <&> (Lam p rI,) . MkANode