842ae4bd224140319ae7feec1872b93dfd491143fielding{-# LANGUAGE CPP #-}

842ae4bd224140319ae7feec1872b93dfd491143fielding{- |

842ae4bd224140319ae7feec1872b93dfd491143fieldingModule : $Header$

842ae4bd224140319ae7feec1872b93dfd491143fieldingDescription : Datatypes and functions for options that hets understands.

842ae4bd224140319ae7feec1872b93dfd491143fieldingCopyright : (c) Martin Kuehl, Christian Maeder, Uni Bremen 2002-2006

842ae4bd224140319ae7feec1872b93dfd491143fieldingLicense : GPLv2 or higher, see LICENSE.txt

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcndMaintainer : Christian.Maeder@dfki.de

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrseStability : provisional

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcndPortability : portable

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcnd

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcndDatatypes for options that hets understands.

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcnd Useful functions to parse and check user-provided values.

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcnd-}

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcnd

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcndmodule Driver.Options

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcnd ( HetcatsOpts (..)

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcnd , Flag

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcnd , optionArgs

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcnd , optionFlags

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcnd , makeOpts

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcnd , AnaType (..)

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcnd , GuiType (..)

ce9621257ef9e54c1bbe5ad8a5f445a1f211c2dcnd , InType (..)

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse , OutType (..)

6ace32dacb8313226eb9019275d0e4fa45a15148rse , PrettyType (..)

70535d6421eb979ac79d8f49d31cd94d75dd8b2fjorton , prettyList

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse , GraphType (..)

a943533fd4d91d114af622731a405407990c4fb1rse , SPFType (..)

67139e2d50d1e11558d87f7042f61cb04bb0d1d2jim , ATType

1660a5facf5797acb7aa1300f5ef86756a0bf493jorton , Delta

1660a5facf5797acb7aa1300f5ef86756a0bf493jorton , hetcatsOpts

a943533fd4d91d114af622731a405407990c4fb1rse , isStructured

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse , guess

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse , rmSuffix

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse , envSuffix

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse , prfSuffix

7933d4a963def02417113b6798d87a36395053b0rse , removePrfOut

7933d4a963def02417113b6798d87a36395053b0rse , hasEnvOut

71c00f988beb28388702e14cb7fe06f08bd792bbdougm , hasPrfOut

71c00f988beb28388702e14cb7fe06f08bd792bbdougm , getFileNames

71c00f988beb28388702e14cb7fe06f08bd792bbdougm , existsAnSource

7933d4a963def02417113b6798d87a36395053b0rse , getExtensions

71c00f988beb28388702e14cb7fe06f08bd792bbdougm , checkRecentEnv

71c00f988beb28388702e14cb7fe06f08bd792bbdougm , downloadExtensions

71c00f988beb28388702e14cb7fe06f08bd792bbdougm , defaultHetcatsOpts

7933d4a963def02417113b6798d87a36395053b0rse , hetsVersion

71c00f988beb28388702e14cb7fe06f08bd792bbdougm , showDiags

71c00f988beb28388702e14cb7fe06f08bd792bbdougm , showDiags1

71c00f988beb28388702e14cb7fe06f08bd792bbdougm , putIfVerbose

7933d4a963def02417113b6798d87a36395053b0rse , doDump

7933d4a963def02417113b6798d87a36395053b0rse , checkUri

d1bb6e2664788e0437acc18e877562c9a796d7cerse , defLogicIsDMU

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse , useCatalogURL

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse , hetsIOError

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse ) where

7933d4a963def02417113b6798d87a36395053b0rse

7933d4a963def02417113b6798d87a36395053b0rseimport Driver.Version

7988a91d9a1c6413f2c1a2138847f513d20de856fuankg

7988a91d9a1c6413f2c1a2138847f513d20de856fuankgimport Common.Utils

7933d4a963def02417113b6798d87a36395053b0rseimport Common.IO

7933d4a963def02417113b6798d87a36395053b0rseimport Common.Id

7988a91d9a1c6413f2c1a2138847f513d20de856fuankgimport Common.Result

53c239bee62c6d55b5ddfba5d99376d4c8de924ejwoolleyimport Common.ResultT

7933d4a963def02417113b6798d87a36395053b0rseimport Common.Amalgamate

7933d4a963def02417113b6798d87a36395053b0rseimport Common.Keywords

7988a91d9a1c6413f2c1a2138847f513d20de856fuankg

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrseimport System.Directory

7933d4a963def02417113b6798d87a36395053b0rseimport System.Console.GetOpt

7933d4a963def02417113b6798d87a36395053b0rseimport System.Exit

7988a91d9a1c6413f2c1a2138847f513d20de856fuankgimport System.IO

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrseimport Control.Monad

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrseimport Control.Monad.Trans

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrseimport Data.Char

e726f34f8da08c01ee8bc90904b26196b69c8587wroweimport Data.List

7933d4a963def02417113b6798d87a36395053b0rseimport Data.Maybe

7988a91d9a1c6413f2c1a2138847f513d20de856fuankg

e9eabac76b50e8f00d0c391f6070d0f42db77aa2wrowe-- | short version without date for ATC files

e9eabac76b50e8f00d0c391f6070d0f42db77aa2wrowehetsVersion :: String

e9eabac76b50e8f00d0c391f6070d0f42db77aa2wrowehetsVersion = takeWhile (/= ',') hetcats_version

7933d4a963def02417113b6798d87a36395053b0rse

7933d4a963def02417113b6798d87a36395053b0rse-- | translate a given http reference using the URL catalog

7988a91d9a1c6413f2c1a2138847f513d20de856fuankguseCatalogURL :: HetcatsOpts -> FilePath -> FilePath

7933d4a963def02417113b6798d87a36395053b0rseuseCatalogURL opts fname = case mapMaybe

7933d4a963def02417113b6798d87a36395053b0rse (\ (a, b) -> fmap (b ++) $ stripPrefix a fname)

7988a91d9a1c6413f2c1a2138847f513d20de856fuankg $ urlCatalog opts of

7933d4a963def02417113b6798d87a36395053b0rse m : _ -> m

7933d4a963def02417113b6798d87a36395053b0rse _ -> fname

7988a91d9a1c6413f2c1a2138847f513d20de856fuankg

7933d4a963def02417113b6798d87a36395053b0rsebracket :: String -> String

7933d4a963def02417113b6798d87a36395053b0rsebracket s = "[" ++ s ++ "]"

7988a91d9a1c6413f2c1a2138847f513d20de856fuankg

176c2742db03fcb7b7d13e6408dd967d87e542e9ben-- use the same strings for parsing and printing!

e0c3fda9f782aee1140d83fbce32672ac299f2a4benverboseS, intypeS, outtypesS, skipS, justStructuredS, transS,

7988a91d9a1c6413f2c1a2138847f513d20de856fuankg guiS, libdirsS, outdirS, amalgS, recursiveS, namedSpecsS,

7a4e3510f3516132ff057ac986fd6350164b7950kbrand interactiveS, modelSparQS, counterSparQS, connectS, xmlS, listenS,

7a4e3510f3516132ff057ac986fd6350164b7950kbrand applyAutomaticRuleS, normalFormS, unlitS :: String

7a4e3510f3516132ff057ac986fd6350164b7950kbrand

7a4e3510f3516132ff057ac986fd6350164b7950kbrandmodelSparQS = "modelSparQ"

7a4e3510f3516132ff057ac986fd6350164b7950kbrandcounterSparQS = "counterSparQ"

7933d4a963def02417113b6798d87a36395053b0rseverboseS = "verbose"

7933d4a963def02417113b6798d87a36395053b0rseintypeS = "input-type"

7988a91d9a1c6413f2c1a2138847f513d20de856fuankgouttypesS = "output-types"

7933d4a963def02417113b6798d87a36395053b0rseskipS = "just-parse"

7933d4a963def02417113b6798d87a36395053b0rsejustStructuredS = "just-structured"

7988a91d9a1c6413f2c1a2138847f513d20de856fuankgguiS = "gui"

e335319a08e12eb7daff9afa80e985dc53f652b8jortonlibdirsS = "hets-libdirs"

e335319a08e12eb7daff9afa80e985dc53f652b8jortonoutdirS = "output-dir"

7988a91d9a1c6413f2c1a2138847f513d20de856fuankgamalgS = "casl-amalg"

e335319a08e12eb7daff9afa80e985dc53f652b8jortonnamedSpecsS = "named-specs"

e335319a08e12eb7daff9afa80e985dc53f652b8jortontransS = "translation"

7988a91d9a1c6413f2c1a2138847f513d20de856fuankgrecursiveS = "recursive"

7933d4a963def02417113b6798d87a36395053b0rseinteractiveS = "interactive"

7933d4a963def02417113b6798d87a36395053b0rseconnectS = "connect"

7988a91d9a1c6413f2c1a2138847f513d20de856fuankgxmlS = "xml"

7933d4a963def02417113b6798d87a36395053b0rselistenS = "listen"

7933d4a963def02417113b6798d87a36395053b0rseapplyAutomaticRuleS = "apply-automatic-rule"

7988a91d9a1c6413f2c1a2138847f513d20de856fuankgnormalFormS = "normal-form"

77504f17963a8dd941a921d9ddfa25ddb0f348d6kbrandunlitS = "unlit"

77504f17963a8dd941a921d9ddfa25ddb0f348d6kbrand

7933d4a963def02417113b6798d87a36395053b0rseurlCatalogS :: String

7933d4a963def02417113b6798d87a36395053b0rseurlCatalogS = "url-catalog"

7988a91d9a1c6413f2c1a2138847f513d20de856fuankg

7933d4a963def02417113b6798d87a36395053b0rserelposS :: String

7933d4a963def02417113b6798d87a36395053b0rserelposS = "relative-positions"

7988a91d9a1c6413f2c1a2138847f513d20de856fuankg

7933d4a963def02417113b6798d87a36395053b0rsefullSignS :: String

7933d4a963def02417113b6798d87a36395053b0rsefullSignS = "full-signatures"

7988a91d9a1c6413f2c1a2138847f513d20de856fuankg

a1de5cf47c9ccfbf493264e8a3fa7ddd5a9c80d1kbrandfullTheoriesS :: String

1fd6337111a9607570691e38857dcece7fb84abekbrandfullTheoriesS = "full-theories"

a1de5cf47c9ccfbf493264e8a3fa7ddd5a9c80d1kbrand

1fd6337111a9607570691e38857dcece7fb84abekbrandlogicGraphS :: String

a1de5cf47c9ccfbf493264e8a3fa7ddd5a9c80d1kbrandlogicGraphS = "logic-graph"

1fd6337111a9607570691e38857dcece7fb84abekbrand

1fd6337111a9607570691e38857dcece7fb84abekbrandfileTypeS :: String

1fd6337111a9607570691e38857dcece7fb84abekbrandfileTypeS = "file-type"

7efe7de73c89c26518714a504359244d03cfbbc5jorton

7efe7de73c89c26518714a504359244d03cfbbc5jortonblacklistS :: String

d9b079a6dd66d36313be56f859c8c61153146527sfblacklistS = "blacklist"

d9b079a6dd66d36313be56f859c8c61153146527sf

d9b079a6dd66d36313be56f859c8c61153146527sfwhitelistS :: String

2b4e45d87889ab2f6b432690cc993a42bc607fafjortonwhitelistS = "whitelist"

2b4e45d87889ab2f6b432690cc993a42bc607fafjorton

f84d3d83a741c21154d42e0ebdec9b9b37efeedcjortonaccessTokenS :: String

43c3e6a4b559b76b750c245ee95e2782c15b4296jimaccessTokenS = "access_token"

e3715027f352040ef98da03359b00f13ddb506cbrpluem

e3715027f352040ef98da03359b00f13ddb506cbrpluemgenTermS, treeS, bafS :: String

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrsegenTermS = "gen_trm"

099c357f282d4aebf2b32264f7dce6ffc0497c37sftreeS = "tree."

099c357f282d4aebf2b32264f7dce6ffc0497c37sfbafS = ".baf"

099c357f282d4aebf2b32264f7dce6ffc0497c37sf

099c357f282d4aebf2b32264f7dce6ffc0497c37sfgraphS, ppS, envS, deltaS, prfS, omdocS, hsS, experimentalS :: String

099c357f282d4aebf2b32264f7dce6ffc0497c37sfgraphS = "graph."

099c357f282d4aebf2b32264f7dce6ffc0497c37sfppS = "pp."

099c357f282d4aebf2b32264f7dce6ffc0497c37sfenvS = "env"

099c357f282d4aebf2b32264f7dce6ffc0497c37sfdeltaS = ".delta"

099c357f282d4aebf2b32264f7dce6ffc0497c37sfprfS = "prf"

e8f95a682820a599fe41b22977010636be5c2717jimomdocS = "omdoc"

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrsehsS = "hs"

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrseexperimentalS = "exp"

cde1010d880fb6230f80c9d697842ea0b1cb79c7dougm

cde1010d880fb6230f80c9d697842ea0b1cb79c7dougmtptpS, dfgS, cS :: String

7988a91d9a1c6413f2c1a2138847f513d20de856fuankgtptpS = "tptp"

7933d4a963def02417113b6798d87a36395053b0rsedfgS = "dfg"

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrsecS = ".c"

1fd6337111a9607570691e38857dcece7fb84abekbrand

7933d4a963def02417113b6798d87a36395053b0rseshowOpt :: String -> String

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrseshowOpt s = if null s then "" else " --" ++ s

7988a91d9a1c6413f2c1a2138847f513d20de856fuankg

8fdc55d1624c714391fe1f93ebafe98ace427f4adougmshowEqOpt :: String -> String -> String

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrseshowEqOpt k s = if null s then "" else showOpt k ++ "=" ++ s

7988a91d9a1c6413f2c1a2138847f513d20de856fuankg

7933d4a963def02417113b6798d87a36395053b0rse-- main Datatypes --

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse

7988a91d9a1c6413f2c1a2138847f513d20de856fuankg-- | 'HetcatsOpts' is a record of all options received from the command line

7933d4a963def02417113b6798d87a36395053b0rsedata HetcatsOpts = HcOpt -- for comments see usage info

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse { analysis :: AnaType

7988a91d9a1c6413f2c1a2138847f513d20de856fuankg , guiType :: GuiType

7933d4a963def02417113b6798d87a36395053b0rse , urlCatalog :: [(String, String)]

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse , infiles :: [FilePath] -- ^ files to be read

7988a91d9a1c6413f2c1a2138847f513d20de856fuankg , specNames :: [SIMPLE_ID] -- ^ specs to be processed

a72de14bfdbf0be9d935be9bdc2df631ca5e032bdougm , transNames :: [SIMPLE_ID] -- ^ comorphism to be processed

a72de14bfdbf0be9d935be9bdc2df631ca5e032bdougm , viewNames :: [SIMPLE_ID] -- ^ views to be processed

7988a91d9a1c6413f2c1a2138847f513d20de856fuankg , intype :: InType

a72de14bfdbf0be9d935be9bdc2df631ca5e032bdougm , libdirs :: [FilePath]

a72de14bfdbf0be9d935be9bdc2df631ca5e032bdougm , modelSparQ :: FilePath

7988a91d9a1c6413f2c1a2138847f513d20de856fuankg , counterSparQ :: Int

77504f17963a8dd941a921d9ddfa25ddb0f348d6kbrand , outdir :: FilePath

77504f17963a8dd941a921d9ddfa25ddb0f348d6kbrand , outtypes :: [OutType]

7933d4a963def02417113b6798d87a36395053b0rse , xupdate :: FilePath

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse , recurse :: Bool

7988a91d9a1c6413f2c1a2138847f513d20de856fuankg , verbose :: Int

7933d4a963def02417113b6798d87a36395053b0rse , defLogic :: String

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse , defSyntax :: String

7988a91d9a1c6413f2c1a2138847f513d20de856fuankg , outputToStdout :: Bool -- ^ send messages to stdout?

44985e4f931d3a75a7e5108705010cc21605ee34druggeri , caslAmalg :: [CASLAmalgOpt]

44985e4f931d3a75a7e5108705010cc21605ee34druggeri , interactive :: Bool

44985e4f931d3a75a7e5108705010cc21605ee34druggeri , connectP :: Int

44985e4f931d3a75a7e5108705010cc21605ee34druggeri , connectH :: String

8f2700898323915da289644dc1f3ee11a5e5b4earpluem , uncolored :: Bool

8f2700898323915da289644dc1f3ee11a5e5b4earpluem , xmlFlag :: Bool

8f2700898323915da289644dc1f3ee11a5e5b4earpluem , applyAutomatic :: Bool

8f2700898323915da289644dc1f3ee11a5e5b4earpluem , computeNormalForm :: Bool

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse , dumpOpts :: [String]

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse , ioEncoding :: Enc

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse -- | use the library name in positions to avoid differences after uploads

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse , useLibPos :: Bool

7933d4a963def02417113b6798d87a36395053b0rse , unlit :: Bool

0839d91ee551a0e19ea9577bb00976b97308dfddmartin , serve :: Bool

7988a91d9a1c6413f2c1a2138847f513d20de856fuankg , listen :: Int

7933d4a963def02417113b6798d87a36395053b0rse , whitelist :: [[String]]

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse , blacklist :: [[String]]

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse , runMMT :: Bool

7933d4a963def02417113b6798d87a36395053b0rse , fullTheories :: Bool

0839d91ee551a0e19ea9577bb00976b97308dfddmartin , outputLogicGraph :: Bool

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse , fileType :: Bool

509111f5f58a9effd4c832f6a0cbd6ad9d549188jorton , accessToken :: String

509111f5f58a9effd4c832f6a0cbd6ad9d549188jorton , fullSign :: Bool }

509111f5f58a9effd4c832f6a0cbd6ad9d549188jorton

509111f5f58a9effd4c832f6a0cbd6ad9d549188jorton{- | 'defaultHetcatsOpts' defines the default HetcatsOpts, which are used as

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrsebasic values when the user specifies nothing else -}

39c7699ec0799d394d3f67145d4a12ed82f587b8jortondefaultHetcatsOpts :: HetcatsOpts

7988a91d9a1c6413f2c1a2138847f513d20de856fuankgdefaultHetcatsOpts = HcOpt

39c7699ec0799d394d3f67145d4a12ed82f587b8jorton { analysis = Basic

39c7699ec0799d394d3f67145d4a12ed82f587b8jorton , guiType = NoGui

39c7699ec0799d394d3f67145d4a12ed82f587b8jorton , urlCatalog = []

7988a91d9a1c6413f2c1a2138847f513d20de856fuankg , infiles = []

a2558ec3af4391b7da7fe61e1e53383bbd0174b9jorton , specNames = []

a2558ec3af4391b7da7fe61e1e53383bbd0174b9jorton , transNames = []

a2558ec3af4391b7da7fe61e1e53383bbd0174b9jorton , viewNames = []

a2558ec3af4391b7da7fe61e1e53383bbd0174b9jorton , intype = GuessIn

a2558ec3af4391b7da7fe61e1e53383bbd0174b9jorton , libdirs = []

a2558ec3af4391b7da7fe61e1e53383bbd0174b9jorton , modelSparQ = ""

39c7699ec0799d394d3f67145d4a12ed82f587b8jorton , counterSparQ = 3

89b8bbc89404e7071e573c4f0a17f528996e855djorton , outdir = ""

89b8bbc89404e7071e573c4f0a17f528996e855djorton , outtypes = [] -- no default

89b8bbc89404e7071e573c4f0a17f528996e855djorton , xupdate = ""

89b8bbc89404e7071e573c4f0a17f528996e855djorton , recurse = False

89b8bbc89404e7071e573c4f0a17f528996e855djorton , defLogic = "CASL"

89b8bbc89404e7071e573c4f0a17f528996e855djorton , defSyntax = ""

89b8bbc89404e7071e573c4f0a17f528996e855djorton , verbose = 1

89b8bbc89404e7071e573c4f0a17f528996e855djorton , outputToStdout = True

89b8bbc89404e7071e573c4f0a17f528996e855djorton , caslAmalg = [Cell]

89b8bbc89404e7071e573c4f0a17f528996e855djorton , interactive = False

89b8bbc89404e7071e573c4f0a17f528996e855djorton , connectP = -1

89b8bbc89404e7071e573c4f0a17f528996e855djorton , connectH = ""

89b8bbc89404e7071e573c4f0a17f528996e855djorton , uncolored = False

89b8bbc89404e7071e573c4f0a17f528996e855djorton , xmlFlag = False

89b8bbc89404e7071e573c4f0a17f528996e855djorton , applyAutomatic = False

89b8bbc89404e7071e573c4f0a17f528996e855djorton , computeNormalForm = False

89b8bbc89404e7071e573c4f0a17f528996e855djorton , dumpOpts = []

89b8bbc89404e7071e573c4f0a17f528996e855djorton , ioEncoding = Utf8

89b8bbc89404e7071e573c4f0a17f528996e855djorton , useLibPos = False

11e076839c8d5a82d55e710194d0daac51390dbdsf , unlit = False

89b8bbc89404e7071e573c4f0a17f528996e855djorton , serve = False

89b8bbc89404e7071e573c4f0a17f528996e855djorton , listen = -1

11e076839c8d5a82d55e710194d0daac51390dbdsf , whitelist = []

89b8bbc89404e7071e573c4f0a17f528996e855djorton , blacklist = []

89b8bbc89404e7071e573c4f0a17f528996e855djorton , runMMT = False

89b8bbc89404e7071e573c4f0a17f528996e855djorton , fullTheories = False

89b8bbc89404e7071e573c4f0a17f528996e855djorton , outputLogicGraph = False

89b8bbc89404e7071e573c4f0a17f528996e855djorton , fileType = False

89b8bbc89404e7071e573c4f0a17f528996e855djorton , accessToken = ""

e6e65585927961caf45d4e9e932bb1f4e9e89ca1jerenkrantz , fullSign = False }

e8f95a682820a599fe41b22977010636be5c2717jim

e6e65585927961caf45d4e9e932bb1f4e9e89ca1jerenkrantzinstance Show HetcatsOpts where

e8f95a682820a599fe41b22977010636be5c2717jim show opts =

e6e65585927961caf45d4e9e932bb1f4e9e89ca1jerenkrantz let showFlag p o = if p opts then showOpt o else ""

e8f95a682820a599fe41b22977010636be5c2717jim showIPLists p s = let ll = p opts in if null ll then "" else

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse showEqOpt s . intercalate "," $ map (intercalate ".") ll

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse in

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse showEqOpt verboseS (show $ verbose opts)

3e4e54d4e3fc0123c63d57aa84ac7ad7a8c73ff8jorton ++ show (guiType opts)

3e4e54d4e3fc0123c63d57aa84ac7ad7a8c73ff8jorton ++ showFlag outputLogicGraph logicGraphS

3e4e54d4e3fc0123c63d57aa84ac7ad7a8c73ff8jorton ++ showFlag fileType fileTypeS

3e4e54d4e3fc0123c63d57aa84ac7ad7a8c73ff8jorton ++ showFlag interactive interactiveS

3e4e54d4e3fc0123c63d57aa84ac7ad7a8c73ff8jorton ++ show (analysis opts)

3e4e54d4e3fc0123c63d57aa84ac7ad7a8c73ff8jorton ++ case defLogic opts of

3e4e54d4e3fc0123c63d57aa84ac7ad7a8c73ff8jorton s | s /= defLogic defaultHetcatsOpts -> showEqOpt logicS s

3e4e54d4e3fc0123c63d57aa84ac7ad7a8c73ff8jorton _ -> ""

3e4e54d4e3fc0123c63d57aa84ac7ad7a8c73ff8jorton ++ case defSyntax opts of

3e4e54d4e3fc0123c63d57aa84ac7ad7a8c73ff8jorton s | s /= defSyntax defaultHetcatsOpts -> showEqOpt serializationS s

3e4e54d4e3fc0123c63d57aa84ac7ad7a8c73ff8jorton _ -> ""

3e4e54d4e3fc0123c63d57aa84ac7ad7a8c73ff8jorton ++ case accessToken opts of

7933d4a963def02417113b6798d87a36395053b0rse "" -> ""

7933d4a963def02417113b6798d87a36395053b0rse t -> showEqOpt accessTokenS t

7933d4a963def02417113b6798d87a36395053b0rse ++ showEqOpt libdirsS (intercalate ":" $ libdirs opts)

2b7078b0c4fd5b6054f6f2d4f626177844f5c6f7wrowe ++ case modelSparQ opts of

2b7078b0c4fd5b6054f6f2d4f626177844f5c6f7wrowe "" -> ""

2b7078b0c4fd5b6054f6f2d4f626177844f5c6f7wrowe f -> showEqOpt modelSparQS f

2b7078b0c4fd5b6054f6f2d4f626177844f5c6f7wrowe ++ case counterSparQ opts of

2b7078b0c4fd5b6054f6f2d4f626177844f5c6f7wrowe n | n /= counterSparQ defaultHetcatsOpts

2b7078b0c4fd5b6054f6f2d4f626177844f5c6f7wrowe -> showEqOpt counterSparQS $ show n

2b7078b0c4fd5b6054f6f2d4f626177844f5c6f7wrowe _ -> ""

2b7078b0c4fd5b6054f6f2d4f626177844f5c6f7wrowe ++ showFlag xmlFlag xmlS

2b7078b0c4fd5b6054f6f2d4f626177844f5c6f7wrowe ++ showFlag ((/= -1) . connectP) connectS

2b7078b0c4fd5b6054f6f2d4f626177844f5c6f7wrowe ++ showFlag ((/= -1) . listen) listenS

2b7078b0c4fd5b6054f6f2d4f626177844f5c6f7wrowe ++ showIPLists whitelist whitelistS

2b7078b0c4fd5b6054f6f2d4f626177844f5c6f7wrowe ++ showIPLists blacklist blacklistS

2b7078b0c4fd5b6054f6f2d4f626177844f5c6f7wrowe ++ concatMap (showEqOpt "dump") (dumpOpts opts)

2b7078b0c4fd5b6054f6f2d4f626177844f5c6f7wrowe ++ showEqOpt "encoding" (map toLower $ show $ ioEncoding opts)

239dd0cf663713025d4451ddd465685021007d82wrowe ++ showFlag unlit unlitS

2b7078b0c4fd5b6054f6f2d4f626177844f5c6f7wrowe ++ showFlag useLibPos relposS

56bd16e394f49423a22aa82643eb27f26db2c748jorton ++ showFlag fullSign fullSignS

56bd16e394f49423a22aa82643eb27f26db2c748jorton ++ showFlag fullTheories fullTheoriesS

56bd16e394f49423a22aa82643eb27f26db2c748jorton ++ case urlCatalog opts of

56bd16e394f49423a22aa82643eb27f26db2c748jorton [] -> ""

56bd16e394f49423a22aa82643eb27f26db2c748jorton cs -> showEqOpt urlCatalogS $ intercalate ","

a73ec375db18806018eabc968baa85b250bbbf5djorton $ map (\ (a, b) -> a ++ '=' : b) cs

a73ec375db18806018eabc968baa85b250bbbf5djorton ++ showEqOpt intypeS (show $ intype opts)

a73ec375db18806018eabc968baa85b250bbbf5djorton ++ showEqOpt outdirS (outdir opts)

a73ec375db18806018eabc968baa85b250bbbf5djorton ++ showEqOpt outtypesS (intercalate "," $ map show $ outtypes opts)

a73ec375db18806018eabc968baa85b250bbbf5djorton ++ showFlag recurse recursiveS

a73ec375db18806018eabc968baa85b250bbbf5djorton ++ showFlag applyAutomatic applyAutomaticRuleS

e8f95a682820a599fe41b22977010636be5c2717jim ++ showFlag computeNormalForm normalFormS

e8f95a682820a599fe41b22977010636be5c2717jim ++ showEqOpt namedSpecsS (intercalate "," $ map show $ specNames opts)

2b7078b0c4fd5b6054f6f2d4f626177844f5c6f7wrowe ++ showEqOpt transS (intercalate ":" $ map show $ transNames opts)

2b7078b0c4fd5b6054f6f2d4f626177844f5c6f7wrowe ++ showEqOpt viewS (intercalate "," $ map show $ viewNames opts)

2b7078b0c4fd5b6054f6f2d4f626177844f5c6f7wrowe ++ showEqOpt amalgS (tail $ init $ show $

239dd0cf663713025d4451ddd465685021007d82wrowe case caslAmalg opts of

2b7078b0c4fd5b6054f6f2d4f626177844f5c6f7wrowe [] -> [NoAnalysis]

d1bb6e2664788e0437acc18e877562c9a796d7cerse l -> l)

71c00f988beb28388702e14cb7fe06f08bd792bbdougm ++ " " ++ unwords (infiles opts)

71c00f988beb28388702e14cb7fe06f08bd792bbdougm

71c00f988beb28388702e14cb7fe06f08bd792bbdougm-- | every 'Flag' describes an option (see usage info)

7933d4a963def02417113b6798d87a36395053b0rsedata Flag =

e8f95a682820a599fe41b22977010636be5c2717jim Verbose Int

b5451913a64155af2eab4f12ecbaf16e15acafc3wrowe | Quiet

b5451913a64155af2eab4f12ecbaf16e15acafc3wrowe | Uncolored

8aced0b621ea45e8621c7073b0bfbe5ea91c2329wrowe | Version

b5451913a64155af2eab4f12ecbaf16e15acafc3wrowe | Recurse

93350a0dfa22a2c523cdcbad3357327013ecc145martin | ApplyAutomatic

2c038bf2465bf2150c396f4e67f68ebc5bb9e6e9wrowe | NormalForm

b5451913a64155af2eab4f12ecbaf16e15acafc3wrowe | Help

b5451913a64155af2eab4f12ecbaf16e15acafc3wrowe | Gui GuiType

b5451913a64155af2eab4f12ecbaf16e15acafc3wrowe | Analysis AnaType

8a5120efd60acf0323371cb30cba489723b03819jorton | DefaultLogic String

b5451913a64155af2eab4f12ecbaf16e15acafc3wrowe | DefaultSyntax String

8aced0b621ea45e8621c7073b0bfbe5ea91c2329wrowe | InType InType

2b7078b0c4fd5b6054f6f2d4f626177844f5c6f7wrowe | LibDirs String

2b7078b0c4fd5b6054f6f2d4f626177844f5c6f7wrowe | OutDir FilePath

2b7078b0c4fd5b6054f6f2d4f626177844f5c6f7wrowe | XUpdate FilePath

2b7078b0c4fd5b6054f6f2d4f626177844f5c6f7wrowe | ModelSparQ FilePath

2b7078b0c4fd5b6054f6f2d4f626177844f5c6f7wrowe | CounterSparQ Int

2b7078b0c4fd5b6054f6f2d4f626177844f5c6f7wrowe | OutTypes [OutType]

af5dd1c93d2185f7e37f8783c593b64fd35ea8a6wrowe | Specs [SIMPLE_ID]

af5dd1c93d2185f7e37f8783c593b64fd35ea8a6wrowe | Trans [SIMPLE_ID]

8dc154408549195c828b823e9dc7396f107f2512jorton | Views [SIMPLE_ID]

8dc154408549195c828b823e9dc7396f107f2512jorton | CASLAmalg [CASLAmalgOpt]

b79b480213d7452db127eec054e52eb2b4fa6153wrowe | Interactive

417f504d4d11631c0d062be85347f82a26c88677aaron | Connect Int String

11f2c481e1d57bedb3f758565307501e9a2730ddtrawick | XML

2792780a6fb0951dc304b940ba9274ed1e37fe26wrowe | Dump String

11f2c481e1d57bedb3f758565307501e9a2730ddtrawick | IOEncoding Enc

2792780a6fb0951dc304b940ba9274ed1e37fe26wrowe | Unlit

11f2c481e1d57bedb3f758565307501e9a2730ddtrawick | RelPos

11f2c481e1d57bedb3f758565307501e9a2730ddtrawick | Serve

417f504d4d11631c0d062be85347f82a26c88677aaron | Listen Int

7933d4a963def02417113b6798d87a36395053b0rse | Whitelist String

7933d4a963def02417113b6798d87a36395053b0rse | Blacklist String

9cb81d96f6b556cec1aa456191f43f7932aabaaedougm | UseMMT

9cb81d96f6b556cec1aa456191f43f7932aabaaedougm | FullTheories

9cb81d96f6b556cec1aa456191f43f7932aabaaedougm | FullSign

9cb81d96f6b556cec1aa456191f43f7932aabaaedougm | OutputLogicGraph

9cb81d96f6b556cec1aa456191f43f7932aabaaedougm | FileType

9cb81d96f6b556cec1aa456191f43f7932aabaaedougm | AccessToken String

9cb81d96f6b556cec1aa456191f43f7932aabaaedougm | UrlCatalog [(String, String)]

9cb81d96f6b556cec1aa456191f43f7932aabaaedougm

9cb81d96f6b556cec1aa456191f43f7932aabaaedougm-- | 'makeOpts' includes a parsed Flag in a set of HetcatsOpts

9cb81d96f6b556cec1aa456191f43f7932aabaaedougmmakeOpts :: HetcatsOpts -> Flag -> HetcatsOpts

807c9f7266ad3a966b6714fe578f3c9da1ca868brpluemmakeOpts opts flg =

2ce2fc3287632e20f1b8759aa17e571f68c6fe6dsf let splitIPs = map (splitBy '.') . splitOn ','

807c9f7266ad3a966b6714fe578f3c9da1ca868brpluem in case flg of

9cb81d96f6b556cec1aa456191f43f7932aabaaedougm Interactive -> opts { interactive = True }

9cb81d96f6b556cec1aa456191f43f7932aabaaedougm XML -> opts { xmlFlag = True }

9cb81d96f6b556cec1aa456191f43f7932aabaaedougm Listen x -> opts { listen = x }

9cb81d96f6b556cec1aa456191f43f7932aabaaedougm Blacklist x -> opts { blacklist = splitIPs x }

9cb81d96f6b556cec1aa456191f43f7932aabaaedougm Whitelist x -> opts { whitelist = splitIPs x }

9cb81d96f6b556cec1aa456191f43f7932aabaaedougm Connect x y -> opts { connectP = x, connectH = y }

9cb81d96f6b556cec1aa456191f43f7932aabaaedougm Analysis x -> opts { analysis = x }

807c9f7266ad3a966b6714fe578f3c9da1ca868brpluem Gui x -> opts { guiType = x }

cde1010d880fb6230f80c9d697842ea0b1cb79c7dougm InType x -> opts { intype = x }

9cb81d96f6b556cec1aa456191f43f7932aabaaedougm LibDirs x -> opts { libdirs = joinHttpLibPath $ splitPaths x }

807c9f7266ad3a966b6714fe578f3c9da1ca868brpluem ModelSparQ x -> opts { modelSparQ = x }

9cb81d96f6b556cec1aa456191f43f7932aabaaedougm CounterSparQ x -> opts { counterSparQ = x }

cde1010d880fb6230f80c9d697842ea0b1cb79c7dougm OutDir x -> opts { outdir = x }

185aa71728867671e105178b4c66fbc22b65ae26sf OutTypes x -> opts { outtypes = x }

2261f694ce2fc09f9df6c65bd8e1f4230313696bjorton XUpdate x -> opts { xupdate = x }

2261f694ce2fc09f9df6c65bd8e1f4230313696bjorton Recurse -> opts { recurse = True }

cde1010d880fb6230f80c9d697842ea0b1cb79c7dougm ApplyAutomatic -> opts { applyAutomatic = True }

cde1010d880fb6230f80c9d697842ea0b1cb79c7dougm NormalForm -> opts { computeNormalForm = True }

cde1010d880fb6230f80c9d697842ea0b1cb79c7dougm Specs x -> opts { specNames = x }

cde1010d880fb6230f80c9d697842ea0b1cb79c7dougm Trans x -> opts { transNames = x }

9cb81d96f6b556cec1aa456191f43f7932aabaaedougm Views x -> opts { viewNames = x }

621bd763d2e4d32f19013ac8b76b375b5a01851fdougm Verbose x -> opts { verbose = x }

621bd763d2e4d32f19013ac8b76b375b5a01851fdougm DefaultLogic x -> opts { defLogic = x }

621bd763d2e4d32f19013ac8b76b375b5a01851fdougm DefaultSyntax x -> opts { defSyntax = x }

621bd763d2e4d32f19013ac8b76b375b5a01851fdougm CASLAmalg x -> opts { caslAmalg = x }

621bd763d2e4d32f19013ac8b76b375b5a01851fdougm Quiet -> opts { verbose = 0 }

621bd763d2e4d32f19013ac8b76b375b5a01851fdougm Uncolored -> opts { uncolored = True }

621bd763d2e4d32f19013ac8b76b375b5a01851fdougm Dump s -> opts { dumpOpts = s : dumpOpts opts }

807c9f7266ad3a966b6714fe578f3c9da1ca868brpluem IOEncoding e -> opts { ioEncoding = e }

621bd763d2e4d32f19013ac8b76b375b5a01851fdougm Serve -> opts { serve = True }

807c9f7266ad3a966b6714fe578f3c9da1ca868brpluem Unlit -> opts { unlit = True }

621bd763d2e4d32f19013ac8b76b375b5a01851fdougm RelPos -> opts { useLibPos = True }

807c9f7266ad3a966b6714fe578f3c9da1ca868brpluem UseMMT -> opts { runMMT = True }

807c9f7266ad3a966b6714fe578f3c9da1ca868brpluem FullTheories -> opts { fullTheories = True }

807c9f7266ad3a966b6714fe578f3c9da1ca868brpluem OutputLogicGraph -> opts { outputLogicGraph = True }

807c9f7266ad3a966b6714fe578f3c9da1ca868brpluem FileType -> opts { fileType = True }

807c9f7266ad3a966b6714fe578f3c9da1ca868brpluem FullSign -> opts { fullSign = True }

807c9f7266ad3a966b6714fe578f3c9da1ca868brpluem UrlCatalog m -> opts { urlCatalog = m ++ urlCatalog opts }

ccbf65bf19ac58a396133923aee4597e0870ec47bnicholes AccessToken s -> opts { accessToken = s }

621bd763d2e4d32f19013ac8b76b375b5a01851fdougm Help -> opts -- skipped

621bd763d2e4d32f19013ac8b76b375b5a01851fdougm Version -> opts -- skipped

621bd763d2e4d32f19013ac8b76b375b5a01851fdougm

621bd763d2e4d32f19013ac8b76b375b5a01851fdougm-- | 'AnaType' describes the type of analysis to be performed

621bd763d2e4d32f19013ac8b76b375b5a01851fdougmdata AnaType = Basic | Structured | Skip

621bd763d2e4d32f19013ac8b76b375b5a01851fdougm

9cb81d96f6b556cec1aa456191f43f7932aabaaedougminstance Show AnaType where

9cb81d96f6b556cec1aa456191f43f7932aabaaedougm show a = case a of

9cb81d96f6b556cec1aa456191f43f7932aabaaedougm Basic -> ""

9cb81d96f6b556cec1aa456191f43f7932aabaaedougm Structured -> showOpt justStructuredS

4ede070ca63bd4c48045e35a7192582769770290jorton Skip -> showOpt skipS

7933d4a963def02417113b6798d87a36395053b0rse

807c9f7266ad3a966b6714fe578f3c9da1ca868brpluem-- | check if structured analysis should be performed

a943533fd4d91d114af622731a405407990c4fb1rseisStructured :: HetcatsOpts -> Bool

9cb81d96f6b556cec1aa456191f43f7932aabaaedougmisStructured a = case analysis a of

469549ac22c6f7b9ecdd9df2565925563e4df84djwoolley Structured -> True

9cb81d96f6b556cec1aa456191f43f7932aabaaedougm _ -> False

807c9f7266ad3a966b6714fe578f3c9da1ca868brpluem

a943533fd4d91d114af622731a405407990c4fb1rse-- | 'GuiType' determines if we want the GUI shown

9cb81d96f6b556cec1aa456191f43f7932aabaaedougmdata GuiType = UseGui | NoGui

9cb81d96f6b556cec1aa456191f43f7932aabaaedougm deriving Eq

9cb81d96f6b556cec1aa456191f43f7932aabaaedougm

807c9f7266ad3a966b6714fe578f3c9da1ca868brplueminstance Show GuiType where

807c9f7266ad3a966b6714fe578f3c9da1ca868brpluem show g = case g of

807c9f7266ad3a966b6714fe578f3c9da1ca868brpluem UseGui -> showOpt guiS

807c9f7266ad3a966b6714fe578f3c9da1ca868brpluem NoGui -> ""

807c9f7266ad3a966b6714fe578f3c9da1ca868brpluem

807c9f7266ad3a966b6714fe578f3c9da1ca868brpluem-- | 'InType' describes the type of input the infile contains

807c9f7266ad3a966b6714fe578f3c9da1ca868brpluemdata InType =

9cb81d96f6b556cec1aa456191f43f7932aabaaedougm ATermIn ATType

9cb81d96f6b556cec1aa456191f43f7932aabaaedougm | CASLIn

9cb81d96f6b556cec1aa456191f43f7932aabaaedougm | HetCASLIn

a943533fd4d91d114af622731a405407990c4fb1rse | DOLIn

a943533fd4d91d114af622731a405407990c4fb1rse | OWLIn

a943533fd4d91d114af622731a405407990c4fb1rse | OwlXmlIn

a943533fd4d91d114af622731a405407990c4fb1rse | OBOIn

a943533fd4d91d114af622731a405407990c4fb1rse | HaskellIn

9cb81d96f6b556cec1aa456191f43f7932aabaaedougm | MaudeIn

185aa71728867671e105178b4c66fbc22b65ae26sf | TwelfIn

2261f694ce2fc09f9df6c65bd8e1f4230313696bjorton | HolLightIn

2261f694ce2fc09f9df6c65bd8e1f4230313696bjorton | IsaIn

baa6746bc66ff1daa1852a3a085906d2dfa96bb6sf | ThyIn

71c00f988beb28388702e14cb7fe06f08bd792bbdougm | PrfIn

a943533fd4d91d114af622731a405407990c4fb1rse | OmdocIn

71c00f988beb28388702e14cb7fe06f08bd792bbdougm | ExperimentalIn -- ^ for testing new functionality

a943533fd4d91d114af622731a405407990c4fb1rse | ProofCommand

a943533fd4d91d114af622731a405407990c4fb1rse | GuessIn

6d7efb8c76b56eaebd6032096771c9e44b247f3fdougm | FreeCADIn

f4c472b8dce3c2e559232dbb5b27ed2466922ea4jerenkrantz | CommonLogicIn Bool -- ^ "clf" or "clif" ('True' is long version)

f4c472b8dce3c2e559232dbb5b27ed2466922ea4jerenkrantz | DgXml

469549ac22c6f7b9ecdd9df2565925563e4df84djwoolley | RDFIn

469549ac22c6f7b9ecdd9df2565925563e4df84djwoolley | Xmi

d0ba3b97557d47323bd055fb4002ed7692f703b9jerenkrantz | Qvt

71c00f988beb28388702e14cb7fe06f08bd792bbdougm | TPTPIn

185aa71728867671e105178b4c66fbc22b65ae26sf | HtmlIn -- just to complain

7988a91d9a1c6413f2c1a2138847f513d20de856fuankg deriving Eq

baa6746bc66ff1daa1852a3a085906d2dfa96bb6sf

71c00f988beb28388702e14cb7fe06f08bd792bbdougminstance Show InType where

a943533fd4d91d114af622731a405407990c4fb1rse show i = case i of

71c00f988beb28388702e14cb7fe06f08bd792bbdougm ATermIn at -> genTermS ++ show at

a943533fd4d91d114af622731a405407990c4fb1rse CASLIn -> "casl"

a943533fd4d91d114af622731a405407990c4fb1rse HetCASLIn -> "het"

71c00f988beb28388702e14cb7fe06f08bd792bbdougm DOLIn -> "dol"

a943533fd4d91d114af622731a405407990c4fb1rse OwlXmlIn -> "owl.xml"

d28d7091912b3d911bdbe18df2d37d315681054bdougm OWLIn -> "owl"

a943533fd4d91d114af622731a405407990c4fb1rse OBOIn -> "obo"

931b4fd1cc9dd3da096c45f4bf7ddcc14e0985c1dougm HaskellIn -> hsS

a943533fd4d91d114af622731a405407990c4fb1rse ExperimentalIn -> "exp"

a943533fd4d91d114af622731a405407990c4fb1rse MaudeIn -> "maude"

a943533fd4d91d114af622731a405407990c4fb1rse TwelfIn -> "elf"

a943533fd4d91d114af622731a405407990c4fb1rse HolLightIn -> "hol"

a943533fd4d91d114af622731a405407990c4fb1rse IsaIn -> "isa"

a943533fd4d91d114af622731a405407990c4fb1rse ThyIn -> "thy"

ea6ff3396df1d6d43ee0ecfa3e26ada981d8e9a3sctemme TPTPIn -> "tptp"

ea6ff3396df1d6d43ee0ecfa3e26ada981d8e9a3sctemme PrfIn -> prfS

ea6ff3396df1d6d43ee0ecfa3e26ada981d8e9a3sctemme OmdocIn -> omdocS

c947acd3d1a604a0acad6a53ef685312d4410fc5dougm ProofCommand -> "hpf"

a943533fd4d91d114af622731a405407990c4fb1rse GuessIn -> ""

a943533fd4d91d114af622731a405407990c4fb1rse FreeCADIn -> "fcstd"

4ede070ca63bd4c48045e35a7192582769770290jorton CommonLogicIn isLong -> if isLong then "clif" else "clf"

a943533fd4d91d114af622731a405407990c4fb1rse DgXml -> xmlS

a943533fd4d91d114af622731a405407990c4fb1rse RDFIn -> "rdf"

7933d4a963def02417113b6798d87a36395053b0rse Xmi -> "xmi"

7933d4a963def02417113b6798d87a36395053b0rse Qvt -> "qvt"

7b6ba9c468f26bdb3492d5e8cb79628a3b04e8c8wrowe HtmlIn -> "html"

7933d4a963def02417113b6798d87a36395053b0rse

a943533fd4d91d114af622731a405407990c4fb1rse-- maybe this optional tree prefix can be omitted

a943533fd4d91d114af622731a405407990c4fb1rseinstance Read InType where

2f32a3d146dc55d81b31660386e17c3b83ad61b8bnicholes readsPrec _ = readShowAux $ map ( \ i -> (show i, i))

a943533fd4d91d114af622731a405407990c4fb1rse (plainInTypes ++ aInTypes)

71c00f988beb28388702e14cb7fe06f08bd792bbdougm ++ [(treeS ++ genTermS ++ show at, ATermIn at)

a943533fd4d91d114af622731a405407990c4fb1rse | at <- [BAF, NonBAF]]

a943533fd4d91d114af622731a405407990c4fb1rse

7933d4a963def02417113b6798d87a36395053b0rse-- | 'ATType' describes distinct types of ATerms

7933d4a963def02417113b6798d87a36395053b0rsedata ATType = BAF | NonBAF deriving Eq

71c00f988beb28388702e14cb7fe06f08bd792bbdougm

7933d4a963def02417113b6798d87a36395053b0rseinstance Show ATType where

a943533fd4d91d114af622731a405407990c4fb1rse show a = case a of

a943533fd4d91d114af622731a405407990c4fb1rse BAF -> bafS

2f32a3d146dc55d81b31660386e17c3b83ad61b8bnicholes NonBAF -> ""

a943533fd4d91d114af622731a405407990c4fb1rse

71c00f988beb28388702e14cb7fe06f08bd792bbdougm-- OwlXmlIn needs to be before OWLIn to avoid a read error in parseInType1

71c00f988beb28388702e14cb7fe06f08bd792bbdougmplainInTypes :: [InType]

a943533fd4d91d114af622731a405407990c4fb1rseplainInTypes =

7933d4a963def02417113b6798d87a36395053b0rse [ CASLIn, HetCASLIn, DOLIn, OwlXmlIn, OWLIn, OBOIn, HaskellIn, ExperimentalIn

7933d4a963def02417113b6798d87a36395053b0rse , MaudeIn, TwelfIn

e726f34f8da08c01ee8bc90904b26196b69c8587wrowe , HolLightIn, IsaIn, ThyIn, PrfIn, OmdocIn, ProofCommand

e726f34f8da08c01ee8bc90904b26196b69c8587wrowe , CommonLogicIn False, CommonLogicIn True

807c9f7266ad3a966b6714fe578f3c9da1ca868brpluem , DgXml, FreeCADIn, RDFIn, Xmi, Qvt, TPTPIn ]

e726f34f8da08c01ee8bc90904b26196b69c8587wrowe

e726f34f8da08c01ee8bc90904b26196b69c8587wroweaInTypes :: [InType]

807c9f7266ad3a966b6714fe578f3c9da1ca868brpluemaInTypes = [ ATermIn x | x <- [BAF, NonBAF] ]

807c9f7266ad3a966b6714fe578f3c9da1ca868brpluem

807c9f7266ad3a966b6714fe578f3c9da1ca868brpluemdata SPFType = ConsistencyCheck | ProveTheory

807c9f7266ad3a966b6714fe578f3c9da1ca868brpluem

807c9f7266ad3a966b6714fe578f3c9da1ca868brplueminstance Show SPFType where

807c9f7266ad3a966b6714fe578f3c9da1ca868brpluem show x = case x of

e726f34f8da08c01ee8bc90904b26196b69c8587wrowe ConsistencyCheck -> cS

e726f34f8da08c01ee8bc90904b26196b69c8587wrowe ProveTheory -> ""

e726f34f8da08c01ee8bc90904b26196b69c8587wrowe

ccbf65bf19ac58a396133923aee4597e0870ec47bnicholesspfTypes :: [SPFType]

e726f34f8da08c01ee8bc90904b26196b69c8587wrowespfTypes = [ConsistencyCheck, ProveTheory]

e726f34f8da08c01ee8bc90904b26196b69c8587wrowe

e726f34f8da08c01ee8bc90904b26196b69c8587wrowe-- | 'OutType' describes the type of outputs that we want to generate

e726f34f8da08c01ee8bc90904b26196b69c8587wrowedata OutType =

e726f34f8da08c01ee8bc90904b26196b69c8587wrowe PrettyOut PrettyType

e726f34f8da08c01ee8bc90904b26196b69c8587wrowe | GraphOut GraphType

e726f34f8da08c01ee8bc90904b26196b69c8587wrowe | Prf

e726f34f8da08c01ee8bc90904b26196b69c8587wrowe | EnvOut

e726f34f8da08c01ee8bc90904b26196b69c8587wrowe | OWLOut

e726f34f8da08c01ee8bc90904b26196b69c8587wrowe | CLIFOut

e726f34f8da08c01ee8bc90904b26196b69c8587wrowe | KIFOut

e726f34f8da08c01ee8bc90904b26196b69c8587wrowe | OmdocOut

e726f34f8da08c01ee8bc90904b26196b69c8587wrowe | XmlOut -- ^ development graph xml output

e726f34f8da08c01ee8bc90904b26196b69c8587wrowe | ExperimentalOut -- ^ for testing new functionality

e726f34f8da08c01ee8bc90904b26196b69c8587wrowe | HaskellOut

e726f34f8da08c01ee8bc90904b26196b69c8587wrowe | FreeCADOut

e726f34f8da08c01ee8bc90904b26196b69c8587wrowe | ThyFile -- ^ isabelle theory file

e726f34f8da08c01ee8bc90904b26196b69c8587wrowe | DfgFile SPFType -- ^ SPASS input file

e726f34f8da08c01ee8bc90904b26196b69c8587wrowe | TPTPFile SPFType

e726f34f8da08c01ee8bc90904b26196b69c8587wrowe | ComptableXml

e726f34f8da08c01ee8bc90904b26196b69c8587wrowe | SigFile Delta -- ^ signature as text

185aa71728867671e105178b4c66fbc22b65ae26sf | TheoryFile Delta -- ^ signature with sentences as text

2261f694ce2fc09f9df6c65bd8e1f4230313696bjorton | RDFOut

2261f694ce2fc09f9df6c65bd8e1f4230313696bjorton | SymXml

e726f34f8da08c01ee8bc90904b26196b69c8587wrowe | SymsXml

4ede070ca63bd4c48045e35a7192582769770290jorton

e726f34f8da08c01ee8bc90904b26196b69c8587wroweinstance Show OutType where

e726f34f8da08c01ee8bc90904b26196b69c8587wrowe show o = case o of

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse PrettyOut p -> ppS ++ show p

7933d4a963def02417113b6798d87a36395053b0rse GraphOut f -> graphS ++ show f

cc003103e52ff9d5fe9bed567ef9438613ab4fbfrse Prf -> prfS

a943533fd4d91d114af622731a405407990c4fb1rse EnvOut -> envS

7933d4a963def02417113b6798d87a36395053b0rse OWLOut -> "omn"

7933d4a963def02417113b6798d87a36395053b0rse CLIFOut -> "clif"

825479074daa2c65852666c4b26d771dff957507jorton KIFOut -> "kif"

e8f95a682820a599fe41b22977010636be5c2717jim OmdocOut -> omdocS

825479074daa2c65852666c4b26d771dff957507jorton XmlOut -> xmlS

825479074daa2c65852666c4b26d771dff957507jorton ExperimentalOut -> experimentalS

a943533fd4d91d114af622731a405407990c4fb1rse HaskellOut -> hsS

dfaea9dfb7e6fd2c97b9d35a75d7bcab94af8ff8dougm FreeCADOut -> "fcxml"

a943533fd4d91d114af622731a405407990c4fb1rse ThyFile -> "thy"

d2ffb32434f79782ff7a364ffa31064698c5c645jorton DfgFile t -> dfgS ++ show t

a943533fd4d91d114af622731a405407990c4fb1rse TPTPFile t -> tptpS ++ show t

7b6ba9c468f26bdb3492d5e8cb79628a3b04e8c8wrowe ComptableXml -> "comptable.xml"

a943533fd4d91d114af622731a405407990c4fb1rse SigFile d -> "sig" ++ show d

fa599e0e097d4d933c4dc378ffbfc3c045dd589ewrowe TheoryFile d -> "th" ++ show d

a943533fd4d91d114af622731a405407990c4fb1rse RDFOut -> "nt"

a72211e92bab814bfa28ee086ca9b2a1a6095c92chrisd SymXml -> "sym.xml"

a72211e92bab814bfa28ee086ca9b2a1a6095c92chrisd SymsXml -> "syms.xml"

a943533fd4d91d114af622731a405407990c4fb1rse

a72211e92bab814bfa28ee086ca9b2a1a6095c92chrisdplainOutTypeList :: [OutType]

a72211e92bab814bfa28ee086ca9b2a1a6095c92chrisdplainOutTypeList =

a72211e92bab814bfa28ee086ca9b2a1a6095c92chrisd [Prf, EnvOut, OWLOut, CLIFOut, KIFOut, OmdocOut, XmlOut, ExperimentalOut,

a72211e92bab814bfa28ee086ca9b2a1a6095c92chrisd HaskellOut, ThyFile, ComptableXml, FreeCADOut, RDFOut, SymXml, SymsXml]

825479074daa2c65852666c4b26d771dff957507jorton

dfaea9dfb7e6fd2c97b9d35a75d7bcab94af8ff8dougmoutTypeList :: [OutType]

17f61d2695369a9b62bc0e5f38e9c4d23eebc664jortonoutTypeList = let dl = [Delta, Fully] in

9cb81d96f6b556cec1aa456191f43f7932aabaaedougm plainOutTypeList

9cb81d96f6b556cec1aa456191f43f7932aabaaedougm ++ [ PrettyOut p | p <- prettyList ++ prettyList2]

621bd763d2e4d32f19013ac8b76b375b5a01851fdougm ++ [ SigFile d | d <- dl ]

fc58f0ff708564b67cd578c626b6500d1cd63a51sf ++ [ TheoryFile d | d <- dl ]

fc58f0ff708564b67cd578c626b6500d1cd63a51sf ++ [ DfgFile x | x <- spfTypes]

fc58f0ff708564b67cd578c626b6500d1cd63a51sf ++ [ TPTPFile x | x <- spfTypes]

fc58f0ff708564b67cd578c626b6500d1cd63a51sf ++ [ GraphOut f | f <- graphList ]

fc58f0ff708564b67cd578c626b6500d1cd63a51sf

fc58f0ff708564b67cd578c626b6500d1cd63a51sfinstance Read OutType where

fc58f0ff708564b67cd578c626b6500d1cd63a51sf readsPrec _ = readShowAux $ map ( \ o -> (show o, o)) outTypeList

fc58f0ff708564b67cd578c626b6500d1cd63a51sf

fc58f0ff708564b67cd578c626b6500d1cd63a51sfdata Delta = Delta | Fully

fc58f0ff708564b67cd578c626b6500d1cd63a51sf

fc58f0ff708564b67cd578c626b6500d1cd63a51sfinstance Show Delta where

7933d4a963def02417113b6798d87a36395053b0rse show d = case d of

7933d4a963def02417113b6798d87a36395053b0rse Delta -> deltaS

6ace32dacb8313226eb9019275d0e4fa45a15148rse Fully -> ""

6ace32dacb8313226eb9019275d0e4fa45a15148rse

7933d4a963def02417113b6798d87a36395053b0rse{- | 'PrettyType' describes the type of output we want the pretty-printer

7933d4a963def02417113b6798d87a36395053b0rseto generate -}

7933d4a963def02417113b6798d87a36395053b0rsedata PrettyType = PrettyAscii Bool | PrettyLatex Bool | PrettyXml | PrettyHtml

7933d4a963def02417113b6798d87a36395053b0rse

7933d4a963def02417113b6798d87a36395053b0rseinstance Show PrettyType where

7933d4a963def02417113b6798d87a36395053b0rse show p = case p of

6ace32dacb8313226eb9019275d0e4fa45a15148rse PrettyAscii b -> (if b then "stripped." else "") ++ "het"

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

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 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 "X" ["server"] (NoArg Serve)

"start hets as web-server"

#endif

, 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 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")

"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 "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)

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 ++ graphS ++ 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)

"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 = drop 11 $ 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"]

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

return (foldr (flip makeOpts) defaultHetcatsOpts flags)

{ infiles = nonOpts }

(_, _, errs) -> hetsIOError (concat errs)

-- | '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]

unless h $ putStr hetsUsage

unless v $ putStrLn ("version of hets: " ++ hetcats_version)

unless (v && h) 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 | elem p ["http", "https"] -> (p ++ ':' : f) : joinHttpLibPath r

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

hPutStrLn stderr s

putStr hetsUsage

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 =

if outputToStdout opts then do

Result ds res' <- lift $ runResultT res

lift $ printDiags (verbose opts) ds

case res' of

Just res'' -> return res''

Nothing -> liftR $ Result [] Nothing

else res