{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE OverloadedLists #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
module TypedAnalysisSpec where

import           Prelude hiding (succ,pred,id)

import           Control.Monad(forM_)
import           Control.Arrow.Transformer.Abstract.Fix.Metrics
import           Control.Arrow.Transformer.Abstract.Fix.ControlFlow

import           Data.GraphViz hiding (diamond)
import           Data.Text(Text)
import           Data.HashSet(HashSet)

import           Data.Abstract.Terminating hiding (toEither)
import           Data.Abstract.MonotoneErrors (toSet)
import qualified Data.Abstract.Boolean as B

import           GHC.Exts

import           System.Directory

import           Syntax as S hiding (Nil)
import           Parser(loadSchemeFile)
import           TypedAnalysis
import           TypedAnalysis.Chaotic(evalInner',evalOuter')
import           TypedAnalysis.Parallel(evalParallel',evalADI')

import           Text.Printf

import           Test.Hspec

main :: IO ()
main = hspec spec

spec :: Spec
spec =
  beforeAll (writeFile metricFile (printf "Function,Algorithm,%s\n" csvHeader)) $ do
    describe "Benchmarks" $ testFixpointAlgorithms benchmarks
    describe "Tests" $ testFixpointAlgorithms customTests

testFixpointAlgorithms :: ((?algorithm :: Algorithm) => Runner -> Spec) -> Spec
testFixpointAlgorithms tests = do
  describe "Chaotic" $ do
    describe "Innermost" $ let ?algorithm = ChaoticInner in tests (runner evalInner')
    describe "Outermost" $ let ?algorithm = ChaoticOuter in tests (runner evalOuter')
  describe "Parallel" $ let ?algorithm = Parallel in tests (runner evalParallel')
  describe "ADI" $ let ?algorithm = ADI in tests (runner evalADI')

benchmarks :: (?algorithm :: Algorithm) => Runner -> Spec
benchmarks run = do
  gabrielBenchmarks run
  scalaAM run

data Algorithm = ChaoticInner | ChaoticOuter | Parallel | ADI deriving (Show,Eq)

-----------------GABRIEL BENCHMARKS---------------------------------------------
gabrielBenchmarks :: (?algorithm :: Algorithm) => Runner -> Spec
gabrielBenchmarks run = describe "Gabriel" $ do
-- TIMEOUT = 30s

    it "boyer" $ do
      let inFile = "gabriel/boyer.scm"
      let expRes = successOrFail (return (BoolVal B.Top))
                                 [ "Excpeted list as argument for cdr, but got Top"
                                 , "Excpeted list as argument for car, but got Top"
                                 ]
      run inFile expRes

    it "browse" $ do
      let inFile = "gabriel/browse.scm"
      let expRes = successOrFail (return (NumVal IntVal))
                                 [ "error: (length): contract violation, expected list"
                                 , "Excpeted list as argument for cdr, but got Top"
                                 , "Excpeted list as argument for car, but got Top"
                                 , "expected a quote as argument for symbol->string, but got Top"
                                 ]
      run inFile expRes

    it "cpstak" $ do
      -- TIME: 105 | STATES: 120
      let inFile = "gabriel/cpstak.scm"
      let expRes = success (NumVal IntVal)
      run inFile expRes

    it "destruc" $ do
      let inFile = "gabriel/destruc.scm"
      let expRes = successOrFail (Terminating (BoolVal B.Top)) $
                                 [ "Excpeted list as argument for cdr, but got Top"
                                 , "Excpeted list as argument for car, but got Top"
                                 ]
                                 -- <>
                                 -- when (?algorithm == Parallel || ?algorithm == ADI)
                                 -- [ "cannot car an empty list" ]
      run inFile expRes

    it "dderiv" $ do
      pendingWith "The analysis is too imprecise to typecheck. \
                  \The analysis tries to call a function, whose closure is top. \
                  \Continuing at this point would be unsound because the analysis\
                  \would not soundly approximate the control-flow of the program."
      let inFile = "gabriel/dderiv.scm"
      let expRes = success (BoolVal B.True)
      run inFile expRes

    it "deriv" $ do
--     => TIMEOUT | STATES: 1645737
      -- when (?algorithm == Parallel || ?algorithm == ADI) $
      --   pendingWith "out of memory"

      let inFile = "gabriel/deriv.scm"
      let expRes = successOrFail (return (BoolVal B.Top))
                                 -- because (equals? (list 1 2) (list 1 2)) recursively calls (equals? 1 1)
                                 [ "error: No derivation method available"
                                 , "error: Cannot map over a non-list"
                                 , "Excpeted list as argument for cdr, but got Top"
                                 , "Excpeted list as argument for car, but got Top"
                                 ]
      run inFile expRes

    it "diviter" $ do
--     => Final Values: Set(#f, {#f,#t})
--     => TIME: 163 | STATES: 175
      -- pendingWith "out of memory"
      let inFile = "gabriel/diviter.scm"
      -- let expRes = Terminating (Success $ fromList [Bottom, BoolVal B.Top])
      let expRes = successOrFail (Terminating (BoolVal B.Top)) []
      run inFile expRes

    it "divrec" $ do
--       => Final Values: Set(#f, {#f,#t})
--       => TIME: 59 | STATES: 219
      -- pendingWith "out of memory"
      let inFile = "gabriel/divrec.scm"
      -- let expRes = Terminating (Success $ fromList [Bottom, BoolVal B.Top])
      let expRes = success (BoolVal B.Top)
      run inFile expRes

    it "takl" $ do
-- => TIMEOUT | STATES: 1959438
      let inFile = "gabriel/takl.scm"
      let expRes = successOrFail (return (BoolVal B.Top))
                                 -- because (equals? (list 1 2) (list 1 2)) recursively calls (equals? 1 1)
                                 [ "Excpeted list as argument for cdr, but got Top"
                                 , "Excpeted list as argument for car, but got Top"
                                 ]
      run inFile expRes

-- -------------------SCALA-AM BENCHMARKS------------------------------------------
scalaAM :: (?algorithm :: Algorithm) => Runner -> Spec
scalaAM run = describe "Scala-AM" $ do
    it "collatz" $ do
-- => Final Values: Set(Int)
-- => TIME: 8 | STATES: 431
      let inFile = "scala-am/collatz.scm"
      let expRes = success $ NumVal IntVal
      run inFile expRes

    it "gcipd" $ do
--       => Final Values: Set(Int)
--       => TIME: 14 | STATES: 1098
      let inFile = "scala-am/gcipd.scm"
      let expRes = success $ NumVal IntVal
      run inFile expRes

    it "nqueens" $ do
-- => TIMEOUT | STATES: 1781142
      let inFile = "scala-am/nqueens.scm"
      let expRes = success $ NumVal IntVal
      run inFile expRes

    it "primtest" $ do
-- => Final Values: Set(Int)
-- => TIME: 8 | STATES: 431
      -- pendingWith "not getting parsed yet"
      let inFile = "scala-am/primtest.scm"
      let expRes = success $ NumVal IntVal
      run inFile expRes

    it "rsa" $ do
-- => Final Values: Set({#f,#t})
-- => TIME: 2831 | STATES: 247915
      -- pendingWith "only works for parallel, but parallel broken?"
      let inFile = "scala-am/rsa.scm"
      let expRes = successOrFail (return (BoolVal B.Top))
                                 [ "error: Not a legal public exponent for that modulus."
                                 , "error: The modulus is too small to encrypt the message."
                                 ]
      run inFile expRes

-- -------------------Custom Tests------------------------------------------
customTests :: (?algorithm :: Algorithm) => Runner -> Spec
customTests run = do
    it "recursion_union_empty_list" $ do
      let inFile = "test_rec_empty.scm"
      let expRes = success (ListVal Nil)
      run inFile expRes

    it "recursion and union with non-empty list" $ do
      let inFile = "test_rec_nonempty.scm"
      let expRes = success $ NumVal IntVal
      run inFile expRes

    it "should return NV for (car (cdr '(2 3 4)))" $ do
      let inFile = "test_cdr.scm"
      let expRes = success $ NumVal IntVal
      run inFile expRes

    it "should return correct val for car" $ do
      let inFile = "test_car.scm"
      let expRes = success $ NumVal IntVal
      run inFile expRes

    it "test_null_cdr" $ do
      let inFile = "test_null.scm"
      let expRes = success (BoolVal B.True)
      run inFile expRes

    it "unifying two list of nums of different size should result in list of nums" $ do
      let inFile = "test_faulty_list.scm"
      let expRes = success Top
      run inFile expRes

    it "test_if" $ do
      let inFile = "test_if.scm"
      let expRes = success (BoolVal B.False)
      run inFile expRes

    it "test_opvars" $ do
      let inFile = "test_opvars.scm"
      let expRes = success $ NumVal IntVal
      run inFile expRes

    it "test_equal" $ do
      let inFile = "test_equal.scm"
      -- Higher sensitivity leads to BoolVal B.True
      let expRes = successOrFail (return (BoolVal B.Top)) ["Excpeted list as argument for cdr, but got Top","Excpeted list as argument for car, but got Top"]
      run inFile expRes

    it "test_cons" $ do
      let inFile = "test_cons.scm"
      let expRes = success (BoolVal B.True)
      run inFile expRes

    it "test_closure_gc" $ do
      let inFile = "test_closure_gc.scm"
      let expRes = success $ NumVal IntVal
      run inFile expRes

    it "lang_scheme_test" $ do
      let inFile = "lang_scheme_test.scm"
      let expRes = success $ NumVal IntVal
      run inFile expRes

    it "test_inner_define" $ do
      let inFile = "test_inner_define.scm"
      let expRes = success $ NumVal IntVal
      run inFile expRes

    it "test_unops" $ do
      let inFile = "test_unops.scm"
      let expRes = success (BoolVal B.Top)
      run inFile expRes

    it "test_eq" $ do
      let inFile = "test_eq.scm"
      let expRes = success (BoolVal B.Top)
      run inFile expRes

    it "test_binops" $ do
      let inFile = "test_binops.scm"
      let expRes = successOrFail NonTerminating ["expected a two ints as arguments for quotient , but got [Top,Int]","expected a two ints as arguments for quotient , but got [True,string]"]
      run inFile expRes

    it "test_opvar_numbool" $ do
      let inFile = "test_opvar_numbool.scm"
      let expRes = successOrFail NonTerminating ["expected a numbers as argument for <, but got [string,string]"]
      run inFile expRes

    it "test_opvar_numnum" $ do
      let inFile = "test_opvar_numnum.scm"
      let expRes = successOrFail (return Top) ["expected a numbers as argument for +, but got [Int,Top]"]
      run inFile expRes

    it "test_opvar_boolbool" $ do
      let inFile = "test_opvar_boolbool.scm"
      let expRes = success $ BoolVal B.True
      run inFile expRes

    it "test_list" $ do
      let inFile = "test_list.scm"
      let expRes = success $ QuoteVal ["+"]
      run inFile expRes

    it "test_factorial" $ do
      let inFile = "test_factorial.scm"
      let expRes = success $ NumVal IntVal
      run inFile expRes

    it "test_symbols" $ do
      let inFile = "test_symbols.scm"
      let expRes = success $ QuoteVal ["sym1", "sym2", "sym3"]
      run inFile expRes

    it "test_random" $ do
      let inFile = "test_random.scm"
      let expRes = success $ NumVal IntVal
      run inFile expRes

success :: Val -> (HashSet Text, Terminating Val)
success v = ([],Terminating v)

successOrFail :: Terminating Val -> HashSet Text -> (HashSet Text, Terminating Val)
successOrFail v errs = (errs, v)

type Runner = (String -> (HashSet Text, Terminating Val) -> IO ())

metricFile :: String
metricFile = "metrics.csv"

runner :: (?algorithm :: Algorithm) => Eval' -> Runner
runner eval inFile expected = do
  prog <- loadSchemeFile inFile
  let ?sensitivity = 0
  let (cfg,(Monotone metric,(errs,res))) = eval [prog]
  let csv = printf "\"%s\",%s,%s\n" inFile (show ?algorithm) (toCSV metric)
  appendFile metricFile csv
  renderCFG inFile cfg
  (toSet errs, res) `shouldBe` expected

renderCFG :: String -> CFG Expr -> IO ()
renderCFG inFile (CFG graph) = do
  let dotGraph = graphToDot fileGraphParams graph
  root <- getCurrentDirectory
  forM_ (["gabriel", "scala-am"] :: [FilePath]) $ \dir ->
    createDirectoryIfMissing True (root ++ "/graph_files/" ++ dir)
  let outPath = root ++ "/graph_files/" ++ inFile ++ ".png"
  _ <- runGraphvizCommand Dot dotGraph Png outPath
  return ()

-- visualize node labels (expr) as actual node labels
fileGraphParams :: GraphvizParams Int Expr () () Expr
fileGraphParams = defaultParams {fmtNode = \(_, vl) -> [toLabel vl]}

when :: IsList l => Bool -> l -> l
when True l = l
when False _ = fromList []
