content: {-# LANGUAGE OverloadedStrings    #-}
  {-# LANGUAGE FlexibleContexts     #-}
  {-# OPTIONS_GHC -Wno-orphans #-}
  
  module Main where
  
  import qualified Control.Concurrent.STM as STM
  import qualified Data.Functor.Compose   as Functor
  import qualified Data.IntMap            as IntMap
  import Control.Monad (when)
  import qualified Control.Monad.State    as State
  import Control.Monad.Trans.Class (lift)
  import Data.List (isSuffixOf)
  import Prelude hiding (log)
  import Data.Maybe (fromMaybe)
  import Data.Monoid (Sum(..))
  import Data.Proxy
  import Data.Tagged
  import Control.Applicative
  import Options.Applicative
  import System.Directory
  import System.Exit
  import System.FilePath
  import System.IO
  import System.IO.Error
  import System.Process
  import Text.Printf
  
  import Test.Tasty
  import Test.Tasty.HUnit
  import Test.Tasty.Ingredients.Rerun
  import Test.Tasty.Options
  import Test.Tasty.Runners
  import Test.Tasty.Runners.AntXML
  
  main :: IO ()
  main    = do
    lfDir <- findLiquidFixpointDir
    run lfDir =<< group "Tests" [unitTests lfDir]
    where
      run lfDir = defaultMainWithIngredients
                [ testRunner lfDir
                , includingOptions [ Option (Proxy :: Proxy FixpointOpts) ]
                ]
  
  -- | Searches for the directory of liquid-fixpoint.cabal and changes to it
  findLiquidFixpointDir :: IO FilePath
  findLiquidFixpointDir = do
      dir0 <- getCurrentDirectory
      let candidates = [dir0, dir0 </> "liquid-fixpoint"]
          findCabalDir :: [FilePath] -> IO (Maybe FilePath)
          findCabalDir [] = return Nothing
          findCabalDir (d:xs) = do
            let cabalFile = d </> "liquid-fixpoint.cabal"
            exists <- doesFileExist cabalFile
            if exists then
              return (Just d)
             else
              findCabalDir xs
      mDir <- findCabalDir candidates
      case mDir of
        Just d  -> return d
        Nothing -> error "Could not find liquid-fixpoint.cabal"
  
  testRunner :: FilePath -> Ingredient
  testRunner lfDir = rerunningTests
                 [ listingTests
                 , combineReporters (myConsoleReporter lfDir) antXMLRunner
                 , myConsoleReporter lfDir
                 ]
  
  myConsoleReporter :: FilePath -> Ingredient
  myConsoleReporter lfDir = combineReporters consoleTestReporter (loggingTestReporter lfDir)
  
  -- | Combine two @TestReporter@s into one.
  --
  -- Runs the reporters in sequence, so it's best to start with the one
  -- that will produce incremental output, e.g. 'consoleTestReporter'.
  combineReporters :: Ingredient -> Ingredient -> Ingredient
  combineReporters (TestReporter opts1 run1) (TestReporter opts2 run2)
    = TestReporter (opts1 ++ opts2) $ \opts tree -> do
        f1 <- run1 opts tree
        f2 <- run2 opts tree
        return $ \smap -> f1 smap >> f2 smap
  combineReporters _ _ = error "combineReporters needs TestReporters"
  
  unitTests :: FilePath -> IO TestTree
  unitTests lfDir
    = group "Unit" [
        testGroup "native-pos" <$> dirTests nativeCmd "tests/pos"    skipNativePos  ExitSuccess
      , testGroup "native-neg" <$> dirTests nativeCmd "tests/neg"    ["float.fq"]   (ExitFailure 1)
      , testGroup "elim-crash" <$> dirTests nativeCmd "tests/crash"  []             (ExitFailure 1)
      , testGroup "elim-pos1"  <$> dirTests elimCmd   "tests/pos"    []             ExitSuccess
      , testGroup "elim-pos2"  <$> dirTests elimCmd   "tests/elim"   []             ExitSuccess
      , testGroup "elim-neg"   <$> dirTests elimCmd   "tests/neg"    ["float.fq"]   (ExitFailure 1)
      , testGroup "elim-crash" <$> dirTests elimCmd   "tests/crash"  []             (ExitFailure 1)
      , testGroup "cvc5-pos"   <$> dirTests cvc5Cmd   "tests/pos"    skipNativePos  ExitSuccess
      , testGroup "proof"      <$> dirTests elimCmd   "tests/proof"     []          ExitSuccess
      , testGroup "rankN"      <$> dirTests elimCmd   "tests/rankNTypes" []         ExitSuccess
      , testGroup "horn-pos-el"      <$> dirTests elimSaveCmd   "tests/horn/pos"  []          ExitSuccess
      , testGroup "horn-pos-cvc5"    <$> dirTests cvc5Cmd       "tests/horn/pos"  []          ExitSuccess
      , testGroup "horn-neg-el"      <$> dirTests elimSaveCmd   "tests/horn/neg"  []          (ExitFailure 1)
      , testGroup "horn-neg-cvc5"    <$> dirTests cvc5Cmd       "tests/horn/neg"  []          (ExitFailure 1)
      , testGroup "horn-json-pos-el" <$> dirJsonTests elimCmd   "tests/horn/pos/.liquid"  []  ExitSuccess
      , testGroup "horn-json-neg-el" <$> dirJsonTests elimCmd   "tests/horn/neg/.liquid"  []  (ExitFailure 1)
      , testGroup "horn-smt2-pos-el" <$> dirHornTests elimCmd  "tests/horn/pos/.liquid"  []  ExitSuccess
      , testGroup "horn-smt2-neg-el" <$> dirHornTests elimCmd  "tests/horn/neg/.liquid"  []  (ExitFailure 1)
      , testGroup "horn-pos-na"      <$> dirTests nativeCmd     "tests/horn/pos"  []          ExitSuccess
      , testGroup "horn-neg-na"      <$> dirTests nativeCmd     "tests/horn/neg"  []          (ExitFailure 1)
     ]
     where
      dirTests     = dirTests' isTest
      dirJsonTests = dirTests' ("horn.json" `isSuffixOf`)
      dirHornTests = dirTests' ("horn.smt2" `isSuffixOf`)
  
      dirTests' :: (FilePath -> Bool) -> TestCmd -> FilePath -> [FilePath] -> ExitCode -> IO [TestTree]
      dirTests' isT testCmd root ignored code = do
        let absRoot = lfDir </> root
        files    <- walkDirectory absRoot
        let tests = [ rel | f <- files, isT f, let rel = makeRelative absRoot f, rel `notElem` ignored ]
        return    $ mkTest testCmd code absRoot <$> tests
  
  isTest   :: FilePath -> Bool
  isTest f = takeExtension f `elem` [".fq", ".smt2"]
  
  skipNativePos :: [FilePath]
  skipNativePos = ["NonLinear-pack.fq"]
  
  newtype FixpointOpts = LO String deriving (Show, Read, Eq, Ord)
  
  instance Semigroup FixpointOpts where
    (LO "") <> y       = y
    x       <> (LO "") = x
    (LO x)  <> (LO y)  = LO $ x ++ (' ' : y)
  
  instance Monoid FixpointOpts where
    mempty = LO ""
    mappend = (<>)
  
  instance IsOption FixpointOpts where
    defaultValue = LO ""
    parseValue = Just . LO
    optionName = return "fixpoint-opts"
    optionHelp = return "Extra options to pass to fixpoint"
    optionCLParser =
      option (fmap LO str)
        (  long (untag (optionName :: Tagged FixpointOpts String))
        <> help (untag (optionHelp :: Tagged FixpointOpts String))
        )
  
  ---------------------------------------------------------------------------
  mkTest :: TestCmd -> ExitCode -> FilePath -> FilePath -> TestTree
  ---------------------------------------------------------------------------
  mkTest testCmd code dir file
    =
      askOption $ \opts ->
      testCase file $
        if test `elem` knownToFail
        then do
          printf "%s is known to fail: SKIPPING" test
          assertEqual "" True True
        else do
          createDirectoryIfMissing True $ takeDirectory log
          c <- withFile log WriteMode $ \h -> do
            let cmd     = testCmd opts "fixpoint" dir file
            (_,_,_,ph) <- createProcess $ (shell cmd) {std_out = UseHandle h, std_err = UseHandle h}
            waitForProcess ph
          when (code /= c) $
            readFile log >>= putStrLn
          assertEqual "Wrong exit code" code c
  
    where
      test = dir </> file
      log  = let (d,f) = splitFileName file in dir </> d </> ".liquid" </> f <.> "log"
  
  knownToFail :: [a]
  knownToFail = []
  ---------------------------------------------------------------------------
  type TestCmd = FixpointOpts -> FilePath -> FilePath -> FilePath -> String
  
  nativeCmd :: TestCmd
  nativeCmd (LO opts) bin dir file =
    printf "cd %s && %s %s %s" dir bin opts file
  
  elimCmd :: TestCmd
  elimCmd (LO opts) bin dir file =
    printf "cd %s && %s --eliminate=some %s %s" dir bin opts file
  
  elimSaveCmd :: TestCmd
  elimSaveCmd (LO opts) bin dir file =
    printf "cd %s && %s --save --eliminate=some %s %s" dir bin opts file
  
  cvc5Cmd :: TestCmd
  cvc5Cmd (LO opts) bin dir file =
    printf "cd %s && %s --solver=cvc5 %s %s" dir bin opts file
  
  cvc5SaveCmd :: TestCmd
  cvc5SaveCmd (LO opts) bin dir file =
    printf "cd %s && %s --save --solver=cvc5 %s %s" dir bin opts file
  
  ----------------------------------------------------------------------------------------
  -- Generic Helpers
  ----------------------------------------------------------------------------------------
  
  group :: Monad f => TestName -> [f TestTree] -> f TestTree
  group n xs = testGroup n <$> sequence xs
  
  ----------------------------------------------------------------------------------------
  walkDirectory :: FilePath -> IO [FilePath]
  ----------------------------------------------------------------------------------------
  walkDirectory root
    = do (ds,fs) <- partitionM doesDirectoryExist . candidates =<< (getDirectoryContents root `catchIOError` const (return []))
         (fs++) <$> concatMapM walkDirectory ds
    where
      candidates fs = [root </> f | f@(c:_) <- fs, not (isExtSeparator c)]
  
  partitionM :: Monad m => (a -> m Bool) -> [a] -> m ([a],[a])
  partitionM f = go [] []
    where
      go ls rs []     = return (ls,rs)
      go ls rs (x:xs) = do b <- f x
                           if b then go (x:ls) rs xs
                                else go ls (x:rs) xs
  
  -- isDirectory :: FilePath -> IO Bool
  -- isDirectory = fmap Posix.isDirectory . Posix.getFileStatus
  
  concatMapM :: Applicative m => (a -> m [b]) -> [a] -> m [b]
  concatMapM _ []     = pure []
  concatMapM f (x:xs) = (++) <$> f x <*> concatMapM f xs
  
  
  
  -- this is largely based on ocharles' test runner at
  -- https://github.com/ocharles/tasty-ant-xml/blob/master/Test/Tasty/Runners/AntXML.hs#L65
  loggingTestReporter :: FilePath -> Ingredient
  loggingTestReporter lfDir = TestReporter [] $ \opts tree -> Just $ \smap -> do
    let
      runTest _ testName _ = Traversal $ Functor.Compose $ do
          i <- State.get
  
          summary <- lift $ STM.atomically $ do
            status <- STM.readTVar $
              fromMaybe (error "Attempted to lookup test by index outside bounds") $
                IntMap.lookup i smap
  
            let mkSuccess time = [(testName, time, True)]
                mkFailure time = [(testName, time, False)]
  
            case status of
              -- If the test is done, generate a summary for it
              Done result
                | resultSuccessful result
                    -> pure (mkSuccess (resultTime result))
                | otherwise
                    -> pure (mkFailure (resultTime result))
              -- Otherwise the test has either not been started or is currently
              -- executing
              _ -> STM.retry
  
          Const summary <$ State.modify (+ 1)
  
      runGroup _ group' children = Traversal $ Functor.Compose $ do
        Const soFar <- Functor.getCompose $ getTraversal $ mconcat children
        pure $ Const $ map (\(n,t,s) -> (group' </> n,t,s)) soFar
  
      computeFailures :: StatusMap -> IO Int
      computeFailures = fmap getSum . getApp . foldMap (\var -> Ap $
        (\r -> Sum $ if resultSuccessful r then 0 else 1) <$> getResultFromTVar var)
  
      getResultFromTVar :: STM.TVar Status -> IO Result
      getResultFromTVar var =
        STM.atomically $ do
          status <- STM.readTVar var
          case status of
            Done r -> return r
            _ -> STM.retry
  
    (Const summary, _tests) <-
       flip State.runStateT 0 $ Functor.getCompose $ getTraversal $
        foldTestTree
          trivialFold { foldSingle = runTest, foldGroup = runGroup }
          opts
          tree
  
    return $ \_elapsedTime -> do
      -- don't use the `time` package, major api differences between ghc 708 and 710
      -- build header
      ref <- gitRef
      timestamp <- gitTimestamp
      epochTime <- gitEpochTimestamp
      hash <- gitHash
      let hdr = unlines [ref ++ " : " ++ hash,
                         "Timestamp: " ++ timestamp,
                         "Epoch Timestamp: " ++ epochTime,
                         headerDelim,
                         "test, time(s), result"]
  
  
      let smry = lfDir </> "tests" </> "logs" </> "cur" </> "summary.csv"
      writeFile smry $ unlines
                     $ hdr
                     : map (\(n, t, r) -> printf "%s, %0.4f, %s" n t (show r)) summary
      (==0) <$> computeFailures smap
  
  
  gitTimestamp :: IO String
  gitTimestamp = do
     res <- gitProcess ["show", "--format=\"%ci\"", "--quiet"]
     return $ filter notNoise res
  
  gitEpochTimestamp :: IO String
  gitEpochTimestamp = do
     res <- gitProcess ["show", "--format=\"%ct\"", "--quiet"]
     return $ filter notNoise res
  
  gitHash :: IO String
  gitHash = do
     res <- gitProcess ["show", "--format=\"%H\"", "--quiet"]
     return $ filter notNoise res
  
  gitRef :: IO String
  gitRef = do
     res <- gitProcess ["show", "--format=\"%d\"", "--quiet"]
     return $ filter notNoise res
  
  -- | Calls `git` for info; returns `"plain"` if we are not in a git directory.
  gitProcess :: [String] -> IO String
  gitProcess args = readProcess "git" args [] `catchIOError` const (return "plain")
  
  notNoise :: Char -> Bool
  notNoise a = a /= '\"' && a /= '\n' && a /= '\r'
  
  headerDelim :: String
  headerDelim = replicate 80 '-'
  