5784N/ADescription : Datatypes and functions for options that hets understands.
5784N/ACopyright : (c) Martin Kuehl, Christian Maeder, Uni Bremen 2002-2006
5784N/AMaintainer : Christian.Maeder@dfki.de
5784N/ADatatypes for options that hets understands.
5784N/A Useful functions to parse and check user-provided values.
5784N/A-- | short version without date for ATC files
5784N/AhetsVersion = takeWhile (/= ',') hetcats_version
5784N/A-- use the same strings for parsing and printing!
5784N/AverboseS, intypeS, outtypesS, skipS, structS, transS, viewS,
5784N/A guiS, libdirsS, outdirS, amalgS, specS, recursiveS,
5784N/A interactiveS, modelSparQS, connectS, xmlS, listenS,
5784N/A applyAutomaticRuleS, normalFormS, unlitS :: String
5784N/AinteractiveS = "interactive"
5784N/AapplyAutomaticRuleS = "apply-automatic-rule"
5784N/ArelposS = "relative-positions"
5784N/AgenTermS, treeS, bafS :: String
5784N/AgraphS, ppS, envS, deltaS, prfS, omdocS, hsS, experimentalS :: String
5784N/AshowOpt s = if null s then "" else " --" ++ s
5784N/AshowEqOpt :: String -> String -> String
5784N/AshowEqOpt k s = if null s then "" else showOpt k ++ "=" ++ s
5784N/A-- | 'HetcatsOpts' is a record of all options received from the command line
5784N/Adata HetcatsOpts = HcOpt -- for comments see usage info
5784N/A , infiles :: [FilePath] -- ^ files to be read
5784N/A , specNames :: [SIMPLE_ID] -- ^ specs to be processed
5784N/A , transNames :: [SIMPLE_ID] -- ^ comorphism to be processed
5784N/A , viewNames :: [SIMPLE_ID] -- ^ views to be processed
5784N/A , outputToStdout :: Bool -- ^ send messages to stdout?
5784N/A , caslAmalg :: [CASLAmalgOpt]
5784N/A , computeNormalForm :: Bool
5784N/A -- | use the library name in positions to avoid differences after uploads
5784N/A{- | 'defaultHetcatsOpts' defines the default HetcatsOpts, which are used as
5784N/Abasic values when the user specifies nothing else -}
5784N/AdefaultHetcatsOpts :: HetcatsOpts
5784N/A , outtypes = [] -- no default
5784N/A , computeNormalForm = False
5784N/Ainstance Show HetcatsOpts where
5784N/A show opts = showEqOpt verboseS (show $ verbose opts)
5784N/A ++ (if interactive opts then showOpt interactiveS else "")
5784N/A ++ showEqOpt libdirsS (intercalate ":" $ libdirs opts)
5784N/A ++ (if modelSparQ opts /= "" then showEqOpt modelSparQS (modelSparQ opts)
5784N/A ++ (if xmlFlag opts then showOpt xmlS else "")
5784N/A ++ (if connectP opts /= -1 then showOpt connectS else "")
5784N/A ++ (if listen opts /= -1 then showOpt listenS else "")
5784N/A ++ concatMap (showEqOpt "dump") (dumpOpts opts)
5784N/A Utf8 -> showEqOpt "encoding" "utf8"
5784N/A ++ (if unlit opts then showOpt unlitS else "")
5784N/A ++ (if useLibPos opts then showOpt relposS else "")
5784N/A ++ showEqOpt intypeS (show $ intype opts)
5784N/A ++ showEqOpt outdirS (outdir opts)
5784N/A ++ showEqOpt outtypesS (intercalate "," $ map show $ outtypes opts)
5784N/A ++ (if recurse opts then showOpt recursiveS else "")
5784N/A ++ (if applyAutomatic opts then showOpt applyAutomaticRuleS else "")
5784N/A ++ (if computeNormalForm opts then showOpt normalFormS else "")
5784N/A ++ showEqOpt specS (intercalate "," $ map show $ specNames opts)
5784N/A ++ showEqOpt transS (intercalate ":" $ map show $ transNames opts)
5784N/A ++ showEqOpt viewS (intercalate "," $ map show $ viewNames opts)
5784N/A ++ showEqOpt amalgS (tail $ init $ show $
5784N/A ++ " " ++ unwords (infiles opts)
5784N/A-- | every 'Flag' describes an option (see usage info)
5784N/A-- | 'makeOpts' includes a parsed Flag in a set of HetcatsOpts
5784N/AmakeOpts :: HetcatsOpts -> Flag -> HetcatsOpts
5784N/AmakeOpts opts flg = case flg of
5784N/A Interactive -> opts { interactive = True }
5784N/A XML -> opts { xmlFlag = True }
5784N/A Listen x -> opts { listen = x }
5784N/A Connect x y -> opts { connectP = x, connectH = y }
5784N/A Analysis x -> opts { analysis = x }
5784N/A Gui x -> opts { guiType = x }
5784N/A InType x -> opts { intype = x }
5784N/A LibDirs x -> opts { libdirs = splitOn ':' x }
5784N/A ModelSparQ x -> opts { modelSparQ = x }
5784N/A OutDir x -> opts { outdir = x }
5784N/A OutTypes x -> opts { outtypes = x }
5784N/A XUpdate x -> opts { xupdate = x }
5784N/A Recurse -> opts { recurse = True }
5784N/A ApplyAutomatic -> opts { applyAutomatic = True }
5784N/A NormalForm -> opts { computeNormalForm = True }
5784N/A Specs x -> opts { specNames = x }
5784N/A Trans x -> opts { transNames = x }
5784N/A Views x -> opts { viewNames = x }
5784N/A Verbose x -> opts { verbose = x }
5784N/A DefaultLogic x -> opts { defLogic = x }
5784N/A CASLAmalg x -> opts { caslAmalg = x }
5784N/A Quiet -> opts { verbose = 0 }
5784N/A Uncolored -> opts { uncolored = True }
5784N/A Dump s -> opts { dumpOpts = s : dumpOpts opts }
5784N/A IOEncoding e -> opts { ioEncoding = e }
5784N/A Serve -> opts { serve = True }
5784N/A Unlit -> opts { unlit = True }
5784N/A RelPos -> opts { useLibPos = True }
5784N/A-- | 'AnaType' describes the type of analysis to be performed
5784N/Adata AnaType = Basic | Structured | Skip
5784N/A Structured -> showOpt structS
5784N/A-- | 'GuiType' determines if we want the GUI shown
5784N/Adata GuiType = UseGui | NoGui
5784N/A-- | 'InType' describes the type of input the infile contains
5784N/A | ExperimentalIn -- ^ for testing new functionality
5784N/A | CommonLogic2In -- ^ "clif"
5784N/A ATermIn at -> genTermS ++ show at
5784N/A-- maybe this optional tree prefix can be omitted
5784N/A readsPrec _ = readShowAux $ map ( \ i -> (show i, i))
5784N/A ++ [(treeS ++ genTermS ++ show at, ATermIn at)
5784N/A-- | 'ATType' describes distinct types of ATerms
5784N/A [ CASLIn, HetCASLIn, OWLIn, HaskellIn, ExperimentalIn, MaudeIn, TwelfIn
5784N/A , HolLightIn, PrfIn, OmdocIn, ProofCommand, CommonLogicIn, CommonLogic2In
5784N/A , DgXml, FreeCADIn, OWL2In, RDFIn ]
5784N/AaInTypes = [ ATermIn x | x <- [BAF, NonBAF] ]
5784N/Adata SPFType = ConsistencyCheck | ProveTheory
5784N/AspfTypes = [ConsistencyCheck, ProveTheory]
5784N/A-- | 'OutType' describes the type of outputs that we want to generate
5784N/A | XmlOut -- ^ development graph xml output
5784N/A | ExperimentalOut -- ^ for testing new functionality
5784N/A | ThyFile -- ^ isabelle theory file
5784N/A | DfgFile SPFType -- ^ SPASS input file
5784N/A | SigFile Delta -- ^ signature as text
5784N/A | TheoryFile Delta -- ^ signature with sentences as text
5784N/A PrettyOut p -> ppS ++ show p
5784N/A GraphOut f -> graphS ++ show f
5784N/A ExperimentalOut -> experimentalS
5784N/A DfgFile t -> dfgS ++ show t
5784N/A TPTPFile t -> tptpS ++ show t
5784N/A SigFile d -> "sig" ++ show d
5784N/A TheoryFile d -> "th" ++ show d
5784N/AplainOutTypeList :: [OutType]
5784N/A [Prf, EnvOut, OWLOut, CLIFOut, OmdocOut, XmlOut, ExperimentalOut,
5784N/A HaskellOut, ThyFile, ComptableXml, FreeCADOut, RDFOut]
5784N/AoutTypeList = let dl = [Delta, Fully] in
5784N/A ++ [ PrettyOut p | p <- prettyList ]
5784N/A ++ [ TheoryFile d | d <- dl ]
5784N/A ++ [ DfgFile x | x <- spfTypes]
5784N/A ++ [ TPTPFile x | x <- spfTypes]
5784N/A ++ [ GraphOut f | f <- graphList ]
5784N/A readsPrec _ = readShowAux $ map ( \ o -> (show o, o)) outTypeList
5784N/A{- | 'PrettyType' describes the type of output we want the pretty-printer
5784N/Adata PrettyType = PrettyAscii | PrettyLatex | PrettyXml | PrettyHtml
5784N/Ainstance Show PrettyType where
5784N/AprettyList = [PrettyAscii, PrettyLatex, PrettyXml, PrettyHtml]
5784N/A-- | 'GraphType' describes the type of Graph that we want generated
5784N/A Dot Bool -- ^ True means show internal node labels
5784N/Ainstance Show GraphType where
5784N/A Dot si -> (if si then "exp." else "") ++ "dot"
5784N/AgraphList = [Dot True, Dot False]
5784N/A{- | 'options' describes all available options and is used to generate usage
5784N/A listS = "is a comma-separated list"
5784N/A ++ crS ++ "of one or more from:"
5784N/A joinBar l = "(" ++ intercalate "|" l ++ ")" in
5784N/A [ Option "v" [verboseS] (OptArg parseVerbosity "0-5")
5784N/A "verbosity, default is -v1"
5784N/A , Option "q" ["quiet"] (NoArg Quiet)
5784N/A "same as -v0, no output to stdout"
5784N/A , Option "V" ["version"] (NoArg Version)
5784N/A "print version number and exit"
5784N/A , Option "h" ["help", "usage"] (NoArg Help)
5784N/A "print usage information and exit"
5784N/A , Option "g" [guiS] (NoArg (Gui UseGui))
5784N/A , Option "u" ["uncolored"] (NoArg Uncolored)
5784N/A "no colors in shown graphs"
5784N/A , Option "I" [interactiveS] (NoArg Interactive)
5784N/A "run in interactive (console) mode"
5784N/A , Option "p" [skipS] (NoArg $ Analysis Skip)
5784N/A "skip static analysis, only parse"
5784N/A , Option "s" [structS] (NoArg $ Analysis Structured)
5784N/A "skip basic, just do structured analysis"
5784N/A , Option "l" ["logic"] (ReqArg DefaultLogic "LOGIC")
5784N/A "choose logic, default is CASL"
5784N/A , Option "L" [libdirsS] (ReqArg LibDirs "DIR")
5784N/A ("colon-separated list of directories"
5784N/A ++ crS ++ "containing HetCASL libraries")
5784N/A , Option "m" [modelSparQS] (ReqArg ModelSparQ "FILE")
5784N/A "lisp file for SparQ definitions"
5784N/A , Option "x" [xmlS] (NoArg XML)
5784N/A "use xml packets to communicate"
5784N/A , Option "X" ["server"] (NoArg Serve)
5784N/A , Option "c" [connectS] (ReqArg parseConnect "HOST:PORT")
5784N/A ("run (console) interface via connection"
5784N/A ++ crS ++ "to given host and port")
5784N/A , Option "S" [listenS] (ReqArg parseListen "PORT")
5784N/A "run interface by listening to the port"
5784N/A , Option "i" [intypeS] (ReqArg parseInType "ITYPE")
5784N/A ("input file type can be one of:" ++
5784N/A concatMap (\ t -> crS ++ bS ++ t)
5784N/A map (++ bracket bafS) [bracket treeS ++ genTermS]))
5784N/A , Option "d" ["dump"] (ReqArg Dump "STRING")
5784N/A , Option "e" ["encoding"] (ReqArg parseEncoding "ENCODING")
5784N/A "latin1 (default) or utf8 encoding"
5784N/A , Option "" [unlitS] (NoArg Unlit) "unlit input source"
5784N/A , Option "" [relposS] (NoArg RelPos) "use relative file positions"
5784N/A , Option "O" [outdirS] (ReqArg OutDir "DIR")
5784N/A "destination directory for output files"
5784N/A , Option "o" [outtypesS] (ReqArg parseOutTypes "OTYPES")
5784N/A ("output file types, default nothing," ++ crS ++
5784N/A listS ++ crS ++ concatMap ( \ t -> bS ++ show t ++ crS)
5784N/A ++ bS ++ joinBar (map show [SigFile Fully,
5784N/A ++ bS ++ ppS ++ joinBar (map show prettyList) ++ crS
5784N/A ++ bS ++ graphS ++ joinBar (map show graphList) ++ crS
5784N/A ++ bS ++ dfgS ++ bracket cS ++ crS
5784N/A ++ bS ++ tptpS ++ bracket cS)
5784N/A , Option "U" ["xupdate"] (ReqArg XUpdate "FILE")
5784N/A "apply additional xupdates from file"
5784N/A , Option "R" [recursiveS] (NoArg Recurse)
5784N/A "output also imported libraries"
5784N/A , Option "A" [applyAutomaticRuleS] (NoArg ApplyAutomatic)
5784N/A "apply automatic dev-graph strategy"
5784N/A , Option "N" [normalFormS] (NoArg NormalForm)
5784N/A "compute normal forms (takes long)"
5784N/A , Option "n" [specS] (ReqArg (Specs . parseSIdOpts) "NSPECS")
5784N/A ("process specs option " ++ crS ++ listS ++ " SIMPLE-ID")
5784N/A , Option "w" [viewS] (ReqArg (Views . parseSIdOpts) "NVIEWS")
5784N/A ("process views option " ++ crS ++ listS ++ " SIMPLE-ID")
5784N/A , Option "t" [transS] (ReqArg parseTransOpt "TRANS")
5784N/A ("translation option " ++ crS ++
5784N/A "is a colon-separated list" ++
5784N/A crS ++ "of one or more from: SIMPLE-ID")
5784N/A , Option "a" [amalgS] (ReqArg parseCASLAmalg "ANALYSIS")
5784N/A ("CASL amalgamability analysis options" ++ crS ++ listS ++
5784N/A crS ++ joinBar (map show caslAmalgOpts)) ]
5784N/A-- parser functions returning Flags --
5784N/A-- | 'parseVerbosity' parses a 'Verbose' Flag from user input
5784N/AparseVerbosity :: Maybe String -> Flag
5784N/AparseVerbosity ms = case ms of
5784N/A _ -> hetsError (s ++ " is not a valid INT")
5784N/AdivideIntoPortHost :: String -> Bool -> (String, String) -> (String, String)
5784N/AdivideIntoPortHost s sw (accP, accH) = case s of
5784N/A ':' : ll -> divideIntoPortHost ll True (accP, accH)
5784N/A c : ll -> if sw then divideIntoPortHost ll True (accP, c : accH)
5784N/A else divideIntoPortHost ll False (c : accP, accH)
5784N/A-- | 'parseConnect' parses a port Flag from user input
5784N/AparseConnect :: String -> Flag
5784N/A = let (sP, sH) = divideIntoPortHost s False ([], [])
5784N/AparseListen :: String -> Flag
5784N/AparseEncoding :: String -> Flag
5784N/AparseEncoding s = case map toLower $ trim s of
5784N/A "latin1" -> IOEncoding Latin1
5784N/A r -> hetsError (r ++ " is not a valid encoding")
5784N/A-- | intypes useable for downloads
5784N/AdownloadExtensions :: [String]
5784N/AdownloadExtensions = map ('.' :) $
5784N/A ++ map ((treeS ++) . show) [ATermIn BAF, ATermIn NonBAF]
5784N/A-- | remove the extension from a file
5784N/ArmSuffix :: FilePath -> FilePath
5784N/ArmSuffix = fst . stripSuffix (envSuffix : downloadExtensions)
5784N/A-- | the suffix of env files
5784N/A-- | the suffix of env files
5784N/AisDefLogic :: String -> HetcatsOpts -> Bool
5784N/AisDefLogic s = (s ==) . defLogic
5784N/AdefLogicIsDMU :: HetcatsOpts -> Bool
5784N/AdefLogicIsDMU = isDefLogic "DMU"
5784N/Achecks if a source file for the given file name exists -}
5784N/AexistsAnSource :: HetcatsOpts -> FilePath -> IO (Maybe FilePath)
5784N/AexistsAnSource opts file = do
5784N/A | defLogicIsDMU opts -> [".xml"]
5784N/A | isDefLogic "Framework" opts
5784N/A -> [".elf", ".thy", ".maude", ".het"]
5784N/A GuessIn -> downloadExtensions
5784N/A e@(ATermIn _) -> ['.' : show e, '.' : treeS ++ show e]
5784N/A names = file : map (base ++) (exts ++ [envSuffix])
5784N/A -- look for the first existing file
5784N/A validFlags <- mapM doesFileExist names
5784N/A return . fmap snd . find fst $ zip validFlags names
5784N/AhasEnvOut :: HetcatsOpts -> Bool
5784N/AhasEnvOut = any ( \ o -> case o of
5784N/AhasPrfOut :: HetcatsOpts -> Bool
5784N/AhasPrfOut = any isPrfOut . outtypes
5784N/AremovePrfOut :: HetcatsOpts -> HetcatsOpts
5784N/A opts { outtypes = filter (not . isPrfOut) $ outtypes opts }
5784N/Agets two Paths and checks if the first file is not older than the
5784N/Asecond one and should return True for two identical files -}
5784N/AcheckRecentEnv :: HetcatsOpts -> FilePath -> FilePath -> IO Bool
5784N/AcheckRecentEnv opts fp1 base2 = catch (do
5784N/A fp1_time <- getModificationTime fp1
5784N/A maybe_source_file <- existsAnSource opts {intype = GuessIn} base2
5784N/A maybe (return False) ( \ fp2 -> do
5784N/A fp2_time <- getModificationTime fp2
5784N/A return (fp1_time >= fp2_time)) maybe_source_file
5784N/A-- | 'parseInType' parses an 'InType' Flag from user input
5784N/AparseInType :: String -> Flag
5784N/AparseInType = InType . parseInType1
5784N/A-- | 'parseInType1' parses an 'InType' Flag from a String
5784N/AparseInType1 :: String -> InType
5784N/A _ -> hetsError (str ++ " is not a valid ITYPE")
5784N/A {- the mere typo read instead of reads caused the runtime error:
5784N/A-- 'parseOutTypes' parses an 'OutTypes' Flag from user input
5784N/AparseOutTypes :: String -> Flag
5784N/AparseOutTypes str = case reads $ bracket str of
5784N/A _ -> hetsError (str ++ " is not a valid OTYPES")
5784N/A-- | parses a comma separated list from user input
5784N/AparseSIdOpts :: String -> [SIMPLE_ID]
5784N/AparseSIdOpts = map mkSimpleId . splitOn ','
5784N/A-- | 'parseTransOpt' parses a 'Trans' Flag from user input
5784N/AparseTransOpt :: String -> Flag
5784N/AparseTransOpt = Trans . map mkSimpleId . splitOn ':'
5784N/Aguess :: String -> InType -> InType
5784N/Aguess file itype = case itype of
5784N/A GuessIn -> guessInType file
5784N/A-- | 'guessInType' parses an 'InType' from the FilePath
5784N/AguessInType :: FilePath -> InType
5784N/AguessInType file = case fileparse downloadExtensions file of
5784N/A (_, _, Just ('.' : suf)) -> parseInType1 suf
5784N/A-- | 'parseCASLAmalg' parses CASL amalgamability options
5784N/AparseCASLAmalg :: String -> Flag
5784N/A case reads $ bracket str of
5784N/A [(l, "")] -> CASLAmalg $ filter ( \ o -> case o of
5784N/A " is not a valid CASL amalgamability analysis option list"
5784N/A-- | 'hetcatsOpts' parses sensible HetcatsOpts from ARGV
5784N/AhetcatsOpts :: [String] -> IO HetcatsOpts
5784N/A let argv' = filter (not . isUni) argv
5784N/A in case getOpt Permute options argv' of
5784N/A do flags <- checkFlags opts
5784N/A infs <- checkInFiles non_opts
5784N/A let hcOpts = (foldr (flip makeOpts) defaultHetcatsOpts flags)
5784N/A if null infs && not (interactive hcOpts) && not (serve hcOpts)
5784N/A && connectP hcOpts < 0 && listen hcOpts < 0
5784N/A then hetsError "missing input files"
5784N/A (_, _, errs) -> hetsError (concat errs)
5784N/A-- | 'checkFlags' checks all parsed Flags for sanity
5784N/AcheckFlags :: [Flag] -> IO [Flag]
5784N/A let collectFlags = collectDirs
5784N/A if not $ null [ () | Help <- fs]
5784N/A else return [] -- fall through
5784N/A if not $ null [ () | Version <- fs]
5784N/A putStrLn ("version of hets: " ++ hetcats_version)
5784N/A else return [] -- fall through
5784N/A-- | 'checkInFiles' checks all given input files for sanity
5784N/AcheckInFiles :: [String] -> IO [FilePath]
5784N/A let ifs = filter (not . checkUri) fs
5784N/A efs = filter hasExtension ifs
5784N/A hasExtension f = any (`isSuffixOf` f) downloadExtensions
5784N/A bs <- mapM doesFileExist efs
5784N/A else hetsError $ "invalid input files: " ++
5784N/A unwords (map snd . filter (not . fst) $ zip bs efs)
5784N/A-- auxiliary functions: FileSystem interaction --
5784N/AcheckUri :: FilePath -> Bool
5784N/AcheckUri file = let (_, t) = span (/= ':') file in
5784N/A else let (_ : c2 : c3 : _) = t in c2 == '/' && c3 == '/'
5784N/A -- (http://, https://, ftp://, file://, etc.)
5784N/A-- | 'checkOutDirs' checks a list of OutDir for sanity
5784N/AcheckOutDirs :: [Flag] -> IO [Flag]
5784N/A "Only one output directory may be specified on the command line"
5784N/A-- | 'checkLibDirs' checks a list of LibDir for sanity
5784N/AcheckLibDirs :: [Flag] -> IO [Flag]
5784N/A s <- getEnvDef "HETS_LIB" ""
5784N/A if null s then return [] else do
5784N/A [LibDirs f] -> mapM_ checkLibDir (splitOn ':' f) >> return fs
5784N/A "Only one library path may be specified on the command line"
5784N/A-- | 'checkLibDir' checks a single LibDir for sanity
5784N/AcheckLibDir :: FilePath -> IO ()
5784N/A exists <- doesDirectoryExist file
5784N/A unless exists . hetsError $ "Not a valid library directory: " ++ file
5784N/A-- | 'checkOutDir' checks a single OutDir for sanity
5784N/AcheckOutDir :: Flag -> IO ()
5784N/AcheckOutDir (OutDir file) = do
5784N/A exists <- doesDirectoryExist file
5784N/A unless exists . hetsError $ "Not a valid output directory: " ++ file
5784N/A-- auxiliary functions: collect flags --
5784N/AcollectDirs :: [Flag] -> IO [Flag]
5784N/A let (ods, fs1) = partition isOutDir fs
5784N/A (lds, fs2) = partition isLibDir fs1
5784N/A isLibDir (LibDirs _) = True
5784N/A return $ ods' ++ lds' ++ fs2
5784N/AcollectVerbosity :: [Flag] -> [Flag]
5784N/A let (v, fs') = foldr (\ f (n, rs) -> case f of
5784N/A Verbose x -> (if n < 0 then x else n + x, rs)
5784N/A _ -> (n, f : rs)) (-1, []) fs
5784N/A in if v < 0 || not (null [() | Quiet <- fs']) then fs' else Verbose v : fs'
5784N/AcollectOutTypes :: [Flag] -> [Flag]
5784N/A let (ots, fs') = foldr (\ f (os, rs) -> case f of
5784N/A OutTypes ot -> (ot ++ os, rs)
5784N/A _ -> (os, f : rs)) ([], []) fs
5784N/A in if null ots then fs' else OutTypes ots : fs'
5784N/AcollectSpecOpts :: [Flag] -> [Flag]
5784N/A let (specs, fs') = foldr (\ f (os, rs) -> case f of
5784N/A _ -> (os, f : rs)) ([], []) fs
5784N/A in if null specs then fs' else Specs specs : fs'
5784N/A-- auxiliary functions: error messages --
5784N/A{- | 'hetsError' is a generic Error messaging function that prints the Error
5784N/Aand usage information, if the user caused the Error -}
5784N/AhetsError = error . (++ '\n' : hetsUsage)
5784N/A-- | 'hetsUsage' generates usage information for the commandline
5784N/AhetsUsage = let header = "Usage: hets [OPTION...] file ... file [+RTS -?]"
5784N/A in usageInfo header options
5784N/A{- | 'putIfVerbose' prints a given String to StdOut when the given HetcatsOpts'
5784N/AVerbosity exceeds the given level -}
5784N/AputIfVerbose :: HetcatsOpts -> Int -> String -> IO ()
5784N/A when (outputToStdout opts) . when (verbose opts >= level) . putStrLn
5784N/AdoDump :: HetcatsOpts -> String -> IO () -> IO ()
5784N/AdoDump opts str = when (elem str $ dumpOpts opts)
5784N/A-- | show diagnostic messages (see
Result.hs), according to verbosity level
5784N/AshowDiags :: HetcatsOpts -> [Diagnosis] -> IO ()
5784N/A runResultT (showDiags1 opts $ liftR $ Result ds Nothing) >> return ()
5784N/A-- | show diagnostic messages (see
Result.hs), according to verbosity level
5784N/AshowDiags1 :: HetcatsOpts -> ResultT IO a -> ResultT IO a
5784N/A if outputToStdout opts then do
5784N/A Result ds res' <- lift $ runResultT res
5784N/A lift $ printDiags (verbose opts) ds
5784N/A Nothing -> liftR $ Result [] Nothing