libdirsS = "hets-libdirs"
namedSpecsS = "named-specs"
interactiveS = "interactive"
applyAutomaticRuleS = "apply-automatic-rule"
normalFormS = "normal-form"
urlCatalogS = "url-catalog"
relposS = "relative-positions"
fullSignS = "full-signatures"
fullTheoriesS = "full-theories"
logicGraphS = "logic-graph"
accessTokenS = "access-token"
genTermS, treeS, bafS :: String
graphE, ppS, envS, deltaS, prfS, omdocS, hsS, experimentalS :: String
tptpS, dfgS, cS :: String
showOpt :: String -> String
showOpt s = if null s then "" else " --" ++ s
showEqOpt :: String -> String -> String
showEqOpt k s = if null s then "" else showOpt k ++ "=" ++ s
-- | 'HetcatsOpts' is a record of all options received from the command line
data HetcatsOpts = HcOpt -- for comments see usage info
, urlCatalog :: [(String, String)]
, infiles :: [FilePath] -- ^ files to be read
, specNames :: [SIMPLE_ID] -- ^ specs to be processed
, transNames :: [SIMPLE_ID] -- ^ comorphism to be processed
, viewNames :: [SIMPLE_ID] -- ^ views to be processed
, outputToStdout :: Bool -- ^ send messages to stdout?
, caslAmalg :: [CASLAmalgOpt]
, computeNormalForm :: Bool
-- | use the library name in positions to avoid differences after uploads
, whitelist :: [[String]]
, blacklist :: [[String]]
, outputLogicGraph :: Bool
{- | 'defaultHetcatsOpts' defines the default HetcatsOpts, which are used as
basic values when the user specifies nothing else -}
defaultHetcatsOpts :: HetcatsOpts
defaultHetcatsOpts = HcOpt
, outtypes = [] -- no default
, computeNormalForm = False
, outputLogicGraph = False
instance Show HetcatsOpts where
let showFlag p o = if p opts then showOpt o else ""
showIPLists p s = let ll = p opts in if null ll then "" else
showEqOpt s . intercalate "," $ map (intercalate ".") ll
showEqOpt verboseS (show $ verbose opts)
++ showFlag outputLogicGraph logicGraphS
++ showFlag fileType fileTypeS
++ showFlag interactive interactiveS
s | s /= defLogic defaultHetcatsOpts -> showEqOpt logicS s
++ case defSyntax opts of
s | s /= defSyntax defaultHetcatsOpts -> showEqOpt serializationS s
++ case accessToken opts of
t -> showEqOpt accessTokenS t
++ showEqOpt libdirsS (intercalate ":" $ libdirs opts)
++ case modelSparQ opts of
f -> showEqOpt modelSparQS f
++ case counterSparQ opts of
n | n /= counterSparQ defaultHetcatsOpts
-> showEqOpt counterSparQS $ show n
++ showFlag ((/= -1) . connectP) connectS
++ showFlag ((/= -1) . listen) listenS
++ showIPLists whitelist whitelistS
++ showIPLists blacklist blacklistS
++ concatMap (showEqOpt "dump") (dumpOpts opts)
++ showEqOpt "encoding" (map toLower $ show $ ioEncoding opts)
++ showFlag useLibPos relposS
++ showFlag fullSign fullSignS
++ showFlag fullTheories fullTheoriesS
++ case urlCatalog opts of
cs -> showEqOpt urlCatalogS $ intercalate ","
$ map (\ (a, b) -> a ++ '=' : b) cs
++ showEqOpt intypeS (show $ intype opts)
++ showEqOpt outdirS (outdir opts)
++ showEqOpt outtypesS (intercalate "," $ map show $ outtypes opts)
++ showFlag recurse recursiveS
++ showFlag applyAutomatic applyAutomaticRuleS
++ showFlag computeNormalForm normalFormS
++ showEqOpt namedSpecsS (intercalate "," $ map show $ specNames opts)
++ showEqOpt transS (intercalate ":" $ map show $ transNames opts)
++ showEqOpt viewS (intercalate "," $ map show $ viewNames opts)
++ showEqOpt amalgS (tail $ init $ show $
++ " " ++ unwords (infiles opts)
-- | every 'Flag' describes an option (see usage info)
| CASLAmalg [CASLAmalgOpt]
| UrlCatalog [(String, String)]
-- | 'makeOpts' includes a parsed Flag in a set of HetcatsOpts
makeOpts :: HetcatsOpts -> Flag -> HetcatsOpts
let splitIPs = map (splitBy '.') . splitOn ','
Interactive -> opts { interactive = True }
XML -> opts { xmlFlag = True }
Listen x -> opts { listen = x }
Blacklist x -> opts { blacklist = splitIPs x }
Whitelist x -> opts { whitelist = splitIPs x }
Connect x y -> opts { connectP = x, connectH = y }
Analysis x -> opts { analysis = x }
Gui x -> opts { guiType = x }
InType x -> opts { intype = x }
LibDirs x -> opts { libdirs = joinHttpLibPath $ splitPaths x }
ModelSparQ x -> opts { modelSparQ = x }
CounterSparQ x -> opts { counterSparQ = x }
OutDir x -> opts { outdir = x }
OutTypes x -> opts { outtypes = x }
XUpdate x -> opts { xupdate = x }
Recurse -> opts { recurse = True }
ApplyAutomatic -> opts { applyAutomatic = True }
NormalForm -> opts { computeNormalForm = True }
Specs x -> opts { specNames = x }
Trans x -> opts { transNames = x }
Views x -> opts { viewNames = x }
Verbose x -> opts { verbose = x }
DefaultLogic x -> opts { defLogic = x }
DefaultSyntax x -> opts { defSyntax = x }
CASLAmalg x -> opts { caslAmalg = x }
Quiet -> opts { verbose = 0 }
Uncolored -> opts { uncolored = True }
Dump s -> opts { dumpOpts = s : dumpOpts opts }
IOEncoding e -> opts { ioEncoding = e }
Serve -> opts { serve = True }
Unlit -> opts { unlit = True }
RelPos -> opts { useLibPos = True }
UseMMT -> opts { runMMT = True }
FullTheories -> opts { fullTheories = True }
OutputLogicGraph -> opts { outputLogicGraph = True }
FileType -> opts { fileType = True }
FullSign -> opts { fullSign = True }
UrlCatalog m -> opts { urlCatalog = m ++ urlCatalog opts }
AccessToken s -> opts { accessToken = s }
Version -> opts -- skipped
-- | 'AnaType' describes the type of analysis to be performed
data AnaType = Basic | Structured | Skip
instance Show AnaType where
Structured -> showOpt justStructuredS
-- | check if structured analysis should be performed
isStructured :: HetcatsOpts -> Bool
isStructured a = case analysis a of
-- | 'GuiType' determines if we want the GUI shown
data GuiType = UseGui | NoGui
instance Show GuiType where
-- | 'InType' describes the type of input the infile contains
| ExperimentalIn -- ^ for testing new functionality
| CommonLogicIn Bool -- ^ "clf" or "clif" ('True' is long version)
| HtmlIn -- just to complain
instance Show InType where
ATermIn at -> genTermS ++ show at
CommonLogicIn isLong -> if isLong then "clif" else "clf"
-- maybe this optional tree prefix can be omitted
instance Read InType where
readsPrec _ = readShowAux $ concatMap showAll (plainInTypes ++ aInTypes)
where showAll i@(ATermIn _) = [(show i, i), (treeS ++ show i, i)]
showAll i = [(show i, i)]
-- | 'ATType' describes distinct types of ATerms
data ATType = BAF | NonBAF deriving Eq
instance Show ATType where
-- OwlXmlIn needs to be before OWLIn to avoid a read error in parseInType1
++ map OWLIn plainOwlFormats ++
[ HaskellIn, ExperimentalIn
, HolLightIn, IsaIn, ThyIn, PrfIn, OmdocIn, ProofCommand
, CommonLogicIn False, CommonLogicIn True
, DgXml, FreeCADIn, Xmi, Qvt, TPTPIn ]
aInTypes = [ ATermIn x | x <- [BAF, NonBAF] ]
-- | 'OWLFormat' lists possibilities for OWL syntax (in + out)
defaultOwlFormat :: OWLFormat
defaultOwlFormat = OwlXml --Manchester
plainOwlFormats :: [OWLFormat]
plainOwlFormats = [ Manchester, OwlXml, RdfXml, OBO, DOL, Turtle ]
instance Show OWLFormat where
-- "
owl.xml" ?? might occur but conflicts with dgxml
data SPFType = ConsistencyCheck | ProveTheory
instance Show SPFType where
spfTypes = [ConsistencyCheck, ProveTheory]
-- | 'OutType' describes the type of outputs that we want to generate
| XmlOut -- ^ development graph xml output
| JsonOut -- ^ development graph json output
| ExperimentalOut -- ^ for testing new functionality
| ThyFile -- ^ isabelle theory file
| DfgFile SPFType -- ^ SPASS input file
| SigFile Delta -- ^ signature as text
| TheoryFile Delta -- ^ signature with sentences as text
instance Show OutType where
PrettyOut p -> ppS ++ show p
GraphOut f -> graphE ++ show f
ExperimentalOut -> experimentalS
DfgFile t -> dfgS ++ show t
TPTPFile t -> tptpS ++ show t
SigFile d -> "sig" ++ show d
TheoryFile d -> "th" ++ show d
plainOutTypeList :: [OutType]
[ Prf, EnvOut ] ++ map OWLOut plainOwlFormats ++
[ CLIFOut, KIFOut, OmdocOut, XmlOut, JsonOut, ExperimentalOut
, HaskellOut, ThyFile, ComptableXml, FreeCADOut, SymXml, SymsXml]
outTypeList = let dl = [Delta, Fully] in
++ [ PrettyOut p | p <- prettyList ++ prettyList2]
++ [ SigFile d | d <- dl ]
++ [ TheoryFile d | d <- dl ]
++ [ DfgFile x | x <- spfTypes]
++ [ TPTPFile x | x <- spfTypes]
++ [ GraphOut f | f <- graphList ]
instance Read OutType where
readsPrec _ = readShow outTypeList
data Delta = Delta | Fully
instance Show Delta where
{- | 'PrettyType' describes the type of output we want the pretty-printer
data PrettyType = PrettyAscii Bool | PrettyLatex Bool | PrettyXml | PrettyHtml
instance Show PrettyType where
PrettyAscii b -> (if b then "stripped." else "") ++ "het"
PrettyLatex b -> (if b then "labelled." else "") ++ "tex"
prettyList :: [PrettyType]
prettyList = [PrettyAscii False, PrettyLatex False, PrettyXml, PrettyHtml]
prettyList2 :: [PrettyType]
prettyList2 = [PrettyAscii True, PrettyLatex True]
-- | 'GraphType' describes the type of Graph that we want generated
Dot Bool -- ^ True means show internal node labels
instance Show GraphType where
Dot si -> (if si then "exp." else "") ++ "dot"
graphList = [Dot True, Dot False]
{- | 'options' describes all available options and is used to generate usage
options :: [OptDescr Flag]
cslst = "is a comma-separated list"
++ crS ++ "of one or more from:"
joinBar l = "(" ++ intercalate "|" l ++ ")" in
[ Option "v" [verboseS] (OptArg parseVerbosity "0-5")
"verbosity, default is -v1"
, Option "q" ["quiet"] (NoArg Quiet)
"same as -v0, no output to stdout"
, Option "V" ["version"] (NoArg Version)
"print version number and exit"
, Option "h" ["help", "usage"] (NoArg Help)
"print usage information and exit"
, Option "g" [guiS] (NoArg (Gui UseGui))
, Option "u" ["uncolored"] (NoArg Uncolored)
"no colors in shown graphs"
, Option "x" [xmlS] (NoArg XML)
"use xml packets to communicate"
, Option "X" ["server"] (NoArg Serve)
"start hets as web-server"
, Option "G" [logicGraphS] (NoArg OutputLogicGraph)
"output logic graph (as xml) or as graph (-g)"
, Option "I" [interactiveS] (NoArg Interactive)
"run in interactive (console) mode"
, Option "F" [fileTypeS] (NoArg FileType)
, Option "p" [skipS] (NoArg $ Analysis Skip)
"skip static analysis, only parse"
, Option "s" [justStructuredS] (NoArg $ Analysis Structured)
"skip basic, just do structured analysis"
, Option "l" [logicS] (ReqArg DefaultLogic "LOGIC")
"choose logic, default is CASL"
, Option "y" [serializationS] (ReqArg DefaultSyntax "SER")
"choose different logic syntax"
, Option "L" [libdirsS] (ReqArg LibDirs "DIR")
("colon-separated list of directories"
++ crS ++ "containing HetCASL libraries")
, Option "m" [modelSparQS] (ReqArg ModelSparQ "FILE")
"lisp file for SparQ definitions"
, Option "" [counterSparQS] (ReqArg parseCounter "0-99")
"maximal number of counter examples"
, Option "c" [connectS] (ReqArg parseConnect "HOST:PORT")
("run (console) interface via connection"
++ crS ++ "to given host and port")
, Option "S" [listenS] (ReqArg parseListen "PORT")
, Option "" [whitelistS] (ReqArg Whitelist "IP4s")
$ "comma-separated list of IP4 addresses"
++ crS ++ "(missing numbers at dots are wildcards)"
, Option "" [blacklistS] (ReqArg Blacklist "IP4s")
$ "comma-separated list of IP4 addresses"
++ crS ++ "(example: 77.75.77.)"
, Option "C" [urlCatalogS] (ReqArg parseCatalog "URLS")
"comma-separated list of URL pairs: srcURL=tarURL"
, Option "i" [intypeS] (ReqArg parseInType "ITYPE")
("input file type can be one of:" ++
concatMap (\ t -> crS ++ bS ++ t)
(map show plainInTypes ++
map (++ bracket bafS) [bracket treeS ++ genTermS]))
, Option "d" ["dump"] (ReqArg Dump "STRING")
, Option "e" ["encoding"] (ReqArg parseEncoding "ENCODING")
"latin1 or utf8 (default) encoding"
, Option "" [unlitS] (NoArg Unlit) "unlit input source"
, Option "" [relposS] (NoArg RelPos) "use relative file positions"
, Option "" [fullSignS] (NoArg FullSign) "xml output full signatures"
, Option "" [fullTheoriesS] (NoArg FullTheories) "xml output full theories"
, Option "" [accessTokenS] (ReqArg AccessToken "TOKEN")
"add access token to URLs (for ontohub)"
, Option "O" [outdirS] (ReqArg OutDir "DIR")
"destination directory for output files"
, Option "o" [outtypesS] (ReqArg parseOutTypes "OTYPES")
("output file types, default nothing," ++ crS ++
cslst ++ crS ++ concatMap ( \ t -> bS ++ show t ++ crS)
++ bS ++ joinBar (map show [SigFile Fully,
++ bS ++ ppS ++ joinBar (map show prettyList) ++ crS
++ bS ++ ppS ++ joinBar (map show prettyList2) ++ crS
++ bS ++ graphE ++ joinBar (map show graphList) ++ crS
++ bS ++ dfgS ++ bracket cS ++ crS
++ bS ++ tptpS ++ bracket cS)
, Option "U" ["xupdate"] (ReqArg XUpdate "FILE")
"apply additional xupdates from file"
, Option "R" [recursiveS] (NoArg Recurse)
"output also imported libraries"
, Option "A" [applyAutomaticRuleS] (NoArg ApplyAutomatic)
"apply automatic dev-graph strategy"
, Option "N" [normalFormS] (NoArg NormalForm)
"compute normal forms (takes long)"
, Option "n" [namedSpecsS] (ReqArg (Specs . parseSIdOpts) "NSPECS")
("process specs option " ++ crS ++ cslst ++ " SIMPLE-ID")
, Option "w" [viewS] (ReqArg (Views . parseSIdOpts) "NVIEWS")
("process views option " ++ crS ++ cslst ++ " SIMPLE-ID")
, Option "t" [transS] (ReqArg parseTransOpt "TRANS")
("translation option " ++ crS ++
"is a colon-separated list" ++
crS ++ "of one or more from: SIMPLE-ID")
, Option "a" [amalgS] (ReqArg parseCASLAmalg "ANALYSIS")
("CASL amalgamability analysis options" ++ crS ++ cslst ++
crS ++ joinBar (map show caslAmalgOpts)),
Option "M" ["MMT"] (NoArg UseMMT)
-- | options that require arguments for the wep-api excluding \"translation\"
optionArgs :: [(String, String -> Flag)]
optionArgs = foldr (\ o l -> case o of
Option _ (s : _) (ReqArg f _) _ | s /= transS -> (s, f) : l
-- | command line switches for the wep-api excluding non-dev-graph related ones
optionFlags :: [(String, Flag)]
optionFlags = drop 11 $ foldr (\ o l -> case o of
Option _ (s : _) (NoArg f) _ -> (s, f) : l
-- parser functions returning Flags --
-- | 'parseVerbosity' parses a 'Verbose' Flag from user input
parseVerbosity :: Maybe String -> Flag
parseVerbosity ms = case ms of
Just s -> Verbose $ parseInt s
parseInt :: String -> Int
parseInt s = fromMaybe (hetsError $ s ++ " is not a valid INT") $ readMaybe s
parseCounter :: String -> Flag
parseCounter = CounterSparQ . parseInt
divideIntoPortHost :: String -> Bool -> (String, String) -> (String, String)
divideIntoPortHost s sw (accP, accH) = case s of
':' : ll -> divideIntoPortHost ll True (accP, accH)
c : ll -> if sw then divideIntoPortHost ll True (accP, c : accH)
else divideIntoPortHost ll False (c : accP, accH)
-- | 'parseConnect' parses a port Flag from user input
parseConnect :: String -> Flag
= let (sP, sH) = divideIntoPortHost s False ([], [])
[(i, "")] -> Connect i sH
parseListen :: String -> Flag
parseEncoding :: String -> Flag
parseEncoding s = case map toLower $ trim s of
"latin1" -> IOEncoding Latin1
"utf8" -> IOEncoding Utf8
r -> hetsError (r ++ " is not a valid encoding")
-- | intypes useable for downloads
downloadExtensions :: [String]
downloadExtensions = map ('.' :) $
++ map ((treeS ++) . show) [ATermIn BAF, ATermIn NonBAF]
-- | remove the extension from a file
rmSuffix :: FilePath -> FilePath
rmSuffix = fst . stripSuffix (envSuffix : downloadExtensions)
-- | the suffix of env files
-- | the suffix of env files
isDefLogic :: String -> HetcatsOpts -> Bool
isDefLogic s = (s ==) . defLogic
defLogicIsDMU :: HetcatsOpts -> Bool
defLogicIsDMU = isDefLogic "DMU"
getExtensions :: HetcatsOpts -> [String]
getExtensions opts = case intype opts of
| defLogicIsDMU opts -> [".xml"]
| isDefLogic "Framework" opts
-> [".elf", ".thy", ".maude", ".het"]
GuessIn -> downloadExtensions
e@(ATermIn _) -> ['.' : show e, '.' : treeS ++ show e]
getFileNames :: [String] -> FilePath -> [FilePath]
file : map (rmSuffix file ++) exts
-- | checks if a source file for the given file name exists
existsAnSource :: HetcatsOpts -> FilePath -> IO (Maybe FilePath)
existsAnSource opts file = do
let names = getFileNames (getExtensions opts) file
-- look for the first existing file
validFlags <- mapM doesFileExist names
return . fmap snd . find fst $ zip validFlags names
-- | should env be written
hasEnvOut :: HetcatsOpts -> Bool
hasEnvOut = any ( \ o -> case o of
-- | should prf be written
isPrfOut :: OutType -> Bool
-- | should prf be written
hasPrfOut :: HetcatsOpts -> Bool
hasPrfOut = any isPrfOut . outtypes
removePrfOut :: HetcatsOpts -> HetcatsOpts
opts { outtypes = filter (not . isPrfOut) $ outtypes 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 opts fp1 base2 = catchIOException False $ do
fp1_time <- getModificationTime fp1
maybe_source_file <- existsAnSource opts {intype = GuessIn} base2
maybe (return False) ( \ fp2 -> do
fp2_time <- getModificationTime fp2
return (fp1_time >= fp2_time)) maybe_source_file
parseCatalog :: String -> Flag
parseCatalog str = UrlCatalog $ map ((\ l -> case l of
_ -> hetsError (str ++ " is not a valid URL catalog"))
. splitOn '=') $ splitOn ',' str
-- | 'parseInType' parses an 'InType' Flag from user input
parseInType :: String -> Flag
parseInType = InType . parseInType1
-- | 'parseInType1' parses an 'InType' Flag from a String
parseInType1 :: String -> InType
_ -> hetsError (str ++ " is not a valid ITYPE")
{- the mere typo read instead of reads caused the runtime error:
-- 'parseOutTypes' parses an 'OutTypes' Flag from user input
parseOutTypes :: String -> Flag
parseOutTypes str = case reads $ bracket str of
_ -> hetsError (str ++ " is not a valid OTYPES")
-- | parses a comma separated list from user input
parseSIdOpts :: String -> [SIMPLE_ID]
parseSIdOpts = map mkSimpleId . splitOn ','
-- | 'parseTransOpt' parses a 'Trans' Flag from user input
parseTransOpt :: String -> Flag
parseTransOpt = Trans . map mkSimpleId . splitPaths
guess :: String -> InType -> InType
guess file itype = case itype of
GuessIn -> guessInType file
-- | 'guessInType' parses an 'InType' from the FilePath
guessInType :: FilePath -> InType
guessInType file = case fileparse downloadExtensions file of
(_, _, Just ('.' : suf)) -> parseInType1 suf
-- | 'parseCASLAmalg' parses CASL amalgamability options
parseCASLAmalg :: String -> Flag
case reads $ bracket str of
[(l, "")] -> CASLAmalg $ filter ( \ o -> case o of
" is not a valid CASL amalgamability analysis option list"
-- | 'hetcatsOpts' parses sensible HetcatsOpts from ARGV
hetcatsOpts :: [String] -> IO HetcatsOpts
let argv' = filter (not . isUni) argv
isUni = isPrefixOf "--uni"
in case getOpt Permute options argv' of
do flags <- checkFlags opts
return (foldr (flip makeOpts) defaultHetcatsOpts flags)
(_, _, errs) -> hetsIOError (concat errs)
-- | 'checkFlags' checks all parsed Flags for sanity
checkFlags :: [Flag] -> IO [Flag]
let collectFlags = collectDirs
-- collect some more here?
h = null [ () | Help <- fs]
v = null [ () | Version <- fs]
unless h $ putStr hetsUsage
unless v $ putStrLn ("version of hets: " ++ hetcats_version)
unless (v && h) exitSuccess
-- auxiliary functions: FileSystem interaction --
-- | check if infile is uri
checkUri :: FilePath -> Bool
checkUri file = "://" `isPrefixOf` dropWhile isAlpha file
-- (http://, https://, ftp://, file://, etc.)
-- | 'checkOutDirs' checks a list of OutDir for sanity
checkOutDirs :: [Flag] -> IO [Flag]
"Only one output directory may be specified on the command line"
-- | 'checkLibDirs' checks a list of LibDir for sanity
checkLibDirs :: [Flag] -> IO [Flag]
s <- getEnvDef "HETS_LIB" ""
if null s then return [] else do
[LibDirs f] -> mapM_ checkLibDir (joinHttpLibPath $ splitPaths f)
"Only one library path may be specified on the command line"
joinHttpLibPath :: [String] -> [String]
joinHttpLibPath l = case l of
p : f : r | elem p ["http", "https"] -> (p ++ ':' : f) : joinHttpLibPath r
f : r -> f : joinHttpLibPath r
-- | 'checkLibDir' checks a single LibDir for sanity
checkLibDir :: FilePath -> IO ()
exists <- if checkUri file then return True else doesDirectoryExist file
unless exists . hetsIOError $ "Not a valid library directory: " ++ file
-- | 'checkOutDir' checks a single OutDir for sanity
checkOutDir :: Flag -> IO ()
checkOutDir (OutDir file) = do
exists <- doesDirectoryExist file
unless exists . hetsIOError $ "Not a valid output directory: " ++ file
checkOutDir _ = return ()
-- auxiliary functions: collect flags --
collectDirs :: [Flag] -> IO [Flag]
let (ods, fs1) = partition isOutDir fs
(lds, fs2) = partition isLibDir fs1
isOutDir (OutDir _) = True
isLibDir (LibDirs _) = True
return $ ods' ++ lds' ++ fs2
collectVerbosity :: [Flag] -> [Flag]
let (v, fs') = foldr (\ f (n, rs) -> case f of
Verbose x -> (if n < 0 then x else n + x, rs)
_ -> (n, f : rs)) (-1, []) fs
in if v < 0 || not (null [() | Quiet <- fs']) then fs' else Verbose v : fs'
collectOutTypes :: [Flag] -> [Flag]
let (ots, fs') = foldr (\ f (os, rs) -> case f of
OutTypes ot -> (ot ++ os, rs)
_ -> (os, f : rs)) ([], []) fs
in if null ots then fs' else OutTypes ots : fs'
collectSpecOpts :: [Flag] -> [Flag]
let (specs, fs') = foldr (\ f (os, rs) -> case f of
Specs ot -> (ot ++ os, rs)
_ -> (os, f : rs)) ([], []) fs
in if null specs then fs' else Specs specs : fs'
-- auxiliary functions: error messages --
-- | only print the error (and no usage info)
hetsError = error . ("command line usage error (see 'hets -h')\n" ++)
-- | print error and usage and exit with code 2
hetsIOError :: String -> IO a
-- | 'hetsUsage' generates usage information for the commandline
hetsUsage = let header = "Usage: hets [OPTION ...] [FILE ...] [+RTS -?]"
in usageInfo header options
{- | 'putIfVerbose' prints a given String to StdOut when the given HetcatsOpts'
Verbosity exceeds the given level -}
putIfVerbose :: HetcatsOpts -> Int -> String -> IO ()
putIfVerbose opts level =
when (outputToStdout opts) . when (verbose opts >= level) . putStrLn
doDump :: HetcatsOpts -> String -> IO () -> IO ()
doDump opts str = when (elem str $ dumpOpts opts)
-- | show diagnostic messages (see
Result.hs), according to verbosity level
showDiags :: HetcatsOpts -> [Diagnosis] -> IO ()
runResultT (showDiags1 opts $ liftR $ Result ds Nothing) >> return ()
-- | show diagnostic messages (see
Result.hs), according to verbosity level
showDiags1 :: HetcatsOpts -> ResultT IO a -> ResultT IO a
if outputToStdout opts then do
Result ds res' <- lift $ runResultT res
lift $ printDiags (verbose opts) ds
Just res'' -> return res''
Nothing -> liftR $ Result [] Nothing