PGIP.Query

Description

Synopsis

• ppList :: [String]
• displayTypes :: [String]
• comorphs :: [String]
• data NodeCmd
  • = Node
  • | Info
  • | Theory
  • | Symbols
• 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)
  • | GlobCmdQuery String
  • | GlProvers ProverMode (Maybe String)
  • | GlTranslations
  • | GlShowProverWindow ProverMode
  • | GlAutoProve ProveCmd
  • | NodeQuery NodeIdOrName NodeCommand
  • | EdgeQuery Int String
• data ProverMode
  • = GlProofs
  • | GlConsistency
• data ProveCmd = ProveCmd {
  • pcProverMode :: ProverMode
  • pcInclTheorems :: Bool
  • pcProver :: Maybe String
  • pcTranslation :: Maybe String
  • pcTimeout :: Maybe Int
  • pcTheoremsOrNodes :: [String]
  • pcXmlResult :: Bool
  }
• 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