{-# 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
(BoundedSize -> BoundedSize -> Bool)
-> (BoundedSize -> BoundedSize -> Bool) -> Eq BoundedSize
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BoundedSize -> BoundedSize -> Bool
== :: BoundedSize -> BoundedSize -> Bool
$c/= :: BoundedSize -> BoundedSize -> Bool
/= :: BoundedSize -> BoundedSize -> Bool
Eq, Offset -> BoundedSize -> ShowS
[BoundedSize] -> ShowS
BoundedSize -> String
(Offset -> BoundedSize -> ShowS)
-> (BoundedSize -> String)
-> ([BoundedSize] -> ShowS)
-> Show BoundedSize
forall a.
(Offset -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Offset -> BoundedSize -> ShowS
showsPrec :: Offset -> BoundedSize -> ShowS
$cshow :: BoundedSize -> String
show :: BoundedSize -> String
$cshowList :: [BoundedSize] -> ShowS
showList :: [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 = a -> m (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
forall (m :: * -> *).
(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 :: forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
(b, a) -> m (Maybe BoundedSize)
isSizeType = a -> m (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
forall (m :: * -> *).
(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 :: forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
Type' a -> m (Maybe BoundedSize)
isSizeType = a -> m (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
forall (m :: * -> *).
(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 :: forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
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 a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> m Term
forall a. a -> m a
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) = Type -> m (Maybe BoundedSize)
forall a (m :: * -> *).
(IsSizeType a, HasOptions m, HasBuiltins m) =>
a -> m (Maybe BoundedSize)
forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
Type -> m (Maybe BoundedSize)
isSizeType Type
a
  isSizeType CompareAs
AsSizes       = Maybe BoundedSize -> m (Maybe BoundedSize)
forall a. a -> m a
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 a. a -> m a
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 :: forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
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 a. a -> m a
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 a. a -> m a
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 (Maybe Term -> Maybe QName) -> m (Maybe Term) -> m (Maybe QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
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 :: forall (m :: * -> *). HasBuiltins m => m (Maybe QName, Maybe QName)
getBuiltinSize = do
  Maybe QName
size   <- BuiltinId -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinDefName BuiltinId
builtinSize
  Maybe QName
sizelt <- BuiltinId -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinDefName BuiltinId
builtinSizeLt
  (Maybe QName, Maybe QName) -> m (Maybe QName, Maybe QName)
forall a. a -> m a
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 = 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 a. a -> m a
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 :: forall (m :: * -> *).
(HasOptions m, HasBuiltins m) =>
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 a. a -> m a
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 a. Eq a => a -> [a] -> 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 a. TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
_ -> Bool -> TCM Bool
forall a. a -> TCMT IO a
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
<$> BuiltinId -> TCMT IO (Maybe QName)
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
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (BuiltinId
s BuiltinId -> [BuiltinId] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BuiltinId
builtinSizeLt, BuiltinId
builtinSizeSuc]) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    (Signature -> Signature) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
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 (BuiltinId
s BuiltinId -> BuiltinId -> Bool
forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinSizeMax) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
    (Signature -> Signature) -> TCM ()
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
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 :: forall (m :: * -> *).
(HasBuiltins m, MonadTCEnv m, ReadTCState m) =>
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
<$> BuiltinId -> m (Maybe Term)
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
  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 a. a -> m a
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
    BuiltinId -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinSizeSuc m (Maybe Term)
-> (Maybe Term -> m (Maybe QName)) -> m (Maybe QName)
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Just (Def QName
x []) -> Maybe QName -> m (Maybe QName)
forall a. a -> m a
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 a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe QName
forall a. Maybe a
Nothing

sizeSuc :: HasBuiltins m => Nat -> Term -> m Term
sizeSuc :: forall (m :: * -> *). HasBuiltins m => Offset -> Term -> m Term
sizeSuc Offset
n Term
v | Offset
n Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
< Offset
0     = m Term
forall a. HasCallStack => a
__IMPOSSIBLE__
            | Offset
n Offset -> Offset -> Bool
forall a. Eq a => a -> a -> Bool
== Offset
0    = Term -> m Term
forall a. a -> m a
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
<$> BuiltinId -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinSizeSuc
  Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ ((Term -> Term) -> Term -> [Term]
forall a. (a -> a) -> a -> [a]
iterate (QName -> Term -> Term
sizeSuc_ QName
suc) Term
v [Term] -> Offset -> Maybe Term
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 [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)
        => 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 :| [] -> Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Term
v
  List1 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 a. a -> m a
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) -> List1 Term -> Term
forall a. (a -> a -> a) -> NonEmpty a -> a
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]) 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 [] <- Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinSizeInf
  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
<$> BuiltinId -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinSizeSuc
  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 a. a -> m a
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 a. a -> m a
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 a. a -> m a
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

-- | 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
(Offset -> ProjectedVar -> ShowS)
-> (ProjectedVar -> String)
-> ([ProjectedVar] -> ShowS)
-> Show ProjectedVar
forall a.
(Offset -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Offset -> ProjectedVar -> ShowS
showsPrec :: Offset -> ProjectedVar -> ShowS
$cshow :: ProjectedVar -> String
show :: ProjectedVar -> String
$cshowList :: [ProjectedVar] -> ShowS
showList :: [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 Offset -> Offset -> Bool
forall a. Eq a => a -> a -> Bool
== Offset
i' Bool -> Bool -> Bool
&& ((ProjOrigin, QName) -> QName) -> [(ProjOrigin, QName)] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map (ProjOrigin, QName) -> QName
forall a b. (a, b) -> b
snd [(ProjOrigin, QName)]
prjs [QName] -> [QName] -> Bool
forall a. Eq a => a -> a -> Bool
== ((ProjOrigin, QName) -> QName) -> [(ProjOrigin, QName)] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map (ProjOrigin, QName) -> QName
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 ([(ProjOrigin, QName)] -> ProjectedVar)
-> Maybe [(ProjOrigin, QName)] -> Maybe ProjectedVar
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Elim -> Maybe (ProjOrigin, QName))
-> [Elim] -> Maybe [(ProjOrigin, QName)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Elim -> Maybe (ProjOrigin, QName)
forall e. IsProjElim e => e -> Maybe (ProjOrigin, QName)
isProjElim [Elim]
es
  Term
_ -> Maybe ProjectedVar
forall a. Maybe a
Nothing

unviewProjectedVar :: ProjectedVar -> Term
unviewProjectedVar :: ProjectedVar -> Term
unviewProjectedVar (ProjectedVar Offset
i [(ProjOrigin, QName)]
prjs) = Offset -> [Elim] -> Term
Var Offset
i ([Elim] -> Term) -> [Elim] -> Term
forall a b. (a -> b) -> a -> b
$ ((ProjOrigin, QName) -> Elim) -> [(ProjOrigin, QName)] -> [Elim]
forall a b. (a -> b) -> [a] -> [b]
map ((ProjOrigin -> QName -> Elim) -> (ProjOrigin, QName) -> Elim
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ProjOrigin -> QName -> Elim
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
(Offset -> DeepSizeView -> ShowS)
-> (DeepSizeView -> String)
-> ([DeepSizeView] -> ShowS)
-> Show DeepSizeView
forall a.
(Offset -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Offset -> DeepSizeView -> ShowS
showsPrec :: Offset -> DeepSizeView -> ShowS
$cshow :: DeepSizeView -> String
show :: DeepSizeView -> String
$cshowList :: [DeepSizeView] -> ShowS
showList :: [DeepSizeView] -> ShowS
Show)

instance Pretty DeepSizeView where
  pretty :: DeepSizeView -> Doc
pretty = \case
    DeepSizeView
DSizeInf        -> Doc
"∞"
    DSizeVar ProjectedVar
pv Offset
o    -> Term -> Doc
forall a. Pretty a => a -> Doc
pretty (ProjectedVar -> Term
unviewProjectedVar ProjectedVar
pv) Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
"+" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Offset -> Doc
forall a. Pretty a => a -> Doc
pretty Offset
o
    DSizeMeta MetaId
x [Elim]
es Offset
o -> Term -> Doc
forall a. Pretty a => a -> Doc
pretty (MetaId -> [Elim] -> Term
MetaV MetaId
x [Elim]
es) Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
"+" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Offset -> Doc
forall a. Pretty a => a -> Doc
pretty Offset
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 ((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
$cfmap :: forall a b.
(a -> b) -> SizeViewComparable a -> SizeViewComparable b
fmap :: forall a b.
(a -> b) -> SizeViewComparable a -> SizeViewComparable b
$c<$ :: forall a b. a -> SizeViewComparable b -> SizeViewComparable a
<$ :: forall a b. a -> SizeViewComparable b -> SizeViewComparable a
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 ProjectedVar
x Offset
n, DSizeVar ProjectedVar
y Offset
m) | ProjectedVar
x ProjectedVar -> ProjectedVar -> Bool
forall a. Eq a => a -> a -> Bool
== ProjectedVar
y -> if Offset
n Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
>= Offset
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 = \case
  DeepSizeView
DSizeInf         -> DeepSizeView
DSizeInf
  DSizeVar ProjectedVar
i Offset
n     -> ProjectedVar -> Offset -> DeepSizeView
DSizeVar ProjectedVar
i (Offset
n Offset -> Offset -> Offset
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 Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
+ Offset
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 :: Offset -> DeepSizeView -> DeepSizeView
sizeViewPred Offset
0 = DeepSizeView -> DeepSizeView
forall a. a -> a
id
sizeViewPred Offset
k = \case
  DeepSizeView
DSizeInf -> DeepSizeView
DSizeInf
  DSizeVar  ProjectedVar
i    Offset
n | Offset
n Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
>= Offset
k -> ProjectedVar -> Offset -> DeepSizeView
DSizeVar  ProjectedVar
i    (Offset
n Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
- Offset
k)
  DSizeMeta MetaId
x [Elim]
vs Offset
n | Offset
n Offset -> Offset -> Bool
forall a. Ord a => a -> a -> Bool
>= Offset
k -> MetaId -> [Elim] -> Offset -> DeepSizeView
DSizeMeta MetaId
x [Elim]
vs (Offset
n Offset -> Offset -> Offset
forall a. Num a => a -> a -> a
- Offset
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 Offset
sizeViewOffset = \case
  DeepSizeView
DSizeInf         -> Maybe Offset
forall a. Maybe a
Nothing
  DSizeVar ProjectedVar
i Offset
n     -> Offset -> Maybe Offset
forall a. a -> Maybe a
Just Offset
n
  DSizeMeta MetaId
x [Elim]
vs Offset
n -> Offset -> Maybe Offset
forall a. a -> Maybe a
Just Offset
n
  DOtherSize Term
u     -> Offset -> Maybe Offset
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) -> Offset -> Offset -> Offset
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 -> 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)   = Offset -> Term -> TCMT IO Term
forall (m :: * -> *). HasBuiltins m => Offset -> Term -> m Term
sizeSuc Offset
1 Term
v
unSizeView (OtherSize Term
v) = Term -> TCMT IO Term
forall a. a -> TCMT IO a
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         -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeInf
  DSizeVar ProjectedVar
pv    Offset
n -> Offset -> Term -> m Term
forall (m :: * -> *). HasBuiltins m => Offset -> Term -> m Term
sizeSuc Offset
n (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ ProjectedVar -> Term
unviewProjectedVar ProjectedVar
pv
  DSizeMeta MetaId
x [Elim]
us Offset
n -> Offset -> Term -> m Term
forall (m :: * -> *). HasBuiltins m => Offset -> Term -> m Term
sizeSuc Offset
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 a. a -> m a
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
_) -> 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 a b. (a -> b -> b) -> b -> NonEmpty a -> b
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
List1.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
wDeepSizeView -> [DeepSizeView] -> [DeepSizeView]
forall a. a -> [a] -> [a]
:) ([DeepSizeView] -> [DeepSizeView])
-> SizeViewComparable [DeepSizeView]
-> SizeViewComparable [DeepSizeView]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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 a b.
(a -> b) -> SizeViewComparable a -> SizeViewComparable b
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 a b. (a -> b) -> NonEmpty a -> NonEmpty b
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 = List1 Term -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
List1 Term -> m Term
sizeMax (List1 Term -> m Term) -> m (List1 Term) -> m Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (DeepSizeView -> m Term) -> SizeMaxView -> m (List1 Term)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> NonEmpty a -> m (NonEmpty b)
Trav.mapM DeepSizeView -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
DeepSizeView -> m Term
unDeepSizeView SizeMaxView
vs