module Agda.TypeChecking.Level where

import Data.Maybe
import qualified Data.List as List
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as NonEmpty
import Data.Traversable (traverse)

import Agda.Syntax.Common
import Agda.Syntax.Internal

import Agda.TypeChecking.Free.Lazy
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Monad.Builtin

import Agda.Utils.Maybe ( caseMaybeM, allJustM )
import Agda.Utils.Monad ( tryMaybe )
import Agda.Utils.Singleton

import Agda.Utils.Impossible

data LevelKit = LevelKit
  { LevelKit -> Term
lvlType  :: Term
  , LevelKit -> Term -> Term
lvlSuc   :: Term -> Term
  , LevelKit -> Term -> Term -> Term
lvlMax   :: Term -> Term -> Term
  , LevelKit -> Term
lvlZero  :: Term
  , LevelKit -> QName
typeName :: QName
  , LevelKit -> QName
sucName  :: QName
  , LevelKit -> QName
maxName  :: QName
  , LevelKit -> QName
zeroName :: QName
  }

-- | Get the 'primLevel' as a 'Type'.
levelType :: (HasBuiltins m) => m Type
levelType :: m Type
levelType = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Integer -> Sort' Term
mkType Integer
0) (Term -> Type) -> (Maybe Term -> Term) -> Maybe Term -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Type) -> m (Maybe Term) -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinLevel

isLevelType :: (HasBuiltins m, MonadReduce m) => Type -> m Bool
isLevelType :: Type -> m Bool
isLevelType Type
a = Term -> m Term
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (Type -> Term
forall t a. Type'' t a -> a
unEl Type
a) m Term -> (Term -> m Bool) -> m Bool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Def QName
f [] -> do
    Def QName
lvl [] <- Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinLevel
    Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
lvl
  Term
_ -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

