{-# OPTIONS_GHC -Wunused-imports #-}

-- | 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 Control.Monad.Except

import qualified Data.Foldable as Fold
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.TypeChecking.Substitute

import Agda.Utils.List
import Agda.Utils.List1 (List1, pattern (:|))
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Syntax.Common.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
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, Offset -> BoundedSize -> ShowS
[BoundedSize] -> ShowS
BoundedSize -> String
forall a.
(Offset -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BoundedSize] -> ShowS
$cshowList :: [BoundedSize] -> ShowS
show :: BoundedSize -> String
$cshow :: BoundedSize -> String
showsPrec :: Offset -> BoundedSize -> ShowS
$cshowsPrec :: Offset -> 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 :: forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
Dom a -> m (Maybe BoundedSize)
isSizeType = forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
isSizeType forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom

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

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

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

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

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

getBuiltinDefName :: (HasBuiltins m) => BuiltinId -> m (Maybe QName)
getBuiltinDefName :: forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinDefName BuiltinId
s = Maybe Term -> Maybe QName
fromDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
s
  where
    fromDef :: Maybe Term -> Maybe QName
fromDef (Just (Def QName
d [])) = forall a. a -> Maybe a
Just QName
d
    fromDef Maybe Term
_                 = forall a. Maybe a
Nothing

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

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

isSizeNameTestRaw :: (HasOptions m, HasBuiltins m) => m (QName -> Bool)
isSizeNameTestRaw :: forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
m (QName -> Bool)
isSizeNameTestRaw = do
  (Maybe QName
size, Maybe QName
sizelt) <- forall (m :: * -> *). HasBuiltins m => m (Maybe QName, Maybe QName)
getBuiltinSize
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Maybe QName
size, Maybe QName
sizelt]) forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
_ [] <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSize
    Def QName
_ [] <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeInf
    Def QName
_ [] <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeSuc
    forall (m :: * -> *). HasOptions m => m Bool
sizedTypesOption
  forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
_ -> 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 = forall a. Maybe a -> Bool
isJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinDefName BuiltinId
builtinSizeLt

-- | Add polarity info to a SIZE builtin.
builtinSizeHook :: BuiltinId -> QName -> Type -> TCM ()
builtinSizeHook :: BuiltinId -> QName -> Type -> TCM ()
builtinSizeHook BuiltinId
s QName
q Type
t = do
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (BuiltinId
s forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BuiltinId
builtinSizeLt, BuiltinId
builtinSizeSuc]) forall a b. (a -> b) -> a -> b
$ do
    forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q
      forall a b. (a -> b) -> a -> b
$ ([Polarity] -> [Polarity]) -> Definition -> Definition
updateDefPolarity       (forall a b. a -> b -> a
const [Polarity
Covariant])
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Occurrence] -> [Occurrence]) -> Definition -> Definition
updateDefArgOccurrences (forall a b. a -> b -> a
const [Occurrence
StrictPos])
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinSizeMax) forall a b. (a -> b) -> a -> b
$ do
    forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q
      forall a b. (a -> b) -> a -> b
