{-# 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
  [QName]
cs <- QName -> TCM [QName]
getNotErasedConstructors QName
d
  E () -> TCM ()
forall a. E a -> TCM a
runE (E () -> TCM ()) -> E () -> TCM ()
forall a b. (a -> b) -> a -> b
$ (QName -> StateT ESt (TCMT IO) FunInfo) -> [QName] -> E ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ QName -> StateT ESt (TCMT IO) FunInfo
getFunInfo [QName]
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
      ([TypeInfo]
_, TypeInfo
h) <- QName -> StateT ESt (TCMT IO) FunInfo
getFunInfo QName
q
      case TypeInfo
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
        ([TypeInfo]
rs, TypeInfo
h) <- QName -> StateT ESt (TCMT IO) FunInfo
getFunInfo QName
c
        Bool -> E () -> E ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
when ([TypeInfo] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeInfo]
rs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [TTerm] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TTerm]
vs) E ()
forall a. HasCallStack => a
__IMPOSSIBLE__
        case TypeInfo
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
        ([TypeInfo]
rs, TypeInfo
h) <- QName -> StateT ESt (TCMT IO) FunInfo
getFunInfo QName
f
        case TypeInfo
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
          TTerm
e <- TTerm -> E TTerm
erase TTerm
e
          if TTerm -> Bool
isErased TTerm
e
            then case TTerm
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 TTerm -> TTerm -> TTerm
tLet TTerm
e (TTerm -> TTerm) -> E TTerm -> E TTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> E TTerm
erase TTerm
b
        TCase Int
x CaseInfo
t TTerm
d [TAlt]
bs -> do
          (TTerm
d, [TAlt]
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
          TTerm
d       <- TTerm -> E TTerm
erase TTerm
d
          [TAlt]
bs      <- (TAlt -> StateT ESt (TCMT IO) TAlt)
-> [TAlt] -> StateT ESt (TCMT IO) [TAlt]
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 TAlt -> StateT ESt (TCMT IO) TAlt
eraseAlt [TAlt]
bs
          Int -> CaseInfo -> TTerm -> [TAlt] -> E TTerm
tCase Int
x CaseInfo
t TTerm
d [TAlt]
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
          TypeInfo
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 TypeInfo
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
        [Bool]
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 :: Substitution' TTerm
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
        QName -> Int -> TTerm -> TAlt
TACon QName
c Int
a (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 (Substitution' (SubstArg TTerm) -> TTerm -> TTerm
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' TTerm
Substitution' (SubstArg TTerm)
sub TTerm
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.
  [QName]
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 :: [TAlt]
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 :: Bool
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' :: TTerm
d' | Bool
complete  = TTerm
tUnreachable
         | Bool
otherwise = TTerm
d
  (TTerm, [TAlt]) -> E (TTerm, [TAlt])
forall a. a -> StateT ESt (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TTerm
d', [TAlt]
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
      ([TypeInfo]
rs, Type
t) <- do
        (ListTel
tel, Type
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
        [TypeInfo]
is     <- (Dom (ArgName, Type) -> StateT ESt (TCMT IO) TypeInfo)
-> ListTel -> 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 (Type -> StateT ESt (TCMT IO) TypeInfo
getTypeInfo (Type -> StateT ESt (TCMT IO) TypeInfo)
-> (Dom (ArgName, Type) -> Type)
-> Dom (ArgName, Type)
-> StateT ESt (TCMT IO) TypeInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ArgName, Type) -> Type
forall a b. (a, b) -> b
snd ((ArgName, Type) -> Type)
-> (Dom (ArgName, Type) -> (ArgName, Type))
-> Dom (ArgName, Type)
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (ArgName, Type) -> (ArgName, Type)
forall (t :: * -> *) a. Decoration t => t a -> a
dget) ListTel
tel
        [ArgUsage]
used   <- TCM [ArgUsage] -> StateT ESt (TCMT IO) [ArgUsage]
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 [ArgUsage] -> StateT ESt (TCMT IO) [ArgUsage])
-> TCM [ArgUsage] -> StateT ESt (TCMT IO) [ArgUsage]
forall a b. (a -> b) -> a -> b
$ ([ArgUsage] -> [ArgUsage] -> [ArgUsage]
forall a. [a] -> [a] -> [a]
++ ArgUsage -> [ArgUsage]
forall a. a -> [a]
repeat ArgUsage
ArgUsed) ([ArgUsage] -> [ArgUsage])
-> (Maybe [ArgUsage] -> [ArgUsage])
-> Maybe [ArgUsage]
-> [ArgUsage]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [ArgUsage] -> Maybe [ArgUsage] -> [ArgUsage]
forall a. a -> Maybe a -> a
fromMaybe [] (Maybe [ArgUsage] -> [ArgUsage])
-> TCMT IO (Maybe [ArgUsage]) -> TCM [ArgUsage]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO (Maybe [ArgUsage])
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe [ArgUsage])
getCompiledArgUse QName
q
        [IsForced]
forced <- TCM [IsForced] -> StateT ESt (TCMT IO) [IsForced]
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 [IsForced] -> StateT ESt (TCMT IO) [IsForced])
-> TCM [IsForced] -> StateT ESt (TCMT IO) [IsForced]
forall a b. (a -> b) -> a -> b
$ ([IsForced] -> [IsForced] -> [IsForced]
forall a. [a] -> [a] -> [a]
++ IsForced -> [IsForced]
forall a. a -> [a]
repeat IsForced
NotForced) ([IsForced] -> [IsForced]) -> TCM [IsForced] -> TCM [IsForced]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCM [IsForced]
forall (m :: * -> *). HasConstInfo m => QName -> m [IsForced]
getForcedArgs QName
q
        ([TypeInfo], Type) -> StateT ESt (TCMT IO) ([TypeInfo], Type)
forall a. a -> StateT ESt (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Dom (ArgName, Type)
 -> (IsForced, ArgUsage) -> TypeInfo -> TypeInfo)
-> ListTel -> [(IsForced, ArgUsage)] -> [TypeInfo] -> [TypeInfo]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 ((IsForced -> ArgUsage -> TypeInfo -> TypeInfo)
-> (IsForced, ArgUsage) -> TypeInfo -> TypeInfo
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((IsForced -> ArgUsage -> TypeInfo -> TypeInfo)
 -> (IsForced, ArgUsage) -> TypeInfo -> TypeInfo)
-> (Dom (ArgName, Type)
    -> IsForced -> ArgUsage -> TypeInfo -> TypeInfo)
-> Dom (ArgName, Type)
-> (IsForced, ArgUsage)
-> TypeInfo
-> TypeInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Modality -> IsForced -> ArgUsage -> TypeInfo -> TypeInfo
mkR (Modality -> IsForced -> ArgUsage -> TypeInfo -> TypeInfo)
-> (Dom (ArgName, Type) -> Modality)
-> Dom (ArgName, Type)
-> IsForced
-> ArgUsage
-> TypeInfo
-> TypeInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (ArgName, Type) -> Modality
forall a. LensModality a => a -> Modality
getModality) ListTel
tel ([IsForced] -> [ArgUsage] -> [(IsForced, ArgUsage)]
forall a b. [a] -> [b] -> [(a, b)]
zip [IsForced]
forced [ArgUsage]
used) [TypeInfo]
is, Type
t)
      TypeInfo
