{-# LANGUAGE OverloadedLists #-}
{-# OPTIONS_GHC -fno-warn-incomplete-uni-patterns #-}
module UnitSpec where

import           Abstract (BaseValue(..))
import qualified Concrete as Concrete
--import qualified Data as D
import           UnitAnalysis as U
import           UnitAnalysisValue as U
import           UnitSoundness
--import           GraphToDot

import qualified Data.ByteString.Lazy as LBS
import qualified Data.Abstract.Except as Exc
import           Data.Abstract.MonotoneErrors(toSet)
import           Data.Abstract.Terminating
import qualified Data.HashSet as HashSet
import           Data.Text.Lazy (pack)

import           Language.Wasm
import qualified Language.Wasm.Interpreter as Wasm
import           Language.Wasm.Structure

--import           Numeric.Natural

import           Test.Hspec

main :: IO ()
main = hspec spec

term :: Terminating a -> a
term (Terminating a) = a
term _ = error "not defined"

getFunctionBody :: Function -> Expression
getFunctionBody (Function _ _ b) = b

readModule :: String -> IO ValidModule
readModule path = do
    content <- LBS.readFile path
    let Right m = parse content
    let Right validMod = validate m
    return validMod

runFunc :: String -> String -> [Value] -> IO Result
runFunc modName funcName args = do
    m <- readModule ("test/samples/" ++ modName ++ ".wast")
    Right (modInst, staticS, tabs) <- instantiateAbstract m
    return $ invokeExported staticS tabs modInst (pack funcName) args

checkSoundness :: String -> String -> [[Concrete.Value]] -> IO Bool
checkSoundness m f args = do
    validMod <- readModule ("test/samples/" ++ m ++ ".wast")
    isSoundlyAbstracted validMod f args

succResult :: Result -> [Value]
succResult (_,(_,(Terminating (_,(_,(Exc.Success (_,result))))))) = result
succResult _ = error "not defined"

terminatedSucc :: Result -> Bool
terminatedSucc (_, (errs, Terminating (_,(_,(Exc.Success _))))) = HashSet.null (toSet errs)
terminatedSucc (_, (errs, NonTerminating)) = HashSet.null (toSet errs)
terminatedSucc _ = False

terminatedErr :: Result -> Bool
terminatedErr (_,(errs, NonTerminating)) = not $ HashSet.null (toSet errs)
terminatedErr _ = False

terminatedMaybeErr :: Result -> Bool
terminatedMaybeErr (_,(errs, Terminating (_,(_,(Exc.Success _))))) = not $ HashSet.null (toSet errs)
terminatedMaybeErr _ = False

isNonTerminating :: Result -> Bool
isNonTerminating (_,(_, NonTerminating)) = True
isNonTerminating _ = False

spec :: Spec
spec = do
    it "run fact" $ do
        result <- runFunc "fact" "fac-rec" [Value $ VI64 ()]
        result `shouldSatisfy` terminatedSucc
        (succResult result) `shouldBe` [Value $ VI64 ()]
        let args = [[Concrete.Value $ Wasm.VI64 1],[Concrete.Value $ Wasm.VI64 10]]
        checkSoundness "fact" "fac-rec" args `shouldReturn` True

    it "run test2" $ do
        result <- runFunc "simple" "test2" []
        result `shouldSatisfy` terminatedSucc
        (succResult result) `shouldBe` [Value $ VI32 ()]
        checkSoundness "simple" "test2" [[]] `shouldReturn` True


    it "run test-br3" $ do
        result <- runFunc "simple" "test-br3" [Value $ VI32 ()]
        result `shouldSatisfy` terminatedSucc
        (succResult result) `shouldBe` [Value $ VI32 ()]
        let args = [[Concrete.Value $ Wasm.VI32 10]]
        checkSoundness "simple" "test-br3" args `shouldReturn` True

    it "run test-call-indirect" $ do
        result <- runFunc "simple" "test-call-indirect" []
        result `shouldSatisfy` terminatedMaybeErr
        (succResult result) `shouldBe` [Value $ VI32 ()]
        checkSoundness "simple" "test-call-indirect" [[]] `shouldReturn` True

    it "run non-terminating" $ do
        result <- runFunc "simple" "non-terminating" []
        result `shouldSatisfy` terminatedSucc
        result `shouldSatisfy` isNonTerminating

    it "run maybe-non-terminating" $ do
        let args = [[Concrete.Value $ Wasm.VI32 42]]
        checkSoundness "simple" "maybe-non-terminating" args `shouldReturn` True

    it "run test-unreachable" $ do
        result <- runFunc "simple" "test-unreachable" []
        (succResult result) `shouldBe` [Value $ VI32 ()]
        checkSoundness "simple" "test-unreachable" [[]] `shouldReturn` True

    it "run test-unreachable2" $ do
        checkSoundness "simple" "test-unreachable2" [[]] `shouldReturn` True

    it "run test-unreachable3" $ do
        checkSoundness "simple" "test-unreachable3" [[]] `shouldReturn` True

    it "run test-unreachable4" $ do
        checkSoundness "simple" "test-unreachable4" [[]] `shouldReturn` True

    it "run test-unreachable5" $ do
        checkSoundness "simple" "test-unreachable4" [[]] `shouldReturn` True

    it "run test-br-and-return" $ do
        let args = [[Concrete.Value $ Wasm.VI32 10]]
        checkSoundness "simple" "test-br-and-return" args `shouldReturn` True

    it "run test-br-and-return2" $ do
        let args = [[Concrete.Value $ Wasm.VI32 10]]
        checkSoundness "simple" "test-br-and-return2" args `shouldReturn` True

    it "run test-br-and-return3" $ do
        let args = [[Concrete.Value $ Wasm.VI32 10]]
        checkSoundness "simple" "test-br-and-return3" args `shouldReturn` True

--    it "print cfg" $ do
--        result <- runFunc "fact" "fac-rec" [Value $ VI64 ()]
--        let cfg = fst result
--        putStrLn (show cfg)
--        putStrLn $ graphToDot showForGraph cfg
--        pending
--
--
--showForGraph :: D.Instruction Natural -> String
--showForGraph (D.I32Const i _) = "I32Const " ++ (show i)
--showForGraph (D.I64Const i _) = "I64Const " ++ (show i)
--showForGraph (D.GetLocal n _) = "GetLocal " ++ (show n)
--showForGraph (D.IRelOp bs op _) = "IRelOp " ++ (show bs) ++ " " ++ (show op)
--showForGraph (D.IBinOp bs op _) = "IBinOp " ++ (show bs) ++ " " ++ (show op)
--showForGraph (D.Call i _) = "Call " ++ (show i)
--showForGraph (D.If t _ _ _) = "If " ++ (show t)
--showForGraph _ = error "todo"
