{-# LANGUAGE CPP #-}
{- |
Module      :  ./Driver/Options.hs
Description :  Datatypes and functions for options that hets understands.
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

Datatypes for options that hets understands.
   Useful functions to parse and check user-provided values.
-}

module Driver.Options
  ( HetcatsOpts (..)
  , Flag
  , optionArgs
  , optionFlags
  , accessTokenS
  , makeOpts
  , AnaType (..)
  , GuiType (..)
  , InType (..)
  , plainInTypes
  , OWLFormat (..)
  , plainOwlFormats
  , OutType (..)
  , PrettyType (..)
  , prettyList
  , GraphType (..)
  , SPFType (..)
  , ATType
  , Delta
  , hetcatsOpts
  , printOptionsWarnings
  , isStructured
  , guess
  , rmSuffix
  , envSuffix
  , prfSuffix
  , removePrfOut
  , hasEnvOut
  , hasPrfOut
  , getFileNames
  , existsAnSource
  , getExtensions
  , checkRecentEnv
  , downloadExtensions
  , defaultHetcatsOpts
  , showDiags
  , showDiags1
  , putIfVerbose
  , doDump
  , checkUri
  , defLogicIsDMU
  , useCatalogURL
  , hetsIOError
  ) where

import Driver.Version

import qualified Persistence.DBConfig as DBConfig
import Persistence.Diagnosis

import Common.Utils
import Common.IO
import Common.Id
import Common.Result
import Common.ResultT
import Common.Amalgamate
import Common.Keywords

import System.Directory
import System.Console.GetOpt
import System.Exit
import System.IO

import Control.Monad
import Control.Monad.Trans
import Data.Char
import Data.List
import Data.Maybe

-- | translate a given http reference using the URL catalog
useCatalogURL :: HetcatsOpts -> FilePath -> FilePath
useCatalogURL :: HetcatsOpts -> FilePath -> FilePath
useCatalogURL opts :: HetcatsOpts
opts fname :: FilePath
fname = case ((FilePath, FilePath) -> Maybe FilePath)
-> [(FilePath, FilePath)] -> [FilePath]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe
    (\ (a :: FilePath
a, b :: FilePath
b) -> (FilePath -> FilePath) -> Maybe FilePath -> Maybe FilePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (FilePath
b FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++) (Maybe FilePath -> Maybe FilePath)
-> Maybe FilePath -> Maybe FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> Maybe FilePath
forall a. Eq a => [a] -> [a] -> Maybe [a]
stripPrefix FilePath
a FilePath
fname)
    ([(FilePath, FilePath)] -> [FilePath])
-> [(FilePath, FilePath)] -> [FilePath]
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> [(FilePath, FilePath)]
urlCatalog HetcatsOpts
opts of
  m :: FilePath
m : _ -> FilePath
m
  _ -> FilePath
fname

bracket :: String -> String
bracket :: FilePath -> FilePath
bracket s :: FilePath
s = "[" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
s FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "]"

-- use the same strings for parsing and printing!
verboseS, intypeS, outtypesS, skipS, justStructuredS, transS, lossyTransS,
     guiS, libdirsS, outdirS, amalgS, recursiveS, namedSpecsS,
     interactiveS, modelSparQS, counterSparQS, connectS, xmlS, dbS, listenS,
     applyAutomaticRuleS, normalFormS, unlitS, pidFileS :: String

modelSparQS :: FilePath
modelSparQS = "modelSparQ"
counterSparQS :: FilePath
counterSparQS = "counterSparQ"
verboseS :: FilePath
verboseS = "verbose"
intypeS :: FilePath
intypeS = "input-type"
outtypesS :: FilePath
outtypesS = "output-types"
skipS :: FilePath
skipS = "just-parse"
justStructuredS :: FilePath
justStructuredS = "just-structured"
guiS :: FilePath
guiS = "gui"
libdirsS :: FilePath
libdirsS = "hets-libdirs"
outdirS :: FilePath
outdirS = "output-dir"
amalgS :: FilePath
amalgS = "casl-amalg"
namedSpecsS :: FilePath
namedSpecsS = "named-specs"
transS :: FilePath
transS = "translation"
lossyTransS :: FilePath
lossyTransS = "lossy"
recursiveS :: FilePath
recursiveS = "recursive"
interactiveS :: FilePath
interactiveS = "interactive"
connectS :: FilePath
connectS = "connect"
xmlS :: FilePath
xmlS = "xml"
dbS :: FilePath
dbS = "db"
listenS :: FilePath
listenS = "listen"
pidFileS :: FilePath
pidFileS = "pidfile"
applyAutomaticRuleS :: FilePath
applyAutomaticRuleS = "apply-automatic-rule"
normalFormS :: FilePath
normalFormS = "normal-form"
unlitS :: FilePath
unlitS = "unlit"

urlCatalogS :: String
urlCatalogS :: FilePath
urlCatalogS = "url-catalog"

relposS :: String
relposS :: FilePath
relposS = "relative-positions"

fullSignS :: String
fullSignS :: FilePath
fullSignS = "full-signatures"

printASTS :: String
printASTS :: FilePath
printASTS = "print-AST"

fullTheoriesS :: String
fullTheoriesS :: FilePath
fullTheoriesS = "full-theories"

logicGraphS :: String
logicGraphS :: FilePath
logicGraphS = "logic-graph"

logicListS :: String
logicListS :: FilePath
logicListS = "logic-list"

fileTypeS :: String
fileTypeS :: FilePath
fileTypeS = "file-type"

blacklistS :: String
blacklistS :: FilePath
blacklistS = "blacklist"

whitelistS :: String
whitelistS :: FilePath
whitelistS = "whitelist"

accessTokenS :: String
accessTokenS :: FilePath
accessTokenS = "access-token"

httpRequestHeaderS :: String
httpRequestHeaderS :: FilePath
httpRequestHeaderS = "http-request-header"

genTermS, treeS, bafS :: String
genTermS :: FilePath
genTermS = "gen_trm"
treeS :: FilePath
treeS = "tree."
bafS :: FilePath
bafS = ".baf"

graphE, ppS, envS, deltaS, prfS, omdocS, hsS, experimentalS :: String
graphE :: FilePath
graphE = "graph."
ppS :: FilePath
ppS = "pp."
envS :: FilePath
envS = "env"
deltaS :: FilePath
deltaS = ".delta"
prfS :: FilePath
prfS = "prf"
omdocS :: FilePath
omdocS = "omdoc"
hsS :: FilePath
hsS = "hs"
experimentalS :: FilePath
experimentalS = "exp"

tptpS, dfgS, cS :: String
tptpS :: FilePath
tptpS = "tptp"
dfgS :: FilePath
dfgS = "dfg"
cS :: FilePath
cS = ".c"

showOpt :: String -> String
showOpt :: FilePath -> FilePath
showOpt s :: FilePath
s = if FilePath -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null FilePath
s then "" else " --" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
s

showEqOpt :: String -> String -> String
showEqOpt :: FilePath -> FilePath -> FilePath
showEqOpt k :: FilePath
k s :: FilePath
s = if FilePath -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null FilePath
s then "" else FilePath -> FilePath
showOpt FilePath
k FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "=" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
s

-- main Datatypes --

-- | 'HetcatsOpts' is a record of all options received from the command line
data HetcatsOpts = HcOpt     -- for comments see usage info
  { HetcatsOpts -> AnaType
analysis :: AnaType
  , HetcatsOpts -> GuiType
guiType :: GuiType
  , HetcatsOpts -> [(FilePath, FilePath)]
urlCatalog :: [(String, String)]
  , HetcatsOpts -> [FilePath]
infiles :: [FilePath] -- ^ files to be read
  , HetcatsOpts -> [SIMPLE_ID]
specNames :: [SIMPLE_ID] -- ^ specs to be processed
  , HetcatsOpts -> [SIMPLE_ID]
transNames :: [SIMPLE_ID] -- ^ comorphism to be processed
  , HetcatsOpts -> Bool
lossyTrans :: Bool                
  , HetcatsOpts -> [SIMPLE_ID]
viewNames :: [SIMPLE_ID] -- ^ views to be processed
  , HetcatsOpts -> InType
intype :: InType
  , HetcatsOpts -> [FilePath]
libdirs :: [FilePath]
  , HetcatsOpts -> FilePath
modelSparQ :: FilePath
  , HetcatsOpts -> Int
counterSparQ :: Int
  , HetcatsOpts -> FilePath
outdir :: FilePath
  , HetcatsOpts -> [OutType]
outtypes :: [OutType]
  , HetcatsOpts -> Bool
databaseDoMigrate :: Bool
  , HetcatsOpts -> FilePath
databaseOutputFile :: FilePath
  , HetcatsOpts -> FilePath
databaseConfigFile :: FilePath
  , HetcatsOpts -> FilePath
databaseSubConfigKey :: String
  , HetcatsOpts -> FilePath
databaseFileVersionId :: String
  , HetcatsOpts -> Bool
databaseReanalyze :: Bool
  , HetcatsOpts -> DBConfig
databaseConfig :: DBConfig.DBConfig
  , HetcatsOpts -> DBContext
databaseContext :: DBConfig.DBContext
  , HetcatsOpts -> FilePath
xupdate :: FilePath
  , HetcatsOpts -> Bool
recurse :: Bool
  , HetcatsOpts -> Int
verbose :: Int
  , HetcatsOpts -> FilePath
defLogic :: String
  , HetcatsOpts -> FilePath
defSyntax :: String
  , HetcatsOpts -> Bool
outputToStdout :: Bool    -- ^ send messages to stdout?
  , HetcatsOpts -> [CASLAmalgOpt]
caslAmalg :: [CASLAmalgOpt]
  , HetcatsOpts -> Bool
interactive :: Bool
  , HetcatsOpts -> Int
connectP :: Int
  , HetcatsOpts -> FilePath
connectH :: String
  , HetcatsOpts -> Bool
uncolored :: Bool
  , HetcatsOpts -> Bool
xmlFlag :: Bool
  , HetcatsOpts -> Bool
applyAutomatic :: Bool
  , HetcatsOpts -> Bool
computeNormalForm :: Bool
  , HetcatsOpts -> [FilePath]
dumpOpts :: [String]
  , HetcatsOpts -> Bool
disableCertificateVerification :: Bool
  , HetcatsOpts -> Enc
ioEncoding :: Enc
    -- | use the library name in positions to avoid differences after uploads
  , HetcatsOpts -> Bool
useLibPos :: Bool
  , HetcatsOpts -> Bool
unlit :: Bool
  , HetcatsOpts -> Bool
serve :: Bool
  , HetcatsOpts -> Int
listen :: Int
  , HetcatsOpts -> FilePath
pidFile :: FilePath
  , HetcatsOpts -> [[FilePath]]
whitelist :: [[String]]
  , HetcatsOpts -> [[FilePath]]
blacklist :: [[String]]
  , HetcatsOpts -> Bool
runMMT :: Bool
  , HetcatsOpts -> Bool
fullTheories :: Bool
  , HetcatsOpts -> Bool
outputLogicList :: Bool
  , HetcatsOpts -> Bool
outputLogicGraph :: Bool
  , HetcatsOpts -> Bool
fileType :: Bool
  , HetcatsOpts -> FilePath
accessToken :: String
  , HetcatsOpts -> [FilePath]
httpRequestHeaders :: [String]
  , HetcatsOpts -> Bool
fullSign :: Bool
  , HetcatsOpts -> Bool
printAST :: Bool }

{- | 'defaultHetcatsOpts' defines the default HetcatsOpts, which are used as
basic values when the user specifies nothing else -}
defaultHetcatsOpts :: HetcatsOpts
defaultHetcatsOpts :: HetcatsOpts
defaultHetcatsOpts = HcOpt :: AnaType
-> GuiType
-> [(FilePath, FilePath)]
-> [FilePath]
-> [SIMPLE_ID]
-> [SIMPLE_ID]
-> Bool
-> [SIMPLE_ID]
-> InType
-> [FilePath]
-> FilePath
-> Int
-> FilePath
-> [OutType]
-> Bool
-> FilePath
-> FilePath
-> FilePath
-> FilePath
-> Bool
-> DBConfig
-> DBContext
-> FilePath
-> Bool
-> Int
-> FilePath
-> FilePath
-> Bool
-> [CASLAmalgOpt]
-> Bool
-> Int
-> FilePath
-> Bool
-> Bool
-> Bool
-> Bool
-> [FilePath]
-> Bool
-> Enc
-> Bool
-> Bool
-> Bool
-> Int
-> FilePath
-> [[FilePath]]
-> [[FilePath]]
-> Bool
-> Bool
-> Bool
-> Bool
-> Bool
-> FilePath
-> [FilePath]
-> Bool
-> Bool
-> HetcatsOpts
HcOpt
  { analysis :: AnaType
analysis = AnaType
Basic
  , guiType :: GuiType
guiType = GuiType
NoGui
  , urlCatalog :: [(FilePath, FilePath)]
urlCatalog = []
  , infiles :: [FilePath]
infiles = []
  , specNames :: [SIMPLE_ID]
specNames = []
  , transNames :: [SIMPLE_ID]
transNames = []
  , lossyTrans :: Bool
lossyTrans = Bool
False  
  , viewNames :: [SIMPLE_ID]
viewNames = []
  , intype :: InType
intype = InType
GuessIn
  , libdirs :: [FilePath]
libdirs = []
  , modelSparQ :: FilePath
modelSparQ = ""
  , counterSparQ :: Int
counterSparQ = 3
  , outdir :: FilePath
outdir = ""
  , outtypes :: [OutType]
outtypes = [] -- no default
  , databaseDoMigrate :: Bool
databaseDoMigrate = Bool
True
  , databaseOutputFile :: FilePath
databaseOutputFile = ""
  , databaseConfigFile :: FilePath
databaseConfigFile = ""
  , databaseSubConfigKey :: FilePath
databaseSubConfigKey = ""
  , databaseFileVersionId :: FilePath
databaseFileVersionId = ""
  , databaseReanalyze :: Bool
databaseReanalyze = Bool
False
  , databaseConfig :: DBConfig
databaseConfig = DBConfig
DBConfig.emptyDBConfig
  , databaseContext :: DBContext
databaseContext = DBContext
DBConfig.emptyDBContext
  , xupdate :: FilePath
xupdate = ""
  , recurse :: Bool
recurse = Bool
False
  , defLogic :: FilePath
defLogic = "CASL"
  , defSyntax :: FilePath
defSyntax = ""
  , verbose :: Int
verbose = 1
  , outputToStdout :: Bool
outputToStdout = Bool
True
  , caslAmalg :: [CASLAmalgOpt]
caslAmalg = [CASLAmalgOpt
Cell]
  , interactive :: Bool
interactive = Bool
False
  , connectP :: Int
connectP = -1
  , connectH :: FilePath
connectH = ""
  , uncolored :: Bool
uncolored = Bool
False
  , xmlFlag :: Bool
xmlFlag = Bool
False
  , applyAutomatic :: Bool
applyAutomatic = Bool
False
  , computeNormalForm :: Bool
computeNormalForm = Bool
False
  , dumpOpts :: [FilePath]
dumpOpts = []
  , disableCertificateVerification :: Bool
disableCertificateVerification = Bool
False
  , ioEncoding :: Enc
ioEncoding = Enc
Utf8
  , useLibPos :: Bool
useLibPos = Bool
False
  , unlit :: Bool
unlit = Bool
False
  , serve :: Bool
serve = Bool
False
  , listen :: Int
listen = -1
  , pidFile :: FilePath
pidFile = ""
  , whitelist :: [[FilePath]]
whitelist = []
  , blacklist :: [[FilePath]]
blacklist = []
  , runMMT :: Bool
runMMT = Bool
False
  , fullTheories :: Bool
fullTheories = Bool
False
  , outputLogicList :: Bool
outputLogicList = Bool
False
  , outputLogicGraph :: Bool
outputLogicGraph = Bool
False
  , fileType :: Bool
fileType = Bool
False
  , accessToken :: FilePath
accessToken = ""
  , httpRequestHeaders :: [FilePath]
httpRequestHeaders = []
  , fullSign :: Bool
fullSign = Bool
False
  , printAST :: Bool
printAST = Bool
False }

instance Show HetcatsOpts where
  show :: HetcatsOpts -> FilePath
show opts :: HetcatsOpts
opts =
    let showFlag :: (HetcatsOpts -> Bool) -> FilePath -> FilePath
showFlag p :: HetcatsOpts -> Bool
p o :: FilePath
o = if HetcatsOpts -> Bool
p HetcatsOpts
opts then FilePath -> FilePath
showOpt FilePath
o else ""
        showIPLists :: (HetcatsOpts -> [[FilePath]]) -> FilePath -> FilePath
showIPLists p :: HetcatsOpts -> [[FilePath]]
p s :: FilePath
s = let ll :: [[FilePath]]
ll = HetcatsOpts -> [[FilePath]]
p HetcatsOpts
opts in if [[FilePath]] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[FilePath]]
ll then "" else
          FilePath -> FilePath -> FilePath
