{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.Compiler.Treeless.Unused
  ( usedArguments
  , stripUnusedArguments
  ) where

import Prelude hiding (null, zip, zipWith)

import Data.Maybe

import Agda.Syntax.Common
import Agda.Syntax.Common.Pretty   ( prettyShow )
import Agda.Syntax.Treeless
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Substitute

import Agda.Compiler.Treeless.Pretty () -- instance only

import Agda.Utils.Function ( iterateUntilM )
import Agda.Utils.List     ( downFrom, takeExactly )
import Agda.Utils.ListInf qualified as ListInf
import Agda.Utils.Null
import Agda.Utils.Singleton
import qualified Agda.Utils.VarSet as VarSet
import Agda.Utils.Zip

usedArguments :: QName -> TTerm -> TCM [ArgUsage]
usedArguments :: QName -> TTerm -> TCM [ArgUsage]
usedArguments QName
q TTerm
t = QName -> TTerm -> [ArgUsage] -> TCM [ArgUsage]
computeUnused QName
q TTerm
b (Int -> ArgUsage -> [ArgUsage]
forall a. Int -> a -> [a]
replicate Int
n ArgUsage
ArgUnused)
  where (Int
n, TTerm
b) = TTerm -> (Int, TTerm)
tLamView TTerm
t

-- | Saturation algorithm, starting with all unused arguments
--   and adding usages until fixed-point has been reached.

computeUnused :: QName -> TTerm -> [ArgUsage] -> TCM [ArgUsage]
computeUnused :: QName -> TTerm -> [ArgUsage] -> TCM [ArgUsage]
computeUnused QName
q TTerm
t = ([ArgUsage] -> [ArgUsage] -> Bool)
-> ([ArgUsage] -> TCM [ArgUsage]) -> [ArgUsage] -> TCM [ArgUsage]
forall (m :: * -> *) a.
Monad m =>
(a -> a -> Bool) -> (a -> m a) -> a -> m a
iterateUntilM [ArgUsage] -> [ArgUsage] -> Bool
forall a. Eq a => a -> a -> Bool
(==) (([ArgUsage] -> TCM [ArgUsage]) -> [ArgUsage] -> TCM [ArgUsage])
-> ([ArgUsage] -> TCM [ArgUsage]) -> [ArgUsage] -> TCM [ArgUsage]
forall a b. (a -> b) -> a -> b
$ \ [ArgUsage]
used -> do

  [Char] -> Int -> [Char] -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"treeless.opt.unused" Int
50 ([Char] -> TCMT IO ()) -> [Char] -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ [Char]
"Unused approximation for ", QName -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow QName
q, [Char]
": "
    , [[Char]] -> [Char]
unwords [ if ArgUsage
u ArgUsage -> ArgUsage -> Bool
forall a. Eq a => a -> a -> Bool
== ArgUsage
ArgUsed then [Char
x] else [Char]
"_" | (Char
x, ArgUsage
u) <- Infinite Char -> [ArgUsage] -> [(Char, ArgUsage)]
forall a b. Infinite a -> [b] -> [(a, b)]
forall (f :: * -> *) (g :: * -> *) (h :: * -> *) a b.
Zip f g h =>
f a -> g b -> h (a, b)
zip (Char -> Infinite Char
forall n. Enum n => n -> ListInf n
ListInf.upFrom Char
'a') [ArgUsage]
used ]
    ]
  -- Update usage information q to so far "best" value.
  QName -> [ArgUsage] -> TCMT IO ()
setCompiledArgUse QName
q [ArgUsage]
used

  -- The new usage information is the free variables of @t@,
  -- computed under the current usage assumptions of the functions it calls.
  fv <- TTerm -> TCMT IO VarSet
go TTerm
t
  return $ [ if VarSet.member i fv then ArgUsed else ArgUnused
           | i <- downFrom (length used)
           ]
  where
    go :: TTerm -> TCMT IO VarSet
go = \case
      TVar Int
