Copyright | (c) Martin Kuehl Christian Maeder Uni Bremen 2002-2006 |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | Christian.Maeder@dfki.de |
Stability | provisional |
Portability | portable |
Safe Haskell | None |
Datatypes for options that hets understands. Useful functions to parse and check user-provided values.
Synopsis
- data HetcatsOpts = HcOpt {
- analysis :: AnaType
- guiType :: GuiType
- urlCatalog :: [(String, String)]
- infiles :: [FilePath]
- specNames :: [SIMPLE_ID]
- transNames :: [SIMPLE_ID]
- lossyTrans :: Bool
- viewNames :: [SIMPLE_ID]
- intype :: InType
- libdirs :: [FilePath]
- modelSparQ :: FilePath
- counterSparQ :: Int
- outdir :: FilePath
- outtypes :: [OutType]
- databaseDoMigrate :: Bool
- databaseOutputFile :: FilePath
- databaseConfigFile :: FilePath
- databaseSubConfigKey :: String
- databaseFileVersionId :: String
- databaseReanalyze :: Bool
- databaseConfig :: DBConfig
- databaseContext :: DBContext
- xupdate :: FilePath
- recurse :: Bool
- verbose :: Int
- defLogic :: String
- defSyntax :: String
- outputToStdout :: Bool
- caslAmalg :: [CASLAmalgOpt]
- interactive :: Bool
- connectP :: Int
- connectH :: String
- uncolored :: Bool
- xmlFlag :: Bool
- applyAutomatic :: Bool
- computeNormalForm :: Bool
- dumpOpts :: [String]
- disableCertificateVerification :: Bool
- ioEncoding :: Enc
- useLibPos :: Bool
- unlit :: Bool
- serve :: Bool
- listen :: Int
- pidFile :: FilePath
- whitelist :: [[String]]
- blacklist :: [[String]]
- runMMT :: Bool
- fullTheories :: Bool
- outputLogicList :: Bool
- outputLogicGraph :: Bool
- fileType :: Bool
- accessToken :: String
- httpRequestHeaders :: [String]
- fullSign :: Bool
- printAST :: Bool
- data Flag
- optionArgs :: [(String, String -> Flag)]
- optionFlags :: [(String, Flag)]
- accessTokenS :: String
- makeOpts :: HetcatsOpts -> Flag -> HetcatsOpts
- data AnaType
- = Basic
- | Structured
- | Skip
- data GuiType
- data InType
- plainInTypes :: [InType]
- data OWLFormat
- = Manchester
- | Functional
- | OwlXml
- | RdfXml
- | OBO
- | Turtle
- plainOwlFormats :: [OWLFormat]
- data OutType
- data PrettyType
- = PrettyAscii Bool
- | PrettyLatex Bool
- | PrettyXml
- | PrettyHtml
- prettyList :: [PrettyType]
- data GraphType = Dot Bool
- data SPFType
- data ATType
- data Delta
- hetcatsOpts :: [String] -> IO HetcatsOpts
- printOptionsWarnings :: HetcatsOpts -> IO ()
- isStructured :: HetcatsOpts -> Bool
- guess :: String -> InType -> InType
- rmSuffix :: FilePath -> FilePath
- envSuffix :: String
- prfSuffix :: String
- removePrfOut :: HetcatsOpts -> HetcatsOpts
- hasEnvOut :: HetcatsOpts -> Bool
- hasPrfOut :: HetcatsOpts -> Bool
- getFileNames :: [String] -> FilePath -> [FilePath]
- existsAnSource :: HetcatsOpts -> FilePath -> IO (Maybe FilePath)
- getExtensions :: HetcatsOpts -> [String]
- checkRecentEnv :: HetcatsOpts -> FilePath -> FilePath -> IO Bool
- downloadExtensions :: [String]
- defaultHetcatsOpts :: HetcatsOpts
- showDiags :: HetcatsOpts -> [Diagnosis] -> IO ()
- showDiags1 :: HetcatsOpts -> ResultT IO a -> ResultT IO a
- putIfVerbose :: HetcatsOpts -> Int -> String -> IO ()
- doDump :: HetcatsOpts -> String -> IO () -> IO ()
- checkUri :: FilePath -> Bool
- defLogicIsDMU :: HetcatsOpts -> Bool
- useCatalogURL :: HetcatsOpts -> FilePath -> FilePath
- hetsIOError :: String -> IO a
Documentation
data HetcatsOpts Source #
HetcatsOpts
is a record of all options received from the command line
HcOpt | |
|
Instances
Show HetcatsOpts Source # | |
Defined in Driver.Options showsPrec :: Int -> HetcatsOpts -> ShowS show :: HetcatsOpts -> String showList :: [HetcatsOpts] -> ShowS |
every Flag
describes an option (see usage info)
optionArgs :: [(String, String -> Flag)] Source #
options that require arguments for the wep-api excluding "translation"
optionFlags :: [(String, Flag)] Source #
command line switches for the wep-api excluding non-dev-graph related ones
accessTokenS :: String Source #
makeOpts :: HetcatsOpts -> Flag -> HetcatsOpts Source #
makeOpts
includes a parsed Flag in a set of HetcatsOpts
AnaType
describes the type of analysis to be performed
GuiType
determines if we want the GUI shown
InType
describes the type of input the infile contains
ATermIn ATType | |
CASLIn | |
HetCASLIn | |
DOLIn | |
OWLIn OWLFormat | |
HaskellIn | |
MaudeIn | |
TwelfIn | |
HolLightIn | |
IsaIn | |
ThyIn | |
PrfIn | |
OmdocIn | |
ExperimentalIn | for testing new functionality |
ProofCommand | |
GuessIn | |
RDFIn | |
FreeCADIn | |
CommonLogicIn Bool | "clf" or "clif" ( |
DgXml | |
Xmi | |
Qvt | |
TPTPIn | |
HtmlIn |
plainInTypes :: [InType] Source #
OWLFormat
lists possibilities for OWL syntax (in + out)
plainOwlFormats :: [OWLFormat] Source #
OutType
describes the type of outputs that we want to generate
PrettyOut PrettyType | |
GraphOut GraphType | |
Prf | |
EnvOut | |
OWLOut OWLFormat | |
CLIFOut | |
KIFOut | |
OmdocOut | |
XmlOut | development graph xml output |
DbOut | development graph database output |
JsonOut | development graph json output |
ExperimentalOut | for testing new functionality |
HaskellOut | |
FreeCADOut | |
ThyFile | isabelle theory file |
DfgFile SPFType | SPASS input file |
TPTPFile | |
ComptableXml | |
MedusaJson | |
RDFOut | |
SigFile Delta | signature as text |
TheoryFile Delta | signature with sentences as text |
SymXml | |
SymsXml |
data PrettyType Source #
PrettyType
describes the type of output we want the pretty-printer
to generate
PrettyAscii Bool | |
PrettyLatex Bool | |
PrettyXml | |
PrettyHtml |
Instances
Eq PrettyType Source # | |
Defined in Driver.Options (==) :: PrettyType -> PrettyType -> Bool (/=) :: PrettyType -> PrettyType -> Bool | |
Show PrettyType Source # | |
Defined in Driver.Options showsPrec :: Int -> PrettyType -> ShowS show :: PrettyType -> String showList :: [PrettyType] -> ShowS |
prettyList :: [PrettyType] Source #
GraphType
describes the type of Graph that we want generated
Dot Bool | True means show internal node labels |
ATType
describes distinct types of ATerms
hetcatsOpts :: [String] -> IO HetcatsOpts Source #
hetcatsOpts
parses sensible HetcatsOpts from ARGV
printOptionsWarnings :: HetcatsOpts -> IO () Source #
isStructured :: HetcatsOpts -> Bool Source #
check if structured analysis should be performed
removePrfOut :: HetcatsOpts -> HetcatsOpts Source #
remove prf writing
hasEnvOut :: HetcatsOpts -> Bool Source #
should env be written
hasPrfOut :: HetcatsOpts -> Bool Source #
should prf be written
getFileNames :: [String] -> FilePath -> [FilePath] Source #
existsAnSource :: HetcatsOpts -> FilePath -> IO (Maybe FilePath) Source #
checks if a source file for the given file name exists
getExtensions :: HetcatsOpts -> [String] Source #
checkRecentEnv :: HetcatsOpts -> FilePath -> FilePath -> IO Bool Source #
gets two Paths and checks if the first file is not older than the second one and should return True for two identical files
downloadExtensions :: [String] Source #
intypes useable for downloads
defaultHetcatsOpts :: HetcatsOpts Source #
defaultHetcatsOpts
defines the default HetcatsOpts, which are used as
basic values when the user specifies nothing else
showDiags :: HetcatsOpts -> [Diagnosis] -> IO () Source #
show diagnostic messages (see Result.hs), according to verbosity level
showDiags1 :: HetcatsOpts -> ResultT IO a -> ResultT IO a Source #
show diagnostic messages (see Result.hs), according to verbosity level
putIfVerbose :: HetcatsOpts -> Int -> String -> IO () Source #
putIfVerbose
prints a given String to StdOut when the given HetcatsOpts'
Verbosity exceeds the given level
doDump :: HetcatsOpts -> String -> IO () -> IO () Source #
defLogicIsDMU :: HetcatsOpts -> Bool Source #
useCatalogURL :: HetcatsOpts -> FilePath -> FilePath Source #
translate a given http reference using the URL catalog
hetsIOError :: String -> IO a Source #
print error and usage and exit with code 2