{-# LANGUAGE DeriveAnyClass       #-}
{-# LANGUAGE DeriveGeneric        #-}
{-# LANGUAGE DerivingStrategies   #-}
{-# LANGUAGE ExplicitNamespaces   #-}
{-# LANGUAGE FlexibleContexts     #-}
{-# LANGUAGE FlexibleInstances    #-}
{-# LANGUAGE MonoLocalBinds       #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE RecordWildCards      #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE StandaloneDeriving   #-}
{-# LANGUAGE UndecidableInstances #-}

module Cleanup (
    Bug (..)
  , DoubleCleanup (..)
  , FinalTest (..)
  , prop_sequential_clean
  , prop_parallel_clean
  , prop_nparallel_clean
  ) where

import           Control.Concurrent.MVar
import           Control.Exception
import           Control.Monad
import           Control.Monad.IO.Class
import           Data.Functor.Classes
                   (Ord1, Show1)
import           Data.List
                   ((\\))
import           Data.Map.Strict
                   (Map)
import qualified Data.Map.Strict               as Map
import           GHC.Generics
                   (Generic, Generic1)
import           Prelude
import           System.Directory
import           System.IO
import           System.Random
import           Test.QuickCheck
import           Test.QuickCheck.Monadic
                   (monadicIO)
import           Test.StateMachine
import qualified Test.StateMachine.Types.Rank2 as Rank2
import           Test.StateMachine.Utils
                   (liftProperty, mkModel, whenFailM)
import           Text.Show.Pretty
                   (ppShow)

{-----------------------------------------------------------------------------------
  This example in mainly used to check how well cleanup of recourses works. In our
  case recourses are files created on the @testDirectory@ (not open handles, just
  files). So it is easy, by the end of the tests to test if there any any recourses
  which are not cleaned up, by the end of the tests.

  We also test different scenarios, like injected exceptions in semantics
  (before and after the recourse is created). Tests also reveal what happens when
  cleaning up a recourse for the second time is not a no-op.

-----------------------------------------------------------------------------------}
data Command r
  = Create String
  | Delete (Reference (Opaque FileRef) r)
  | Ls
  | Write Int
  | Increment
  deriving stock (Eq, Generic1)
  deriving anyclass (Rank2.Functor, Rank2.Foldable, Rank2.Traversable, CommandNames)

deriving stock instance Show (Command Symbolic)
deriving stock instance Read (Command Symbolic)
deriving stock instance Show (Command Concrete)

data Response r
  = Created (Reference (Opaque FileRef) r)
  | Deleted
  | Contents [String]
  | ChangedValue Int
  deriving stock (Eq, Generic1)
  deriving anyclass (Rank2.Foldable)

deriving stock instance Show (Response Symbolic)
deriving stock instance Read (Response Symbolic)
deriving stock instance Show (Response Concrete)

data Model r = Model {
      files            :: Map (Reference (Opaque FileRef) r) String
    , counter          :: Int
    , semanticsCounter :: Opaque (MVar Int)
    , ref              :: Opaque (MVar Int)
    , value            :: Int
  }
  deriving stock (Generic, Show, Eq)

instance ToExpr (Model Symbolic)
instance ToExpr (Model Concrete)

initModel :: MVar Int -> MVar Int -> Model r
initModel sc ref = Model Map.empty 0 (Opaque sc) (Opaque ref) 0

transition :: Ord1 r => Model r -> Command r -> Response r -> Model r
transition m@Model {..} cmd resp = case (cmd, resp) of
    (Create p, Created rf)      -> m {files = Map.insert rf p files, counter = counter + 1}
    (Delete rf, Deleted)        -> m {files = Map.delete rf files}
    (Ls, Contents _)            -> m
    (Write n, ChangedValue _)   -> m {value = n}
    (Increment, ChangedValue _) -> m {value = value + 1}
    _                           -> error "transition impossible"

precondition :: Model Symbolic -> Command Symbolic -> Logic
precondition Model {..} cmd = case cmd of
    Create p  -> Boolean $ notElem p (Map.elems files)
    Delete rf -> Boolean $ Map.member rf files
    Ls        -> Top
    Write _   -> Top
    Increment -> Top

sameElements :: Eq a => [a] -> [a] -> Bool
sameElements x y = null (x \\ y) && null (y \\ x)

postcondition :: Model Concrete -> Command Concrete -> Response Concrete -> Logic
postcondition  Model{..} cmd resp = case (cmd, resp) of
  (Create _,      Created _)  -> Top
  (Delete _, Deleted)         -> Top
  (Ls, Contents ls)           -> if sameElements ls (Map.elems files) then Top
        else Annotate ("Not same elements between " ++ show ls ++ "and " ++ show (Map.elems files)) Bot
  (Increment, ChangedValue _) -> Top
  (Write n, ChangedValue m)   -> m .== n
  _                           -> Bot

data MVarC a = MVarC (MVar a) Int
type FileRef = MVarC (String, Bool)

removeFileRef :: DoubleCleanup -> FileRef -> IO ()
removeFileRef dc (MVarC r _) = modifyMVar_ r $ \(file, isHere) -> do
      case (isHere, dc) of
        (_, ReDo)     -> removeFile file
        (True, _)     -> removeFile file
        (False, NoOp) -> return ()
      return (file, False)

instance Eq (MVarC a) where
    MVarC _ a == MVarC _ b = a == b

instance Ord (MVarC a) where
    compare (MVarC _ a) (MVarC _ b) = compare a b

semantics :: MVar Int -> MVar Int -> String -> Bug -> Command Concrete -> IO (Response Concrete)
semantics counter ref tstDir bug cmd = case cmd of
    Create f  -> createFile f
            `onException` removePathForcibly (makePath tstDir f)
    Delete rf -> do
        let MVarC lockedFile _ = unOpaque $ concrete rf
        modifyMVar_ lockedFile $ \(file, _) -> do
            removeFile file
            return (file, False)
        return Deleted
    Ls        -> do
        ls <- listDirectory tstDir
        return $ Contents ls
    Write n   ->
        modifyMVar ref (\_ -> return (n, ChangedValue n))
    Increment ->
        modifyMVar ref (\m -> return (m + 1, ChangedValue $ m + 1))
    where
        createFile :: String -> IO (Response Concrete)
        createFile f = do
            let path = makePath tstDir f
            c <- modifyMVar counter $ \n -> return (n + 1, n)
            when (c > 3 && bug == Exception) $
                throwIO $ userError "semantics injected bug"
            withFile path WriteMode (\_ -> return ())
            when (c > 3 && bug == ExcAfter) $
                throwIO $ userError "semantics injected bug"
            rf <- newMVar (path, True)
            return $ Created $ reference $ Opaque $ MVarC rf c

mock :: Model Symbolic -> Command Symbolic -> GenSym (Response Symbolic)
mock Model{..} cmd = case cmd of
    Create _  -> Created <$> genSym
    Delete _  -> return Deleted
    Ls        -> return $ Contents $ Map.elems files
    Write n   -> return $ ChangedValue n
    Increment -> return $ ChangedValue $ value + 1

generator :: Model Symbolic -> Maybe (Gen (Command Symbolic))
generator Model{..} = Just $ do
    n <- choose (1,10)
    frequency
        [ (7, return $ Create $ mkFileName counter)
        , (if Map.null files then 0 else 3, Delete . fst <$> elements (Map.toList files))
        , (1, return Ls)
        , (1, return $ Write n)
        , (1, return Increment)
        ]

shrinker :: Model Symbolic -> Command Symbolic -> [Command Symbolic]
shrinker _ _             = []

cleanup :: String -> DoubleCleanup -> Model Concrete -> IO ()
cleanup testDir dc Model{..} = do
    let cl = do
            forM_ (Map.keys files) $ \rf ->
                removeFileRef dc $ unOpaque $ concrete rf
            modifyMVar_ (unOpaque semanticsCounter) (\_ -> return 0)
            modifyMVar_ (unOpaque ref) (\_ -> return 0)
    -- onException here does not affect any tests. It just makes sure
    -- no leftover directories remain after the end of tests.
    -- We have it here, because we found no other way to handle the
    -- exceptions in the ProperyM level.
    cl `onException` removePathForcibly testDir

sm :: MVar Int -> MVar Int -> String -> Bug -> DoubleCleanup -> StateMachine Model Command IO Response
sm counter ref tstDir bug dc = StateMachine (initModel counter ref) transition precondition postcondition
           Nothing generator shrinker (semantics counter ref tstDir bug) mock (cleanup tstDir dc)

smUnused :: StateMachine Model Command IO Response
smUnused = sm undefined undefined undefined undefined undefined

prop_sequential_clean :: FinalTest -> Bug -> DoubleCleanup -> Property
prop_sequential_clean testing bug dc = forAllCommands smUnused Nothing $ \cmds -> monadicIO $ do
    folderId :: Word <- liftIO randomIO
    let testDir = testDirectoryBase ++ "-" ++ show folderId
    liftIO $ do
        removePathForcibly testDir
        createDirectory testDir
    c <- liftIO $ newMVar 0
    ref <- liftIO $ newMVar 0
    let sm' = sm c ref testDir bug dc
    (hist, model, res) <- runCommands sm' cmds
    ls <- liftIO $ listDirectory testDir
    liftIO $ removePathForcibly testDir
    case testing of
        Regular -> prettyCommands sm' hist $ checkCommandNames cmds (res === Ok)
        Files   -> printFiles ls `whenFailM` (ls === [])
        Eq _    -> liftProperty $ mkModel sm' hist === model

prop_parallel_clean :: FinalTest -> Bug -> DoubleCleanup -> Property
prop_parallel_clean testing bug dc = forAllParallelCommands smUnused Nothing $ \cmds -> monadicIO $ do
    folderId :: Word <- liftIO randomIO
    let testDir = testDirectoryBase ++ "-" ++ show folderId
    liftIO $ do
        removePathForcibly testDir
        createDirectory testDir
    c <- liftIO $ newMVar 0
    ref <- liftIO $ newMVar 0
    let sm' = sm c ref testDir bug dc
    ret <- runParallelCommandsNTimes 2 sm' cmds
    ls <- liftIO $ listDirectory testDir
    liftIO $ removePathForcibly testDir
    case testing of
        Regular -> prettyParallelCommands cmds ret
        Files   -> printFiles ls `whenFailM` (ls === [])
        Eq bl   -> do
            let (a, b) = case mkModel sm' . fst <$> ret of
                    (x : y : _) -> (x,y)
                    _           -> error "expected at least two histories"
            liftProperty $ printModels a b `whenFail`
                property (modelEquivalence bl a b)

prop_nparallel_clean :: Int -> FinalTest -> Bug -> DoubleCleanup -> Property
prop_nparallel_clean np testing bug dc = forAllNParallelCommands smUnused np $ \cmds -> monadicIO $ do
    folderId :: Word <- liftIO randomIO
    let testDir = testDirectoryBase ++ "-" ++ show folderId
    liftIO $ do
        removePathForcibly testDir
        createDirectory testDir
    c <- liftIO $ newMVar 0
    ref <- liftIO $ newMVar 0
    let sm' = sm c ref testDir bug dc
    ret <- runNParallelCommandsNTimes 2 sm' cmds
    ls <- liftIO $ listDirectory testDir
    liftIO $ removePathForcibly testDir
    case testing of
        Regular -> prettyNParallelCommands cmds ret
        Files   -> printFiles ls `whenFailM` (ls === [])
        Eq bl   -> do
            let (a, b) = case mkModel sm' . fst <$> ret of
                    (x : y : _) -> (x,y)
                    _           -> error "expected at least two histories"
            liftProperty $ printModels a b `whenFail`
                property (modelEquivalence bl a b)

printModels :: Show1 r => Model r -> Model r -> IO ()
printModels a b =
    putStrLn $ "Models are not equivalent: \n" ++ ppShow a ++ " \nand \n" ++ ppShow b

printFiles :: [String] -> IO ()
printFiles ls' =
    putStrLn $ "Cleanup was not complete. Found files " ++ show ls'

data Bug = NoBug
         | Exception
         | ExcAfter
         deriving stock (Eq, Show)

data DoubleCleanup = NoOp
                   | ReDo
                   deriving stock (Eq, Show)

data FinalTest = Regular
               | Files
               | Eq Bool
                 deriving stock (Eq, Show)

-- | This is meant to be used, in order to test equality of two
-- Models, created by two different executions of the same program.
-- Note that we don't test reference equality. This is because
-- different executions in the parallel case, may create references
-- with different order, so the counter assigned by the semantics
-- can be different.
modelEquivalence :: Bool -> Model Concrete -> Model Concrete -> Bool
modelEquivalence bl a b =
    sameElements (Map.elems $ files a) (Map.elems $ files b)
    && counter a == counter b
    && (not bl || value a == value b)

makePath :: String -> String -> String
makePath tstDir file = tstDir ++ "/" ++ file

mkFileName :: Int -> String
mkFileName n = "file" ++ show n

testDirectoryBase :: String
testDirectoryBase = "cleanup-test-folder"