Let.hs

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

module Hyper.Syntax.Let
    ( Let (..)
    , letVar
    , letEquals
    , letIn
    , W_Let (..)
    , MorphWitness (..)
    ) where

import Generics.Constraints (Constraints)
import Hyper
import Hyper.Class.Unify (UVarOf, UnifyGen)
import Hyper.Infer
import Hyper.Unify.Generalize (GTerm, generalize)
import Text.PrettyPrint (($+$), (<+>))
import qualified Text.PrettyPrint as Pretty
import Text.PrettyPrint.HughesPJClass (Pretty (..), maybeParens)

import Hyper.Internal.Prelude

-- | A term for let-expressions with let-generalization.
--
-- @Let v expr@s express let-expressions with @v@s as variable names and @expr@s for terms.
--
-- Apart from the data type, an 'Infer' instance is also provided.
data Let v expr h = Let
    { _letVar :: v
    , _letEquals :: h :# expr
    , _letIn :: h :# expr
    }
    deriving (Generic)

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

instance
    Constraints (Let v expr h) Pretty =>
    Pretty (Let v expr h)
    where
    pPrintPrec lvl p (Let v e i) =
        Pretty.text "let"
            <+> pPrintPrec lvl 0 v
            <+> Pretty.text "="
            <+> pPrintPrec lvl 0 e
            $+$ pPrintPrec lvl 0 i
            & maybeParens (p > 0)

type instance InferOf (Let _ e) = InferOf e

instance
    ( MonadScopeLevel m
    , LocalScopeType v (GTerm (UVarOf m) # TypeOf expr) m
    , UnifyGen m (TypeOf expr)
    , HasInferredType expr
    , HNodesConstraint (InferOf expr) (UnifyGen m)
    , HTraversable (InferOf expr)
    , Infer m expr
    ) =>
    Infer m (Let v expr)
    where
    inferBody (Let v e i) =
        do
            (eI, eG) <-
                do
                    InferredChild eI eR <- inferChild e
                    generalize (eR ^# inferredType (Proxy @expr))
                        <&> (eI,)
                    & localLevel
            inferChild i
                & localScopeType v eG
                <&> \(InferredChild iI iR) -> (Let v eI iI, iR)