$ ([Polarity] -> [Polarity]) -> Definition -> Definition
updateDefPolarity       (forall a b. a -> b -> a
const [Polarity
Covariant, Polarity
Covariant])
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Occurrence] -> [Occurrence]) -> Definition -> Definition
updateDefArgOccurrences (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 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 = forall t a. Sort' t -> a -> Type'' t a
El Sort
sizeSort forall a b. (a -> b) -> a -> b
$ QName -> [Elim] -> Term
Def QName
size []

{-# SPECIALIZE sizeType :: TCM Type #-}
-- | The built-in type @SIZE@.
sizeType :: (HasBuiltins m, MonadTCEnv m, ReadTCState m) => m Type
sizeType :: forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
m Type
sizeType = forall t a. Sort' t -> a -> Type'' t a
El Sort
sizeSort forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinSize

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

{-# SPECIALIZE sizeSuc :: Nat -> Term -> TCM Term #-}
sizeSuc :: HasBuiltins m => Nat -> Term -> m Term
sizeSuc :: forall (m :: * -> *). HasBuiltins m => Offset -> Term -> m Term
sizeSuc Offset
n Term
v | Offset
n forall a. Ord a => a -> a -> Bool
< Offset
0     = forall a. HasCallStack => a
__IMPOSSIBLE__
            | Offset
n forall a. Eq a => a -> a -> Bool
== Offset
0    = forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
            | Bool
otherwise = do
  Def QName
suc [] <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinSizeSuc
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ (forall a. (a -> a) -> a -> [a]
iterate (QName -> Term -> Term
sizeSuc_ QName
suc) Term
v forall a. [a] -> Offset -> Maybe a
!!! Offset
n)

sizeSuc_ :: QName -> Term -> Term
sizeSuc_ :: QName -> Term -> Term
sizeSuc_ QName
suc Term
v = QName -> [Elim] -> Term
Def QName
suc [forall a. Arg a -> Elim' a
Apply forall a b. (a -> b) -> a -> b
$ 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)
        => List1 Term -> m Term
sizeMax :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
List1 Term -> m Term
sizeMax List1 Term
vs = case List1 Term
vs of
  Term
v :| [] -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
  List1 Term
vs  -> do
    Def QName
max [] <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeMax
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (\ Term
u Term
v -> QName -> [Elim] -> Term
Def QName
max forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. Arg a -> Elim' a
Apply forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Arg a
defaultArg) [Term
u,Term
v]) List1 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, MonadTCEnv m, ReadTCState m)
         => Term -> m SizeView
sizeView :: forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
Term -> m SizeView
sizeView Term
v = do
  Def QName
inf [] <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinSizeInf
  Def QName
suc [] <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinSizeSuc
  case Term
v of
    Def QName
x []        | QName
x forall a. Eq a => a -> a -> Bool
== QName
inf -> forall (m :: * -> *) a. Monad m => a -> m a
return SizeView
SizeInf
    Def QName
x [Apply Arg Term
u] | QName
x forall a. Eq a => a -> a -> Bool
== QName
suc -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Term -> SizeView
SizeSuc (forall e. Arg e -> e
unArg Arg Term
u)
    Term
_                          -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Term -> SizeView
OtherSize Term
v

-- | A de Bruijn index under some projections.

data ProjectedVar = ProjectedVar
  { ProjectedVar -> Offset
pvIndex :: Int
  , ProjectedVar -> [(ProjOrigin, QName)]
prProjs :: [(ProjOrigin, QName)]
  }
  deriving (Offset -> ProjectedVar -> ShowS
[ProjectedVar] -> ShowS
ProjectedVar -> String
forall a.
(Offset -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ProjectedVar] -> ShowS
$cshowList :: [ProjectedVar] -> ShowS
show :: ProjectedVar -> String
$cshow :: ProjectedVar -> String
showsPrec :: Offset -> ProjectedVar -> ShowS
$cshowsPrec :: Offset -> ProjectedVar -> ShowS
Show)

-- | Ignore 'ProjOrigin' in equality test.

instance Eq ProjectedVar where
  ProjectedVar Offset
i [(ProjOrigin, QName)]
prjs == :: ProjectedVar -> ProjectedVar -> Bool
== ProjectedVar Offset
i' [(ProjOrigin, QName)]
prjs' =
    Offset
i forall a. Eq a => a -> a -> Bool
== Offset
i' Bool -> Bool -> Bool
&& forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(ProjOrigin, QName)]
prjs forall a. Eq a => a -> a -> Bool
== forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(ProjOrigin, QName)]
prjs'

viewProjectedVar :: Term -> Maybe ProjectedVar
viewProjectedVar :: Term -> Maybe ProjectedVar
viewProjectedVar = \case
  Var Offset
i [Elim]
es -> Offset -> [(ProjOrigin, QName)] -> ProjectedVar
ProjectedVar Offset
i forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
isProjElim [Elim]
es
  Term
