module Agda.TypeChecking.Level where

import Data.Maybe
import qualified Data.List as List
import Data.List.NonEmpty (NonEmpty(..))
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.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 :: PureTCM 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
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 (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)

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 :: PureTCM 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 :: * -> *). PureTCM 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' :: PureTCM 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 -> m Level
view Term
a = do
        Blocked Term
ba <- Term -> m (Blocked Term)
forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Term
a
        case Blocked Term -> Term
forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
ba of
          Level Level
l -> Level -> m 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) -> 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 (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 (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 (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
  Term -> m Level
view Term
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 (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 (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 (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 (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 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 (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 (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 -> String -> String
[SingleLevel' t] -> String -> String
SingleLevel' t -> String
(VerboseLevel -> SingleLevel' t -> String -> String)
-> (SingleLevel' t -> String)
-> ([SingleLevel' t] -> String -> String)
-> Show (SingleLevel' t)
forall t.
Show t =>
VerboseLevel -> SingleLevel' t -> String -> String
forall t. Show t => [SingleLevel' t] -> String -> String
forall t. Show t => SingleLevel' t -> String
forall a.
(VerboseLevel -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [SingleLevel' t] -> String -> String
$cshowList :: forall t. Show t => [SingleLevel' t] -> String -> String
show :: SingleLevel' t -> String
$cshow :: forall t. Show t => SingleLevel' t -> String
showsPrec :: VerboseLevel -> SingleLevel' t -> String -> String
$cshowsPrec :: forall t.
Show t =>
VerboseLevel -> SingleLevel' t -> String -> String
Show, a -> SingleLevel' b -> SingleLevel' a
(a -> b) -> SingleLevel' a -> SingleLevel' b
(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
<$ :: a -> SingleLevel' b -> SingleLevel' a
$c<$ :: forall a b. a -> SingleLevel' b -> SingleLevel' a
fmap :: (a -> b) -> SingleLevel' a -> SingleLevel' b
$cfmap :: forall a b. (a -> b) -> SingleLevel' a -> SingleLevel' b
Functor, SingleLevel' a -> Bool
(a -> m) -> SingleLevel' a -> m
(a -> b -> b) -> b -> SingleLevel' a -> b
(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
product :: SingleLevel' a -> a
$cproduct :: forall a. Num a => SingleLevel' a -> a
sum :: SingleLevel' a -> a
$csum :: forall a. Num a => SingleLevel' a -> a
minimum :: SingleLevel' a -> a
$cminimum :: forall a. Ord a => SingleLevel' a -> a
maximum :: SingleLevel' a -> a
$cmaximum :: forall a. Ord a => SingleLevel' a -> a
elem :: a -> SingleLevel' a -> Bool
$celem :: forall a. Eq a => a -> SingleLevel' a -> Bool
length :: SingleLevel' a -> VerboseLevel
$clength :: forall a. SingleLevel' a -> VerboseLevel
null :: SingleLevel' a -> Bool
$cnull :: forall a. SingleLevel' a -> Bool
toList :: SingleLevel' a -> [a]
$ctoList :: forall a. SingleLevel' a -> [a]
foldl1 :: (a -> a -> a) -> SingleLevel' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> SingleLevel' a -> a
foldr1 :: (a -> a -> a) -> SingleLevel' a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> SingleLevel' a -> a
foldl' :: (b -> a -> b) -> b -> SingleLevel' a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> SingleLevel' a -> b
foldl :: (b -> a -> b) -> b -> SingleLevel' a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> SingleLevel' a -> b
foldr' :: (a -> b -> b) -> b -> SingleLevel' a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> SingleLevel' a -> b
foldr :: (a -> b -> b) -> b -> SingleLevel' a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> SingleLevel' a -> b
foldMap' :: (a -> m) -> SingleLevel' a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> SingleLevel' a -> m
foldMap :: (a -> m) -> SingleLevel' a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> SingleLevel' a -> m
fold :: SingleLevel' m -> m
$cfold :: forall m. Monoid m => SingleLevel' m -> m
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'
(a -> f b) -> SingleLevel' a -> f (SingleLevel' b)
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)
sequence :: SingleLevel' (m a) -> m (SingleLevel' a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
SingleLevel' (m a) -> m (SingleLevel' a)
mapM :: (a -> m b) -> SingleLevel' a -> m (SingleLevel' b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SingleLevel' a -> m (SingleLevel' b)
sequenceA :: SingleLevel' (f a) -> f (SingleLevel' a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
SingleLevel' (f a) -> f (SingleLevel' a)
traverse :: (a -> f b) -> SingleLevel' a -> f (SingleLevel' b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SingleLevel' a -> f (SingleLevel' b)
$cp2Traversable :: Foldable SingleLevel'
$cp1Traversable :: Functor SingleLevel'
Traversable)

type SingleLevel = SingleLevel' Term

deriving instance Eq SingleLevel

unSingleLevel :: SingleLevel' t -> Level' t
unSingleLevel :: 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 (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 -> NonEmpty (SingleLevel' t)
levelMaxView :: Level' t -> NonEmpty (SingleLevel' t)
levelMaxView (Max Integer
n [])     = SingleLevel' t -> NonEmpty (SingleLevel' t)
forall el coll. Singleton el coll => el -> coll
singleton (SingleLevel' t -> NonEmpty (SingleLevel' t))
-> SingleLevel' t -> NonEmpty (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] -> NonEmpty (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] -> NonEmpty (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 :: Level' t -> Maybe (SingleLevel' t)
singleLevelView Level' t
l = case Level' t -> NonEmpty (SingleLevel' t)
forall t. Level' t -> NonEmpty (SingleLevel' t)
levelMaxView Level' t
l of
  SingleLevel' t
s :| [] -> SingleLevel' t -> Maybe (SingleLevel' t)
forall a. a -> Maybe a
Just SingleLevel' t
s
  NonEmpty (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' :: 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
freeVars' PlusLevel' t
a