-- | 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  if | Bool
inlining, Defn -> Bool
shouldInline Defn
defn -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall i o. Lens' i o -> LensSet i o
set Lens' Bool Defn
funInline Bool
True Defn
defn
     | Bool
otherwise                   -> 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) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Ord a => a -> a -> Bool
< Variable
2) [Variable]
counts Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Variable
length [Variable]
counts forall a. Ord a => a -> a -> Bool
< forall (t :: * -> *) a. Foldable t => t a -> Variable
length [Arg ArgName]
xs
  where counts :: [Variable]
counts = forall a. IntMap a -> [a]
IntMap.elems forall a b. (a -> b) -> a -> b
$ VarCounts -> IntMap Variable
varCounts forall a b. (a -> b) -> a -> b
$ forall a c t.
(IsVarSet a c, Singleton Variable c, Free t) =>
t -> c
freeVars Term
body
shouldInline' CompiledClauses
_ = Bool
False