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