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 = forall t a. Sort' t -> a -> Type'' t a
El (Integer -> Sort
mkType Integer
0) forall b c a. (b -> c) -> (a -> b) -> a -> c
. LevelKit -> Term
lvlType forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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.

-- | 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' = forall t a. Sort' t -> a -> Type'' t a
El (Integer -> Sort
mkType Integer
0) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinLevel

isLevelType :: PureTCM m => Type -> m Bool
isLevelType :: forall (m :: * -> *). PureTCM m => Type -> m Bool
isLevelType Type
a = forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce (forall t a. Type'' t a -> a
unEl Type
a) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
  Def QName
f [] -> do
    Def QName
lvl [] <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinLevel
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ QName
f forall a. Eq a => a -> a -> Bool
== QName
lvl
  Term
_ -> 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 :: Term
level@(Def QName
l []) <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinLevel
    zero :: Term
zero@(Def QName
z [])  <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinLevelZero
    suc :: Term
suc@(Def QName
s [])   <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinLevelSuc
    max :: Term
max@(Def QName
m [])   <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinLevelMax
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ LevelKit
      { lvlType :: Term
lvlType  = Term
level
      , lvlSuc :: Term -> Term
lvlSuc   = \ Term
a -> Term
suc forall t. Apply t => t -> Term -> t
`apply1` Term
a
      , lvlMax :: Term -> Term -> Term
lvlMax   = \ Term
a Term
b -> Term
max 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
      }

{-# 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 :: Term
level@(Def QName
l []) <- forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinLevel
    zero :: Term
zero@(Def QName
z [])  <- forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinLevelZero
    suc :: Term
suc@(Def QName
s [])   <- forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinLevelSuc
    max :: Term
max@(Def QName
m [])   <- forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinLevelMax
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ LevelKit
      { lvlType :: Term
lvlType  = Term
level
      , lvlSuc :: Term -> Term
lvlSuc   = \ Term
a -> Term
suc forall t. Apply t => t -> Term -> t
`apply1` Term
a
      , lvlMax :: Term -> Term -> Term
lvlMax   = \ Term
a Term
b -> Term
max 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
      }

-- | Checks whether level kit is fully available.
haveLevels :: HasBuiltins m => m Bool
haveLevels :: forall (m :: * -> *). HasBuiltins m => m Bool
haveLevels = forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *) a. Monad m => [m (Maybe a)] -> m (Maybe [a])
allJustM forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' [String]
levelBuiltins)
    (forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False)
    (\ [Term]
_bs -> 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 :: forall (m :: * -> *). HasBuiltins m => Term -> m Term
unLevel (Level Level
l)  = forall (m :: * -> *). HasBuiltins m => Level -> m Term
reallyUnLevelView Level
l
unLevel Term
v = 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) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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  -> forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 Term -> Term -> Term
max forall a b. (a -> b) -> a -> b
$ [ Term -> (Term -> Term) -> Integer -> Term
unConstV Term
zer Term -> Term
suc Integer
m | Integer
m forall a. Ord a => a -> a -> Bool
> Integer
0 ] forall a. [a] -> [a] -> [a]
++ 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 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a b. (a -> b) -> a -> b
($) Term
zer (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) = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall a b. (a -> b) -> a -> b
($) Term
a (forall i a. Integral i => i -> a -> [a]
List.genericReplicate Integer
n Term -> Term
suc)

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

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

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

levelView' :: PureTCM m => Term -> m Level
levelView' :: forall (m :: * -> *). PureTCM m => Term -> m Level
levelView' Term
a = do
  Def QName
lzero [] <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinLevelZero
  Def QName
lsuc  [] <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinLevelSuc
  Def QName
lmax  [] <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinLevelMax
  let view :: Term -> m Level
view Term
a = do
        Blocked Term
ba <- forall a (m :: * -> *).
(Reduce a, MonadReduce m) =>
a -> m (Blocked a)
reduceB Term
a
        case forall t a. Blocked' t a -> a
ignoreBlocking Blocked Term
ba of
          Level Level
l -> forall (m :: * -> *) a. Monad m => a -> m a
return Level
l
          Def QName
s [Apply Arg Term
arg]
            | QName
s forall a. Eq a => a -> a -> Bool
== QName
lsuc  -> Level -> Level
levelSuc forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m Level
view (forall e. Arg e -> e
unArg Arg Term
arg)
          Def QName