showEqOpt FilePath
s (FilePath -> FilePath)
-> ([FilePath] -> FilePath) -> [FilePath] -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate "," ([FilePath] -> FilePath) -> [FilePath] -> FilePath
forall a b. (a -> b) -> a -> b
$ ([FilePath] -> FilePath) -> [[FilePath]] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate ".") [[FilePath]]
ll
    in
    FilePath -> FilePath -> FilePath
showEqOpt FilePath
verboseS (Int -> FilePath
forall a. Show a => a -> FilePath
show (Int -> FilePath) -> Int -> FilePath
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> Int
verbose HetcatsOpts
opts)
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ GuiType -> FilePath
forall a. Show a => a -> FilePath
show (HetcatsOpts -> GuiType
guiType HetcatsOpts
opts)
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (HetcatsOpts -> Bool) -> FilePath -> FilePath
showFlag HetcatsOpts -> Bool
outputLogicList FilePath
logicListS
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (HetcatsOpts -> Bool) -> FilePath -> FilePath
showFlag HetcatsOpts -> Bool
outputLogicGraph FilePath
logicGraphS
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (HetcatsOpts -> Bool) -> FilePath -> FilePath
showFlag HetcatsOpts -> Bool
fileType FilePath
fileTypeS
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (HetcatsOpts -> Bool) -> FilePath -> FilePath
showFlag HetcatsOpts -> Bool
interactive FilePath
interactiveS
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ AnaType -> FilePath
forall a. Show a => a -> FilePath
show (HetcatsOpts -> AnaType
analysis HetcatsOpts
opts)
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ case HetcatsOpts -> FilePath
defLogic HetcatsOpts
opts of
          s :: FilePath
s | FilePath
s FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
/= HetcatsOpts -> FilePath
defLogic HetcatsOpts
defaultHetcatsOpts -> FilePath -> FilePath -> FilePath
showEqOpt FilePath
logicS FilePath
s
          _ -> ""
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ case HetcatsOpts -> FilePath
defSyntax HetcatsOpts
opts of
          s :: FilePath
s | FilePath
s FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
/= HetcatsOpts -> FilePath
defSyntax HetcatsOpts
defaultHetcatsOpts -> FilePath -> FilePath -> FilePath
showEqOpt FilePath
serializationS FilePath
s
          _ -> ""
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ case HetcatsOpts -> [FilePath]
httpRequestHeaders HetcatsOpts
opts of
          [] -> ""
          headers :: [FilePath]
headers -> (FilePath -> FilePath) -> [FilePath] -> FilePath
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (FilePath -> FilePath -> FilePath
showEqOpt FilePath
httpRequestHeaderS (FilePath -> FilePath)
-> (FilePath -> FilePath) -> FilePath -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> FilePath
forall a. Show a => a -> FilePath
show) [FilePath]
headers
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ case HetcatsOpts -> FilePath
accessToken HetcatsOpts
opts of
          "" -> ""
          t :: FilePath
t -> FilePath -> FilePath -> FilePath
showEqOpt FilePath
accessTokenS FilePath
t
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath -> FilePath
showEqOpt FilePath
libdirsS (FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate ":" ([FilePath] -> FilePath) -> [FilePath] -> FilePath
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> [FilePath]
libdirs HetcatsOpts
opts)
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ case HetcatsOpts -> FilePath
modelSparQ HetcatsOpts
opts of
          "" -> ""
          f :: FilePath
f -> FilePath -> FilePath -> FilePath
showEqOpt FilePath
modelSparQS FilePath
f
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ case HetcatsOpts -> Int
counterSparQ HetcatsOpts
opts of
          n :: Int
n | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= HetcatsOpts -> Int
counterSparQ HetcatsOpts
defaultHetcatsOpts
              -> FilePath -> FilePath -> FilePath
