content: {-# 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 opts fname = case mapMaybe
      (\ (a, b) -> fmap (b ++) $ stripPrefix a fname)
      $ urlCatalog opts of
    m : _ -> m
    _ -> fname
  
  bracket :: String -> String
  bracket s = "[" ++ s ++ "]"
  
  -- 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 = "modelSparQ"
  counterSparQS = "counterSparQ"
  verboseS = "verbose"
  intypeS = "input-type"
  outtypesS = "output-types"
  skipS = "just-parse"
  justStructuredS = "just-structured"
  guiS = "gui"
  libdirsS = "hets-libdirs"
  outdirS = "output-dir"
  amalgS = "casl-amalg"
  namedSpecsS = "named-specs"
  transS = "translation"
  lossyTransS = "lossy"
  recursiveS = "recursive"
  interactiveS = "interactive"
  connectS = "connect"
  xmlS = "xml"
  dbS = "db"
  listenS = "listen"
  pidFileS = "pidfile"
  applyAutomaticRuleS = "apply-automatic-rule"
  normalFormS = "normal-form"
  unlitS = "unlit"
  
  urlCatalogS :: String
  urlCatalogS = "url-catalog"
  
  relposS :: String
  relposS = "relative-positions"
  
  fullSignS :: String
  fullSignS = "full-signatures"
  
  printASTS :: String
  printASTS = "print-AST"
  
  fullTheoriesS :: String
  fullTheoriesS = "full-theories"
  
  logicGraphS :: String
  logicGraphS = "logic-graph"
  
  logicListS :: String
  logicListS = "logic-list"
  
  fileTypeS :: String
  fileTypeS = "file-type"
  
  blacklistS :: String
  blacklistS = "blacklist"
  
  whitelistS :: String
  whitelistS = "whitelist"
  
  accessTokenS :: String
  accessTokenS = "access-token"
  
  httpRequestHeaderS :: String
  httpRequestHeaderS = "http-request-header"
  
  genTermS, treeS, bafS :: String
  genTermS = "gen_trm"
  treeS = "tree."
  bafS = ".baf"
  
  graphE, ppS, envS, deltaS, prfS, omdocS, hsS, experimentalS :: String
  graphE = "graph."
  ppS = "pp."
  envS = "env"
  deltaS = ".delta"
  prfS = "prf"
  omdocS = "omdoc"
  hsS = "hs"
  experimentalS = "exp"
  
  tptpS, dfgS, cS :: String
  tptpS = "tptp"
  dfgS = "dfg"
  cS = ".c"
  
  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
  
  -- main Datatypes --
  
  -- | 'HetcatsOpts' is a record of all options received from the command line
  data HetcatsOpts = HcOpt     -- for comments see usage info
    { analysis :: AnaType
    , guiType :: GuiType
    , urlCatalog :: [(String, String)]
    , infiles :: [FilePath] -- ^ files to be read
    , specNames :: [SIMPLE_ID] -- ^ specs to be processed
    , transNames :: [SIMPLE_ID] -- ^ comorphism to be processed
    , lossyTrans :: Bool                
    , viewNames :: [SIMPLE_ID] -- ^ views to be processed
    , intype :: InType
    , libdirs :: [FilePath]
    , modelSparQ :: FilePath
    , counterSparQ :: Int
    , outdir :: FilePath
    , outtypes :: [OutType]
    , databaseDoMigrate :: Bool
    , databaseOutputFile :: FilePath
    , databaseConfigFile :: FilePath
    , databaseSubConfigKey :: String
    , databaseFileVersionId :: String
    , databaseReanalyze :: Bool
    , databaseConfig :: DBConfig.DBConfig
    , databaseContext :: DBConfig.DBContext
    , xupdate :: FilePath
    , recurse :: Bool
    , verbose :: Int
    , defLogic :: String
    , defSyntax :: String
    , outputToStdout :: Bool    -- ^ send messages to stdout?
    , caslAmalg :: [CASLAmalgOpt]
    , interactive :: Bool
    , connectP :: Int
    , connectH :: String
    , uncolored :: Bool
    , xmlFlag :: Bool
    , applyAutomatic :: Bool
    , computeNormalForm :: Bool
    , dumpOpts :: [String]
    , disableCertificateVerification :: Bool
    , ioEncoding :: Enc
      -- | use the library name in positions to avoid differences after uploads
    , useLibPos :: Bool
    , unlit :: Bool
    , serve :: Bool
    , listen :: Int
    , pidFile :: FilePath
    , whitelist :: [[String]]
    , blacklist :: [[String]]
    , runMMT :: Bool
    , fullTheories :: Bool
    , outputLogicList :: Bool
    , outputLogicGraph :: Bool
    , fileType :: Bool
    , accessToken :: String
    , httpRequestHeaders :: [String]
    , fullSign :: Bool
    , printAST :: Bool }
  
  {- | 'defaultHetcatsOpts' defines the default HetcatsOpts, which are used as
  basic values when the user specifies nothing else -}
  defaultHetcatsOpts :: HetcatsOpts
  defaultHetcatsOpts = HcOpt
    { analysis = Basic
    , guiType = NoGui
    , urlCatalog = []
    , infiles = []
    , specNames = []
    , transNames = []
    , lossyTrans = False  
    , viewNames = []
    , intype = GuessIn
    , libdirs = []
    , modelSparQ = ""
    , counterSparQ = 3
    , outdir = ""
    , outtypes = [] -- no default
    , databaseDoMigrate = True
    , databaseOutputFile = ""
    , databaseConfigFile = ""
    , databaseSubConfigKey = ""
    , databaseFileVersionId = ""
    , databaseReanalyze = False
    , databaseConfig = DBConfig.emptyDBConfig
    , databaseContext = DBConfig.emptyDBContext
    , xupdate = ""
    , recurse = False
    , defLogic = "CASL"
    , defSyntax = ""
    , verbose = 1
    , outputToStdout = True
    , caslAmalg = [Cell]
    , interactive = False
    , connectP = -1
    , connectH = ""
    , uncolored = False
    , xmlFlag = False
    , applyAutomatic = False
    , computeNormalForm = False
    , dumpOpts = []
    , disableCertificateVerification = False
    , ioEncoding = Utf8
    , useLibPos = False
    , unlit = False
    , serve = False
    , listen = -1
    , pidFile = ""
    , whitelist = []
    , blacklist = []
    , runMMT = False
    , fullTheories = False
    , outputLogicList = False
    , outputLogicGraph = False
    , fileType = False
    , accessToken = ""
    , httpRequestHeaders = []
    , fullSign = False
    , printAST = False }
  
  instance Show HetcatsOpts where
    show opts =
      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
      in
      showEqOpt verboseS (show $ verbose opts)
      ++ show (guiType opts)
      ++ showFlag outputLogicList logicListS
      ++ showFlag outputLogicGraph logicGraphS
      ++ showFlag fileType fileTypeS
      ++ showFlag interactive interactiveS
      ++ show (analysis opts)
      ++ case defLogic opts of
            s | s /= defLogic defaultHetcatsOpts -> showEqOpt logicS s
            _ -> ""
      ++ case defSyntax opts of
            s | s /= defSyntax defaultHetcatsOpts -> showEqOpt serializationS s
            _ -> ""
      ++ case httpRequestHeaders opts of
            [] -> ""
            headers -> concatMap (showEqOpt httpRequestHeaderS . show) headers
      ++ 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 xmlFlag xmlS
      ++ showFlag ((/= -1) . connectP) connectS
      ++ showFlag ((/= -1) . listen) listenS
      ++ showEqOpt pidFileS (pidFile opts)
      ++ showIPLists whitelist whitelistS
      ++ showIPLists blacklist blacklistS
      ++ concatMap (showEqOpt "dump") (dumpOpts opts)
      ++ showEqOpt "encoding" (map toLower $ show $ ioEncoding opts)
      ++ showFlag unlit unlitS
      ++ showFlag useLibPos relposS
      ++ showFlag fullSign fullSignS
      ++ showFlag printAST printASTS
      ++ 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)
      ++ showFlag lossyTrans lossyTransS
      ++ showEqOpt viewS (intercalate "," $ map show $ viewNames opts)
      ++ showEqOpt amalgS (tail $ init $ show $
                                        case caslAmalg opts of
                                        [] -> [NoAnalysis]
                                        l -> l)
      ++ " " ++ unwords (infiles 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 Show
  
  -- | 'makeOpts' includes a parsed Flag in a set of HetcatsOpts
  makeOpts :: HetcatsOpts -> Flag -> HetcatsOpts
  makeOpts opts flg =
    let splitIPs = map (splitBy '.') . splitOn ','
    in case flg of
      Interactive -> opts { interactive = True }
      XML -> opts { xmlFlag = True }
      Listen x -> opts { listen = x }
      PidFile x -> opts { pidFile = 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 }
      DatabaseDoNotMigrate -> opts { databaseDoMigrate = False }
      DatabaseOutputFile x -> opts { databaseOutputFile = x }
      DatabaseConfigFile x -> opts { databaseConfigFile = x }
      DatabaseSubConfigKey x -> opts { databaseSubConfigKey = x }
      DatabaseFileVersionId x -> opts { databaseFileVersionId = x }
      DatabaseReanalyze -> opts { databaseReanalyze = True }
      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 }
      LossyTrans -> opts { lossyTrans = True }
      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 }
      DisableCertificateVerification ->
        opts { disableCertificateVerification = True }
      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 }
      OutputLogicList -> opts { outputLogicList = True }
      OutputLogicGraph -> opts { outputLogicGraph = True }
      FileType -> opts { fileType = True }
      FullSign -> opts { fullSign = True }
      PrintAST -> opts { printAST = True }
      UrlCatalog m -> opts { urlCatalog = m ++ urlCatalog opts }
      AccessToken s -> opts { accessToken = s }
      HttpRequestHeader header -> opts { httpRequestHeaders = header : httpRequestHeaders opts }
      Help -> opts -- skipped
      Version -> opts -- skipped
      VersionNumeric -> opts -- skipped
  
  -- | 'AnaType' describes the type of analysis to be performed
  data AnaType = Basic | Structured | Skip
  
  instance Show AnaType where
    show a = case a of
      Basic -> ""
      Structured -> showOpt justStructuredS
      Skip -> showOpt skipS
  
  -- | check if structured analysis should be performed
  isStructured :: HetcatsOpts -> Bool
  isStructured a = case analysis a of
      Structured -> True
      _ -> False
  
  -- | 'GuiType' determines if we want the GUI shown
  data GuiType = UseGui | NoGui
    deriving Eq
  
  instance Show GuiType where
    show g = case g of
      UseGui -> showOpt 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 Eq
  
  instance Show InType where
    show i = case i of
      ATermIn at -> genTermS ++ show at
      CASLIn -> "casl"
      HetCASLIn -> "het"
      DOLIn -> "dol"
      OWLIn oty -> show oty
      HaskellIn -> hsS
      ExperimentalIn -> "exp"
      MaudeIn -> "maude"
      TwelfIn -> "elf"
      HolLightIn -> "hol"
      IsaIn -> "isa"
      ThyIn -> "thy"
      TPTPIn -> "tptp"
      PrfIn -> prfS
      OmdocIn -> omdocS
      ProofCommand -> "hpf"
      GuessIn -> ""
      RDFIn -> "rdf"
      FreeCADIn -> "fcstd"
      CommonLogicIn isLong -> if isLong then "clif" else "clf"
      DgXml -> xmlS
      Xmi -> "xmi"
      Qvt -> "qvt"
      HtmlIn -> "html"
  
  -- 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
    show a = case a of
      BAF -> bafS
      NonBAF -> ""
  
  -- RDFIn is on purpose not listed; must be added manually if neccessary
  plainInTypes :: [InType]
  plainInTypes =
    [ CASLIn, HetCASLIn, DOLIn ]
    ++ map OWLIn plainOwlFormats ++
    [ HaskellIn, ExperimentalIn
    , MaudeIn, TwelfIn
    , HolLightIn, IsaIn, ThyIn, PrfIn, OmdocIn, ProofCommand
    , CommonLogicIn False, CommonLogicIn True
    , DgXml, FreeCADIn, Xmi, Qvt, TPTPIn ]
  
  aInTypes :: [InType]
  aInTypes = [ ATermIn x | x <- [BAF, NonBAF] ]
  
  -- | 'OWLFormat' lists possibilities for OWL syntax (in + out)
  data OWLFormat =
      Manchester
    | Functional
    | OwlXml
    | RdfXml
    | OBO
    | Turtle
    deriving Eq
  
  plainOwlFormats :: [OWLFormat]
  plainOwlFormats = [ Manchester, Functional, OwlXml, RdfXml, OBO, Turtle ]
  
  instance Show OWLFormat where
    show ty = case 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 Eq
  
  instance Show SPFType where
    show x = case x of
      ConsistencyCheck -> cS
      ProveTheory -> ""
  
  spfTypes :: [SPFType]
  spfTypes = [ConsistencyCheck, 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 Eq
  
  instance Show OutType where
    show o = case o of
      PrettyOut p -> ppS ++ show p
      GraphOut f -> graphE ++ show f
      Prf -> prfS
      EnvOut -> envS
      OWLOut oty -> show oty
      CLIFOut -> "clif"
      KIFOut -> "kif"
      OmdocOut -> omdocS
      XmlOut -> xmlS
      DbOut -> dbS
      JsonOut -> "json"
      ExperimentalOut -> experimentalS
      HaskellOut -> hsS
      FreeCADOut -> "fcxml"
      ThyFile -> "thy"
      DfgFile t -> dfgS ++ show t
      TPTPFile -> tptpS
      ComptableXml -> "comptable.xml"
      MedusaJson -> "medusa.json"
      RDFOut -> "nt"
      SigFile d -> "sig" ++ show d
      TheoryFile d -> "th" ++ show d
      SymXml -> "sym.xml"
      SymsXml -> "syms.xml"
  
  plainOutTypeList :: [OutType]
  plainOutTypeList =
    [ Prf, EnvOut ] ++ map OWLOut plainOwlFormats ++
    [ RDFOut, CLIFOut, KIFOut, OmdocOut, XmlOut, JsonOut, DbOut, ExperimentalOut
    , HaskellOut, ThyFile, ComptableXml, MedusaJson, FreeCADOut, SymXml, SymsXml
    , TPTPFile]
  
  outTypeList :: [OutType]
  outTypeList = let dl = [Delta, Fully] in
      plainOutTypeList
      ++ [ PrettyOut p | p <- prettyList ++ prettyList2]
      ++ [ SigFile d | d <- dl ]
      ++ [ TheoryFile d | d <- dl ]
      ++ [ DfgFile x | x <- spfTypes]
      ++ [ GraphOut f | f <- graphList ]
  
  instance Read OutType where
      readsPrec _ = readShow outTypeList
  
  data Delta = Delta | Fully deriving Eq
  
  instance Show Delta where
    show d = case d of
      Delta -> deltaS
      Fully -> ""
  
  {- | 'PrettyType' describes the type of output we want the pretty-printer
  to generate -}
  data PrettyType = PrettyAscii Bool | PrettyLatex Bool | PrettyXml | PrettyHtml
    deriving Eq
  
  instance Show PrettyType where
    show p = case p of
      PrettyAscii b -> (if b then "stripped." else "") ++ "dol"
      PrettyLatex b -> (if b then "labelled." else "") ++ "tex"
      PrettyXml -> xmlS
      PrettyHtml -> "html"
  
  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
  data GraphType =
      Dot Bool -- ^ True means show internal node labels
    deriving Eq
  
  instance Show GraphType where
    show g = case g of
      Dot si -> (if si then "exp." else "") ++ "dot"
  
  graphList :: [GraphType]
  graphList = [Dot True, Dot False]
  
  {- | 'options' describes all available options and is used to generate usage
  information -}
  options :: [OptDescr Flag]
  options = let
      cslst = "is a comma-separated list"
         ++ crS ++ "of one or more from:"
      crS = "\n  "
      bS = "| "
      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 information and exit"
      , Option "" ["numeric-version"] (NoArg VersionNumeric)
        "print version number and exit"
      , Option "h" ["help", "usage"] (NoArg Help)
        "print usage information and exit"
  #ifdef UNI_PACKAGE
      , Option "g" [guiS] (NoArg (Gui UseGui))
        "show graphs in windows"
      , Option "u" ["uncolored"] (NoArg Uncolored)
        "no colors in shown graphs"
  #endif
      , Option "x" [xmlS] (NoArg XML)
         "use xml packets to communicate"
  #ifdef SERVER
      , Option "P" [pidFileS] (ReqArg PidFile "FILEPATH")
         "path to put the PID file of the hets server (omit if no pidfile is desired)"
      , Option "X" ["server"] (NoArg Serve)
         "start hets as web-server"
  #endif
      , Option "z" [logicListS] (NoArg OutputLogicList)
        "output logic list as plain text"
      , 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)
        "only display file type"
      , 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 DOL libraries."
         ++ crS ++ "If an http[s] URL is specified here, it is treated as the last libdir because colons can occur in such URLs")
      , 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")
        "run interface/server by listening to the 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")
        "dump various strings"
      , Option "" ["disable-certificate-verification"]
        (NoArg DisableCertificateVerification)
        "Disable TLS certificate verification"
      , 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 "" [printASTS] (NoArg PrintAST) ("print AST in xml/json output")
      , Option "" [fullTheoriesS] (NoArg FullTheories) "xml output full theories"
      , Option "" [accessTokenS] (ReqArg AccessToken "TOKEN")
        "add access token to URLs (for ontohub)"
      , Option "H" [httpRequestHeaderS] (ReqArg HttpRequestHeader "HTTP_HEADER")
        ("additional headers to use for HTTP requests"
        ++ crS ++ "this option can be used multiple times")
      , 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)
               plainOutTypeList
         ++ bS ++ joinBar (map show [SigFile Fully,
                                     TheoryFile Fully])
                ++ bracket deltaS ++ crS
         ++ 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 "" ["database-do-not-migrate"] (NoArg DatabaseDoNotMigrate)
         ("Disallow Hets to create or alter the database tables" ++ crS
         ++ "This option is ignored if the option --database-config is given.")
      , Option "" ["database-file"] (ReqArg DatabaseOutputFile "FILEPATH")
         ("path to the sqlite database file" ++ crS
         ++ "This option is ignored if the option --database-config is given.")
      , Option "" ["database-config"] (ReqArg DatabaseConfigFile "FILEPATH")
         "path to the database configuration (yaml) file"
      , Option "" ["database-subconfig"] (ReqArg DatabaseSubConfigKey "KEY")
         ("subconfig of the database-config" ++ crS
         ++ "one of: production, development, test")
      , Option "" ["database-fileversion-id"] (ReqArg DatabaseFileVersionId "ID")
         "ID (sha1-hash) of the file version to associate the data with"
      , Option "" ["database-reanalyze"] (NoArg DatabaseReanalyze)
         "Overwrite data of this document and its imports in the database"
      , 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 "Y" [lossyTransS] (NoArg LossyTrans)
        "apply translations in a lossy way"
      , Option "a" [amalgS] (ReqArg parseCASLAmalg "ANALYSIS")
        ("CASL amalgamability analysis options" ++ crS ++ cslst ++
         crS ++ joinBar (map show caslAmalgOpts)),
        Option "M" ["MMT"] (NoArg UseMMT)
        "use MMT" ]
  
  -- | 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
    _ -> l) [] options
  
  -- | command line switches for the wep-api excluding non-dev-graph related ones
  optionFlags :: [(String, Flag)]
  optionFlags = dropWhile ((/= justStructuredS). fst) $ foldr (\ o l -> case o of
    Option _ (s : _) (NoArg f) _ -> (s, f) : l
    _ -> l) [] options
  
  -- parser functions returning Flags --
  
  -- | 'parseVerbosity' parses a 'Verbose' Flag from user input
  parseVerbosity :: Maybe String -> Flag
  parseVerbosity ms = case ms of
      Nothing -> Verbose 2
      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)
      [] -> (accP, accH)
  
  -- | 'parseConnect' parses a port Flag from user input
  parseConnect :: String -> Flag
  parseConnect s
   = let (sP, sH) = divideIntoPortHost s False ([], [])
     in case reads sP of
                  [(i, "")] -> Connect i sH
                  _ -> Connect (-1) sH
  
  parseListen :: String -> Flag
  parseListen s
   = case reads s of
                  [(i, "")] -> Listen i
                  _ -> Listen (-1)
  
  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 show plainInTypes
      ++ map ((treeS ++) . show) [ATermIn BAF, ATermIn NonBAF]
      ++ map show aInTypes
  
  -- | remove the extension from a file
  rmSuffix :: FilePath -> FilePath
  rmSuffix = fst . stripSuffix (envSuffix : downloadExtensions)
  
  -- | the suffix of env files
  envSuffix :: String
  envSuffix = '.' : envS
  
  -- | the suffix of env files
  prfSuffix :: String
  prfSuffix = '.' : prfS
  
  isDefLogic :: String -> HetcatsOpts -> Bool
  isDefLogic s = (s ==) . defLogic
  
  defLogicIsDMU :: HetcatsOpts -> Bool
  defLogicIsDMU = isDefLogic "DMU"
  
  getExtensions :: HetcatsOpts -> [String]
  getExtensions opts = case intype opts of
          GuessIn
            | defLogicIsDMU opts -> [".xml"]
            | isDefLogic "Framework" opts
              -> [".elf", ".thy", ".maude", ".het", ".dol"]
          GuessIn -> downloadExtensions
          e@(ATermIn _) -> ['.' : show e, '.' : treeS ++ show e]
          e -> ['.' : show e]
    ++ [envSuffix]
  
  getFileNames :: [String] -> FilePath -> [FilePath]
  getFileNames exts file =
    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
                             EnvOut -> True
                             _ -> False) . outtypes
  
  -- | should prf be written
  isPrfOut :: OutType -> Bool
  isPrfOut o = case o of
      Prf -> True
      _ -> False
  
  -- | should prf be written
  hasPrfOut :: HetcatsOpts -> Bool
  hasPrfOut = any isPrfOut . outtypes
  
  -- | remove prf writing
  removePrfOut :: HetcatsOpts -> HetcatsOpts
  removePrfOut opts =
       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
    [a, b] -> (a, b)
    _ -> 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
  parseInType1 str =
    case reads str of
      [(t, "")] -> t
      _ -> hetsError (str ++ " 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 str = case reads $ bracket str of
      [(l, "")] -> OutTypes l
      _ -> 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
  
  -- | guesses the InType
  guess :: String -> InType -> InType
  guess file itype = case itype of
      GuessIn -> guessInType file
      _ -> itype
  
  -- | 'guessInType' parses an 'InType' from the FilePath
  guessInType :: FilePath -> InType
  guessInType file = case fileparse downloadExtensions file of
        (_, _, Just ('.' : suf)) -> parseInType1 suf
        (_, _, _) -> GuessIn
  
  -- | 'parseCASLAmalg' parses CASL amalgamability options
  parseCASLAmalg :: String -> Flag
  parseCASLAmalg str =
      case reads $ bracket str of
      [(l, "")] -> CASLAmalg $ filter ( \ o -> case o of
                                        NoAnalysis -> False
                                        _ -> True ) l
      _ -> hetsError $ str ++
                      " is not a valid CASL amalgamability analysis option list"
  
  -- main functions --
  
  -- | 'hetcatsOpts' parses sensible HetcatsOpts from ARGV
  hetcatsOpts :: [String] -> IO HetcatsOpts
  hetcatsOpts argv =
    let argv' = filter (not . isUni) argv
        isUni = isPrefixOf "--uni"
     in case getOpt Permute options argv' of
          (opts, nonOpts, []) ->
              do flags <- checkFlags opts
                 let opts' = (foldr (flip makeOpts) defaultHetcatsOpts flags)
                              { infiles = nonOpts }
                 setupDatabaseOptions opts'
          (_, _, errs) -> hetsIOError (concat errs)
    where
      setupDatabaseOptions :: HetcatsOpts -> IO HetcatsOpts
      setupDatabaseOptions opts = do
        let filepath = if null $ infiles opts then "" else head $ infiles opts
        let dbContext = DBConfig.emptyDBContext
              { DBConfig.contextFileVersion = databaseFileVersionId opts
              , DBConfig.contextFilePath = 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' =
              null (databaseFileVersionId opts) || databaseReanalyze opts
        dbConfig <- if DbOut `elem` outtypes opts
                    then DBConfig.parseDatabaseConfig
                           (databaseOutputFile opts)
                           (databaseConfigFile opts)
                           (databaseSubConfigKey opts)
                           (databaseDoMigrate opts)
                    else return DBConfig.emptyDBConfig
        return opts { databaseConfig = dbConfig
                    , databaseContext = dbContext
                    , databaseReanalyze = databaseReanalyze'
                    }
  
  
  printOptionsWarnings :: HetcatsOpts -> IO ()
  printOptionsWarnings opts =
    let v = verbose opts in
    unless (null (pidFile opts) || serve opts)
      (verbMsgIOLn 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 fs = do
      let collectFlags = collectDirs
                          . collectOutTypes
                          . collectVerbosity
                          . collectSpecOpts
                          -- collect some more here?
          h = null [ () | Help <- fs]
          v = null [ () | Version <- fs]
          vn = null [ () | VersionNumeric <- fs]
      unless h $ putStr hetsUsage
      unless v $ putStrLn hetsVersion
      unless vn $ putStrLn hetsVersionNumeric
      unless (h && v && vn) exitSuccess
      collectFlags fs
  
  -- 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]
  checkOutDirs fs = do
      case fs of
          [] -> return ()
          [f] -> checkOutDir f
          _ -> hetsIOError
              "Only one output directory may be specified on the command line"
      return fs
  
  -- | 'checkLibDirs' checks a list of LibDir for sanity
  checkLibDirs :: [Flag] -> IO [Flag]
  checkLibDirs fs =
      case fs of
          [] -> do
              s <- getEnvDef "HETS_LIB" ""
              if null s then return [] else do
                  let d = LibDirs s
                  checkLibDirs [d]
                  return [d]
          [LibDirs f] -> mapM_ checkLibDir (joinHttpLibPath $ splitPaths f)
            >> return fs
          _ -> hetsIOError
              "Only one library path may be specified on the command line"
  
  joinHttpLibPath :: [String] -> [String]
  joinHttpLibPath l = case l of
    p : f : r | p  == "file" && take 2 f == "//" ->
      (p ++ ':' : f) : joinHttpLibPath r
    p : f : _ | elem p ["http", "https"] && take 2 f == "//" ->
      [intercalate ":" l]
    f : r -> f : joinHttpLibPath r
    [] -> []
  
  -- | 'checkLibDir' checks a single LibDir for sanity
  checkLibDir :: FilePath -> IO ()
  checkLibDir file = do
      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]
  collectDirs fs = do
      let (ods, fs1) = partition isOutDir fs
          (lds, fs2) = partition isLibDir fs1
          isOutDir (OutDir _) = True
          isOutDir _ = False
          isLibDir (LibDirs _) = True
          isLibDir _ = False
      ods' <- checkOutDirs ods
      lds' <- checkLibDirs lds
      return $ ods' ++ lds' ++ fs2
  
  collectVerbosity :: [Flag] -> [Flag]
  collectVerbosity fs =
      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]
  collectOutTypes fs =
      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]
  collectSpecOpts fs =
      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 :: String -> a
  hetsError = error . ("command line usage error (see 'hets -h')\n" ++)
  
  -- | print error and usage and exit with code 2
  hetsIOError :: String -> IO a
  hetsIOError s = do
    unless (null s) $ hPutStrLn stderr s
    putStr "for Hets usage, use: hets -h\n"
    exitWith $ ExitFailure 2
  
  -- | 'hetsUsage' generates usage information for the commandline
  hetsUsage :: String
  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 ()
  showDiags opts ds =
      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
  showDiags1 opts res =
    let dbout = DbOut `elem` outtypes opts in
    if outputToStdout opts || dbout then do
      Result ds res' <- lift $ runResultT res
      when (outputToStdout opts) $ lift $ printDiags (verbose opts) ds
      when dbout $ lift $
        saveDiagnoses (databaseConfig opts) (databaseContext opts) (verbose opts) ds
      case res' of
        Just res'' -> return res''
        Nothing -> liftR $ Result [] Nothing
    else res
  