    -- | 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.Syntax.Internal
    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 = do
      inlining <- optAutoInline <$> pragmaOptions
      if | inlining, shouldInline defn -> return $ set funInline True defn
         | otherwise                   -> return defn

    shouldInline :: Defn -> Bool
    shouldInline Function{funCompiled = Just cc} = shouldInline' cc
    shouldInline _ = 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' (Done xs body) = all (< 2) counts && length counts < length xs
      where counts = IntMap.elems $ varCounts $ freeVars body
    shouldInline' _ = False