showEqOpt FilePath
counterSparQS (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ Int -> FilePath
forall a. Show a => a -> FilePath
show Int
n
          _ -> ""
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (HetcatsOpts -> Bool) -> FilePath -> FilePath
showFlag HetcatsOpts -> Bool
xmlFlag FilePath
xmlS
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (HetcatsOpts -> Bool) -> FilePath -> FilePath
showFlag ((Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= -1) (Int -> Bool) -> (HetcatsOpts -> Int) -> HetcatsOpts -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HetcatsOpts -> Int
connectP) FilePath
connectS
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (HetcatsOpts -> Bool) -> FilePath -> FilePath
showFlag ((Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= -1) (Int -> Bool) -> (HetcatsOpts -> Int) -> HetcatsOpts -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HetcatsOpts -> Int
listen) FilePath
listenS
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath -> FilePath
showEqOpt FilePath
pidFileS (HetcatsOpts -> FilePath
pidFile HetcatsOpts
opts)
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (HetcatsOpts -> [[FilePath]]) -> FilePath -> FilePath
showIPLists HetcatsOpts -> [[FilePath]]
whitelist FilePath
whitelistS
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (HetcatsOpts -> [[FilePath]]) -> FilePath -> FilePath
showIPLists HetcatsOpts -> [[FilePath]]
blacklist FilePath
blacklistS
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (FilePath -> FilePath) -> [FilePath] -> FilePath
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (FilePath -> FilePath -> FilePath
showEqOpt "dump") (HetcatsOpts -> [FilePath]
dumpOpts HetcatsOpts
opts)
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath -> FilePath
showEqOpt "encoding" ((Char -> Char) -> FilePath -> FilePath
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ Enc -> FilePath
forall a. Show a => a -> FilePath
show (Enc -> FilePath) -> Enc -> FilePath
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> Enc
ioEncoding HetcatsOpts
opts)
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (HetcatsOpts -> Bool) -> FilePath -> FilePath
showFlag HetcatsOpts -> Bool
unlit FilePath
unlitS
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (HetcatsOpts -> Bool) -> FilePath -> FilePath
showFlag HetcatsOpts -> Bool
useLibPos FilePath
relposS
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (HetcatsOpts -> Bool) -> FilePath -> FilePath
showFlag HetcatsOpts -> Bool
fullSign FilePath
fullSignS
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (HetcatsOpts -> Bool) -> FilePath -> FilePath
showFlag HetcatsOpts -> Bool
printAST FilePath
printASTS
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (HetcatsOpts -> Bool) -> FilePath -> FilePath
showFlag HetcatsOpts -> Bool
fullTheories FilePath
fullTheoriesS
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ case HetcatsOpts -> [(FilePath, FilePath)]
urlCatalog HetcatsOpts
opts of
         [] -> ""
         cs :: [(FilePath, FilePath)]
cs -> FilePath -> FilePath -> FilePath
showEqOpt FilePath
urlCatalogS (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate ","
           ([FilePath] -> FilePath) -> [FilePath] -> FilePath
forall a b. (a -> b) -> a -> b
$ ((FilePath, FilePath) -> FilePath)
-> [(FilePath, FilePath)] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (\ (a :: FilePath
a, b :: FilePath
b) -> FilePath
a FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ '=' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: FilePath
b) [(FilePath, FilePath)]
cs
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath -> FilePath
showEqOpt FilePath
intypeS (InType -> FilePath
forall a. Show a => a -> FilePath
show (InType -> FilePath) -> InType -> FilePath
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> InType
intype HetcatsOpts
opts)
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath -> FilePath
showEqOpt FilePath
outdirS (HetcatsOpts -> FilePath
outdir HetcatsOpts
opts)
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath -> FilePath
showEqOpt FilePath
outtypesS (FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate "," ([FilePath] -> FilePath) -> [FilePath] -> FilePath
forall a b. (a -> b) -> a -> b
$ (OutType -> FilePath) -> [OutType] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map OutType -> FilePath
forall a. Show a => a -> FilePath
show ([OutType] -> [FilePath]) -> [OutType] -> [FilePath]
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> [OutType]
outtypes HetcatsOpts
opts)
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (HetcatsOpts -> Bool) -> FilePath -> FilePath
showFlag HetcatsOpts -> Bool
recurse FilePath
recursiveS
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (HetcatsOpts -> Bool) -> FilePath -> FilePath
showFlag HetcatsOpts -> Bool
applyAutomatic FilePath
applyAutomaticRuleS
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (HetcatsOpts -> Bool) -> FilePath -> FilePath
showFlag HetcatsOpts -> Bool
computeNormalForm FilePath
normalFormS
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath -> FilePath
showEqOpt FilePath
namedSpecsS (FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate "," ([FilePath] -> FilePath) -> [FilePath] -> FilePath
forall a b. (a -> b) -> a -> b
$ (SIMPLE_ID -> FilePath) -> [SIMPLE_ID] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map SIMPLE_ID -> FilePath
forall a. Show a => a -> FilePath
show ([SIMPLE_ID] -> [FilePath]) -> [SIMPLE_ID] -> [FilePath]
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> [SIMPLE_ID]
specNames HetcatsOpts
opts)
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath -> FilePath
showEqOpt FilePath
transS (FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate ":" ([FilePath] -> FilePath) -> [FilePath] -> FilePath
forall a b. (a -> b) -> a -> b
$ (SIMPLE_ID -> FilePath) -> [SIMPLE_ID] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map SIMPLE_ID -> FilePath
forall a. Show a => a -> FilePath
show ([SIMPLE_ID] -> [FilePath]) -> [SIMPLE_ID] -> [FilePath]
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> [SIMPLE_ID]
transNames HetcatsOpts
opts)
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (HetcatsOpts -> Bool) -> FilePath -> FilePath
showFlag HetcatsOpts -> Bool
lossyTrans FilePath
lossyTransS
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath -> FilePath
showEqOpt FilePath
viewS (FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate "," ([FilePath] -> FilePath) -> [FilePath] -> FilePath
forall a b. (a -> b) -> a -> b
$ (SIMPLE_ID -> FilePath) -> [SIMPLE_ID] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map SIMPLE_ID -> FilePath
forall a. Show a => a -> FilePath
show ([SIMPLE_ID] -> [FilePath]) -> [SIMPLE_ID] -> [FilePath]
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> [SIMPLE_ID]
viewNames HetcatsOpts
opts)
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath -> FilePath
showEqOpt FilePath
amalgS (FilePath -> FilePath
forall a. [a] -> [a]
tail (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath
forall a. [a] -> [a]
init (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ [CASLAmalgOpt] -> FilePath
forall a. Show a => a -> FilePath
show ([CASLAmalgOpt] -> FilePath) -> [CASLAmalgOpt] -> FilePath
forall a b. (a -> b) -> a -> b
$
                                      case HetcatsOpts -> [CASLAmalgOpt]
caslAmalg HetcatsOpts
opts of
                                      [] -> [CASLAmalgOpt
NoAnalysis]
                                      l :: [CASLAmalgOpt]
l -> [CASLAmalgOpt]
l)
    FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
unwords (HetcatsOpts -> [FilePath]
infiles HetcatsOpts
opts)

-- | every 'Flag' describes an option (see usage info)
data Flag =
    Verbose Int
  | Quiet
  | Uncolored
  | Version
  | VersionNumeric
  | Recurse
  | ApplyAutomatic
  | NormalForm
  | Help
  | Gui GuiType
  | Analysis AnaType
  | DefaultLogic String
  | DefaultSyntax String
  | InType InType
  | LibDirs String
  | OutDir FilePath
  | XUpdate FilePath
  | ModelSparQ FilePath
  | CounterSparQ Int
  | OutTypes [OutType]
  | DatabaseDoNotMigrate
  | DatabaseOutputFile FilePath
  | DatabaseConfigFile FilePath
  | DatabaseSubConfigKey String
  | DatabaseFileVersionId String
  | DatabaseReanalyze
  | Specs [SIMPLE_ID]
  | Trans [SIMPLE_ID]
  | LossyTrans   
  | Views [SIMPLE_ID]
  | CASLAmalg [CASLAmalgOpt]
  | Interactive
  | Connect Int String
  | XML
  | Dump String
  | DisableCertificateVerification
  | IOEncoding Enc
  | Unlit
  | RelPos
  | Serve
  | Listen Int
  | PidFile FilePath
  | Whitelist String
  | Blacklist String
  | UseMMT
  | FullTheories
  | FullSign
  | PrintAST
  | OutputLogicList
  | OutputLogicGraph
  | FileType
  | AccessToken String
  | HttpRequestHeader String
  | UrlCatalog [(String, String)] deriving Int -> Flag -> FilePath -> FilePath
[Flag] -> FilePath -> FilePath
Flag -> FilePath
(Int -> Flag -> FilePath -> FilePath)
-> (Flag -> FilePath)
-> ([Flag] -> FilePath -> FilePath)
-> Show Flag
forall a.
(Int -> a -> FilePath -> FilePath)
-> (a -> FilePath) -> ([a] -> FilePath -> FilePath) -> Show a
showList :: [Flag] -> FilePath -> FilePath
$cshowList :: [Flag] -> FilePath -> FilePath
show :: Flag -> FilePath
$cshow :: Flag -> FilePath
showsPrec :: Int -> Flag -> FilePath -> FilePath
$cshowsPrec :: Int -> Flag -> FilePath -> FilePath
Show

-- | 'makeOpts' includes a parsed Flag in a set of HetcatsOpts
makeOpts :: HetcatsOpts -> Flag -> HetcatsOpts
makeOpts :: HetcatsOpts -> Flag -> HetcatsOpts
makeOpts opts :: HetcatsOpts
opts flg :: Flag
flg =
  let splitIPs :: FilePath -> [[FilePath]]
splitIPs = (FilePath -> [FilePath]) -> [FilePath] -> [[FilePath]]
forall a b. (a -> b) -> [a] -> [b]
map (Char -> FilePath -> [FilePath]
forall a. Eq a => a -> [a] -> [[a]]
splitBy '.') ([FilePath] -> [[FilePath]])
-> (FilePath -> [FilePath]) -> FilePath -> [[FilePath]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> FilePath -> [FilePath]
forall a. Eq a => a -> [a] -> [[a]]
splitOn ','
  in case Flag
flg of
    Interactive -> HetcatsOpts
opts { interactive :: Bool
interactive = Bool
True }
    XML -> HetcatsOpts
opts { xmlFlag :: Bool
xmlFlag = Bool
True }
    Listen x :: Int
x -> HetcatsOpts
opts { listen :: Int
listen = Int
x }
    PidFile x :: FilePath
x -> HetcatsOpts
opts { pidFile :: FilePath
pidFile = FilePath
x }
    Blacklist x :: FilePath
x -> HetcatsOpts
opts { blacklist :: [[FilePath]]
blacklist = FilePath -> [[FilePath]]
splitIPs FilePath
x }
    Whitelist x :: FilePath
x -> HetcatsOpts
opts { whitelist :: [[FilePath]]
whitelist = FilePath -> [[FilePath]]
splitIPs FilePath
x }
    Connect x :: Int
x y :: FilePath
y -> HetcatsOpts
opts { connectP :: Int
connectP = Int
x, connectH :: FilePath
connectH = FilePath
y }
    Analysis x :: AnaType
x -> HetcatsOpts
opts { analysis :: AnaType
analysis = AnaType
x }
    Gui x :: GuiType
x -> HetcatsOpts
opts { guiType :: GuiType
guiType = GuiType
x }
    InType x :: InType
x -> HetcatsOpts
opts { intype :: InType
intype = InType
x }
    LibDirs x :: FilePath
x -> HetcatsOpts
opts { libdirs :: [FilePath]
libdirs = [FilePath] -> [FilePath]
joinHttpLibPath ([FilePath] -> [FilePath]) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> a -> b
$ FilePath -> [FilePath]
splitPaths FilePath
x }
    ModelSparQ x :: FilePath
x -> HetcatsOpts
opts { modelSparQ :: FilePath
modelSparQ = FilePath
x }
    CounterSparQ x :: Int
x -> HetcatsOpts
opts { counterSparQ :: Int
counterSparQ = Int
x }
    OutDir x :: FilePath
x -> HetcatsOpts
opts { outdir :: FilePath
outdir = FilePath
x }
    OutTypes x :: [OutType]
x -> HetcatsOpts
opts { outtypes :: [OutType]
outtypes = [OutType]
x }
    DatabaseDoNotMigrate -> HetcatsOpts
opts { databaseDoMigrate :: Bool
databaseDoMigrate = Bool
False }
    DatabaseOutputFile x :: FilePath
x -> HetcatsOpts
opts { databaseOutputFile :: FilePath
databaseOutputFile = FilePath
x }
    DatabaseConfigFile x :: FilePath
x -> HetcatsOpts
opts { databaseConfigFile :: FilePath
databaseConfigFile = FilePath
x }
    DatabaseSubConfigKey x :: FilePath
x -> HetcatsOpts
opts { databaseSubConfigKey :: FilePath
databaseSubConfigKey = FilePath
x }
    DatabaseFileVersionId x :: FilePath
x -> HetcatsOpts
opts { databaseFileVersionId :: FilePath
databaseFileVersionId = FilePath
x }
    DatabaseReanalyze -> HetcatsOpts
opts { databaseReanalyze :: Bool
databaseReanalyze = Bool
True }
    XUpdate x :: FilePath
x -> HetcatsOpts
opts { xupdate :: FilePath
xupdate = FilePath
x }
    Recurse -> HetcatsOpts
opts { recurse :: Bool
recurse = Bool
True }
    ApplyAutomatic -> HetcatsOpts
opts { applyAutomatic :: Bool
applyAutomatic = Bool
True }
    NormalForm -> HetcatsOpts
opts { computeNormalForm :: Bool
computeNormalForm = Bool
True }
    Specs x :: [SIMPLE_ID]
x -> HetcatsOpts
opts { specNames :: [SIMPLE_ID]
specNames = [SIMPLE_ID]
x }
    Trans x :: [SIMPLE_ID]
x -> HetcatsOpts
opts { transNames :: [SIMPLE_ID]
transNames = [SIMPLE_ID]
x }
    LossyTrans -> HetcatsOpts
opts { lossyTrans :: Bool
lossyTrans = Bool
True }
    Views x :: [SIMPLE_ID]
x -> HetcatsOpts
opts { viewNames :: [SIMPLE_ID]
viewNames = [SIMPLE_ID]
x }
    Verbose x :: Int
x -> HetcatsOpts
opts { verbose :: Int
verbose = Int
x }
    DefaultLogic x :: FilePath
x -> HetcatsOpts
opts { defLogic :: FilePath
defLogic = FilePath
x }
    DefaultSyntax x :: FilePath
x -> HetcatsOpts
opts { defSyntax :: FilePath
defSyntax = FilePath
x }
    CASLAmalg x :: [CASLAmalgOpt]
x -> HetcatsOpts
opts { caslAmalg :: [CASLAmalgOpt]
caslAmalg = [CASLAmalgOpt]
x }
    Quiet -> HetcatsOpts
opts { verbose :: Int
verbose = 0 }
    Uncolored -> HetcatsOpts
opts { uncolored :: Bool
uncolored = Bool
True }
    Dump s :: FilePath
s -> HetcatsOpts
opts { dumpOpts :: [FilePath]
dumpOpts = FilePath
s FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: HetcatsOpts -> [FilePath]
dumpOpts HetcatsOpts
opts }
    DisableCertificateVerification ->
      HetcatsOpts
opts { disableCertificateVerification :: Bool
disableCertificateVerification = Bool
True }
    IOEncoding e :: Enc
e -> HetcatsOpts
opts { ioEncoding :: Enc
ioEncoding = Enc
e }
    Serve -> HetcatsOpts
opts { serve :: Bool
serve = Bool
True }
    Unlit -> HetcatsOpts
opts { unlit :: Bool
unlit = Bool
True }
    RelPos -> HetcatsOpts
opts { useLibPos :: Bool
useLibPos = Bool
True }
    UseMMT -> HetcatsOpts
opts { runMMT :: Bool
runMMT = Bool
True }
    FullTheories -> HetcatsOpts
opts { fullTheories :: Bool
fullTheories = Bool
True }
    OutputLogicList -> HetcatsOpts
opts { outputLogicList :: Bool
outputLogicList = Bool
True }
    OutputLogicGraph -> HetcatsOpts
opts { outputLogicGraph :: Bool
outputLogicGraph = Bool
True }
    FileType -> HetcatsOpts
opts { fileType :: Bool
fileType = Bool
True }
    FullSign -> HetcatsOpts
opts { fullSign :: Bool
fullSign = Bool
True }
    PrintAST -> HetcatsOpts
opts { printAST :: Bool
printAST = Bool
True }
    UrlCatalog m :: [(FilePath, FilePath)]
m -> HetcatsOpts
opts { urlCatalog :: [(FilePath, FilePath)]
urlCatalog = [(FilePath, FilePath)]
m [(FilePath, FilePath)]
-> [(FilePath, FilePath)] -> [(FilePath, FilePath)]
forall a. [a] -> [a] -> [a]
++ HetcatsOpts -> [(FilePath, FilePath)]
urlCatalog HetcatsOpts
opts }
    AccessToken s :: FilePath
s -> HetcatsOpts
opts { accessToken :: FilePath
accessToken = FilePath
s }
    HttpRequestHeader header :: FilePath
header -> HetcatsOpts
opts { httpRequestHeaders :: [FilePath]
httpRequestHeaders = FilePath
header FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: HetcatsOpts -> [FilePath]
httpRequestHeaders HetcatsOpts
opts }
    Help -> HetcatsOpts
opts -- skipped
    Version -> HetcatsOpts
opts -- skipped
    VersionNumeric -> HetcatsOpts
opts -- skipped

-- | 'AnaType' describes the type of analysis to be performed
data AnaType = Basic | Structured | Skip

instance Show AnaType where
  show :: AnaType -> FilePath
show a :: AnaType
a = case AnaType
a of
    Basic -> ""
    Structured -> FilePath -> FilePath
showOpt FilePath
justStructuredS
    Skip -> FilePath -> FilePath
showOpt FilePath
skipS

-- | check if structured analysis should be performed
isStructured :: HetcatsOpts -> Bool
isStructured :: HetcatsOpts -> Bool
isStructured a :: HetcatsOpts
a = case HetcatsOpts -> AnaType
analysis HetcatsOpts
a of
    Structured -> Bool
True
    _ -> Bool
False

-- | 'GuiType' determines if we want the GUI shown
data GuiType = UseGui | NoGui
  deriving GuiType -> GuiType -> Bool
(GuiType -> GuiType -> Bool)
-> (GuiType -> GuiType -> Bool) -> Eq GuiType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: GuiType -> GuiType -> Bool
$c/= :: GuiType -> GuiType -> Bool
== :: GuiType -> GuiType -> Bool
$c== :: GuiType -> GuiType -> Bool
Eq

instance Show GuiType where
  show :: GuiType -> FilePath
show g :: GuiType
g = case GuiType
g of
    UseGui -> FilePath -> FilePath
showOpt FilePath
guiS
    NoGui -> ""

-- | 'InType' describes the type of input the infile contains
data InType =
    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" ('True' is long version)
  | DgXml
  | Xmi
  | Qvt
  | TPTPIn
  | HtmlIn -- just to complain
  deriving InType -> InType -> Bool
(InType -> InType -> Bool)
-> (InType -> InType -> Bool) -> Eq InType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: InType -> InType -> Bool
$c/= :: InType -> InType -> Bool
== :: InType -> InType -> Bool
$c== :: InType -> InType -> Bool
Eq

instance Show InType where
  show :: InType -> FilePath
show i :: InType
i = case InType
i of
    ATermIn at :: ATType
at -> FilePath
genTermS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ATType -> FilePath
forall a. Show a => a -> FilePath
show ATType
at
    CASLIn -> "casl"
    HetCASLIn -> "het"
    DOLIn -> "dol"
    OWLIn oty :: OWLFormat
oty -> OWLFormat -> FilePath
forall a. Show a => a -> FilePath
show OWLFormat
oty
    HaskellIn -> FilePath
hsS
    ExperimentalIn -> "exp"
    MaudeIn -> "maude"
    TwelfIn -> "elf"
    HolLightIn -> "hol"
    IsaIn -> "isa"
    ThyIn -> "thy"
    TPTPIn -> "tptp"
    PrfIn -> FilePath
prfS
    OmdocIn -> FilePath
omdocS
    ProofCommand -> "hpf"
    GuessIn -> ""
    RDFIn -> "rdf"
    FreeCADIn -> "fcstd"
    CommonLogicIn isLong :: Bool
isLong -> if Bool
isLong then "clif" else "clf"
    DgXml -> FilePath
xmlS
    Xmi -> "xmi"
    Qvt -> "qvt"
    HtmlIn -> "html"

-- maybe this optional tree prefix can be omitted
instance Read InType where
    readsPrec :: Int -> ReadS InType
readsPrec _ = [(FilePath, InType)] -> ReadS InType
forall a. [(FilePath, a)] -> ReadS a
readShowAux ([(FilePath, InType)] -> ReadS InType)
-> [(FilePath, InType)] -> ReadS InType
forall a b. (a -> b) -> a -> b
$ (InType -> [(FilePath, InType)])
-> [InType] -> [(FilePath, InType)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap InType -> [(FilePath, InType)]
showAll ([InType]
plainInTypes [InType] -> [InType] -> [InType]
forall a. [a] -> [a] -> [a]
++ [InType]
aInTypes)
      where showAll :: InType -> [(FilePath, InType)]
showAll i :: InType
i@(ATermIn _) = [(InType -> FilePath
forall a. Show a => a -> FilePath
show InType
i, InType
i), (FilePath
treeS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ InType -> FilePath
forall a. Show a => a -> FilePath
show InType
i, InType
i)]
            showAll i :: InType
i = [(InType -> FilePath
forall a. Show a => a -> FilePath
show InType
i, InType
i)]

-- | 'ATType' describes distinct types of ATerms
data ATType = BAF | NonBAF deriving ATType -> ATType -> Bool
(ATType -> ATType -> Bool)
-> (ATType -> ATType -> Bool) -> Eq ATType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ATType -> ATType -> Bool
$c/= :: ATType -> ATType -> Bool
== :: ATType -> ATType -> Bool
$c== :: ATType -> ATType -> Bool
Eq

instance Show ATType where
  show :: ATType -> FilePath
show a :: ATType
a = case ATType
a of
    BAF -> FilePath
bafS
    NonBAF -> ""

-- RDFIn is on purpose not listed; must be added manually if neccessary
plainInTypes :: [InType]
plainInTypes :: [InType]
plainInTypes =
  [ InType
CASLIn, InType
HetCASLIn, InType
DOLIn ]
  [InType] -> [InType] -> [InType]
forall a. [a] -> [a] -> [a]
++ (OWLFormat -> InType) -> [OWLFormat] -> [InType]
forall a b. (a -> b) -> [a] -> [b]
map OWLFormat -> InType
OWLIn [OWLFormat]
plainOwlFormats [InType] -> [InType] -> [InType]
forall a. [a] -> [a] -> [a]
++
  [ InType
HaskellIn, InType
ExperimentalIn
  , InType
MaudeIn, InType
TwelfIn
  , InType
HolLightIn, InType
IsaIn, InType
ThyIn, InType
PrfIn, InType
OmdocIn, InType
ProofCommand
  , Bool -> InType
CommonLogicIn Bool
False, Bool -> InType
CommonLogicIn Bool
True
  , InType
DgXml, InType
FreeCADIn, InType
Xmi, InType
Qvt, InType
TPTPIn ]

aInTypes :: [InType]
aInTypes :: [InType]
aInTypes = [ ATType -> InType
ATermIn ATType
x | ATType
x <- [ATType
BAF, ATType
NonBAF] ]

-- | 'OWLFormat' lists possibilities for OWL syntax (in + out)
data OWLFormat =
    Manchester
  | Functional
  | OwlXml
  | RdfXml
  | OBO
  | Turtle
  deriving OWLFormat -> OWLFormat -> Bool
(OWLFormat -> OWLFormat -> Bool)
-> (OWLFormat -> OWLFormat -> Bool) -> Eq OWLFormat
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OWLFormat -> OWLFormat -> Bool
$c/= :: OWLFormat -> OWLFormat -> Bool
== :: OWLFormat -> OWLFormat -> Bool
$c== :: OWLFormat -> OWLFormat -> Bool
Eq

plainOwlFormats :: [OWLFormat]
plainOwlFormats :: [OWLFormat]
plainOwlFormats = [ OWLFormat
Manchester, OWLFormat
Functional, OWLFormat
OwlXml, OWLFormat
RdfXml, OWLFormat
OBO, OWLFormat
Turtle ]

instance Show OWLFormat where
  show :: OWLFormat -> FilePath
show ty :: OWLFormat
ty = case OWLFormat
ty of
    Manchester -> "omn"
    Functional -> "ofn"
    OwlXml -> "owl"
    -- "owl.xml" ?? might occur but conflicts with dgxml
    RdfXml -> "rdf"
    OBO -> "obo"
    Turtle -> "ttl"

data SPFType = ConsistencyCheck | ProveTheory deriving SPFType -> SPFType -> Bool
(SPFType -> SPFType -> Bool)
-> (SPFType -> SPFType -> Bool) -> Eq SPFType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SPFType -> SPFType -> Bool
$c/= :: SPFType -> SPFType -> Bool
== :: SPFType -> SPFType -> Bool
$c== :: SPFType -> SPFType -> Bool
Eq

instance Show SPFType where
  show :: SPFType -> FilePath
show x :: SPFType
x = case SPFType
x of
    ConsistencyCheck -> FilePath
cS
    ProveTheory -> ""

spfTypes :: [SPFType]
spfTypes :: [SPFType]
spfTypes = [SPFType
ConsistencyCheck, SPFType
ProveTheory]

-- | 'OutType' describes the type of outputs that we want to generate
data OutType =
    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
  deriving OutType -> OutType -> Bool
(OutType -> OutType -> Bool)
-> (OutType -> OutType -> Bool) -> Eq OutType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OutType -> OutType -> Bool
$c/= :: OutType -> OutType -> Bool
== :: OutType -> OutType -> Bool
$c== :: OutType -> OutType -> Bool
Eq

instance Show OutType where
  show :: OutType -> FilePath
show o :: OutType
o = case OutType
o of
    PrettyOut p :: PrettyType
p -> FilePath
ppS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ PrettyType -> FilePath
forall a. Show a => a -> FilePath
show PrettyType
p
    GraphOut f :: GraphType
f -> FilePath
graphE FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ GraphType -> FilePath
forall a. Show a => a -> FilePath
show GraphType
f
    Prf -> FilePath
prfS
    EnvOut -> FilePath
envS
    OWLOut oty :: OWLFormat
oty -> OWLFormat -> FilePath
forall a. Show a => a -> FilePath
show OWLFormat
oty
    CLIFOut -> "clif"
    KIFOut -> "kif"
    OmdocOut -> FilePath
omdocS
    XmlOut -> FilePath
xmlS
    DbOut -> FilePath
dbS
    JsonOut -> "json"
    ExperimentalOut -> FilePath
experimentalS
    HaskellOut -> FilePath
hsS
    FreeCADOut -> "fcxml"
    ThyFile -> "thy"
    DfgFile t :: SPFType
t -> FilePath
dfgS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ SPFType -> FilePath
forall a. Show a => a -> FilePath
show SPFType
t
    TPTPFile -> FilePath
tptpS
    ComptableXml -> "comptable.xml"
    MedusaJson -> "medusa.json"
    RDFOut -> "nt"
    SigFile d :: Delta
d -> "sig" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Delta -> FilePath
forall a. Show a => a -> FilePath
show Delta
d
    TheoryFile d :: Delta
d -> "th" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ Delta -> FilePath
forall a. Show a => a -> FilePath
show Delta
d
    SymXml -> "sym.xml"
    SymsXml -> "syms.xml"

plainOutTypeList :: [OutType]
plainOutTypeList :: [OutType]
plainOutTypeList =
  [ OutType
Prf, OutType
EnvOut ] [OutType] -> [OutType] -> [OutType]
forall a. [a] -> [a] -> [a]
++ (OWLFormat -> OutType) -> [OWLFormat] -> [OutType]
forall a b. (a -> b) -> [a] -> [b]
map OWLFormat -> OutType
OWLOut [OWLFormat]
plainOwlFormats [OutType] -> [OutType] -> [OutType]
forall a. [a] -> [a] -> [a]
++
  [ OutType
RDFOut, OutType
CLIFOut, OutType
KIFOut, OutType
OmdocOut, OutType
XmlOut, OutType
JsonOut, OutType
DbOut, OutType
ExperimentalOut
  , OutType
HaskellOut, OutType
ThyFile, OutType
ComptableXml, OutType
MedusaJson, OutType
FreeCADOut, OutType
SymXml, OutType
SymsXml
  , OutType
TPTPFile]

outTypeList :: [OutType]
outTypeList :: [OutType]
outTypeList = let dl :: [Delta]
dl = [Delta
Delta, Delta
Fully] in
    [OutType]
plainOutTypeList
    [OutType] -> [OutType] -> [OutType]
forall a. [a] -> [a] -> [a]
++ [ PrettyType -> OutType
PrettyOut PrettyType
p | PrettyType
p <- [PrettyType]
prettyList [PrettyType] -> [PrettyType] -> [PrettyType]
forall a. [a] -> [a] -> [a]
++ [PrettyType]
prettyList2]
    [OutType] -> [OutType] -> [OutType]
forall a. [a] -> [a] -> [a]
++ [ Delta -> OutType
SigFile Delta
d | Delta
d <- [Delta]
dl ]
    [OutType] -> [OutType] -> [OutType]
forall a. [a] -> [a] -> [a]
++ [ Delta -> OutType
TheoryFile Delta
d | Delta
d <- [Delta]
dl ]
    [OutType] -> [OutType] -> [OutType]
forall a. [a] -> [a] -> [a]
++ [ SPFType -> OutType
DfgFile SPFType
x | SPFType
x <- [SPFType]
spfTypes]
    [OutType] -> [OutType] -> [OutType]
forall a. [a] -> [a] -> [a]
++ [ GraphType -> OutType
GraphOut GraphType
f | GraphType
f <- [GraphType]
graphList ]

instance Read OutType where
    readsPrec :: Int -> ReadS OutType
readsPrec _ = [OutType] -> ReadS OutType
forall a. Show a => [a] -> ReadS a
readShow [OutType]
outTypeList

data Delta = Delta | Fully deriving Delta -> Delta -> Bool
(Delta -> Delta -> Bool) -> (Delta -> Delta -> Bool) -> Eq Delta
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Delta -> Delta -> Bool
$c/= :: Delta -> Delta -> Bool
== :: Delta -> Delta -> Bool
$c== :: Delta -> Delta -> Bool
Eq

instance Show Delta where
  show :: Delta -> FilePath
show d :: Delta
d = case Delta
d of
    Delta -> FilePath
deltaS
    Fully -> ""

{- | 'PrettyType' describes the type of output we want the pretty-printer
to generate -}
data PrettyType = PrettyAscii Bool | PrettyLatex Bool | PrettyXml | PrettyHtml
  deriving PrettyType -> PrettyType -> Bool
(PrettyType -> PrettyType -> Bool)
-> (PrettyType -> PrettyType -> Bool) -> Eq PrettyType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PrettyType -> PrettyType -> Bool
$c/= :: PrettyType -> PrettyType -> Bool
== :: PrettyType -> PrettyType -> Bool
$c== :: PrettyType -> PrettyType -> Bool
Eq

instance Show PrettyType where
  show :: PrettyType -> FilePath
show p :: PrettyType
p = case PrettyType
p of
    PrettyAscii b :: Bool
b -> (if Bool
b then "stripped." else "") FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "dol"
    PrettyLatex b :: Bool
b -> (if Bool
b then "labelled." else "") FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "tex"
    PrettyXml -> FilePath
xmlS
    PrettyHtml -> "html"

prettyList :: [PrettyType]
prettyList :: [PrettyType]
prettyList = [Bool -> PrettyType
PrettyAscii Bool
False, Bool -> PrettyType
PrettyLatex Bool
False, PrettyType
PrettyXml, PrettyType
PrettyHtml]

prettyList2 :: [PrettyType]
prettyList2 :: [PrettyType]
prettyList2 = [Bool -> PrettyType
PrettyAscii Bool
True, Bool -> PrettyType
PrettyLatex Bool
True]

-- | 'GraphType' describes the type of Graph that we want generated
data GraphType =
    Dot Bool -- ^ True means show internal node labels
  deriving GraphType -> GraphType -> Bool
(GraphType -> GraphType -> Bool)
-> (GraphType -> GraphType -> Bool) -> Eq GraphType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: GraphType -> GraphType -> Bool
$c/= :: GraphType -> GraphType -> Bool
== :: GraphType -> GraphType -> Bool
$c== :: GraphType -> GraphType -> Bool
Eq

instance Show GraphType where
  show :: GraphType -> FilePath
show g :: GraphType
g = case GraphType
g of
    Dot si :: Bool
si -> (if Bool
si then "exp." else "") FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "dot"

graphList :: [GraphType]
graphList :: [GraphType]
graphList = [Bool -> GraphType
Dot Bool
True, Bool -> GraphType
Dot Bool
False]

{- | 'options' describes all available options and is used to generate usage
information -}
options :: [OptDescr Flag]
options :: [OptDescr Flag]
options = let
    cslst :: FilePath
cslst = "is a comma-separated list"
       FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
crS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "of one or more from:"
    crS :: FilePath
crS = "\n  "
    bS :: FilePath
bS = "| "
    joinBar :: [FilePath] -> FilePath
joinBar l :: [FilePath]
l = "(" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate "|" [FilePath]
l FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ")" in
    [ FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "v" [FilePath
verboseS] ((Maybe FilePath -> Flag) -> FilePath -> ArgDescr Flag
forall a. (Maybe FilePath -> a) -> FilePath -> ArgDescr a
OptArg Maybe FilePath -> Flag
parseVerbosity "0-5")
      "verbosity, default is -v1"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "q" ["quiet"] (Flag -> ArgDescr Flag
forall a. a -> ArgDescr a
NoArg Flag
Quiet)
      "same as -v0, no output to stdout"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "V" ["version"] (Flag -> ArgDescr Flag
forall a. a -> ArgDescr a
NoArg Flag
Version)
      "print version information and exit"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "" ["numeric-version"] (Flag -> ArgDescr Flag
forall a. a -> ArgDescr a
NoArg Flag
VersionNumeric)
      "print version number and exit"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "h" ["help", "usage"] (Flag -> ArgDescr Flag
forall a. a -> ArgDescr a
NoArg Flag
Help)
      "print usage information and exit"
#ifdef UNI_PACKAGE
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "g" [FilePath
guiS] (Flag -> ArgDescr Flag
forall a. a -> ArgDescr a
NoArg (GuiType -> Flag
Gui GuiType
UseGui))
      "show graphs in windows"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "u" ["uncolored"] (Flag -> ArgDescr Flag
forall a. a -> ArgDescr a
NoArg Flag
Uncolored)
      "no colors in shown graphs"
#endif
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "x" [FilePath
xmlS] (Flag -> ArgDescr Flag
forall a. a -> ArgDescr a
NoArg Flag
XML)
       "use xml packets to communicate"
#ifdef SERVER
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "P" [FilePath
pidFileS] ((FilePath -> Flag) -> FilePath -> ArgDescr Flag
forall a. (FilePath -> a) -> FilePath -> ArgDescr a
ReqArg FilePath -> Flag
PidFile "FILEPATH")
       "path to put the PID file of the hets server (omit if no pidfile is desired)"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "X" ["server"] (Flag -> ArgDescr Flag
forall a. a -> ArgDescr a
NoArg Flag
Serve)
       "start hets as web-server"
#endif
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "z" [FilePath
logicListS] (Flag -> ArgDescr Flag
forall a. a -> ArgDescr a
NoArg Flag
OutputLogicList)
      "output logic list as plain text"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "G" [FilePath
logicGraphS] (Flag -> ArgDescr Flag
forall a. a -> ArgDescr a
NoArg Flag
OutputLogicGraph)
      "output logic graph (as xml) or as graph (-g)"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "I" [FilePath
interactiveS] (Flag -> ArgDescr Flag
forall a. a -> ArgDescr a
NoArg Flag
Interactive)
      "run in interactive (console) mode"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "F" [FilePath
fileTypeS] (Flag -> ArgDescr Flag
forall a. a -> ArgDescr a
NoArg Flag
FileType)
      "only display file type"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "p" [FilePath
skipS] (Flag -> ArgDescr Flag
forall a. a -> ArgDescr a
NoArg (Flag -> ArgDescr Flag) -> Flag -> ArgDescr Flag
forall a b. (a -> b) -> a -> b
$ AnaType -> Flag
Analysis AnaType
Skip)
      "skip static analysis, only parse"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "s" [FilePath
justStructuredS] (Flag -> ArgDescr Flag
forall a. a -> ArgDescr a
NoArg (Flag -> ArgDescr Flag) -> Flag -> ArgDescr Flag
forall a b. (a -> b) -> a -> b
$ AnaType -> Flag
Analysis AnaType
Structured)
      "skip basic, just do structured analysis"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "l" [FilePath
logicS] ((FilePath -> Flag) -> FilePath -> ArgDescr Flag
forall a. (FilePath -> a) -> FilePath -> ArgDescr a
ReqArg FilePath -> Flag
DefaultLogic "LOGIC")
      "choose logic, default is CASL"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "y" [FilePath
serializationS] ((FilePath -> Flag) -> FilePath -> ArgDescr Flag
forall a. (FilePath -> a) -> FilePath -> ArgDescr a
ReqArg FilePath -> Flag
DefaultSyntax "SER")
      "choose different logic syntax"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "L" [FilePath
libdirsS] ((FilePath -> Flag) -> FilePath -> ArgDescr Flag
forall a. (FilePath -> a) -> FilePath -> ArgDescr a
ReqArg FilePath -> Flag
LibDirs "DIR")
      ("colon-separated list of directories"
       FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
crS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "containing DOL libraries."
       FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
crS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "If an http[s] URL is specified here, it is treated as the last libdir because colons can occur in such URLs")
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "m" [FilePath
modelSparQS] ((FilePath -> Flag) -> FilePath -> ArgDescr Flag
forall a. (FilePath -> a) -> FilePath -> ArgDescr a
ReqArg FilePath -> Flag
ModelSparQ "FILE")
      "lisp file for SparQ definitions"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "" [FilePath
counterSparQS] ((FilePath -> Flag) -> FilePath -> ArgDescr Flag
forall a. (FilePath -> a) -> FilePath -> ArgDescr a
ReqArg FilePath -> Flag
parseCounter "0-99")
      "maximal number of counter examples"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "c" [FilePath
connectS] ((FilePath -> Flag) -> FilePath -> ArgDescr Flag
forall a. (FilePath -> a) -> FilePath -> ArgDescr a
ReqArg FilePath -> Flag
parseConnect "HOST:PORT")
      ("run (console) interface via connection"
       FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
crS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "to given host and port")
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "S" [FilePath
listenS] ((FilePath -> Flag) -> FilePath -> ArgDescr Flag
forall a. (FilePath -> a) -> FilePath -> ArgDescr a
ReqArg FilePath -> Flag
parseListen "PORT")
      "run interface/server by listening to the port"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "" [FilePath
whitelistS] ((FilePath -> Flag) -> FilePath -> ArgDescr Flag
forall a. (FilePath -> a) -> FilePath -> ArgDescr a
ReqArg FilePath -> Flag
Whitelist "IP4s")
      (FilePath -> OptDescr Flag) -> FilePath -> OptDescr Flag
forall a b. (a -> b) -> a -> b
$ "comma-separated list of IP4 addresses"
      FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
crS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "(missing numbers at dots are wildcards)"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "" [FilePath
blacklistS] ((FilePath -> Flag) -> FilePath -> ArgDescr Flag
forall a. (FilePath -> a) -> FilePath -> ArgDescr a
ReqArg FilePath -> Flag
Blacklist "IP4s")
      (FilePath -> OptDescr Flag) -> FilePath -> OptDescr Flag
forall a b. (a -> b) -> a -> b
$ "comma-separated list of IP4 addresses"
      FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
crS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "(example: 77.75.77.)"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "C" [FilePath
urlCatalogS] ((FilePath -> Flag) -> FilePath -> ArgDescr Flag
forall a. (FilePath -> a) -> FilePath -> ArgDescr a
ReqArg FilePath -> Flag
parseCatalog "URLS")
      "comma-separated list of URL pairs: srcURL=tarURL"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "i" [FilePath
intypeS] ((FilePath -> Flag) -> FilePath -> ArgDescr Flag
forall a. (FilePath -> a) -> FilePath -> ArgDescr a
ReqArg FilePath -> Flag
parseInType "ITYPE")
      ("input file type can be one of:" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
       (FilePath -> FilePath) -> [FilePath] -> FilePath
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ t :: FilePath
t -> FilePath
crS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
bS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
t)
       ((InType -> FilePath) -> [InType] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map InType -> FilePath
forall a. Show a => a -> FilePath
show [InType]
plainInTypes [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++
        (FilePath -> FilePath) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath
bracket FilePath
bafS) [FilePath -> FilePath
bracket FilePath
treeS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
genTermS]))
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "d" ["dump"] ((FilePath -> Flag) -> FilePath -> ArgDescr Flag
forall a. (FilePath -> a) -> FilePath -> ArgDescr a
ReqArg FilePath -> Flag
Dump "STRING")
      "dump various strings"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "" ["disable-certificate-verification"]
      (Flag -> ArgDescr Flag
forall a. a -> ArgDescr a
NoArg Flag
DisableCertificateVerification)
      "Disable TLS certificate verification"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "e" ["encoding"] ((FilePath -> Flag) -> FilePath -> ArgDescr Flag
forall a. (FilePath -> a) -> FilePath -> ArgDescr a
ReqArg FilePath -> Flag
parseEncoding "ENCODING")
      "latin1 or utf8 (default) encoding"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "" [FilePath
unlitS] (Flag -> ArgDescr Flag
forall a. a -> ArgDescr a
NoArg Flag
Unlit) "unlit input source"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "" [FilePath
relposS] (Flag -> ArgDescr Flag
forall a. a -> ArgDescr a
NoArg Flag
RelPos) "use relative file positions"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "" [FilePath
fullSignS] (Flag -> ArgDescr Flag
forall a. a -> ArgDescr a
NoArg Flag
FullSign) "xml output full signatures"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "" [FilePath
printASTS] (Flag -> ArgDescr Flag
forall a. a -> ArgDescr a
NoArg Flag
PrintAST) ("print AST in xml/json output")
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "" [FilePath
fullTheoriesS] (Flag -> ArgDescr Flag
forall a. a -> ArgDescr a
NoArg Flag
FullTheories) "xml output full theories"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "" [FilePath
accessTokenS] ((FilePath -> Flag) -> FilePath -> ArgDescr Flag
forall a. (FilePath -> a) -> FilePath -> ArgDescr a
ReqArg FilePath -> Flag
AccessToken "TOKEN")
      "add access token to URLs (for ontohub)"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "H" [FilePath
httpRequestHeaderS] ((FilePath -> Flag) -> FilePath -> ArgDescr Flag
forall a. (FilePath -> a) -> FilePath -> ArgDescr a
ReqArg FilePath -> Flag
HttpRequestHeader "HTTP_HEADER")
      ("additional headers to use for HTTP requests"
      FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
crS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "this option can be used multiple times")
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "O" [FilePath
outdirS] ((FilePath -> Flag) -> FilePath -> ArgDescr Flag
forall a. (FilePath -> a) -> FilePath -> ArgDescr a
ReqArg FilePath -> Flag
OutDir "DIR")
      "destination directory for output files"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "o" [FilePath
outtypesS] ((FilePath -> Flag) -> FilePath -> ArgDescr Flag
forall a. (FilePath -> a) -> FilePath -> ArgDescr a
ReqArg FilePath -> Flag
parseOutTypes "OTYPES")
      ("output file types, default nothing," FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
crS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
       FilePath
cslst FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
crS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ (OutType -> FilePath) -> [OutType] -> FilePath
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ( \ t :: OutType
t -> FilePath
bS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ OutType -> FilePath
forall a. Show a => a -> FilePath
show OutType
t FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
crS)
             [OutType]
plainOutTypeList
       FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
bS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
joinBar ((OutType -> FilePath) -> [OutType] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map OutType -> FilePath
forall a. Show a => a -> FilePath
show [Delta -> OutType
SigFile Delta
Fully,
                                   Delta -> OutType
TheoryFile Delta
Fully])
              FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath
bracket FilePath
deltaS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
crS
       FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
bS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
ppS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
joinBar ((PrettyType -> FilePath) -> [PrettyType] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map PrettyType -> FilePath
forall a. Show a => a -> FilePath
show [PrettyType]
prettyList) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
crS
       FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
bS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
ppS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
joinBar ((PrettyType -> FilePath) -> [PrettyType] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map PrettyType -> FilePath
forall a. Show a => a -> FilePath
show [PrettyType]
prettyList2) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
crS
       FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
bS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
graphE FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
joinBar ((GraphType -> FilePath) -> [GraphType] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map GraphType -> FilePath
forall a. Show a => a -> FilePath
show [GraphType]
graphList) FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
crS
       FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
bS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
dfgS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath
bracket FilePath
cS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
crS
       FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
bS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
tptpS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath -> FilePath
bracket FilePath
cS)
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "" ["database-do-not-migrate"] (Flag -> ArgDescr Flag
forall a. a -> ArgDescr a
NoArg Flag
DatabaseDoNotMigrate)
       ("Disallow Hets to create or alter the database tables" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
crS
       FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "This option is ignored if the option --database-config is given.")
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "" ["database-file"] ((FilePath -> Flag) -> FilePath -> ArgDescr Flag
forall a. (FilePath -> a) -> FilePath -> ArgDescr a
ReqArg FilePath -> Flag
DatabaseOutputFile "FILEPATH")
       ("path to the sqlite database file" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
crS
       FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "This option is ignored if the option --database-config is given.")
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "" ["database-config"] ((FilePath -> Flag) -> FilePath -> ArgDescr Flag
forall a. (FilePath -> a) -> FilePath -> ArgDescr a
ReqArg FilePath -> Flag
DatabaseConfigFile "FILEPATH")
       "path to the database configuration (yaml) file"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "" ["database-subconfig"] ((FilePath -> Flag) -> FilePath -> ArgDescr Flag
forall a. (FilePath -> a) -> FilePath -> ArgDescr a
ReqArg FilePath -> Flag
DatabaseSubConfigKey "KEY")
       ("subconfig of the database-config" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
crS
       FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "one of: production, development, test")
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "" ["database-fileversion-id"] ((FilePath -> Flag) -> FilePath -> ArgDescr Flag
forall a. (FilePath -> a) -> FilePath -> ArgDescr a
ReqArg FilePath -> Flag
DatabaseFileVersionId "ID")
       "ID (sha1-hash) of the file version to associate the data with"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "" ["database-reanalyze"] (Flag -> ArgDescr Flag
forall a. a -> ArgDescr a
NoArg Flag
DatabaseReanalyze)
       "Overwrite data of this document and its imports in the database"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "U" ["xupdate"] ((FilePath -> Flag) -> FilePath -> ArgDescr Flag
forall a. (FilePath -> a) -> FilePath -> ArgDescr a
ReqArg FilePath -> Flag
XUpdate "FILE")
      "apply additional xupdates from file"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "R" [FilePath
recursiveS] (Flag -> ArgDescr Flag
forall a. a -> ArgDescr a
NoArg Flag
Recurse)
      "output also imported libraries"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "A" [FilePath
applyAutomaticRuleS] (Flag -> ArgDescr Flag
forall a. a -> ArgDescr a
NoArg Flag
ApplyAutomatic)
      "apply automatic dev-graph strategy"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "N" [FilePath
normalFormS] (Flag -> ArgDescr Flag
forall a. a -> ArgDescr a
NoArg Flag
NormalForm)
      "compute normal forms (takes long)"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "n" [FilePath
namedSpecsS] ((FilePath -> Flag) -> FilePath -> ArgDescr Flag
forall a. (FilePath -> a) -> FilePath -> ArgDescr a
ReqArg ([SIMPLE_ID] -> Flag
Specs ([SIMPLE_ID] -> Flag)
-> (FilePath -> [SIMPLE_ID]) -> FilePath -> Flag
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> [SIMPLE_ID]
parseSIdOpts) "NSPECS")
      ("process specs option " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
crS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
cslst FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " SIMPLE-ID")
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "w" [FilePath
viewS] ((FilePath -> Flag) -> FilePath -> ArgDescr Flag
forall a. (FilePath -> a) -> FilePath -> ArgDescr a
ReqArg ([SIMPLE_ID] -> Flag
Views ([SIMPLE_ID] -> Flag)
-> (FilePath -> [SIMPLE_ID]) -> FilePath -> Flag
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> [SIMPLE_ID]
parseSIdOpts) "NVIEWS")
      ("process views option " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
crS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
cslst FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " SIMPLE-ID")
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "t" [FilePath
transS] ((FilePath -> Flag) -> FilePath -> ArgDescr Flag
forall a. (FilePath -> a) -> FilePath -> ArgDescr a
ReqArg FilePath -> Flag
parseTransOpt "TRANS")
      ("translation option " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
crS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
          "is a colon-separated list" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
          FilePath
crS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ "of one or more from: SIMPLE-ID")
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "Y" [FilePath
lossyTransS] (Flag -> ArgDescr Flag
forall a. a -> ArgDescr a
NoArg Flag
LossyTrans)
      "apply translations in a lossy way"
    , FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "a" [FilePath
amalgS] ((FilePath -> Flag) -> FilePath -> ArgDescr Flag
forall a. (FilePath -> a) -> FilePath -> ArgDescr a
ReqArg FilePath -> Flag
parseCASLAmalg "ANALYSIS")
      ("CASL amalgamability analysis options" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
crS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
cslst FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
       FilePath
crS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ [FilePath] -> FilePath
joinBar ((CASLAmalgOpt -> FilePath) -> [CASLAmalgOpt] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map CASLAmalgOpt -> FilePath
forall a. Show a => a -> FilePath
show [CASLAmalgOpt]
caslAmalgOpts)),
      FilePath
-> [FilePath] -> ArgDescr Flag -> FilePath -> OptDescr Flag
forall a.
FilePath -> [FilePath] -> ArgDescr a -> FilePath -> OptDescr a
Option "M" ["MMT"] (Flag -> ArgDescr Flag
forall a. a -> ArgDescr a
NoArg Flag
UseMMT)
      "use MMT" ]

-- | options that require arguments for the wep-api excluding \"translation\"
optionArgs :: [(String, String -> Flag)]
optionArgs :: [(FilePath, FilePath -> Flag)]
optionArgs = (OptDescr Flag
 -> [(FilePath, FilePath -> Flag)]
 -> [(FilePath, FilePath -> Flag)])
-> [(FilePath, FilePath -> Flag)]
-> [OptDescr Flag]
-> [(FilePath, FilePath -> Flag)]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ o :: OptDescr Flag
o l :: [(FilePath, FilePath -> Flag)]
l -> case OptDescr Flag
o of
  Option _ (s :: FilePath
s : _) (ReqArg f :: FilePath -> Flag
f _) _ | FilePath
s FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
/= FilePath
transS -> (FilePath
s, FilePath -> Flag
f) (FilePath, FilePath -> Flag)
-> [(FilePath, FilePath -> Flag)] -> [(FilePath, FilePath -> Flag)]
forall a. a -> [a] -> [a]
: [(FilePath, FilePath -> Flag)]
l
  _ -> [(FilePath, FilePath -> Flag)]
l) [] [OptDescr Flag]
options

-- | command line switches for the wep-api excluding non-dev-graph related ones
optionFlags :: [(String, Flag)]
optionFlags :: [(FilePath, Flag)]
optionFlags = ((FilePath, Flag) -> Bool)
-> [(FilePath, Flag)] -> [(FilePath, Flag)]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile ((FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
/= FilePath
justStructuredS)(FilePath -> Bool)
-> ((FilePath, Flag) -> FilePath) -> (FilePath, Flag) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FilePath, Flag) -> FilePath
forall a b. (a, b) -> a
fst) ([(FilePath, Flag)] -> [(FilePath, Flag)])
-> [(FilePath, Flag)] -> [(FilePath, Flag)]
forall a b. (a -> b) -> a -> b
$ (OptDescr Flag -> [(FilePath, Flag)] -> [(FilePath, Flag)])
-> [(FilePath, Flag)] -> [OptDescr Flag] -> [(FilePath, Flag)]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ o :: OptDescr Flag
o l :: [(FilePath, Flag)]
l -> case OptDescr Flag
o of
  Option _ (s :: FilePath
s : _) (NoArg f :: Flag
f) _ -> (FilePath
s, Flag
f) (FilePath, Flag) -> [(FilePath, Flag)] -> [(FilePath, Flag)]
forall a. a -> [a] -> [a]
: [(FilePath, Flag)]
l
  _ -> [(FilePath, Flag)]
l) [] [OptDescr Flag]
options

-- parser functions returning Flags --

-- | 'parseVerbosity' parses a 'Verbose' Flag from user input
parseVerbosity :: Maybe String -> Flag
parseVerbosity :: Maybe FilePath -> Flag
parseVerbosity ms :: Maybe FilePath
ms = case Maybe FilePath
ms of
    Nothing -> Int -> Flag
Verbose 2
    Just s :: FilePath
s -> Int -> Flag
Verbose (Int -> Flag) -> Int -> Flag
forall a b. (a -> b) -> a -> b
$ FilePath -> Int
parseInt FilePath
s

parseInt :: String -> Int
parseInt :: FilePath -> Int
parseInt s :: FilePath
s = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe (FilePath -> Int
forall a. FilePath -> a
hetsError (FilePath -> Int) -> FilePath -> Int
forall a b. (a -> b) -> a -> b
$ FilePath
s FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " is not a valid INT") (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ FilePath -> Maybe Int
forall a. Read a => FilePath -> Maybe a
readMaybe FilePath
s

parseCounter :: String -> Flag
parseCounter :: FilePath -> Flag
parseCounter = Int -> Flag
CounterSparQ (Int -> Flag) -> (FilePath -> Int) -> FilePath -> Flag
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Int
parseInt

divideIntoPortHost :: String -> Bool -> (String, String) -> (String, String)
divideIntoPortHost :: FilePath -> Bool -> (FilePath, FilePath) -> (FilePath, FilePath)
divideIntoPortHost s :: FilePath
s sw :: Bool
sw (accP :: FilePath
accP, accH :: FilePath
accH) = case FilePath
s of
    ':' : ll :: FilePath
ll -> FilePath -> Bool -> (FilePath, FilePath) -> (FilePath, FilePath)
divideIntoPortHost FilePath
ll Bool
True (FilePath
accP, FilePath
accH)
    c :: Char
c : ll :: FilePath
ll -> if Bool
sw then FilePath -> Bool -> (FilePath, FilePath) -> (FilePath, FilePath)
divideIntoPortHost FilePath
ll Bool
True (FilePath
accP, Char
c Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: FilePath
accH)
              else FilePath -> Bool -> (FilePath, FilePath) -> (FilePath, FilePath)
divideIntoPortHost FilePath
ll Bool
False (Char
c Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: FilePath
accP, FilePath
accH)
    [] -> (FilePath
accP, FilePath
accH)

-- | 'parseConnect' parses a port Flag from user input
parseConnect :: String -> Flag
parseConnect :: FilePath -> Flag
parseConnect s :: FilePath
s
 = let (sP :: FilePath
sP, sH :: FilePath
sH) = FilePath -> Bool -> (FilePath, FilePath) -> (FilePath, FilePath)
divideIntoPortHost FilePath
s Bool
False ([], [])
   in case ReadS Int
forall a. Read a => ReadS a
reads FilePath
sP of
                [(i :: Int
i, "")] -> Int -> FilePath -> Flag
Connect Int
i FilePath
sH
                _ -> Int -> FilePath -> Flag
Connect (-1) FilePath
sH

parseListen :: String -> Flag
parseListen :: FilePath -> Flag
parseListen s :: FilePath
s
 = case ReadS Int
forall a. Read a => ReadS a
reads FilePath
s of
                [(i :: Int
i, "")] -> Int -> Flag
Listen Int
i
                _ -> Int -> Flag
Listen (-1)

parseEncoding :: String -> Flag
parseEncoding :: FilePath -> Flag
parseEncoding s :: FilePath
s = case (Char -> Char) -> FilePath -> FilePath
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (FilePath -> FilePath) -> FilePath -> FilePath
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath
trim FilePath
s of
  "latin1" -> Enc -> Flag
IOEncoding Enc
Latin1
  "utf8" -> Enc -> Flag
IOEncoding Enc
Utf8
  r :: FilePath
r -> FilePath -> Flag
forall a. FilePath -> a
hetsError (FilePath
r FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " is not a valid encoding")

-- | intypes useable for downloads
downloadExtensions :: [String]
downloadExtensions :: [FilePath]
downloadExtensions = (FilePath -> FilePath) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map ('.' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
:) ([FilePath] -> [FilePath]) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> a -> b
$
    (InType -> FilePath) -> [InType] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map InType -> FilePath
forall a. Show a => a -> FilePath
show [InType]
plainInTypes
    [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ (InType -> FilePath) -> [InType] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map ((FilePath
treeS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++) (FilePath -> FilePath)
-> (InType -> FilePath) -> InType -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InType -> FilePath
forall a. Show a => a -> FilePath
show) [ATType -> InType
ATermIn ATType
BAF, ATType -> InType
ATermIn ATType
NonBAF]
    [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ (InType -> FilePath) -> [InType] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map InType -> FilePath
forall a. Show a => a -> FilePath
show [InType]
aInTypes

-- | remove the extension from a file
rmSuffix :: FilePath -> FilePath
rmSuffix :: FilePath -> FilePath
rmSuffix = (FilePath, Maybe FilePath) -> FilePath
forall a b. (a, b) -> a
fst ((FilePath, Maybe FilePath) -> FilePath)
-> (FilePath -> (FilePath, Maybe FilePath)) -> FilePath -> FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [FilePath] -> FilePath -> (FilePath, Maybe FilePath)
stripSuffix (FilePath
envSuffix FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: [FilePath]
downloadExtensions)

-- | the suffix of env files
envSuffix :: String
envSuffix :: FilePath
envSuffix = '.' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: FilePath
envS

-- | the suffix of env files
prfSuffix :: String
prfSuffix :: FilePath
prfSuffix = '.' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: FilePath
prfS

isDefLogic :: String -> HetcatsOpts -> Bool
isDefLogic :: FilePath -> HetcatsOpts -> Bool
isDefLogic s :: FilePath
s = (FilePath
s FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
==) (FilePath -> Bool)
-> (HetcatsOpts -> FilePath) -> HetcatsOpts -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HetcatsOpts -> FilePath
defLogic

defLogicIsDMU :: HetcatsOpts -> Bool
defLogicIsDMU :: HetcatsOpts -> Bool
defLogicIsDMU = FilePath -> HetcatsOpts -> Bool
isDefLogic "DMU"

getExtensions :: HetcatsOpts -> [String]
getExtensions :: HetcatsOpts -> [FilePath]
getExtensions opts :: HetcatsOpts
opts = case HetcatsOpts -> InType
intype HetcatsOpts
opts of
        GuessIn
          | HetcatsOpts -> Bool
defLogicIsDMU HetcatsOpts
opts -> [".xml"]
          | FilePath -> HetcatsOpts -> Bool
isDefLogic "Framework" HetcatsOpts
opts
            -> [".elf", ".thy", ".maude", ".het", ".dol"]
        GuessIn -> [FilePath]
downloadExtensions
        e :: InType
e@(ATermIn _) -> ['.' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: InType -> FilePath
forall a. Show a => a -> FilePath
show InType
e, '.' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: FilePath
treeS FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ InType -> FilePath
forall a. Show a => a -> FilePath
show InType
e]
        e :: InType
e -> ['.' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: InType -> FilePath
forall a. Show a => a -> FilePath
show InType
e]
  [FilePath] -> [FilePath] -> [FilePath]
forall a. [a] -> [a] -> [a]
++ [FilePath
envSuffix]

getFileNames :: [String] -> FilePath -> [FilePath]
getFileNames :: [FilePath] -> FilePath -> [FilePath]
getFileNames exts :: [FilePath]
exts file :: FilePath
file =
  FilePath
file FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: (FilePath -> FilePath) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (FilePath -> FilePath
rmSuffix FilePath
file FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++) [FilePath]
exts

-- | checks if a source file for the given file name exists
existsAnSource :: HetcatsOpts -> FilePath -> IO (Maybe FilePath)
existsAnSource :: HetcatsOpts -> FilePath -> IO (Maybe FilePath)
existsAnSource opts :: HetcatsOpts
opts file :: FilePath
file = do
  let names :: [FilePath]
names = [FilePath] -> FilePath -> [FilePath]
getFileNames (HetcatsOpts -> [FilePath]
getExtensions HetcatsOpts
opts) FilePath
file
  -- look for the first existing file
  [Bool]
validFlags <- (FilePath -> IO Bool) -> [FilePath] -> IO [Bool]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM FilePath -> IO Bool
doesFileExist [FilePath]
names
  Maybe FilePath -> IO (Maybe FilePath)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe FilePath -> IO (Maybe FilePath))
-> ([(Bool, FilePath)] -> Maybe FilePath)
-> [(Bool, FilePath)]
-> IO (Maybe FilePath)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Bool, FilePath) -> FilePath)
-> Maybe (Bool, FilePath) -> Maybe FilePath
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Bool, FilePath) -> FilePath
forall a b. (a, b) -> b
snd (Maybe (Bool, FilePath) -> Maybe FilePath)
-> ([(Bool, FilePath)] -> Maybe (Bool, FilePath))
-> [(Bool, FilePath)]
-> Maybe FilePath
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Bool, FilePath) -> Bool)
-> [(Bool, FilePath)] -> Maybe (Bool, FilePath)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (Bool, FilePath) -> Bool
forall a b. (a, b) -> a
fst ([(Bool, FilePath)] -> IO (Maybe FilePath))
-> [(Bool, FilePath)] -> IO (Maybe FilePath)
forall a b. (a -> b) -> a -> b
$ [Bool] -> [FilePath] -> [(Bool, FilePath)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Bool]
validFlags [FilePath]
names

