content: {-# 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"
  