License	GPLv2 or higher, see LICENSE.txt
Safe Haskell	None

PGIP.Shared

Description

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.

Synopsis

type RsrcIO a = IO a
data ProverMode
- = GlProofs
- | GlConsistency
type ProofResult = (String, String, String, ProverOrConsChecker, AnyComorphism, Maybe (ProofStatus G_proof_tree), Maybe String)
data Session = Session {
- sessLibEnv :: LibEnv
- sessLibName :: LibName
- sessPath :: [String]
- sessKey :: Int
- sessStart :: UTCTime
- lastAccess :: UTCTime
- usage :: Int
- sessCleanable :: Bool
}
type SessMap = Map [String] Session
type Cache = IORef (IntMap Session, SessMap)
parseJson :: String -> Maybe Json
jsonBody :: ByteString -> RsrcIO (Maybe Json)
receivedRequestBody :: Request -> RsrcIO ByteString

Documentation

type RsrcIO a = IO a Source #

data ProverMode Source #

Constructors

GlProofs
GlConsistency

Instances

Instances details

Eq ProverMode Source #
Instance details Defined in PGIP.Shared Methods (==) :: ProverMode -> ProverMode -> Bool (/=) :: ProverMode -> ProverMode -> Bool
Show ProverMode Source #
Instance details Defined in PGIP.Shared Methods showsPrec :: Int -> ProverMode -> ShowS show :: ProverMode -> String showList :: [ProverMode] -> ShowS

type ProofResult = (String, String, String, ProverOrConsChecker, AnyComorphism, Maybe (ProofStatus G_proof_tree), Maybe String) Source #

data Session Source #

This data type represents a session of a specific analysis library. | It is first created when a library is accessed for the first time.

Constructors

Session
Fields sessLibEnv :: LibEnv sessLibName :: LibName sessPath :: [String] sessKey :: Int sessStart :: UTCTime lastAccess :: UTCTime usage :: Int sessCleanable :: Bool

Instances

Instances details

Show Session Source #
Instance details Defined in PGIP.Shared Methods showsPrec :: Int -> Session -> ShowS show :: Session -> String showList :: [Session] -> ShowS

type SessMap = Map [String] Session Source #

type Cache = IORef (IntMap Session, SessMap) Source #

In this IORef a cache of all accessed libraries is saved

parseJson :: String -> Maybe Json Source #

jsonBody :: ByteString -> RsrcIO (Maybe Json) Source #

receivedRequestBody :: Request -> RsrcIO ByteString Source #