{-# LANGUAGE CPP #-}

{- |

Module : $Header$

Description : Datatypes and functions for options that hets understands.

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

License : GPLv2 or higher, see LICENSE.txt

Maintainer : Christian.Maeder@dfki.de

Stability : provisional

Portability : portable

Datatypes for options that hets understands.

Useful functions to parse and check user-provided values.

-}

module Driver.Options

( HetcatsOpts (..)

, optionFlags

, makeOpts

, AnaType (..)

, GuiType (..)

, InType (..)

, OutType (..)

, PrettyType (..)

, prettyList

, GraphType (..)

, SPFType (..)

, ATType

, Delta

, hetcatsOpts

, isStructured

, guess

, rmSuffix

, envSuffix

, prfSuffix

, removePrfOut

, hasEnvOut

, hasPrfOut

, getFileNames

, existsAnSource

, getExtensions

, checkRecentEnv

, downloadExtensions

, defaultHetcatsOpts

, hetsVersion

, showDiags

, showDiags1

, putIfVerbose

, doDump

, checkUri

, defLogicIsDMU

, useCatalogURL

, hetsIOError

) where

import Driver.Version

import Common.Utils

import Common.IO

import Common.Id

import Common.Result

import Common.ResultT

import Common.Amalgamate

import Common.Keywords

import System.Directory

import System.Console.GetOpt

import System.Exit

import System.IO

import Control.Monad

import Control.Monad.Trans

import Data.Char

import Data.List

import Data.Maybe

-- | short version without date for ATC files

hetsVersion :: String

hetsVersion = takeWhile (/= ',') hetcats_version

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

useCatalogURL :: HetcatsOpts -> FilePath -> FilePath

useCatalogURL opts fname = case mapMaybe

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

$ urlCatalog opts of

m : _ -> m

_ -> fname

bracket :: String -> String

bracket s = "[" ++ s ++ "]"

-- use the same strings for parsing and printing!

verboseS, intypeS, outtypesS, skipS, justStructuredS, transS,

guiS, libdirsS, outdirS, amalgS, recursiveS, namedSpecsS,

interactiveS, modelSparQS, counterSparQS, connectS, xmlS, listenS,

applyAutomaticRuleS, normalFormS, unlitS :: String

modelSparQS = "modelSparQ"

counterSparQS = "counterSparQ"

verboseS = "verbose"

intypeS = "input-type"

outtypesS = "output-types"

skipS = "just-parse"

justStructuredS = "just-structured"

guiS = "gui"

libdirsS = "hets-libdirs"

outdirS = "output-dir"

amalgS = "casl-amalg"

namedSpecsS = "named-specs"

transS = "translation"

recursiveS = "recursive"

interactiveS = "interactive"

connectS = "connect"

xmlS = "xml"

listenS = "listen"

applyAutomaticRuleS = "apply-automatic-rule"

normalFormS = "normal-form"

unlitS = "unlit"

urlCatalogS :: String

urlCatalogS = "url-catalog"

relposS :: String

relposS = "relative-positions"

fullSignS :: String

fullSignS = "full-signatures"

fullTheoriesS :: String

fullTheoriesS = "full-theories"

logicGraphS :: String

logicGraphS = "logic-graph"

fileTypeS :: String

fileTypeS = "file-type"

blacklistS :: String

blacklistS = "blacklist"

whitelistS :: String

whitelistS = "whitelist"

genTermS, treeS, bafS :: String

genTermS = "gen_trm"

treeS = "tree."

bafS = ".baf"

graphS, ppS, envS, deltaS, prfS, omdocS, hsS, experimentalS :: String

graphS = "graph."

ppS = "pp."

envS = "env"

deltaS = ".delta"

prfS = "prf"

omdocS = "omdoc"

hsS = "hs"

experimentalS = "exp"

tptpS, dfgS, cS :: String

tptpS = "tptp"

dfgS = "dfg"

cS = ".c"

showOpt :: String -> String

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

showEqOpt :: String -> String -> String

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

-- main Datatypes --

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

data HetcatsOpts = HcOpt -- for comments see usage info

{ analysis :: AnaType

, guiType :: GuiType

, urlCatalog :: [(String, String)]

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

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

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

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

, intype :: InType

, libdirs :: [FilePath]

, modelSparQ :: FilePath

, counterSparQ :: Int

, outdir :: FilePath

, outtypes :: [OutType]

, xupdate :: FilePath

, recurse :: Bool

, verbose :: Int

, defLogic :: String

, defSyntax :: String

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

, caslAmalg :: [CASLAmalgOpt]

, interactive :: Bool

, connectP :: Int

, connectH :: String

, uncolored :: Bool

, xmlFlag :: Bool

, applyAutomatic :: Bool

, computeNormalForm :: Bool

, dumpOpts :: [String]

, ioEncoding :: Enc

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

, useLibPos :: Bool

, unlit :: Bool

, serve :: Bool

, listen :: Int

, whitelist :: [[String]]

, blacklist :: [[String]]

, runMMT :: Bool

, fullTheories :: Bool

, outputLogicGraph :: Bool

, fileType :: Bool

, fullSign :: Bool }

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

basic values when the user specifies nothing else -}

