{-# 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 ( MonadError(..) )

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.CallStack
import Agda.Utils.Function (iterate')
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

------------------------------------------------------------------------
-- * Builtins
------------------------------------------------------------------------

-- | Ensure that option @--sized-types@ is on, for the given reason.
--
requireOptionSizedTypes :: (HasCallStack, HasOptions m, MonadTCError m) => String -> m ()
requireOptionSizedTypes :: forall (m :: * -> *).
(HasCallStack, HasOptions m, MonadTCError m) =>
String -> m ()
requireOptionSizedTypes String
reason = m Bool -> m () -> m ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM m Bool
forall (m :: * -> *). HasOptions m => m Bool
sizedTypesOption (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
  TypeError -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m ()) -> TypeError -> m ()
forall a b. (a -> b) -> a -> b
$ String -> TypeError
NeedOptionSizedTypes String
reason

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

-- | 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)
getBuiltinName' 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 b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
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 b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
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 =
-}

------------------------------------------------------------------------
-- * 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, 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
$cshowsPrec :: Int -> BoundedSize -> ShowS
showsPrec :: Int -> 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
    (size, sizelt) <- m (Maybe QName, Maybe QName)
forall (m :: * -> *). HasBuiltins m => m (Maybe QName, Maybe QName)
getBuiltinSize
    let 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
    return testType

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
  (size, sizelt) <- m (Maybe QName, Maybe QName)
forall (m :: * -> *). HasBuiltins m => m (Maybe QName, Maybe QName)
getBuiltinSize
  return $ (`elem` [size, sizelt]) . Just

------------------------------------------------------------------------
-- * 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 []

{-# SPECIALIZE sizeType :: TCM Type #-}
-- | The built-in type @SIZE@.
sizeType :: (HasBuiltins m) => m Type
sizeType :: forall (m :: * -> *). HasBuiltins 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

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

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
    max <- BuiltinId -> m QName
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m QName
getBuiltinName_ BuiltinId
builtinSizeMax
    return $ 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]) 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)
         => Term -> m SizeView
sizeView :: forall (m :: * -> *). HasBuiltins m => Term -> m SizeView
sizeView Term
v = do
  inf <- QName -> Maybe QName -> QName
forall a. a -> Maybe a -> a
fromMaybe QName
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe QName -> QName) -> m (Maybe QName) -> m QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName' BuiltinId
builtinSizeInf
  suc <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinSizeSuc
  case 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 -> Int
pvIndex :: Int
  , ProjectedVar -> [(ProjOrigin, QName)]
