| 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 |
Driver.Options
Description
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
Constructors
| HcOpt | |
Fields
| |
Instances
| Show HetcatsOpts Source # | |
Defined in Driver.Options Methods 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
Constructors
| Basic | |
| Structured | |
| Skip |
GuiType determines if we want the GUI shown
InType describes the type of input the infile contains
Constructors
| 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)
Constructors
| Manchester | |
| Functional | |
| OwlXml | |
| RdfXml | |
| OBO | |
| Turtle |
plainOwlFormats :: [OWLFormat] Source #
OutType describes the type of outputs that we want to generate
Constructors
| 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
Constructors
| PrettyAscii Bool | |
| PrettyLatex Bool | |
| PrettyXml | |
| PrettyHtml |
Instances
| Eq PrettyType Source # | |
Defined in Driver.Options | |
| Show PrettyType Source # | |
Defined in Driver.Options Methods showsPrec :: Int -> PrettyType -> ShowS show :: PrettyType -> String showList :: [PrettyType] -> ShowS | |
prettyList :: [PrettyType] Source #
GraphType describes the type of Graph that we want generated
Constructors
| Dot Bool | True means show internal node labels |
Constructors
| ConsistencyCheck | |
| ProveTheory |
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