-- | Stuff for sized types that does not require modules
--   "Agda.TypeChecking.Reduce" or "Agda.TypeChecking.Constraints"
--   (which import "Agda.TypeChecking.Monad").

module Agda.TypeChecking.Monad.SizedTypes where

import qualified Data.Foldable as Fold
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as NonEmpty
import qualified Data.Traversable as Trav

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

import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad.State
import Agda.TypeChecking.Positivity.Occurrence

import Agda.Utils.Except ( MonadError(catchError) )
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Pretty
import Agda.Utils.Singleton

import Agda.Utils.Impossible

------------------------------------------------------------------------
-- * Testing for type 'Size'
------------------------------------------------------------------------

-- | Result of querying whether size variable @i@ is bounded by another
--   size.
data BoundedSize
  =  BoundedLt Term -- ^ yes @i : Size< t@
  |  BoundedNo
     deriving (BoundedSize -> BoundedSize -> Bool
(BoundedSize -> BoundedSize -> Bool)
-> (BoundedSize -> BoundedSize -> Bool) -> Eq BoundedSize
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BoundedSize -> BoundedSize -> Bool
$c/= :: BoundedSize -> BoundedSize -> Bool
== :: BoundedSize -> BoundedSize -> Bool
$c== :: BoundedSize -> BoundedSize -> Bool
Eq, Int -> BoundedSize -> ShowS
[BoundedSize] -> ShowS
BoundedSize -> String
(Int -> BoundedSize -> ShowS)
-> (BoundedSize -> String)
-> ([BoundedSize] -> ShowS)
-> Show BoundedSize
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BoundedSize] -> ShowS
$cshowList :: [BoundedSize] -> ShowS
show :: BoundedSize -> String
$cshow :: BoundedSize -> String
showsPrec :: Int -> BoundedSize -> ShowS
$cshowsPrec :: Int -> BoundedSize -> ShowS
Show)

-- | Check if a type is the 'primSize' type. The argument should be 'reduce'd.
class IsSizeType a where
  isSizeType :: (HasOptions m, HasBuiltins m) => a -> m (Maybe BoundedSize)

instance IsSizeType a => IsSizeType (Dom a) where
  isSizeType :: Dom a -> m (Maybe BoundedSize)
