content: {-# LANGUAGE DataKinds                  #-}
  {-# LANGUAGE DeriveGeneric              #-}
  {-# LANGUAGE DerivingStrategies         #-}
  {-# LANGUAGE FlexibleContexts           #-}
  {-# LANGUAGE FlexibleInstances          #-}
  {-# LANGUAGE GADTs                      #-}
  {-# LANGUAGE GeneralizedNewtypeDeriving #-}
  {-# LANGUAGE LambdaCase                 #-}
  {-# LANGUAGE MultiParamTypeClasses      #-}
  {-# LANGUAGE OverloadedStrings          #-}
  {-# LANGUAGE PolyKinds                  #-}
  {-# LANGUAGE QuasiQuotes                #-}
  {-# LANGUAGE ScopedTypeVariables        #-}
  {-# LANGUAGE StandaloneDeriving         #-}
  {-# LANGUAGE TemplateHaskell            #-}
  {-# LANGUAGE TypeFamilies               #-}
  {-# LANGUAGE TypeOperators              #-}
  {-# LANGUAGE UndecidableInstances       #-}
  {-# OPTIONS_GHC -Wno-redundant-constraints #-}
  
  -- NOTE: Make sure NOT to use DeriveAnyClass, or persistent-template
  -- will do the wrong thing.
  
  ------------------------------------------------------------------------
  -- |
  -- Module      :  CrudWebserverDb
  -- Copyright   :  (C) 2016, James M.C. Haver II, Sönke Hahn;
  --                (C) 2017-2018, Stevan Andjelkovic
  -- License     :  BSD-style (see the file LICENSE)
  --
  -- Maintainer  :  Stevan Andjelkovic <stevan.andjelkovic@strath.ac.uk>
  -- Stability   :  provisional
  -- Portability :  non-portable (GHC extensions)
  --
  -- This module contains the implementation and specification of a simple
  -- CRUD webserver that uses a postgresql database to store data.
  --
  -- The implementation is based on Servant's
  -- <https://github.com/haskell-servant/example-servant-persistent example-servant-persistent>
  -- repository.
  --
  -- Readers who are not familiar with the
  -- <http://haskell-servant.readthedocs.io/en/stable/ Servant> library
  -- and/or the <http://www.yesodweb.com/book/persistent Persistent>
  -- library might want consult the respective library's documentation in
  -- case any part of the implementation of the webserver is unclear.
  --
  ------------------------------------------------------------------------
  
  module CrudWebserverDb
    ( prop_crudWebserverDb
    , prop_crudWebserverDbParallel
    , Bug(..)
    , setup
    , cleanup
    , connectionString
    , demoNoBug
    , demoLogicBug
    , demoNoRace
    , demoRace
    , UserId -- Only to silence unused warning.
    )
    where
  
  import           Control.Concurrent
                     (newEmptyMVar, putMVar, takeMVar, threadDelay)
  import           Control.Exception
                     (IOException, bracket, catch, onException)
  import           Control.Monad.Logger
                     (NoLoggingT, runNoLoggingT)
  import           Control.Monad.Reader
                     (ReaderT, ask, runReaderT)
  import           Control.Monad.Trans.Resource
                     (ResourceT)
  import qualified Data.ByteString.Char8         as BS
  import           Data.Char
                     (isPrint)
  import           Data.Functor.Classes
                     (Eq1)
  import           Data.Kind
                     (Type)
  import           Data.List
                     (dropWhileEnd)
  import           Data.Monoid
  import           Data.Proxy
                     (Proxy(Proxy))
  import           Data.String.Conversions
                     (cs)
  import           Data.Text
                     (Text)
  import qualified Data.Text                     as T
  import           Data.TreeDiff
                     (Expr(App))
  import           Database.Persist.Class
  import           Database.Persist.Postgresql
                     (ConnectionPool, ConnectionString, SqlBackend,
                     liftSqlPersistMPool, runMigrationQuiet, runSqlPool,
                     withPostgresqlPool, (+=.))
  import           Database.Persist.TH
                     (mkMigrate, mkPersist, persistLowerCase, share,
                     sqlSettings)
  import           GHC.Generics
                     (Generic, Generic1)
  import           Network.HTTP.Client
                     (Manager, defaultManagerSettings, newManager)
  import           Network.Socket
                     (AddrInfoFlag(AI_NUMERICHOST, AI_NUMERICSERV),
                     Socket, SocketType(Stream), addrAddress, addrFamily,
                     addrFlags, addrProtocol, addrSocketType, close,
                     connect, defaultHints, getAddrInfo, socket)
  import qualified Network.Wai.Handler.Warp      as Warp
  import           Prelude
  import           Servant
                     ((:<|>)(..), (:>), Application, Capture, Delete,
                     Get, JSON, Post, Put, ReqBody, Server, serve)
  import           Servant.Client
                     (BaseUrl(..), ClientEnv(..), ClientM, Scheme(Http),
                     client, mkClientEnv, runClientM)
  import           Servant.Server
                     (Handler)
  import           System.Process
                     (callProcess, readProcess)
  import           Test.QuickCheck
                     (Arbitrary, Gen, Property, arbitrary, elements,
                     expectFailure, frequency, ioProperty, listOf,
                     quickCheck, shrink, suchThat, verboseCheck, (===))
  import           Test.QuickCheck.Instances
                     ()
  import           Test.QuickCheck.Monadic
                     (monadic)
  import           UnliftIO
                     (Async, MonadIO, async, cancel, liftIO, waitEither)
  
  import           Test.StateMachine
  import qualified Test.StateMachine.Types.Rank2 as Rank2
  
  ------------------------------------------------------------------------
  -- * User datatype
  
  
  
  
  share [mkPersist sqlSettings, mkMigrate "migrateAll"] [persistLowerCase|
  User json
    name Text
    age  Int
    deriving Eq Read Show Generic
  |]
  
  -- data User = User
  --   { name :: Text
  --   , age  :: Int
  --   }
  
  instance ToExpr User where
  
  ------------------------------------------------------------------------
  -- * API
  
  
  
  
  type Api =
         "user" :> "add" :> ReqBody '[JSON] User     :> Post    '[JSON] (Key User)
    :<|> "user" :> "get" :> Capture "key" (Key User) :> Get     '[JSON] (Maybe User)
    :<|> "user" :> "inc" :> Capture "key" (Key User) :> Put     '[JSON] ()
    :<|> "user" :> "del" :> Capture "key" (Key User) :> Delete  '[JSON] ()
  
    :<|> "health"                                    :> Get     '[JSON] ()
  
  
  
  
  
  
  
  ------------------------------------------------------------------------
  -- * Server implementation
  
  data Bug = None | Logic | Race
  
  server :: Bug -> ConnectionPool -> Server Api
  server bug pool =
    userAdd :<|> userGet :<|> userBirthday :<|> userDelete :<|> health
    where
    userAdd :: User -> Handler (Key User)
    userAdd newUser = sql (insert newUser)
  
    userGet :: Key User -> Handler (Maybe User)
    userGet key = sql (get key)
  
    userBirthday :: Key User -> Handler ()
    userBirthday key = sql $ case bug of
      None  -> update key [UserAge +=. 1]
      Logic -> update key [UserAge +=. 2]
      Race  -> do
        User name age <- getJust key
        replace key (User name (age + 1))
  
    userDelete :: Key User -> Handler ()
    userDelete key = sql $ do
      muser <- get key  -- Make sure that the record exists.
      case muser of
        Just _  -> delete key
        Nothing -> error "userDelete: user doesn't exist."
  
    health :: Handler ()
    health = return ()
  
    sql :: ReaderT SqlBackend (NoLoggingT (ResourceT IO)) a -> Handler a
    sql q = liftSqlPersistMPool q pool
  
  ------------------------------------------------------------------------
  -- * Client bindings
  
  
  postUserC    :: User     -> ClientM (Key User)
  getUserC     :: Key User -> ClientM (Maybe User)
  incAgeUserC  :: Key User -> ClientM ()
  deleteUserC  :: Key User -> ClientM ()
  healthC      ::             ClientM ()
  
  postUserC :<|> getUserC :<|> incAgeUserC :<|> deleteUserC :<|> healthC
    = client api
  
  
  
  
  
  
  
  ------------------------------------------------------------------------
  -- * Implementation done, modelling starts
  
  
  
  data Action (r :: Type -> Type)
    = PostUser   User
    | GetUser    (Reference (Key User) r)
    | IncAgeUser (Reference (Key User) r)
    | DeleteUser (Reference (Key User) r)
    deriving stock (Show, Generic1)
  
  instance Rank2.Functor     Action where
  instance Rank2.Foldable    Action where
  instance Rank2.Traversable Action where
  instance CommandNames      Action where
  
  data Response (r :: Type -> Type)
    = PostedUser (Reference (Key User) r)
    | GotUser    (Maybe User)
    | IncedAgeUser
    | DeletedUser
    deriving stock (Show, Generic1)
  
  instance Rank2.Foldable Response where
  
  ------------------------------------------------------------------------
  -- * State machine model
  
  
  newtype Model r = Model [(Reference (Key User) r, User)]
    deriving stock (Generic, Show)
  
  instance ToExpr (Model Concrete) where
  
  instance ToExpr (Key User) where
    toExpr key = App (show key) []
  
  initModel :: Model v
  initModel = Model []
  
  transitions :: Eq1 r => Model r -> Action r -> Response r -> Model r
  transitions (Model m) (PostUser   user) (PostedUser key) =
    Model (m ++ [(key, user)])
  transitions m         (GetUser    _)    (GotUser _)      =
    m
  transitions (Model m) (IncAgeUser key)  IncedAgeUser     =
    case lookup key m of
      Nothing              -> Model m
      Just (User user age) ->
        Model (updateModel key (User user (age + 1)) m)
  transitions (Model m) (DeleteUser key)  DeletedUser      =
    Model (filter ((/= key) . fst) m)
  transitions _         _                 _                =
    error "transitions"
  
  
  ------------------------------------------------------------------------
  -- * Pre-requisites and invariants
  
  preconditions :: Model Symbolic -> Action Symbolic -> Logic
  preconditions _         (PostUser _)     = Top
  preconditions (Model m) (GetUser    key) = key `member` map fst m
  preconditions (Model m) (IncAgeUser key) = key `member` map fst m
  preconditions (Model m) (DeleteUser key) = key `member` map fst m
  
  
  
  postconditions :: Model Concrete -> Action Concrete -> Response Concrete -> Logic
  postconditions _         (PostUser _)   _              = Top
  postconditions (Model m) (GetUser key)  (GotUser musr) = lookup key m .== musr
  postconditions _         (IncAgeUser _) _              = Top
  postconditions _         (DeleteUser _) _              = Top
  postconditions _         _              _              = error "postconditions"
  
  
  
  ------------------------------------------------------------------------
  -- * How to generate and shrink programs.
  
  generator :: Model Symbolic -> Maybe (Gen (Action Symbolic))
  generator (Model []) = Just $ PostUser <$> arbitrary
  generator (Model m)  = Just $ frequency
    [ (1, PostUser   <$> arbitrary)
    , (3, GetUser    <$> elements (map fst m))
    , (4, IncAgeUser <$> elements (map fst m))
    , (2, DeleteUser <$> elements (map fst m))
    ]
  
  shrinker :: Model Symbolic -> Action Symbolic -> [Action Symbolic]
  shrinker _ (PostUser (User user age)) =
    [ PostUser (User user' age') | (user', age') <- shrink (user, age) ]
  shrinker _ _                          = []
  
  ------------------------------------------------------------------------
  -- * The semantics.
  
  
  semantics :: Action Concrete -> ReaderT ClientEnv IO (Response Concrete)
  semantics act = do
    env <- ask
    res <- liftIO $ flip runClientM env $ case act of
      PostUser   user -> PostedUser . reference <$> postUserC   user
      GetUser    key  -> GotUser                <$> getUserC    (concrete key)
      IncAgeUser key  -> IncedAgeUser           <$  incAgeUserC (concrete key)
      DeleteUser key  -> DeletedUser            <$  deleteUserC (concrete key)
    case res of
      Left  err  -> error (show err)
      Right resp -> return resp
  
  mock :: Model Symbolic -> Action Symbolic -> GenSym (Response Symbolic)
  mock (Model m) act = case act of
    PostUser   _    -> PostedUser <$> genSym
    GetUser    key  -> GotUser <$> pure (lookup key m)
    IncAgeUser _key -> pure IncedAgeUser
    DeleteUser _key -> pure DeletedUser
  
  ------------------------------------------------------------------------
  
  sm :: StateMachine Model Action (ReaderT ClientEnv IO) Response
  sm = StateMachine initModel transitions preconditions postconditions
         Nothing generator shrinker semantics mock noCleanup
  
  ------------------------------------------------------------------------
  -- * Sequential property
  
  prop_crudWebserverDb :: Int -> Property
  prop_crudWebserverDb port =
    forAllCommands sm Nothing $ \cmds -> monadic (ioProperty . runner port) $ do
      (hist, _, res) <- runCommands sm cmds
      prettyCommands sm hist (res === Ok)
  
  withCrudWebserverDb :: Bug -> Int -> IO () -> IO ()
  withCrudWebserverDb bug port run =
    bracket
      (setup bug connectionString port)
      cleanup
      (const run)
  
  demoNoBug', demoLogicBug', demoNoRace' :: Int -> IO ()
  demoNoBug'    port = withCrudWebserverDb None  port
    (verboseCheck (prop_crudWebserverDb port))
  demoLogicBug' port = withCrudWebserverDb Logic port
    (verboseCheck (expectFailure (prop_crudWebserverDb port)))
  demoNoRace'   port = withCrudWebserverDb Race  port
    (quickCheck (prop_crudWebserverDb port))
  
  demoNoBug, demoLogicBug, demoNoRace :: IO ()
  demoNoBug    = demoNoBug'    crudWebserverDbPort
  demoLogicBug = demoLogicBug' crudWebserverDbPort
  demoNoRace   = demoNoRace'   crudWebserverDbPort
  
  -----------------------------------------------------------------------
  -- * Parallel property
  
  prop_crudWebserverDbParallel :: Int -> Property
  prop_crudWebserverDbParallel port =
    forAllParallelCommands sm Nothing $ \cmds -> monadic (ioProperty . runner port) $
      prettyParallelCommands cmds =<< runParallelCommandsNTimes 30 sm cmds
  
  demoRace' :: Int -> IO ()
  demoRace' port = withCrudWebserverDb Race port
    (quickCheck (expectFailure (prop_crudWebserverDbParallel port)))
  
  demoRace :: IO ()
  demoRace = demoRace' crudWebserverDbParallelPort
  
  ------------------------------------------------------------------------
  
  app :: Bug -> ConnectionPool -> Application
  app bug pool = serve (Proxy :: Proxy Api) (server bug pool)
  
  mkApp :: Bug -> ConnectionString -> IO Application
  mkApp bug conn = runNoLoggingT $
    withPostgresqlPool (cs conn) 10 $ \pool -> do
      _ <- runSqlPool (runMigrationQuiet migrateAll) pool
      return (app bug pool)
  
  runServer :: Bug -> ConnectionString -> Warp.Port -> IO () -> IO ()
  runServer bug conn port ready = do
    app' <- mkApp bug conn
    Warp.runSettings settings app'
    where
      settings
        = Warp.setPort port
        . Warp.setBeforeMainLoop ready
        $ Warp.defaultSettings
  
  ------------------------------------------------------------------------
  
  connectionString :: String -> ConnectionString
  connectionString ip = "host=" <> BS.pack ip
    <> " dbname=postgres user=postgres password=mysecretpassword port=5432"
  
  updateModel :: Eq a => a -> b -> [(a, b)] -> [(a, b)]
  updateModel x y xys = (x, y) : filter ((/= x) . fst) xys
  
  api :: Proxy Api
  api = Proxy
  
  crudWebserverDbPort :: Int
  crudWebserverDbPort = 8083
  
  crudWebserverDbParallelPort :: Int
  crudWebserverDbParallelPort = 8084
  
  instance Arbitrary User where
    arbitrary = User <$> (T.pack <$> listOf (arbitrary `suchThat` isPrint))
                     <*> arbitrary
  
  runner :: Warp.Port -> ReaderT ClientEnv IO Property -> IO Property
  runner port p = do
    mgr <- newManager defaultManagerSettings
    runReaderT p (mkClientEnv mgr (burl port))
  
  burl :: Warp.Port -> BaseUrl
  burl port = BaseUrl Http "localhost" port ""
  
  setup
    :: MonadIO m
    => Bug -> (String -> ConnectionString) -> Warp.Port -> m (String, Async ())
  setup bug conn port = liftIO $ do
    (pid, dbIp) <- setupDb
    signal   <- newEmptyMVar
    aServer  <- async (runServer bug (conn dbIp) port (putMVar signal ()))
    aConfirm <- async (takeMVar signal)
    ok <- waitEither aServer aConfirm
    case ok of
      Right () -> do
        mgr <- newManager defaultManagerSettings
        healthy mgr 10
        return (pid, aServer)
      Left () -> error "Server should not return"
    where
    healthy :: Manager -> Int -> IO ()
    healthy _   0     = error "healthy: server isn't healthy"
    healthy mgr tries = do
      res <- liftIO $ runClientM healthC (mkClientEnv mgr (burl port))
      case res of
        Left  _  -> do
          threadDelay 1000000
          healthy mgr (tries - 1)
        Right () -> return ()
  
  setupDb :: IO (String, String)
  setupDb = do
    pid <- trim <$> readProcess "docker"
      [ "run"
      , "-d"
      , "-e", "POSTGRES_PASSWORD=mysecretpassword"
      , "postgres:10.2"
      ] ""
    ip <- trim <$> readProcess "docker"
      [ "inspect"
      , pid
      , "--format"
      , "'{{range .NetworkSettings.Networks}}{{.IPAddress}}{{end}}'"
      ] ""
    healthyDb pid ip `onException` callProcess "docker" [ "rm", "-f", "-v", pid ]
    return (pid, ip)
    where
      trim :: String -> String
      trim = dropWhileEnd isGarbage . dropWhile isGarbage
        where
          isGarbage = flip elem ['\'', '\n']
  
      healthyDb :: String -> String -> IO ()
      healthyDb pid ip = do
        sock <- go 10
        close sock
        where
          go :: Int -> IO Socket
          go 0 = error "healthyDb: db isn't healthy"
          go n = do
            let hints = defaultHints
                  { addrFlags      = [AI_NUMERICHOST , AI_NUMERICSERV]
                  , addrSocketType = Stream
                  }
            addr : _ <- getAddrInfo (Just hints) (Just ip) (Just "5432")
            sock <- socket (addrFamily addr) (addrSocketType addr) (addrProtocol addr)
            (connect sock (addrAddress addr) >>
              readProcess "docker"
                [ "exec"
                , "-u", "postgres"
                , pid
                , "psql", "-U", "postgres", "-d", "postgres", "-c", "SELECT 1 + 1"
                ] "" >> return sock)
              `catch` (\(_ :: IOException) -> do
                          threadDelay 1000000
                          go (n - 1))
  
  
  cleanup :: (String, Async ()) -> IO ()
  cleanup (pid, aServer) = do
    callProcess "docker" [ "rm", "-f", "-v", pid ]
    cancel aServer
  