-- | should env be written
hasEnvOut :: HetcatsOpts -> Bool
hasEnvOut :: HetcatsOpts -> Bool
hasEnvOut = (OutType -> Bool) -> [OutType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ( \ o :: OutType
o -> case OutType
o of
                           EnvOut -> Bool
True
                           _ -> Bool
False) ([OutType] -> Bool)
-> (HetcatsOpts -> [OutType]) -> HetcatsOpts -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HetcatsOpts -> [OutType]
outtypes

-- | should prf be written
isPrfOut :: OutType -> Bool
isPrfOut :: OutType -> Bool
isPrfOut o :: OutType
o = case OutType
o of
    Prf -> Bool
True
    _ -> Bool
False

-- | should prf be written
hasPrfOut :: HetcatsOpts -> Bool
hasPrfOut :: HetcatsOpts -> Bool
hasPrfOut = (OutType -> Bool) -> [OutType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any OutType -> Bool
isPrfOut ([OutType] -> Bool)
-> (HetcatsOpts -> [OutType]) -> HetcatsOpts -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HetcatsOpts -> [OutType]
outtypes

-- | remove prf writing
removePrfOut :: HetcatsOpts -> HetcatsOpts
removePrfOut :: HetcatsOpts -> HetcatsOpts
removePrfOut opts :: HetcatsOpts
opts =
     HetcatsOpts
opts { outtypes :: [OutType]
outtypes = (OutType -> Bool) -> [OutType] -> [OutType]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (OutType -> Bool) -> OutType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OutType -> Bool
isPrfOut) ([OutType] -> [OutType]) -> [OutType] -> [OutType]
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> [OutType]
outtypes HetcatsOpts
opts }

{- |
gets two Paths and checks if the first file is not older than the
second one and should return True for two identical files -}
checkRecentEnv :: HetcatsOpts -> FilePath -> FilePath -> IO Bool
checkRecentEnv :: HetcatsOpts -> FilePath -> FilePath -> IO Bool
checkRecentEnv opts :: HetcatsOpts
opts fp1 :: FilePath
fp1 base2 :: FilePath
base2 = Bool -> IO Bool -> IO Bool
forall a. a -> IO a -> IO a
catchIOException Bool
False (IO Bool -> IO Bool) -> IO Bool -> IO Bool
forall a b. (a -> b) -> a -> b
$ do
    UTCTime
fp1_time <- FilePath -> IO UTCTime
getModificationTime FilePath
fp1
    Maybe FilePath
maybe_source_file <- HetcatsOpts -> FilePath -> IO (Maybe FilePath)
existsAnSource HetcatsOpts
opts {intype :: InType
intype = InType
GuessIn} FilePath
base2
    IO Bool -> (FilePath -> IO Bool) -> Maybe FilePath -> IO Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False) ( \ fp2 :: FilePath
fp2 -> do
       UTCTime
fp2_time <- FilePath -> IO UTCTime
getModificationTime FilePath
fp2
       Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return (UTCTime
fp1_time UTCTime -> UTCTime -> Bool
forall a. Ord a => a -> a -> Bool
>= UTCTime
fp2_time)) Maybe FilePath
maybe_source_file

