    module Agda.TypeChecking.Level where

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

    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.Utils.List1 ( List1, pattern (:|) )
    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
      }

    {-# SPECIALIZE levelType :: TCM Type #-}
    -- | Get the 'primLevel' as a 'Type'.  Aborts if any of the level BUILTINs is undefined.
    levelType :: (HasBuiltins m, MonadTCError m) => m Type
    levelType :: forall (m :: * -> *). (HasBuiltins m, MonadTCError m) => m Type
    levelType =
      Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort' Term
    forall t. Sort' t
    LevelUniv (Term -> Type) -> (LevelKit -> Term) -> LevelKit -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . LevelKit -> Term
    lvlType (LevelKit -> Type) -> m LevelKit -> m Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m LevelKit
    forall (m :: * -> *). (HasBuiltins m, MonadTCError m) => m LevelKit
    requireLevels
      -- Andreas, 2022-10-11, issue #6168
      -- It seems superfluous to require all level builtins here,
      -- but since we are in MonadTCError here, this is our chance to make sure
      -- that all level builtins are defined.
      -- Otherwise, we might run into an __IMPOSSIBLE__ later,
      -- e.g. if only BUILTIN LEVEL was defined by reallyUnLevelView requires all builtins.

    {-# SPECIALIZE levelType' :: TCM Type #-}
    -- | Get the 'primLevel' as a 'Type'.  Unsafe, crashes if the BUILTIN LEVEL is undefined.
    levelType' :: (HasBuiltins m) => m Type
    levelType' :: forall (m :: * -> *). HasBuiltins m => m Type
    levelType' =
      Sort' Term -> Term -> Type
    forall t a. Sort' t -> a -> Type'' t a
    El Sort' Term
    forall t. Sort' t
    LevelUniv (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
    <$> BuiltinId -> m (Maybe Term)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
    getBuiltin' BuiltinId
    builtinLevel

    {-# SPECIALIZE isLevelType :: Type -> TCM Bool #-}
    isLevelType :: PureTCM m => Type -> m Bool
    isLevelType :: forall (m :: * -> *). PureTCM m => 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 a b. m a -> (a -> m b) -> m b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
      Def QName
    f [] -> do
        lvl <- QName -> Maybe QName -> QName
    forall a. a -> Maybe a -> a
    fromMaybe QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe QName -> QName) -> m (Maybe QName) -> m QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> BuiltinId -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
    getBuiltinName' BuiltinId
    builtinLevel
        return $ f == lvl
      Term
    _ -> Bool -> m Bool
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False

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

    {-# SPECIALIZE requireLevels :: TCM LevelKit #-}
    -- | Raises an error if no level kit is available.
    requireLevels :: (HasBuiltins m, MonadTCError m) => m LevelKit
    requireLevels :: forall (m :: * -> *). (HasBuiltins m, MonadTCError m) => m LevelKit
    requireLevels = do
        level <- BuiltinId -> m QName
    forall (m :: * -> *).
    (HasBuiltins m, MonadTCError m) =>
    BuiltinId -> m QName
    getBuiltinName_ BuiltinId
    builtinLevel
        zero  <- getBuiltinName_ builtinLevelZero
        suc   <- getBuiltinName_ builtinLevelSuc
        max   <- getBuiltinName_ builtinLevelMax
        return $ LevelKit
          { lvlType  = Def level []
          , lvlSuc   = \ Term
    a -> QName -> [Elim] -> Term
    Def QName
    suc [] Term -> Term -> Term
    forall t. Apply t => t -> Term -> t
    `apply1` Term
    a
          , lvlMax   = \ Term
    a Term
    b -> QName -> [Elim] -> Term
    Def QName
    max [] Term -> [Term] -> Term
    forall t. Apply t => t -> [Term] -> t
    `applys` [Term
    a, Term
    b]
          , lvlZero  = Def zero []
          , typeName = level
          , sucName  = suc
          , maxName  = max
          , zeroName = zero
          }

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

    {-# SPECIALIZE unLevel :: Term -> TCM Term #-}
    {-# SPECIALIZE unLevel :: Term -> ReduceM Term #-}
    unLevel :: (HasBuiltins m) => Term -> m Term
    unLevel :: forall (m :: * -> *). HasBuiltins m => 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 a. a -> m a
    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 :: forall (m :: * -> *). HasBuiltins m => Level -> m Term
    reallyUnLevelView Level
    nv = (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, Term -> Term -> Term
    lvlMax :: LevelKit -> Term -> Term -> Term
    lvlMax :: Term -> Term -> Term
    lvlMax } = \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 a. (a -> a -> a) -> [a] -> a
    forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
    foldl1 Term -> Term -> Term
    lvlMax ([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
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (Term -> Term) -> Term -> Term
    forall a b. (a -> b) -> a -> b
    ($) Term
    zer (Integer -> (Term -> Term) -> [Term -> Term]
    forall i a. Integral i => i -> a -> [a]
    List.genericReplicate Integer
    n Term -> Term
    suc)

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

    {-# SPECIALIZE levelView :: Term -> TCM Level #-}
    levelView :: PureTCM m => Term -> m Level
    levelView :: forall (m :: * -> *). PureTCM m => Term -> m Level
    levelView Term
    a = do
      [Char] -> VerboseLevel -> [Char] -> m ()
    forall (m :: * -> *).
    MonadDebug m =>
    [Char] -> VerboseLevel -> [Char] -> m ()
    reportSLn [Char]
    "tc.level.view" VerboseLevel
    50 ([Char] -> m ()) -> [Char] -> m ()
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "{ levelView " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Term -> [Char]
    forall a. Show a => a -> [Char]
    show Term
    a
      v <- Term -> m Level
    forall (m :: * -> *). PureTCM m => Term -> m Level
    levelView' Term
    a
      reportSLn "tc.level.view" 50 $ "  view: " ++ show v ++ "}"
      return v

    {-# SPECIALIZE levelView' :: Term -> TCM Level #-}
    levelView' :: PureTCM m => Term -> m Level
    levelView' :: forall (m :: * -> *). PureTCM m => Term -> m Level
    levelView' Term
    a = do
      lzero <- QName -> Maybe QName -> QName
    forall a. a -> Maybe a -> a
    fromMaybe QName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe QName -> QName) -> m (Maybe QName) -> m QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> BuiltinId -> m (Maybe QName)
    forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
    getBuiltinName' BuiltinId
    builtinLevelZero
      lsuc  <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinLevelSuc
      lmax  <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinLevelMax
      let view Term
    a = do
            ba <- Term -> m (Blocked Term)
    forall a (m :: * -> *).
    (Reduce a, MonadReduce m) =>
    a -> m (Blocked a)
    reduceB Term
    a
            case ignoreBlocking ba of
              Level Level
    l -> Level -> m Level
    forall a. a -> m a
    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) -> m Level -> m Level
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> m 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 -> m Level
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Level -> m Level) -> Level -> m 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) -> m Level -> m (Level -> Level)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> m Level
    view (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    arg1) m (Level -> Level) -> m Level -> m Level
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> m Level
    view (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    arg2)
              Term
    l              -> Level -> m Level
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Level -> m Level) -> Level -> m Level
    forall a b. (a -> b) -> a -> b
    $ Term -> Level
    forall t. t -> Level' t
    atomicLevel Term
    l
      view a

    -- | 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
    sub [PlusLevel' Term]
    as))
      where
        minN :: Integer
    minN = [Integer] -> Integer
    forall a. Ord a => [a] -> a
    forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
    minimum [ Integer
    n | Plus Integer
    n Term
    _ <- [PlusLevel' Term]
    as ]
        sub :: PlusLevel' Term -> PlusLevel' Term
    sub (Plus Integer
    n Term
    a) = Integer -> Term -> PlusLevel' Term
    forall t. Integer -> t -> PlusLevel' t
    Plus (Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    minN) Term
    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
    sub [PlusLevel' Term]
    as))
      where
        minN :: Integer
    minN = [Integer] -> Integer
    forall a. Ord a => [a] -> a
    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' Term
    _ <- [PlusLevel' Term]
    as ]
        sub :: PlusLevel' Term -> PlusLevel' Term
    sub (Plus Integer
    n' Term
    a) = Integer -> Term -> PlusLevel' Term
    forall t. Integer -> t -> PlusLevel' t
    Plus (Integer
    n' Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    - Integer
    minN) Term
    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 a. Ord a => [a] -> a
    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 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 a b. Maybe (a -> b) -> Maybe a -> Maybe b
    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)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [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 a. [a] -> 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 Term
    l) = Integer -> Term -> PlusLevel' Term
    forall t. Integer -> t -> PlusLevel' t
    Plus (Integer -> Term -> PlusLevel' Term)
    -> Maybe Integer -> Maybe (Term -> PlusLevel' Term)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Integer -> Maybe Integer
    sub Integer
    j Maybe (Term -> PlusLevel' Term)
    -> Maybe Term -> Maybe (PlusLevel' Term)
    forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Term -> Maybe Term
    forall a. a -> Maybe a
    Just 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 a b. Maybe (a -> b) -> Maybe a -> Maybe b
    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 Term
    x) : [PlusLevel' Term]
    as) (b :: PlusLevel' Term
    b@(Plus Integer
    n Term
    y) : [PlusLevel' Term]
    bs)
          | Term
    x Term -> Term -> Bool
    forall a. Eq a => a -> a -> Bool
    == 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 -> Term -> PlusLevel' Term
    forall t. Integer -> t -> PlusLevel' t
    Plus Integer
    m 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' t = SingleClosed Integer | SinglePlus (PlusLevel' t)
      deriving (VerboseLevel -> SingleLevel' t -> [Char] -> [Char]
    [SingleLevel' t] -> [Char] -> [Char]
    SingleLevel' t -> [Char]
    (VerboseLevel -> SingleLevel' t -> [Char] -> [Char])
    -> (SingleLevel' t -> [Char])
    -> ([SingleLevel' t] -> [Char] -> [Char])
    -> Show (SingleLevel' t)
    forall t.
    Show t =>
    VerboseLevel -> SingleLevel' t -> [Char] -> [Char]
    forall t. Show t => [SingleLevel' t] -> [Char] -> [Char]
    forall t. Show t => SingleLevel' t -> [Char]
    forall a.
    (VerboseLevel -> a -> [Char] -> [Char])
    -> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
    $cshowsPrec :: forall t.
    Show t =>
    VerboseLevel -> SingleLevel' t -> [Char] -> [Char]
    showsPrec :: VerboseLevel -> SingleLevel' t -> [Char] -> [Char]
    $cshow :: forall t. Show t => SingleLevel' t -> [Char]
    show :: SingleLevel' t -> [Char]
    $cshowList :: forall t. Show t => [SingleLevel' t] -> [Char] -> [Char]
    showList :: [SingleLevel' t] -> [Char] -> [Char]
    Show, (forall a b. (a -> b) -> SingleLevel' a -> SingleLevel' b)
    -> (forall a b. a -> SingleLevel' b -> SingleLevel' a)
    -> Functor SingleLevel'
    forall a b. a -> SingleLevel' b -> SingleLevel' a
    forall a b. (a -> b) -> SingleLevel' a -> SingleLevel' b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> SingleLevel' a -> SingleLevel' b
    fmap :: forall a b. (a -> b) -> SingleLevel' a -> SingleLevel' b
    $c<$ :: forall a b. a -> SingleLevel' b -> SingleLevel' a
    <$ :: forall a b. a -> SingleLevel' b -> SingleLevel' a
    Functor, (forall m. Monoid m => SingleLevel' m -> m)
    -> (forall m a. Monoid m => (a -> m) -> SingleLevel' a -> m)
    -> (forall m a. Monoid m => (a -> m) -> SingleLevel' a -> m)
    -> (forall a b. (a -> b -> b) -> b -> SingleLevel' a -> b)
    -> (forall a b. (a -> b -> b) -> b -> SingleLevel' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> SingleLevel' a -> b)
    -> (forall b a. (b -> a -> b) -> b -> SingleLevel' a -> b)
    -> (forall a. (a -> a -> a) -> SingleLevel' a -> a)
    -> (forall a. (a -> a -> a) -> SingleLevel' a -> a)
    -> (forall a. SingleLevel' a -> [a])
    -> (forall a. SingleLevel' a -> Bool)
    -> (forall a. SingleLevel' a -> VerboseLevel)
    -> (forall a. Eq a => a -> SingleLevel' a -> Bool)
    -> (forall a. Ord a => SingleLevel' a -> a)
    -> (forall a. Ord a => SingleLevel' a -> a)
    -> (forall a. Num a => SingleLevel' a -> a)
    -> (forall a. Num a => SingleLevel' a -> a)
    -> Foldable SingleLevel'
    forall a. Eq a => a -> SingleLevel' a -> Bool
    forall a. Num a => SingleLevel' a -> a
    forall a. Ord a => SingleLevel' a -> a
    forall m. Monoid m => SingleLevel' m -> m
    forall a. SingleLevel' a -> Bool
    forall a. SingleLevel' a -> VerboseLevel
    forall a. SingleLevel' a -> [a]
    forall a. (a -> a -> a) -> SingleLevel' a -> a
    forall m a. Monoid m => (a -> m) -> SingleLevel' a -> m
    forall b a. (b -> a -> b) -> b -> SingleLevel' a -> b
    forall a b. (a -> b -> b) -> b -> SingleLevel' a -> b
    forall (t :: * -> *).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> VerboseLevel)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    $cfold :: forall m. Monoid m => SingleLevel' m -> m
    fold :: forall m. Monoid m => SingleLevel' m -> m
    $cfoldMap :: forall m a. Monoid m => (a -> m) -> SingleLevel' a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> SingleLevel' a -> m
    $cfoldMap' :: forall m a. Monoid m => (a -> m) -> SingleLevel' a -> m
    foldMap' :: forall m a. Monoid m => (a -> m) -> SingleLevel' a -> m
    $cfoldr :: forall a b. (a -> b -> b) -> b -> SingleLevel' a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> SingleLevel' a -> b
    $cfoldr' :: forall a b. (a -> b -> b) -> b -> SingleLevel' a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> SingleLevel' a -> b
    $cfoldl :: forall b a. (b -> a -> b) -> b -> SingleLevel' a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> SingleLevel' a -> b
    $cfoldl' :: forall b a. (b -> a -> b) -> b -> SingleLevel' a -> b
    foldl' :: forall b a. (b -> a -> b) -> b -> SingleLevel' a -> b
    $cfoldr1 :: forall a. (a -> a -> a) -> SingleLevel' a -> a
    foldr1 :: forall a. (a -> a -> a) -> SingleLevel' a -> a
    $cfoldl1 :: forall a. (a -> a -> a) -> SingleLevel' a -> a
    foldl1 :: forall a. (a -> a -> a) -> SingleLevel' a -> a
    $ctoList :: forall a. SingleLevel' a -> [a]
    toList :: forall a. SingleLevel' a -> [a]
    $cnull :: forall a. SingleLevel' a -> Bool
    null :: forall a. SingleLevel' a -> Bool
    $clength :: forall a. SingleLevel' a -> VerboseLevel
    length :: forall a. SingleLevel' a -> VerboseLevel
    $celem :: forall a. Eq a => a -> SingleLevel' a -> Bool
    elem :: forall a. Eq a => a -> SingleLevel' a -> Bool
    $cmaximum :: forall a. Ord a => SingleLevel' a -> a
    maximum :: forall a. Ord a => SingleLevel' a -> a
    $cminimum :: forall a. Ord a => SingleLevel' a -> a
    minimum :: forall a. Ord a => SingleLevel' a -> a
    $csum :: forall a. Num a => SingleLevel' a -> a
    sum :: forall a. Num a => SingleLevel' a -> a
    $cproduct :: forall a. Num a => SingleLevel' a -> a
    product :: forall a. Num a => SingleLevel' a -> a
    Foldable, Functor SingleLevel'
    Foldable SingleLevel'
    (Functor SingleLevel', Foldable SingleLevel') =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> SingleLevel' a -> f (SingleLevel' b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        SingleLevel' (f a) -> f (SingleLevel' a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> SingleLevel' a -> m (SingleLevel' b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        SingleLevel' (m a) -> m (SingleLevel' a))
    -> Traversable SingleLevel'
    forall (t :: * -> *).
    (Functor t, Foldable t) =>
    (forall (f :: * -> *) a b.
     Applicative f =>
     (a -> f b) -> t a -> f (t b))
    -> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall (m :: * -> *) a.
    Monad m =>
    SingleLevel' (m a) -> m (SingleLevel' a)
    forall (f :: * -> *) a.
    Applicative f =>
    SingleLevel' (f a) -> f (SingleLevel' a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> SingleLevel' a -> m (SingleLevel' b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> SingleLevel' a -> f (SingleLevel' b)
    $ctraverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> SingleLevel' a -> f (SingleLevel' b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> SingleLevel' a -> f (SingleLevel' b)
    $csequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    SingleLevel' (f a) -> f (SingleLevel' a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    SingleLevel' (f a) -> f (SingleLevel' a)
    $cmapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> SingleLevel' a -> m (SingleLevel' b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> SingleLevel' a -> m (SingleLevel' b)
    $csequence :: forall (m :: * -> *) a.
    Monad m =>
    SingleLevel' (m a) -> m (SingleLevel' a)
    sequence :: forall (m :: * -> *) a.
    Monad m =>
    SingleLevel' (m a) -> m (SingleLevel' a)
    Traversable)

    type SingleLevel = SingleLevel' Term

    deriving instance Eq SingleLevel

    unSingleLevel :: SingleLevel' t -> Level' t
    unSingleLevel :: forall t. SingleLevel' t -> Level' t
    unSingleLevel (SingleClosed Integer
    m) = Integer -> [PlusLevel' t] -> Level' t
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max Integer
    m []
    unSingleLevel (SinglePlus PlusLevel' t
    a)   = Integer -> [PlusLevel' t] -> Level' t
    forall t. Integer -> [PlusLevel' t] -> Level' t
    Max Integer
    0 [PlusLevel' t
    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 a. Ord a => [a] -> a
    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' t -> List1 (SingleLevel' t)
    levelMaxView :: forall t. Level' t -> List1 (SingleLevel' t)
    levelMaxView (Max Integer
    n [])     = SingleLevel' t -> List1 (SingleLevel' t)
    forall el coll. Singleton el coll => el -> coll
    singleton (SingleLevel' t -> List1 (SingleLevel' t))
    -> SingleLevel' t -> List1 (SingleLevel' t)
    forall a b. (a -> b) -> a -> b
    $ Integer -> SingleLevel' t
    forall t. Integer -> SingleLevel' t
    SingleClosed Integer
    n
    levelMaxView (Max Integer
    0 (PlusLevel' t
    a:[PlusLevel' t]
    as)) = PlusLevel' t -> SingleLevel' t
    forall t. PlusLevel' t -> SingleLevel' t
    SinglePlus PlusLevel' t
    a SingleLevel' t -> [SingleLevel' t] -> List1 (SingleLevel' t)
    forall a. a -> [a] -> NonEmpty a
    :| (PlusLevel' t -> SingleLevel' t)
    -> [PlusLevel' t] -> [SingleLevel' t]
    forall a b. (a -> b) -> [a] -> [b]
    map PlusLevel' t -> SingleLevel' t
    forall t. PlusLevel' t -> SingleLevel' t
    SinglePlus [PlusLevel' t]
    as
    levelMaxView (Max Integer
    n [PlusLevel' t]
    as)     = Integer -> SingleLevel' t
    forall t. Integer -> SingleLevel' t
    SingleClosed Integer
    n SingleLevel' t -> [SingleLevel' t] -> List1 (SingleLevel' t)
    forall a. a -> [a] -> NonEmpty a
    :| (PlusLevel' t -> SingleLevel' t)
    -> [PlusLevel' t] -> [SingleLevel' t]
    forall a b. (a -> b) -> [a] -> [b]
    map PlusLevel' t -> SingleLevel' t
    forall t. PlusLevel' t -> SingleLevel' t
    SinglePlus [PlusLevel' t]
    as

    singleLevelView :: Level' t -> Maybe (SingleLevel' t)
    singleLevelView :: forall t. Level' t -> Maybe (SingleLevel' t)
    singleLevelView Level' t
    l = case Level' t -> List1 (SingleLevel' t)
    forall t. Level' t -> List1 (SingleLevel' t)
    levelMaxView Level' t
    l of
      SingleLevel' t
    s :| [] -> SingleLevel' t -> Maybe (SingleLevel' t)
    forall a. a -> Maybe a
    Just SingleLevel' t
    s
      List1 (SingleLevel' t)
    _       -> Maybe (SingleLevel' t)
    forall a. Maybe a
    Nothing

    instance Subst t => Subst (SingleLevel' t) where
      type SubstArg (SingleLevel' t) = SubstArg t

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

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