b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder{-# LANGUAGE CPP #-}
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : Datatypes and functions for options that hets understands.
2725abe920f91de62ae5c0b7230c1627cccf5fabChristian MaederCopyright : (c) Martin Kuehl, Christian Maeder, Uni Bremen 2002-2006
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederStability : provisional
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederDatatypes for options that hets understands.
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Useful functions to parse and check user-provided values.
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder ( HetcatsOpts (..)
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder , optionArgs
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder , optionFlags
93603bd881e43d4ff5a57d7ca4e2b9fa619f25b4cmaeder , accessTokenS
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , AnaType (..)
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , GuiType (..)
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , InType (..)
4811c997e10bcfbd8e0fdfb130c3368abd33bbcaEugen Kuksa , plainInTypes
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist , OWLFormat (..)
df87ff823273ae2969e9d29e833845b4c0a9ee77notanartist , plainOwlFormats
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , OutType (..)
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , PrettyType (..)
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , GraphType (..)
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , SPFType (..)
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , hetcatsOpts
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa , printOptionsWarnings
91e24fc45834b35f2a3830d72565640251149bf3Christian Maeder , isStructured
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , removePrfOut
0130083f314580170af1195037be3325f125fbceChristian Maeder , getFileNames
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , existsAnSource
0130083f314580170af1195037be3325f125fbceChristian Maeder , getExtensions
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , checkRecentEnv
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , downloadExtensions
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , defaultHetcatsOpts
109a53dbf4c9233f869f63ba7a7f3fece49973c3Christian Maeder , putIfVerbose
a461314c811f4187dff85c8be079a41b2f13f176Christian Maeder , defLogicIsDMU
4eb859461f8fd904f40f57261cf23e5c73cf8ecaChristian Maeder , useCatalogURL
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder , hetsIOError
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksaimport qualified Persistence.DBConfig as DBConfig
4eb859461f8fd904f40f57261cf23e5c73cf8ecaChristian Maeder-- | translate a given http reference using the URL catalog
4eb859461f8fd904f40f57261cf23e5c73cf8ecaChristian MaederuseCatalogURL :: HetcatsOpts -> FilePath -> FilePath
4eb859461f8fd904f40f57261cf23e5c73cf8ecaChristian MaederuseCatalogURL opts fname = case mapMaybe
4eb859461f8fd904f40f57261cf23e5c73cf8ecaChristian Maeder (\ (a, b) -> fmap (b ++) $ stripPrefix a fname)
4eb859461f8fd904f40f57261cf23e5c73cf8ecaChristian Maeder $ urlCatalog opts of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederbracket :: String -> String
2353f65833a3da763392f771223250cd50b8d873Christian Maederbracket s = "[" ++ s ++ "]"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- use the same strings for parsing and printing!
dff1de7ad15d1582e25d636c3724dd202874897fChristian MaederverboseS, intypeS, outtypesS, skipS, justStructuredS, transS,
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder guiS, libdirsS, outdirS, amalgS, recursiveS, namedSpecsS,
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa interactiveS, modelSparQS, counterSparQS, connectS, xmlS, dbS, listenS,
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa applyAutomaticRuleS, normalFormS, unlitS, pidFileS :: String
d81905a5b924415c524d702df26204683c82c12eChristian MaedermodelSparQS = "modelSparQ"
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian MaedercounterSparQS = "counterSparQ"
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederverboseS = "verbose"
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederintypeS = "input-type"
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederouttypesS = "output-types"
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederskipS = "just-parse"
dff1de7ad15d1582e25d636c3724dd202874897fChristian MaederjustStructuredS = "just-structured"
cb2044812811d66efe038d914966e04290be93faChristian MaederlibdirsS = "hets-libdirs"
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederoutdirS = "output-dir"
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederamalgS = "casl-amalg"
dff1de7ad15d1582e25d636c3724dd202874897fChristian MaedernamedSpecsS = "named-specs"
0ae7a79e865d4a6022d705d160530682b3c1f825Christian MaedertransS = "translation"
083bc1972a66d73749760eab3a90bf4eb9ca7951Christian MaederrecursiveS = "recursive"
6352f3c31da3043783a13be6594aacb2147378baRazvan PascanuinteractiveS = "interactive"
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan PascanuconnectS = "connect"
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan PascanulistenS = "listen"
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen KuksapidFileS = "pidfile"
bc263f610d20a9cd3014ddfca903026127fa0d48Christian MaederapplyAutomaticRuleS = "apply-automatic-rule"
966519955f5f7111abac20118563132b9dd41165Christian MaedernormalFormS = "normal-form"
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian MaederunlitS = "unlit"
0b13f102310e03a20b38c870b5acb88712f316a4Christian MaederurlCatalogS :: String
0b13f102310e03a20b38c870b5acb88712f316a4Christian MaederurlCatalogS = "url-catalog"
33fcc19ef2b59493b4e91eebf701df95fd230765Christian MaederrelposS :: String
33fcc19ef2b59493b4e91eebf701df95fd230765Christian MaederrelposS = "relative-positions"
d4ebd9e5adc974cfa2bdf4bdd155e07be0e26f75Christian MaederfullSignS :: String
d4ebd9e5adc974cfa2bdf4bdd155e07be0e26f75Christian MaederfullSignS = "full-signatures"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintASTS :: String
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen KuksaprintASTS = "print-AST"
0d79ea4ed8512a802ecb6645edac141e0fbcee3fChristian MaederfullTheoriesS :: String
0d79ea4ed8512a802ecb6645edac141e0fbcee3fChristian MaederfullTheoriesS = "full-theories"
a31430de8b0632d29f42634d6395e982bf31b14dChristian MaederlogicGraphS :: String
a31430de8b0632d29f42634d6395e982bf31b14dChristian MaederlogicGraphS = "logic-graph"
31bc219bae758272d0f064281b8ce7740a4553e9Till MossakowskilogicListS :: String
31bc219bae758272d0f064281b8ce7740a4553e9Till MossakowskilogicListS = "logic-list"
ce8a93047aaf0dc36fa221642292d47852a9862aChristian MaederfileTypeS :: String
ce8a93047aaf0dc36fa221642292d47852a9862aChristian MaederfileTypeS = "file-type"
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian MaederblacklistS :: String
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian MaederblacklistS = "blacklist"
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian MaederwhitelistS :: String
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian MaederwhitelistS = "whitelist"
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaederaccessTokenS :: String
93603bd881e43d4ff5a57d7ca4e2b9fa619f25b4cmaederaccessTokenS = "access-token"
fb89f291c4e12ee44de11d4a900c445ed727b90dEugen KuksahttpRequestHeaderS :: String
fb89f291c4e12ee44de11d4a900c445ed727b90dEugen KuksahttpRequestHeaderS = "http-request-header"
8865728716566f42fa73e7e0bc080ba3225df764Christian MaedergenTermS, treeS, bafS :: String
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedergenTermS = "gen_trm"
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedertreeS = "tree."
1f2c732265a1292f0d7c51a4a7ca6be5dd370df6cmaedergraphE, ppS, envS, deltaS, prfS, omdocS, hsS, experimentalS :: String
1f2c732265a1292f0d7c51a4a7ca6be5dd370df6cmaedergraphE = "graph."
beff4152e9f0fe90885458d1a1733b183a2a8816Christian MaederdeltaS = ".delta"
fdac680252d7347858bd67b4c2a2aaa52e623815Christian MaederomdocS = "omdoc"
f8cc2399c16fcda7e3bf9d901a0de0cc8a455f86Ewaryst SchulzexperimentalS = "exp"
b76d27eba526ecac2a20400fa505ec5c642ae7d2Dominik LuecketptpS, dfgS, cS :: String
b76d27eba526ecac2a20400fa505ec5c642ae7d2Dominik LuecketptpS = "tptp"
2353f65833a3da763392f771223250cd50b8d873Christian MaedershowOpt :: String -> String
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedershowOpt s = if null s then "" else " --" ++ s
2353f65833a3da763392f771223250cd50b8d873Christian MaedershowEqOpt :: String -> String -> String
2353f65833a3da763392f771223250cd50b8d873Christian MaedershowEqOpt k s = if null s then "" else showOpt k ++ "=" ++ s
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- main Datatypes --
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'HetcatsOpts' is a record of all options received from the command line
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederdata HetcatsOpts = HcOpt -- for comments see usage info
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder { analysis :: AnaType
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , guiType :: GuiType
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder , urlCatalog :: [(String, String)]
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , infiles :: [FilePath] -- ^ files to be read
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , specNames :: [SIMPLE_ID] -- ^ specs to be processed
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , transNames :: [SIMPLE_ID] -- ^ comorphism to be processed
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder , viewNames :: [SIMPLE_ID] -- ^ views to be processed
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , intype :: InType
cb2044812811d66efe038d914966e04290be93faChristian Maeder , libdirs :: [FilePath]
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , modelSparQ :: FilePath
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder , counterSparQ :: Int
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , outdir :: FilePath
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , outtypes :: [OutType]
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , databaseDoMigrate :: Bool
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , databaseOutputFile :: FilePath
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , databaseConfigFile :: FilePath
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , databaseSubConfigKey :: String
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , databaseFileVersionId :: String
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , databaseReanalyze :: Bool
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , databaseConfig :: DBConfig.DBConfig
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , databaseContext :: DBConfig.DBContext
8d780c893d6df5dab3dcc7d8444b7517f6547f11Christian Maeder , xupdate :: FilePath
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , recurse :: Bool
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , verbose :: Int
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , defLogic :: String
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder , defSyntax :: String
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , outputToStdout :: Bool -- ^ send messages to stdout?
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , caslAmalg :: [CASLAmalgOpt]
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , interactive :: Bool
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , connectP :: Int
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , connectH :: String
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , uncolored :: Bool
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , xmlFlag :: Bool
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder , applyAutomatic :: Bool
966519955f5f7111abac20118563132b9dd41165Christian Maeder , computeNormalForm :: Bool
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder , dumpOpts :: [String]
55282ad62e8b6758abec43734ebde0015ac14b89Eugen Kuksa , disableCertificateVerification :: Bool
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder , ioEncoding :: Enc
d96bfd1d7a4595bfff87771b91797330fa939455Christian Maeder -- | use the library name in positions to avoid differences after uploads
d96bfd1d7a4595bfff87771b91797330fa939455Christian Maeder , useLibPos :: Bool
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder , unlit :: Bool
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder , serve :: Bool
34d14197eb3dd643a8e6ef3ed8cba5629528e97fAivaras Jakubauskas , listen :: Int
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa , pidFile :: FilePath
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder , whitelist :: [[String]]
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder , blacklist :: [[String]]
d4ebd9e5adc974cfa2bdf4bdd155e07be0e26f75Christian Maeder , runMMT :: Bool
0d79ea4ed8512a802ecb6645edac141e0fbcee3fChristian Maeder , fullTheories :: Bool
31bc219bae758272d0f064281b8ce7740a4553e9Till Mossakowski , outputLogicList :: Bool
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder , outputLogicGraph :: Bool
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder , fileType :: Bool
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaeder , accessToken :: String
fb89f291c4e12ee44de11d4a900c445ed727b90dEugen Kuksa , httpRequestHeaders :: [String]
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , fullSign :: Bool
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , printAST :: Bool }
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder{- | 'defaultHetcatsOpts' defines the default HetcatsOpts, which are used as
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maederbasic values when the user specifies nothing else -}
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederdefaultHetcatsOpts :: HetcatsOpts
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederdefaultHetcatsOpts = HcOpt
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder { analysis = Basic
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , guiType = NoGui
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder , urlCatalog = []
2360728d4185c0c04279c999941c64d36626af79Christian Maeder , infiles = []
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , specNames = []
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , transNames = []
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder , viewNames = []
2360728d4185c0c04279c999941c64d36626af79Christian Maeder , intype = GuessIn
2360728d4185c0c04279c999941c64d36626af79Christian Maeder , libdirs = []
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , modelSparQ = ""
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder , counterSparQ = 3
2360728d4185c0c04279c999941c64d36626af79Christian Maeder , outdir = ""
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , outtypes = [] -- no default
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , databaseDoMigrate = True
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , databaseOutputFile = ""
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , databaseConfigFile = ""
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , databaseSubConfigKey = ""
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , databaseFileVersionId = ""
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , databaseReanalyze = False
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , databaseConfig = DBConfig.emptyDBConfig
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , databaseContext = DBConfig.emptyDBContext
8d780c893d6df5dab3dcc7d8444b7517f6547f11Christian Maeder , xupdate = ""
2360728d4185c0c04279c999941c64d36626af79Christian Maeder , recurse = False
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , defLogic = "CASL"
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder , defSyntax = ""
2360728d4185c0c04279c999941c64d36626af79Christian Maeder , verbose = 1
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , outputToStdout = True
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , caslAmalg = [Cell]
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , interactive = False
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , connectP = -1
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , connectH = ""
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , uncolored = False
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder , xmlFlag = False
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder , applyAutomatic = False
966519955f5f7111abac20118563132b9dd41165Christian Maeder , computeNormalForm = False
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder , dumpOpts = []
55282ad62e8b6758abec43734ebde0015ac14b89Eugen Kuksa , disableCertificateVerification = False
5a448e9be8c4482a978b174b744237757335140fChristian Maeder , ioEncoding = Utf8
d96bfd1d7a4595bfff87771b91797330fa939455Christian Maeder , useLibPos = False
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder , unlit = False
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder , serve = False
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa , pidFile = ""
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder , whitelist = []
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder , blacklist = []
d4ebd9e5adc974cfa2bdf4bdd155e07be0e26f75Christian Maeder , runMMT = False
0d79ea4ed8512a802ecb6645edac141e0fbcee3fChristian Maeder , fullTheories = False
31bc219bae758272d0f064281b8ce7740a4553e9Till Mossakowski , outputLogicList = False
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder , outputLogicGraph = False
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder , fileType = False
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaeder , accessToken = ""
fb89f291c4e12ee44de11d4a900c445ed727b90dEugen Kuksa , httpRequestHeaders = []
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , fullSign = False
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , printAST = False }
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance Show HetcatsOpts where
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder let showFlag p o = if p opts then showOpt o else ""
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder showIPLists p s = let ll = p opts in if null ll then "" else
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder showEqOpt s . intercalate "," $ map (intercalate ".") ll
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder showEqOpt verboseS (show $ verbose opts)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ++ show (guiType opts)
31bc219bae758272d0f064281b8ce7740a4553e9Till Mossakowski ++ showFlag outputLogicList logicListS
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder ++ showFlag outputLogicGraph logicGraphS
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder ++ showFlag fileType fileTypeS
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder ++ showFlag interactive interactiveS
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ++ show (analysis opts)
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder ++ case defLogic opts of
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder s | s /= defLogic defaultHetcatsOpts -> showEqOpt logicS s
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder ++ case defSyntax opts of
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder s | s /= defSyntax defaultHetcatsOpts -> showEqOpt serializationS s
fb89f291c4e12ee44de11d4a900c445ed727b90dEugen Kuksa ++ case httpRequestHeaders opts of
fb89f291c4e12ee44de11d4a900c445ed727b90dEugen Kuksa headers -> concatMap (showEqOpt httpRequestHeaderS . show) headers
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaeder ++ case accessToken opts of
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaeder t -> showEqOpt accessTokenS t
cb2044812811d66efe038d914966e04290be93faChristian Maeder ++ showEqOpt libdirsS (intercalate ":" $ libdirs opts)
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder ++ case modelSparQ opts of
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder f -> showEqOpt modelSparQS f
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder ++ case counterSparQ opts of
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder n | n /= counterSparQ defaultHetcatsOpts
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder -> showEqOpt counterSparQS $ show n
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder ++ showFlag xmlFlag xmlS
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder ++ showFlag ((/= -1) . connectP) connectS
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder ++ showFlag ((/= -1) . listen) listenS
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa ++ showEqOpt pidFileS (pidFile opts)
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder ++ showIPLists whitelist whitelistS
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder ++ showIPLists blacklist blacklistS
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder ++ concatMap (showEqOpt "dump") (dumpOpts opts)
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder ++ showEqOpt "encoding" (map toLower $ show $ ioEncoding opts)
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder ++ showFlag unlit unlitS
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder ++ showFlag useLibPos relposS
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder ++ showFlag fullSign fullSignS
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa ++ showFlag printAST printASTS
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder ++ showFlag fullTheories fullTheoriesS
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder ++ case urlCatalog opts of
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder cs -> showEqOpt urlCatalogS $ intercalate ","
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder $ map (\ (a, b) -> a ++ '=' : b) cs
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ++ showEqOpt intypeS (show $ intype opts)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ++ showEqOpt outdirS (outdir opts)
8bb80c9684e905de8dcfcfb1291542677e7d77b6Christian Maeder ++ showEqOpt outtypesS (intercalate "," $ map show $ outtypes opts)
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder ++ showFlag recurse recursiveS
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder ++ showFlag applyAutomatic applyAutomaticRuleS
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder ++ showFlag computeNormalForm normalFormS
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder ++ showEqOpt namedSpecsS (intercalate "," $ map show $ specNames opts)
8bb80c9684e905de8dcfcfb1291542677e7d77b6Christian Maeder ++ showEqOpt transS (intercalate ":" $ map show $ transNames opts)
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder ++ showEqOpt viewS (intercalate "," $ map show $ viewNames opts)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ++ showEqOpt amalgS (tail $ init $ show $
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder case caslAmalg opts of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder [] -> [NoAnalysis]
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder ++ " " ++ unwords (infiles opts)
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder-- | every 'Flag' describes an option (see usage info)
60e6795dd310e10194e12bb660575aadf941328bEugen Kuksa | VersionNumeric
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder | ApplyAutomatic
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder | Gui GuiType
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder | Analysis AnaType
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder | DefaultLogic String
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder | DefaultSyntax String
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder | InType InType
cb2044812811d66efe038d914966e04290be93faChristian Maeder | LibDirs String
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder | OutDir FilePath
8d780c893d6df5dab3dcc7d8444b7517f6547f11Christian Maeder | XUpdate FilePath
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder | ModelSparQ FilePath
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder | CounterSparQ Int
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder | OutTypes [OutType]
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa | DatabaseDoNotMigrate
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa | DatabaseOutputFile FilePath
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa | DatabaseConfigFile FilePath
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa | DatabaseSubConfigKey String
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa | DatabaseFileVersionId String
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa | DatabaseReanalyze
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder | Specs [SIMPLE_ID]
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder | Trans [SIMPLE_ID]
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder | Views [SIMPLE_ID]
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder | CASLAmalg [CASLAmalgOpt]
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder | Interactive
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder | Connect Int String
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder | Dump String
55282ad62e8b6758abec43734ebde0015ac14b89Eugen Kuksa | DisableCertificateVerification
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder | IOEncoding Enc
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa | PidFile FilePath
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder | Whitelist String
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder | Blacklist String
0d79ea4ed8512a802ecb6645edac141e0fbcee3fChristian Maeder | FullTheories
31bc219bae758272d0f064281b8ce7740a4553e9Till Mossakowski | OutputLogicList
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder | OutputLogicGraph
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaeder | AccessToken String
fb89f291c4e12ee44de11d4a900c445ed727b90dEugen Kuksa | HttpRequestHeader String
9b3e946be44391d35acb2168f4e67d629e560f79Till Mossakowski | UrlCatalog [(String, String)] deriving Show
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'makeOpts' includes a parsed Flag in a set of HetcatsOpts
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedermakeOpts :: HetcatsOpts -> Flag -> HetcatsOpts
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian MaedermakeOpts opts flg =
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder let splitIPs = map (splitBy '.') . splitOn ','
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder in case flg of
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder Interactive -> opts { interactive = True }
2360728d4185c0c04279c999941c64d36626af79Christian Maeder XML -> opts { xmlFlag = True }
2360728d4185c0c04279c999941c64d36626af79Christian Maeder Listen x -> opts { listen = x }
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa PidFile x -> opts { pidFile = x }
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder Blacklist x -> opts { blacklist = splitIPs x }
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder Whitelist x -> opts { whitelist = splitIPs x }
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Connect x y -> opts { connectP = x, connectH = y }
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder Analysis x -> opts { analysis = x }
2360728d4185c0c04279c999941c64d36626af79Christian Maeder Gui x -> opts { guiType = x }
2360728d4185c0c04279c999941c64d36626af79Christian Maeder InType x -> opts { intype = x }
0130083f314580170af1195037be3325f125fbceChristian Maeder LibDirs x -> opts { libdirs = joinHttpLibPath $ splitPaths x }
d81905a5b924415c524d702df26204683c82c12eChristian Maeder ModelSparQ x -> opts { modelSparQ = x }
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder CounterSparQ x -> opts { counterSparQ = x }
2360728d4185c0c04279c999941c64d36626af79Christian Maeder OutDir x -> opts { outdir = x }
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder OutTypes x -> opts { outtypes = x }
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa DatabaseDoNotMigrate -> opts { databaseDoMigrate = False }
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa DatabaseOutputFile x -> opts { databaseOutputFile = x }
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa DatabaseConfigFile x -> opts { databaseConfigFile = x }
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa DatabaseSubConfigKey x -> opts { databaseSubConfigKey = x }
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa DatabaseFileVersionId x -> opts { databaseFileVersionId = x }
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa DatabaseReanalyze -> opts { databaseReanalyze = True }
8d780c893d6df5dab3dcc7d8444b7517f6547f11Christian Maeder XUpdate x -> opts { xupdate = x }
2360728d4185c0c04279c999941c64d36626af79Christian Maeder Recurse -> opts { recurse = True }
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder ApplyAutomatic -> opts { applyAutomatic = True }
966519955f5f7111abac20118563132b9dd41165Christian Maeder NormalForm -> opts { computeNormalForm = True }
2360728d4185c0c04279c999941c64d36626af79Christian Maeder Specs x -> opts { specNames = x }
2360728d4185c0c04279c999941c64d36626af79Christian Maeder Trans x -> opts { transNames = x }
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder Views x -> opts { viewNames = x }
2360728d4185c0c04279c999941c64d36626af79Christian Maeder Verbose x -> opts { verbose = x }
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder DefaultLogic x -> opts { defLogic = x }
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder DefaultSyntax x -> opts { defSyntax = x }
2360728d4185c0c04279c999941c64d36626af79Christian Maeder CASLAmalg x -> opts { caslAmalg = x }
2360728d4185c0c04279c999941c64d36626af79Christian Maeder Quiet -> opts { verbose = 0 }
2360728d4185c0c04279c999941c64d36626af79Christian Maeder Uncolored -> opts { uncolored = True }
2360728d4185c0c04279c999941c64d36626af79Christian Maeder Dump s -> opts { dumpOpts = s : dumpOpts opts }
55282ad62e8b6758abec43734ebde0015ac14b89Eugen Kuksa DisableCertificateVerification ->
55282ad62e8b6758abec43734ebde0015ac14b89Eugen Kuksa opts { disableCertificateVerification = True }
2360728d4185c0c04279c999941c64d36626af79Christian Maeder IOEncoding e -> opts { ioEncoding = e }
d27b1887e61f1dc53d77c37f59dbf5019242a686Christian Maeder Serve -> opts { serve = True }
8994ef587ce7c7c39ddd20f0f7e4575838a6694aChristian Maeder Unlit -> opts { unlit = True }
33fcc19ef2b59493b4e91eebf701df95fd230765Christian Maeder RelPos -> opts { useLibPos = True }
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder UseMMT -> opts { runMMT = True }
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder FullTheories -> opts { fullTheories = True }
31bc219bae758272d0f064281b8ce7740a4553e9Till Mossakowski OutputLogicList -> opts { outputLogicList = True }
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder OutputLogicGraph -> opts { outputLogicGraph = True }
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder FileType -> opts { fileType = True }
ce8a93047aaf0dc36fa221642292d47852a9862aChristian Maeder FullSign -> opts { fullSign = True }
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa PrintAST -> opts { printAST = True }
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder UrlCatalog m -> opts { urlCatalog = m ++ urlCatalog opts }
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaeder AccessToken s -> opts { accessToken = s }
fb89f291c4e12ee44de11d4a900c445ed727b90dEugen Kuksa HttpRequestHeader header -> opts { httpRequestHeaders = header : httpRequestHeaders opts }
2360728d4185c0c04279c999941c64d36626af79Christian Maeder Help -> opts -- skipped
2360728d4185c0c04279c999941c64d36626af79Christian Maeder Version -> opts -- skipped
60e6795dd310e10194e12bb660575aadf941328bEugen Kuksa VersionNumeric -> opts -- skipped
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'AnaType' describes the type of analysis to be performed
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederdata AnaType = Basic | Structured | Skip
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance Show AnaType where
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder show a = case a of
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder Structured -> showOpt justStructuredS
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Skip -> showOpt skipS
91e24fc45834b35f2a3830d72565640251149bf3Christian Maeder-- | check if structured analysis should be performed
91e24fc45834b35f2a3830d72565640251149bf3Christian MaederisStructured :: HetcatsOpts -> Bool
91e24fc45834b35f2a3830d72565640251149bf3Christian MaederisStructured a = case analysis a of
91e24fc45834b35f2a3830d72565640251149bf3Christian Maeder Structured -> True
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'GuiType' determines if we want the GUI shown
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederdata GuiType = UseGui | NoGui
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance Show GuiType where
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder show g = case g of
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder UseGui -> showOpt guiS
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'InType' describes the type of input the infile contains
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ATermIn ATType
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist | OWLIn OWLFormat
63da71bfb4226f504944b293fb77177ebcaea7d4Ewaryst Schulz | ExperimentalIn -- ^ for testing new functionality
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder | ProofCommand
b47b1ea8a412f6e4c731779f6a572384e7cf06d8Christian Maeder | CommonLogicIn Bool -- ^ "clf" or "clif" ('True' is long version)
6f70475dddc12732bdbef3e3dd116373e34cd6b9Christian Maeder | HtmlIn -- just to complain
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance Show InType where
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder show i = case i of
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ATermIn at -> genTermS ++ show at
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder CASLIn -> "casl"
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder HetCASLIn -> "het"
8762d0e3d492aba4d1621fb0de685f0be1372864notanartist DOLIn -> "dol"
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist OWLIn oty -> show oty
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder HaskellIn -> hsS
63da71bfb4226f504944b293fb77177ebcaea7d4Ewaryst Schulz ExperimentalIn -> "exp"
76d027be764e2ff61bef959efb3ac8f56499e646Christian Maeder MaudeIn -> "maude"
9f85afecbd79b3df5a0bb17bd28cd0b288dc3213Kristina Sojakova TwelfIn -> "elf"
a166da43d4e8f9dfa7a2651d033c6bea02627ca6Mihai Codescu HolLightIn -> "hol"
f730570f7c284b252ad2e24cf23cc594021f9e25Jonathan von Schroeder TPTPIn -> "tptp"
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder PrfIn -> prfS
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder OmdocIn -> omdocS
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ProofCommand -> "hpf"
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder GuessIn -> ""
8762d0e3d492aba4d1621fb0de685f0be1372864notanartist RDFIn -> "rdf"
af6e92e4a9ca308f928f9909acee115f801c5db5Ewaryst Schulz FreeCADIn -> "fcstd"
b47b1ea8a412f6e4c731779f6a572384e7cf06d8Christian Maeder CommonLogicIn isLong -> if isLong then "clif" else "clf"
26b1c101b72100b69045effdfaab3889de6c8c93Christian Maeder DgXml -> xmlS
6f70475dddc12732bdbef3e3dd116373e34cd6b9Christian Maeder HtmlIn -> "html"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- maybe this optional tree prefix can be omitted
2353f65833a3da763392f771223250cd50b8d873Christian Maederinstance Read InType where
1ebf8299efa3cdb39c73d40d15e1d1a8a2246e68notanartist readsPrec _ = readShowAux $ concatMap showAll (plainInTypes ++ aInTypes)
1ebf8299efa3cdb39c73d40d15e1d1a8a2246e68notanartist where showAll i@(ATermIn _) = [(show i, i), (treeS ++ show i, i)]
1ebf8299efa3cdb39c73d40d15e1d1a8a2246e68notanartist showAll i = [(show i, i)]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'ATType' describes distinct types of ATerms
897a04683fb30873e84dc3360dea770a4435971cChristian Maederdata ATType = BAF | NonBAF deriving Eq
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance Show ATType where
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder show a = case a of
8762d0e3d492aba4d1621fb0de685f0be1372864notanartist-- RDFIn is on purpose not listed; must be added manually if neccessary
1ebf8299efa3cdb39c73d40d15e1d1a8a2246e68notanartistplainInTypes :: [InType]
1ebf8299efa3cdb39c73d40d15e1d1a8a2246e68notanartistplainInTypes =
8762d0e3d492aba4d1621fb0de685f0be1372864notanartist [ CASLIn, HetCASLIn, DOLIn ]
1ebf8299efa3cdb39c73d40d15e1d1a8a2246e68notanartist ++ map OWLIn plainOwlFormats ++
1ebf8299efa3cdb39c73d40d15e1d1a8a2246e68notanartist [ HaskellIn, ExperimentalIn
1ebf8299efa3cdb39c73d40d15e1d1a8a2246e68notanartist , MaudeIn, TwelfIn
1ebf8299efa3cdb39c73d40d15e1d1a8a2246e68notanartist , HolLightIn, IsaIn, ThyIn, PrfIn, OmdocIn, ProofCommand
1ebf8299efa3cdb39c73d40d15e1d1a8a2246e68notanartist , CommonLogicIn False, CommonLogicIn True
1ebf8299efa3cdb39c73d40d15e1d1a8a2246e68notanartist , DgXml, FreeCADIn, Xmi, Qvt, TPTPIn ]
1ebf8299efa3cdb39c73d40d15e1d1a8a2246e68notanartistaInTypes :: [InType]
1ebf8299efa3cdb39c73d40d15e1d1a8a2246e68notanartistaInTypes = [ ATermIn x | x <- [BAF, NonBAF] ]
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist-- | 'OWLFormat' lists possibilities for OWL syntax (in + out)
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartistdata OWLFormat =
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartistplainOwlFormats :: [OWLFormat]
8762d0e3d492aba4d1621fb0de685f0be1372864notanartistplainOwlFormats = [ Manchester, OwlXml, RdfXml, OBO, Turtle ]
df87ff823273ae2969e9d29e833845b4c0a9ee77notanartistinstance Show OWLFormat where
df87ff823273ae2969e9d29e833845b4c0a9ee77notanartist show ty = case ty of
df87ff823273ae2969e9d29e833845b4c0a9ee77notanartist Manchester -> "omn"
df87ff823273ae2969e9d29e833845b4c0a9ee77notanartist OwlXml -> "owl"
df87ff823273ae2969e9d29e833845b4c0a9ee77notanartist -- "owl.xml" ?? might occur but conflicts with dgxml
df87ff823273ae2969e9d29e833845b4c0a9ee77notanartist RdfXml -> "rdf"
df87ff823273ae2969e9d29e833845b4c0a9ee77notanartist OBO -> "obo"
df87ff823273ae2969e9d29e833845b4c0a9ee77notanartist Turtle -> "ttl"
e38219f3dd2f5711440478cbffa76ce3db530543cmaederdata SPFType = ConsistencyCheck | ProveTheory deriving Eq
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettichinstance Show SPFType where
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder show x = case x of
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ConsistencyCheck -> cS
2360728d4185c0c04279c999941c64d36626af79Christian Maeder ProveTheory -> ""
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus LuettichspfTypes :: [SPFType]
7ebcceae3d34771cae3bbb8c8060bef0b894376eChristian MaederspfTypes = [ConsistencyCheck, ProveTheory]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'OutType' describes the type of outputs that we want to generate
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederdata OutType =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder PrettyOut PrettyType
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder | GraphOut GraphType
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist | OWLOut OWLFormat
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder | XmlOut -- ^ development graph xml output
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa | DbOut -- ^ development graph database output
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder | JsonOut -- ^ development graph json output
f8cc2399c16fcda7e3bf9d901a0de0cc8a455f86Ewaryst Schulz | ExperimentalOut -- ^ for testing new functionality
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder | ThyFile -- ^ isabelle theory file
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder | DfgFile SPFType -- ^ SPASS input file
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder | ComptableXml
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder | SigFile Delta -- ^ signature as text
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder | TheoryFile Delta -- ^ signature with sentences as text
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder deriving Eq
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance Show OutType where
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder show o = case o of
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder PrettyOut p -> ppS ++ show p
1f2c732265a1292f0d7c51a4a7ca6be5dd370df6cmaeder GraphOut f -> graphE ++ show f
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder EnvOut -> envS
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist OWLOut oty -> show oty
3ec3a22fe2b9c38a3575c98a82b4e3f988af64a6Eugen Kuksa CLIFOut -> "clif"
4c872eeb600fe8479dbda395405cf13c3d573c24Soeren D. Schulze KIFOut -> "kif"
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder OmdocOut -> omdocS
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder XmlOut -> xmlS
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa DbOut -> dbS
024703c9d1326c23e307c0b0d453ed3358e87fe4cmaeder JsonOut -> "json"
f8cc2399c16fcda7e3bf9d901a0de0cc8a455f86Ewaryst Schulz ExperimentalOut -> experimentalS
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder HaskellOut -> hsS
53a3042e1da2253fd3f103bfef4deb47fc0bf6a6Ewaryst Schulz FreeCADOut -> "fcxml"
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ThyFile -> "thy"
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder DfgFile t -> dfgS ++ show t
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa TPTPFile -> tptpS
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ComptableXml -> "comptable.xml"
726baec6dfb69adb27f2afb4b2027fe5e7670c4aTill Mossakowski MedusaJson -> "medusa.json"
987bd66ac5bc367e2bbe50ce2b6355993fb335d9cmaeder RDFOut -> "nt"
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder SigFile d -> "sig" ++ show d
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder TheoryFile d -> "th" ++ show d
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian MaederplainOutTypeList :: [OutType]
59aa5703ac7f3b99e97cd5926e77088b256c5f40Christian MaederplainOutTypeList =
bbba10ee00dcf6bcbc9f22473b1acd0983b10512notanartist [ Prf, EnvOut ] ++ map OWLOut plainOwlFormats ++
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa [ RDFOut, CLIFOut, KIFOut, OmdocOut, XmlOut, JsonOut, DbOut, ExperimentalOut
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , HaskellOut, ThyFile, ComptableXml, MedusaJson, FreeCADOut, SymXml, SymsXml
beff4152e9f0fe90885458d1a1733b183a2a8816Christian MaederoutTypeList :: [OutType]
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian MaederoutTypeList = let dl = [Delta, Fully] in
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian Maeder plainOutTypeList
78c294da55788b25e175180168371c9536a6d440Christian Maeder ++ [ PrettyOut p | p <- prettyList ++ prettyList2]
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder ++ [ SigFile d | d <- dl ]
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder ++ [ TheoryFile d | d <- dl ]
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich ++ [ DfgFile x | x <- spfTypes]
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder ++ [ GraphOut f | f <- graphList ]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance Read OutType where
1ebf8299efa3cdb39c73d40d15e1d1a8a2246e68notanartist readsPrec _ = readShow outTypeList
e38219f3dd2f5711440478cbffa76ce3db530543cmaederdata Delta = Delta | Fully deriving Eq
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maederinstance Show Delta where
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder show d = case d of
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Delta -> deltaS
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder{- | 'PrettyType' describes the type of output we want the pretty-printer
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maederto generate -}
78c294da55788b25e175180168371c9536a6d440Christian Maederdata PrettyType = PrettyAscii Bool | PrettyLatex Bool | PrettyXml | PrettyHtml
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder deriving Eq
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance Show PrettyType where
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder show p = case p of
78c294da55788b25e175180168371c9536a6d440Christian Maeder PrettyAscii b -> (if b then "stripped." else "") ++ "het"
78c294da55788b25e175180168371c9536a6d440Christian Maeder PrettyLatex b -> (if b then "labelled." else "") ++ "tex"
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder PrettyXml -> xmlS
511284753313165e629cedf508752d6818ccc4d2Christian Maeder PrettyHtml -> "html"
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederprettyList :: [PrettyType]
78c294da55788b25e175180168371c9536a6d440Christian MaederprettyList = [PrettyAscii False, PrettyLatex False, PrettyXml, PrettyHtml]
78c294da55788b25e175180168371c9536a6d440Christian MaederprettyList2 :: [PrettyType]
78c294da55788b25e175180168371c9536a6d440Christian MaederprettyList2 = [PrettyAscii True, PrettyLatex True]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'GraphType' describes the type of Graph that we want generated
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederdata GraphType =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Dot Bool -- ^ True means show internal node labels
e38219f3dd2f5711440478cbffa76ce3db530543cmaeder deriving Eq
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance Show GraphType where
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder show g = case g of
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Dot si -> (if si then "exp." else "") ++ "dot"
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedergraphList :: [GraphType]
8865728716566f42fa73e7e0bc080ba3225df764Christian MaedergraphList = [Dot True, Dot False]
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder{- | 'options' describes all available options and is used to generate usage
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maederinformation -}
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederoptions :: [OptDescr Flag]
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder cslst = "is a comma-separated list"
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ++ crS ++ "of one or more from:"
8bb80c9684e905de8dcfcfb1291542677e7d77b6Christian Maeder joinBar l = "(" ++ intercalate "|" l ++ ")" in
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder [ Option "v" [verboseS] (OptArg parseVerbosity "0-5")
91ba5d95b2472cb075646b6120a559dc6581a867Christian Maeder "verbosity, default is -v1"
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder , Option "q" ["quiet"] (NoArg Quiet)
91ba5d95b2472cb075646b6120a559dc6581a867Christian Maeder "same as -v0, no output to stdout"
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder , Option "V" ["version"] (NoArg Version)
60e6795dd310e10194e12bb660575aadf941328bEugen Kuksa "print version information and exit"
60e6795dd310e10194e12bb660575aadf941328bEugen Kuksa , Option "" ["numeric-version"] (NoArg VersionNumeric)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder "print version number and exit"
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder , Option "h" ["help", "usage"] (NoArg Help)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder "print usage information and exit"
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder#ifdef UNI_PACKAGE
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder , Option "g" [guiS] (NoArg (Gui UseGui))
91ba5d95b2472cb075646b6120a559dc6581a867Christian Maeder "show graphs in windows"
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder , Option "u" ["uncolored"] (NoArg Uncolored)
91ba5d95b2472cb075646b6120a559dc6581a867Christian Maeder "no colors in shown graphs"
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder , Option "x" [xmlS] (NoArg XML)
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder "use xml packets to communicate"
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder#ifdef SERVER
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa , Option "P" [pidFileS] (ReqArg PidFile "FILEPATH")
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa "path to put the PID file of the hets server (omit if no pidfile is desired)"
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder , Option "X" ["server"] (NoArg Serve)
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder "start hets as web-server"
31bc219bae758272d0f064281b8ce7740a4553e9Till Mossakowski , Option "z" [logicListS] (NoArg OutputLogicList)
31bc219bae758272d0f064281b8ce7740a4553e9Till Mossakowski "output logic list as plain text"
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder , Option "G" [logicGraphS] (NoArg OutputLogicGraph)
a31430de8b0632d29f42634d6395e982bf31b14dChristian Maeder "output logic graph (as xml) or as graph (-g)"
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder , Option "I" [interactiveS] (NoArg Interactive)
f03420e44d8204b2945edaab5c70a84e7c381892Christian Maeder "run in interactive (console) mode"
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder , Option "F" [fileTypeS] (NoArg FileType)
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder "only display file type"
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder , Option "p" [skipS] (NoArg $ Analysis Skip)
91ba5d95b2472cb075646b6120a559dc6581a867Christian Maeder "skip static analysis, only parse"
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder , Option "s" [justStructuredS] (NoArg $ Analysis Structured)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder "skip basic, just do structured analysis"
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder , Option "l" [logicS] (ReqArg DefaultLogic "LOGIC")
91ba5d95b2472cb075646b6120a559dc6581a867Christian Maeder "choose logic, default is CASL"
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder , Option "y" [serializationS] (ReqArg DefaultSyntax "SER")
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder "choose different logic syntax"
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder , Option "L" [libdirsS] (ReqArg LibDirs "DIR")
f03420e44d8204b2945edaab5c70a84e7c381892Christian Maeder ("colon-separated list of directories"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa ++ crS ++ "containing DOL libraries."
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa ++ crS ++ "If an http[s] URL is specified here, it is treated as the last libdir because colons can occur in such URLs")
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder , Option "m" [modelSparQS] (ReqArg ModelSparQ "FILE")
d81905a5b924415c524d702df26204683c82c12eChristian Maeder "lisp file for SparQ definitions"
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder , Option "" [counterSparQS] (ReqArg parseCounter "0-99")
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder "maximal number of counter examples"
f03420e44d8204b2945edaab5c70a84e7c381892Christian Maeder , Option "c" [connectS] (ReqArg parseConnect "HOST:PORT")
f03420e44d8204b2945edaab5c70a84e7c381892Christian Maeder ("run (console) interface via connection"
f03420e44d8204b2945edaab5c70a84e7c381892Christian Maeder ++ crS ++ "to given host and port")
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder , Option "S" [listenS] (ReqArg parseListen "PORT")
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder "run interface/server by listening to the port"
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder , Option "" [whitelistS] (ReqArg Whitelist "IP4s")
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder $ "comma-separated list of IP4 addresses"
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder ++ crS ++ "(missing numbers at dots are wildcards)"
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder , Option "" [blacklistS] (ReqArg Blacklist "IP4s")
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder $ "comma-separated list of IP4 addresses"
9f4902edfa3d477e42343e0ec357a2f93b1119d1Christian Maeder ++ crS ++ "(example: 77.75.77.)"
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder , Option "C" [urlCatalogS] (ReqArg parseCatalog "URLS")
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder "comma-separated list of URL pairs: srcURL=tarURL"
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder , Option "i" [intypeS] (ReqArg parseInType "ITYPE")
f03420e44d8204b2945edaab5c70a84e7c381892Christian Maeder ("input file type can be one of:" ++
f03420e44d8204b2945edaab5c70a84e7c381892Christian Maeder concatMap (\ t -> crS ++ bS ++ t)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (map show plainInTypes ++
818b228955ef40dd5a253bd942dd6ab8779ed713Christian Maeder map (++ bracket bafS) [bracket treeS ++ genTermS]))
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder , Option "d" ["dump"] (ReqArg Dump "STRING")
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian Maeder "dump various strings"
55282ad62e8b6758abec43734ebde0015ac14b89Eugen Kuksa , Option "" ["disable-certificate-verification"]
55282ad62e8b6758abec43734ebde0015ac14b89Eugen Kuksa (NoArg DisableCertificateVerification)
55282ad62e8b6758abec43734ebde0015ac14b89Eugen Kuksa "Disable TLS certificate verification"
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder , Option "e" ["encoding"] (ReqArg parseEncoding "ENCODING")
353187efd08a2cb65226f414f192b59d312f27acChristian Maeder "latin1 or utf8 (default) encoding"
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder , Option "" [unlitS] (NoArg Unlit) "unlit input source"
33fcc19ef2b59493b4e91eebf701df95fd230765Christian Maeder , Option "" [relposS] (NoArg RelPos) "use relative file positions"
d4ebd9e5adc974cfa2bdf4bdd155e07be0e26f75Christian Maeder , Option "" [fullSignS] (NoArg FullSign) "xml output full signatures"
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa , Option "" [printASTS] (NoArg PrintAST) ("print AST in xml/json output")
0d79ea4ed8512a802ecb6645edac141e0fbcee3fChristian Maeder , Option "" [fullTheoriesS] (NoArg FullTheories) "xml output full theories"
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaeder , Option "" [accessTokenS] (ReqArg AccessToken "TOKEN")
9ee80c455784287a8b5e1b6bac1f8efa6a2f4bb3cmaeder "add access token to URLs (for ontohub)"
fb89f291c4e12ee44de11d4a900c445ed727b90dEugen Kuksa , Option "H" [httpRequestHeaderS] (ReqArg HttpRequestHeader "HTTP_HEADER")
fb89f291c4e12ee44de11d4a900c445ed727b90dEugen Kuksa ("additional headers to use for HTTP requests"
fb89f291c4e12ee44de11d4a900c445ed727b90dEugen Kuksa ++ crS ++ "this option can be used multiple times")
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder , Option "O" [outdirS] (ReqArg OutDir "DIR")
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder "destination directory for output files"
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder , Option "o" [outtypesS] (ReqArg parseOutTypes "OTYPES")
4a2f7efdf67dfcda0946f1b6373f41976ddea7a4Christian Maeder ("output file types, default nothing," ++ crS ++
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder cslst ++ crS ++ concatMap ( \ t -> bS ++ show t ++ crS)
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian Maeder plainOutTypeList
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder ++ bS ++ joinBar (map show [SigFile Fully,
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder TheoryFile Fully])
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian Maeder ++ bracket deltaS ++ crS
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder ++ bS ++ ppS ++ joinBar (map show prettyList) ++ crS
78c294da55788b25e175180168371c9536a6d440Christian Maeder ++ bS ++ ppS ++ joinBar (map show prettyList2) ++ crS
1f2c732265a1292f0d7c51a4a7ca6be5dd370df6cmaeder ++ bS ++ graphE ++ joinBar (map show graphList) ++ crS
ab2f38d9cd1249f6bc9cc5b838dc2fcd76189c0fChristian Maeder ++ bS ++ dfgS ++ bracket cS ++ crS
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa ++ bS ++ tptpS ++ bracket cS)
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , Option "" ["database-do-not-migrate"] (NoArg DatabaseDoNotMigrate)
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa ("Disallow Hets to create or alter the database tables" ++ crS
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa ++ "This option is ignored if the option --database-config is given.")
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , Option "" ["database-file"] (ReqArg DatabaseOutputFile "FILEPATH")
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa ("path to the sqlite database file" ++ crS
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa ++ "This option is ignored if the option --database-config is given.")
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , Option "" ["database-config"] (ReqArg DatabaseConfigFile "FILEPATH")
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa "path to the database configuration (yaml) file"
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , Option "" ["database-subconfig"] (ReqArg DatabaseSubConfigKey "KEY")
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa ("subconfig of the database-config" ++ crS
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa ++ "one of: production, development, test")
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , Option "" ["database-fileversion-id"] (ReqArg DatabaseFileVersionId "ID")
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa "ID (sha1-hash) of the file version to associate the data with"
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , Option "" ["database-reanalyze"] (NoArg DatabaseReanalyze)
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa "Overwrite data of this document and its imports in the database"
8d780c893d6df5dab3dcc7d8444b7517f6547f11Christian Maeder , Option "U" ["xupdate"] (ReqArg XUpdate "FILE")
8d780c893d6df5dab3dcc7d8444b7517f6547f11Christian Maeder "apply additional xupdates from file"
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder , Option "R" [recursiveS] (NoArg Recurse)
083bc1972a66d73749760eab3a90bf4eb9ca7951Christian Maeder "output also imported libraries"
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder , Option "A" [applyAutomaticRuleS] (NoArg ApplyAutomatic)
bc263f610d20a9cd3014ddfca903026127fa0d48Christian Maeder "apply automatic dev-graph strategy"
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder , Option "N" [normalFormS] (NoArg NormalForm)
966519955f5f7111abac20118563132b9dd41165Christian Maeder "compute normal forms (takes long)"
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder , Option "n" [namedSpecsS] (ReqArg (Specs . parseSIdOpts) "NSPECS")
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder ("process specs option " ++ crS ++ cslst ++ " SIMPLE-ID")
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder , Option "w" [viewS] (ReqArg (Views . parseSIdOpts) "NVIEWS")
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder ("process views option " ++ crS ++ cslst ++ " SIMPLE-ID")
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder , Option "t" [transS] (ReqArg parseTransOpt "TRANS")
0ae7a79e865d4a6022d705d160530682b3c1f825Christian Maeder ("translation option " ++ crS ++
f03420e44d8204b2945edaab5c70a84e7c381892Christian Maeder "is a colon-separated list" ++
0ae7a79e865d4a6022d705d160530682b3c1f825Christian Maeder crS ++ "of one or more from: SIMPLE-ID")
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder , Option "a" [amalgS] (ReqArg parseCASLAmalg "ANALYSIS")
dff1de7ad15d1582e25d636c3724dd202874897fChristian Maeder ("CASL amalgamability analysis options" ++ crS ++ cslst ++
34d14197eb3dd643a8e6ef3ed8cba5629528e97fAivaras Jakubauskas crS ++ joinBar (map show caslAmalgOpts)),
34d14197eb3dd643a8e6ef3ed8cba5629528e97fAivaras Jakubauskas Option "M" ["MMT"] (NoArg UseMMT)
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder-- | options that require arguments for the wep-api excluding \"translation\"
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaederoptionArgs :: [(String, String -> Flag)]
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaederoptionArgs = foldr (\ o l -> case o of
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder Option _ (s : _) (ReqArg f _) _ | s /= transS -> (s, f) : l
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder _ -> l) [] options
0a26144c20fa9cdcd05011ca5019cbac8e4afae0cmaeder-- | command line switches for the wep-api excluding non-dev-graph related ones
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaederoptionFlags :: [(String, Flag)]
01a143ff12e858a18437e18aab76b32f5bbb18c4cmaederoptionFlags = dropWhile ((/= justStructuredS). fst) $ foldr (\ o l -> case o of
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder Option _ (s : _) (NoArg f) _ -> (s, f) : l
d1c667fd9445963d9d31e2cf5d0ead15e77082a4cmaeder _ -> l) [] options
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- parser functions returning Flags --
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'parseVerbosity' parses a 'Verbose' Flag from user input
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian MaederparseVerbosity :: Maybe String -> Flag
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederparseVerbosity ms = case ms of
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Nothing -> Verbose 2
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder Just s -> Verbose $ parseInt s
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian MaederparseInt :: String -> Int
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian MaederparseInt s = fromMaybe (hetsError $ s ++ " is not a valid INT") $ readMaybe s
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian MaederparseCounter :: String -> Flag
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian MaederparseCounter = CounterSparQ . parseInt
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederdivideIntoPortHost :: String -> Bool -> (String, String) -> (String, String)
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian MaederdivideIntoPortHost s sw (accP, accH) = case s of
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder ':' : ll -> divideIntoPortHost ll True (accP, accH)
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder c : ll -> if sw then divideIntoPortHost ll True (accP, c : accH)
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder else divideIntoPortHost ll False (c : accP, accH)
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder [] -> (accP, accH)
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu-- | 'parseConnect' parses a port Flag from user input
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan PascanuparseConnect :: String -> Flag
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan PascanuparseConnect s
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder = let (sP, sH) = divideIntoPortHost s False ([], [])
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu in case reads sP of
9308cb2aebeae23f49713896e6d7028b0ac0f83enotanartist [(i, "")] -> Connect i sH
2360728d4185c0c04279c999941c64d36626af79Christian Maeder _ -> Connect (-1) sH
fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan PascanuparseListen :: String -> Flag
66a774f13272fde036481edd2298081ab3d04678Razvan Pascanu = case reads s of
9308cb2aebeae23f49713896e6d7028b0ac0f83enotanartist [(i, "")] -> Listen i
2360728d4185c0c04279c999941c64d36626af79Christian Maeder _ -> Listen (-1)
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian MaederparseEncoding :: String -> Flag
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian MaederparseEncoding s = case map toLower $ trim s of
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder "latin1" -> IOEncoding Latin1
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder "utf8" -> IOEncoding Utf8
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder r -> hetsError (r ++ " is not a valid encoding")
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | intypes useable for downloads
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederdownloadExtensions :: [String]
9dd71ac51c9a6e72bcb126224f9c64131698b636Christian MaederdownloadExtensions = map ('.' :) $
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder map show plainInTypes
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ++ map ((treeS ++) . show) [ATermIn BAF, ATermIn NonBAF]
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder ++ map show aInTypes
0ea2cddb8715a770e646895e16b7b8085f49167cChristian Maeder-- | remove the extension from a file
0ea2cddb8715a770e646895e16b7b8085f49167cChristian MaederrmSuffix :: FilePath -> FilePath
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian MaederrmSuffix = fst . stripSuffix (envSuffix : downloadExtensions)
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian Maeder-- | the suffix of env files
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian MaederenvSuffix :: String
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian MaederenvSuffix = '.' : envS
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder-- | the suffix of env files
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian MaederprfSuffix :: String
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian MaederprfSuffix = '.' : prfS
a461314c811f4187dff85c8be079a41b2f13f176Christian MaederisDefLogic :: String -> HetcatsOpts -> Bool
a461314c811f4187dff85c8be079a41b2f13f176Christian MaederisDefLogic s = (s ==) . defLogic
a461314c811f4187dff85c8be079a41b2f13f176Christian MaederdefLogicIsDMU :: HetcatsOpts -> Bool
a461314c811f4187dff85c8be079a41b2f13f176Christian MaederdefLogicIsDMU = isDefLogic "DMU"
0130083f314580170af1195037be3325f125fbceChristian MaedergetExtensions :: HetcatsOpts -> [String]
0130083f314580170af1195037be3325f125fbceChristian MaedergetExtensions opts = case intype opts of
c770b05f3d85f8eeb25ba15f7192044f9dd534ddSoeren D. Schulze | defLogicIsDMU opts -> [".xml"]
c770b05f3d85f8eeb25ba15f7192044f9dd534ddSoeren D. Schulze | isDefLogic "Framework" opts
c770b05f3d85f8eeb25ba15f7192044f9dd534ddSoeren D. Schulze -> [".elf", ".thy", ".maude", ".het"]
c770b05f3d85f8eeb25ba15f7192044f9dd534ddSoeren D. Schulze GuessIn -> downloadExtensions
c770b05f3d85f8eeb25ba15f7192044f9dd534ddSoeren D. Schulze e@(ATermIn _) -> ['.' : show e, '.' : treeS ++ show e]
0130083f314580170af1195037be3325f125fbceChristian Maeder e -> ['.' : show e]
0130083f314580170af1195037be3325f125fbceChristian Maeder ++ [envSuffix]
0130083f314580170af1195037be3325f125fbceChristian MaedergetFileNames :: [String] -> FilePath -> [FilePath]
0130083f314580170af1195037be3325f125fbceChristian MaedergetFileNames exts file =
0130083f314580170af1195037be3325f125fbceChristian Maeder file : map (rmSuffix file ++) exts
057b3bffc58757a98e8e7c1aeaf5cbbc986b3117Christian Maeder-- | checks if a source file for the given file name exists
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian MaederexistsAnSource :: HetcatsOpts -> FilePath -> IO (Maybe FilePath)
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian MaederexistsAnSource opts file = do
057b3bffc58757a98e8e7c1aeaf5cbbc986b3117Christian Maeder let names = getFileNames (getExtensions opts) file
c770b05f3d85f8eeb25ba15f7192044f9dd534ddSoeren D. Schulze -- look for the first existing file
c770b05f3d85f8eeb25ba15f7192044f9dd534ddSoeren D. Schulze validFlags <- mapM doesFileExist names
c770b05f3d85f8eeb25ba15f7192044f9dd534ddSoeren D. Schulze return . fmap snd . find fst $ zip validFlags names
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder-- | should env be written
9d6562465b41f17c7967d4e5678f34811d958cb2Christian MaederhasEnvOut :: HetcatsOpts -> Bool
daec53c285f692c56db0cefe16061b46ba602cf0Christian MaederhasEnvOut = any ( \ o -> case o of
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder EnvOut -> True
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder _ -> False) . outtypes
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder-- | should prf be written
daec53c285f692c56db0cefe16061b46ba602cf0Christian MaederisPrfOut :: OutType -> Bool
daec53c285f692c56db0cefe16061b46ba602cf0Christian MaederisPrfOut o = case o of
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder-- | should prf be written
daec53c285f692c56db0cefe16061b46ba602cf0Christian MaederhasPrfOut :: HetcatsOpts -> Bool
daec53c285f692c56db0cefe16061b46ba602cf0Christian MaederhasPrfOut = any isPrfOut . outtypes
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder-- | remove prf writing
daec53c285f692c56db0cefe16061b46ba602cf0Christian MaederremovePrfOut :: HetcatsOpts -> HetcatsOpts
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaederremovePrfOut opts =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder opts { outtypes = filter (not . isPrfOut) $ outtypes opts }
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maedergets two Paths and checks if the first file is not older than the
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maedersecond one and should return True for two identical files -}
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian MaedercheckRecentEnv :: HetcatsOpts -> FilePath -> FilePath -> IO Bool
9db2bd64088c7e5935b94dd9c3ad5cdc24f48814Christian MaedercheckRecentEnv opts fp1 base2 = catchIOException False $ do
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder fp1_time <- getModificationTime fp1
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder maybe_source_file <- existsAnSource opts {intype = GuessIn} base2
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder maybe (return False) ( \ fp2 -> do
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder fp2_time <- getModificationTime fp2
0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder return (fp1_time >= fp2_time)) maybe_source_file
0b13f102310e03a20b38c870b5acb88712f316a4Christian MaederparseCatalog :: String -> Flag
0b13f102310e03a20b38c870b5acb88712f316a4Christian MaederparseCatalog str = UrlCatalog $ map ((\ l -> case l of
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder [a, b] -> (a, b)
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder _ -> hetsError (str ++ " is not a valid URL catalog"))
0b13f102310e03a20b38c870b5acb88712f316a4Christian Maeder . splitOn '=') $ splitOn ',' str
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'parseInType' parses an 'InType' Flag from user input
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederparseInType :: String -> Flag
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederparseInType = InType . parseInType1
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'parseInType1' parses an 'InType' Flag from a String
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederparseInType1 :: String -> InType
2353f65833a3da763392f771223250cd50b8d873Christian MaederparseInType1 str =
2353f65833a3da763392f771223250cd50b8d873Christian Maeder case reads str of
9308cb2aebeae23f49713896e6d7028b0ac0f83enotanartist [(t, "")] -> t
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder _ -> hetsError (str ++ " is not a valid ITYPE")
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder {- the mere typo read instead of reads caused the runtime error:
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Fail: Prelude.read: no parse -}
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- 'parseOutTypes' parses an 'OutTypes' Flag from user input
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederparseOutTypes :: String -> Flag
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederparseOutTypes str = case reads $ bracket str of
9308cb2aebeae23f49713896e6d7028b0ac0f83enotanartist [(l, "")] -> OutTypes l
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder _ -> hetsError (str ++ " is not a valid OTYPES")
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian Maeder-- | parses a comma separated list from user input
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian MaederparseSIdOpts :: String -> [SIMPLE_ID]
00df6fd583c19393fa141d5a0e21ac74c7bf5b19Christian MaederparseSIdOpts = map mkSimpleId . splitOn ','
528539f3d544c24afe14e979fe51f03e50aa6e9cChristian Maeder-- | 'parseTransOpt' parses a 'Trans' Flag from user input
0ae7a79e865d4a6022d705d160530682b3c1f825Christian MaederparseTransOpt :: String -> Flag
863d4b011d04907325f3eed8e89975e38603cb05Christian MaederparseTransOpt = Trans . map mkSimpleId . splitPaths
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | guesses the InType
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederguess :: String -> InType -> InType
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maederguess file itype = case itype of
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder GuessIn -> guessInType file
59a10395caff224b2ec541f94dac5082a506c00fChristian Maeder-- | 'guessInType' parses an 'InType' from the FilePath
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederguessInType :: FilePath -> InType
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian MaederguessInType file = case fileparse downloadExtensions file of
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder (_, _, Just ('.' : suf)) -> parseInType1 suf
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder (_, _, _) -> GuessIn
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'parseCASLAmalg' parses CASL amalgamability options
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederparseCASLAmalg :: String -> Flag
2353f65833a3da763392f771223250cd50b8d873Christian MaederparseCASLAmalg str =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder case reads $ bracket str of
9308cb2aebeae23f49713896e6d7028b0ac0f83enotanartist [(l, "")] -> CASLAmalg $ filter ( \ o -> case o of
2353f65833a3da763392f771223250cd50b8d873Christian Maeder NoAnalysis -> False
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder _ -> True ) l
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder _ -> hetsError $ str ++
12aef5992d3af07dee81a4e02cf4be65a83f28bcChristian Maeder " is not a valid CASL amalgamability analysis option list"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- main functions --
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'hetcatsOpts' parses sensible HetcatsOpts from ARGV
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederhetcatsOpts :: [String] -> IO HetcatsOpts
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederhetcatsOpts argv =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let argv' = filter (not . isUni) argv
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder isUni = isPrefixOf "--uni"
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder in case getOpt Permute options argv' of
057b3bffc58757a98e8e7c1aeaf5cbbc986b3117Christian Maeder (opts, nonOpts, []) ->
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder do flags <- checkFlags opts
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa let opts' = (foldr (flip makeOpts) defaultHetcatsOpts flags)
057b3bffc58757a98e8e7c1aeaf5cbbc986b3117Christian Maeder { infiles = nonOpts }
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa setupDatabaseOptions opts'
502483734c83d0bf1eadcc94113d0362f8713784Christian Maeder (_, _, errs) -> hetsIOError (concat errs)
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa setupDatabaseOptions :: HetcatsOpts -> IO HetcatsOpts
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa setupDatabaseOptions opts = do
649fdc0d0502d62d160c150684356fef2c273484Eugen Kuksa let filepath = if null $ infiles opts then "" else head $ infiles opts
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa { DBConfig.contextFileVersion = databaseFileVersionId opts
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa -- If the fileVersionId is not given, Hets has not been called by Ontohub.
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa -- Hence, there is no git handling and we always need to reanalyze the
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa let databaseReanalyze' =
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa null (databaseFileVersionId opts) || databaseReanalyze opts
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa dbConfig <- if DbOut `elem` outtypes opts
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa (databaseOutputFile opts)
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa (databaseConfigFile opts)
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa (databaseSubConfigKey opts)
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa (databaseDoMigrate opts)
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa return opts { databaseConfig = dbConfig
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , databaseContext = dbContext
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa , databaseReanalyze = databaseReanalyze'
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen KuksaprintOptionsWarnings :: HetcatsOpts -> IO ()
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen KuksaprintOptionsWarnings opts =
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa let v = verbose opts in
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa unless (null (pidFile opts) || serve opts)
fe495a0978e5aa70776103c37fb0eb2bd6abea69Eugen Kuksa (verbMsgIOLn v 1 "option -P has no effect because it is used without -X")
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'checkFlags' checks all parsed Flags for sanity
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercheckFlags :: [Flag] -> IO [Flag]
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian MaedercheckFlags fs = do
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder let collectFlags = collectDirs
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder . collectOutTypes
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder . collectVerbosity
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder . collectSpecOpts
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -- collect some more here?
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder h = null [ () | Help <- fs]
96ae1a1d2197d0e0d5b80da2474b64c456feb1b0Christian Maeder v = null [ () | Version <- fs]
60e6795dd310e10194e12bb660575aadf941328bEugen Kuksa vn = null [ () | VersionNumeric <- fs]
afb32b54f3e87b51c5a6242040022f497f7f20abChristian Maeder unless h $ putStr hetsUsage
60e6795dd310e10194e12bb660575aadf941328bEugen Kuksa unless v $ putStrLn hetsVersion
60e6795dd310e10194e12bb660575aadf941328bEugen Kuksa unless vn $ putStrLn hetsVersionNumeric
60e6795dd310e10194e12bb660575aadf941328bEugen Kuksa unless (h && v && vn) exitSuccess
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder collectFlags fs
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- auxiliary functions: FileSystem interaction --
2353f65833a3da763392f771223250cd50b8d873Christian Maeder-- | check if infile is uri
4b1833c7d3af466e6bcba24f16304e0a78e8da87Christian MaedercheckUri :: FilePath -> Bool
fba4eac6b080849889892e1e273ac4c74ddde840Christian MaedercheckUri file = "://" `isPrefixOf` dropWhile isAlpha file
4347b243063d414f97a68b64e30a4f27a612af0aChristian Maeder -- (http://, https://, ftp://, file://, etc.)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'checkOutDirs' checks a list of OutDir for sanity
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercheckOutDirs :: [Flag] -> IO [Flag]
2353f65833a3da763392f771223250cd50b8d873Christian MaedercheckOutDirs fs = do
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder [] -> return ()
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder [f] -> checkOutDir f
502483734c83d0bf1eadcc94113d0362f8713784Christian Maeder _ -> hetsIOError
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder "Only one output directory may be specified on the command line"
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder-- | 'checkLibDirs' checks a list of LibDir for sanity
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian MaedercheckLibDirs :: [Flag] -> IO [Flag]
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian MaedercheckLibDirs fs =
dbc98cd8a9a829e020cfa0a9f3aff89de75caaa9Christian Maeder s <- getEnvDef "HETS_LIB" ""
2353f65833a3da763392f771223250cd50b8d873Christian Maeder if null s then return [] else do
cb2044812811d66efe038d914966e04290be93faChristian Maeder let d = LibDirs s
cb2044812811d66efe038d914966e04290be93faChristian Maeder checkLibDirs [d]
0130083f314580170af1195037be3325f125fbceChristian Maeder [LibDirs f] -> mapM_ checkLibDir (joinHttpLibPath $ splitPaths f)
502483734c83d0bf1eadcc94113d0362f8713784Christian Maeder _ -> hetsIOError
cb2044812811d66efe038d914966e04290be93faChristian Maeder "Only one library path may be specified on the command line"
0130083f314580170af1195037be3325f125fbceChristian MaederjoinHttpLibPath :: [String] -> [String]
0130083f314580170af1195037be3325f125fbceChristian MaederjoinHttpLibPath l = case l of
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa p : f : r | p == "file" && take 2 f == "//" ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa (p ++ ':' : f) : joinHttpLibPath r
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa p : f : _ | elem p ["http", "https"] && take 2 f == "//" ->
7bb0a9e92bc7a6f868eaa0b9c3212c0af4f96b7fEugen Kuksa [intercalate ":" l]
0130083f314580170af1195037be3325f125fbceChristian Maeder f : r -> f : joinHttpLibPath r
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder-- | 'checkLibDir' checks a single LibDir for sanity
cb2044812811d66efe038d914966e04290be93faChristian MaedercheckLibDir :: FilePath -> IO ()
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian MaedercheckLibDir file = do
0130083f314580170af1195037be3325f125fbceChristian Maeder exists <- if checkUri file then return True else doesDirectoryExist file
502483734c83d0bf1eadcc94113d0362f8713784Christian Maeder unless exists . hetsIOError $ "Not a valid library directory: " ++ file
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'checkOutDir' checks a single OutDir for sanity
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian MaedercheckOutDir :: Flag -> IO ()
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian MaedercheckOutDir (OutDir file) = do
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder exists <- doesDirectoryExist file
502483734c83d0bf1eadcc94113d0362f8713784Christian Maeder unless exists . hetsIOError $ "Not a valid output directory: " ++ file
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian MaedercheckOutDir _ = return ()
2353f65833a3da763392f771223250cd50b8d873Christian Maeder-- auxiliary functions: collect flags --
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian MaedercollectDirs :: [Flag] -> IO [Flag]
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian MaedercollectDirs fs = do
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder let (ods, fs1) = partition isOutDir fs
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder (lds, fs2) = partition isLibDir fs1
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder isOutDir (OutDir _) = True
2360728d4185c0c04279c999941c64d36626af79Christian Maeder isOutDir _ = False
cb2044812811d66efe038d914966e04290be93faChristian Maeder isLibDir (LibDirs _) = True
2360728d4185c0c04279c999941c64d36626af79Christian Maeder isLibDir _ = False
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder ods' <- checkOutDirs ods
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder lds' <- checkLibDirs lds
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian Maeder return $ ods' ++ lds' ++ fs2
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercollectVerbosity :: [Flag] -> [Flag]
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercollectVerbosity fs =
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder let (v, fs') = foldr (\ f (n, rs) -> case f of
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder Verbose x -> (if n < 0 then x else n + x, rs)
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder _ -> (n, f : rs)) (-1, []) fs
8c8545dd3bf34fbcbc16904b65d249658f8f9efcChristian Maeder in if v < 0 || not (null [() | Quiet <- fs']) then fs' else Verbose v : fs'
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercollectOutTypes :: [Flag] -> [Flag]
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercollectOutTypes fs =
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder let (ots, fs') = foldr (\ f (os, rs) -> case f of
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder OutTypes ot -> (ot ++ os, rs)
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder _ -> (os, f : rs)) ([], []) fs
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder in if null ots then fs' else OutTypes ots : fs'
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian MaedercollectSpecOpts :: [Flag] -> [Flag]
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian MaedercollectSpecOpts fs =
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder let (specs, fs') = foldr (\ f (os, rs) -> case f of
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder Specs ot -> (ot ++ os, rs)
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder _ -> (os, f : rs)) ([], []) fs
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder in if null specs then fs' else Specs specs : fs'
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- auxiliary functions: error messages --
0ede68718d0fd43b5d67c233ccfb7a2b673fc9cbChristian Maeder-- | only print the error (and no usage info)
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederhetsError :: String -> a
0ede68718d0fd43b5d67c233ccfb7a2b673fc9cbChristian MaederhetsError = error . ("command line usage error (see 'hets -h')\n" ++)
0ede68718d0fd43b5d67c233ccfb7a2b673fc9cbChristian Maeder-- | print error and usage and exit with code 2
502483734c83d0bf1eadcc94113d0362f8713784Christian MaederhetsIOError :: String -> IO a
502483734c83d0bf1eadcc94113d0362f8713784Christian MaederhetsIOError s = do
1c4dfa148603d4fcf4cdd2ed66c8b6e1de0dd696Till Mossakowski unless (null s) $ hPutStrLn stderr s
1c4dfa148603d4fcf4cdd2ed66c8b6e1de0dd696Till Mossakowski putStr "for Hets usage, use: hets -h\n"
502483734c83d0bf1eadcc94113d0362f8713784Christian Maeder exitWith $ ExitFailure 2
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'hetsUsage' generates usage information for the commandline
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederhetsUsage :: String
9175e29c044318498a40f323f189f9dfd50378efChristian MaederhetsUsage = let header = "Usage: hets [OPTION ...] [FILE ...] [+RTS -?]"
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder in usageInfo header options
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian Maeder{- | 'putIfVerbose' prints a given String to StdOut when the given HetcatsOpts'
b6ff72be73dad3d1394cf2c71e29e67624ff030bChristian MaederVerbosity exceeds the given level -}
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederputIfVerbose :: HetcatsOpts -> Int -> String -> IO ()
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian MaederputIfVerbose opts level =
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian Maeder when (outputToStdout opts) . when (verbose opts >= level) . putStrLn
bbba6dd86153aacb0f662b182b128df0eb09fd54Christian MaederdoDump :: HetcatsOpts -> String -> IO () -> IO ()
be43c3fa0292555bd126784ae27ff5c1d23438cbChristian MaederdoDump opts str = when (elem str $ dumpOpts opts)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | show diagnostic messages (see Result.hs), according to verbosity level
16b71dad8d398af412d66a4f4763f1ada5b03d23Christian MaedershowDiags :: HetcatsOpts -> [Diagnosis] -> IO ()
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedershowDiags opts ds =
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder runResultT (showDiags1 opts $ liftR $ Result ds Nothing) >> return ()
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | show diagnostic messages (see Result.hs), according to verbosity level
7f7460e7095628f3437b116ee78d3043d11f8febChristian MaedershowDiags1 :: HetcatsOpts -> ResultT IO a -> ResultT IO a
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian MaedershowDiags1 opts res =
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa let dbout = DbOut `elem` outtypes opts in
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa if outputToStdout opts || dbout then do
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Result ds res' <- lift $ runResultT res
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa when (outputToStdout opts) $ lift $ printDiags (verbose opts) ds
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa when dbout $ lift $
a389e88e0acb83d8489bdc5e55bc5522b152bbecEugen Kuksa saveDiagnoses (databaseConfig opts) (databaseContext opts) (verbose opts) ds
a3a7d8b3cdf05c8040c62dbcf9a15dc5042cd721Christian Maeder Just res'' -> return res''
5941ba0b9a99ac98f78a89a9f3303102657e36ccChristian Maeder Nothing -> liftR $ Result [] Nothing