-- | 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