h <- if QName -> Bool
isAbsurdLambdaName QName
q then TypeInfo -> StateT ESt (TCMT IO) TypeInfo
forall a. a -> StateT ESt (TCMT IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeInfo
Erasable else Type -> StateT ESt (TCMT IO) TypeInfo
getTypeInfo Type
t
      TCM () -> E ()
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 () -> E ()) -> TCM () -> E ()
forall a b. (a -> b) -> a -> b
$ ArgName -> Int -> ArgName -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"treeless.opt.erase.info" Int
50 (ArgName -> TCM ()) -> ArgName -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgName
"type info for " ArgName -> ShowS
forall a. [a] -> [a] -> [a]
++ QName -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow QName
q ArgName -> ShowS
forall a. [a] -> [a] -> [a]
++ ArgName
": " ArgName -> ShowS
forall a. [a] -> [a] -> [a]
++ [TypeInfo] -> ArgName
forall a. Show a => a -> ArgName
show [TypeInfo]
rs ArgName -> ShowS
forall a. [a] -> [a] -> [a]
++ ArgName
" -> " ArgName -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeInfo -> ArgName
forall a. Show a => a -> ArgName
show TypeInfo
h
      TCM () -> E ()
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 () -> E ()) -> TCM () -> E ()
forall a b. (a -> b) -> a -> b
$ QName -> [Bool] -> TCM ()
setErasedConArgs QName
q ([Bool] -> TCM ()) -> [Bool] -> TCM ()
forall a b. (a -> b) -> a -> b
$ (TypeInfo -> Bool) -> [TypeInfo] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map TypeInfo -> Bool
erasable [TypeInfo]
rs
      FunInfo -> StateT ESt (TCMT IO) FunInfo
forall a. a -> StateT ESt (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return ([TypeInfo]
rs, TypeInfo
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 Tele (Dom Type)
tel Type
t <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
telViewPath Type
t
  (ListTel, Type) -> TCMT IO (ListTel, Type)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Tele (Dom Type) -> ListTel
forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom Type)
tel, Type
t)

typeWithoutParams :: QName -> TCM (ListTel, Type)
typeWithoutParams :: QName -> TCMT IO (ListTel, Type)
typeWithoutParams QName
q = do
  Definition
def <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
  let d :: Int
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
  (ListTel -> ListTel) -> (ListTel, Type) -> (ListTel, Type)