isSizeType = a -> m (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
isSizeType (a -> m (Maybe BoundedSize))
-> (Dom a -> a) -> Dom a -> m (Maybe BoundedSize)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom a -> a
forall t e. Dom' t e -> e
unDom

instance IsSizeType a => IsSizeType (b,a) where
  isSizeType :: (b, a) -> m (Maybe BoundedSize)
isSizeType = a -> m (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
isSizeType (a -> m (Maybe BoundedSize))
-> ((b, a) -> a) -> (b, a) -> m (Maybe BoundedSize)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b, a) -> a
forall a b. (a, b) -> b
snd

instance IsSizeType a => IsSizeType (Type' a) where
  isSizeType :: Type' a -> m (Maybe BoundedSize)
isSizeType = a -> m (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
isSizeType (a -> m (Maybe BoundedSize))
-> (Type' a -> a) -> Type' a -> m (Maybe BoundedSize)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type' a -> a
forall t a. Type'' t a -> a
unEl

instance IsSizeType Term where
  isSizeType :: Term -> m (Maybe BoundedSize)
isSizeType Term
v = m (Term -> Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
m (Term -> Maybe BoundedSize)
isSizeTypeTest m (Term -> Maybe BoundedSize) -> m Term -> m (Maybe BoundedSize)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m Term
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
v

instance IsSizeType CompareAs where
  isSizeType :: CompareAs -> m (Maybe BoundedSize)
isSizeType (AsTermsOf Type
a) = Type -> m (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
isSizeType Type
a
  isSizeType CompareAs
AsSizes       = Maybe BoundedSize -> m (Maybe BoundedSize)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe BoundedSize -> m (Maybe BoundedSize))
-> Maybe BoundedSize -> m (Maybe BoundedSize)
forall a b. (a -> b) -> a -> b
$ BoundedSize -> Maybe BoundedSize
forall a. a -> Maybe a
Just BoundedSize
BoundedNo
  isSizeType CompareAs
AsTypes       = Maybe BoundedSize -> m (Maybe BoundedSize)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe BoundedSize
forall a. Maybe a
Nothing

isSizeTypeTest :: (HasOptions m, HasBuiltins m) => m (Term -> Maybe BoundedSize)
isSizeTypeTest :: m (Term -> Maybe BoundedSize)
isSizeTypeTest =
  (m (Term -> Maybe BoundedSize)
 -> m (Term -> Maybe BoundedSize) -> m (Term -> Maybe BoundedSize))
-> m (Term -> Maybe BoundedSize)
-> m (Term -> Maybe BoundedSize)
-> m (Term -> Maybe BoundedSize)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (m Bool
-> m (Term -> Maybe BoundedSize)
-> m (Term -> Maybe BoundedSize)
-> m (Term -> Maybe BoundedSize)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM m Bool
forall (m :: * -> *). HasOptions m => m Bool
sizedTypesOption) ((Term -> Maybe BoundedSize) -> m (Term -> Maybe BoundedSize)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Term -> Maybe BoundedSize) -> m (Term -> Maybe BoundedSize))
-> (Term -> Maybe BoundedSize) -> m (Term -> Maybe BoundedSize)
forall a b. (a -> b) -> a -> b
$ Maybe BoundedSize -> Term -> Maybe BoundedSize
forall a b. a -> b -> a
const Maybe BoundedSize
forall a. Maybe a
Nothing) (m (Term -> Maybe BoundedSize) -> m (Term -> Maybe BoundedSize))
-> m (Term -> Maybe BoundedSize) -> m (Term -> Maybe BoundedSize)
forall a b. (a -> b) -> a -> b
$ do
    (Maybe QName
size, Maybe QName
sizelt) <- m (Maybe QName, Maybe QName)
forall (m :: * -> *). HasBuiltins m => m (Maybe QName, Maybe QName)
getBuiltinSize
    let testType :: Term -> Maybe BoundedSize
testType (Def QName
d [])        | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
d Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
size   = BoundedSize -> Maybe BoundedSize
forall a. a -> Maybe a
Just BoundedSize
BoundedNo
        testType (Def QName
d [Apply Arg Term
v]) | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
d Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
sizelt = BoundedSize -> Maybe BoundedSize
forall a. a -> Maybe a
Just (BoundedSize -> Maybe BoundedSize)
-> BoundedSize -> Maybe BoundedSize
forall a b. (a -> b) -> a -> b
$ Term -> BoundedSize
BoundedLt (Term -> BoundedSize) -> Term -> BoundedSize
forall a b. (a -> b) -> a -> b
$ Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
v
        testType Term
_                                    = Maybe BoundedSize
forall a. Maybe a
Nothing
    (Term -> Maybe BoundedSize) -> m (Term -> Maybe BoundedSize)
forall (m :: * -> *) a. Monad m => a -> m a
return Term -> Maybe BoundedSize
testType

getBuiltinDefName :: (HasBuiltins m) => String -> m (Maybe QName)
getBuiltinDefName :: String -> m (Maybe QName)
getBuiltinDefName String
s = Maybe Term -> Maybe QName
fromDef (Maybe Term -> Maybe QName) -> m (Maybe Term) -> m (Maybe QName)
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
s
  where
    fromDef :: Maybe Term -> Maybe QName
fromDef (Just (Def QName
d [])) = QName -> Maybe QName
forall a. a -> Maybe a
Just QName
d
    fromDef Maybe Term
_                 = Maybe QName
forall a. Maybe a
Nothing

getBuiltinSize :: (HasBuiltins m) => m (Maybe QName, Maybe QName)
getBuiltinSize :: m (Maybe QName, Maybe QName)
getBuiltinSize = do
  Maybe QName
size   <- String -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getBuiltinDefName String
builtinSize
  Maybe QName
sizelt <- String -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getBuiltinDefName String
builtinSizeLt
  (Maybe QName, Maybe QName) -> m (Maybe QName, Maybe QName)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe QName
size, Maybe QName
sizelt)

isSizeNameTest :: (HasOptions m, HasBuiltins m) => m (QName -> Bool)
isSizeNameTest :: m (QName -> Bool)
isSizeNameTest = m Bool
-> m (QName -> Bool) -> m (QName -> Bool) -> m (QName -> Bool)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM m Bool
forall (m :: * -> *). HasOptions m => m Bool
sizedTypesOption
  m (QName -> Bool)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
m (QName -> Bool)
isSizeNameTestRaw
  ((QName -> Bool) -> m (QName -> Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return ((QName -> Bool) -> m (QName -> Bool))
-> (QName -> Bool) -> m (QName -> Bool)
forall a b. (a -> b) -> a -> b
$ Bool -> QName -> Bool
forall a b. a -> b -> a
const Bool
False)

isSizeNameTestRaw :: (HasOptions m, HasBuiltins m) => m (QName -> Bool)
isSizeNameTestRaw :: m (QName -> Bool)
isSizeNameTestRaw = do
  (Maybe QName
size, Maybe QName
sizelt) <- m (Maybe QName, Maybe QName)
forall (m :: * -> *). HasBuiltins m => m (Maybe QName, Maybe QName)
getBuiltinSize
  (QName -> Bool) -> m (QName -> Bool)
forall (m :: * -> *) a. Monad m => a -> m a
return ((QName -> Bool) -> m (QName -> Bool))
-> (QName -> Bool) -> m (QName -> Bool)
forall a b. (a -> b) -> a -> b
$ (Maybe QName -> [Maybe QName] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Maybe QName
size, Maybe QName
sizelt]) (Maybe QName -> Bool) -> (QName -> Maybe QName) -> QName -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Maybe QName
forall a. a -> Maybe a
Just

-- | Test whether OPTIONS --sized-types and whether
--   the size built-ins are defined.
haveSizedTypes :: TCM Bool
haveSizedTypes :: TCM Bool
haveSizedTypes = do
    Def QName
_ [] <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSize
    Def QName
_ [] <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeInf
    Def QName
_ [] <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeSuc
    TCM Bool
forall (m :: * -> *). HasOptions m => m Bool
sizedTypesOption
  TCM Bool -> (TCErr -> TCM Bool) -> TCM Bool
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
_ -> Bool -> TCM Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

-- | Test whether the SIZELT builtin is defined.
haveSizeLt :: TCM Bool
haveSizeLt :: TCM Bool
haveSizeLt = Maybe QName -> Bool
forall a. Maybe a -> Bool
isJust (Maybe QName -> Bool) -> TCMT IO (Maybe QName) -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> TCMT IO (Maybe QName)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getBuiltinDefName String
builtinSizeLt

-- | Add polarity info to a SIZE builtin.
builtinSizeHook :: String -> QName -> Type -> TCM ()
builtinSizeHook :: String -> QName -> Type -> TCM ()
builtinSizeHook String
s QName
q Type
t = do
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (String
s String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String
builtinSizeLt, String
builtinSizeSuc]) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    (Signature -> Signature) -> TCM ()
modifySignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q
      ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ ([Polarity] -> [Polarity]) -> Definition -> Definition
updateDefPolarity       ([Polarity] -> [Polarity] -> [Polarity]
forall a b. a -> b -> a
const [Polarity
Covariant])
      (Definition -> Definition)
-> (Definition -> Definition) -> Definition -> Definition
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Occurrence] -> [Occurrence]) -> Definition -> Definition
updateDefArgOccurrences ([Occurrence] -> [Occurrence] -> [Occurrence]
forall a b. a -> b -> a
const [Occurrence
StrictPos])
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
builtinSizeMax) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    (Signature -> Signature) -> TCM ()
modifySignature ((Signature -> Signature) -> TCM ())
-> (Signature -> Signature) -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q
      ((Definition -> Definition) -> Signature -> Signature)
