{-# 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) 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) 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 = 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 forall k a. Map k a
Map.empty 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
  forall a. E a -> TCM a
runE forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ QName -> E 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 forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall a. E a -> TCM a
runE (QName -> TTerm -> StateT ESt (TCMT IO) TTerm
eraseTop QName
q TTerm
t)
  where
    eraseTop :: QName -> TTerm -> StateT ESt (TCMT IO) TTerm
eraseTop QName
q TTerm
t = do
      ([TypeInfo]
_, TypeInfo
h) <- QName -> E FunInfo
getFunInfo QName
q
      case TypeInfo
h of
        TypeInfo
Erasable -> forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
TErased
        TypeInfo
Empty    -> forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
TErased
        TypeInfo
_        -> TTerm -> StateT ESt (TCMT IO) TTerm
erase TTerm
t

    erase :: TTerm -> StateT ESt (TCMT IO) TTerm
erase TTerm
t = case TTerm -> (TTerm, [TTerm])
tAppView TTerm
t of

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

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

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

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

    -- #3380: this is not safe for strict backends
    tLam :: TTerm -> TTerm
tLam TTerm
TErased | EvaluationStrategy
eval 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
      | forall a. HasFree a => Int -> a -> Bool
freeIn Int
0 TTerm
b = TTerm -> TTerm -> TTerm
TLet TTerm
e TTerm
b
      | Bool
otherwise  = forall a. Subst a => Impossible -> a -> a
strengthen HasCallStack => Impossible
impossible TTerm
b

    tApp :: TTerm -> [TTerm] -> TTerm
tApp TTerm
f []                  = TTerm
f
    tApp TTerm
TErased [TTerm]
_             = TTerm
TErased
    tApp TTerm
f [TTerm]
_ | 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] -> StateT ESt (TCMT IO) TTerm
tCase Int
x CaseInfo
t TTerm
d [TAlt]
bs
      | TTerm -> Bool
isErased TTerm
d Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (TTerm -> Bool
isErased forall b c a. (b -> c) -> (a -> b) -> a -> c
. TAlt -> TTerm
aBody) [TAlt]
bs = 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 <- forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> E FunInfo
getFunInfo QName
c
          case TypeInfo
h of
            TypeInfo
NotErasable -> StateT ESt (TCMT IO) TTerm
noerase
            TypeInfo
Empty       -> forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
TErased
            TypeInfo
Erasable    -> (if Int
a forall a. Eq a => a -> a -> Bool
== Int
0 then forall (f :: * -> *) a. Applicative f => a -> f a
pure else TTerm -> StateT ESt (TCMT IO) TTerm
erase) forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (forall a. Int -> a -> [a]
replicate Int
a TTerm
TErased forall a. DeBruijn a => [a] -> Substitution' a -> Substitution' a
++# forall a. Substitution' a
idS) TTerm
b
                              -- might enable more erasure
        [TAlt]
_ -> StateT ESt (TCMT IO) TTerm
noerase
      where
        noerase :: StateT ESt (TCMT IO) TTerm
noerase = forall (f :: * -> *) a. Applicative f => a -> f a
pure 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 forall a. Eq a => a -> a -> Bool
== TTerm
TErased Bool -> Bool -> Bool
|| forall a. Unreachable a => a -> Bool
isUnreachable TTerm
t

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

    eraseAlt :: TAlt -> StateT ESt (TCMT IO) TAlt
eraseAlt = \case
      TALit Literal
l TTerm
b   -> Literal -> TTerm -> TAlt
TALit Literal
l   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> StateT ESt (TCMT IO) TTerm
erase TTerm
b
      TACon QName
c Int
a TTerm
b -> do
        [Bool]
rs <- forall a b. (a -> b) -> [a] -> [b]
map TypeInfo -> Bool
erasable forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> E FunInfo
getFunInfo QName
c
        let sub :: Substitution' TTerm
sub = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ Bool
e -> if Bool
e then (TTerm
TErased forall a. a -> Substitution' a -> Substitution' a
:#) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> Substitution' a -> Substitution' a
wkS Int
1 else forall a. Int -> Substitution' a -> Substitution' a
liftS Int
1) forall a. Substitution' a
idS forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse [Bool]
rs
        QName -> Int -> TTerm -> TAlt
