{-# 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 qualified Data.List as List

import Agda.Syntax.Common
import Agda.Syntax.Internal as I
import Agda.Syntax.Position
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.Utils.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' (Map QName FunInfo) ESt
funMap :: Lens' (Map QName FunInfo) ESt
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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ Map QName FunInfo
a -> ESt
r { _funMap :: Map QName FunInfo
_funMap = Map QName FunInfo
a }

typeMap :: Lens' (Map QName TypeInfo) ESt
typeMap :: Lens' (Map QName TypeInfo) ESt
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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ Map QName TypeInfo
a -> ESt
r { _typeMap :: Map QName TypeInfo
_typeMap = Map QName TypeInfo
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 (f :: * -> *). Applicative f => Bool -> f () -> f ()
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 -> CaseType -> TTerm -> [TAlt] -> E (TTerm, [TAlt])
pruneUnreachable Int
x (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
        [TACon QName
c Int
a TTerm
b] -> 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
noerase
            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    -> (if Int
a 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
$ 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
a TTerm
TErased [TTerm] -> Substitution' TTerm -> Substitution' TTerm
forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# Substitution' TTerm
forall a. Substitution' a
idS) TTerm
b
                              -- might enable more erasure
        [TAlt]
_ -> E TTerm
noerase
      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

    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

-- | 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 -> CaseType -> TTerm -> [TAlt] -> E (TTerm, [TAlt])
pruneUnreachable :: Int -> CaseType -> TTerm -> [TAlt] -> E (TTerm, [TAlt])
pruneUnreachable Int
_ (CTData Quantity
quantity QName
q) TTerm
d [TAlt]
bs' = do
  -- In an erased setting erased constructors are not treated
  -- specially.
  [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 Quantity -> Bool
forall a. LensQuantity a => a -> Bool
hasQuantity0 Quantity
quantity
        then QName -> TCM [QName]
getConstructors QName
q
        else QName -> TCM [QName]
getNotErasedConstructors QName
q
  let bs :: [TAlt]
bs | Quantity -> Bool
forall a. LensQuantity a => a -> Bool
hasQuantity0 Quantity
quantity = [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 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 ]
  let 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 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 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
_ 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' (Maybe FunInfo) ESt
-> StateT ESt (TCMT IO) FunInfo -> StateT ESt (TCMT IO) FunInfo
forall s (m :: * -> *) a.
MonadState s m =>
Lens' (Maybe a) s -> m a -> m a
memo ((Map QName FunInfo -> f (Map QName FunInfo)) -> ESt -> f ESt
Lens' (Map QName FunInfo) ESt
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' (Maybe FunInfo) (Map QName FunInfo)
forall k v. Ord k => k -> Lens' (Maybe v) (Map k 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 =
  -- 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' (Maybe ArgName) TCEnv -> TCMT IO (Maybe ArgName)
forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC (Maybe ArgName -> f (Maybe ArgName)) -> TCEnv -> f TCEnv
Lens' (Maybe ArgName) TCEnv
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 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' (Map QName TypeInfo) ESt
-> StateT ESt (TCMT IO) (Map QName TypeInfo)
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use (Map QName TypeInfo -> f (Map QName TypeInfo)) -> ESt -> f ESt
Lens' (Map QName TypeInfo) ESt
typeMap
      TypeInfo
dInfo <- QName -> StateT ESt (TCMT IO) TypeInfo
typeInfo QName
d
      (Map QName TypeInfo -> f (Map QName TypeInfo)) -> ESt -> f ESt
Lens' (Map QName TypeInfo) ESt
typeMap Lens' (Map QName TypeInfo) ESt -> Map QName TypeInfo -> E ()
forall o (m :: * -> *) i. MonadState o m => Lens' i o -> 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' (Maybe TypeInfo) ESt
-> TypeInfo
-> StateT ESt (TCMT IO) TypeInfo
-> StateT ESt (TCMT IO) TypeInfo
forall s (m :: * -> *) a.
MonadState s m =>
Lens' (Maybe a) s -> a -> m a -> m a
memoRec ((Map QName TypeInfo -> f (Map QName TypeInfo)) -> ESt -> f ESt
Lens' (Map QName TypeInfo) ESt
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' (Maybe TypeInfo) (Map QName TypeInfo)
forall k v. Ord k => k -> Lens' (Maybe v) (Map k 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
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
$ ArgName -> TCM (Maybe QName)
forall (m :: * -> *). HasBuiltins m => ArgName -> m (Maybe QName)
getName' ArgName
builtinId
      [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
$ (ArgName -> TCM (Maybe QName)) -> [ArgName] -> 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 ArgName -> TCM (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
ArgName -> m (Maybe QName)
getBuiltinName
                         [ArgName
builtinSize, ArgName
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
== 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
          (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