    {-# 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