TACon QName
c Int
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> StateT ESt (TCMT IO) TTerm
erase (forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' TTerm
sub TTerm
b)
      TAGuard TTerm
g TTerm
b -> TTerm -> TTerm -> TAlt
TAGuard   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> StateT ESt (TCMT IO) TTerm
erase TTerm
g forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TTerm -> StateT ESt (TCMT IO) 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 <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$
        if 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 | forall a. LensQuantity a => a -> Bool
hasQuantity0 Quantity
quantity = [TAlt]
bs'
         | Bool
otherwise             =
           forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a. (a -> Bool) -> [a] -> [a]
filter [TAlt]
bs' forall a b. (a -> b) -> a -> b
$ \case
             a :: TAlt
a@TACon{} -> (TAlt -> QName
aCon TAlt
a) forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [QName]
cs
             TAGuard{} -> Bool
True
             TALit{}   -> Bool
True
  let complete :: Bool
complete =forall (t :: * -> *) a. Foldable t => t a -> Int
length [QName]
cs forall a. Eq a => a -> a -> Bool
== 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
  forall (m :: * -> *) a. Monad m => a -> m a
return (TTerm
d', [TAlt]
bs)
pruneUnreachable Int
x CaseType
CTNat TTerm
d [TAlt]
bs = forall (m :: * -> *) a. Monad m => a -> m a
return 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 = forall (m :: * -> *) a. Monad m => a -> m a
return 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 = 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 $bBelow :: Int -> Integer -> TTerm
$mBelow :: forall {r}. TTerm -> (Int -> Integer -> r) -> ((# #) -> r) -> r
Below x n = TApp (TPrim PLt)  [TVar x, TLit (LitNat n)]

pattern Above :: Int -> Integer -> TTerm
pattern $bAbove :: Int -> Integer -> TTerm
$mAbove :: forall {r}. TTerm -> (Int -> Integer -> r) -> ((# #) -> r) -> r
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 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 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 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
_                                -> forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (TAlt
b forall a. a -> [a] -> [a]
:) forall a b. (a -> b) -> a -> b
$ [TAlt] -> IntSet -> (TTerm, [TAlt])
go [TAlt]
bs IntSet
cover
      where
        rec :: IntSet -> (TTerm, [TAlt])
rec IntSet
this = forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second [TAlt] -> [TAlt]
addAlt 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' forall a. Semigroup a => a -> a -> a
<> IntSet
cover
            addAlt :: [TAlt] -> [TAlt]
addAlt = case IntSet -> Maybe [Integer]
IntSet.toFiniteList IntSet
this' of
                       Just []  -> forall a. a -> a
id                                     -- unreachable case
                       Just [Integer
n] -> (Literal -> TTerm -> TAlt
TALit (Integer -> Literal
LitNat Integer
n) (TAlt -> TTerm
aBody TAlt
b) forall a. a -> [a] -> [a]
:) -- possibly refined case
                       Maybe [Integer]
_        -> (TAlt
b forall a. a -> [a] -> [a]
:)                                  -- unchanged case

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

sumTypeInfo :: [TypeInfo] -> TypeInfo
sumTypeInfo :: [TypeInfo] -> TypeInfo
sumTypeInfo [TypeInfo]
is = 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 -> E FunInfo
getFunInfo QName
q = forall s (m :: * -> *) a.
MonadState s m =>
Lens' (Maybe a) s -> m a -> m a
memo (Lens' (Map QName FunInfo) ESt
funMap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. Ord k => k -> Lens' (Maybe v) (Map k v)
key QName
q) forall a b. (a -> b) -> a -> b
$ QName -> E FunInfo
getInfo QName
q
  where
    getInfo :: QName -> E FunInfo
    getInfo :: QName -> E FunInfo
getInfo QName
q = do
      ([TypeInfo]
rs, Type
t) <- do
        (ListTel
tel, Type
t) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ QName -> TCM (ListTel, Type)
typeWithoutParams QName
q
        [TypeInfo]
is     <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Type -> StateT ESt (TCMT IO) TypeInfo
getTypeInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Decoration t => t a -> a
dget) ListTel
tel
        [ArgUsage]
used   <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ (forall a. [a] -> [a] -> [a]
++ forall a. a -> [a]
repeat ArgUsage
ArgUsed) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe [] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe [ArgUsage])
getCompiledArgUse QName
q
        [IsForced]
forced <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ (forall a. [a] -> [a] -> [a]
++ forall a. a -> [a]
repeat IsForced
NotForced) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m [IsForced]
getForcedArgs QName
q
        forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall b c a. (b -> c) -> (a -> b) -> a -> c
. Modality -> IsForced -> ArgUsage -> TypeInfo -> TypeInfo
mkR forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensModality a => a -> Modality
getModality) ListTel
tel (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 forall (f :: * -> *) a. Applicative f => a -> f a
pure TypeInfo
Erasable else Type -> StateT ESt (TCMT IO) TypeInfo
getTypeInfo Type
t
      forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> ArgName -> m ()
reportSLn ArgName
"treeless.opt.erase.info" Int
50 forall a b. (a -> b) -> a -> b
$ ArgName
"type info for " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> ArgName
prettyShow QName
q forall a. [a] -> [a] -> [a]
++ ArgName
": " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show [TypeInfo]
rs forall a. [a] -> [a] -> [a]
++ ArgName
" -> " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show TypeInfo
h
      forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ QName -> [Bool] -> TCM ()
setErasedConArgs QName
q forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map TypeInfo -> Bool
erasable [TypeInfo]
rs
      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 (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
  forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (forall (m :: * -> *) a. MonadTCEnv m => Lens' a TCEnv -> m a
viewTC Lens' (Maybe ArgName) TCEnv
eActiveBackendName) forall a. HasCallStack => a
__IMPOSSIBLE__ 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.
  forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (ArgName -> TCM (Maybe Backend)
lookupBackend ArgName
bname)       (forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False)   forall a b. (a -> b) -> a -> b
$ \ Backend
_ ->
  TypeInfo -> Bool
erasable forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. E a -> TCM a
runE (QName -> E FunInfo
getFunInfo QName
qn)

telListView :: Type -> TCM (ListTel, Type)
telListView :: Type -> TCM (ListTel, Type)
telListView Type
t = do
  TelV Tele (Dom Type)
tel Type
t <- forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
telViewPath Type
t
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall t. Tele (Dom t) -> [Dom (ArgName, t)]
telToList Tele (Dom Type)
tel, Type
t)

typeWithoutParams :: QName -> TCM (ListTel, Type)
typeWithoutParams :: QName -> TCM (ListTel, Type)
typeWithoutParams QName
q = do
  Definition
def <- 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 forall a. Num a => a -> a -> a
- Int
1
        Constructor{ conPars :: Defn -> Int
conPars = Int
n } -> Int
n
        Defn
_                          -> Int
0
  forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (forall a. Int -> [a] -> [a]
drop Int
d) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> TCM (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) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Type -> TCM (ListTel, Type)
telListView Type
t0
  TypeInfo
et <- case 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 <- forall o (m :: * -> *) i. MonadState o m => Lens' i o -> m i
use Lens' (Map QName TypeInfo) ESt
typeMap
      TypeInfo
dInfo <- QName -> StateT ESt (TCMT IO) TypeInfo
typeInfo QName
d
      Lens' (Map QName TypeInfo) ESt
typeMap forall o (m :: * -> *) i. MonadState o m => Lens' i o -> i -> m ()
.= forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert QName
d TypeInfo
dInfo Map QName TypeInfo
oldMap
      forall (m :: * -> *) a. Monad m => a -> m a
return TypeInfo
dInfo
    Sort{}    -> forall (m :: * -> *) a. Monad m => a -> m a
return TypeInfo
Erasable
    Term
_         -> forall (m :: * -> *) a. Monad m => a -> m a
return TypeInfo
NotErasable
  [TypeInfo]
is <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Type -> StateT ESt (TCMT IO) TypeInfo
getTypeInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Decoration t => t a -> a
dget) ListTel
tel
  let e :: TypeInfo
e | TypeInfo
Empty forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TypeInfo]
is = TypeInfo
Erasable
        | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [TypeInfo]