prProjs :: [(ProjOrigin, QName)]
  }
  deriving (Int -> ProjectedVar -> ShowS
[ProjectedVar] -> ShowS
ProjectedVar -> String
(Int -> ProjectedVar -> ShowS)
-> (ProjectedVar -> String)
-> ([ProjectedVar] -> ShowS)
-> Show ProjectedVar
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ProjectedVar -> ShowS
showsPrec :: Int -> 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 Int
i [(ProjOrigin, QName)]
prjs == :: ProjectedVar -> ProjectedVar -> Bool
== ProjectedVar Int
i' [(ProjOrigin, QName)]
prjs' =
    Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
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 Int
i [Elim]
es -> Int -> [(ProjOrigin, QName)] -> ProjectedVar
ProjectedVar Int
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 Int
i [(ProjOrigin, QName)]
prjs) = Int -> [Elim] -> Term
Var Int
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 (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
$cshowsPrec :: Int -> DeepSizeView -> ShowS
showsPrec :: Int -> 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 Int
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
<+> Int -> Doc
forall a. Pretty a => a -> Doc
pretty Int
o
    DSizeMeta MetaId
x [Elim]
es Int
o -> Term -> Doc
forall a. Pretty a => a -> Doc
pretty (MetaId -> [Elim] -> Term
MetaV MetaId
x [Elim]
es) Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Doc
"+" Doc -> Doc -> Doc
forall a. Doc a -> Doc a -> Doc a
<+> Int -> Doc
forall a. Pretty a => a -> Doc
pretty Int
o
    DOtherSize Term
t     -> Term -> Doc
forall a. Pretty a => a -> Doc
pretty Term
t

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

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

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

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

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

-- | Turn a size view into a term.
unSizeView :: SizeView -> TCM Term
unSizeView :: SizeView -> TCM Term
unSizeView SizeView
SizeInf       = TCM Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeInf
unSizeView (SizeSuc Term
v)   = Int -> Term -> TCM Term
forall (m :: * -> *). HasBuiltins m => Int -> Term -> m Term
sizeSuc Int
1 Term
v
unSizeView (OtherSize Term
v) = Term -> TCM 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    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
$ ProjectedVar -> Term
unviewProjectedVar ProjectedVar
pv
  DSizeMeta MetaId
x [Elim]
us Int
n -> Int -> Term -> m Term
forall (m :: * -> *). HasBuiltins m => Int -> Term -> m Term
sizeSuc Int
n (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$ MetaId -> [Elim] -> Term
MetaV MetaId
x [Elim]
us
  DOtherSize Term
u     -> Term -> m Term
forall 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 :: NonEmpty DeepSizeView
-> NonEmpty DeepSizeView -> NonEmpty DeepSizeView
maxViewMax NonEmpty DeepSizeView
v NonEmpty DeepSizeView
w = case (NonEmpty DeepSizeView
v,NonEmpty DeepSizeView
w) of
  (DeepSizeView
DSizeInf :| [DeepSizeView]
_, NonEmpty DeepSizeView
_) -> DeepSizeView -> NonEmpty DeepSizeView
forall el coll. Singleton el coll => el -> coll
singleton DeepSizeView
DSizeInf
  (NonEmpty DeepSizeView
_, DeepSizeView
DSizeInf :| [DeepSizeView]
_) -> DeepSizeView -> NonEmpty DeepSizeView
forall el coll. Singleton el coll => el -> coll
singleton DeepSizeView
DSizeInf
  (NonEmpty DeepSizeView, NonEmpty DeepSizeView)
_                 -> (DeepSizeView -> NonEmpty DeepSizeView -> NonEmpty DeepSizeView)
-> NonEmpty DeepSizeView
-> NonEmpty DeepSizeView
-> NonEmpty DeepSizeView
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 -> NonEmpty DeepSizeView -> NonEmpty DeepSizeView
maxViewCons NonEmpty DeepSizeView
w NonEmpty DeepSizeView
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 -> NonEmpty DeepSizeView -> NonEmpty DeepSizeView
maxViewCons DeepSizeView
_ (DeepSizeView
DSizeInf :| [DeepSizeView]
_) = DeepSizeView -> NonEmpty DeepSizeView
forall el coll. Singleton el coll => el -> coll
singleton DeepSizeView
DSizeInf
maxViewCons DeepSizeView
DSizeInf NonEmpty DeepSizeView
_        = DeepSizeView -> NonEmpty DeepSizeView
forall el coll. Singleton el coll => el -> coll
singleton DeepSizeView
DSizeInf
maxViewCons DeepSizeView
v NonEmpty DeepSizeView
ws = case DeepSizeView
-> NonEmpty DeepSizeView -> SizeViewComparable [DeepSizeView]
sizeViewComparableWithMax DeepSizeView
v NonEmpty DeepSizeView
ws of
  SizeViewComparable [DeepSizeView]
NotComparable  -> DeepSizeView -> NonEmpty DeepSizeView -> NonEmpty DeepSizeView
forall a. a -> NonEmpty a -> NonEmpty a
List1.cons DeepSizeView
v NonEmpty DeepSizeView
ws
  YesAbove DeepSizeView
_ [DeepSizeView]
ws' -> DeepSizeView
v DeepSizeView -> [DeepSizeView] -> NonEmpty DeepSizeView
forall a. a -> [a] -> NonEmpty a
:| [DeepSizeView]
ws'
  YesBelow{}     -> NonEmpty DeepSizeView
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
-> NonEmpty DeepSizeView -> 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
-> NonEmpty DeepSizeView -> SizeViewComparable [DeepSizeView]
sizeViewComparableWithMax DeepSizeView
v (DeepSizeView
w' DeepSizeView -> [DeepSizeView] -> NonEmpty DeepSizeView
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 -> NonEmpty DeepSizeView -> NonEmpty DeepSizeView
maxViewSuc_ QName
suc = (DeepSizeView -> DeepSizeView)
-> NonEmpty DeepSizeView -> NonEmpty DeepSizeView
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) =>
NonEmpty DeepSizeView -> m Term
unMaxView NonEmpty DeepSizeView
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) -> NonEmpty DeepSizeView -> 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 NonEmpty DeepSizeView
vs