_ -> forall a. Maybe a
Nothing

unviewProjectedVar :: ProjectedVar -> Term
unviewProjectedVar :: ProjectedVar -> Term
unviewProjectedVar (ProjectedVar Offset
i [(ProjOrigin, QName)]
prjs) = Offset -> [Elim] -> Term
Var Offset
i forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a. ProjOrigin -> QName -> Elim' a
Proj) [(ProjOrigin, QName)]
prjs

type Offset = Nat

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

instance Pretty DeepSizeView where
  pretty :: DeepSizeView -> Doc
pretty = \case
    DeepSizeView
DSizeInf        -> Doc
"∞"
    DSizeVar ProjectedVar
pv Offset
o    -> forall a. Pretty a => a -> Doc
pretty (ProjectedVar -> Term
unviewProjectedVar ProjectedVar
pv) forall a. Doc a -> Doc a -> Doc a
<+> Doc
"+" forall a. Doc a -> Doc a -> Doc a
<+> forall a. Pretty a => a -> Doc
pretty Offset
o
    DSizeMeta MetaId
x [Elim]
es Offset
o -> forall a. Pretty a => a -> Doc
pretty (MetaId -> [Elim] -> Term
MetaV MetaId
x [Elim]
es) forall a. Doc a -> Doc a -> Doc a
<+> Doc
"+" forall a. Doc a -> Doc a -> Doc a
<+> forall a. Pretty a => a -> Doc
pretty Offset
o
    DOtherSize Term
t     -> forall a. Pretty a => a -> Doc
pretty Term
t