parseCatalog :: String -> Flag
parseCatalog :: FilePath -> Flag
parseCatalog str :: FilePath
str = [(FilePath, FilePath)] -> Flag
UrlCatalog ([(FilePath, FilePath)] -> Flag) -> [(FilePath, FilePath)] -> Flag
forall a b. (a -> b) -> a -> b
$ (FilePath -> (FilePath, FilePath))
-> [FilePath] -> [(FilePath, FilePath)]
forall a b. (a -> b) -> [a] -> [b]
map ((\ l :: [FilePath]
l -> case [FilePath]
l of
  [a :: FilePath
a, b :: FilePath
b] -> (FilePath
a, FilePath
b)
  _ -> FilePath -> (FilePath, FilePath)
forall a. FilePath -> a
hetsError (FilePath
str FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " is not a valid URL catalog"))
  ([FilePath] -> (FilePath, FilePath))
-> (FilePath -> [FilePath]) -> FilePath -> (FilePath, FilePath)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> FilePath -> [FilePath]
forall a. Eq a => a -> [a] -> [[a]]
splitOn '=') ([FilePath] -> [(FilePath, FilePath)])
-> [FilePath] -> [(FilePath, FilePath)]
forall a b. (a -> b) -> a -> b
$ Char -> FilePath -> [FilePath]
forall a. Eq a => a -> [a] -> [[a]]
splitOn ',' FilePath
str

