    -- | 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
      Bool
    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 | Bool
    inlining, Defn -> Bool
    shouldInline Defn
    defn -> Defn -> TCM Defn
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Defn -> TCM Defn) -> Defn -> TCM Defn
    forall a b. (a -> b) -> a -> b
    $ Lens' Bool Defn -> LensSet Bool Defn
    forall i o. Lens' i o -> LensSet i o
    set Lens' Bool Defn
    funInline Bool
    True Defn
    defn
         | Bool
    otherwise                   -> Defn -> TCM Defn
    forall (m :: * -> *) a. Monad m => a -> m a
    return Defn
    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 (t :: * -> *) a. Foldable t => t a -> Variable
    length [Variable]
    counts Variable -> Variable -> Bool
    forall a. Ord a => a -> a -> Bool
    < [Arg ArgName] -> 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