{-# LANGUAGE CPP, DoAndIfThenElse #-}
{- |
Module      : ./PGIP/Shared.hs
Description : Provides resources for caching requests to the RESTful interface.
License     : GPLv2 or higher, see LICENSE.txt

This module provides various Hets resources that are used t.e. for caching of an analysis
library during a request to the RESTful interface, proving data types etc.
-}

module PGIP.Shared where

import Common.LibName
import Common.Json (Json (..), pJson)
import Logic.Comorphism (AnyComorphism)
import qualified Logic.Prover as LP
import Proofs.AbstractState (G_proof_tree, ProverOrConsChecker)
import Static.DevGraph

import qualified Data.ByteString.Char8 as B8
import qualified Data.ByteString.Lazy.Char8 as BS
import Data.IORef
import Data.Time
import qualified Data.Map as Map
import qualified Data.IntMap as IntMap
import Network.Wai
import Text.ParserCombinators.Parsec (parse)

#ifdef WARP1
type RsrcIO a = ResourceT IO a
#else
type RsrcIO a = IO a
#endif

data ProverMode = GlProofs | GlConsistency deriving (Int -> ProverMode -> ShowS
[ProverMode] -> ShowS
ProverMode -> String
(Int -> ProverMode -> ShowS)
-> (ProverMode -> String)
-> ([ProverMode] -> ShowS)
-> Show ProverMode
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ProverMode] -> ShowS
$cshowList :: [ProverMode] -> ShowS
show :: ProverMode -> String
$cshow :: ProverMode -> String
showsPrec :: Int -> ProverMode -> ShowS
$cshowsPrec :: Int -> ProverMode -> ShowS
Show, ProverMode -> ProverMode -> Bool
(ProverMode -> ProverMode -> Bool)
-> (ProverMode -> ProverMode -> Bool) -> Eq ProverMode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ProverMode -> ProverMode -> Bool
$c/= :: ProverMode -> ProverMode -> Bool
== :: ProverMode -> ProverMode -> Bool
$c== :: ProverMode -> ProverMode -> Bool
Eq)

type ProofResult = (String, String, String, ProverOrConsChecker,
                -- (goalName, goalResult, goalDetails, prover,
                    AnyComorphism, Maybe (LP.ProofStatus G_proof_tree),
                -- comorphism, proofStatusM)
                    Maybe String)
                -- ConsistencyChecker output

-- | This data type represents a session of a specific analysis library.
-- | It is first created when a library is accessed for the first time.
data Session = Session
  { Session -> LibEnv
sessLibEnv :: LibEnv
  , Session -> LibName
sessLibName :: LibName
  , Session -> [String]
sessPath :: [String]
  , Session -> Int
sessKey :: Int
  , Session -> UTCTime
sessStart :: UTCTime
  , Session -> UTCTime
lastAccess :: UTCTime
  , Session -> Int
usage :: Int
  , Session -> Bool
sessCleanable :: Bool } deriving (Int -> Session -> ShowS
[Session] -> ShowS
Session -> String
(Int -> Session -> ShowS)
-> (Session -> String) -> ([Session] -> ShowS) -> Show Session
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Session] -> ShowS
$cshowList :: [Session] -> ShowS
show :: Session -> String
$cshow :: Session -> String
showsPrec :: Int -> Session -> ShowS
$cshowsPrec :: Int -> Session -> ShowS
Show)

type SessMap = Map.Map [String] Session

-- | In this IORef a cache of all accessed libraries is saved
type Cache = IORef (IntMap.IntMap Session, SessMap)

parseJson :: String -> Maybe Json
parseJson :: String -> Maybe Json
parseJson s :: String
s = case Parsec String () Json -> String -> String -> Either ParseError Json
forall s t a.
Stream s Identity t =>
Parsec s () a -> String -> s -> Either ParseError a
parse Parsec String () Json
forall st. CharParser st Json
pJson "" String
s of
  Left _ -> Maybe Json
forall a. Maybe a
Nothing
  Right json :: Json
json -> Json -> Maybe Json
forall a. a -> Maybe a
Just Json
json

jsonBody :: BS.ByteString -> RsrcIO (Maybe Json)
jsonBody :: ByteString -> RsrcIO (Maybe Json)
jsonBody = Maybe Json -> RsrcIO (Maybe Json)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Json -> RsrcIO (Maybe Json))
-> (ByteString -> Maybe Json) -> ByteString -> RsrcIO (Maybe Json)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Maybe Json
parseJson (String -> Maybe Json)
-> (ByteString -> String) -> ByteString -> Maybe Json
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> String
BS.unpack

receivedRequestBody :: Request -> RsrcIO B8.ByteString
receivedRequestBody :: Request -> RsrcIO ByteString
receivedRequestBody = (ByteString -> ByteString) -> IO ByteString -> RsrcIO ByteString
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (String -> ByteString
B8.pack (String -> ByteString)
-> (ByteString -> String) -> ByteString -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> String
BS.unpack) (IO ByteString -> RsrcIO ByteString)
-> (Request -> IO ByteString) -> Request -> RsrcIO ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Request -> IO ByteString
lazyRequestBody