-- | 'parseInType' parses an 'InType' Flag from user input
parseInType :: String -> Flag
parseInType :: FilePath -> Flag
parseInType = InType -> Flag
InType (InType -> Flag) -> (FilePath -> InType) -> FilePath -> Flag
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> InType
parseInType1

-- | 'parseInType1' parses an 'InType' Flag from a String
parseInType1 :: String -> InType
parseInType1 :: FilePath -> InType
parseInType1 str :: FilePath
str =
  case ReadS InType
forall a. Read a => ReadS a
reads FilePath
str of
    [(t :: InType
t, "")] -> InType
t
    _ -> FilePath -> InType
forall a. FilePath -> a
hetsError (FilePath
str FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " is not a valid ITYPE")
      {- the mere typo read instead of reads caused the runtime error:
         Fail: Prelude.read: no parse -}

-- 'parseOutTypes' parses an 'OutTypes' Flag from user input
parseOutTypes :: String -> Flag
parseOutTypes :: FilePath -> Flag
parseOutTypes str :: FilePath
str = case ReadS [OutType]
forall a. Read a => ReadS a
reads ReadS [OutType] -> ReadS [OutType]
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath
bracket FilePath
str of
    [(l :: [OutType]
l, "")] -> [OutType] -> Flag
OutTypes [OutType]
l
    _ -> FilePath -> Flag
