    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 (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.
      Set Int
    fv <- TTerm -> TCMT IO (Set Int)
    go TTerm
    t
      [ArgUsage] -> TCM [ArgUsage]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([ArgUsage] -> TCM [ArgUsage]) -> [ArgUsage] -> TCM [ArgUsage]
    forall a b. (a -> b) -> a -> b
    $ [ if Int -> Set Int -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member Int
    i Set Int
    fv then ArgUsage
    ArgUsed else ArgUsage
    ArgUnused
               | Int
    i <- Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom ([ArgUsage] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [ArgUsage]
    used)
               ]
      where
        go :: TTerm -> TCMT IO (Set Int)
    go = \case
          TVar Int
    x    -> Set Int -> TCMT IO (Set Int)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Set Int -> TCMT IO (Set Int)) -> Set Int -> TCMT IO (Set Int)
    forall a b. (a -> b) -> a -> b
    $ Int -> Set Int
    forall a. a -> Set a
    Set.singleton Int
    x
          TPrim{}   -> Set Int -> TCMT IO (Set Int)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Set Int
    forall a. Set a
    Set.empty
          TDef{}    -> Set Int -> TCMT IO (Set Int)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Set Int
    forall a. Set a
    Set.empty
          TLit{}    -> Set Int -> TCMT IO (Set Int)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Set Int
    forall a. Set a
    Set.empty
          TCon{}    -> Set Int -> TCMT IO (Set Int)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Set Int
    forall a. Set a
    Set.empty

          TApp (TDef QName
    f) Args
    ts -> do
            [ArgUsage]
    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
            [Set Int] -> Set Int
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions ([Set Int] -> Set Int) -> TCMT IO [Set Int] -> TCMT IO (Set Int)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [TCMT IO (Set Int)] -> TCMT IO [Set Int]
    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) <- Args -> [ArgUsage] -> [(TTerm, ArgUsage)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip Args
    ts ([ArgUsage] -> [(TTerm, ArgUsage)])
    -> [ArgUsage] -> [(TTerm, 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 ]

          TApp TTerm
    f Args
    ts -> [Set Int] -> Set Int
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions ([Set Int] -> Set Int) -> TCMT IO [Set Int] -> TCMT IO (Set Int)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TTerm -> TCMT IO (Set Int)) -> Args -> TCMT IO [Set Int]
    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 TTerm -> Args -> Args
    forall a. a -> [a] -> [a]
    : Args
    ts)
          TLam TTerm
    b    -> Set Int -> Set Int
    underBinder (Set Int -> Set Int) -> TCMT IO (Set Int) -> TCMT IO (Set Int)
    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 | Int -> Set Int -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member Int
    0 Set Int
    uses -> Set Int -> Set Int -> Set Int
    forall a. Ord a => Set a -> Set a -> Set a
    Set.union (Set Int -> Set Int
    underBinder Set Int
    uses) (Set Int -> Set Int) -> TCMT IO (Set Int) -> TCMT IO (Set Int)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> TCMT IO (Set Int)
    go TTerm
    e
               | Bool
    otherwise         -> Set Int -> TCMT IO (Set Int)
    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 -> Int -> Set Int -> Set Int
    forall a. Ord a => a -> Set a -> Set a
    Set.insert Int
    x (Set Int -> Set Int)
    -> ([Set Int] -> Set Int) -> [Set Int] -> Set Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Set Int] -> Set Int
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions ([Set Int] -> Set Int) -> TCMT IO [Set Int] -> TCMT IO (Set Int)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((:) (Set Int -> [Set Int] -> [Set Int])
    -> TCMT IO (Set Int) -> TCMT IO ([Set Int] -> [Set Int])
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> TCMT IO (Set Int)
    go TTerm
    d TCMT IO ([Set Int] -> [Set Int])
    -> TCMT IO [Set Int] -> TCMT IO [Set Int]
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (TAlt -> TCMT IO (Set Int)) -> [TAlt] -> TCMT IO [Set Int]
    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{}   -> Set Int -> TCMT IO (Set Int)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Set Int
    forall a. Set a
    Set.empty
          TSort{}   -> Set Int -> TCMT IO (Set Int)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Set Int
    forall a. Set a
    Set.empty
          TErased{} -> Set Int -> TCMT IO (Set Int)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Set Int
    forall a. Set a
    Set.empty
          TError{}  -> Set Int -> TCMT IO (Set Int)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Set Int
    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) = Set Int -> Set Int -> Set Int
    forall a. Ord a => Set a -> Set a -> Set a
    Set.union (Set Int -> Set Int -> Set Int)
    -> TCMT IO (Set Int) -> TCMT IO (Set Int -> Set Int)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> TCMT IO (Set Int)
    go TTerm
    g TCMT IO (Set Int -> Set Int)
    -> TCMT IO (Set Int) -> TCMT IO (Set Int)
    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) = Int -> Set Int -> Set Int
    forall {a}. (Num a, Ord a) => a -> Set a -> Set a
    underBinders Int
    a (Set Int -> Set Int) -> TCMT IO (Set Int) -> TCMT IO (Set Int)
    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 = Int -> Set Int -> Set Int
    forall {a}. (Num a, Ord a) => a -> Set a -> Set a
    underBinders Int
    1
        underBinders :: a -> Set a -> Set a
    underBinders a
    0 = Set a -> Set a
    forall a. a -> a
    id
        underBinders a
    n = (a -> Bool) -> Set a -> Set a
    forall a. (a -> Bool) -> Set a -> Set a
    Set.filter (a -> a -> Bool
    forall a. Ord a => a -> a -> Bool
    >= a
    0) (Set a -> Set a) -> (Set a -> Set a) -> Set a -> Set a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> a) -> Set a -> Set a
    forall a b. (a -> b) -> Set a -> Set b
    Set.mapMonotonic (a -> a -> a
    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 (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 (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