forall b c d. (b -> c) -> (b, d) -> (c, d)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (Int -> ListTel -> ListTel
forall a. Int -> [a] -> [a]
drop Int
d) ((ListTel, Type) -> (ListTel, Type))
-> TCMT IO (ListTel, Type) -> TCMT IO (ListTel, Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCMT IO (ListTel, Type)
telListView (Definition -> Type
defType Definition
def)

getTypeInfo :: Type -> E TypeInfo
getTypeInfo :: Type -> StateT ESt (TCMT IO) TypeInfo
getTypeInfo Type
t0 = do
  (ListTel
tel, Type
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
  TypeInfo
et <- case Type -> Term
forall t a. Type'' t a -> a
I.unEl Type
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!
      Map QName TypeInfo
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
      TypeInfo
dInfo <- QName -> StateT ESt (TCMT IO) TypeInfo
typeInfo QName
d
      (Map QName TypeInfo -> f (Map QName TypeInfo)) -> ESt -> f ESt
Lens' ESt (Map QName TypeInfo)
typeMap Lens' ESt (Map QName TypeInfo) -> Map QName TypeInfo -> E ()
forall o (m :: * -> *) i. MonadState o m => Lens' o i -> i -> m ()
.= QName -> TypeInfo -> Map QName TypeInfo -> Map QName TypeInfo
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert QName
d TypeInfo
dInfo Map QName TypeInfo
oldMap
      TypeInfo -> StateT ESt (TCMT IO) TypeInfo
forall a. a -> StateT ESt (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return TypeInfo
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
  [TypeInfo]
is <- (Dom (ArgName, Type) -> StateT ESt (TCMT IO) TypeInfo)
-> ListTel -> 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 (Type -> StateT ESt (TCMT IO) TypeInfo
getTypeInfo (Type -> StateT ESt (TCMT IO) TypeInfo)
-> (Dom (ArgName, Type) -> Type)
-> Dom (ArgName, Type)
-> StateT ESt (TCMT IO) TypeInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ArgName, Type) -> Type
forall a b. (a, b) -> b
snd ((ArgName, Type) -> Type)
-> (Dom (ArgName, Type) -> (ArgName, Type))
-> Dom (ArgName, Type)
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (ArgName, Type) -> (ArgName, Type)
forall (t :: * -> *) a. Decoration t => t a -> a
dget) ListTel
tel
  let e :: TypeInfo
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
  TCM () -> E ()
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 () -> E ()) -> TCM () -> E ()
forall a b. (a -> b) -> a -> b
$ ArgName -> Int -> TCMT IO Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"treeless.opt.erase.type" Int
50 (TCMT IO Doc -> TCM ()) -> TCMT IO Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ Type -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => Type -> m Doc
prettyTCM Type
t0 TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> ArgName -> TCMT IO Doc
forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName
"is " ArgName -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeInfo -> ArgName
forall a. Show a => a -> ArgName
show TypeInfo
e)
  TypeInfo -> StateT ESt (TCMT IO) TypeInfo
forall a. a -> StateT ESt (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return TypeInfo
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
      [Maybe QName]
msizes <- 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 -> TCMT IO (Maybe QName))
-> [BuiltinId] -> TCM [Maybe 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 BuiltinId -> TCMT IO (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
BuiltinId -> m (Maybe QName)
getBuiltinName
                         [BuiltinId
builtinSize, BuiltinId
builtinSizeLt]
      Definition
def    <- TCMT IO Definition -> StateT ESt (TCMT IO) Definition
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 Definition -> StateT ESt (TCMT IO) Definition)
-> TCMT IO Definition -> StateT ESt (TCMT IO) Definition
forall a b. (a -> b) -> a -> b
$ QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
      let mcs :: Maybe [QName]
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 Maybe [QName]
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
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
          (ListTel
ts, Type
_) <- 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 :: [Modality]
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
          [TypeInfo]
is <- (Dom (ArgName, Type) -> StateT ESt (TCMT IO) TypeInfo)
-> ListTel -> 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 (Type -> StateT ESt (TCMT IO) TypeInfo
getTypeInfo (Type -> StateT ESt (TCMT IO) TypeInfo)
-> (Dom (ArgName, Type) -> Type)
-> Dom (ArgName, Type)
-> StateT ESt (TCMT IO) TypeInfo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ArgName, Type) -> Type
forall a b. (a, b) -> b
snd ((ArgName, Type) -> Type)
-> (Dom (ArgName, Type) -> (ArgName, Type))
-> Dom (ArgName, Type)
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (ArgName, Type) -> (ArgName, Type)
forall (t :: * -> *) a. Decoration t => t a -> a
dget) ListTel
ts
          let er :: Bool
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 ]
          TypeInfo -> StateT ESt (TCMT IO) TypeInfo
forall a. a -> StateT ESt (TCMT IO) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TypeInfo -> StateT ESt (TCMT IO) TypeInfo)
-> TypeInfo -> StateT ESt (TCMT IO) TypeInfo
forall a b. (a -> b) -> a -> b
$ if Bool
er then TypeInfo
Erasable else TypeInfo
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