-> (Definition -> Definition) -> Signature -> Signature
forall a b. (a -> b) -> a -> b
$ ([Polarity] -> [Polarity]) -> Definition -> Definition
updateDefPolarity       ([Polarity] -> [Polarity] -> [Polarity]
forall a b. a -> b -> a
const [Polarity
Covariant, Polarity
Covariant])
      (Definition -> Definition)
-> (Definition -> Definition) -> Definition -> Definition
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Occurrence] -> [Occurrence]) -> Definition -> Definition
updateDefArgOccurrences ([Occurrence] -> [Occurrence] -> [Occurrence]
forall a b. a -> b -> a
const [Occurrence
StrictPos, Occurrence
StrictPos])
{-
      . updateDefType           (const tmax)
  where
    -- TODO: max : (i j : Size) -> Size< (suc (max i j))
    tmax =
-}

------------------------------------------------------------------------
-- * Constructors
------------------------------------------------------------------------

-- | The sort of built-in types @SIZE@ and @SIZELT@.
sizeSort :: Sort
sizeSort :: Sort
sizeSort = Integer -> Sort
mkType Integer
0

-- | The type of built-in types @SIZE@ and @SIZELT@.
sizeUniv :: Type
sizeUniv :: Type
sizeUniv = Sort -> Type
sort (Sort -> Type) -> Sort -> Type
forall a b. (a -> b) -> a -> b
$ Sort
sizeSort

