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

import Data.Maybe

import qualified Data.Set as Set
  -- Andreas, 2021-02-10
  -- TODO: Replace Set by IntSet.
  -- However, this has to wait until we can comfortably bump to
  -- containers-0.6.3.1, which is the first to contain IntSet.mapMonotonic.
  -- Currently, such a constraints gets us into cabal hell.
  -- GHC 8.10 is still shipped with 0.6.2.1, so we either have to wait
  -- until we drop GHC 8 or until we adopt v2-cabal.

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 Agda.Utils.Pretty   ( prettyShow )

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 (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 = forall (m :: * -> *) a.
Monad m =>
(a -> a -> Bool) -> (a -> m a) -> a -> m a
iterateUntilM forall a. Eq a => a -> a -> Bool
(==) forall a b. (a -> b) -> a -> b
$ \ [ArgUsage]
used -> do

  forall (m :: * -> *).
MonadDebug m =>
[Char] -> Int -> [Char] -> m ()
reportSLn [Char]
"treeless.opt.unused" Int
50 forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ [Char]
"Unused approximation for ", forall a. Pretty a => a -> [Char]
prettyShow QName
q, [Char]
": "
    , [[Char]] -> [Char]
unwords [ if ArgUsage
u forall a. Eq a => a -> a -> Bool
== ArgUsage
ArgUsed then [Char
x] else [Char]
"_" | (Char
x, ArgUsage
u) <- 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.
  Set Int
fv <- TTerm -> TCMT IO (Set Int)
go TTerm
t
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [ if forall a. Ord a => a -> Set a -> Bool
Set.member Int
i Set Int
fv then ArgUsage
ArgUsed else ArgUsage
ArgUnused
           | Int
i <- forall a. Integral a => a -> [a]
downFrom (forall (t :: * -> *) a. Foldable t => t a -> Int
length [ArgUsage]
used)
           ]
  where
    go :: TTerm -> TCMT IO (Set Int)
go = \case
      TVar Int
x    -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> Set a
Set.singleton Int
x
      TPrim{}   -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Set a
Set.empty
      TDef{}    -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Set a
Set.empty
      TLit{}    -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Set a
Set.empty
      TCon{}    -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Set a
Set.empty

      TApp (TDef QName
f) Args
ts -> do
        [ArgUsage]
used <- 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
f
        forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [ TTerm -> TCMT IO (Set Int)
go TTerm
t | (TTerm
t, ArgUsage
ArgUsed) <- forall a b. [a] -> [b] -> [(a, b)]
zip Args
ts forall a b. (a -> b) -> a -> b
$ [ArgUsage]
used forall a. [a] -> [a] -> [a]
++ forall a. a -> [a]
repeat ArgUsage
ArgUsed ]

      TApp TTerm
f Args
ts -> forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions 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 TTerm -> TCMT IO (Set Int)
go (TTerm
f forall a. a -> [a] -> [a]
: Args
ts)
      TLam TTerm
b    -> Set Int -> Set Int
underBinder forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> TCMT IO (Set Int)
go TTerm
b
      TLet TTerm
e TTerm
b  -> do
        Set Int
uses <- TTerm -> TCMT IO (Set Int)
go TTerm
b
        if | forall a. Ord a => a -> Set a -> Bool
Set.member Int
0 Set Int
uses -> forall a. Ord a => Set a -> Set a -> Set a
Set.union (Set Int -> Set Int
underBinder Set Int
uses) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> TCMT IO (Set Int)
go TTerm
e
           | Bool
otherwise         -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set Int -> Set Int
underBinder Set Int
uses)
      TCase Int
x CaseInfo
_ TTerm
d [TAlt]
bs -> forall a. Ord a => a -> Set a -> Set a
Set.insert Int
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> TCMT IO (Set Int)
go TTerm
d 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 TAlt -> TCMT IO (Set Int)
goAlt [TAlt]
bs)
      TUnit{}   -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Set a
Set.empty
      TSort{}   -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Set a
Set.empty
      TErased{} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Set a
Set.empty
      TError{}  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Set a
Set.empty
      TCoerce TTerm
t -> TTerm -> TCMT IO (Set Int)
go TTerm
t

    goAlt :: TAlt -> TCMT IO (Set Int)
goAlt (TALit Literal
_   TTerm
b) = TTerm -> TCMT IO (Set Int)
go TTerm
b
    goAlt (TAGuard TTerm
g TTerm
b) = forall a. Ord a => Set a -> Set a -> Set a
Set.union forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> TCMT IO (Set Int)
go TTerm
g forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TTerm -> TCMT IO (Set Int)
go TTerm
b
    goAlt (TACon QName
_ Int
a TTerm
b) = forall {a}. (Num a, Ord a) => a -> Set a -> Set a
underBinders Int
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> TCMT IO (Set Int)
go TTerm
b

    underBinder :: Set Int -> Set Int
underBinder = forall {a}. (Num a, Ord a) => a -> Set a -> Set a
underBinders Int
1
    underBinders :: a -> Set a -> Set a
underBinders a
0 = forall a. a -> a
id
    underBinders a
n = forall a. (a -> Bool) -> Set a -> Set a
Set.filter (forall a. Ord a => a -> a -> Bool
>= a
0) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic (forall a. Num a => a -> a -> a
subtract a
n)

stripUnusedArguments :: [ArgUsage] -> TTerm -> TTerm
stripUnusedArguments :: [ArgUsage] -> TTerm -> TTerm
stripUnusedArguments [ArgUsage]
used TTerm
t = Int -> TTerm -> TTerm
mkTLam Int
m forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' TTerm
rho TTerm
b
  where
    (Int
n, TTerm
b) = TTerm -> (Int, TTerm)
tLamView TTerm
t
    m :: Int
m      = forall (t :: * -> *) a. Foldable t => t a -> Int
length forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
== ArgUsage
ArgUsed) [ArgUsage]
used'
    used' :: [ArgUsage]
used'  = forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
take Int
n forall a b. (a -> b) -> a -> b
$ [ArgUsage]
used forall a. [a] -> [a] -> [a]
++ 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 forall a. a -> Substitution' a -> Substitution' a
:# [ArgUsage] -> Substitution' TTerm
computeSubst [ArgUsage]
bs
    computeSubst (ArgUsage
ArgUsed   : [ArgUsage]
bs) = forall a. Int -> Substitution' a -> Substitution' a
liftS Int
1 forall a b. (a -> b) -> a -> b
$ [ArgUsage] -> Substitution' TTerm
computeSubst [ArgUsage]
bs
    computeSubst []               = forall a. Substitution' a
idS