z []
            | QName
z forall a. Eq a => a -> a -> Bool
== QName
lzero -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall a. Eq a => a -> a -> Bool
== QName
lmax  -> Level -> Level -> Level
levelLub forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> m Level
view (forall e. Arg e -> e
unArg Arg Term
arg1) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m Level
view (forall e. Arg e -> e
unArg Arg Term
arg2)
          Term
l              -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 , forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
0 [])
levelPlusView (Max Integer
0 as :: [PlusLevel' Term]
as@(PlusLevel' Term
_:[PlusLevel' Term]
_)) = (Integer
minN , forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
0 (forall a b. (a -> b) -> [a] -> [b]
map PlusLevel' Term -> PlusLevel' Term
sub [PlusLevel' Term]
as))
  where
    minN :: Integer
minN = 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) = forall t. Integer -> t -> PlusLevel' t
Plus (Integer
n forall a. Num a => a -> a -> a
- Integer
minN) Term
a
levelPlusView (Max Integer
n [PlusLevel' Term]
as) = (Integer
minN , forall t. Integer -> [PlusLevel' t] -> Level' t
Max (Integer
n forall a. Num a => a -> a -> a
- Integer
minN) (forall a b. (a -> b) -> [a] -> [b]
map PlusLevel' Term -> PlusLevel' Term
sub [PlusLevel' Term]
as))
  where
    minN :: Integer
minN = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum forall a b. (a -> b) -> a -> b
$ Integer
n 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) = forall t. Integer -> t -> PlusLevel' t
Plus (Integer
n' 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) = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum forall a b. (a -> b) -> a -> b
$ Integer
m 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) = forall t. Integer -> [PlusLevel' t] -> Level' t
Max forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Integer
m' forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 forall a. Eq a => a -> a -> Bool
== Integer
0, Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [PlusLevel' Term]
ls) = 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 forall a. Ord a => a -> a -> Bool
>= Integer
0 = forall a. a -> Maybe a
Just Integer
j
             | Bool
otherwise = forall a. Maybe a
Nothing

    sub :: Integer -> Maybe Integer
    sub :: Integer -> Maybe Integer
sub = Integer -> Maybe Integer
nonNeg forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) = forall t. Integer -> t -> PlusLevel' t
Plus forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Integer -> Maybe Integer
sub Integer
j forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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) = forall t. Integer -> [PlusLevel' t] -> Level' t
Max forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Integer -> Integer -> Maybe Integer
diffC Integer
m Integer
n 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 forall a. Eq a => a -> a -> Bool
== Integer
n    = forall a. a -> Maybe a
Just Integer
0
      | Integer
m forall a. Ord a => a -> a -> Bool
> Integer
n     = forall a. a -> Maybe a
Just Integer
m
      | Bool
otherwise = forall a. Maybe a
Nothing

    diffP :: [PlusLevel] -> [PlusLevel] -> Maybe [PlusLevel]
    diffP :: [PlusLevel' Term] -> [PlusLevel' Term] -> Maybe [PlusLevel' Term]
diffP [PlusLevel' Term]
as     []     = forall a. a -> Maybe a
Just [PlusLevel' Term]
as
    diffP []     [PlusLevel' Term]
bs     = 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 forall a. Eq a => a -> a -> Bool
== Term
y = if
        | Integer
m 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 forall a. Ord a => a -> a -> Bool
> Integer
n     -> (forall t. Integer -> t -> PlusLevel' t
Plus Integer
m Term
xforall a. a -> [a] -> [a]
:) 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 -> forall a. Maybe a
Nothing
      | Bool
otherwise = (PlusLevel' Term
aforall a. a -> [a] -> [a]
:) 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
bforall 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 -> ShowS
forall t. Show t => VerboseLevel -> SingleLevel' t -> ShowS
forall t. Show t => [SingleLevel' t] -> ShowS
forall t. Show t => SingleLevel' t -> String
forall a.
(VerboseLevel -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SingleLevel' t] -> ShowS
$cshowList :: forall t. Show t => [SingleLevel' t] -> ShowS
show :: SingleLevel' t -> String
$cshow :: forall t. Show t => SingleLevel' t -> String
showsPrec :: VerboseLevel -> SingleLevel' t -> ShowS
$cshowsPrec :: forall t. Show t => VerboseLevel -> SingleLevel' t -> ShowS
Show, 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
<$ :: forall a b. a -> SingleLevel' b -> SingleLevel' a
$c<$ :: forall a b. a -> SingleLevel' b -> SingleLevel' a
fmap :: forall a b. (a -> b) -> SingleLevel' a -> SingleLevel' b
$cfmap :: forall a b. (a -> b) -> SingleLevel' a -> SingleLevel' b
Functor, 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 :: forall a. Num a => SingleLevel' a -> a
$cproduct :: forall a. Num a => SingleLevel' a -> a
sum :: forall a. Num a => SingleLevel' a -> a
$csum :: forall a. Num a => SingleLevel' a -> a
minimum :: forall a. Ord a => SingleLevel' a -> a
$cminimum :: forall a. Ord a => SingleLevel' a -> a
maximum :: forall a. Ord a => SingleLevel' a -> a
$cmaximum :: forall a. Ord a => SingleLevel' a -> a
elem :: forall a. Eq a => a -> SingleLevel' a -> Bool
$celem :: forall a. Eq a => a -> SingleLevel' a -> Bool
length :: forall a. SingleLevel' a -> VerboseLevel
$clength :: forall a. SingleLevel' a -> VerboseLevel
null :: forall a. SingleLevel' a -> Bool
$cnull :: forall a. SingleLevel' a -> Bool
toList :: forall a. SingleLevel' a -> [a]
$ctoList :: forall a. SingleLevel' a -> [a]
foldl1 :: forall a. (a -> a -> a) -> SingleLevel' a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> SingleLevel' a -> a
foldr1 :: forall a. (a -> a -> a) -> SingleLevel' a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> SingleLevel' a -> a
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
$cfoldl :: forall b a. (b -> a -> 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
$cfoldr :: forall a b. (a -> b -> b) -> b -> SingleLevel' a -> b
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
$cfoldMap :: forall m a. Monoid m => (a -> m) -> SingleLevel' a -> m
fold :: forall m. Monoid m => SingleLevel' m -> m
$cfold :: forall m. Monoid m => SingleLevel' m -> m
Foldable, Functor SingleLevel'
Foldable 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)
sequence :: forall (m :: * -> *) a.
Monad m =>
SingleLevel' (m a) -> m (SingleLevel' a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
SingleLevel' (m a) -> m (SingleLevel' a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SingleLevel' a -> m (SingleLevel' b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SingleLevel' a -> m (SingleLevel' b)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
SingleLevel' (f a) -> f (SingleLevel' a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
SingleLevel' (f a) -> f (SingleLevel' a)
traverse :: 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)
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) = forall t. Integer -> [PlusLevel' t] -> Level' t
Max Integer
m []
unSingleLevel (SinglePlus PlusLevel' t
a)   = 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 = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum forall a b. (a -> b) -> a -> b
$ Integer
0 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 [])     = forall el coll. Singleton el coll => el -> coll
singleton forall a b. (a -> b) -> a -> b
$ forall t. Integer -> SingleLevel' t
SingleClosed Integer
n
levelMaxView (Max Integer
0 (PlusLevel' t
a:[PlusLevel' t]
as)) = forall t. PlusLevel' t -> SingleLevel' t
SinglePlus PlusLevel' t
a forall a. a -> [a] -> NonEmpty a
:| forall a b. (a -> b) -> [a] -> [b]
map forall t. PlusLevel' t -> SingleLevel' t
SinglePlus [PlusLevel' t]
as
levelMaxView (Max Integer
n [PlusLevel' t]
as)     = forall t. Integer -> SingleLevel' t
SingleClosed Integer
n forall a. a -> [a] -> NonEmpty a
:| forall a b. (a -> b) -> [a] -> [b]
map 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 forall t. Level' t -> List1 (SingleLevel' t)
levelMaxView Level' t
l of
  SingleLevel' t
s :| [] -> forall a. a -> Maybe a
Just SingleLevel' t
s
  NonEmpty (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) = forall t. Integer -> SingleLevel' t
SingleClosed Integer
m
  applySubst Substitution' (SubstArg (SingleLevel' t))
sub (SinglePlus PlusLevel' t
a)   = forall t. PlusLevel' t -> SingleLevel' t
SinglePlus forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst 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) = forall a. Monoid a => a
mempty
  freeVars' (SinglePlus PlusLevel' t
a)   = forall t a c. (Free t, IsVarSet a c) => t -> FreeM a c
freeVars' PlusLevel' t
a