x    -> VarSet -> TCMT IO VarSet
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarSet -> TCMT IO VarSet) -> VarSet -> TCMT IO VarSet
forall a b. (a -> b) -> a -> b
$ Int -> VarSet
forall el coll. Singleton el coll => el -> coll
singleton Int
x
      TPrim{}   -> VarSet -> TCMT IO VarSet
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VarSet
forall a. Null a => a
empty
      TDef{}    -> VarSet -> TCMT IO VarSet
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VarSet
forall a. Null a => a
empty
      TLit{}    -> VarSet -> TCMT IO VarSet
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VarSet
forall a. Null a => a
empty
      TCon{}    -> VarSet -> TCMT IO VarSet
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VarSet
forall a. Null a => a
empty

      TApp (TDef QName
f) Args
ts -> do
        used <- [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
f
        VarSet.unions <$> sequence [ go t | (t, ArgUsed) <- zip ts $ ListInf.pad used ArgUsed ]

      TApp TTerm
f Args
ts -> [VarSet] -> VarSet
forall (f :: * -> *). Foldable f => f VarSet -> VarSet
VarSet.unions ([VarSet] -> VarSet) -> TCMT IO [VarSet] -> TCMT IO VarSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TTerm -> TCMT IO VarSet) -> Args -> TCMT IO [VarSet]
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 -> TCMT IO VarSet
go (TTerm
f TTerm -> Args -> Args
forall a. a -> [a] -> [a]
: Args
ts)
      TLam TTerm
b    -> VarSet -> VarSet
underBinder (VarSet -> VarSet) -> TCMT IO VarSet -> TCMT IO VarSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> TCMT IO VarSet
go TTerm
b
      TLet TTerm
e TTerm
b  -> do
        uses <- TTerm -> TCMT IO VarSet
go TTerm
b
        if | VarSet.member 0 uses -> VarSet.union (underBinder uses) <$> go e
           | otherwise            -> pure (underBinder uses)
      TCase Int
x CaseInfo
i TTerm
d [TAlt]
bs ->
        let e :: Erased
e    = CaseInfo -> Erased
caseErased CaseInfo
i
            cont :: TCMT IO VarSet
cont = [VarSet] -> VarSet
forall (f :: * -> *). Foldable f => f VarSet -> VarSet
VarSet.unions ([VarSet] -> VarSet) -> TCMT IO [VarSet] -> TCMT IO VarSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((:) (VarSet -> [VarSet] -> [VarSet])
-> TCMT IO VarSet -> TCMT IO ([VarSet] -> [VarSet])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> TCMT IO VarSet
go TTerm
d TCMT IO ([VarSet] -> [VarSet])
-> TCMT IO [VarSet] -> TCMT IO [VarSet]
forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (TAlt -> TCMT IO VarSet) -> [TAlt] -> TCMT IO [VarSet]
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 (Erased -> TAlt -> TCMT IO VarSet
goAlt Erased
e) [TAlt]
bs) in
        case Erased
e of
          Erased{}    -> TCMT IO VarSet
cont
          NotErased{} -> Int -> VarSet -> VarSet
VarSet.insert Int
x (VarSet -> VarSet) -> TCMT IO VarSet -> TCMT IO VarSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO VarSet
cont
      TUnit{}   -> VarSet -> TCMT IO VarSet
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VarSet
forall a. Null a => a
empty
      TSort{}   -> VarSet -> TCMT IO VarSet
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VarSet
forall a. Null a => a
empty
      TErased{} -> VarSet -> TCMT IO VarSet
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VarSet
forall a. Null a => a
empty
      TError{}  -> VarSet -> TCMT IO VarSet
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VarSet
forall a. Null a => a
empty
      TCoerce TTerm
t -> TTerm -> TCMT IO VarSet
go TTerm
t

    goAlt :: Erased -> TAlt -> TCMT IO VarSet