is         = TypeInfo
et        -- TODO: guard should really be "all inhabited is"
        | TypeInfo
et forall a. Eq a => a -> a -> Bool
== TypeInfo
Empty     = TypeInfo
Erasable
        | Bool
otherwise       = TypeInfo
et
  forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadDebug m =>
ArgName -> Int -> TCMT IO Doc -> m ()
reportSDoc ArgName
"treeless.opt.erase.type" Int
50 forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM Type
t0 forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => ArgName -> m Doc
text (ArgName
"is " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> ArgName
show TypeInfo
e)
  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 = forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM (QName -> E Bool
erasureForbidden QName
q) (forall (m :: * -> *) a. Monad m => a -> m a
return TypeInfo
NotErasable) forall a b. (a -> b) -> a -> b
$ {-else-} do
    forall s (m :: * -> *) a.
MonadState s m =>
Lens' (Maybe a) s -> a -> m a -> m a
memoRec (Lens' (Map QName TypeInfo) ESt
typeMap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k v. Ord k => k -> Lens' (Maybe v) (Map k v)
key QName
q) TypeInfo
Erasable forall a b. (a -> b) -> a -> b
$ do  -- assume recursive occurrences are erasable
      Maybe QName
mId    <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). HasBuiltins m => ArgName -> m (Maybe QName)
getName' ArgName
builtinId
      [Maybe QName]
