{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE PatternSynonyms #-}

module Agda.Compiler.Treeless.Erase
       ( eraseTerms
       , computeErasedConstructorArgs
       , isErasable
       ) where

import Control.Arrow       ( first, second )
import Control.Monad.State ( StateT, evalStateT )

import Data.Map (Map)
import qualified Data.Map as Map

import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.Syntax.Treeless
import Agda.Syntax.Literal

import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Monad as I
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Datatypes
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Primitive

import Agda.Compiler.Treeless.Subst
import Agda.Compiler.Treeless.Unused

import Agda.Utils.Functor
import Agda.Utils.Lens
import Agda.Utils.Maybe
import Agda.Utils.Memo
import Agda.Utils.Monad
import Agda.Syntax.Common.Pretty (prettyShow)
import Agda.Utils.IntSet.Infinite (IntSet)
import qualified Agda.Utils.IntSet.Infinite as IntSet

import Agda.Utils.Impossible

-- | State of the eraser.
data ESt = ESt
  { ESt -> Map QName FunInfo
_funMap  :: Map QName FunInfo
      -- ^ Memoize computed `FunInfo` for functions/constructors/... `QName`.
  , ESt -> Map QName TypeInfo
_typeMap :: Map QName TypeInfo
      -- ^ Memoize computed `TypeInfo` for data/record types `QName`.
  }

funMap :: Lens' ESt (Map QName FunInfo)
funMap :: Lens' ESt (Map QName FunInfo)
funMap Map QName FunInfo -> f (Map QName FunInfo)
f ESt
r = Map QName FunInfo -> f (Map QName FunInfo)
f (ESt -> Map QName FunInfo
_funMap ESt
r) f (Map QName FunInfo) -> (Map QName FunInfo -> ESt) -> f ESt
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Map QName FunInfo
a -> ESt
r { _funMap = a }

typeMap :: Lens' ESt (Map QName TypeInfo)
typeMap :: Lens' ESt (Map QName TypeInfo)
typeMap Map QName TypeInfo -> f (Map QName TypeInfo)
f ESt
r = Map QName TypeInfo -> f (Map QName TypeInfo)
f (ESt -> Map QName TypeInfo
_typeMap ESt
r) f (Map QName TypeInfo) -> (Map QName TypeInfo -> ESt) -> f ESt
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Map QName TypeInfo
a -> ESt
r { _typeMap = a }

-- | Eraser monad.
type E = StateT ESt TCM

runE :: E a -> TCM a
runE :: forall a. E a -> TCM a
runE E a
m = E a -> ESt -> TCMT IO a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT E a
m (Map QName FunInfo -> Map QName TypeInfo -> ESt
ESt Map QName FunInfo
forall k a. Map k a
Map.empty Map QName TypeInfo
forall k a. Map k a
Map.empty)

-- | Takes the name of the data/record type.
computeErasedConstructorArgs :: QName -> TCM ()
computeErasedConstructorArgs :: QName -> TCM ()
computeErasedConstructorArgs QName
d = do
  cs <- QName -> TCM [QName]
getNotErasedConstructors QName
d
  runE $ mapM_ getFunInfo cs

eraseTerms :: QName -> EvaluationStrategy -> TTerm -> TCM TTerm
eraseTerms :: QName -> EvaluationStrategy -> TTerm -> TCM TTerm
eraseTerms QName
q EvaluationStrategy
eval TTerm
t = QName -> TTerm -> TCM [ArgUsage]
usedArguments QName
q TTerm
t TCM [ArgUsage] -> TCM TTerm -> TCM TTerm
forall a b. TCMT IO a -> TCMT IO b -> TCMT IO b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> E TTerm -> TCM TTerm
forall a. E a -> TCM a
runE (QName -> TTerm -> E TTerm
eraseTop QName
q TTerm
t)
  where
    eraseTop :: QName -> TTerm -> E TTerm
eraseTop QName
q TTerm
t = do
      (_, h) <- QName -> StateT ESt (TCMT IO) FunInfo
getFunInfo QName
q
      case h of
        TypeInfo
Erasable -> TTerm -> E TTerm
forall a. a -> StateT ESt (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
TErased
        TypeInfo
Empty    -> TTerm -> E TTerm
forall a. a -> StateT ESt (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
TErased
        TypeInfo
_        -> TTerm -> E TTerm
erase TTerm
t

    erase :: TTerm -> E TTerm
erase TTerm
t = case TTerm -> (TTerm, [TTerm])
tAppView TTerm
t of

      (TCon QName
c, [TTerm]
vs) -> do
        (rs, h) <- QName -> StateT ESt (TCMT IO) FunInfo
getFunInfo QName
c
        when (length rs < length vs) __IMPOSSIBLE__
        case h of
          TypeInfo
Erasable -> TTerm -> E TTerm
forall a. a -> StateT ESt (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
TErased
          TypeInfo
Empty    -> TTerm -> E TTerm
forall a. a -> StateT ESt (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
TErased
          TypeInfo
_        -> TTerm -> [TTerm] -> TTerm
tApp (QName -> TTerm
TCon QName
c) ([TTerm] -> TTerm) -> StateT ESt (TCMT IO) [TTerm] -> E TTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TypeInfo -> TTerm -> E TTerm)
-> [TypeInfo] -> [TTerm] -> StateT ESt (TCMT IO) [TTerm]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM TypeInfo -> TTerm -> E TTerm
eraseRel [TypeInfo]
rs [TTerm]
vs

      (TDef QName
f, [TTerm]
vs) -> do
        (rs, h) <- QName -> StateT ESt (TCMT IO) FunInfo
getFunInfo QName
f
        case h of
          TypeInfo
Erasable -> TTerm -> E TTerm
forall a. a -> StateT ESt (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
TErased
          TypeInfo
Empty    -> TTerm -> E TTerm
forall a. a -> StateT ESt (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
TErased
          TypeInfo
_        -> TTerm -> [TTerm] -> TTerm
tApp (QName -> TTerm
TDef QName
f) ([TTerm] -> TTerm) -> StateT ESt (TCMT IO) [TTerm] -> E TTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TypeInfo -> TTerm -> E TTerm)
-> [TypeInfo] -> [TTerm] -> StateT ESt (TCMT IO) [TTerm]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM TypeInfo -> TTerm -> E TTerm
eraseRel ([TypeInfo]
rs [TypeInfo] -> [TypeInfo] -> [TypeInfo]
forall a. [a] -> [a] -> [a]
++ TypeInfo -> [TypeInfo]
forall a. a -> [a]
repeat TypeInfo
NotErasable) [TTerm]
vs

      (TTerm, [TTerm])
_ -> case TTerm
t of
        TVar{}         -> TTerm -> E TTerm
forall a. a -> StateT ESt (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
t
        TDef{}         -> TTerm -> E TTerm
forall a. a -> StateT ESt (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
t
        TPrim{}        -> TTerm -> E TTerm
forall a. a -> StateT ESt (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
t
        TLit{}         -> TTerm -> E TTerm
forall a. a -> StateT ESt (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
t
        TCon{}         -> TTerm -> E TTerm
forall a. a -> StateT ESt (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
t
        TApp TTerm
f [TTerm]
es      -> TTerm -> [TTerm] -> TTerm
tApp (TTerm -> [TTerm] -> TTerm)
-> E TTerm -> StateT ESt (TCMT IO) ([TTerm] -> TTerm)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> E TTerm
erase TTerm
f StateT ESt (TCMT IO) ([TTerm] -> TTerm)
-> StateT ESt (TCMT IO) [TTerm] -> E TTerm
forall a b.
StateT ESt (TCMT IO) (a -> b)
-> StateT ESt (TCMT IO) a -> StateT ESt (TCMT IO) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (TTerm -> E TTerm) -> [TTerm] -> StateT ESt (TCMT IO) [TTerm]
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 TTerm -> E TTerm
erase [TTerm]
es
        TLam TTerm
b         -> TTerm -> TTerm
tLam (TTerm -> TTerm) -> E TTerm -> E TTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> E TTerm
erase TTerm
b
        TLet TTerm
e TTerm
b       -> do
          e <- TTerm -> E TTerm
erase TTerm
e
          if isErased e
            then case b of
                   TCase Int
0 CaseInfo
_ TTerm
_ [TAlt]
_ -> TTerm -> TTerm -> TTerm
tLet TTerm
TErased (TTerm -> TTerm) -> E TTerm -> E TTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> E TTerm
erase TTerm
b
                   TTerm
_             -> TTerm -> E TTerm
erase (TTerm -> E TTerm) -> TTerm -> E TTerm
forall a b. (a -> b) -> a -> b
$ Int -> SubstArg TTerm -> TTerm -> TTerm
forall a. Subst a => Int -> SubstArg a -> a -> a
subst Int
0 TTerm
SubstArg TTerm
TErased TTerm
b
            else tLet e <$> erase b
        TCase Int
x CaseInfo
t TTerm
d [TAlt]
bs -> do
          (d, bs) <- Int -> Erased -> CaseType -> TTerm -> [TAlt] -> E (TTerm, [TAlt])
pruneUnreachable Int
x (CaseInfo -> Erased
caseErased CaseInfo
t) (CaseInfo -> CaseType
caseType CaseInfo
t) TTerm
d [TAlt]
bs
          d       <- erase d
          bs      <- mapM eraseAlt bs
          tCase x t d bs

        TTerm
TUnit          -> TTerm -> E TTerm
forall a. a -> StateT ESt (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
t
        TTerm
TSort          -> TTerm -> E TTerm
forall a. a -> StateT ESt (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
t
        TTerm
TErased        -> TTerm -> E TTerm
forall a. a -> StateT ESt (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
t
        TError{}       -> TTerm -> E TTerm
forall a. a -> StateT ESt (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
t
        TCoerce TTerm
e      -> TTerm -> TTerm
TCoerce (TTerm -> TTerm) -> E TTerm -> E TTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> E TTerm
erase TTerm
e

    -- #3380: this is not safe for strict backends
    tLam :: TTerm -> TTerm
tLam TTerm
TErased | EvaluationStrategy
eval EvaluationStrategy -> EvaluationStrategy -> Bool
forall a. Eq a => a -> a -> Bool
== EvaluationStrategy
LazyEvaluation = TTerm
TErased
    tLam TTerm
t                                = TTerm -> TTerm
TLam TTerm
t

    tLet :: TTerm -> TTerm -> TTerm
tLet TTerm
e TTerm
b
      | Int -> TTerm -> Bool
forall a. HasFree a => Int -> a -> Bool
freeIn Int
0 TTerm
b = TTerm -> TTerm -> TTerm
TLet TTerm
e TTerm
b
      | Bool
otherwise  = Impossible -> TTerm -> TTerm
forall a. Subst a => Impossible -> a -> a
strengthen Impossible
HasCallStack => Impossible
impossible TTerm
b

    tApp :: TTerm -> [TTerm] -> TTerm
tApp TTerm
f []                  = TTerm
f
    tApp TTerm
TErased [TTerm]
_             = TTerm
TErased
    tApp TTerm
f [TTerm]
_ | TTerm -> Bool
forall a. Unreachable a => a -> Bool
isUnreachable TTerm
f = TTerm
tUnreachable
    tApp TTerm
f [TTerm]
es                  = TTerm -> [TTerm] -> TTerm
mkTApp TTerm
f [TTerm]
es

    tCase :: Int -> CaseInfo -> TTerm -> [TAlt] -> E TTerm
tCase Int
x CaseInfo
t TTerm
d [TAlt]
bs
      | TTerm -> Bool
isErased TTerm
d Bool -> Bool -> Bool
&& (TAlt -> Bool) -> [TAlt] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (TTerm -> Bool
isErased (TTerm -> Bool) -> (TAlt -> TTerm) -> TAlt -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TAlt -> TTerm
aBody) [TAlt]
bs = TTerm -> E TTerm
forall a. a -> StateT ESt (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
TErased
      | Bool
otherwise = case [TAlt]
bs of
        [b :: TAlt
b@(TACon QName
c Int
_ TTerm
_)] -> do
          h <- FunInfo -> TypeInfo
forall a b. (a, b) -> b
snd (FunInfo -> TypeInfo)
-> StateT ESt (TCMT IO) FunInfo -> StateT ESt (TCMT IO) TypeInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> StateT ESt (TCMT IO) FunInfo
getFunInfo QName
c
          case h of
            TypeInfo
NotErasable -> E TTerm
fallback
            TypeInfo
Empty       -> TTerm -> E TTerm
forall a. a -> StateT ESt (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
TErased
            TypeInfo
Erasable    -> TAlt -> E TTerm
erasedBody TAlt
b
        [TAlt]
_ -> E TTerm
fallback
      where
        noerase :: E TTerm
noerase = TTerm -> E TTerm
forall a. a -> StateT ESt (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TTerm -> E TTerm) -> TTerm -> E TTerm
forall a b. (a -> b) -> a -> b
$ Int -> CaseInfo -> TTerm -> [TAlt] -> TTerm
TCase Int
x CaseInfo
t TTerm
d [TAlt]
bs

        erasedBody :: TAlt -> E TTerm
erasedBody = \case
          TACon QName
_ Int
arity TTerm
body ->
            (if Int
arity Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then TTerm -> E TTerm
forall a. a -> StateT ESt (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure else TTerm -> E TTerm
erase) (TTerm -> E TTerm) -> TTerm -> E TTerm
forall a b. (a -> b) -> a -> b
$
               -- might enable more erasure
            Substitution' (SubstArg TTerm) -> TTerm -> TTerm
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Int -> TTerm -> [TTerm]
forall a. Int -> a -> [a]
replicate Int
arity TTerm
TErased [TTerm] -> Substitution' TTerm -> Substitution' TTerm
forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# Substitution' TTerm
forall a. Substitution' a
idS) TTerm
body
          TALit Literal
_ TTerm
body   -> TTerm -> E TTerm
forall a. a -> StateT ESt (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
body
          TAGuard TTerm
_ TTerm
body -> TTerm -> E TTerm
forall a. a -> StateT ESt (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
body

        fallback :: E TTerm
fallback = case (CaseInfo -> Erased
caseErased CaseInfo
t, [TAlt]
bs) of
          (Erased{}, [TAlt
b]) ->
            -- The case variable is erased, and there is exactly one
            -- case: use the case's body.
            TAlt -> E TTerm
erasedBody TAlt
b
          (Erased{}, [])  ->
            -- The case variable is erased, and there is no case: use
            -- the default.
            TTerm -> E TTerm
forall a. a -> StateT ESt (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TTerm -> E TTerm) -> TTerm -> E TTerm
forall a b. (a -> b) -> a -> b
$ if TTerm -> Bool
isErased TTerm
d then TTerm
TErased else TTerm
d
          (Erased{}, TAlt
_ : TAlt
_ : [TAlt]
_) ->
            -- The case variable is erased, and there are at least two
            -- cases: crash.
            E TTerm
forall a. HasCallStack => a
__IMPOSSIBLE__
          (Erased, [TAlt])
_ ->
            -- The case variable is not erased: do not erase anything.
            E TTerm
noerase

    isErased :: TTerm -> Bool
isErased TTerm
t = TTerm
t TTerm -> TTerm -> Bool
forall a. Eq a => a -> a -> Bool
== TTerm
TErased Bool -> Bool -> Bool
|| TTerm -> Bool
forall a. Unreachable a => a -> Bool
isUnreachable TTerm
t

    eraseRel :: TypeInfo -> TTerm -> E TTerm
eraseRel TypeInfo
r TTerm
t | TypeInfo -> Bool
erasable TypeInfo
r = TTerm -> E TTerm
forall a. a -> StateT ESt (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
TErased
                 | Bool
otherwise  = TTerm -> E TTerm
erase TTerm
t

    eraseAlt :: TAlt -> StateT ESt (TCMT IO) TAlt
eraseAlt = \case
      TALit Literal
l TTerm
b   -> Literal -> TTerm -> TAlt
TALit Literal
l   (TTerm -> TAlt) -> E TTerm -> StateT ESt (TCMT IO) TAlt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> E TTerm
erase TTerm
b
      TACon QName
c Int
a TTerm
b -> do
        rs <- (TypeInfo -> Bool) -> [TypeInfo] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map TypeInfo -> Bool
erasable ([TypeInfo] -> [Bool])
-> (FunInfo -> [TypeInfo]) -> FunInfo -> [Bool]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FunInfo -> [TypeInfo]
forall a b. (a, b) -> a
fst (FunInfo -> [Bool])
-> StateT ESt (TCMT IO) FunInfo -> StateT ESt (TCMT IO) [Bool]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> StateT ESt (TCMT IO) FunInfo
getFunInfo QName
c
        let sub = (Bool -> Substitution' TTerm -> Substitution' TTerm)
-> Substitution' TTerm -> [Bool] -> Substitution' TTerm
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ Bool
e -> if Bool
e then (TTerm
TErased TTerm -> Substitution' TTerm -> Substitution' TTerm
forall a. a -> Substitution' a -> Substitution' a
:#) (Substitution' TTerm -> Substitution' TTerm)
-> (Substitution' TTerm -> Substitution' TTerm)
-> Substitution' TTerm
-> Substitution' TTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Substitution' TTerm -> Substitution' TTerm
forall a. Int -> Substitution' a -> Substitution' a
wkS Int
1 else Int -> Substitution' TTerm -> Substitution' TTerm
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
1) Substitution' TTerm
forall a. Substitution' a
idS ([Bool] -> Substitution' TTerm) -> [Bool] -> Substitution' TTerm
forall a b. (a -> b) -> a -> b
$ [Bool] -> [Bool]
forall a. [a] -> [a]
reverse [Bool]
rs
        TACon c a <$> erase (applySubst sub b)
      TAGuard TTerm
g TTerm
b -> TTerm -> TTerm -> TAlt
TAGuard   (TTerm -> TTerm -> TAlt)
-> E TTerm -> StateT ESt (TCMT IO) (TTerm -> TAlt)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> E TTerm
erase TTerm
g StateT ESt (TCMT IO) (TTerm -> TAlt)
-> E TTerm -> StateT ESt (TCMT IO) TAlt
forall a b.
StateT ESt (TCMT IO) (a -> b)
-> StateT ESt (TCMT IO) a -> StateT ESt (TCMT IO) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TTerm -> E TTerm
erase TTerm
b

pruneUnreachable ::
  Int -> Erased -> CaseType -> TTerm -> [TAlt] -> E (TTerm, [TAlt])
pruneUnreachable :: Int -> Erased -> CaseType -> TTerm -> [TAlt] -> E (TTerm, [TAlt])
pruneUnreachable Int
x Erased
erased CaseType
t TTerm
d [TAlt]
bs = case Erased
erased of
  NotErased{} -> Int -> Erased -> CaseType -> TTerm -> [TAlt] -> E (TTerm, [TAlt])
pruneUnreachable' Int
x Erased
erased CaseType
t TTerm
d [TAlt]
bs
  Erased{}    ->
    -- If the match is on an erased argument, then the first branch
    -- should match.
    case [TAlt]
bs of
      []    -> Int -> Erased -> CaseType -> TTerm -> [TAlt] -> E (TTerm, [TAlt])
pruneUnreachable' Int
x Erased
erased CaseType
t TTerm
d            []
      TAlt
b : [TAlt]
_ -> Int -> Erased -> CaseType -> TTerm -> [TAlt] -> E (TTerm, [TAlt])
pruneUnreachable' Int
x Erased
erased CaseType
t TTerm
tUnreachable [TAlt
b]

-- | Doesn't have any type information (other than the name of the data type),
--   so we can't do better than checking if all constructors are present.
pruneUnreachable' ::
  Int -> Erased -> CaseType -> TTerm -> [TAlt] -> E (TTerm, [TAlt])
pruneUnreachable' :: Int -> Erased -> CaseType -> TTerm -> [TAlt] -> E (TTerm, [TAlt])
pruneUnreachable' Int
_ Erased
erased (CTData QName
q) TTerm
d [TAlt]
bs' = do
  -- Erased constructors are pruned iff the match is made on a
  -- non-erased argument.
  cs <- TCM [QName] -> StateT ESt (TCMT IO) [QName]
forall (m :: * -> *) a. Monad m => m a -> StateT ESt m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM [QName] -> StateT ESt (TCMT IO) [QName])
-> TCM [QName] -> StateT ESt (TCMT IO) [QName]
forall a b. (a -> b) -> a -> b
$
        if Erased -> Bool
isErased Erased
erased
        then QName -> TCM [QName]
getConstructors QName
q
        else QName -> TCM [QName]
getNotErasedConstructors QName
q
  let bs | Erased -> Bool
isErased Erased
erased = [TAlt]
bs'
         | Bool
otherwise       =
           ((TAlt -> Bool) -> [TAlt] -> [TAlt])
-> [TAlt] -> (TAlt -> Bool) -> [TAlt]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (TAlt -> Bool) -> [TAlt] -> [TAlt]
forall a. (a -> Bool) -> [a] -> [a]
filter [TAlt]
bs' ((TAlt -> Bool) -> [TAlt]) -> (TAlt -> Bool) -> [TAlt]
forall a b. (a -> b) -> a -> b
$ \case
             a :: TAlt
a@TACon{} -> (TAlt -> QName
aCon TAlt
a) QName -> [QName] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [QName]
cs
             TAGuard{} -> Bool
True
             TALit{}   -> Bool
True
  let -- In the case of a match on an erased argument the value d is
      -- equal to tUnreachable, except perhaps if bs is empty. In the
      -- latter case complete is True exactly when the type has zero
      -- constructors (erased or not), in which case it makes sense to
      -- replace d with tUnreachable.
      complete = [QName] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [QName]
cs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [TAlt] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ TAlt
b | b :: TAlt
b@TACon{} <- [TAlt]
bs ]
      d' | Bool
complete  = TTerm
tUnreachable
         | Bool
otherwise = TTerm
d
  return (d', bs)
pruneUnreachable' Int
x Erased
_ CaseType
CTNat TTerm
d [TAlt]
bs =
  (TTerm, [TAlt]) -> E (TTerm, [TAlt])
forall a. a -> StateT ESt (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ((TTerm, [TAlt]) -> E (TTerm, [TAlt]))
-> (TTerm, [TAlt]) -> E (TTerm, [TAlt])
forall a b. (a -> b) -> a -> b
$ Int -> TTerm -> [TAlt] -> IntSet -> (TTerm, [TAlt])
pruneIntCase Int
x TTerm
d [TAlt]
bs (Integer -> IntSet
IntSet.below Integer
0)
pruneUnreachable' Int
x Erased
_ CaseType
CTInt TTerm
d [TAlt]
bs =
  (TTerm, [TAlt]) -> E (TTerm, [TAlt])
forall a. a -> StateT ESt (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ((TTerm, [TAlt]) -> E (TTerm, [TAlt]))
-> (TTerm, [TAlt]) -> E (TTerm, [TAlt])
forall a b. (a -> b) -> a -> b
$ Int -> TTerm -> [TAlt] -> IntSet -> (TTerm, [TAlt])
pruneIntCase Int
x TTerm
d [TAlt]
bs IntSet
IntSet.empty
pruneUnreachable' Int
_ Erased
_ CaseType
_ TTerm
d [TAlt]
bs =
  (TTerm, [TAlt]) -> E (TTerm, [TAlt])
forall a. a -> StateT ESt (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TTerm
d, [TAlt]
bs)

-- These are the guards we generate for Int/Nat pattern matching
pattern Below :: Int -> Integer -> TTerm
pattern $mBelow :: forall {r}. TTerm -> (Int -> Integer -> r) -> ((# #) -> r) -> r
$bBelow :: Int -> Integer -> TTerm
Below x n = TApp (TPrim PLt)  [TVar x, TLit (LitNat n)]

pattern Above :: Int -> Integer -> TTerm
pattern $mAbove :: forall {r}. TTerm -> (Int -> Integer -> r) -> ((# #) -> r) -> r
$bAbove :: Int -> Integer -> TTerm
Above x n = TApp (TPrim PGeq) [TVar x, TLit (LitNat n)]

-- | Strip unreachable clauses (replace by tUnreachable for the default).
--   Fourth argument is the set of ints covered so far.
pruneIntCase :: Int -> TTerm -> [TAlt] -> IntSet -> (TTerm, [TAlt])
pruneIntCase :: Int -> TTerm -> [TAlt] -> IntSet -> (TTerm, [TAlt])
pruneIntCase Int
x TTerm
d [TAlt]
bs IntSet
cover = [TAlt] -> IntSet -> (TTerm, [TAlt])
go [TAlt]
bs IntSet
cover
  where
    go :: [TAlt] -> IntSet -> (TTerm, [TAlt])
go [] IntSet
cover
      | IntSet
cover IntSet -> IntSet -> Bool
forall a. Eq a => a -> a -> Bool
== IntSet
IntSet.full = (TTerm
tUnreachable, [])
      | Bool
otherwise            = (TTerm
d, [])
    go (TAlt
b : [TAlt]
bs) IntSet
cover =
      case TAlt
b of
        TAGuard (Below Int
y Integer
n) TTerm
_ | Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
y -> IntSet -> (TTerm, [TAlt])
rec (Integer -> IntSet
IntSet.below Integer
n)
        TAGuard (Above Int
y Integer
n) TTerm
_ | Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
y -> IntSet -> (TTerm, [TAlt])
rec (Integer -> IntSet
IntSet.above Integer
n)
        TALit (LitNat Integer
n) TTerm
_             -> IntSet -> (TTerm, [TAlt])
rec (Integer -> IntSet
IntSet.singleton Integer
n)
        TAlt
_                                -> ([TAlt] -> [TAlt]) -> (TTerm, [TAlt]) -> (TTerm, [TAlt])
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (TAlt
b TAlt -> [TAlt] -> [TAlt]
forall a. a -> [a] -> [a]
:) ((TTerm, [TAlt]) -> (TTerm, [TAlt]))
-> (TTerm, [TAlt]) -> (TTerm, [TAlt])
forall a b. (a -> b) -> a -> b
$ [TAlt] -> IntSet -> (TTerm, [TAlt])
go [TAlt]
bs IntSet
cover
      where
        rec :: IntSet -> (TTerm, [TAlt])
rec IntSet
this = ([TAlt] -> [TAlt]) -> (TTerm, [TAlt]) -> (TTerm, [TAlt])
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second [TAlt] -> [TAlt]
addAlt ((TTerm, [TAlt]) -> (TTerm, [TAlt]))
-> (TTerm, [TAlt]) -> (TTerm, [TAlt])
forall a b. (a -> b) -> a -> b
$ [TAlt] -> IntSet -> (TTerm, [TAlt])
go [TAlt]
bs IntSet
cover'
          where
            this' :: IntSet
this'  = IntSet -> IntSet -> IntSet
IntSet.difference IntSet
this IntSet
cover
            cover' :: IntSet
cover' = IntSet
this' IntSet -> IntSet -> IntSet
forall a. Semigroup a => a -> a -> a
<> IntSet
cover
            addAlt :: [TAlt] -> [TAlt]
addAlt = case IntSet -> Maybe [Integer]
IntSet.toFiniteList IntSet
this' of
                       Just []  -> [TAlt] -> [TAlt]
forall a. a -> a
id                                     -- unreachable case
                       Just [Integer
n] -> (Literal -> TTerm -> TAlt
TALit (Integer -> Literal
LitNat Integer
n) (TAlt -> TTerm
aBody TAlt
b) TAlt -> [TAlt] -> [TAlt]
forall a. a -> [a] -> [a]
:) -- possibly refined case
                       Maybe [Integer]
_        -> (TAlt
b TAlt -> [TAlt] -> [TAlt]
forall a. a -> [a] -> [a]
:)                                  -- unchanged case

data TypeInfo = Empty | Erasable | NotErasable
  deriving (TypeInfo -> TypeInfo -> Bool
(TypeInfo -> TypeInfo -> Bool)
-> (TypeInfo -> TypeInfo -> Bool) -> Eq TypeInfo
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TypeInfo -> TypeInfo -> Bool
== :: TypeInfo -> TypeInfo -> Bool
$c/= :: TypeInfo -> TypeInfo -> Bool
/= :: TypeInfo -> TypeInfo -> Bool
Eq, Int -> TypeInfo -> ShowS
[TypeInfo] -> ShowS
TypeInfo -> ArgName
(Int -> TypeInfo -> ShowS)
-> (TypeInfo -> ArgName) -> ([TypeInfo] -> ShowS) -> Show TypeInfo
forall a.
(Int -> a -> ShowS) -> (a -> ArgName) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TypeInfo -> ShowS
showsPrec :: Int -> TypeInfo -> ShowS
$cshow :: TypeInfo -> ArgName
show :: TypeInfo -> ArgName
$cshowList :: [TypeInfo] -> ShowS
showList :: [TypeInfo] -> ShowS
Show)

sumTypeInfo :: [TypeInfo] -> TypeInfo
sumTypeInfo :: [TypeInfo] -> TypeInfo
sumTypeInfo [TypeInfo]
is = (TypeInfo -> TypeInfo -> TypeInfo)
-> TypeInfo -> [TypeInfo] -> TypeInfo
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TypeInfo -> TypeInfo -> TypeInfo
plus TypeInfo
Empty [TypeInfo]
is
  where
    plus :: TypeInfo -> TypeInfo -> TypeInfo
plus TypeInfo
Empty       TypeInfo
r           = TypeInfo
r
    plus TypeInfo
r           TypeInfo
Empty       = TypeInfo
r
    plus TypeInfo
Erasable    TypeInfo
r           = TypeInfo
r
    plus TypeInfo
r           TypeInfo
Erasable    = TypeInfo
r
    plus TypeInfo
NotErasable TypeInfo
NotErasable = TypeInfo
NotErasable

erasable :: TypeInfo -> Bool
erasable :: TypeInfo -> Bool
erasable TypeInfo
Erasable    = Bool
True
erasable TypeInfo
Empty       = Bool
True
erasable TypeInfo
NotErasable = Bool
False

type FunInfo = ([TypeInfo], TypeInfo)

getFunInfo :: QName -> E FunInfo
getFunInfo :: QName -> StateT ESt (TCMT IO) FunInfo
getFunInfo QName
q = Lens' ESt (Maybe FunInfo)
-> StateT ESt (TCMT IO) FunInfo -> StateT ESt (TCMT IO) FunInfo
forall s (m :: * -> *) a.
MonadState s m =>
Lens' s (Maybe a) -> m a -> m a
memo ((Map QName FunInfo -> f (Map QName FunInfo)) -> ESt -> f ESt
Lens' ESt (Map QName FunInfo)
funMap ((Map QName FunInfo -> f (Map QName FunInfo)) -> ESt -> f ESt)
-> ((Maybe FunInfo -> f (Maybe FunInfo))
    -> Map QName FunInfo -> f (Map QName FunInfo))
-> (Maybe FunInfo -> f (Maybe FunInfo))
-> ESt
-> f ESt
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Lens' (Map QName FunInfo) (Maybe FunInfo)
forall k v. Ord k => k -> Lens' (Map k v) (Maybe v)
key QName
q) (StateT ESt (TCMT IO) FunInfo -> StateT ESt (TCMT IO) FunInfo)
-> StateT ESt (TCMT IO) FunInfo -> StateT ESt (TCMT IO) FunInfo
forall a b. (a -> b) -> a -> b
$ QName -> StateT ESt (TCMT IO) FunInfo
getInfo QName
q
  where
    getInfo :: QName -> E FunInfo
    getInfo :: QName -> StateT ESt (TCMT IO) FunInfo
getInfo QName
q = do
      (rs, t) <- do
        (tel, t) <- TCMT IO (ListTel, Type) -> StateT ESt (TCMT IO) (ListTel, Type)
forall (m :: * -> *) a. Monad m => m a -> StateT ESt m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO (ListTel, Type) -> StateT ESt (TCMT IO) (ListTel, Type))
-> TCMT IO (ListTel, Type) -> StateT ESt (TCMT IO) (ListTel, Type)
forall a b. (a -> b) -> a -> b
$ QName -> TCMT IO (ListTel, Type)
typeWithoutParams QName
q
        is     <- mapM (getTypeInfo . snd . dget) tel
        used   <- lift $ (++ repeat ArgUsed) . fromMaybe [] <$> getCompiledArgUse q
        forced <- lift $ (++ repeat NotForced) <$> getForcedArgs q
        return (zipWith3 (uncurry . mkR . getModality) tel (zip forced used) is, t)
      h <- if isAbsurdLambdaName q then pure Erasable else getTypeInfo t
      lift $ reportSLn "treeless.opt.erase.info" 50 $ "type info for " ++ prettyShow q ++ ": " ++ show rs ++ " -> " ++ show h
      lift $ setErasedConArgs q $ map erasable rs
      return (rs, h)

    -- Treat empty, erasable, or unused arguments as Erasable
    mkR :: Modality -> IsForced -> ArgUsage -> TypeInfo -> TypeInfo
    mkR :: Modality -> IsForced -> ArgUsage -> TypeInfo -> TypeInfo
mkR Modality
m IsForced
f ArgUsage
u TypeInfo
i
      | Bool -> Bool
not (Modality -> Bool
forall a. LensModality a => a -> Bool
usableModality Modality
m) = TypeInfo
Erasable
      | ArgUsage
ArgUnused <- ArgUsage
u         = TypeInfo
Erasable
      | IsForced
Forced <- IsForced
f            = TypeInfo
Erasable
      | Bool
otherwise              = TypeInfo
i

isErasable :: QName -> TCM Bool
isErasable :: QName -> TCM Bool
isErasable QName
qn =
  TypeInfo -> Bool
erasable (TypeInfo -> Bool) -> (FunInfo -> TypeInfo) -> FunInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FunInfo -> TypeInfo
forall a b. (a, b) -> b
snd (FunInfo -> Bool) -> TCMT IO FunInfo -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ESt (TCMT IO) FunInfo -> TCMT IO FunInfo
forall a. E a -> TCM a
runE (QName -> StateT ESt (TCMT IO) FunInfo
getFunInfo QName
qn)

telListView :: Type -> TCM (ListTel, Type)
telListView :: Type -> TCMT IO (ListTel, Type)
telListView Type
t = do
  TelV tel t <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
telViewPath Type
t
  return (telToList tel, t)

typeWithoutParams :: QName -> TCM (ListTel, Type)
typeWithoutParams :: QName -> TCMT IO (ListTel, Type)
typeWithoutParams QName
q = do
  def <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
  let d = case Definition -> Defn
I.theDef Definition
def of
        Function{ funProjection :: Defn -> Either ProjectionLikenessMissing Projection
funProjection = Right Projection{ projIndex :: Projection -> Int
projIndex = Int
i } } -> Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
        Constructor{ conPars :: Defn -> Int
conPars = Int
n } -> Int
n
        Defn
_                          -> Int
0
  first (drop d) <$> telListView (defType def)

getTypeInfo :: Type -> E TypeInfo
getTypeInfo :: Type -> StateT ESt (TCMT IO) TypeInfo
getTypeInfo Type
t0 = do
  (tel, t) <- TCMT IO (ListTel, Type) -> StateT ESt (TCMT IO) (ListTel, Type)
forall (m :: * -> *) a. Monad m => m a -> StateT ESt m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO (ListTel, Type) -> StateT ESt (TCMT IO) (ListTel, Type))
-> TCMT IO (ListTel, Type) -> StateT ESt (TCMT IO) (ListTel, Type)
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO (ListTel, Type)
telListView Type
t0
  et <- case I.unEl t of
    I.Def QName
d Elims
_ -> do
      -- #2916: Only update the memo table for d. Results for other types are
      -- under the assumption that d is erasable!
      oldMap <- Lens' ESt (Map QName TypeInfo)
-> StateT ESt (TCMT IO) (Map QName TypeInfo)
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> m i
use (Map QName TypeInfo -> f (Map QName TypeInfo)) -> ESt -> f ESt
Lens' ESt (Map QName TypeInfo)
typeMap
      dInfo <- typeInfo d
      typeMap .= Map.insert d dInfo oldMap
      return dInfo
    Sort{}    -> TypeInfo -> StateT ESt (TCMT IO) TypeInfo
forall a. a -> StateT ESt (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return TypeInfo
Erasable
    Term
_         -> TypeInfo -> StateT ESt (TCMT IO) TypeInfo
forall a. a -> StateT ESt (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return TypeInfo
NotErasable
  is <- mapM (getTypeInfo . snd . dget) tel
  let e | TypeInfo
Empty TypeInfo -> [TypeInfo] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TypeInfo]
is = TypeInfo
Erasable
        | [TypeInfo] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeInfo]
is         = TypeInfo
et        -- TODO: guard should really be "all inhabited is"
        | TypeInfo
et TypeInfo -> TypeInfo -> Bool
forall a. Eq a => a -> a -> Bool
== TypeInfo
Empty     = TypeInfo
Erasable
        | Bool
otherwise       = TypeInfo
et
  lift $ reportSDoc "treeless.opt.erase.type" 50 $ prettyTCM t0 <+> text ("is " ++ show e)
  return e
  where
  typeInfo :: QName -> E TypeInfo
  typeInfo :: QName -> StateT ESt (TCMT IO) TypeInfo
typeInfo QName
q = StateT ESt (TCMT IO) Bool
-> StateT ESt (TCMT IO) TypeInfo
-> StateT ESt (TCMT IO) TypeInfo
-> StateT ESt (TCMT IO) TypeInfo
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (QName -> StateT ESt (TCMT IO) Bool
erasureForbidden QName
q) (TypeInfo -> StateT ESt (TCMT IO) TypeInfo
forall a. a -> StateT ESt (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return TypeInfo
NotErasable) (StateT ESt (TCMT IO) TypeInfo -> StateT ESt (TCMT IO) TypeInfo)
-> StateT ESt (TCMT IO) TypeInfo -> StateT ESt (TCMT IO) TypeInfo
forall a b. (a -> b) -> a -> b
$ {-else-} do
    Lens' ESt (Maybe TypeInfo)
-> TypeInfo
-> StateT ESt (TCMT IO) TypeInfo
-> StateT ESt (TCMT IO) TypeInfo
forall s (m :: * -> *) a.
MonadState s m =>
Lens' s (Maybe a) -> a -> m a -> m a
memoRec ((Map QName TypeInfo -> f (Map QName TypeInfo)) -> ESt -> f ESt
Lens' ESt (Map QName TypeInfo)
typeMap ((Map QName TypeInfo -> f (Map QName TypeInfo)) -> ESt -> f ESt)
-> ((Maybe TypeInfo -> f (Maybe TypeInfo))
    -> Map QName TypeInfo -> f (Map QName TypeInfo))
-> (Maybe TypeInfo -> f (Maybe TypeInfo))
-> ESt
-> f ESt
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Lens' (Map QName TypeInfo) (Maybe TypeInfo)
forall k v. Ord k => k -> Lens' (Map k v) (Maybe v)
key QName
q) TypeInfo
Erasable (StateT ESt (TCMT IO) TypeInfo -> StateT ESt (TCMT IO) TypeInfo)
-> StateT ESt (TCMT IO) TypeInfo -> StateT ESt (TCMT IO) TypeInfo
forall a b. (a -> b) -> a -> b
$ do  -- assume recursive occurrences are erasable
      mId    <- TCM (Maybe QName) -> StateT ESt (TCMT IO) (Maybe QName)
forall (m :: * -> *) a. Monad m => m a -> StateT ESt m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (Maybe QName) -> StateT ESt (TCMT IO) (Maybe QName))
-> TCM (Maybe QName) -> StateT ESt (TCMT IO) (Maybe QName)
forall a b. (a -> b) -> a -> b
$ BuiltinId -> TCM (Maybe QName)
forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
a -> m (Maybe QName)
getName' BuiltinId
builtinId
      msizes <- lift $ mapM getBuiltinName
                         [builtinSize, builtinSizeLt]
      def    <- lift $ getConstInfo q
      let mcs = case Definition -> Defn
I.theDef Definition
def of
                  I.Datatype{ dataCons :: Defn -> [QName]
dataCons = [QName]
cs } -> [QName] -> Maybe [QName]
forall a. a -> Maybe a
Just [QName]
cs
                  I.Record{ recConHead :: Defn -> ConHead
recConHead = ConHead
c }  -> [QName] -> Maybe [QName]
forall a. a -> Maybe a
Just [ConHead -> QName
conName ConHead
c]
                  Defn
_                           -> Maybe [QName]
forall a. Maybe a
Nothing
      case mcs of
        Maybe [QName]
_ | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
mId        -> TypeInfo -> StateT ESt (TCMT IO) TypeInfo
forall a. a -> StateT ESt (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return TypeInfo
NotErasable
        Maybe [QName]
_ | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q 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]
msizes -> TypeInfo -> StateT ESt (TCMT IO) TypeInfo
forall a. a -> StateT ESt (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return TypeInfo
Erasable
        Just [QName
c] -> do
          (ts, _) <- TCMT IO (ListTel, Type) -> StateT ESt (TCMT IO) (ListTel, Type)
forall (m :: * -> *) a. Monad m => m a -> StateT ESt m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO (ListTel, Type) -> StateT ESt (TCMT IO) (ListTel, Type))
-> TCMT IO (ListTel, Type) -> StateT ESt (TCMT IO) (ListTel, Type)
forall a b. (a -> b) -> a -> b
$ QName -> TCMT IO (ListTel, Type)
typeWithoutParams QName
c
          let rs = (Dom (ArgName, Type) -> Modality) -> ListTel -> [Modality]
forall a b. (a -> b) -> [a] -> [b]
map Dom (ArgName, Type) -> Modality
forall a. LensModality a => a -> Modality
getModality ListTel
ts
          is <- mapM (getTypeInfo . snd . dget) ts
          let er = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [ TypeInfo -> Bool
erasable TypeInfo
i Bool -> Bool -> Bool
|| Bool -> Bool
not (Modality -> Bool
forall a. LensModality a => a -> Bool
usableModality Modality
r) | (TypeInfo
i, Modality
r) <- [TypeInfo] -> [Modality] -> [(TypeInfo, Modality)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TypeInfo]
is [Modality]
rs ]
          return $ if er then Erasable else NotErasable
        Just []      -> TypeInfo -> StateT ESt (TCMT IO) TypeInfo
forall a. a -> StateT ESt (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return TypeInfo
Empty
        Just (QName
_:QName
_:[QName]
_) -> TypeInfo -> StateT ESt (TCMT IO) TypeInfo
forall a. a -> StateT ESt (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return TypeInfo
NotErasable
        Maybe [QName]
Nothing ->
          case Definition -> Defn
I.theDef Definition
def of
            I.Function{ funClauses :: Defn -> [Clause]
funClauses = [Clause]
cs } ->
              [TypeInfo] -> TypeInfo
sumTypeInfo ([TypeInfo] -> TypeInfo)
-> StateT ESt (TCMT IO) [TypeInfo] -> StateT ESt (TCMT IO) TypeInfo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Clause -> StateT ESt (TCMT IO) TypeInfo)
-> [Clause] -> StateT ESt (TCMT IO) [TypeInfo]
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 (StateT ESt (TCMT IO) TypeInfo
-> (Term -> StateT ESt (TCMT IO) TypeInfo)
-> Maybe Term
-> StateT ESt (TCMT IO) TypeInfo
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (TypeInfo -> StateT ESt (TCMT IO) TypeInfo
forall a. a -> StateT ESt (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return TypeInfo
Empty) (Type -> StateT ESt (TCMT IO) TypeInfo
getTypeInfo (Type -> StateT ESt (TCMT IO) TypeInfo)
-> (Term -> Type) -> Term -> StateT ESt (TCMT IO) TypeInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
HasCallStack => Sort' Term
__DUMMY_SORT__) (Maybe Term -> StateT ESt (TCMT IO) TypeInfo)
-> (Clause -> Maybe Term)
-> Clause
-> StateT ESt (TCMT IO) TypeInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Maybe Term
clauseBody) [Clause]
cs
            Defn
_ -> TypeInfo -> StateT ESt (TCMT IO) TypeInfo
forall a. a -> StateT ESt (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return TypeInfo
NotErasable
  -- The backend also has a say whether a type is eraseable or not.
  erasureForbidden :: QName -> E Bool
  erasureForbidden :: QName -> StateT ESt (TCMT IO) Bool
erasureForbidden QName
q = TCM Bool -> StateT ESt (TCMT IO) Bool
forall (m :: * -> *) a. Monad m => m a -> StateT ESt m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM Bool -> StateT ESt (TCMT IO) Bool)
-> TCM Bool -> StateT ESt (TCMT IO) Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> TCM Bool -> TCM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCM Bool
activeBackendMayEraseType QName
q