-- | 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 v :: 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 a :: Type
a) = Type -> m (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
isSizeType Type
a
  isSizeType 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 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
    (size :: Maybe QName
size, sizelt :: 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 d :: 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 d :: QName
d [Apply v :: 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 _                                    = 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 s :: 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 d :: QName
d [])) = QName -> Maybe QName
forall a. a -> Maybe a
Just QName
d
    fromDef _                 = 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
  (size :: Maybe QName
size, sizelt :: 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 _ [] <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSize
    Def _ [] <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeInf
    Def _ [] <- 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` \_ -> 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 s :: String
s q :: QName
q t :: 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 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_ size :: 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 -> Elims -> 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 x :: 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 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 n :: Int
n v :: Term
v | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0     = m Term
forall a. HasCallStack => a
__IMPOSSIBLE__
            | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0    = Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
            | Bool
otherwise = do
  Def suc :: 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
             Nothing -> Term
forall a. HasCallStack => a
__IMPOSSIBLE__
             Just t :: Term
t  -> Term
t

sizeSuc_ :: QName -> Term -> Term
sizeSuc_ :: QName -> Term -> Term
sizeSuc_ suc :: QName
suc v :: Term
v = QName -> Elims -> Term
Def QName
suc [Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term) -> Arg Term -> Elim' Term
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 vs :: NonEmpty Term
vs = case NonEmpty Term
vs of
  v :: Term
v :| [] -> Term -> m Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
  vs :: NonEmpty Term
vs  -> do
    Def max :: 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 (\ u :: Term
u v :: Term
v -> QName -> Elims -> Term
Def QName
max (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Term -> Elim' Term) -> [Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map (Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply (Arg Term -> Elim' Term)
-> (Term -> Arg Term) -> Term -> Elim' Term
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 v :: Term
v = do
  Def inf :: QName
inf [] <- m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeInf
  Def suc :: QName
suc [] <- m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeSuc
  case Term
v of
    Def x :: 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 x :: QName
x [Apply u :: 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)
    _                          -> 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
    DSizeInf        -> "∞"
    DSizeVar n :: Int
n o :: Int
o     -> String -> Doc
text ("@" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n) Doc -> Doc -> Doc
<+> "+" Doc -> Doc -> Doc
<+> Int -> Doc
forall a. Pretty a => a -> Doc
pretty Int
o
    DSizeMeta x :: MetaId
x es :: Elims
es o :: Int
o -> Term -> Doc
forall a. Pretty a => a -> Doc
pretty (MetaId -> Elims -> Term
MetaV MetaId
x Elims
es) Doc -> Doc -> Doc
<+> "+" Doc -> Doc -> Doc
<+> Int -> Doc
forall a. Pretty a => a -> Doc
pretty Int
o
    DOtherSize t :: 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 v :: DeepSizeView
v w :: DeepSizeView
w = case (DeepSizeView
v,DeepSizeView
w) of
  (DSizeInf, _) -> DeepSizeView -> () -> SizeViewComparable ()
forall a. DeepSizeView -> a -> SizeViewComparable a
YesAbove DeepSizeView
w ()
  (_, DSizeInf) -> DeepSizeView -> () -> SizeViewComparable ()
forall a. DeepSizeView -> a -> SizeViewComparable a
YesBelow DeepSizeView
w ()
  (DSizeVar x :: Int
x n :: Int
n, DSizeVar y :: Int
y m :: 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 ()
  _ -> SizeViewComparable ()
forall a. SizeViewComparable a
NotComparable

sizeViewSuc_ :: QName -> DeepSizeView -> DeepSizeView
sizeViewSuc_ :: QName -> DeepSizeView -> DeepSizeView
sizeViewSuc_ suc :: QName
suc v :: DeepSizeView
v = case DeepSizeView
v of
  DSizeInf         -> DeepSizeView
DSizeInf
  DSizeVar i :: Int
i n :: Int
n     -> Int -> Int -> DeepSizeView
DSizeVar Int
i (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)
  DSizeMeta x :: MetaId
x vs :: Elims
vs n :: Int
n -> MetaId -> Elims -> Int -> DeepSizeView
DSizeMeta MetaId
x Elims
vs (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)
  DOtherSize u :: 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 0 v :: DeepSizeView
v = DeepSizeView
v
sizeViewPred k :: Int
k v :: DeepSizeView
v = case DeepSizeView
v of
  DSizeInf -> DeepSizeView
DSizeInf
  DSizeVar  i :: Int
i    n :: 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 x :: MetaId
x vs :: Elims
vs n :: Int
n | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
k -> MetaId -> Elims -> Int -> DeepSizeView
DSizeMeta MetaId
x Elims
vs (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k)
  _ -> 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 v :: DeepSizeView
v = case DeepSizeView
v of
  DSizeInf         -> Maybe Int
forall a. Maybe a
Nothing
  DSizeVar i :: Int
i n :: Int
n     -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
n
  DSizeMeta x :: MetaId
x vs :: Elims
vs n :: Int
n -> Int -> Maybe Int
forall a. a -> Maybe a
Just Int
n
  DOtherSize u :: Term
u     -> Int -> Maybe Int
forall a. a -> Maybe a
Just 0

-- | Remove successors common to both sides.
removeSucs :: (DeepSizeView, DeepSizeView) -> (DeepSizeView, DeepSizeView)
removeSucs :: (DeepSizeView, DeepSizeView) -> (DeepSizeView, DeepSizeView)
removeSucs (v :: DeepSizeView
v, w :: 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  n :: Int
n, Just  m :: Int
m) -> Int -> Int -> Int
forall a. Ord a => a -> a -> a
min Int
n Int
m
              (Just  n :: Int
n, Nothing) -> Int
n
              (Nothing, Just  m :: Int
m) -> Int
m
              (Nothing, Nothing) -> 0

-- | Turn a size view into a term.
unSizeView :: SizeView -> TCM Term
unSizeView :: SizeView -> TCMT IO Term
unSizeView SizeInf       = TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeInf
unSizeView (SizeSuc v :: Term
v)   = Int -> Term -> TCMT IO Term
forall (m :: * -> *). HasBuiltins m => Int -> Term -> m Term
sizeSuc 1 Term
v
unSizeView (OtherSize v :: 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 v :: DeepSizeView
v = case DeepSizeView
v of
  DSizeInf         -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeInf
  DSizeVar i :: Int
i     n :: 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 x :: MetaId
x us :: Elims
us n :: 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 -> Elims -> Term
MetaV MetaId
x Elims
us
  DOtherSize u :: 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 v :: SizeMaxView
v w :: SizeMaxView
w = case (SizeMaxView
v,SizeMaxView
w) of
  (DSizeInf :| _, _) -> DeepSizeView -> SizeMaxView
forall el coll. Singleton el coll => el -> coll
singleton DeepSizeView
DSizeInf
  (_, DSizeInf :| _) -> DeepSizeView -> SizeMaxView
forall el coll. Singleton el coll => el -> coll
singleton DeepSizeView
DSizeInf
  _                 -> (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 _ (DSizeInf :| _) = DeepSizeView -> SizeMaxView
forall el coll. Singleton el coll => el -> coll
singleton DeepSizeView
DSizeInf
maxViewCons DSizeInf _        = DeepSizeView -> SizeMaxView
forall el coll. Singleton el coll => el -> coll
singleton DeepSizeView
DSizeInf
maxViewCons v :: DeepSizeView
v ws :: SizeMaxView
ws = case DeepSizeView -> SizeMaxView -> SizeViewComparable [DeepSizeView]
sizeViewComparableWithMax DeepSizeView
v SizeMaxView
ws of
  NotComparable  -> DeepSizeView -> SizeMaxView -> SizeMaxView
forall a. a -> NonEmpty a -> NonEmpty a
NonEmpty.cons DeepSizeView
v SizeMaxView
ws
  YesAbove _ ws' :: [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 v :: DeepSizeView
v (w :: DeepSizeView
w :| ws :: [DeepSizeView]
ws) =
  case ([DeepSizeView]
ws, DeepSizeView -> DeepSizeView -> SizeViewComparable ()
sizeViewComparable DeepSizeView
v DeepSizeView
w) of
    (w' :: DeepSizeView
w':ws' :: [DeepSizeView]
ws', 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')
    (ws :: [DeepSizeView]
ws    , r :: 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_ suc :: 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 vs :: 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