-- | The built-in type @SIZE@ with user-given name.
sizeType_ :: QName -> Type
sizeType_ :: QName -> Type
sizeType_ QName
size = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
sizeSort (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ QName -> [Elim] -> Term
Def QName
size []

-- | The built-in type @SIZE@.
sizeType :: (HasBuiltins m, MonadTCEnv m, ReadTCState m) => m Type
sizeType :: m Type
sizeType = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
sizeSort (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
builtinSize

-- | The name of @SIZESUC@.
sizeSucName :: (HasBuiltins m, HasOptions m) => m (Maybe QName)
sizeSucName :: m (Maybe QName)
sizeSucName = do
  m Bool -> m (Maybe QName) -> m (Maybe QName) -> m (Maybe QName)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (Bool -> Bool
not (Bool -> Bool) -> m Bool -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Bool
forall (m :: * -> *). HasOptions m => m Bool
sizedTypesOption) (Maybe QName -> m (Maybe QName)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe QName
forall a. Maybe a
Nothing) (m (Maybe QName) -> m (Maybe QName))
-> m (Maybe QName) -> m (Maybe QName)
forall a b. (a -> b) -> a -> b
$ do
    String -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinSizeSuc m (Maybe Term)
-> (Maybe Term -> m (Maybe QName)) -> m (Maybe QName)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Just (Def QName
x []) -> Maybe QName -> m (Maybe QName)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe QName -> m (Maybe QName)) -> Maybe QName -> m (Maybe QName)
forall a b. (a -> b) -> a -> b
$ QName -> Maybe QName
forall a. a -> Maybe a
Just QName
x
      Maybe Term
_               -> Maybe QName -> m (Maybe QName)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe QName
forall a. Maybe a
Nothing

sizeSuc :: HasBuiltins m => Nat -> Term -> m Term
sizeSuc :: Int -> Term -> m Term
sizeSuc Int
n Term
v | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0     = m Term
forall a. HasCallStack => a
__IMPOSSIBLE__
            | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0    = Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
            | Bool
otherwise = do
  Def QName
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
builtinSizeSuc
  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
$ case (Term -> Term) -> Term -> [Term]
forall a. (a -> a) -> a -> [a]
iterate (QName -> Term -> Term
sizeSuc_ QName
suc) Term
v [Term] -> Int -> Maybe Term
forall a. [a] -> Int -> Maybe a
!!! Int
n of
             Maybe Term
Nothing -> Term
forall a. HasCallStack => a
__IMPOSSIBLE__
             Just Term
t  -> Term
t

sizeSuc_ :: QName -> Term -> Term
sizeSuc_ :: QName -> Term -> Term
sizeSuc_ QName
suc Term
v = QName -> [Elim] -> Term
Def QName
suc [Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim) -> Arg Term -> Elim
forall a b. (a -> b) -> a -> b
$ Term -> Arg Term
forall a. a -> Arg a
defaultArg Term
v]

-- | Transform list of terms into a term build from binary maximum.
sizeMax :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m)
        => NonEmpty Term -> m Term
sizeMax :: NonEmpty Term -> m Term
sizeMax NonEmpty Term
vs = case NonEmpty Term
vs of
  Term
v :| [] -> Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
  NonEmpty Term
vs  -> do
    Def QName
