    {-# OPTIONS_GHC -Wunused-imports #-}

    -- | Logic for deciding which functions should be automatically inlined.
    module Agda.TypeChecking.Inlining (autoInline) where

    import qualified Data.IntMap as IntMap

    import Agda.Interaction.Options
    import Agda.TypeChecking.Monad.Base
    import Agda.TypeChecking.CompiledClause
    import Agda.TypeChecking.Free
    import Agda.Utils.Lens

    -- | Mark a definition to be inlined if it satisfies the inlining criterion.
    autoInline :: Defn -> TCM Defn
    autoInline :: Defn -> TCM Defn
    autoInline Defn
    defn = do
      inlining <- PragmaOptions -> Bool
    optAutoInline (PragmaOptions -> Bool) -> TCMT IO PragmaOptions -> TCMT IO Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions
      if | inlining, shouldInline defn -> return $ set funInline True defn
         | otherwise                   -> return defn

    shouldInline :: Defn -> Bool
    shouldInline :: Defn -> Bool
    shouldInline Function{funCompiled :: Defn -> Maybe CompiledClauses
    funCompiled = Just CompiledClauses
    cc} = CompiledClauses -> Bool
    shouldInline' CompiledClauses
    cc
    shouldInline Defn
    _ = Bool
    False

    -- Only auto-inline simple definitions (no pattern matching) where no variable
    -- is used more than once, and some variables are not used at all.
    shouldInline' :: CompiledClauses -> Bool
    shouldInline' :: CompiledClauses -> Bool
    shouldInline' (Done [Arg ArgName]
    xs Term
    body) = (Variable -> Bool) -> [Variable] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (Variable -> Variable -> Bool
    forall a. Ord a => a -> a -> Bool
    < Variable
    2) [Variable]
    counts Bool -> Bool -> Bool
    && [Variable] -> Variable
    forall a. [a] -> Variable
    forall (t :: * -> *) a. Foldable t => t a -> Variable
    length [Variable]
    counts Variable -> Variable -> Bool
    forall a. Ord a => a -> a -> Bool
    < [Arg ArgName] -> Variable
    forall a. [a] -> Variable
    forall (t :: * -> *) a. Foldable t => t a -> Variable
    length [Arg ArgName]
    xs
      where counts :: [Variable]
    counts = IntMap Variable -> [Variable]
    forall a. IntMap a -> [a]
    IntMap.elems (IntMap Variable -> [Variable]) -> IntMap Variable -> [Variable]
    forall a b. (a -> b) -> a -> b
    $ VarCounts -> IntMap Variable
    varCounts (VarCounts -> IntMap Variable) -> VarCounts -> IntMap Variable
    forall a b. (a -> b) -> a -> b
    $ Term -> VarCounts
    forall a c t.
    (IsVarSet a c, Singleton Variable c, Free t) =>
    t -> c
    freeVars Term
    body
    shouldInline' CompiledClauses
    _ = Bool
    False