data SizeViewComparable a
  = NotComparable
  | YesAbove DeepSizeView a
  | YesBelow DeepSizeView a
  deriving (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
<$ :: forall a b. a -> SizeViewComparable b -> SizeViewComparable a
$c<$ :: forall a b. a -> SizeViewComparable b -> SizeViewComparable a
fmap :: forall a b.
(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
_) -> forall a. DeepSizeView -> a -> SizeViewComparable a
YesAbove DeepSizeView
w ()
  (DeepSizeView
_, DeepSizeView
DSizeInf) -> forall a. DeepSizeView -> a -> SizeViewComparable a
YesBelow DeepSizeView
w ()
  (DSizeVar ProjectedVar
x Offset
n, DSizeVar ProjectedVar
y Offset
m) | ProjectedVar
x forall a. Eq a => a -> a -> Bool
== ProjectedVar
y -> if Offset
n forall a. Ord a => a -> a -> Bool
>= Offset
m then forall a. DeepSizeView -> a -> SizeViewComparable a
YesAbove DeepSizeView
w () else forall a. DeepSizeView -> a -> SizeViewComparable a
YesBelow DeepSizeView
w ()
  (DeepSizeView, DeepSizeView)
_ -> forall a. SizeViewComparable a
NotComparable

sizeViewSuc_ :: QName -> DeepSizeView -> DeepSizeView
sizeViewSuc_ :: QName -> DeepSizeView -> DeepSizeView
sizeViewSuc_ QName
suc = \case
  DeepSizeView
DSizeInf         -> DeepSizeView
DSizeInf
  DSizeVar ProjectedVar
i Offset
n     -> ProjectedVar -> Offset -> DeepSizeView
DSizeVar ProjectedVar
i (Offset
n forall a. Num a => a -> a -> a
+ Offset
1)
  DSizeMeta MetaId
x [Elim]
vs Offset
n -> MetaId -> [Elim] -> Offset -> DeepSizeView
DSizeMeta MetaId
x [Elim]
vs (Offset
n forall a. Num a => a -> a -> a
+ Offset
1)
  DOtherSize Term
u     -> Term -> DeepSizeView
DOtherSize 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 :: Offset -> DeepSizeView -> DeepSizeView
sizeViewPred Offset
0 = forall a. a -> a
id
sizeViewPred Offset
k = \case
  DeepSizeView
DSizeInf -> DeepSizeView
DSizeInf
  DSizeVar  ProjectedVar
i    Offset
n | Offset
n forall a. Ord a => a -> a -> Bool
>= Offset
k -> ProjectedVar -> Offset -> DeepSizeView
DSizeVar  ProjectedVar
i    (Offset
n forall a. Num a => a -> a -> a
- Offset
k)
  DSizeMeta MetaId
x [Elim]
vs Offset
n | Offset
n forall a. Ord a => a -> a -> Bool
>= Offset
k -> MetaId -> [Elim] -> Offset -> DeepSizeView
DSizeMeta MetaId
x [Elim]
vs (Offset
n forall a. Num a => a -> a -> a
- Offset
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 Offset
sizeViewOffset = \case
  DeepSizeView
DSizeInf         -> forall a. Maybe a
Nothing
  DSizeVar ProjectedVar
i Offset
n     -> forall a. a -> Maybe a
Just Offset
n
  DSizeMeta MetaId
x [Elim]
vs Offset
n -> forall a. a -> Maybe a
Just Offset
n
  DOtherSize Term
u     -> forall a. a -> Maybe a
Just Offset
0

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

-- | Turn a size view into a term.
unSizeView :: SizeView -> TCM Term
unSizeView :: SizeView -> TCM Term
unSizeView SizeView
SizeInf       = forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeInf
unSizeView (SizeSuc Term
v)   = forall (m :: * -> *). HasBuiltins m => Offset -> Term -> m Term
sizeSuc Offset
1 Term
v
unSizeView (OtherSize Term
v) = 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 :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
DeepSizeView -> m Term
unDeepSizeView = \case
  DeepSizeView
DSizeInf         -> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeInf
  DSizeVar ProjectedVar
pv    Offset
n -> forall (m :: * -> *). HasBuiltins m => Offset -> Term -> m Term
sizeSuc Offset
n forall a b. (a -> b) -> a -> b
$ ProjectedVar -> Term
unviewProjectedVar ProjectedVar
pv
  DSizeMeta MetaId
x [Elim]
us Offset
n -> forall (m :: * -> *). HasBuiltins m => Offset -> Term -> m Term
sizeSuc Offset
n forall a b. (a -> b) -> a -> b
$ MetaId -> [Elim] -> Term
MetaV MetaId
x [Elim]
us
  DOtherSize Term
u     -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
u

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

type SizeMaxView = List1 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
_) -> forall el coll. Singleton el coll => el -> coll
singleton DeepSizeView
DSizeInf
  (SizeMaxView
_, DeepSizeView
DSizeInf :| [DeepSizeView]
_) -> forall el coll. Singleton el coll => el -> coll
singleton DeepSizeView
DSizeInf
  (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]
_) = forall el coll. Singleton el coll => el -> coll
singleton DeepSizeView
DSizeInf
maxViewCons DeepSizeView
DSizeInf 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  -> forall a. a -> NonEmpty a -> NonEmpty a
List1.cons DeepSizeView
v SizeMaxView
ws
  YesAbove DeepSizeView
_ [DeepSizeView]
ws' -> DeepSizeView
v 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
wforall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DeepSizeView -> SizeMaxView -> SizeViewComparable [DeepSizeView]
sizeViewComparableWithMax DeepSizeView
v (DeepSizeView
w' forall a. a -> [a] -> NonEmpty a
:| [DeepSizeView]
ws')
    ([DeepSizeView]
ws    , SizeViewComparable ()
r)             -> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. a -> b -> a
const [DeepSizeView]
ws) SizeViewComparable ()
r


maxViewSuc_ :: QName -> SizeMaxView -> SizeMaxView
maxViewSuc_ :: QName -> SizeMaxView -> SizeMaxView
maxViewSuc_ QName
suc = 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 :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
SizeMaxView -> m Term
unMaxView SizeMaxView
vs = forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
List1 Term -> m Term
sizeMax forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
Trav.mapM forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
DeepSizeView -> m Term
unDeepSizeView SizeMaxView
vs