goAlt Erased
_ (TALit Literal
_   TTerm
b) = TTerm -> TCMT IO VarSet
go TTerm
b
    goAlt Erased
e (TAGuard TTerm
g TTerm
b) = case Erased
e of
      NotErased{} -> VarSet -> VarSet -> VarSet
VarSet.union (VarSet -> VarSet -> VarSet)
-> TCMT IO VarSet -> TCMT IO (VarSet -> VarSet)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> TCMT IO VarSet
go TTerm
g TCMT IO (VarSet -> VarSet) -> TCMT IO VarSet -> TCMT IO VarSet
forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TTerm -> TCMT IO VarSet
go TTerm
b
      Erased{}    -> -- The guard will not be executed if the match
                     -- is on an erased argument.
                     TTerm -> TCMT IO VarSet
go TTerm
b
    goAlt Erased
_ (TACon QName
_ Int
a TTerm
b) = Int -> VarSet -> VarSet
underBinders Int
a (VarSet -> VarSet) -> TCMT IO VarSet -> TCMT IO VarSet
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> TCMT IO VarSet
go TTerm
b

    underBinder :: VarSet -> VarSet
underBinder = Int -> VarSet -> VarSet
underBinders Int
1
    underBinders :: Int -> VarSet -> VarSet
underBinders Int
n = Int -> VarSet -> VarSet
VarSet.strengthen Int
n

stripUnusedArguments :: [ArgUsage] -> TTerm -> TTerm
stripUnusedArguments :: [ArgUsage] -> TTerm -> TTerm
stripUnusedArguments [ArgUsage]
used TTerm
t = Int -> TTerm -> TTerm
mkTLam Int
m (TTerm -> TTerm) -> TTerm -> TTerm
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg TTerm) -> TTerm -> TTerm
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' TTerm
Substitution' (SubstArg TTerm)
rho TTerm
b
  where
    (Int
n, TTerm
b) = TTerm -> (Int, TTerm)
tLamView TTerm
t
    m :: Int
m      = [ArgUsage] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([ArgUsage] -> Int) -> [ArgUsage] -> Int
forall a b. (a -> b) -> a -> b
$ (ArgUsage -> Bool) -> [ArgUsage] -> [ArgUsage]
forall a. (a -> Bool) -> [a] -> [a]
filter (ArgUsage -> ArgUsage -> Bool
forall a. Eq a => a -> a -> Bool
== ArgUsage
ArgUsed) [ArgUsage]
used'
    used' :: [ArgUsage]
used'  = [ArgUsage] -> [ArgUsage]
forall a. [a] -> [a]
reverse ([ArgUsage] -> [ArgUsage]) -> [ArgUsage] -> [ArgUsage]
forall a b. (a -> b) -> a -> b
$ ArgUsage -> Int -> [ArgUsage] -> [ArgUsage]
forall a n. Integral n => a -> n -> [a] -> [a]
takeExactly ArgUsage
ArgUsed Int
n [ArgUsage]
used
    rho :: Substitution' TTerm
rho = [ArgUsage] -> Substitution' TTerm
computeSubst [ArgUsage]
used'
    computeSubst :: [ArgUsage] -> Substitution' TTerm
computeSubst (ArgUsage
ArgUnused : [ArgUsage]
bs) = TTerm
TErased TTerm -> Substitution' TTerm -> Substitution' TTerm
forall a. a -> Substitution' a -> Substitution' a
:# [ArgUsage] -> Substitution' TTerm
computeSubst [ArgUsage]
bs
    computeSubst (ArgUsage
ArgUsed   : [ArgUsage]
bs) = Int -> Substitution' TTerm -> Substitution' TTerm
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
1 (Substitution' TTerm -> Substitution' TTerm)
-> Substitution' TTerm -> Substitution' TTerm
forall a b. (a -> b) -> a -> b
$ [ArgUsage] -> Substitution' TTerm
computeSubst [ArgUsage]
bs
    computeSubst []               = Substitution' TTerm
forall a. Substitution' a
idS