{-# OPTIONS_GHC -Wunused-imports #-}
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
autoInline :: Defn -> TCM Defn
autoInline :: Defn -> TCM Defn
autoInline Defn
defn = do
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 | inlining, shouldInline defn -> return $ set funInline True defn
| otherwise -> return 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
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 a. [a] -> 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 a. [a] -> 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