ScopeLevel.hs

{-# LANGUAGE TemplateHaskell #-}

module Hyper.Infer.ScopeLevel
    ( ScopeLevel (..)
    , _ScopeLevel
    , MonadScopeLevel (..)
    ) where

import Algebra.PartialOrd (PartialOrd (..))
import Hyper.Unify.Constraints (TypeConstraints (..))
import qualified Text.PrettyPrint as Pretty
import Text.PrettyPrint.HughesPJClass (Pretty (..))

import Hyper.Internal.Prelude

-- | A representation of scope nesting level,
-- for use in let-generalization and skolem escape detection.
--
-- See ["Efficient generalization with levels"](http://okmij.org/ftp/ML/generalization.html#levels)
-- for a detailed explanation.
--
-- Commonly used as the 'Hyper.Unify.Constraints.TypeConstraintsOf' of terms.
--
-- /Note/: The 'Ord' instance is only for use as a 'Data.Map.Map' key, not a
-- logical ordering, for which 'PartialOrd' is used.
newtype ScopeLevel = ScopeLevel Int
    deriving stock (Eq, Ord, Show, Generic)

makePrisms ''ScopeLevel

instance PartialOrd ScopeLevel where
    {-# INLINE leq #-}
    ScopeLevel x `leq` ScopeLevel y = x >= y

instance Semigroup ScopeLevel where
    {-# INLINE (<>) #-}
    ScopeLevel x <> ScopeLevel y = ScopeLevel (min x y)

instance Monoid ScopeLevel where
    {-# INLINE mempty #-}
    mempty = ScopeLevel maxBound

instance TypeConstraints ScopeLevel where
    {-# INLINE generalizeConstraints #-}
    generalizeConstraints _ = mempty
    toScopeConstraints = id

instance Pretty ScopeLevel where
    pPrint (ScopeLevel x)
        | x == maxBound = Pretty.text "*"
        | otherwise = Pretty.text "scope#" <> pPrint x

instance NFData ScopeLevel
instance Binary ScopeLevel

-- | A class of 'Monad's which maintain a scope level,
-- where the level can be locally increased for computations.
class Monad m => MonadScopeLevel m where
    localLevel :: m a -> m a