-- | 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) = (Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
2) [Int]
counts Bool -> Bool -> Bool
&& [Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
counts Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [Arg ArgName] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg ArgName]
xs
  where counts :: [Int]
counts = IntMap Int -> [Int]
forall a. IntMap a -> [a]
IntMap.elems (IntMap Int -> [Int]) -> IntMap Int -> [Int]
forall a b. (a -> b) -> a -> b
$ VarCounts -> IntMap Int
varCounts (VarCounts -> IntMap Int) -> VarCounts -> IntMap Int
forall a b. (a -> b) -> a -> b
$ Term -> VarCounts
forall a c t. (IsVarSet a c, Singleton Int c, Free t) => t -> c
freeVars Term
body
shouldInline' CompiledClauses
_ = Bool
False