{-# 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 (ScopeLevel -> ScopeLevel -> Bool
(ScopeLevel -> ScopeLevel -> Bool)
-> (ScopeLevel -> ScopeLevel -> Bool) -> Eq ScopeLevel
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ScopeLevel -> ScopeLevel -> Bool
$c/= :: ScopeLevel -> ScopeLevel -> Bool
== :: ScopeLevel -> ScopeLevel -> Bool
$c== :: ScopeLevel -> ScopeLevel -> Bool
Eq, Eq ScopeLevel
Eq ScopeLevel
-> (ScopeLevel -> ScopeLevel -> Ordering)
-> (ScopeLevel -> ScopeLevel -> Bool)
-> (ScopeLevel -> ScopeLevel -> Bool)
-> (ScopeLevel -> ScopeLevel -> Bool)
-> (ScopeLevel -> ScopeLevel -> Bool)
-> (ScopeLevel -> ScopeLevel -> ScopeLevel)
-> (ScopeLevel -> ScopeLevel -> ScopeLevel)
-> Ord ScopeLevel
ScopeLevel -> ScopeLevel -> Bool
ScopeLevel -> ScopeLevel -> Ordering
ScopeLevel -> ScopeLevel -> ScopeLevel
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ScopeLevel -> ScopeLevel -> ScopeLevel
$cmin :: ScopeLevel -> ScopeLevel -> ScopeLevel
max :: ScopeLevel -> ScopeLevel -> ScopeLevel
$cmax :: ScopeLevel -> ScopeLevel -> ScopeLevel
>= :: ScopeLevel -> ScopeLevel -> Bool
$c>= :: ScopeLevel -> ScopeLevel -> Bool
> :: ScopeLevel -> ScopeLevel -> Bool
$c> :: ScopeLevel -> ScopeLevel -> Bool
<= :: ScopeLevel -> ScopeLevel -> Bool
$c<= :: ScopeLevel -> ScopeLevel -> Bool
< :: ScopeLevel -> ScopeLevel -> Bool
$c< :: ScopeLevel -> ScopeLevel -> Bool
compare :: ScopeLevel -> ScopeLevel -> Ordering
$ccompare :: ScopeLevel -> ScopeLevel -> Ordering
$cp1Ord :: Eq ScopeLevel
Ord, Int -> ScopeLevel -> ShowS
[ScopeLevel] -> ShowS
ScopeLevel -> String
(Int -> ScopeLevel -> ShowS)
-> (ScopeLevel -> String)
-> ([ScopeLevel] -> ShowS)
-> Show ScopeLevel
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ScopeLevel] -> ShowS
$cshowList :: [ScopeLevel] -> ShowS
show :: ScopeLevel -> String
$cshow :: ScopeLevel -> String
showsPrec :: Int -> ScopeLevel -> ShowS
$cshowsPrec :: Int -> ScopeLevel -> ShowS
Show, (forall x. ScopeLevel -> Rep ScopeLevel x)
-> (forall x. Rep ScopeLevel x -> ScopeLevel) -> Generic ScopeLevel
forall x. Rep ScopeLevel x -> ScopeLevel
forall x. ScopeLevel -> Rep ScopeLevel x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep ScopeLevel x -> ScopeLevel
$cfrom :: forall x. ScopeLevel -> Rep ScopeLevel x
Generic)
makePrisms ''ScopeLevel

instance PartialOrd ScopeLevel where
    {-# INLINE leq #-}
    ScopeLevel Int
x leq :: ScopeLevel -> ScopeLevel -> Bool
`leq` ScopeLevel Int
y = Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
y

instance Semigroup ScopeLevel where
    {-# INLINE (<>) #-}
    ScopeLevel Int
x <> :: ScopeLevel -> ScopeLevel -> ScopeLevel
<> ScopeLevel Int
y = Int -> ScopeLevel
ScopeLevel (Int -> Int -> Int
forall a. Ord a => a -> a -> a
min Int
x Int
y)

instance Monoid ScopeLevel where
    {-# INLINE mempty #-}
    mempty :: ScopeLevel
mempty = Int -> ScopeLevel
ScopeLevel Int
forall a. Bounded a => a
maxBound

instance TypeConstraints ScopeLevel where
    {-# INLINE generalizeConstraints #-}
    generalizeConstraints :: ScopeLevel -> ScopeLevel
generalizeConstraints ScopeLevel
_ = ScopeLevel
forall a. Monoid a => a
mempty
    toScopeConstraints :: ScopeLevel -> ScopeLevel
toScopeConstraints = ScopeLevel -> ScopeLevel
forall a. a -> a
id

instance Pretty ScopeLevel where
    pPrint :: ScopeLevel -> Doc
pPrint (ScopeLevel Int
x)
        | Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
forall a. Bounded a => a
maxBound = String -> Doc
Pretty.text String
"*"
        | Bool
otherwise = String -> Doc
Pretty.text String
"scope#" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Int -> Doc
forall a. Pretty a => a -> Doc
pPrint Int
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