HaskellCheck.hs

module G2.Translation.HaskellCheck ( validateStates
                                   , runHPC) where

import GHC hiding (Name, entry)
import GHC.Paths

import Data.Either
import Data.List
import qualified Data.Text as T
import Text.Regex
import Unsafe.Coerce

import G2.Initialization.MkCurrExpr
import G2.Interface.OutputTypes
import G2.Language
import G2.Translation.Haskell
import G2.Translation.TransTypes
import G2.Lib.Printers

import Control.Exception

import System.Process

import Control.Monad.IO.Class

validateStates :: [FilePath] -> [FilePath] -> String -> String -> [String] -> [GeneralFlag] -> [ExecRes t] -> IO Bool
validateStates proj src modN entry chAll gflags in_out = do
    return . all id =<< runGhc (Just libdir) (do
        loadToCheck proj src modN gflags
        mapM (runCheck modN entry chAll) in_out)

-- Compile with GHC, and check that the output we got is correct for the input
runCheck :: String -> String -> [String] -> ExecRes t -> Ghc Bool
runCheck modN entry chAll (ExecRes {final_state = s, conc_args = ars, conc_out = out}) = do
    (v, chAllR) <- runCheck' modN entry chAll s ars out

    v' <- liftIO $ (unsafeCoerce v :: IO (Either SomeException Bool))
    let outStr = T.unpack $ printHaskell s out
    let v'' = case v' of
                    Left _ -> outStr == "error"
                    Right b -> b && outStr /= "error"

    chAllR' <- liftIO $ (unsafeCoerce chAllR :: IO [Either SomeException Bool])
    let chAllR'' = rights chAllR'

    return $ v'' && and chAllR''

runCheck' :: String -> String -> [String] -> State t -> [Expr] -> Expr -> Ghc (HValue, [HValue])
runCheck' modN entry chAll s ars out = do
    let Left (v, _) = findFunc (T.pack entry) (Just $ T.pack modN) (expr_env s)
    let e = mkApp $ Var v:ars
    let pg = updatePrettyGuide (exprNames e)
           . updatePrettyGuide (exprNames out)
           $ mkPrettyGuide $ varIds v
    let arsStr = T.unpack $ printHaskellPG pg s e
    let outStr = T.unpack $ printHaskellPG pg s out

    let arsType = T.unpack $ mkTypeHaskell (typeOf e)
        outType = T.unpack $ mkTypeHaskell (typeOf out)

    let chck = case outStr == "error" of
                    False -> "try (evaluate (" ++ arsStr ++ " == " ++ "("
                                    ++ outStr ++ " :: " ++ outType ++ ")" ++ ")) :: IO (Either SomeException Bool)"
                    True -> "try (evaluate ( (" ++ arsStr ++ " :: " ++ arsType ++
                                                    ") == " ++ arsStr ++ ")) :: IO (Either SomeException Bool)"

    v' <- compileExpr chck

    let chArgs = ars ++ [out] 
    let chAllStr = map (\f -> T.unpack $ printHaskellPG pg s $ mkApp ((simpVar $ T.pack f):chArgs)) chAll
    let chAllStr' = map (\str -> "try (evaluate (" ++ str ++ ")) :: IO (Either SomeException Bool)") chAllStr

    chAllR <- mapM compileExpr chAllStr'

    return $ (v', chAllR)

loadToCheck :: [FilePath] -> [FilePath] -> String -> [GeneralFlag] -> Ghc ()
loadToCheck proj src modN gflags = do
        _ <- loadProj Nothing proj src gflags simplTranslationConfig

        let prN = mkModuleName "Prelude"
        let prImD = simpleImportDecl prN

        let exN = mkModuleName "Control.Exception"
        let exImD = simpleImportDecl exN

        let coerceN = mkModuleName "Data.Coerce"
        let coerceImD = simpleImportDecl coerceN

        let charN = mkModuleName "Data.Char"
        let charD = simpleImportDecl charN

        let mdN = mkModuleName modN
        let imD = simpleImportDecl mdN

        setContext [IIDecl prImD, IIDecl exImD, IIDecl coerceImD, IIDecl imD, IIDecl charD]

simpVar :: T.Text -> Expr
simpVar s = Var (Id (Name s Nothing 0 Nothing) TyBottom)

runHPC :: FilePath -> String -> String -> [(State t, Bindings, [Expr], Expr, Maybe FuncCall)] -> IO ()
runHPC src modN entry in_out = do
    let calls = map (\(s, _, i, o, _) -> toCall entry s i o) in_out

    runHPC' src modN calls

-- Compile with GHC, and check that the output we got is correct for the input
runHPC' :: FilePath -> String -> [String] -> IO ()
runHPC' src modN ars = do
    srcCode <- readFile src
    let srcCode' = removeModule modN srcCode

    let spces = "  "

    let chck = intercalate ("\n" ++ spces) $ map (\s -> "print (" ++ s ++ ")") ars

    let mainFunc = "\n\nmain :: IO ()\nmain =do\n" ++ spces ++ chck ++ "\n" ++ spces

    let mainN = "Main_" ++ modN

    writeFile (mainN ++ ".hs") (srcCode' ++ mainFunc)

    callProcess "ghc" ["-fhpc", mainN ++ ".hs"]
    callProcess ("./" ++ mainN) []

    callProcess "hpc" ["report", mainN]

    -- putStrLn mainFunc

toCall :: String -> State t -> [Expr] -> Expr -> String
toCall entry s ars _ = T.unpack . printHaskell s $ mkApp ((simpVar $ T.pack entry):ars)

removeModule :: String -> String -> String
removeModule modN s =
    let
        r = mkRegex $ "module " ++ modN ++ " where"
    in
    subRegex r s ""