msizes <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
ArgName -> m (Maybe QName)
getBuiltinName
                         [ArgName
builtinSize, ArgName
builtinSizeLt]
      Definition
def    <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ 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 } -> forall a. a -> Maybe a
Just [QName]
cs
                  I.Record{ recConHead :: Defn -> ConHead
recConHead = ConHead
c }  -> forall a. a -> Maybe a
Just [ConHead -> QName
conName ConHead
c]
                  Defn
_                           -> forall a. Maybe a
Nothing
      case Maybe [QName]
mcs of
        Maybe [QName]
_ | forall a. a -> Maybe a
Just QName
q forall a. Eq a => a -> a -> Bool
== Maybe QName
mId        -> forall (m :: * -> *) a. Monad m => a -> m a
return TypeInfo
NotErasable
        Maybe [QName]
_ | forall a. a -> Maybe a
Just QName
q forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Maybe QName]
msizes -> forall (m :: * -> *) a. Monad m => a -> m a
return TypeInfo
Erasable
        Just [QName
c] -> do
          (ListTel
ts, Type
_) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ QName -> TCM (ListTel, Type)
typeWithoutParams QName
c
          let rs :: [Modality]
rs = forall a b. (a -> b) -> [a] -> [b]
map forall a. LensModality a => a -> Modality
getModality ListTel
ts
          [TypeInfo]
is <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Type -> StateT ESt (TCMT IO) TypeInfo
getTypeInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Decoration t => t a -> a
dget) ListTel
ts
          let er :: Bool
er = forall (t :: * -> *). Foldable t => t Bool -> Bool
and [ TypeInfo -> Bool
erasable TypeInfo
i Bool -> Bool -> Bool
|| Bool -> Bool
not (forall a. LensModality a => a -> Bool
usableModality Modality
r) | (TypeInfo
i, Modality
r) <- forall a b. [a] -> [b] -> [(a, b)]
zip [TypeInfo]
is [Modality]
rs ]
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ if Bool
er then TypeInfo
Erasable else TypeInfo
NotErasable
        Just []      -> forall (m :: * -> *) a. Monad m => a -> m a
return TypeInfo
Empty
        Just (QName
_:QName
_:[QName]
_) -> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall (m :: * -> *) a. Monad m => a -> m a
return TypeInfo
Empty) (Type -> StateT ESt (TCMT IO) TypeInfo
getTypeInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t a. Sort' t -> a -> Type'' t a
El HasCallStack => Sort
__DUMMY_SORT__) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Maybe Term
clauseBody) [Clause]
cs
            Defn
_ -> 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 -> E Bool
erasureForbidden QName
q = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCM Bool
activeBackendMayEraseType QName
q