max [] <- m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeMax
    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) -> NonEmpty Term -> Term
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (\ Term
u Term
v -> QName -> [Elim] -> Term
Def QName
max ([Elim] -> Term) -> [Elim] -> Term
forall a b. (a -> b) -> a -> b
$ (Term -> Elim) -> [Term] -> [Elim]
forall a b. (a -> b) -> [a] -> [b]
map (Arg Term -> Elim
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim) -> (Term -> Arg Term) -> Term -> Elim
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Arg Term
forall a. a -> Arg a
defaultArg) [Term
u,Term
v]) NonEmpty Term
vs


------------------------------------------------------------------------
-- * Viewing and unviewing sizes
------------------------------------------------------------------------

-- | A useful view on sizes.
data SizeView = SizeInf | SizeSuc Term | OtherSize Term

-- | Expects argument to be 'reduce'd.
sizeView :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m)
         => Term -> m SizeView
sizeView :: Term -> m SizeView
sizeView Term
v = do
  Def QName
inf [] <- m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeInf
  Def QName
suc [] <- m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeSuc
  case Term
v of
    Def QName
x []        | QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
inf -> SizeView -> m SizeView
forall (m :: * -> *) a. Monad m => a -> m a
return SizeView
SizeInf
    Def QName
x [Apply Arg Term
u] | QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
suc -> SizeView -> m SizeView
forall (m :: * -> *) a. Monad m => a -> m a
return (SizeView -> m SizeView) -> SizeView -> m SizeView
forall a b. (a -> b) -> a -> b
$ Term -> SizeView
SizeSuc (Arg Term -> Term
forall e. Arg e -> e
unArg Arg Term
u)
    Term
_                          -> SizeView -> m SizeView
forall (m :: * -> *) a. Monad m => a -> m a
return (SizeView -> m SizeView) -> SizeView -> m SizeView
forall a b. (a -> b) -> a -> b
$ Term -> SizeView
OtherSize Term
v

type Offset = Nat

-- | A deep view on sizes.
data DeepSizeView
  = DSizeInf
  | DSizeVar Nat Offset
  | DSizeMeta MetaId Elims Offset
  | DOtherSize Term
  deriving (Int -> DeepSizeView -> ShowS
[DeepSizeView] -> ShowS
DeepSizeView -> String
(Int -> DeepSizeView -> ShowS)
-> (DeepSizeView -> String)
-> ([DeepSizeView] -> ShowS)
-> Show DeepSizeView
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DeepSizeView] -> ShowS
$cshowList :: [DeepSizeView] -> ShowS
show :: DeepSizeView -> String
$cshow :: DeepSizeView -> String
showsPrec :: Int -> DeepSizeView -> ShowS
$cshowsPrec :: Int -> DeepSizeView -> ShowS
Show)

instance Pretty DeepSizeView where
  pretty :: DeepSizeView -> Doc
pretty = \case
    DeepSizeView
DSizeInf        -> Doc
"∞"
    DSizeVar Int
n Int
o     -> String -> Doc
text (String
"@" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n) Doc -> Doc -> Doc
<+> Doc
"+" Doc -> Doc -> Doc
<+> Int -> Doc
forall a. Pretty a => a -> Doc
pretty Int
o
    DSizeMeta MetaId
x [Elim]
es Int
o -> Term -> Doc
forall a. Pretty a => a -> Doc
pretty (MetaId -> [Elim] -> Term
MetaV MetaId
x [Elim]
es) Doc -> Doc -> Doc
<+> Doc
"+" Doc -> Doc -> Doc
<+> Int -> Doc
forall a. Pretty a => a -> Doc
pretty Int
o
    DOtherSize Term
t     -> Term -> Doc
forall a. Pretty a => a -> Doc
pretty Term
t

data SizeViewComparable a
  = NotComparable
  | YesAbove DeepSizeView a
  | YesBelow DeepSizeView a
  deriving (a -> SizeViewComparable b -> SizeViewComparable a
(a -> b) -> SizeViewComparable a -> SizeViewComparable b
(forall a b.
 (a -> b) -> SizeViewComparable a -> SizeViewComparable b)
-> (forall a b. a -> SizeViewComparable b -> SizeViewComparable a)
-> Functor SizeViewComparable
forall a b. a -> SizeViewComparable b -> SizeViewComparable a
forall a b.
(a -> b) -> SizeViewComparable a -> SizeViewComparable b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> SizeViewComparable b -> SizeViewComparable a
$c<$ :: forall a b. a -> SizeViewComparable b -> SizeViewComparable a
fmap :: (a -> b) -> SizeViewComparable a -> SizeViewComparable b
$cfmap :: forall a b.
(a -> b) -> SizeViewComparable a -> SizeViewComparable b
Functor)

