Copyright	(c) Christian Maeder DFKI GmbH 2010
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	provisional
Portability	non-portable (via imports)
Safe Haskell	None

PGIP.Query

Description

query strings

Synopsis

ppList :: [String]
displayTypes :: [String]
comorphs :: [String]
data NodeCmd
- = Node
- | Info
- | Theory
- | Symbols
- | Translate String
nodeCmds :: [NodeCmd]
showNodeCmd :: NodeCmd -> String
nodeCommands :: [String]
proveParams :: [String]
edgeCommands :: [String]
knownQueryKeys :: [String]
data DGQuery
- = DGQuery {
  - queryId :: Int
  - optQueryLibPath :: Maybe String
  }
- | NewDGQuery {
  - queryLib :: FilePath
  - commands :: [String]
  }
data Query = Query {
- dgQuery :: DGQuery
- queryKind :: QueryKind
}
type NodeIdOrName = Either Int String
type QueryPair = (String, Maybe String)
showQuery :: [QueryPair] -> String
showPath :: [String] -> String
showPathQuery :: [String] -> [QueryPair] -> String
data QueryKind
- = DisplayQuery (Maybe String)
- | DGTranslation String
- | GlobCmdQuery String
- | GlProvers ProverMode (Maybe String)
- | GlTranslations
- | GlShowProverWindow ProverMode
- | GlAutoProveREST ProverMode ReasoningParameters
- | GlAutoProve ProveCmd
- | NodeQuery NodeIdOrName NodeCommand
- | EdgeQuery Int String
data ProveCmd = ProveCmd {
- pcProverMode :: ProverMode
- pcInclTheorems :: Bool
- pcProver :: Maybe String
- pcTranslation :: Maybe String
- pcTimeout :: Maybe Int
- pcTheoremsOrNodes :: [String]
- pcXmlResult :: Bool
- pcAxioms :: [String]
}
data NodeCommand
- = NcCmd NodeCmd
- | NcProvers ProverMode (Maybe String)
- | NcTranslations (Maybe String)
- | ProveNode ProveCmd
anaUri :: [String] -> [QueryPair] -> [String] -> Either String Query
isNat :: String -> Bool
getSwitches :: [QueryPair] -> Either String ([QueryPair], [(String, Flag)])
getArgFlags :: [QueryPair] -> IO (Either String ([QueryPair], [(String, String)], [Flag]))
anaQuery :: [QueryPair] -> [String] -> Either String (Maybe Int, QueryKind)
getIdOrName :: [QueryPair] -> [QueryPair] -> [QueryPair] -> NodeIdOrName
escMap :: [(Char, Char)]
escStr :: String -> String
unEsc :: String -> String
decodePlus :: Char -> Char
decodeQuery :: String -> String
getFragOfCode :: String -> String
getFragment :: String -> String
anaNodeQuery :: [String] -> NodeIdOrName -> [String] -> [String] -> [QueryPair] -> Either String QueryKind

Documentation

ppList :: [String] Source #

displayTypes :: [String] Source #

comorphs :: [String] Source #

data NodeCmd Source #

Constructors

Node
Info
Theory
Symbols
Translate String

Instances

Instances details

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

nodeCmds :: [NodeCmd] Source #

showNodeCmd :: NodeCmd -> String Source #

nodeCommands :: [String] Source #

proveParams :: [String] Source #

edgeCommands :: [String] Source #

knownQueryKeys :: [String] Source #

data DGQuery Source #

Constructors

DGQuery
Fields queryId :: Int optQueryLibPath :: Maybe String
NewDGQuery
Fields queryLib :: FilePath commands :: [String]

Instances

Instances details

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

data Query Source #

Constructors

Query
Fields dgQuery :: DGQuery queryKind :: QueryKind

Instances

Instances details

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

type NodeIdOrName = Either Int String Source #

type QueryPair = (String, Maybe String) Source #

showQuery :: [QueryPair] -> String Source #

showPath :: [String] -> String Source #

showPathQuery :: [String] -> [QueryPair] -> String Source #

data QueryKind Source #

Constructors

DisplayQuery (Maybe String)
DGTranslation String
GlobCmdQuery String
GlProvers ProverMode (Maybe String)
GlTranslations
GlShowProverWindow ProverMode
GlAutoProveREST ProverMode ReasoningParameters
GlAutoProve ProveCmd
NodeQuery NodeIdOrName NodeCommand
EdgeQuery Int String

Instances

Instances details

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

data ProveCmd Source #

Constructors

ProveCmd
Fields pcProverMode :: ProverMode pcInclTheorems :: Bool pcProver :: Maybe String pcTranslation :: Maybe String pcTimeout :: Maybe Int pcTheoremsOrNodes :: [String] pcXmlResult :: Bool pcAxioms :: [String]

Instances

Instances details

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

data NodeCommand Source #

Constructors

NcCmd NodeCmd
NcProvers ProverMode (Maybe String)
NcTranslations (Maybe String)
ProveNode ProveCmd

Instances

Instances details

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

anaUri :: [String] -> [QueryPair] -> [String] -> Either String Query Source #

the path is not empty and leading slashes are removed

isNat :: String -> Bool Source #

getSwitches :: [QueryPair] -> Either String ([QueryPair], [(String, Flag)]) Source #

getArgFlags :: [QueryPair] -> IO (Either String ([QueryPair], [(String, String)], [Flag])) Source #

anaQuery :: [QueryPair] -> [String] -> Either String (Maybe Int, QueryKind) Source #

a leading question mark is removed, possibly a session id is returned

getIdOrName :: [QueryPair] -> [QueryPair] -> [QueryPair] -> NodeIdOrName Source #

escMap :: [(Char, Char)] Source #

escStr :: String -> String Source #

unEsc :: String -> String Source #

decodePlus :: Char -> Char Source #

decodeQuery :: String -> String Source #

getFragOfCode :: String -> String Source #

getFragment :: String -> String Source #

anaNodeQuery :: [String] -> NodeIdOrName -> [String] -> [String] -> [QueryPair] -> Either String QueryKind Source #