{-# OPTIONS_GHC -Wunused-imports #-}

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

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 )
import qualified Agda.Utils.VarSet as VarSet

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) <- [Char] -> [ArgUsage] -> [(Char, ArgUsage)]
forall a b. [a] -> [b] -> [(a, b)]
zip [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 IntSet
go TTerm
t
  return $ [ if VarSet.member i fv then ArgUsed else ArgUnused
           | i <- downFrom (length used)
           ]
  where
    go :: TTerm -> TCMT IO IntSet
go = \case
      TVar Int
x    -> IntSet -> TCMT IO IntSet
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (IntSet -> TCMT IO IntSet) -> IntSet -> TCMT IO IntSet
forall a b. (a -> b) -> a -> b
$ Int -> IntSet
VarSet.singleton Int
x
      TPrim{}   -> IntSet -> TCMT IO IntSet
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure IntSet
VarSet.empty
      TDef{}    -> IntSet -> TCMT IO IntSet
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure IntSet
VarSet.empty
      TLit{}    -> IntSet -> TCMT IO IntSet
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure IntSet
VarSet.empty
      TCon{}    -> IntSet -> TCMT IO IntSet
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure IntSet
VarSet.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 $ used ++ repeat ArgUsed ]

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

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

    underBinder :: IntSet -> IntSet
underBinder = Int -> IntSet -> IntSet
underBinders Int
1
    underBinders :: Int -> IntSet -> IntSet
underBinders Int
0 = IntSet -> IntSet
forall a. a -> a
id
    underBinders Int
n = Int -> IntSet -> IntSet
VarSet.filterGE Int
0 (IntSet -> IntSet) -> (IntSet -> IntSet) -> IntSet -> IntSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> IntSet -> IntSet
VarSet.subtract 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
$ Int -> [ArgUsage] -> [ArgUsage]
forall a. Int -> [a] -> [a]
take Int
n ([ArgUsage] -> [ArgUsage]) -> [ArgUsage] -> [ArgUsage]
forall a b. (a -> b) -> a -> b
$ [ArgUsage]
used [ArgUsage] -> [ArgUsage] -> [ArgUsage]
forall a. [a] -> [a] -> [a]
++ ArgUsage -> [ArgUsage]
forall a. a -> [a]
repeat ArgUsage
ArgUsed
    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