Options.hs revision 083bc1972a66d73749760eab3a90bf4eb9ca7951
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederModule : $Header$
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian MaederCopyright : (c) Martin K�hl, Christian Maeder, Uni Bremen 2002-2006
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer : maeder@tzi.de
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederStability : provisional
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederDatatypes for options that hets understands.
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Useful functions to parse and check user-provided values.
38c817b94e0a5b1ae94178b1075c187e07bcc5e1Christian Maeder-- | short version without date for ATC files
38c817b94e0a5b1ae94178b1075c187e07bcc5e1Christian MaederhetsVersion :: String
38c817b94e0a5b1ae94178b1075c187e07bcc5e1Christian MaederhetsVersion = takeWhile (/= ',') hetcats_version
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederbracket :: String -> String
2353f65833a3da763392f771223250cd50b8d873Christian Maederbracket s = "[" ++ s ++ "]"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- use the same strings for parsing and printing!
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederverboseS, intypeS, outtypesS, rawS, skipS, structS,
083bc1972a66d73749760eab3a90bf4eb9ca7951Christian Maeder guiS, onlyGuiS, libdirS, outdirS, amalgS, specS, recursiveS :: String
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederverboseS = "verbose"
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederintypeS = "input-type"
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederouttypesS = "output-types"
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederskipS = "just-parse"
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederstructS = "just-structured"
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederonlyGuiS = "only-gui"
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederlibdirS = "hets-libdir"
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederoutdirS = "output-dir"
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederamalgS = "casl-amalg"
083bc1972a66d73749760eab3a90bf4eb9ca7951Christian MaederspecS = "named-specs"
083bc1972a66d73749760eab3a90bf4eb9ca7951Christian MaederrecursiveS = "recursive"
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederasciiS, latexS, textS, texS :: String
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederasciiS = "ascii"
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederlatexS = "latex"
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedertextS = "text"
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedergenTermS, treeS, bafS, astS :: String
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedergenTermS = "gen_trm"
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedertreeS = "tree."
fdac680252d7347858bd67b4c2a2aaa52e623815Christian MaedergraphS, ppS, envS, naxS, deltaS, prfS, omdocS :: String
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedergraphS = "graph."
beff4152e9f0fe90885458d1a1733b183a2a8816Christian MaederdeltaS = ".delta"
fdac680252d7347858bd67b4c2a2aaa52e623815Christian MaederomdocS = "omdoc"
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus LuettichdfgS, cS :: String
2353f65833a3da763392f771223250cd50b8d873Christian MaedershowOpt :: String -> String
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedershowOpt s = if null s then "" else " --" ++ s
2353f65833a3da763392f771223250cd50b8d873Christian MaedershowEqOpt :: String -> String -> String
2353f65833a3da763392f771223250cd50b8d873Christian MaedershowEqOpt k s = if null s then "" else showOpt k ++ "=" ++ s
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- main Datatypes --
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'HetcatsOpts' is a record of all options received from the command line
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederdata HetcatsOpts = -- for comments see usage info
2353f65833a3da763392f771223250cd50b8d873Christian Maeder HcOpt { analysis :: AnaType
2353f65833a3da763392f771223250cd50b8d873Christian Maeder , gui :: GuiType
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , infiles :: [FilePath] -- files to be read
2353f65833a3da763392f771223250cd50b8d873Christian Maeder , specNames :: [SIMPLE_ID] -- specs to be processed
2353f65833a3da763392f771223250cd50b8d873Christian Maeder , intype :: InType
2353f65833a3da763392f771223250cd50b8d873Christian Maeder , libdir :: FilePath
2353f65833a3da763392f771223250cd50b8d873Christian Maeder , outdir :: FilePath
2353f65833a3da763392f771223250cd50b8d873Christian Maeder , outtypes :: [OutType]
083bc1972a66d73749760eab3a90bf4eb9ca7951Christian Maeder , recurse :: Bool
2353f65833a3da763392f771223250cd50b8d873Christian Maeder , rawopts :: [RawOpt]
2353f65833a3da763392f771223250cd50b8d873Christian Maeder , verbose :: Int
2353f65833a3da763392f771223250cd50b8d873Christian Maeder , defLogic :: String
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , outputToStdout :: Bool -- flag: output diagnostic messages?
2353f65833a3da763392f771223250cd50b8d873Christian Maeder , caslAmalg :: [CASLAmalgOpt]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance Show HetcatsOpts where
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder show opts = showEqOpt verboseS (show $ verbose opts)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ++ show (gui opts)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ++ show (analysis opts)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ++ showEqOpt libdirS (libdir opts)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ++ showEqOpt intypeS (show $ intype opts)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ++ showEqOpt outdirS (outdir opts)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ++ showEqOpt outtypesS (showOutTypes $ outtypes opts)
083bc1972a66d73749760eab3a90bf4eb9ca7951Christian Maeder ++ (if recurse opts then showOpt recursiveS else "")
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder ++ showEqOpt specS (joinWith ',' $ map show $ specNames opts)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ++ showRaw (rawopts opts)
2353f65833a3da763392f771223250cd50b8d873Christian Maeder ++ showEqOpt amalgS ( tail $ init $ show $
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder case caslAmalg opts of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder [] -> [NoAnalysis]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ++ " " ++ showInFiles (infiles opts)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder showInFiles = joinWith ' '
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder showOutTypes = joinWith ',' . map show
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder showRaw = joinWith ' ' . map show
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'makeOpts' includes a parsed Flag in a set of HetcatsOpts
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedermakeOpts :: HetcatsOpts -> Flag -> HetcatsOpts
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian MaedermakeOpts opts flg = case flg of
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder Analysis x -> opts { analysis = x }
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder Gui x -> opts { gui = x }
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder InType x -> opts { intype = x }
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder LibDir x -> opts { libdir = x }
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder OutDir x -> opts { outdir = x }
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder OutTypes x -> opts { outtypes = x }
083bc1972a66d73749760eab3a90bf4eb9ca7951Christian Maeder Recurse -> opts { recurse = True }
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder Specs x -> opts { specNames = x }
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder Raw x -> opts { rawopts = x }
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder Verbose x -> opts { verbose = x }
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder DefaultLogic x -> opts { defLogic = x }
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder CASLAmalg x -> opts { caslAmalg = x }
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder Quiet -> opts { verbose = 0 }
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder Help -> opts -- skipped
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder Version -> opts -- skipped
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'defaultHetcatsOpts' defines the default HetcatsOpts, which are used as
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- basic values when the user specifies nothing else
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederdefaultHetcatsOpts :: HetcatsOpts
2353f65833a3da763392f771223250cd50b8d873Christian MaederdefaultHetcatsOpts =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder HcOpt { analysis = Basic
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , infiles = []
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder , specNames = []
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , intype = GuessIn
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , libdir = ""
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , outdir = ""
4a2f7efdf67dfcda0946f1b6373f41976ddea7a4Christian Maeder , outtypes = [] -- no default
083bc1972a66d73749760eab3a90bf4eb9ca7951Christian Maeder , recurse = False
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , rawopts = []
3a9d784341454573b50b32fa1b494e7418df3086Christian Maeder , defLogic = "CASL"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , verbose = 1
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , outputToStdout = True
3a9d784341454573b50b32fa1b494e7418df3086Christian Maeder , caslAmalg = [Cell]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | every 'Flag' describes an option (see usage info)
2353f65833a3da763392f771223250cd50b8d873Christian Maederdata Flag = Verbose Int
2353f65833a3da763392f771223250cd50b8d873Christian Maeder | Gui GuiType
2353f65833a3da763392f771223250cd50b8d873Christian Maeder | Analysis AnaType
2353f65833a3da763392f771223250cd50b8d873Christian Maeder | DefaultLogic String
2353f65833a3da763392f771223250cd50b8d873Christian Maeder | InType InType
2353f65833a3da763392f771223250cd50b8d873Christian Maeder | LibDir FilePath
2353f65833a3da763392f771223250cd50b8d873Christian Maeder | OutDir FilePath
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder | OutTypes [OutType]
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder | Specs [SIMPLE_ID]
2353f65833a3da763392f771223250cd50b8d873Christian Maeder | Raw [RawOpt]
2353f65833a3da763392f771223250cd50b8d873Christian Maeder | CASLAmalg [CASLAmalgOpt]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'AnaType' describes the type of analysis to be performed
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederdata AnaType = Basic | Structured | Skip
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance Show AnaType where
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder show a = case a of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Structured -> showOpt structS
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Skip -> showOpt skipS
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'GuiType' determines if we want the GUI shown
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederdata GuiType = Only | Also | Not
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance Show GuiType where
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder show g = case g of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Only -> showOpt onlyGuiS
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Also -> showOpt guiS
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'InType' describes the type of input the infile contains
2353f65833a3da763392f771223250cd50b8d873Christian Maederdata InType = ATermIn ATType | ASTreeIn ATType | CASLIn | HetCASLIn | OWL_DLIn
fdac680252d7347858bd67b4c2a2aaa52e623815Christian Maeder | HaskellIn | PrfIn | OmdocIn | GuessIn
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance Show InType where
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder show i = case i of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ATermIn at -> genTermS ++ show at
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ASTreeIn at -> astS ++ show at
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder CASLIn -> "casl"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder HetCASLIn -> "het"
4b1833c7d3af466e6bcba24f16304e0a78e8da87Christian Maeder OWL_DLIn -> "owl"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder HaskellIn -> "hs"
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder PrfIn -> prfS
fdac680252d7347858bd67b4c2a2aaa52e623815Christian Maeder OmdocIn -> omdocS
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder GuessIn -> ""
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- maybe this optional tree prefix can be omitted
2353f65833a3da763392f771223250cd50b8d873Christian Maederinstance Read InType where
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder readsPrec _ = readShowAux $ map ( \ i -> (show i, i))
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder (plainInTypes ++ aInTypes)
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder ++ [(treeS ++ genTermS ++ show at, ATermIn at)
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder | at <- [BAF, NonBAF]]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'ATType' describes distinct types of ATerms
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederdata ATType = BAF | NonBAF
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance Show ATType where
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder show a = case a of BAF -> bafS
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederplainInTypes :: [InType]
fdac680252d7347858bd67b4c2a2aaa52e623815Christian MaederplainInTypes = [CASLIn, HetCASLIn, OWL_DLIn, HaskellIn, PrfIn, OmdocIn]
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederaInTypes :: [InType]
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederaInTypes = [ f x | f <- [ASTreeIn, ATermIn], x <- [BAF, NonBAF] ]
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettichdata SPFType = ConsistencyCheck | OnlyAxioms
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettichinstance Show SPFType where
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich show x = case x of
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich ConsistencyCheck -> cS
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich OnlyAxioms -> ""
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus LuettichspfTypes :: [SPFType]
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus LuettichspfTypes = [ConsistencyCheck, OnlyAxioms]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'OutType' describes the type of outputs that we want to generate
2353f65833a3da763392f771223250cd50b8d873Christian Maederdata OutType = PrettyOut PrettyType
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder | HetCASLOut HetOutType HetOutFormat
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder | GraphOut GraphType
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder | ThyFile -- isabelle theory file
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich | DfgFile SPFType -- SPASS input file
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder | ComptableXml
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder | SigFile Delta -- signature as text
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder | TheoryFile Delta -- signature with sentences as text
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance Show OutType where
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder show o = case o of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder PrettyOut p -> ppS ++ show p
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder HetCASLOut h f -> show h ++ "." ++ show f
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder GraphOut f -> graphS ++ show f
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder EnvOut -> envS
fdac680252d7347858bd67b4c2a2aaa52e623815Christian Maeder OmdocOut -> omdocS
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian Maeder ThyFile -> "thy"
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich DfgFile t -> dfgS ++ show t
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian Maeder ComptableXml -> "comptable.xml"
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian Maeder SigFile d -> "sig" ++ show d
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian Maeder TheoryFile d -> "th" ++ show d
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian MaederplainOutTypeList :: [OutType]
fdac680252d7347858bd67b4c2a2aaa52e623815Christian MaederplainOutTypeList = [Prf, EnvOut, OmdocOut, ThyFile, ComptableXml]
beff4152e9f0fe90885458d1a1733b183a2a8816Christian MaederoutTypeList :: [OutType]
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian MaederoutTypeList = let dl = [Delta, Fully] in
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian Maeder plainOutTypeList
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder ++ [ PrettyOut p | p <- prettyList ]
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder ++ [ SigFile d | d <- dl ]
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder ++ [ TheoryFile d | d <- dl ]
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich ++ [ DfgFile x | x <- spfTypes]
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder ++ [ HetCASLOut h f | h <- OutASTree : hetOutTypeList, f <- formatList ]
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder ++ [ GraphOut f | f <- graphList ]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance Read OutType where
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder readsPrec _ = readShowAux $ map ( \ o -> (show o, o)) outTypeList
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder ++ [(show h ++ naxS ++ "." ++ show f, HetCASLOut h f)
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder | h <- hetOutTypeList, f <- formatList ]
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maederdata Delta = Delta | Fully
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maederinstance Show Delta where
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder show d = case d of
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder Delta -> deltaS
2353f65833a3da763392f771223250cd50b8d873Christian Maeder-- | 'PrettyType' describes the type of output we want the pretty-printer
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- to generate
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederdata PrettyType = PrettyAscii | PrettyLatex | PrettyHtml
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance Show PrettyType where
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder show p = case p of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder PrettyAscii -> "het"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder PrettyLatex -> "tex"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder PrettyHtml -> "html"
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederprettyList :: [PrettyType]
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederprettyList = [PrettyAscii, PrettyLatex, PrettyHtml]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'HetOutType' describes the type of Output we want Hets to create
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederdata HetOutType = OutASTree | OutDGraph Flattening Bool
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance Show HetOutType where
2353f65833a3da763392f771223250cd50b8d873Christian Maeder show h = case h of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder OutASTree -> astS
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder OutDGraph f b -> show f ++ "dg" ++ if b then naxS else ""
beff4152e9f0fe90885458d1a1733b183a2a8816Christian MaederhetOutTypeList :: [HetOutType]
beff4152e9f0fe90885458d1a1733b183a2a8816Christian MaederhetOutTypeList = [ OutDGraph f False | f <- [ Flattened, HidingOutside, Full]]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'Flattening' describes how flat the Earth really is (TODO: add comment)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederdata Flattening = Flattened | HidingOutside | Full
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance Show Flattening where
2353f65833a3da763392f771223250cd50b8d873Christian Maeder show f = case f of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Flattened -> "f"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder HidingOutside -> "h"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'HetOutFormat' describes the format of Output that HetCASL shall create
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederdata HetOutFormat = OutAscii | OutTerm | OutTaf | OutHtml | OutXml
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance Show HetOutFormat where
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder show f = case f of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder OutAscii -> "het"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder OutTerm -> "trm"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder OutTaf -> "taf"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder OutHtml -> "html"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder OutXml -> "xml"
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederformatList :: [HetOutFormat]
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederformatList = [OutAscii, OutTerm, OutTaf, OutHtml, OutXml]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'GraphType' describes the type of Graph that we want generated
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederdata GraphType = Dot | PostScript | Davinci
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance Show GraphType where
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder show g = case g of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder PostScript -> "ps"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Davinci -> "davinci"
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedergraphList :: [GraphType]
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedergraphList = [Dot, PostScript, Davinci]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'RawOpt' describes the options we want to be passed to the Pretty-Printer
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederdata RawOpt = RawAscii String | RawLatex String
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederinstance Show RawOpt where
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder show r = case r of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder RawAscii s -> showRawOpt asciiS s
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder RawLatex s -> showRawOpt latexS s
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder where showRawOpt f = showEqOpt (rawS ++ "=" ++ f)
2353f65833a3da763392f771223250cd50b8d873Christian Maeder-- | 'options' describes all available options and is used to generate usage
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- information
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederoptions :: [OptDescr Flag]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder [ Option ['v'] [verboseS] (OptArg parseVerbosity "Int")
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder "set verbosity level, -v1 is the default"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , Option ['q'] ["quiet"] (NoArg Quiet)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder "same as -v0, no output at all to stdout"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , Option ['V'] ["version"] (NoArg Version)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder "print version number and exit"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , Option ['h'] ["help", "usage"] (NoArg Help)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder "print usage information and exit"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , Option ['g'] [guiS] (NoArg (Gui Also))
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder "show graphical output in a GUI window"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , Option ['G'] [onlyGuiS] (NoArg $ Gui Only)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder "like -g but write no output files"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , Option ['p'] [skipS] (NoArg $ Analysis Skip)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder "skip static analysis, just parse"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , Option ['s'] [structS] (NoArg $ Analysis Structured)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder "skip basic, just do structured analysis"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , Option ['l'] ["logic"] (ReqArg DefaultLogic "LOGIC")
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder "choose initial logic, the default is CASL"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , Option ['L'] [libdirS] (ReqArg LibDir "DIR")
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder "source directory of [Het]CASL libraries"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , Option ['i'] [intypeS] (ReqArg parseInType "ITYPE")
2353f65833a3da763392f771223250cd50b8d873Christian Maeder ("input file type can be one of:" ++ crS ++ joinBar
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (map show plainInTypes ++
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder map (++ bracket bafS) [astS, bracket treeS ++ genTermS]))
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , Option ['O'] [outdirS] (ReqArg OutDir "DIR")
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder "destination directory for output files"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , Option ['o'] [outtypesS] (ReqArg parseOutTypes "OTYPES")
4a2f7efdf67dfcda0946f1b6373f41976ddea7a4Christian Maeder ("output file types, default nothing," ++ crS ++
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian Maeder listS ++ crS ++ concatMap ( \ t -> bS ++ show t ++ crS)
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian Maeder plainOutTypeList
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder ++ bS ++ joinBar (map show [SigFile Fully,
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder TheoryFile Fully])
3490b73f69b58ab742417b0867d0e2d4a7778cc0Christian Maeder ++ bracket deltaS ++ crS
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder ++ bS ++ ppS ++ joinBar (map show prettyList) ++ crS
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder ++ bS ++ graphS ++ joinBar (map show graphList) ++ crS
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder ++ bS ++ astS ++ formS ++ crS
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich ++ bS ++ joinBar (map show hetOutTypeList) ++ bracket naxS ++formS++crS
8a5c05062ef501bf725a86a370a5145a198e81fdKlaus Luettich ++ bS ++ dfgS ++ bracket cS)
083bc1972a66d73749760eab3a90bf4eb9ca7951Christian Maeder , Option ['R'] [recursiveS] (NoArg Recurse)
083bc1972a66d73749760eab3a90bf4eb9ca7951Christian Maeder "output also imported libraries"
083bc1972a66d73749760eab3a90bf4eb9ca7951Christian Maeder , Option ['n'] [specS] (ReqArg parseSpecOpts "NSPECS")
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder ("process specs option " ++ crS ++ listS ++ " SIMPLE-ID")
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , Option ['r'] [rawS] (ReqArg parseRawOpts "RAW")
2353f65833a3da763392f771223250cd50b8d873Christian Maeder ("raw options for pretty printing" ++ crS ++ "RAW is "
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder ++ joinBar [asciiS, textS, latexS, texS]
2353f65833a3da763392f771223250cd50b8d873Christian Maeder ++ "=STRING where " ++ crS ++
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder "STRING is passed to the appropriate printer")
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , Option ['a'] [amalgS] (ReqArg parseCASLAmalg "ANALYSIS")
2353f65833a3da763392f771223250cd50b8d873Christian Maeder ("CASL amalgamability analysis options" ++ crS ++ listS ++
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder crS ++ joinBar (map show caslAmalgOpts))
2353f65833a3da763392f771223250cd50b8d873Christian Maeder ] where listS = "is a comma-separated list without blanks"
3a9d784341454573b50b32fa1b494e7418df3086Christian Maeder ++ crS ++ "of one or more from:"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder joinBar l = "(" ++ joinWith '|' l ++ ")"
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder formS = '.' : joinBar (map show formatList)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- parser functions returning Flags --
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'parseVerbosity' parses a 'Verbose' Flag from user input
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederparseVerbosity :: (Maybe String) -> Flag
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederparseVerbosity Nothing = Verbose 2
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederparseVerbosity (Just s)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder = case reads s of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder [(i,"")] -> Verbose i
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder _ -> hetsError (s ++ " is not a valid INT")
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | intypes useable for downloads
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederdownloadExtensions :: [String]
9dd71ac51c9a6e72bcb126224f9c64131698b636Christian MaederdownloadExtensions = map ('.' :) $
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder map show plainInTypes
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder ++ map ((treeS ++) . show) [ATermIn BAF, ATermIn NonBAF]
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder ++ map show aInTypes
0ea2cddb8715a770e646895e16b7b8085f49167cChristian Maeder-- | remove the extension from a file
0ea2cddb8715a770e646895e16b7b8085f49167cChristian MaederrmSuffix :: FilePath -> FilePath
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian MaederrmSuffix = fst . stripSuffix (envSuffix : downloadExtensions)
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian Maeder-- | the suffix of env files
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian MaederenvSuffix :: String
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian MaederenvSuffix = '.' : envS
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder-- | the suffix of env files
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian MaederprfSuffix :: String
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian MaederprfSuffix = '.' : prfS
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder-- checks if a source file for the given file name exists
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian MaederexistsAnSource :: HetcatsOpts -> FilePath -> IO (Maybe FilePath)
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian MaederexistsAnSource opts file = do
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder let base = rmSuffix file
beff4152e9f0fe90885458d1a1733b183a2a8816Christian Maeder exts = case intype opts of
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder GuessIn -> downloadExtensions
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder e@(ATermIn _) -> ['.' : show e, '.' : treeS ++ show e]
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder e -> ['.' : show e]
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian Maeder names = file : map (base ++) (exts ++ [envSuffix])
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -- look for the first existing file
2353f65833a3da763392f771223250cd50b8d873Christian Maeder validFlags <- mapM checkInFile names
2353f65833a3da763392f771223250cd50b8d873Christian Maeder return (find fst (zip validFlags names) >>= (return . snd))
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder-- | should env be written
9d6562465b41f17c7967d4e5678f34811d958cb2Christian MaederhasEnvOut :: HetcatsOpts -> Bool
daec53c285f692c56db0cefe16061b46ba602cf0Christian MaederhasEnvOut = any ( \ o -> case o of
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder EnvOut -> True
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder _ -> False) . outtypes
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder-- | should prf be written
daec53c285f692c56db0cefe16061b46ba602cf0Christian MaederisPrfOut :: OutType -> Bool
daec53c285f692c56db0cefe16061b46ba602cf0Christian MaederisPrfOut o = case o of
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder-- | should prf be written
daec53c285f692c56db0cefe16061b46ba602cf0Christian MaederhasPrfOut :: HetcatsOpts -> Bool
daec53c285f692c56db0cefe16061b46ba602cf0Christian MaederhasPrfOut = any isPrfOut . outtypes
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder-- | remove prf writing
daec53c285f692c56db0cefe16061b46ba602cf0Christian MaederremovePrfOut :: HetcatsOpts -> HetcatsOpts
daec53c285f692c56db0cefe16061b46ba602cf0Christian MaederremovePrfOut opts = opts { outtypes = filter (not . isPrfOut)
daec53c285f692c56db0cefe16061b46ba602cf0Christian Maeder $ outtypes opts }
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian Maeder-- gets two Paths and checks if the first file is not older than the
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian Maeder-- second one and should return True for two identical files
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian MaedercheckRecentEnv :: HetcatsOpts -> FilePath -> FilePath -> IO Bool
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian MaedercheckRecentEnv opts fp1 base2 =
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder do fp1_valid <- checkInFile fp1
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder if not fp1_valid then return False
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder maybe_source_file <- existsAnSource opts base2
2353f65833a3da763392f771223250cd50b8d873Christian Maeder maybe (return False)
3a9d784341454573b50b32fa1b494e7418df3086Christian Maeder (\ fp2 -> do fp1_time <- getModificationTime fp1
3a9d784341454573b50b32fa1b494e7418df3086Christian Maeder fp2_time <- getModificationTime fp2
7245138e91992b96b153b8ac527e263d9dc8ff5bChristian Maeder return (fp1_time >= fp2_time))
3a9d784341454573b50b32fa1b494e7418df3086Christian Maeder maybe_source_file
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'parseInType' parses an 'InType' Flag from user input
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederparseInType :: String -> Flag
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederparseInType = InType . parseInType1
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'parseInType1' parses an 'InType' Flag from a String
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederparseInType1 :: String -> InType
2353f65833a3da763392f771223250cd50b8d873Christian MaederparseInType1 str =
2353f65833a3da763392f771223250cd50b8d873Christian Maeder case reads str of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder [(t, "")] -> t
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder _ -> hetsError (str ++ " is not a valid ITYPE")
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder {- the mere typo read instead of reads caused the runtime error:
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Fail: Prelude.read: no parse -}
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- 'parseOutTypes' parses an 'OutTypes' Flag from user input
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederparseOutTypes :: String -> Flag
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederparseOutTypes str = case reads $ bracket str of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder [(l, "")] -> OutTypes l
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder _ -> hetsError (str ++ " is not a valid OTYPES")
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian Maeder-- | 'parseSpecOpts' parses a 'Specs' Flag from user input
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian MaederparseSpecOpts :: String -> Flag
f39b8dd9651dfcc38b06191cda23cacbfc298323Christian MaederparseSpecOpts s = Specs $ map mkSimpleId $ splitOn ',' s
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'parseRawOpts' parses a 'Raw' Flag from user input
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederparseRawOpts :: String -> Flag
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederparseRawOpts s =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let (prefix, string) = break (== '=') s
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder parsePrefix p = if p `elem` [asciiS, textS] then RawAscii
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder else if p `elem` [latexS, texS] then RawLatex
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder else hetsError (s ++ " is not a valid RAW String")
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder in Raw [(parsePrefix prefix) (drop 1 string)]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | guesses the InType
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederguess :: String -> InType -> InType
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederguess file GuessIn = guessInType file
b53688bfed888214b485cf76439d57262d80e0a7Christian Maederguess _file itype = itype
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'guessInType' parses an 'InType' from the FilePath to our 'InFile'
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederguessInType :: FilePath -> InType
2353f65833a3da763392f771223250cd50b8d873Christian MaederguessInType file =
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder case fileparse downloadExtensions file of
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder (_,_,Just ('.' : suf)) -> parseInType1 suf
3bcd9d942601d59dd55a6069d8b2d1c33d7ced0eChristian Maeder (_,_,_) -> GuessIn
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'parseCASLAmalg' parses CASL amalgamability options
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederparseCASLAmalg :: String -> Flag
2353f65833a3da763392f771223250cd50b8d873Christian MaederparseCASLAmalg str =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder case reads $ bracket str of
2353f65833a3da763392f771223250cd50b8d873Christian Maeder [(l, "")] -> CASLAmalg $ filter ( \ o -> case o of
2353f65833a3da763392f771223250cd50b8d873Christian Maeder NoAnalysis -> False
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder _ -> True ) l
2353f65833a3da763392f771223250cd50b8d873Christian Maeder _ -> hetsError (str ++
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder " is not a valid CASL amalgamability analysis option list")
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- main functions --
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'hetcatsOpts' parses sensible HetcatsOpts from ARGV
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederhetcatsOpts :: [String] -> IO HetcatsOpts
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederhetcatsOpts argv =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let argv' = filter (not . isUni) argv
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder isUni s = take 5 s == "--uni"
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder in case (getOpt Permute options argv') of
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (opts,non_opts,[]) ->
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder do flags <- checkFlags opts
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder infs <- checkInFiles non_opts
2353f65833a3da763392f771223250cd50b8d873Christian Maeder hcOpts <- return $
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder foldr (flip makeOpts) defaultHetcatsOpts flags
3a9d784341454573b50b32fa1b494e7418df3086Christian Maeder let hcOpts' = hcOpts { infiles = infs }
2353f65833a3da763392f771223250cd50b8d873Christian Maeder seq (length $ show hcOpts') $ return $ hcOpts'
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder (_,_,errs) -> hetsError (concat errs)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'checkFlags' checks all parsed Flags for sanity
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercheckFlags :: [Flag] -> IO [Flag]
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercheckFlags fs =
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder let collectFlags = (collectDirs
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder . collectOutTypes
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder . collectVerbosity
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder . collectRawOpts
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder . collectSpecOpts
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder -- collect some more here?
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder in do if not $ null [ () | Help <- fs]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder then do putStrLn hetsUsage
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder exitWith ExitSuccess
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder else return [] -- fall through
2353f65833a3da763392f771223250cd50b8d873Christian Maeder if not $ null [ () | Version <- fs]
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder then do putStrLn ("version of hets: " ++ hetcats_version)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder exitWith ExitSuccess
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder else return [] -- fall through
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder fs' <- collectFlags fs
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'checkInFiles' checks all given InFiles for sanity
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercheckInFiles :: [String] -> IO [FilePath]
2353f65833a3da763392f771223250cd50b8d873Christian MaedercheckInFiles fs =
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder [] -> hetsError "No valid input file specified"
2353f65833a3da763392f771223250cd50b8d873Christian Maeder let ifs = filter (not . checkUri) fs
2353f65833a3da763392f771223250cd50b8d873Christian Maeder efs = filter hasExtension ifs
2353f65833a3da763392f771223250cd50b8d873Christian Maeder hasExtension f = any ( \ e -> isSuffixOf e f)
2353f65833a3da763392f771223250cd50b8d873Christian Maeder downloadExtensions
2353f65833a3da763392f771223250cd50b8d873Christian Maeder bs <- mapM checkInFile efs
2353f65833a3da763392f771223250cd50b8d873Christian Maeder then return fs
2353f65833a3da763392f771223250cd50b8d873Christian Maeder else hetsError $ "invalid input files: " ++
2353f65833a3da763392f771223250cd50b8d873Christian Maeder (unwords $ map snd $ filter (not . fst) $ zip bs efs)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- auxiliary functions: FileSystem interaction --
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'checkInFile' checks a single InFile for sanity
2353f65833a3da763392f771223250cd50b8d873Christian MaedercheckInFile :: FilePath -> IO Bool
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercheckInFile file =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder do exists <- doesFileExist file
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder perms <- catch (getPermissions file) (\_ -> return noPerms)
2353f65833a3da763392f771223250cd50b8d873Christian Maeder return $ exists && readable perms
2353f65833a3da763392f771223250cd50b8d873Christian Maeder-- | check if infile is uri
4b1833c7d3af466e6bcba24f16304e0a78e8da87Christian MaedercheckUri :: FilePath -> Bool
4b1833c7d3af466e6bcba24f16304e0a78e8da87Christian MaedercheckUri file = let (_, t) = span (/=':') file in
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder if length t < 4 then False
e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder else let (_:c2:c3:_) = t in
2353f65833a3da763392f771223250cd50b8d873Christian Maeder if c2 == '/' && c3 == '/' then True
4b1833c7d3af466e6bcba24f16304e0a78e8da87Christian Maeder -- (http://, https://, ftp://, file://, etc.)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'checkOutDirs' checks a list of OutDir for sanity
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercheckOutDirs :: [Flag] -> IO [Flag]
2353f65833a3da763392f771223250cd50b8d873Christian MaedercheckOutDirs fs = do
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder [] -> return ()
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder [f] -> checkOutDir f
2353f65833a3da763392f771223250cd50b8d873Christian Maeder _ -> hetsError
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder "Only one output directory may be specified on the command line"
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder-- | 'checkLibDirs' checks a list of LibDir for sanity
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian MaedercheckLibDirs :: [Flag] -> IO [Flag]
2353f65833a3da763392f771223250cd50b8d873Christian MaedercheckLibDirs fs = do
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder s <- catch (getEnv "HETS_LIB") (const $ return "")
2353f65833a3da763392f771223250cd50b8d873Christian Maeder if null s then return [] else do
2353f65833a3da763392f771223250cd50b8d873Christian Maeder let d = LibDir s
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder checkLibDir d
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder [f] -> checkLibDir f >> return fs
2353f65833a3da763392f771223250cd50b8d873Christian Maeder _ -> hetsError
9d6562465b41f17c7967d4e5678f34811d958cb2Christian Maeder "Only one library directory may be specified on the command line"
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder-- | 'checkLibDir' checks a single LibDir for sanity
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian MaedercheckLibDir :: Flag -> IO ()
2353f65833a3da763392f771223250cd50b8d873Christian MaedercheckLibDir (LibDir file) =
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder do exists <- doesDirectoryExist file
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder perms <- catch (getPermissions file) (\_ -> return noPerms)
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder if exists && readable perms then return ()
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder else hetsError $ "Not a valid library directory: " ++ file
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian MaedercheckLibDir _ = return ()
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'checkOutDir' checks a single OutDir for sanity
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian MaedercheckOutDir :: Flag -> IO ()
2353f65833a3da763392f771223250cd50b8d873Christian MaedercheckOutDir (OutDir file) =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder do exists <- doesDirectoryExist file
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder perms <- catch (getPermissions file) (\_ -> return noPerms)
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder if exists && writable perms then return ()
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder else hetsError $ "Not a valid output directory: " ++ file
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian MaedercheckOutDir _ = return ()
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- Nil Permissions. Returned, if an Error occurred in FS-Interaction
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedernoPerms :: Permissions
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedernoPerms = Permissions { readable = False
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , writable = False
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , executable = False
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder , searchable = False
2353f65833a3da763392f771223250cd50b8d873Christian Maeder-- auxiliary functions: collect flags --
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian MaedercollectDirs :: [Flag] -> IO [Flag]
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian MaedercollectDirs fs =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let (ods,fs') = partition isOutDir fs
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder (lds,fs'') = partition isLibDir fs'
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder isOutDir (OutDir _) = True
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder isOutDir _ = False
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder isLibDir (LibDir _) = True
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder isLibDir _ = False
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder in do ods' <- checkOutDirs ods
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder lds' <- checkLibDirs lds
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder return $ ods' ++ lds' ++ fs''
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercollectVerbosity :: [Flag] -> [Flag]
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercollectVerbosity fs =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let (vs,fs') = partition isVerb fs
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder verbosity = (sum . map (\(Verbose x) -> x)) vs
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder isVerb (Verbose _) = True
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder isVerb _ = False
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder vfs = Verbose verbosity : fs'
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder in if not $ null [() | Quiet <- fs'] then Verbose 0 : fs' else
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder if null vs then Verbose 1 : fs' else vfs
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercollectOutTypes :: [Flag] -> [Flag]
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercollectOutTypes fs =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let (ots,fs') = partition isOType fs
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder isOType (OutTypes _) = True
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder isOType _ = False
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder otypes = foldl concatOTypes [] ots
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder concatOTypes = (\os (OutTypes ot) -> os ++ ot)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder in if null otypes || not (null [() | Gui Only <- fs'])
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder else ((OutTypes otypes):fs')
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercollectRawOpts :: [Flag] -> [Flag]
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedercollectRawOpts fs =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder let (rfs,fs') = partition isRawOpt fs
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder isRawOpt (Raw _) = True
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder isRawOpt _ = False
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder raws = foldl concatRawOpts [] rfs
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder concatRawOpts = (\os (Raw ot) -> os ++ ot)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder in if (null raws) then fs' else ((Raw raws):fs')
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian MaedercollectSpecOpts :: [Flag] -> [Flag]
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian MaedercollectSpecOpts fs =
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder let (rfs,fs') = partition isSpecOpt fs
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder isSpecOpt (Specs _) = True
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder isSpecOpt _ = False
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder specs = foldl concatSpecOpts [] rfs
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder concatSpecOpts = (\os (Specs ot) -> os ++ ot)
c5a4c5f506ea34fa527065b4187127a18c6e2418Christian Maeder in if null specs then fs' else (Specs specs : fs')
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- auxiliary functions: error messages --
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'hetsError' is a generic Error messaging function that prints the Error
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- and usage information, if the user caused the Error
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederhetsError :: String -> a
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederhetsError errorString = error (errorString ++ "\n" ++ hetsUsage)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | 'hetsUsage' generates usage information for the commandline
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederhetsUsage :: String
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederhetsUsage = usageInfo header options
d01f5008234242395b1eac85792fd703acf755d9Christian Maeder where header = "Usage: hets [OPTION...] file ... file [+RTS -?]"
2353f65833a3da763392f771223250cd50b8d873Christian Maeder-- | 'putIfVerbose' prints a given String to StdOut when the given HetcatsOpts'
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- Verbosity exceeds the given level
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederputIfVerbose :: HetcatsOpts -> Int -> String -> IO ()
2353f65833a3da763392f771223250cd50b8d873Christian MaederputIfVerbose opts level str =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder if outputToStdout opts
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder then doIfVerbose opts level (putStrLn str)
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder else return()
2353f65833a3da763392f771223250cd50b8d873Christian Maeder-- | 'doIfVerbose' executes a given function when the given HetcatsOpts'
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- Verbosity exceeds the given level
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederdoIfVerbose :: HetcatsOpts -> Int -> (IO ()) -> IO ()
b53688bfed888214b485cf76439d57262d80e0a7Christian MaederdoIfVerbose opts level func =
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder if (verbose opts) >= level then func
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder else return ()
a1c6679d00e15a949730ab640159e0adc5b0e3e7Christian Maeder-- | add base file name (second argument) to path
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian MaederpathAndBase :: FilePath -> FilePath -> FilePath
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian MaederpathAndBase path base =
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder if null path then base
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder else if last path == '/' then path ++ base
7968d3a131e5a684ec1ff0c6d88aae638549153dChristian Maeder else path ++ "/" ++ base
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | show diagnostic messages (see Result.hs), according to verbosity level
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedershowDiags :: HetcatsOpts -> [Diagnosis] -> IO()
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedershowDiags opts ds = do
7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder runResultT $ showDiags1 opts $ liftR $ Result ds Nothing
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder-- | show diagnostic messages (see Result.hs), according to verbosity level
7f7460e7095628f3437b116ee78d3043d11f8febChristian MaedershowDiags1 :: HetcatsOpts -> ResultT IO a -> ResultT IO a
b53688bfed888214b485cf76439d57262d80e0a7Christian MaedershowDiags1 opts res = do
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder if outputToStdout opts
7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder then do Result ds res' <- lift $ runResultT res
7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder lift $ sequence $ map (putStrLn . show) -- take maxdiags
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder $ filter (relevantDiagKind . diagKind) ds
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder Just res'' -> return res''
7f7460e7095628f3437b116ee78d3043d11f8febChristian Maeder Nothing -> liftR $ Result [] Nothing
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder where relevantDiagKind Error = True
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder relevantDiagKind Warning = (verbose opts) >= 2
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder relevantDiagKind Hint = (verbose opts) >= 4
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder relevantDiagKind Debug = (verbose opts) >= 5
b53688bfed888214b485cf76439d57262d80e0a7Christian Maeder relevantDiagKind MessageW = False