defaultHetcatsOpts :: HetcatsOpts

defaultHetcatsOpts = HcOpt

{ analysis = Basic

, guiType = NoGui

, urlCatalog = []

, infiles = []

, specNames = []

, transNames = []

, viewNames = []

, intype = GuessIn

, libdirs = []

, modelSparQ = ""

, counterSparQ = 3

, outdir = ""

, outtypes = [] -- no default

, xupdate = ""

, recurse = False

, defLogic = "CASL"

, defSyntax = ""

, verbose = 1

, outputToStdout = True

, caslAmalg = [Cell]

, interactive = False

, connectP = -1

, connectH = ""

, uncolored = False

, xmlFlag = False

, applyAutomatic = False

, computeNormalForm = False

, dumpOpts = []

, ioEncoding = Utf8

, useLibPos = False

, unlit = False

, serve = False

, listen = -1

, whitelist = []

, blacklist = []

, runMMT = False

, fullTheories = False

, outputLogicGraph = False

, fileType = False

, fullSign = False }

instance Show HetcatsOpts where

show opts =

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

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

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

in

showEqOpt verboseS (show $ verbose opts)

++ show (guiType opts)

++ showFlag outputLogicGraph logicGraphS

++ showFlag fileType fileTypeS

++ showFlag interactive interactiveS

++ show (analysis opts)

++ case defLogic opts of

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

_ -> ""

++ case defSyntax opts of

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

_ -> ""

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

++ case modelSparQ opts of

"" -> ""

f -> showEqOpt modelSparQS f

++ case counterSparQ opts of

n | n /= counterSparQ defaultHetcatsOpts

-> showEqOpt counterSparQS $ show n

_ -> ""

++ showFlag xmlFlag xmlS

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

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

++ showIPLists whitelist whitelistS

++ showIPLists blacklist blacklistS

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

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

++ showFlag unlit unlitS

++ showFlag useLibPos relposS

++ showFlag fullSign fullSignS

++ showFlag fullTheories fullTheoriesS

++ case urlCatalog opts of

[] -> ""

cs -> showEqOpt urlCatalogS $ intercalate ","

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

++ showEqOpt intypeS (show $ intype opts)

++ showEqOpt outdirS (outdir opts)

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

++ showFlag recurse recursiveS

++ showFlag applyAutomatic applyAutomaticRuleS

++ showFlag computeNormalForm normalFormS

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

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

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

++ showEqOpt amalgS (tail $ init $ show $

case caslAmalg opts of

[] -> [NoAnalysis]

l -> l)

++ " " ++ unwords (infiles opts)

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

data Flag =

Verbose Int

