Hets - the Heterogeneous Tool Set

LicenseGPLv2 or higher, see LICENSE.txt
Safe HaskellNone

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

Documentation

type RsrcIO a = IO a Source #

data ProverMode Source #

Constructors

GlProofs 
GlConsistency 

Instances

Eq ProverMode Source # 

Methods

(==) :: ProverMode -> ProverMode -> Bool

(/=) :: ProverMode -> ProverMode -> Bool

Show ProverMode Source # 

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

Instances

Show Session Source # 

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 #