forall a. FilePath -> a
hetsError (FilePath
str FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ " is not a valid OTYPES")

-- | parses a comma separated list from user input
parseSIdOpts :: String -> [SIMPLE_ID]
parseSIdOpts :: FilePath -> [SIMPLE_ID]
parseSIdOpts = (FilePath -> SIMPLE_ID) -> [FilePath] -> [SIMPLE_ID]
forall a b. (a -> b) -> [a] -> [b]
map FilePath -> SIMPLE_ID
mkSimpleId ([FilePath] -> [SIMPLE_ID])
-> (FilePath -> [FilePath]) -> FilePath -> [SIMPLE_ID]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> FilePath -> [FilePath]
forall a. Eq a => a -> [a] -> [[a]]
splitOn ','

-- | 'parseTransOpt' parses a 'Trans' Flag from user input
parseTransOpt :: String -> Flag
parseTransOpt :: FilePath -> Flag
parseTransOpt = [SIMPLE_ID] -> Flag
Trans ([SIMPLE_ID] -> Flag)
-> (FilePath -> [SIMPLE_ID]) -> FilePath -> Flag
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FilePath -> SIMPLE_ID) -> [FilePath] -> [SIMPLE_ID]
forall a b. (a -> b) -> [a] -> [b]
map FilePath -> SIMPLE_ID
mkSimpleId ([FilePath] -> [SIMPLE_ID])
-> (FilePath -> [FilePath]) -> FilePath -> [SIMPLE_ID]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> [FilePath]
splitPaths

-- | guesses the InType
guess :: String -> InType -> InType
guess :: FilePath -> InType -> InType
guess file :: FilePath
file itype :: InType
itype = case InType
itype of
    GuessIn -> FilePath -> InType
guessInType FilePath
file
    _ -> InType
itype

-- | 'guessInType' parses an 'InType' from the FilePath
guessInType :: FilePath -> InType
guessInType :: FilePath -> InType
guessInType file :: FilePath
file = case [FilePath] -> FilePath -> (FilePath, FilePath, Maybe FilePath)
fileparse [FilePath]
downloadExtensions FilePath
file of
      (_, _, Just ('.' : suf :: FilePath
suf)) -> FilePath -> InType
parseInType1 FilePath
suf
      (_, _, _) -> InType
GuessIn

-- | 'parseCASLAmalg' parses CASL amalgamability options
parseCASLAmalg :: String -> Flag
parseCASLAmalg :: FilePath -> Flag
parseCASLAmalg str :: FilePath
str =
    case ReadS [CASLAmalgOpt]
forall a. Read a => ReadS a
reads ReadS [CASLAmalgOpt] -> ReadS [CASLAmalgOpt]
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath
bracket FilePath
str of
    [(l :: [CASLAmalgOpt]
l, "")] -> [CASLAmalgOpt] -> Flag
CASLAmalg ([CASLAmalgOpt] -> Flag) -> [CASLAmalgOpt] -> Flag
forall a b. (a -> b) -> a -> b
$ (CASLAmalgOpt -> Bool) -> [CASLAmalgOpt] -> [CASLAmalgOpt]
forall a. (a -> Bool) -> [a] -> [a]
filter ( \ o :: CASLAmalgOpt
o -> case CASLAmalgOpt
o of
                                      NoAnalysis -> Bool
False
                                      _ -> Bool
True ) [CASLAmalgOpt]
l
    _ -> FilePath -> Flag
forall a. FilePath -> a
hetsError (FilePath -> Flag) -> FilePath -> Flag
forall a b. (a -> b) -> a -> b
$ FilePath
str FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++
                    " is not a valid CASL amalgamability analysis option list"

-- main functions --

-- | 'hetcatsOpts' parses sensible HetcatsOpts from ARGV
hetcatsOpts :: [String] -> IO HetcatsOpts
hetcatsOpts :: [FilePath] -> IO HetcatsOpts
hetcatsOpts argv :: [FilePath]
argv =
  let argv' :: [FilePath]
argv' = (FilePath -> Bool) -> [FilePath] -> [FilePath]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (FilePath -> Bool) -> FilePath -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Bool
isUni) [FilePath]
argv
      isUni :: FilePath -> Bool
isUni = FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf "--uni"
   in case ArgOrder Flag
-> [OptDescr Flag]
-> [FilePath]
-> ([Flag], [FilePath], [FilePath])
forall a.
ArgOrder a
-> [OptDescr a] -> [FilePath] -> ([a], [FilePath], [FilePath])
getOpt ArgOrder Flag
forall a. ArgOrder a
Permute [OptDescr Flag]
options [FilePath]
argv' of
        (opts :: [Flag]
opts, nonOpts :: [FilePath]
nonOpts, []) ->
            do [Flag]
flags <- [Flag] -> IO [Flag]
checkFlags [Flag]
opts
               let opts' :: HetcatsOpts
opts' = ((Flag -> HetcatsOpts -> HetcatsOpts)
-> HetcatsOpts -> [Flag] -> HetcatsOpts
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((HetcatsOpts -> Flag -> HetcatsOpts)
-> Flag -> HetcatsOpts -> HetcatsOpts
forall a b c. (a -> b -> c) -> b -> a -> c
flip HetcatsOpts -> Flag -> HetcatsOpts
makeOpts) HetcatsOpts
defaultHetcatsOpts [Flag]
flags)
                            { infiles :: [FilePath]
infiles = [FilePath]
nonOpts }
               HetcatsOpts -> IO HetcatsOpts
setupDatabaseOptions HetcatsOpts
opts'
        (_, _, errs :: [FilePath]
errs) -> FilePath -> IO HetcatsOpts
forall a. FilePath -> IO a
hetsIOError ([FilePath] -> FilePath
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [FilePath]
errs)
  where
    setupDatabaseOptions :: HetcatsOpts -> IO HetcatsOpts
    setupDatabaseOptions :: HetcatsOpts -> IO HetcatsOpts
setupDatabaseOptions opts :: HetcatsOpts
opts = do
      let filepath :: FilePath
filepath = if [FilePath] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([FilePath] -> Bool) -> [FilePath] -> Bool
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> [FilePath]
infiles HetcatsOpts
opts then "" else [FilePath] -> FilePath
forall a. [a] -> a
head ([FilePath] -> FilePath) -> [FilePath] -> FilePath
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> [FilePath]
infiles HetcatsOpts
opts
      let dbContext :: DBContext
dbContext = DBContext
DBConfig.emptyDBContext
            { contextFileVersion :: FilePath
DBConfig.contextFileVersion = HetcatsOpts -> FilePath
databaseFileVersionId HetcatsOpts
opts
            , contextFilePath :: FilePath
DBConfig.contextFilePath = FilePath
filepath
            }
      -- If the fileVersionId is not given, Hets has not been called by Ontohub.
      -- Hence, there is no git handling and we always need to reanalyze the
      -- file.
      let databaseReanalyze' :: Bool
databaseReanalyze' =
            FilePath -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (HetcatsOpts -> FilePath
databaseFileVersionId HetcatsOpts
opts) Bool -> Bool -> Bool
|| HetcatsOpts -> Bool
databaseReanalyze HetcatsOpts
opts
      DBConfig
dbConfig <- if OutType
DbOut OutType -> [OutType] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` HetcatsOpts -> [OutType]
outtypes HetcatsOpts
opts
                  then FilePath -> FilePath -> FilePath -> Bool -> IO DBConfig
DBConfig.parseDatabaseConfig
                         (HetcatsOpts -> FilePath
databaseOutputFile HetcatsOpts
opts)
                         (HetcatsOpts -> FilePath
databaseConfigFile HetcatsOpts
opts)
                         (HetcatsOpts -> FilePath
databaseSubConfigKey HetcatsOpts
opts)
                         (HetcatsOpts -> Bool
databaseDoMigrate HetcatsOpts
opts)
                  else DBConfig -> IO DBConfig
forall (m :: * -> *) a. Monad m => a -> m a
return DBConfig
DBConfig.emptyDBConfig
      HetcatsOpts -> IO HetcatsOpts
forall (m :: * -> *) a. Monad m => a -> m a
return HetcatsOpts
opts { databaseConfig :: DBConfig
databaseConfig = DBConfig
dbConfig
                  , databaseContext :: DBContext
databaseContext = DBContext
dbContext
                  , databaseReanalyze :: Bool
databaseReanalyze = Bool
databaseReanalyze'
                  }


printOptionsWarnings :: HetcatsOpts -> IO ()
printOptionsWarnings :: HetcatsOpts -> IO ()
printOptionsWarnings opts :: HetcatsOpts
opts =
  let v :: Int
v = HetcatsOpts -> Int
verbose HetcatsOpts
opts in
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (FilePath -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (HetcatsOpts -> FilePath
pidFile HetcatsOpts
opts) Bool -> Bool -> Bool
|| HetcatsOpts -> Bool
serve HetcatsOpts
opts)
    (Int -> Int -> FilePath -> IO ()
verbMsgIOLn Int
v 1 "option -P has no effect because it is used without -X")

-- | 'checkFlags' checks all parsed Flags for sanity
checkFlags :: [Flag] -> IO [Flag]
checkFlags :: [Flag] -> IO [Flag]
checkFlags fs :: [Flag]
fs = do
    let collectFlags :: [Flag] -> IO [Flag]
collectFlags = [Flag] -> IO [Flag]
collectDirs
                        ([Flag] -> IO [Flag]) -> ([Flag] -> [Flag]) -> [Flag] -> IO [Flag]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Flag] -> [Flag]
collectOutTypes
                        ([Flag] -> [Flag]) -> ([Flag] -> [Flag]) -> [Flag] -> [Flag]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Flag] -> [Flag]
collectVerbosity
                        ([Flag] -> [Flag]) -> ([Flag] -> [Flag]) -> [Flag] -> [Flag]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Flag] -> [Flag]
collectSpecOpts
                        -- collect some more here?
        h :: Bool
h = [()] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ () | Flag
Help <- [Flag]
fs]
        v :: Bool
v = [()] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ () | Flag
Version <- [Flag]
fs]
        vn :: Bool
vn = [()] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ () | Flag
VersionNumeric <- [Flag]
fs]
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
h (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> IO ()
putStr FilePath
hetsUsage
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
v (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> IO ()
putStrLn FilePath
hetsVersion
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
vn (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> IO ()
putStrLn FilePath
hetsVersionNumeric
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
h Bool -> Bool -> Bool
&& Bool
v Bool -> Bool -> Bool
&& Bool
vn) IO ()
forall a. IO a
exitSuccess
    [Flag] -> IO [Flag]
collectFlags [Flag]
fs

-- auxiliary functions: FileSystem interaction --

-- | check if infile is uri
checkUri :: FilePath -> Bool
checkUri :: FilePath -> Bool
checkUri file :: FilePath
file = "://" FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` (Char -> Bool) -> FilePath -> FilePath
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isAlpha FilePath
file
   -- (http://, https://, ftp://, file://, etc.)

-- | 'checkOutDirs' checks a list of OutDir for sanity
checkOutDirs :: [Flag] -> IO [Flag]
checkOutDirs :: [Flag] -> IO [Flag]
checkOutDirs fs :: [Flag]
fs = do
    case [Flag]
fs of
        [] -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        [f :: Flag
f] -> Flag -> IO ()
checkOutDir Flag
f
        _ -> FilePath -> IO ()
forall a. FilePath -> IO a
hetsIOError
            "Only one output directory may be specified on the command line"
    [Flag] -> IO [Flag]
forall (m :: * -> *) a. Monad m => a -> m a
return [Flag]
fs

-- | 'checkLibDirs' checks a list of LibDir for sanity
checkLibDirs :: [Flag] -> IO [Flag]
checkLibDirs :: [Flag] -> IO [Flag]
checkLibDirs fs :: [Flag]
fs =
    case [Flag]
fs of
        [] -> do
            FilePath
s <- FilePath -> FilePath -> IO FilePath
getEnvDef "HETS_LIB" ""
            if FilePath -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null FilePath
s then [Flag] -> IO [Flag]
forall (m :: * -> *) a. Monad m => a -> m a
return [] else do
                let d :: Flag
d = FilePath -> Flag
LibDirs FilePath
s
                [Flag] -> IO [Flag]
checkLibDirs [Flag
d]
                [Flag] -> IO [Flag]
forall (m :: * -> *) a. Monad m => a -> m a
return [Flag
d]
        [LibDirs f :: FilePath
f] -> (FilePath -> IO ()) -> [FilePath] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ FilePath -> IO ()
checkLibDir ([FilePath] -> [FilePath]
joinHttpLibPath ([FilePath] -> [FilePath]) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> a -> b
$ FilePath -> [FilePath]
splitPaths FilePath
f)
          IO () -> IO [Flag] -> IO [Flag]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Flag] -> IO [Flag]
