{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE PatternSynonyms #-}

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

import Control.Arrow (first, second)
import Control.Monad
import Control.Monad.State
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 {-# SOURCE #-} Agda.Compiler.Backend
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 =
  -- The active backend should be set
  TCMT IO (Maybe ArgName)
-> TCM Bool -> (ArgName -> TCM Bool) -> TCM Bool
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Lens' TCEnv (Maybe ArgName) -> TCMT IO (Maybe ArgName)
forall (m :: * -> *) a. MonadTCEnv m => Lens' TCEnv a -> m a
viewTC (Maybe ArgName -> f (Maybe ArgName)) -> TCEnv -> f TCEnv
Lens' TCEnv (Maybe ArgName)
eActiveBackendName) TCM Bool
forall a. HasCallStack => a
__IMPOSSIBLE__ ((ArgName -> TCM Bool) -> TCM Bool)
-> (ArgName -> TCM Bool) -> TCM Bool
forall a b. (a -> b) -> a -> b
$ \ ArgName
bname ->
  -- However it may not be part of the set of available backends
  -- in which case we default to not erasable to avoid false negatives.
  TCMT IO (Maybe Backend)
-> TCM Bool -> (Backend -> TCM Bool) -> TCM Bool
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (ArgName -> TCMT IO (Maybe Backend)
lookupBackend ArgName
bname)       (Bool -> TCM Bool
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False)   ((Backend -> TCM Bool) -> TCM Bool)
-> (Backend -> TCM Bool) -> TCM Bool
forall a b. (a -> b) -> a -> b
$ \ Backend
_ ->
  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