module Test.Target.Monad
( whenVerbose
, noteUsed
, addDep
, addConstraint
, addConstructor
, inModule
, making
, lookupCtor
, guarded
, fresh
, freshChoice
, freshInt
, getValue
, Target, runTarget
, TargetState(..), initState
, TargetOpts(..), defaultOpts
) where
import Control.Applicative
import Control.Arrow (first, (***))
import qualified Control.Exception as Ex
import Control.Monad
import Control.Monad.Catch
import Control.Monad.Reader
import Control.Monad.State
import Data.Generics (Data, everywhere, mkT)
import qualified Data.HashMap.Strict as M
import qualified Data.HashSet as S
import Data.IORef
import Data.List hiding (sort)
import Data.Monoid
import qualified Data.Text.Lazy as LT
import Language.Haskell.TH.Lift
import System.IO.Unsafe
import Text.Printf
import Language.Fixpoint.Config (SMTSolver (..))
import Language.Fixpoint.Names
import Language.Fixpoint.Smt.Interface hiding (verbose)
import Language.Fixpoint.Types
import Language.Haskell.Liquid.PredType
import Language.Haskell.Liquid.RefType
import Language.Haskell.Liquid.Tidy
import Language.Haskell.Liquid.Types hiding (var, Target)
import qualified GHC
import Test.Target.Types
import Test.Target.Util
instance Symbolic LT.Text where
symbol = symbol . LT.toStrict
newtype Target a = Target (StateT TargetState (ReaderT TargetOpts IO) a)
deriving ( Functor, Applicative, Monad, MonadIO, Alternative
, MonadState TargetState, MonadCatch, MonadReader TargetOpts )
instance MonadThrow Target where
throwM = Ex.throw
runTarget :: TargetOpts -> TargetState -> Target a -> IO a
runTarget opts st (Target x) = runReaderT (evalStateT x st) opts
seed :: IORef Int
seed = unsafePerformIO $ newIORef 0
freshInt :: Target Int
freshInt = liftIO $ do
n <- readIORef seed
modifyIORef' seed (+1)
return n
data TargetOpts = TargetOpts
{ depth :: !Int
, solver :: !SMTSolver
, verbose :: !Bool
, logging :: !Bool
, keepGoing :: !Bool
, maxSuccess :: !(Maybe Int)
, scDepth :: !Bool
, ghcOpts :: ![String]
}
defaultOpts :: TargetOpts
defaultOpts = TargetOpts
{ depth = 3
, solver = Z3
, verbose = False
, logging = True
, keepGoing = False
, maxSuccess = Nothing
, scDepth = True
, ghcOpts = []
}
data TargetState = TargetState
{ variables :: ![Variable]
, choices :: ![Variable]
, constraints :: !Constraint
, deps :: !(M.HashMap Symbol [Symbol])
, realized :: ![(Symbol, Value)]
, dconEnv :: ![(Symbol, DataConP)]
, ctorEnv :: !DataConEnv
, measEnv :: !MeasureEnv
, embEnv :: !(TCEmb GHC.TyCon)
, tyconInfo :: !(M.HashMap GHC.TyCon RTyCon)
, freesyms :: ![(Symbol,Symbol)]
, constructors :: ![Variable]
, sigs :: ![(Symbol, SpecType)]
, chosen :: !(Maybe Symbol)
, sorts :: !(S.HashSet Sort)
, modName :: !Symbol
, filePath :: !FilePath
, makingTy :: !Sort
, smtContext :: !Context
}
initState :: FilePath -> GhcSpec -> Context -> TargetState
initState fp sp ctx = TargetState
{ variables = []
, choices = []
, constraints = []
, deps = mempty
, realized = []
, dconEnv = dcons
, ctorEnv = cts
, measEnv = meas
, embEnv = tcEmbeds sp
, tyconInfo = tyi
, freesyms = free
, constructors = []
, sigs = sigs
, chosen = Nothing
, sorts = S.empty
, modName = ""
, filePath = fp
, makingTy = FObj ""
, smtContext = ctx
}
where
dcons = tidy $ map (first symbol) (dconsP sp)
cts = tidy $ map (symbol *** val) (ctors sp)
tyi = tidy $ makeTyConInfo (tconsP sp)
free = tidy $ map (symbol *** symbol) $ freeSyms sp
sigs = tidy $ map (symbol *** val) $ tySigs sp
meas = tidy $ measures sp
tidy :: forall a. Data a => a -> a
tidy = everywhere (mkT tidySymbol)
whenVerbose :: Target () -> Target ()
whenVerbose x
= do v <- asks verbose
when v x
noteUsed :: (Symbol, Value) -> Target ()
noteUsed (v,x) = modify $ \s@(TargetState {..}) -> s { realized = (v,x) : realized }
addDep :: Symbol -> Expr -> Target ()
addDep from (EVar to) = modify $ \s@(TargetState {..}) ->
s { deps = M.insertWith (flip (++)) from [to] deps }
addDep _ _ = return ()
addConstraint :: Pred -> Target ()
addConstraint p = modify $ \s@(TargetState {..}) -> s { constraints = p:constraints }
addConstructor :: Variable -> Target ()
addConstructor c
= do
modify $ \s@(TargetState {..}) -> s { constructors = nub $ c:constructors }
inModule :: Symbol -> Target a -> Target a
inModule m act
= do m' <- gets modName
modify $ \s -> s { modName = m }
r <- act
modify $ \s -> s { modName = m' }
return r
making :: Sort -> Target a -> Target a
making ty act
= do ty' <- gets makingTy
modify $ \s -> s { makingTy = ty }
r <- act
modify $ \s -> s { makingTy = ty' }
return r
lookupCtor :: Symbol -> Target SpecType
lookupCtor c
= do mt <- lookup c <$> gets ctorEnv
m <- gets filePath
o <- asks ghcOpts
case mt of
Just t -> return t
Nothing -> do
t <- io $ runGhc o $ do
_ <- loadModule m
t <- GHC.exprType (printf "(%s)" (symbolString c))
return (ofType t)
modify $ \s@(TargetState {..}) -> s { ctorEnv = (c,t) : ctorEnv }
return t
guarded :: String -> Target Expr -> Target (Expr, Expr)
guarded cn act
= do c <- freshChoice cn
mc <- gets chosen
modify $ \s -> s { chosen = Just c }
x <- act
modify $ \s -> s { chosen = mc }
return (x, EVar c)
fresh :: Sort -> Target Symbol
fresh sort
= do n <- freshInt
let sorts' = sortTys sort
modify $ \s@(TargetState {..}) -> s { sorts = S.union (S.fromList (arrowize sort : sorts')) sorts }
let x = symbol $ LT.unpack (LT.intercalate "->" $ map (LT.fromStrict.symbolText.unObj) sorts') ++ show n
modify $ \s@(TargetState {..}) -> s { variables = (x,sort) : variables }
return x
sortTys :: Sort -> [Sort]
sortTys (FFunc _ ts) = concatMap sortTys ts
sortTys t = [t]
arrowize :: Sort -> Sort
arrowize = FObj . symbol . LT.intercalate "->" . map (LT.fromStrict . symbolText . unObj) . sortTys
unObj :: Sort -> Symbol
unObj FInt = "Int"
unObj (FObj s) = s
unObj s = error $ "unObj: " ++ show s
freshChoice :: String -> Target Symbol
freshChoice cn
= do n <- freshInt
modify $ \s@(TargetState {..}) -> s { sorts = S.insert choicesort sorts }
let x = symbol $ LT.unpack (smt2 choicesort) ++ "-" ++ cn ++ "-" ++ show n
modify $ \s@(TargetState {..}) -> s { variables = (x,choicesort) : variables }
return x
getValue :: Symbol -> Target Value
getValue v = do
ctx <- gets smtContext
Values [x] <- io $ ensureValues $ command ctx (GetValue [v])
noteUsed x
return (snd x)
deriveLiftMany [''SMTSolver, ''TargetOpts]