forall (m :: * -> *) a. Monad m => a -> m a
return [Flag]
fs
        _ -> FilePath -> IO [Flag]
forall a. FilePath -> IO a
hetsIOError
            "Only one library path may be specified on the command line"

joinHttpLibPath :: [String] -> [String]
joinHttpLibPath :: [FilePath] -> [FilePath]
joinHttpLibPath l :: [FilePath]
l = case [FilePath]
l of
  p :: FilePath
p : f :: FilePath
f : r :: [FilePath]
r | FilePath
p  FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== "file" Bool -> Bool -> Bool
&& Int -> FilePath -> FilePath
forall a. Int -> [a] -> [a]
take 2 FilePath
f FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== "//" ->
    (FilePath
p FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ ':' Char -> FilePath -> FilePath
forall a. a -> [a] -> [a]
: FilePath
f) FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: [FilePath] -> [FilePath]
joinHttpLibPath [FilePath]
r
  p :: FilePath
p : f :: FilePath
f : _ | FilePath -> [FilePath] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem FilePath
p ["http", "https"] Bool -> Bool -> Bool
&& Int -> FilePath -> FilePath
forall a. Int -> [a] -> [a]
take 2 FilePath
f FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== "//" ->
    [FilePath -> [FilePath] -> FilePath
forall a. [a] -> [[a]] -> [a]
intercalate ":" [FilePath]
l]
  f :: FilePath
f : r :: [FilePath]
r -> FilePath
f FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: [FilePath] -> [FilePath]
joinHttpLibPath [FilePath]
r
  [] -> []

-- | 'checkLibDir' checks a single LibDir for sanity
checkLibDir :: FilePath -> IO ()
checkLibDir :: FilePath -> IO ()
checkLibDir file :: FilePath
file = do
    Bool
exists <- if FilePath -> Bool
checkUri FilePath
file then Bool -> IO Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True else FilePath -> IO Bool
doesDirectoryExist FilePath
file
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
exists (IO () -> IO ()) -> (FilePath -> IO ()) -> FilePath -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> IO ()
forall a. FilePath -> IO a
hetsIOError (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ "Not a valid library directory: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
file

-- | 'checkOutDir' checks a single OutDir for sanity
checkOutDir :: Flag -> IO ()
checkOutDir :: Flag -> IO ()
checkOutDir (OutDir file :: FilePath
file) = do
    Bool
exists <- FilePath -> IO Bool
doesDirectoryExist FilePath
file
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
exists (IO () -> IO ()) -> (FilePath -> IO ()) -> FilePath -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> IO ()
forall a. FilePath -> IO a
hetsIOError (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ "Not a valid output directory: " FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++ FilePath
file
checkOutDir _ = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- auxiliary functions: collect flags --

collectDirs :: [Flag] -> IO [Flag]
collectDirs :: [Flag] -> IO [Flag]
collectDirs fs :: [Flag]
fs = do
    let (ods :: [Flag]
ods, fs1 :: [Flag]
fs1) = (Flag -> Bool) -> [Flag] -> ([Flag], [Flag])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Flag -> Bool
isOutDir [Flag]
fs
        (lds :: [Flag]
lds, fs2 :: [Flag]
fs2) = (Flag -> Bool) -> [Flag] -> ([Flag], [Flag])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Flag -> Bool
isLibDir [Flag]
fs1
        isOutDir :: Flag -> Bool
isOutDir (OutDir _) = Bool
True
        isOutDir _ = Bool
False
        isLibDir :: Flag -> Bool
isLibDir (LibDirs _) = Bool
True
        isLibDir _ = Bool
False
    [Flag]
ods' <- [Flag] -> IO [Flag]
checkOutDirs [Flag]
ods
    [Flag]
lds' <- [Flag] -> IO [Flag]
checkLibDirs [Flag]
lds
    [Flag] -> IO [Flag]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Flag] -> IO [Flag]) -> [Flag] -> IO [Flag]
forall a b. (a -> b) -> a -> b
$ [Flag]
ods' [Flag] -> [Flag] -> [Flag]
forall a. [a] -> [a] -> [a]
++ [Flag]
lds' [Flag] -> [Flag] -> [Flag]
forall a. [a] -> [a] -> [a]
++ [Flag]
fs2

collectVerbosity :: [Flag] -> [Flag]
collectVerbosity :: [Flag] -> [Flag]
collectVerbosity fs :: [Flag]
fs =
    let (v :: Int
v, fs' :: [Flag]
fs') = (Flag -> (Int, [Flag]) -> (Int, [Flag]))
-> (Int, [Flag]) -> [Flag] -> (Int, [Flag])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ f :: Flag
f (n :: Int
n, rs :: [Flag]
rs) -> case Flag
f of
           Verbose x :: Int
x -> (if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0 then Int
x else Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
x, [Flag]
rs)
           _ -> (Int
n, Flag
f Flag -> [Flag] -> [Flag]
forall a. a -> [a] -> [a]
: [Flag]
rs)) (-1, []) [Flag]
fs
    in if Int
v Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 0 Bool -> Bool -> Bool
|| Bool -> Bool
not ([()] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [() | Flag
Quiet <- [Flag]
fs']) then [Flag]
fs' else Int -> Flag
Verbose Int
v Flag -> [Flag] -> [Flag]
forall a. a -> [a] -> [a]
: [Flag]
fs'

collectOutTypes :: [Flag] -> [Flag]
collectOutTypes :: [Flag] -> [Flag]
collectOutTypes fs :: [Flag]
fs =
    let (ots :: [OutType]
ots, fs' :: [Flag]
fs') = (Flag -> ([OutType], [Flag]) -> ([OutType], [Flag]))
-> ([OutType], [Flag]) -> [Flag] -> ([OutType], [Flag])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ f :: Flag
f (os :: [OutType]
os, rs :: [Flag]
rs) -> case Flag
f of
           OutTypes ot :: [OutType]
ot -> ([OutType]
ot [OutType] -> [OutType] -> [OutType]
forall a. [a] -> [a] -> [a]
++ [OutType]
os, [Flag]
rs)
           _ -> ([OutType]
os, Flag
f Flag -> [Flag] -> [Flag]
forall a. a -> [a] -> [a]
: [Flag]
rs)) ([], []) [Flag]
fs
    in if [OutType] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [OutType]
ots then [Flag]
fs' else [OutType] -> Flag
OutTypes [OutType]
ots Flag -> [Flag] -> [Flag]
forall a. a -> [a] -> [a]
: [Flag]
fs'

collectSpecOpts :: [Flag] -> [Flag]
collectSpecOpts :: [Flag] -> [Flag]
collectSpecOpts fs :: [Flag]
fs =
    let (specs :: [SIMPLE_ID]
specs, fs' :: [Flag]
fs') = (Flag -> ([SIMPLE_ID], [Flag]) -> ([SIMPLE_ID], [Flag]))
-> ([SIMPLE_ID], [Flag]) -> [Flag] -> ([SIMPLE_ID], [Flag])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ f :: Flag
f (os :: [SIMPLE_ID]
os, rs :: [Flag]
rs) -> case Flag
f of
           Specs ot :: [SIMPLE_ID]
ot -> ([SIMPLE_ID]
ot [SIMPLE_ID] -> [SIMPLE_ID] -> [SIMPLE_ID]
forall a. [a] -> [a] -> [a]
++ [SIMPLE_ID]
os, [Flag]
rs)
           _ -> ([SIMPLE_ID]
os, Flag
f Flag -> [Flag] -> [Flag]
forall a. a -> [a] -> [a]
: [Flag]
rs)) ([], []) [Flag]
fs
    in if [SIMPLE_ID] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SIMPLE_ID]
specs then [Flag]
fs' else [SIMPLE_ID] -> Flag
Specs [SIMPLE_ID]
specs Flag -> [Flag] -> [Flag]
forall a. a -> [a] -> [a]
: [Flag]
fs'

-- auxiliary functions: error messages --

-- | only print the error (and no usage info)
hetsError :: String -> a
hetsError :: FilePath -> a
hetsError = FilePath -> a
forall a. HasCallStack => FilePath -> a
error (FilePath -> a) -> (FilePath -> FilePath) -> FilePath -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ("command line usage error (see 'hets -h')\n" FilePath -> FilePath -> FilePath
forall a. [a] -> [a] -> [a]
++)

-- | print error and usage and exit with code 2
hetsIOError :: String -> IO a
hetsIOError :: FilePath -> IO a
hetsIOError s :: FilePath
s = do
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (FilePath -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null FilePath
s) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Handle -> FilePath -> IO ()
hPutStrLn Handle
stderr FilePath
s
  FilePath -> IO ()
putStr "for Hets usage, use: hets -h\n"
  ExitCode -> IO a
forall a. ExitCode -> IO a
exitWith (ExitCode -> IO a) -> ExitCode -> IO a
forall a b. (a -> b) -> a -> b
$ Int -> ExitCode
ExitFailure 2

-- | 'hetsUsage' generates usage information for the commandline
hetsUsage :: String
hetsUsage :: FilePath
hetsUsage = let header :: FilePath
header = "Usage: hets [OPTION ...] [FILE ...] [+RTS -?]"
  in FilePath -> [OptDescr Flag] -> FilePath
forall a. FilePath -> [OptDescr a] -> FilePath
usageInfo FilePath
header [OptDescr Flag]
options

{- | 'putIfVerbose' prints a given String to StdOut when the given HetcatsOpts'
Verbosity exceeds the given level -}
putIfVerbose :: HetcatsOpts -> Int -> String -> IO ()
putIfVerbose :: HetcatsOpts -> Int -> FilePath -> IO ()
putIfVerbose opts :: HetcatsOpts
opts level :: Int
level =
    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (HetcatsOpts -> Bool
outputToStdout HetcatsOpts
opts) (IO () -> IO ()) -> (FilePath -> IO ()) -> FilePath -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (HetcatsOpts -> Int
verbose HetcatsOpts
opts Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
level) (IO () -> IO ()) -> (FilePath -> IO ()) -> FilePath -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> IO ()
putStrLn

doDump :: HetcatsOpts -> String -> IO () -> IO ()
doDump :: HetcatsOpts -> FilePath -> IO () -> IO ()
doDump opts :: HetcatsOpts
opts str :: FilePath
str = Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (FilePath -> [FilePath] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem FilePath
str ([FilePath] -> Bool) -> [FilePath] -> Bool
forall a b. (a -> b) -> a -> b
$ HetcatsOpts -> [FilePath]
dumpOpts HetcatsOpts
opts)

-- | show diagnostic messages (see Result.hs), according to verbosity level
showDiags :: HetcatsOpts -> [Diagnosis] -> IO ()
showDiags :: HetcatsOpts -> [Diagnosis] -> IO ()
showDiags opts :: HetcatsOpts
opts ds :: [Diagnosis]
ds =
    ResultT IO Any -> IO (Result Any)
forall (m :: * -> *) a. ResultT m a -> m (Result a)
runResultT (HetcatsOpts -> ResultT IO Any -> ResultT IO Any
forall a. HetcatsOpts -> ResultT IO a -> ResultT IO a
showDiags1 HetcatsOpts
opts (ResultT IO Any -> ResultT IO Any)
-> ResultT IO Any -> ResultT IO Any
forall a b. (a -> b) -> a -> b
$ Result Any -> ResultT IO Any
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result Any -> ResultT IO Any) -> Result Any -> ResultT IO Any
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> Maybe Any -> Result Any
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
ds Maybe Any
forall a. Maybe a
Nothing) IO (Result Any) -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

-- | show diagnostic messages (see Result.hs), according to verbosity level
showDiags1 :: HetcatsOpts -> ResultT IO a -> ResultT IO a
showDiags1 :: HetcatsOpts -> ResultT IO a -> ResultT IO a
showDiags1 opts :: HetcatsOpts
opts res :: ResultT IO a
res =
  let dbout :: Bool
dbout = OutType
DbOut OutType -> [OutType] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` HetcatsOpts -> [OutType]
outtypes HetcatsOpts
opts in
  if HetcatsOpts -> Bool
outputToStdout HetcatsOpts
opts Bool -> Bool -> Bool
|| Bool
dbout then do
    Result ds :: [Diagnosis]
ds res' :: Maybe a
res' <- IO (Result a) -> ResultT IO (Result a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (Result a) -> ResultT IO (Result a))
-> IO (Result a) -> ResultT IO (Result a)
forall a b. (a -> b) -> a -> b
$ ResultT IO a -> IO (Result a)
forall (m :: * -> *) a. ResultT m a -> m (Result a)
runResultT ResultT IO a
res
    Bool -> ResultT IO () -> ResultT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (HetcatsOpts -> Bool
outputToStdout HetcatsOpts
opts) (ResultT IO () -> ResultT IO ()) -> ResultT IO () -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ IO () -> ResultT IO ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> ResultT IO ()) -> IO () -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ Int -> [Diagnosis] -> IO ()
printDiags (HetcatsOpts -> Int
verbose HetcatsOpts
opts) [Diagnosis]
ds
    Bool -> ResultT IO () -> ResultT IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
dbout (ResultT IO () -> ResultT IO ()) -> ResultT IO () -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$ IO () -> ResultT IO ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> ResultT IO ()) -> IO () -> ResultT IO ()
forall a b. (a -> b) -> a -> b
$
      DBConfig -> DBContext -> Int -> [Diagnosis] -> IO ()
saveDiagnoses (HetcatsOpts -> DBConfig
databaseConfig HetcatsOpts
opts) (HetcatsOpts -> DBContext
databaseContext HetcatsOpts
opts) (HetcatsOpts -> Int
verbose HetcatsOpts
opts) [Diagnosis]
ds
    case Maybe a
res' of
      Just res'' :: a
res'' -> a -> ResultT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return a
res''
      Nothing -> Result a -> ResultT IO a
forall (m :: * -> *) a. MonadResult m => Result a -> m a
liftR (Result a -> ResultT IO a) -> Result a -> ResultT IO a
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> Maybe a -> Result a
forall a. [Diagnosis] -> Maybe a -> Result a
Result [] Maybe a
forall a. Maybe a
Nothing
  else ResultT IO a
res