App.hs

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

module Hyper.Syntax.App
    ( App (..)
    , appFunc
    , appArg
    , W_App (..)
    , MorphWitness (..)
    ) where

import Hyper
import Hyper.Class.Optic (HSubset (..), HSubset')
import Hyper.Infer
import Hyper.Syntax.FuncType
import Hyper.Unify (UnifyGen, unify)
import Hyper.Unify.New (newTerm, newUnbound)
import Text.PrettyPrint ((<+>))
import Text.PrettyPrint.HughesPJClass (Pretty (..), maybeParens)

import Hyper.Internal.Prelude

-- | A term for function applications.
--
-- @App expr@s express function applications of @expr@s.
--
-- Apart from the data type, an 'Infer' instance is also provided.
data App expr h = App
    { _appFunc :: h :# expr
    , _appArg :: h :# expr
    }
    deriving (Generic)

makeLenses ''App
makeZipMatch ''App
makeHContext ''App
makeHMorph ''App
makeHTraversableApplyAndBases ''App
makeCommonInstances [''App]

instance RNodes e => RNodes (App e)
instance (c (App e), Recursively c e) => Recursively c (App e)
instance RTraversable e => RTraversable (App e)

instance Pretty (h :# expr) => Pretty (App expr h) where
    pPrintPrec lvl p (App f x) =
        pPrintPrec lvl 10 f
            <+> pPrintPrec lvl 11 x
            & maybeParens (p > 10)

type instance InferOf (App e) = ANode (TypeOf e)

instance
    ( Infer m expr
    , HasInferredType expr
    , HSubset' (TypeOf expr) (FuncType (TypeOf expr))
    , UnifyGen m (TypeOf expr)
    ) =>
    Infer m (App expr)
    where
    {-# INLINE inferBody #-}
    inferBody (App func arg) =
        do
            InferredChild argI argR <- inferChild arg
            InferredChild funcI funcR <- inferChild func
            funcRes <- newUnbound
            (App funcI argI, MkANode funcRes)
                <$ (newTerm (hSubset # FuncType (argR ^# l) funcRes) >>= unify (funcR ^# l))
        where
            l = inferredType (Proxy @expr)