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 #-}
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
{-# SPECIALIZE levelType' :: TCM Type #-}
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
Def 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
<$> BuiltinId -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' 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@(Def 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
<$> BuiltinId -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinLevel
zero@(Def z []) <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinLevelZero
suc@(Def s []) <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinLevelSuc
max@(Def m []) <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinLevelMax
return $ LevelKit
{ lvlType = level
, lvlSuc = \ Term
a -> Term
suc Term -> Term -> Term
forall t. Apply t => t -> Term -> t
`apply1` Term
a
, lvlMax = \ Term
a Term
b -> Term
max Term -> [Term] -> Term
forall t. Apply t => t -> [Term] -> t
`applys` [Term
a, Term
b]
, lvlZero = zero
, typeName = l
, sucName = s
, maxName = m
, zeroName = z
}
{-# SPECIALIZE requireLevels :: TCM LevelKit #-}
requireLevels :: (HasBuiltins m, MonadTCError m) => m LevelKit
requireLevels :: forall (m :: * -> *). (HasBuiltins m, MonadTCError m) => m LevelKit
requireLevels = do
level@(Def l []) <- BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinLevel
zero@(Def z []) <- getBuiltin builtinLevelZero
suc@(Def s []) <- getBuiltin builtinLevelSuc
max@(Def m []) <- getBuiltin builtinLevelMax
return $ LevelKit
{ lvlType = level
, lvlSuc = \ Term
a -> Term
suc Term -> Term -> Term
forall t. Apply t => t -> Term -> t
`apply1` Term
a
, lvlMax = \ Term
a Term
b -> Term
max Term -> [Term] -> Term
forall t. Apply t => t -> [Term] -> t
`applys` [Term
a, Term
b]
, lvlZero = zero
, typeName = l
, sucName = s
, maxName = m
, zeroName = z
}
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, 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 a. (a -> a -> a) -> [a] -> a
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 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)
maybePrimCon :: TCM Term -> TCM (Maybe ConHead)
maybePrimCon :: TCM Term -> TCM (Maybe ConHead)
maybePrimCon TCM 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 c ci [] <- TCM Term
prim
return c
maybePrimDef :: TCM Term -> TCM (Maybe QName)
maybePrimDef :: TCM Term -> TCM (Maybe QName)
maybePrimDef TCM 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 f [] <- TCM Term
prim
return f
{-# 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
Def 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
<$> BuiltinId -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinLevelZero
Def lsuc [] <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinLevelSuc
Def lmax [] <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' 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
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
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]
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
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
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)
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]
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