-- | @sizeViewComparable v w@ checks whether @v >= w@ (then @Left@)
--   or @v <= w@ (then @Right@).  If uncomparable, it returns @NotComparable@.
sizeViewComparable :: DeepSizeView -> DeepSizeView -> SizeViewComparable ()
sizeViewComparable :: DeepSizeView -> DeepSizeView -> SizeViewComparable ()
sizeViewComparable DeepSizeView
v DeepSizeView
w = case (DeepSizeView
v,DeepSizeView
w) of
  (DeepSizeView
DSizeInf, DeepSizeView
_) -> DeepSizeView -> () -> SizeViewComparable ()
forall a. DeepSizeView -> a -> SizeViewComparable a
YesAbove DeepSizeView
w ()
  (DeepSizeView
_, DeepSizeView
DSizeInf) -> DeepSizeView -> () -> SizeViewComparable ()
forall a. DeepSizeView -> a -> SizeViewComparable a
YesBelow DeepSizeView
w ()
  (DSizeVar Int
x Int
n, DSizeVar Int
y Int
m) | Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
y -> if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
m then DeepSizeView -> () -> SizeViewComparable ()
forall a. DeepSizeView -> a -> SizeViewComparable a
YesAbove DeepSizeView
w () else DeepSizeView -> () -> SizeViewComparable ()
forall a. DeepSizeView -> a -> SizeViewComparable a
YesBelow DeepSizeView
w ()
  (DeepSizeView, DeepSizeView)
_ -> SizeViewComparable ()
forall a. SizeViewComparable a
NotComparable

sizeViewSuc_ :: QName -> DeepSizeView -> DeepSizeView
sizeViewSuc_ :: QName -> DeepSizeView -> DeepSizeView
sizeViewSuc_ QName
suc DeepSizeView
v = case DeepSizeView
v of
  DeepSizeView
DSizeInf         -> DeepSizeView
DSizeInf
  DSizeVar Int
