module Data.SBV.Plugin.Plugin(plugin) where
import GhcPlugins
import System.Exit
import Data.Maybe (fromJust)
import Data.List (sortBy)
import Data.Ord (comparing)
import Data.Bits (bitSizeMaybe)
import qualified Data.Map as M
import Data.SBV.Plugin.Common
import Data.SBV.Plugin.Env
import Data.SBV.Plugin.Analyze (analyzeBind)
plugin :: Plugin
plugin = defaultPlugin {installCoreToDos = install}
where install :: [CommandLineOption] -> [CoreToDo] -> CoreM [CoreToDo]
install [] todos = reinitializeGlobals >> return (sbvPass : todos)
install opts _ = do liftIO $ putStrLn $ "[SBV] Unexpected command line options: " ++ show opts
liftIO exitFailure
sbvPass = CoreDoPluginPass "SBV based analysis" pass
pass :: ModGuts -> CoreM ModGuts
pass guts@(ModGuts {mg_binds}) = do
df <- getDynFlags
anns <- getAnnotations deserializeWithData guts
let wsz = fromJust (bitSizeMaybe (0::Int))
baseTCs <- buildTCEnv wsz
baseEnv <- buildFunEnv
baseSpecials <- buildSpecialEnv wsz
let cfg = Config { dflags = df
, opts = []
, wordSize = wsz
, isGHCi = hscTarget df == HscInterpreted
, knownTCs = baseTCs
, knownFuns = baseEnv
, knownSpecials = baseSpecials
, sbvAnnotation = lookupWithDefaultUFM anns [] . varUnique
, allBinds = M.fromList (flattenBinds mg_binds)
}
let bindLoc (NonRec b _) = bindSpan b
bindLoc (Rec []) = noSrcSpan
bindLoc (Rec ((b, _):_)) = bindSpan b
mapM_ (analyzeBind cfg) $ sortBy (comparing bindLoc) mg_binds
return guts