levelSucFunction :: TCM (Term -> Term)
levelSucFunction :: TCM (Term -> Term)
levelSucFunction = Term -> Term -> Term
forall t. Apply t => t -> Term -> t
apply1 (Term -> Term -> Term) -> TCMT IO Term -> TCM (Term -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc

{-# SPECIALIZE builtinLevelKit :: TCM LevelKit #-}
{-# SPECIALIZE builtinLevelKit :: ReduceM LevelKit #-}
builtinLevelKit :: (HasBuiltins m) => m LevelKit
builtinLevelKit :: m LevelKit
builtinLevelKit = do
    level :: Term
level@(Def QName
l []) <- Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinLevel
    zero :: Term
zero@(Def QName
z [])  <- Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinLevelZero
    suc :: Term
suc@(Def QName
s [])   <- Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinLevelSuc
    max :: Term
max@(Def QName
m [])   <- Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinLevelMax
    LevelKit -> m LevelKit
forall (m :: * -> *) a. Monad m => a -> m a
return (LevelKit -> m LevelKit) -> LevelKit -> m LevelKit
forall a b. (a -> b) -> a -> b
$ LevelKit :: Term
-> (Term -> Term)
-> (Term -> Term -> Term)
-> Term
-> QName
-> QName
-> QName
-> QName
-> LevelKit
LevelKit
      { lvlType :: Term
lvlType  = Term
level
      , lvlSuc :: Term -> Term
lvlSuc   = \ Term
a -> Term
suc Term -> Term -> Term
forall t. Apply t => t -> Term -> t
`apply1` Term
a
      , lvlMax :: Term -> Term -> Term
lvlMax   = \ Term
a Term
b -> Term
max Term -> [Term] -> Term
forall t. Apply t => t -> [Term] -> t
`applys` [Term
a, Term
b]
      , lvlZero :: Term
lvlZero  = Term
zero
      , typeName :: QName
typeName = QName
l
      , sucName :: QName
sucName  = QName
s
      , maxName :: QName
maxName  = QName
m
      , zeroName :: QName
zeroName = QName
z
      }

-- | Raises an error if no level kit is available.
requireLevels :: HasBuiltins m => m LevelKit
requireLevels :: m LevelKit
requireLevels = m LevelKit
forall (m :: * -> *). HasBuiltins m => m LevelKit
builtinLevelKit

-- | Checks whether level kit is fully available.
haveLevels :: HasBuiltins m => m Bool
haveLevels :: m Bool
haveLevels = m (Maybe [Term]) -> m Bool -> ([Term] -> m Bool) -> m Bool
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM ([m (Maybe Term)] -> m (Maybe [Term])
forall (m :: * -> *) a. Monad m => [m (Maybe a)] -> m (Maybe [a])
allJustM ([m (Maybe Term)] -> m (Maybe [Term]))
-> [m (Maybe Term)] -> m (Maybe [Term])
forall a b. (a -> b) -> a -> b
$ (String -> m (Maybe Term)) -> [String] -> [m (Maybe Term)]
forall a b. (a -> b) -> [a] -> [b]
map String -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' [String]
levelBuiltins)
    (Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False)
    (\ [Term]
_bs -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
  where
  levelBuiltins :: [String]
levelBuiltins =
    [ String
builtinLevel
    , String
builtinLevelZero
    , String
builtinLevelSuc
    , String
builtinLevelMax
    ]

{-# SPECIALIZE unLevel :: Term -> TCM Term #-}
{-# SPECIALIZE unLevel :: Term -> ReduceM Term #-}
unLevel :: (HasBuiltins m) => Term -> m Term
unLevel :: Term -> m Term
unLevel (Level Level
l)  = Level -> m Term
forall (m :: * -> *). HasBuiltins m => Level -> m Term
reallyUnLevelView Level
l
unLevel Term
v = Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v

{-# SPECIALIZE reallyUnLevelView :: Level -> TCM Term #-}
{-# SPECIALIZE reallyUnLevelView :: Level -> ReduceM Term #-}
reallyUnLevelView :: (HasBuiltins m) => Level -> m Term
reallyUnLevelView :: Level -> m Term
reallyUnLevelView Level
nv = do
  Term
suc <- Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinLevelSuc
  Term
zer <- Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinLevelZero
  case Level
nv of
    Max Integer
n []       -> Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ Term -> (Term -> Term) -> Integer -> Term
unConstV Term
zer (Term -> Term -> Term
forall t. Apply t => t -> Term -> t
apply1 Term
suc) Integer
n
    Max Integer
0 [PlusLevel' Term
a]      -> Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ (Term -> Term) -> PlusLevel' Term -> Term
unPlusV (Term -> Term -> Term
forall t. Apply t => t -> Term -> t
apply1 Term
suc) PlusLevel' Term
a
    Level
_              -> (LevelKit -> Level -> Term
`unlevelWithKit` Level
nv) (LevelKit -> Term) -> m LevelKit -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m LevelKit
forall (m :: * -> *). HasBuiltins m => m LevelKit
builtinLevelKit

unlevelWithKit :: LevelKit -> Level -> Term
unlevelWithKit :: LevelKit -> Level -> Term
unlevelWithKit LevelKit{ lvlZero :: LevelKit -> Term
lvlZero = Term
zer, lvlSuc :: LevelKit -> Term -> Term
lvlSuc = Term -> Term
suc, lvlMax :: LevelKit -> Term -> Term -> Term
lvlMax = Term -> Term -> Term
max } = \case
  Max Integer
m []  -> Term -> (Term -> Term) -> Integer -> Term
unConstV Term
zer Term -> Term
suc Integer
m
  Max Integer
0 [PlusLevel' Term
a] -> (Term -> Term) -> PlusLevel' Term -> Term
unPlusV Term -> Term
suc PlusLevel' Term
a
  Max Integer
m [PlusLevel' Term]
as  -> (Term -> Term -> Term) -> [Term] -> Term
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Term -> Term -> Term
max ([Term] -> Term) -> [Term] -> Term
forall a b. (a -> b) -> a -> b
$ [ Term -> (Term -> Term) -> Integer -> Term
unConstV Term
zer Term -> Term
suc Integer
m | Integer
m Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 ] [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ (PlusLevel' Term -> Term) -> [PlusLevel' Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map ((Term -> Term) -> PlusLevel' Term -> Term
unPlusV Term -> Term
suc) [PlusLevel' Term]
as

unConstV :: Term -> (Term -> Term) -> Integer -> Term
unConstV :: Term -> (Term -> Term) -> Integer -> Term
unConstV Term
zer Term -> Term
suc Integer
n = ((Term -> Term) -> (Term -> Term) -> Term -> Term)
-> (Term -> Term) -> [Term -> Term] -> Term -> Term
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) Term -> Term
forall a. a -> a
id (Integer -> (Term -> Term) -> [Term -> Term]
forall i a. Integral i => i -> a -> [a]
List.genericReplicate Integer
n Term -> Term
suc) Term
zer

unPlusV :: (Term -> Term) -> PlusLevel -> Term
unPlusV :: (Term -> Term) -> PlusLevel' Term -> Term
unPlusV Term -> Term
suc (Plus Integer
n LevelAtom' Term
a) = ((Term -> Term) -> (Term -> Term) -> Term -> Term)
-> (Term -> Term) -> [Term -> Term] -> Term -> Term
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) Term -> Term
forall a. a -> a
id (Integer -> (Term -> Term) -> [Term -> Term]
forall i a. Integral i => i -> a -> [a]
List.genericReplicate Integer
n Term -> Term
suc) (LevelAtom' Term -> Term
unLevelAtom LevelAtom' Term
a)

maybePrimCon :: TCM Term -> TCM (Maybe ConHead)
maybePrimCon :: TCMT IO Term -> TCM (Maybe ConHead)
maybePrimCon TCMT IO Term
prim = TCMT IO ConHead -> TCM (Maybe ConHead)
forall e (m :: * -> *) a.
(MonadError e m, Functor m) =>
m a -> m (Maybe a)
tryMaybe (TCMT IO ConHead -> TCM (Maybe ConHead))
-> TCMT IO ConHead -> TCM (Maybe ConHead)
forall a b. (a -> b) -> a -> b
$ do
    Con ConHead
c ConInfo
ci [] <- TCMT IO Term
prim
    ConHead -> TCMT IO ConHead
forall (m :: * -> *) a. Monad m => a -> m a
return ConHead
c

maybePrimDef :: TCM Term -> TCM (Maybe QName)
maybePrimDef :: TCMT IO Term -> TCM (Maybe QName)
maybePrimDef TCMT IO Term
prim = TCMT IO QName -> TCM (Maybe QName)
forall e (m :: * -> *) a.
(MonadError e m, Functor m) =>
m a -> m (Maybe a)
tryMaybe (TCMT IO QName -> TCM (Maybe QName))
-> TCMT IO QName -> TCM (Maybe QName)
forall a b. (a -> b) -> a -> b
$ do
    Def QName
f [] <- TCMT IO Term
prim
    QName -> TCMT IO QName
forall (m :: * -> *) a. Monad m => a -> m a
return QName
f

levelView :: (HasBuiltins m, MonadReduce m, MonadDebug m)
          => Term -> m Level
levelView :: Term -> m Level
levelView Term
a = do
  String -> VerboseLevel -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"tc.level.view" VerboseLevel
50 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"{ levelView " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term -> String
forall a. Show a => a -> String
show Term
a
  Level
v <- Term -> m Level
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m, MonadDebug m) =>
Term -> m Level
levelView' Term
a
  String -> VerboseLevel -> String -> m ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"tc.level.view" VerboseLevel
50 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"  view: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Level -> String
forall a. Show a => a -> String
show Level
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}"
  Level -> m Level
forall (m :: * -> *) a. Monad m => a -> m a
return Level
v

levelView' :: (HasBuiltins m, MonadReduce m, MonadDebug m)
           => Term -> m Level
levelView' :: Term -> m Level
levelView' Term
a = do
  Def QName
lzero [] <- Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinLevelZero
  Def QName
lsuc  [] <- Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinLevelSuc
  Def QName
lmax  [] <- Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinLevelMax
  let view :: Term -> f Level
view Term
a = do
        Blocked Term
ba <- Term -> f (Blocked Term)
forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Term
a
        case Blocked Term -> Term
forall t. Blocked t -> t
ignoreBlocking Blocked Term
ba of
          Level Level
l -> Level -> f Level
forall (m :: * -> *) a. Monad m => a -> m a
return Level
l
          Def QName
s [Apply Arg Term
arg]
            | QName
s QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
lsuc  -> Level -> Level
levelSuc (Level -> Level) -> f Level -> f Level
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> f Level
view (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
arg)
          Def QName
z []
            | QName
z QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
lzero -> Level -> f Level
forall (m :: * -> *) a. Monad m => a -> m a
return (Level -> f Level) -> Level -> f Level
forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
0
          Def QName
m [Apply Arg Term
arg1, Apply Arg Term
arg2]
            | QName
m QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
lmax  -> Level -> Level -> Level
levelLub (Level -> Level -> Level) -> f Level -> f (Level -> Level)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> f Level
view (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
arg1) f (Level -> Level) -> f Level -> f Level
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> f Level
view (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
arg2)
          Term
_              -> Level -> f Level
forall (m :: * -> *) a. Monad m => a -> m a
return (Level -> f Level) -> Level -> f Level
forall a b. (a -> b) -> a -> b
$ Blocked Term -> Level
mkAtom Blocked Term
ba
  Term -> m Level
forall (f :: * -> *). MonadReduce f => Term -> f Level
view Term
a
  where
    mkAtom :: Blocked Term -> Level
mkAtom Blocked Term
ba = LevelAtom' Term -> Level
atomicLevel (LevelAtom' Term -> Level) -> LevelAtom' Term -> Level
forall a b. (a -> b) -> a -> b
$ case Blocked Term
ba of
        NotBlocked NotBlocked
_ (MetaV MetaId
m [Elim]
as) -> MetaId -> [Elim] -> LevelAtom' Term
forall t. MetaId -> [Elim' t] -> LevelAtom' t
MetaLevel MetaId
m [Elim]
as
        NotBlocked NotBlocked
r Term
_            -> case NotBlocked
r of
          StuckOn{}               -> NotBlocked -> Term -> LevelAtom' Term
forall t. NotBlocked -> t -> LevelAtom' t
NeutralLevel NotBlocked
r (Term -> LevelAtom' Term) -> Term -> LevelAtom' Term
forall a b. (a -> b) -> a -> b
$ Blocked Term -> Term
forall t. Blocked t -> t
ignoreBlocking Blocked Term
ba
          Underapplied{}          -> NotBlocked -> Term -> LevelAtom' Term
forall t. NotBlocked -> t -> LevelAtom' t
NeutralLevel NotBlocked
r (Term -> LevelAtom' Term) -> Term -> LevelAtom' Term
forall a b. (a -> b) -> a -> b
$ Blocked Term -> Term
forall t. Blocked t -> t
ignoreBlocking Blocked Term
ba
          AbsurdMatch{}           -> NotBlocked -> Term -> LevelAtom' Term
forall t. NotBlocked -> t -> LevelAtom' t
NeutralLevel NotBlocked
r (Term -> LevelAtom' Term) -> Term -> LevelAtom' Term
forall a b. (a -> b) -> a -> b
$ Blocked Term -> Term
forall t. Blocked t -> t
ignoreBlocking Blocked Term
ba
          MissingClauses{}        -> Term -> LevelAtom' Term
forall t. t -> LevelAtom' t
UnreducedLevel (Term -> LevelAtom' Term) -> Term -> LevelAtom' Term
forall a b. (a -> b) -> a -> b
$ Blocked Term -> Term
forall t. Blocked t -> t
ignoreBlocking Blocked Term
ba
          ReallyNotBlocked{}      -> NotBlocked -> Term -> LevelAtom' Term
forall t. NotBlocked -> t -> LevelAtom' t
NeutralLevel NotBlocked
r (Term -> LevelAtom' Term) -> Term -> LevelAtom' Term
forall a b. (a -> b) -> a -> b
$ Blocked Term -> Term
forall t. Blocked t -> t
ignoreBlocking Blocked Term
ba
        Blocked MetaId
m Term
_               -> MetaId -> Term -> LevelAtom' Term
forall t. MetaId -> t -> LevelAtom' t
BlockedLevel MetaId
m (Term -> LevelAtom' Term) -> Term -> LevelAtom' Term
forall a b. (a -> b) -> a -> b
$ Blocked Term -> Term
forall t. Blocked t -> t
ignoreBlocking Blocked Term
ba

-- | Given a level @l@, find the maximum constant @n@ such that @l = n + l'@
levelPlusView :: Level -> (Integer, Level)
levelPlusView :: Level -> (Integer, Level)
levelPlusView (Max Integer
0 []) = (Integer
0 , Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
0 [])
levelPlusView (Max Integer
0 as :: [PlusLevel' Term]
as@(PlusLevel' Term
_:[PlusLevel' Term]
_)) = (Integer
minN , Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
0 ((PlusLevel' Term -> PlusLevel' Term)
-> [PlusLevel' Term] -> [PlusLevel' Term]
forall a b. (a -> b) -> [a] -> [b]
map PlusLevel' Term -> PlusLevel' Term
forall t. PlusLevel' t -> PlusLevel' t
sub [PlusLevel' Term]
as))
  where
    minN :: Integer
minN = [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [ Integer
n | Plus Integer
n LevelAtom' Term
_ <- [PlusLevel' Term]
as ]
    sub :: PlusLevel' t -> PlusLevel' t
sub (Plus Integer
n LevelAtom' t
a) = Integer -> LevelAtom' t -> PlusLevel' t
forall t. Integer -> LevelAtom' t -> PlusLevel' t
Plus (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
minN) LevelAtom' t
a
levelPlusView (Max Integer
n [PlusLevel' Term]
as) = (Integer
minN , Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
minN) ((PlusLevel' Term -> PlusLevel' Term)
-> [PlusLevel' Term] -> [PlusLevel' Term]
forall a b. (a -> b) -> [a] -> [b]
map PlusLevel' Term -> PlusLevel' Term
forall t. PlusLevel' t -> PlusLevel' t
sub [PlusLevel' Term]
as))
  where
    minN :: Integer
minN = [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum ([Integer] -> Integer) -> [Integer] -> Integer
forall a b. (a -> b) -> a -> b
$ Integer
n Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
: [ Integer
n' | Plus Integer
n' LevelAtom' Term
_ <- [PlusLevel' Term]
as ]
    sub :: PlusLevel' t -> PlusLevel' t
sub (Plus Integer
n' LevelAtom' t
a) = Integer -> LevelAtom' t -> PlusLevel' t
forall t. Integer -> LevelAtom' t -> PlusLevel' t
Plus (Integer
n' Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
minN) LevelAtom' t
a

-- | Given a level @l@, find the biggest constant @n@ such that @n <= l@
levelLowerBound :: Level -> Integer
levelLowerBound :: Level -> Integer
levelLowerBound (Max Integer
m [PlusLevel' Term]
as) = [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Integer] -> Integer) -> [Integer] -> Integer
forall a b. (a -> b) -> a -> b
$ Integer
m Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
: [Integer
n | Plus Integer
n LevelAtom' Term
_ <- [PlusLevel' Term]
as]

-- | Given a constant @n@ and a level @l@, find the level @l'@ such
--   that @l = n + l'@ (or Nothing if there is no such level).
--   Operates on levels in canonical form.
subLevel :: Integer -> Level -> Maybe Level
subLevel :: Integer -> Level -> Maybe Level
subLevel Integer
n (Max Integer
m [PlusLevel' Term]
ls) = Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max (Integer -> [PlusLevel' Term] -> Level)
-> Maybe Integer -> Maybe ([PlusLevel' Term] -> Level)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Integer
m' Maybe ([PlusLevel' Term] -> Level)
-> Maybe [PlusLevel' Term] -> Maybe Level
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (PlusLevel' Term -> Maybe (PlusLevel' Term))
-> [PlusLevel' Term] -> Maybe [PlusLevel' Term]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse PlusLevel' Term -> Maybe (PlusLevel' Term)
subPlus [PlusLevel' Term]
ls
  where
    m' :: Maybe Integer
    m' :: Maybe Integer
m' | Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0, Bool -> Bool
not ([PlusLevel' Term] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PlusLevel' Term]
ls) = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0
       | Bool
otherwise             = Integer -> Maybe Integer
sub Integer
m

    -- General purpose function.
    nonNeg :: Integer -> Maybe Integer
    nonNeg :: Integer -> Maybe Integer
nonNeg Integer
j | Integer
j Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
j
             | Bool
otherwise = Maybe Integer
forall a. Maybe a
Nothing

    sub :: Integer -> Maybe Integer
    sub :: Integer -> Maybe Integer
sub = Integer -> Maybe Integer
nonNeg (Integer -> Maybe Integer)
-> (Integer -> Integer) -> Integer -> Maybe Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
subtract Integer
n

    subPlus :: PlusLevel -> Maybe PlusLevel
    subPlus :: PlusLevel' Term -> Maybe (PlusLevel' Term)
subPlus (Plus Integer
j LevelAtom' Term
l) = Integer -> LevelAtom' Term -> PlusLevel' Term
forall t. Integer -> LevelAtom' t -> PlusLevel' t
Plus (Integer -> LevelAtom' Term -> PlusLevel' Term)
-> Maybe Integer -> Maybe (LevelAtom' Term -> PlusLevel' Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Integer -> Maybe Integer
sub Integer
j Maybe (LevelAtom' Term -> PlusLevel' Term)
-> Maybe (LevelAtom' Term) -> Maybe (PlusLevel' Term)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> LevelAtom' Term -> Maybe (LevelAtom' Term)
forall a. a -> Maybe a
Just LevelAtom' Term
l

-- | Given two levels @a@ and @b@, try to decompose the first one as
-- @a = a' ⊔ b@ (for the minimal value of @a'@).
levelMaxDiff :: Level -> Level -> Maybe Level
levelMaxDiff :: Level -> Level -> Maybe Level
levelMaxDiff (Max Integer
m [PlusLevel' Term]
as) (Max Integer
n [PlusLevel' Term]
bs) = Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max (Integer -> [PlusLevel' Term] -> Level)
-> Maybe Integer -> Maybe ([PlusLevel' Term] -> Level)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Integer -> Integer -> Maybe Integer
diffC Integer
m Integer
n Maybe ([PlusLevel' Term] -> Level)
-> Maybe [PlusLevel' Term] -> Maybe Level
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [PlusLevel' Term] -> [PlusLevel' Term] -> Maybe [PlusLevel' Term]
diffP [PlusLevel' Term]
as [PlusLevel' Term]
bs
  where
    diffC :: Integer -> Integer -> Maybe Integer
    diffC :: Integer -> Integer -> Maybe Integer
diffC Integer
m Integer
n
      | Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
n    = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0
      | Integer
m Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
n     = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
m
      | Bool
otherwise = Maybe Integer
forall a. Maybe a
Nothing

    diffP :: [PlusLevel] -> [PlusLevel] -> Maybe [PlusLevel]
    diffP :: [PlusLevel' Term] -> [PlusLevel' Term] -> Maybe [PlusLevel' Term]
diffP [PlusLevel' Term]
as     []     = [PlusLevel' Term] -> Maybe [PlusLevel' Term]
forall a. a -> Maybe a
Just [PlusLevel' Term]
as
    diffP []     [PlusLevel' Term]
bs     = Maybe [PlusLevel' Term]
forall a. Maybe a
Nothing
    diffP (a :: PlusLevel' Term
a@(Plus Integer
m LevelAtom' Term
x) : [PlusLevel' Term]
as) (b :: PlusLevel' Term
b@(Plus Integer
n LevelAtom' Term
y) : [PlusLevel' Term]
bs)
      | LevelAtom' Term
x LevelAtom' Term -> LevelAtom' Term -> Bool
forall a. Eq a => a -> a -> Bool
== LevelAtom' Term
y = if
        | Integer
m Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
n    -> [PlusLevel' Term] -> [PlusLevel' Term] -> Maybe [PlusLevel' Term]
diffP [PlusLevel' Term]
as [PlusLevel' Term]
bs
        | Integer
m Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
n     -> (Integer -> LevelAtom' Term -> PlusLevel' Term
forall t. Integer -> LevelAtom' t -> PlusLevel' t
Plus Integer
m LevelAtom' Term
xPlusLevel' Term -> [PlusLevel' Term] -> [PlusLevel' Term]
forall a. a -> [a] -> [a]
:) ([PlusLevel' Term] -> [PlusLevel' Term])
-> Maybe [PlusLevel' Term] -> Maybe [PlusLevel' Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PlusLevel' Term] -> [PlusLevel' Term] -> Maybe [PlusLevel' Term]
diffP [PlusLevel' Term]
as [PlusLevel' Term]
bs
        | Bool
otherwise -> Maybe [PlusLevel' Term]
forall a. Maybe a
Nothing
      | Bool
otherwise = (PlusLevel' Term
aPlusLevel' Term -> [PlusLevel' Term] -> [PlusLevel' Term]
forall a. a -> [a] -> [a]
:) ([PlusLevel' Term] -> [PlusLevel' Term])
-> Maybe [PlusLevel' Term] -> Maybe [PlusLevel' Term]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [PlusLevel' Term] -> [PlusLevel' Term] -> Maybe [PlusLevel' Term]
diffP [PlusLevel' Term]
as (PlusLevel' Term
bPlusLevel' Term -> [PlusLevel' Term] -> [PlusLevel' Term]
forall a. a -> [a] -> [a]
:[PlusLevel' Term]
bs)

-- | A @SingleLevel@ is a @Level@ that cannot be further decomposed as
--   a maximum @a ⊔ b@.
data SingleLevel = SingleClosed Integer | SinglePlus PlusLevel
  deriving (SingleLevel -> SingleLevel -> Bool
(SingleLevel -> SingleLevel -> Bool)
-> (SingleLevel -> SingleLevel -> Bool) -> Eq SingleLevel
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SingleLevel -> SingleLevel -> Bool
$c/= :: SingleLevel -> SingleLevel -> Bool
== :: SingleLevel -> SingleLevel -> Bool
$c== :: SingleLevel -> SingleLevel -> Bool
Eq, VerboseLevel -> SingleLevel -> String -> String
[SingleLevel] -> String -> String
SingleLevel -> String
(VerboseLevel -> SingleLevel -> String -> String)
-> (SingleLevel -> String)
-> ([SingleLevel] -> String -> String)
-> Show SingleLevel
forall a.
(VerboseLevel -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [SingleLevel] -> String -> String
$cshowList :: [SingleLevel] -> String -> String
show :: SingleLevel -> String
$cshow :: SingleLevel -> String
showsPrec :: VerboseLevel -> SingleLevel -> String -> String
$cshowsPrec :: VerboseLevel -> SingleLevel -> String -> String
Show)

unSingleLevel :: SingleLevel -> Level
unSingleLevel :: SingleLevel -> Level
unSingleLevel (SingleClosed Integer
m) = Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
m []
unSingleLevel (SinglePlus PlusLevel' Term
a)   = Integer -> [PlusLevel' Term] -> Level
forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
0 [PlusLevel' Term
a]

-- | Return the maximum of the given @SingleLevel@s
unSingleLevels :: [SingleLevel] -> Level
unSingleLevels :: [SingleLevel] -> Level
unSingleLevels [SingleLevel]
ls = Integer -> [PlusLevel' Term] -> Level
levelMax Integer
n [PlusLevel' Term]
as
  where
    n :: Integer
n = [Integer] -> Integer
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Integer] -> Integer) -> [Integer] -> Integer
forall a b. (a -> b) -> a -> b
$ Integer
0 Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
: [Integer
m | SingleClosed Integer
m <- [SingleLevel]
ls]
    as :: [PlusLevel' Term]
as = [PlusLevel' Term
a | SinglePlus PlusLevel' Term
a <- [SingleLevel]
ls]

levelMaxView :: Level -> NonEmpty SingleLevel
levelMaxView :: Level -> NonEmpty SingleLevel
levelMaxView (Max Integer
n [])     = SingleLevel -> NonEmpty SingleLevel
forall el coll. Singleton el coll => el -> coll
singleton (SingleLevel -> NonEmpty SingleLevel)
-> SingleLevel -> NonEmpty SingleLevel
forall a b. (a -> b) -> a -> b
$ Integer -> SingleLevel
SingleClosed Integer
n
levelMaxView (Max Integer
0 (PlusLevel' Term
a:[PlusLevel' Term]
as)) = PlusLevel' Term -> SingleLevel
SinglePlus PlusLevel' Term
a SingleLevel -> [SingleLevel] -> NonEmpty SingleLevel
forall a. a -> [a] -> NonEmpty a
:| (PlusLevel' Term -> SingleLevel)
-> [PlusLevel' Term] -> [SingleLevel]
forall a b. (a -> b) -> [a] -> [b]
map PlusLevel' Term -> SingleLevel
SinglePlus [PlusLevel' Term]
as
levelMaxView (Max Integer
n [PlusLevel' Term]
as)     = Integer -> SingleLevel
SingleClosed Integer
n SingleLevel -> [SingleLevel] -> NonEmpty SingleLevel
forall a. a -> [a] -> NonEmpty a
:| (PlusLevel' Term -> SingleLevel)
-> [PlusLevel' Term] -> [SingleLevel]
forall a b. (a -> b) -> [a] -> [b]
map PlusLevel' Term -> SingleLevel
SinglePlus [PlusLevel' Term]
as

singleLevelView :: Level -> Maybe SingleLevel
singleLevelView :: Level -> Maybe SingleLevel
singleLevelView Level
l = case Level -> NonEmpty SingleLevel
levelMaxView Level
l of
  SingleLevel
s :| [] -> SingleLevel -> Maybe SingleLevel
forall a. a -> Maybe a
Just SingleLevel
s
  NonEmpty SingleLevel
_       -> Maybe SingleLevel
forall a. Maybe a
Nothing

instance Subst Term SingleLevel where
  applySubst :: Substitution' Term -> SingleLevel -> SingleLevel
applySubst Substitution' Term
sub (SingleClosed Integer
m) = Integer -> SingleLevel
SingleClosed Integer
m
  applySubst Substitution' Term
sub (SinglePlus PlusLevel' Term
a)   = PlusLevel' Term -> SingleLevel
SinglePlus (PlusLevel' Term -> SingleLevel) -> PlusLevel' Term -> SingleLevel
forall a b. (a -> b) -> a -> b
$ Substitution' Term -> PlusLevel' Term -> PlusLevel' Term
forall t a. Subst t a => Substitution' t -> a -> a
applySubst Substitution' Term
sub PlusLevel' Term
a

instance Free SingleLevel where
  freeVars' :: SingleLevel -> FreeM a c
freeVars' (SingleClosed Integer
m) = FreeM a c
forall a. Monoid a => a
mempty
  freeVars' (SinglePlus PlusLevel' Term
a)   = PlusLevel' Term -> FreeM a c
forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' PlusLevel' Term
a