i Int
n     -> Int -> Int -> DeepSizeView
DSizeVar Int
i (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
  DSizeMeta MetaId
x [Elim]
vs Int
n -> MetaId -> [Elim] -> Int -> DeepSizeView
DSizeMeta MetaId
x [Elim]
vs (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
  DOtherSize Term
u     -> Term -> DeepSizeView
DOtherSize (Term -> DeepSizeView) -> Term -> DeepSizeView
forall a b. (a -> b) -> a -> b
$ QName -> Term -> Term
sizeSuc_ QName
suc Term
u

-- | @sizeViewPred k v@ decrements @v@ by @k@ (must be possible!).
sizeViewPred :: Nat -> DeepSizeView -> DeepSizeView
sizeViewPred :: Int -> DeepSizeView -> DeepSizeView
sizeViewPred Int
0 DeepSizeView
v = DeepSizeView
v
sizeViewPred Int
k DeepSizeView
v = case DeepSizeView
v of
  DeepSizeView
DSizeInf -> DeepSizeView
DSizeInf
  DSizeVar  Int
i    Int
n | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
k -> Int -> Int -> DeepSizeView
DSizeVar  Int
i    (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k)
  DSizeMeta MetaId
x [Elim]
vs Int
n | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
k -> MetaId -> [Elim] -> Int -> DeepSizeView
DSizeMeta MetaId
x [Elim]
vs (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k)
  DeepSizeView
_ -> DeepSizeView
forall a. HasCallStack => a
__IMPOSSIBLE__

-- | @sizeViewOffset v@ returns the number of successors or Nothing when infty.
sizeViewOffset :: DeepSizeView -> Maybe Offset
sizeViewOffset :: DeepSizeView -> Maybe Int
sizeViewOffset DeepSizeView
v = case DeepSizeView
v of
  DeepSizeView
DSizeInf         -> Maybe Int
forall a. Maybe a
Nothing
  DSizeVar Int
i Int
n     -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
n
  DSizeMeta MetaId
x [Elim]
vs Int
n -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
n
  DOtherSize Term
u     -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
0

-- | Remove successors common to both sides.
removeSucs :: (DeepSizeView, DeepSizeView) -> (DeepSizeView, DeepSizeView)
removeSucs :: (DeepSizeView, DeepSizeView) -> (DeepSizeView, DeepSizeView)
removeSucs (DeepSizeView
v, DeepSizeView
w) = (Int -> DeepSizeView -> DeepSizeView
sizeViewPred Int
k DeepSizeView
v, Int -> DeepSizeView -> DeepSizeView
sizeViewPred Int
k DeepSizeView
w)
  where k :: Int
k = case (DeepSizeView -> Maybe Int
sizeViewOffset DeepSizeView
v, DeepSizeView -> Maybe Int
sizeViewOffset DeepSizeView
w) of
              (Just  Int
n, Just  Int
m) -> Int -> Int -> Int
forall a. Ord a => a -> a -> a
min Int
n Int
m
              (Just  Int
n, Maybe Int
Nothing) -> Int
n
              (Maybe Int
Nothing, Just  Int
m) -> Int
m
              (Maybe Int
Nothing, Maybe Int
Nothing) -> Int
0

-- | Turn a size view into a term.
unSizeView :: SizeView -> TCM Term
unSizeView :: SizeView -> TCMT IO Term
unSizeView SizeView
SizeInf       = TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeInf
unSizeView (SizeSuc Term
v)   = Int -> Term -> TCMT IO Term
forall (m :: * -> *). HasBuiltins m => Int -> Term -> m Term
sizeSuc Int
1 Term
v
unSizeView (OtherSize Term
v) = Term -> TCMT IO Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v

unDeepSizeView :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m)
               => DeepSizeView -> m Term
unDeepSizeView :: DeepSizeView -> m Term
unDeepSizeView DeepSizeView
v = case DeepSizeView
v of
  DeepSizeView
DSizeInf         -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeInf
  DSizeVar Int
i     Int
n -> Int -> Term -> m Term
forall (m :: * -> *). HasBuiltins m => Int -> Term -> m Term
sizeSuc Int
n (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ Int -> Term
var Int
i
  DSizeMeta MetaId
x [Elim]
us Int
n -> Int -> Term -> m Term
forall (m :: * -> *). HasBuiltins m => Int -> Term -> m Term
sizeSuc Int
n (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ MetaId -> [Elim] -> Term
MetaV MetaId
x [Elim]
us
  DOtherSize Term
u     -> Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
u

------------------------------------------------------------------------
-- * View on sizes where maximum is pulled to the top
------------------------------------------------------------------------

type SizeMaxView = NonEmpty DeepSizeView
type SizeMaxView' = [DeepSizeView]

maxViewMax :: SizeMaxView -> SizeMaxView -> SizeMaxView
maxViewMax :: SizeMaxView -> SizeMaxView -> SizeMaxView
maxViewMax SizeMaxView
v SizeMaxView
w = case (SizeMaxView
v,SizeMaxView
w) of
  (DeepSizeView
DSizeInf :| [DeepSizeView]
_, SizeMaxView
_) -> DeepSizeView -> SizeMaxView
forall el coll. Singleton el coll => el -> coll
singleton DeepSizeView
DSizeInf
  (SizeMaxView
_, DeepSizeView
DSizeInf :| [DeepSizeView]
_) -> DeepSizeView -> SizeMaxView
forall el coll. Singleton el coll => el -> coll
singleton DeepSizeView
DSizeInf
  (SizeMaxView, SizeMaxView)
_                 -> (DeepSizeView -> SizeMaxView -> SizeMaxView)
-> SizeMaxView -> SizeMaxView -> SizeMaxView
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
Fold.foldr DeepSizeView -> SizeMaxView -> SizeMaxView
maxViewCons SizeMaxView
w SizeMaxView
v

-- | @maxViewCons v ws = max v ws@.  It only adds @v@ to @ws@ if it is not
--   subsumed by an element of @ws@.
maxViewCons :: DeepSizeView -> SizeMaxView -> SizeMaxView
maxViewCons :: DeepSizeView -> SizeMaxView -> SizeMaxView
maxViewCons DeepSizeView
_ (DeepSizeView
DSizeInf :| [DeepSizeView]
_) = DeepSizeView -> SizeMaxView
forall el coll. Singleton el coll => el -> coll
singleton DeepSizeView
DSizeInf
maxViewCons DeepSizeView
DSizeInf SizeMaxView
_        = DeepSizeView -> SizeMaxView
forall el coll. Singleton el coll => el -> coll
singleton DeepSizeView
DSizeInf
maxViewCons DeepSizeView
v SizeMaxView
ws = case DeepSizeView -> SizeMaxView -> SizeViewComparable [DeepSizeView]
sizeViewComparableWithMax DeepSizeView
v SizeMaxView
ws of
  SizeViewComparable [DeepSizeView]
NotComparable  -> DeepSizeView -> SizeMaxView -> SizeMaxView
forall a. a -> NonEmpty a -> NonEmpty a
NonEmpty.cons DeepSizeView
v SizeMaxView
ws
  YesAbove DeepSizeView
_ [DeepSizeView]
ws' -> DeepSizeView
v DeepSizeView -> [DeepSizeView] -> SizeMaxView
forall a. a -> [a] -> NonEmpty a
:| [DeepSizeView]
ws'
  YesBelow{}     -> SizeMaxView
ws

-- | @sizeViewComparableWithMax v ws@ tries to find @w@ in @ws@ that compares with @v@
--   and singles this out.
--   Precondition: @v /= DSizeInv@.
sizeViewComparableWithMax :: DeepSizeView -> SizeMaxView -> SizeViewComparable SizeMaxView'
sizeViewComparableWithMax :: DeepSizeView -> SizeMaxView -> SizeViewComparable [DeepSizeView]
sizeViewComparableWithMax DeepSizeView
v (DeepSizeView
w :| [DeepSizeView]
ws) =
  case ([DeepSizeView]
ws, DeepSizeView -> DeepSizeView -> SizeViewComparable ()
sizeViewComparable DeepSizeView
v DeepSizeView
w) of
    (DeepSizeView
w':[DeepSizeView]
ws', SizeViewComparable ()
NotComparable) -> ([DeepSizeView] -> [DeepSizeView])
-> SizeViewComparable [DeepSizeView]
-> SizeViewComparable [DeepSizeView]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (DeepSizeView
wDeepSizeView -> [DeepSizeView] -> [DeepSizeView]
forall a. a -> [a] -> [a]
:) (SizeViewComparable [DeepSizeView]
 -> SizeViewComparable [DeepSizeView])
-> SizeViewComparable [DeepSizeView]
-> SizeViewComparable [DeepSizeView]
forall a b. (a -> b) -> a -> b
$ DeepSizeView -> SizeMaxView -> SizeViewComparable [DeepSizeView]
sizeViewComparableWithMax DeepSizeView
v (DeepSizeView
w' DeepSizeView -> [DeepSizeView] -> SizeMaxView
forall a. a -> [a] -> NonEmpty a
:| [DeepSizeView]
ws')
    ([DeepSizeView]
ws    , SizeViewComparable ()
r)             -> (() -> [DeepSizeView])
-> SizeViewComparable () -> SizeViewComparable [DeepSizeView]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([DeepSizeView] -> () -> [DeepSizeView]
forall a b. a -> b -> a
const [DeepSizeView]
ws) SizeViewComparable ()
r


maxViewSuc_ :: QName -> SizeMaxView -> SizeMaxView
maxViewSuc_ :: QName -> SizeMaxView -> SizeMaxView
maxViewSuc_ QName
suc = (DeepSizeView -> DeepSizeView) -> SizeMaxView -> SizeMaxView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (QName -> DeepSizeView -> DeepSizeView
sizeViewSuc_ QName
suc)

unMaxView :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m)
          => SizeMaxView -> m Term
unMaxView :: SizeMaxView -> m Term
unMaxView SizeMaxView
vs = NonEmpty Term -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
NonEmpty Term -> m Term
sizeMax (NonEmpty Term -> m Term) -> m (NonEmpty Term) -> m Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (DeepSizeView -> m Term) -> SizeMaxView -> m (NonEmpty Term)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
Trav.mapM DeepSizeView -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
DeepSizeView -> m Term
unDeepSizeView SizeMaxView
vs