| Quiet

| Uncolored

| Version

| Recurse

| ApplyAutomatic

| NormalForm

| Help

| Gui GuiType

| Analysis AnaType

| DefaultLogic String

| DefaultSyntax String

| InType InType

| LibDirs String

| OutDir FilePath

| XUpdate FilePath

| ModelSparQ FilePath

| CounterSparQ Int

| OutTypes [OutType]

| Specs [SIMPLE_ID]

| Trans [SIMPLE_ID]

| Views [SIMPLE_ID]

| CASLAmalg [CASLAmalgOpt]

| Interactive

| Connect Int String

| XML

| Dump String

| IOEncoding Enc

| Unlit

| RelPos

| Serve

| Listen Int

| Whitelist String

| Blacklist String

| UseMMT

| FullTheories

| FullSign

| OutputLogicGraph

| FileType

| UrlCatalog [(String, String)]

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

makeOpts :: HetcatsOpts -> Flag -> HetcatsOpts

makeOpts opts flg =

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

in case flg of

Interactive -> opts { interactive = True }

XML -> opts { xmlFlag = True }

Listen x -> opts { listen = x }

Blacklist x -> opts { blacklist = splitIPs x }

Whitelist x -> opts { whitelist = splitIPs x }

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

Analysis x -> opts { analysis = x }

Gui x -> opts { guiType = x }

InType x -> opts { intype = x }

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

ModelSparQ x -> opts { modelSparQ = x }

CounterSparQ x -> opts { counterSparQ = x }

OutDir x -> opts { outdir = x }

OutTypes x -> opts { outtypes = x }

XUpdate x -> opts { xupdate = x }

Recurse -> opts { recurse = True }

ApplyAutomatic -> opts { applyAutomatic = True }

NormalForm -> opts { computeNormalForm = True }

Specs x -> opts { specNames = x }

Trans x -> opts { transNames = x }

Views x -> opts { viewNames = x }

Verbose x -> opts { verbose = x }

DefaultLogic x -> opts { defLogic = x }

DefaultSyntax x -> opts { defSyntax = x }

CASLAmalg x -> opts { caslAmalg = x }

Quiet -> opts { verbose = 0 }

Uncolored -> opts { uncolored = True }

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

IOEncoding e -> opts { ioEncoding = e }

Serve -> opts { serve = True }

Unlit -> opts { unlit = True }

RelPos -> opts { useLibPos = True }

UseMMT -> opts { runMMT = True }

FullTheories -> opts { fullTheories = True }

OutputLogicGraph -> opts { outputLogicGraph = True }

FileType -> opts { fileType = True }

FullSign -> opts { fullSign = True }

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

Help -> opts -- skipped

Version -> opts -- skipped

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

data AnaType = Basic | Structured | Skip

instance Show AnaType where

show a = case a of

Basic -> ""

Structured -> showOpt justStructuredS

Skip -> showOpt skipS

-- | check if structured analysis should be performed

isStructured :: HetcatsOpts -> Bool

isStructured a = case analysis a of

Structured -> True

_ -> False

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

data GuiType = UseGui | NoGui

deriving Eq

instance Show GuiType where

show g = case g of

UseGui -> showOpt guiS

NoGui -> ""

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

data InType =

ATermIn ATType

| CASLIn

| HetCASLIn

| DOLIn

| OWLIn

| OwlXmlIn

| OBOIn

| HaskellIn

| MaudeIn

| TwelfIn

| HolLightIn

| IsaIn

| ThyIn

| PrfIn

| OmdocIn

| ExperimentalIn -- ^ for testing new functionality

| ProofCommand

| GuessIn

| FreeCADIn

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

| DgXml

| RDFIn

| Xmi

| Qvt

| TPTPIn

| HtmlIn -- just to complain

deriving Eq

instance Show InType where

show i = case i of

ATermIn at -> genTermS ++ show at

CASLIn -> "casl"

HetCASLIn -> "het"

DOLIn -> "dol"

OwlXmlIn -> "owl.xml"

OWLIn -> "owl"

OBOIn -> "obo"

HaskellIn -> hsS

ExperimentalIn -> "exp"

MaudeIn -> "maude"

TwelfIn -> "elf"

HolLightIn -> "hol"

IsaIn -> "isa"

ThyIn -> "thy"

TPTPIn -> "tptp"

PrfIn -> prfS

OmdocIn -> omdocS

ProofCommand -> "hpf"

GuessIn -> ""

FreeCADIn -> "fcstd"

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

DgXml -> xmlS

RDFIn -> "rdf"

Xmi -> "xmi"

Qvt -> "qvt"

HtmlIn -> "html"

-- maybe this optional tree prefix can be omitted

instance Read InType where

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

(plainInTypes ++ aInTypes)

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

| at <- [BAF, NonBAF]]

-- | 'ATType' describes distinct types of ATerms

data ATType = BAF | NonBAF deriving Eq

instance Show ATType where

show a = case a of

BAF -> bafS

NonBAF -> ""

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

plainInTypes :: [InType]

plainInTypes =

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

, MaudeIn, TwelfIn

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

, CommonLogicIn False, CommonLogicIn True

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

aInTypes :: [InType]

aInTypes = [ ATermIn x | x <- [BAF, NonBAF] ]

data SPFType = ConsistencyCheck | ProveTheory

instance Show SPFType where

show x = case x of

ConsistencyCheck -> cS

ProveTheory -> ""

spfTypes :: [SPFType]

spfTypes = [ConsistencyCheck, ProveTheory]

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

data OutType =

PrettyOut PrettyType

| GraphOut GraphType

| Prf

| EnvOut

| OWLOut

| CLIFOut

| KIFOut

| OmdocOut

| XmlOut -- ^ development graph xml output

| ExperimentalOut -- ^ for testing new functionality

| HaskellOut

| FreeCADOut

| ThyFile -- ^ isabelle theory file

| DfgFile SPFType -- ^ SPASS input file

| TPTPFile SPFType

| ComptableXml

| SigFile Delta -- ^ signature as text

| TheoryFile Delta -- ^ signature with sentences as text

| RDFOut

| SymXml

| SymsXml

instance Show OutType where

show o = case o of

PrettyOut p -> ppS ++ show p

GraphOut f -> graphS ++ show f

Prf -> prfS

EnvOut -> envS

OWLOut -> "omn"

CLIFOut -> "clif"

KIFOut -> "kif"

OmdocOut -> omdocS

XmlOut -> xmlS

ExperimentalOut -> experimentalS

HaskellOut -> hsS

FreeCADOut -> "fcxml"

ThyFile -> "thy"

DfgFile t -> dfgS ++ show t

TPTPFile t -> tptpS ++ show t

ComptableXml -> "comptable.xml"

SigFile d -> "sig" ++ show d

TheoryFile d -> "th" ++ show d

RDFOut -> "nt"

SymXml -> "sym.xml"

SymsXml -> "syms.xml"

plainOutTypeList :: [OutType]

plainOutTypeList =

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

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

outTypeList :: [OutType]

outTypeList = let dl = [Delta, Fully] in

plainOutTypeList

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

++ [ SigFile d | d <- dl ]

++ [ TheoryFile d | d <- dl ]

++ [ DfgFile x | x <- spfTypes]

++ [ TPTPFile x | x <- spfTypes]

++ [ GraphOut f | f <- graphList ]

instance Read OutType where

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

data Delta = Delta | Fully

instance Show Delta where

show d = case d of

Delta -> deltaS

Fully -> ""

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

to generate -}

data PrettyType = PrettyAscii Bool | PrettyLatex Bool | PrettyXml | PrettyHtml

instance Show PrettyType where

show p = case p of

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

optionFlags :: [(String, Flag)]

optionFlags = drop 9 $ 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