module Utils.ArgumentParser (parseArgs, Args(..), ExampleFile(..), Config(..), NeedsFiles(..), DynamizeArgs(..), getConfigFile, writeConfigFile, removeConfigFile, actionSpecified)where

{-
This module defines parsing of the arguments and reading/writing of the config file
-}

import TypeSystem
import AssetsHelper as AH
import qualified Assets

import Utils.Utils
import Utils.PureIO hiding (writeFile, readFile, putStrLn)

import Data.Monoid ((<>))
import Data.List (intercalate, isPrefixOf, isSuffixOf)
import Data.Maybe
import qualified Data.Map as M

import SyntaxHighlighting.AsHTMLPt (cssFor)
import SyntaxHighlighting.Coloring

import Control.Monad

import Options.Applicative

import System.Directory
import System.Exit

import Assets
import qualified Data.ByteString as B




descriptionText	= "ALGT (Automated Language Generation Tool)- automatically parse, interpret and proof properties of aribtrary languages.\n\n"++
			"This tool parses a '.language'-file, where the syntax of your language is defined. With this, your target file is parsed."++
			"In the language file, rewrite rules (or functions) can be defined - or better, rules defining properties can be defined."++
			"These can be applied to your target language to interpret, typecheck or proof some other property."

showVersion (v, vId)	= (v |> show & intercalate ".") ++", "++show vId
headerText v
		= "Automated Language Generation Tool (version "++ showVersion v ++" )"


class ActionSpecified a where
	actionSpecified	:: a -> Bool


data MainArgs	= MainArgs 
			{ showVersionNr	:: () -> ()
			, manualPDF	:: Bool
			, manualHTML	:: Bool
			, realArgs	:: Maybe Args
			, runTests	:: Bool
			, saveGTKSourceview	:: Bool
			, styles	:: Bool
			, styleCSS	:: Maybe Name
			}

instance ActionSpecified MainArgs where
	actionSpecified args
		= [realArgs] |> (args &) |> isJust & or
			|| [styleCSS] |> (args &) |> isJust & or
			|| [manualPDF, manualHTML, runTests] |> (args &) & or

data Args = Args 	{ tsFile		:: String
			, exampleFiles		:: [ExampleFile]
			, changeFiles		:: [FilePath]
			, dumpTS		:: Bool
			, noCheck		:: Bool
			, numberOfQuickChecks	:: String
			, interpretAbstract	:: Bool
			, interpretFunctionAbs	:: [String]
			, interpretFunctionArgs	:: Maybe String
			, interpretRulesAbstract:: Bool
			, interpretRules	:: [String]
			, subtypingSVG		:: Maybe String
			, iraSVG		:: Maybe String
			, dynamizeArgs		:: Maybe DynamizeArgs
			, styleName		:: Name
			, interactiveArg	:: Maybe Symbol
			, noMakeupArg		:: Bool
			, shortProofs		:: Maybe String
			}
	deriving (Show)

instance NeedsFiles Args where
	filesNeeded args	
		= let	exFiles		= exampleFiles args >>= filesNeeded
			styleFile	= [styleName args | ".style" `isSuffixOf` styleName args]
			in tsFile args : (changeFiles args ++ exFiles ++ styleFile)

instance ActionSpecified Args where
	actionSpecified args
		= [interpretFunctionAbs, interpretRules] 		|> (args &) |> (not . null) & or
		  	|| [exampleFiles]				|> (args &) |> (not . null) & or
			|| [subtypingSVG, iraSVG] 	|> (args &) |> isJust & or
			|| [dynamizeArgs] 		|> (args &) |> isJust & or
			|| [dumpTS, interpretAbstract, interpretRulesAbstract]	|> (args &) & or

data ExampleFile	= ExFileArgs
	{ fileName	:: FilePath
	, parser	:: Name
	, lineByLine	:: Bool
	, ruleSymbol	:: Maybe Symbol
	, function	:: Maybe Name
	, stepByStep	:: Maybe Name
	, testProp	:: Maybe Name
	, testAllProps	:: Bool
	, verbose	:: Bool
	, ptSvg		:: Maybe Name
	, renderHTML	:: Bool
	, renderHTMLNoCss	:: Bool
	, renderLatex	:: Bool
	, renderParts	:: Bool
	} deriving (Show)

data DynamizeArgs	= DynamizeArgs
	{ typeRule	:: TypeName
	, stuckError	:: String
	, relsToErr	:: [Symbol]
	, relsToAdd	:: [Symbol]
	} deriving (Show)



instance ActionSpecified ExampleFile where
	actionSpecified args
		= [testAllProps, renderHTML, renderLatex, renderHTMLNoCss, renderParts] |> (args &) & or
			|| ([ruleSymbol, function, stepByStep, testProp, ptSvg] |> (args &) |> isJust & or)

	
instance NeedsFiles ExampleFile where
	filesNeeded exfile	= [fileName exfile | fileName exfile /= "."]


data Config	= Config 	
	{ autoSyntaxes	:: [Int] }
		deriving (Show, Read, Eq)

emptyConfig
	= Config []


parseArgs	:: ([Int], String) -> [String] -> IO (Bool, Maybe Args)
parseArgs version strs	
	= do	let result	= execParserPure defaultPrefs (parserInfo version) strs
		MainArgs doShowVersion saveManPDF saveManHTML args runTests saveGTKSourceview styles styleCSS
				<- handleParseResult result
		return $ doShowVersion ()
		when saveManPDF $ do
			B.writeFile "ALGT_Manual.pdf" _Manual_Output_ALGT_Manual_pdf
			putStrLn "Manual saved as ALGT_Manual.pdf"
			exitSuccess
		when saveManHTML $ do
			writeFile "ALGT_Manual.html" _Manual_Output_ALGT_Manual_html
			putStrLn "Manual saved as ALGT_Manual.html"
			exitSuccess
		when saveGTKSourceview $ do
			writeFile "language.lang" _language_lang
			putStrLn "Saved 'language.lang' to current directory. Move it to: '~/.local/share/gtksourceview-3.0/language-specs' to enable highlighting"
			exitSuccess
		when styles $ do
			putStrLn $ AH.knownStyles & M.keys & unlines
			exitSuccess
		when (isJust styleCSS) $ do
			style	<- createStyle $ fromJust styleCSS
			putStrLn $ cssFor style
			exitSuccess

		return (runTests, args)


createStyle styleName
	= 	if ".style" `isSuffixOf` styleName then do
			styleContents	<- readFile styleName
			parseColoringFile styleName styleContents & either error return
		else styleName & AH.fetchStyle & either error return


dataPath	= getXdgDirectory XdgData "ALGT"
configPath	= dataPath |> (++"/config")

getConfigFile	:: IO Config
getConfigFile	
	= do	fp	<- configPath
		exists	<- doesFileExist fp
		if exists then
			readFile fp |> read
		else
			return emptyConfig

writeConfigFile	:: Config -> IO ()
writeConfigFile config
 | config == emptyConfig	= removeConfigFile
 | otherwise
	= do	fp	<- dataPath
		createDirectoryIfMissing True fp
		cfp	<- configPath
		putStrLn $ "# Config updated ("++show cfp++")"
		writeFile cfp $ show config

removeConfigFile	:: IO ()
removeConfigFile
	= do	cfp	<- configPath
		exists	<- doesFileExist cfp
		when exists $ removeFile cfp

parserInfo	:: ([Int], String) -> ParserInfo MainArgs
parserInfo v	= parserInfo' (mainArgs $ showVersion v) v

parserInfo' parser v
	= info (helper <*> parser)
			(fullDesc <> progDesc descriptionText <> header (headerText v))




targetFile	:: Parser ExampleFile
targetFile
	= ExFileArgs <$> 
		argument str
			(metavar "TARGET-PROGRAM-FILE"
			<> help "Filepath of the target programming language; use . to read from stdIn"
			<> action "file")
		<*> argument str
			(metavar "PARSE-TYPE"
			<> help "Parse the target program with this bnf-rule as type")
		<*> switch
			(long "line-by-line"
			<> short 'l'
			<> help "Parse the target file line by line")
		<*> optional (strOption 
			 (metavar "RELATION"
			 <> long "relation"
			 <> short 'r'
			 <> help "Prove that this relation is applicable to the example file" ))
		<*> optional (strOption 
			(metavar "FUNCTION"
			 <> long "function"
			 <> short 'f'
			 <> help "Apply given function to the program"))
		<*> optional (strOption
			(metavar "FUNCTION"
			<> long "step-by-step"
			<> short 's'
			<> help "Apply the given function, step by step, until the result of the function is the same as the input"
			))
		<*> optional (strOption
			(metavar "PROPERTY"
			<> long "test-property"
			<> long "tp"
			<> help "Tests the given property on all the examples. The property should take exactly one PARSER-TYPE argument. Only reports failures (unless with ppp)"))
		<*> switch
			(long "test-all-properties"
			<> long "tap"
			<> long "tp*"
			<> long "tpa"
			<> help "Tests all properties on all the examples. The property should take exactly one PARSER-TYPE argument. Only reports failures (unless with ppp)")
		<*> switch
			(long "print-property-proofs"
			<> long "ppp"
			<> help "With 'test-property' and 'test-all-properties': print full proofs of each application of the properties")		
		<*> optional (strOption
			(metavar "svg-name"
			<> long "parstree-svg"
			<> long "ptsvg"
			<> help "Create a neat svg-image of each parsetree"
			))
		<*> switch
			(long "html"
			<> help "Render the file as styled HTML")
		<*> switch
			(long "html-no-css"
			<> help "Render the file as html, without css")
		<*> switch
			(long "latex"
			<> help "Render the file as styled LaTeX")
		<*> switch
			(long "parts"
			<> help "Render the file as parts, e.g. for other programs")

args	:: Parser Args
args	= Args <$> argument str
			(metavar "LANGUAGE-FILE"
			<> help "FilePath of the language-file"
			<> action "file")
		<*> many targetFile
		<*> many (strOption
			(metavar "LANGUAGE-CHANGES-FILE"
			<> long "changes"
			<> short 'c'
			<> help "Apply the given changes to the type-system file. These changes are applied before any other action"
			))
		<*> switch
			(long "dump-language-file"
			<> long "dlf"
			<> help "Dump the parsed type system, usefull for debugging purposes")
		<*> switch
			(long "no-check"
			<> long "nc"
			<> help "Supress liveabilitychecks, totality checker, quickcheck and others")
		<*> strOption
			(long "quickcheck-runs"
			<> metavar "NUMBER-OF-TESTS"
			<> value "8"
			<> help "Number of times each property is tested against random arguments. Default: 100")
		<*> switch
			(long "interpret-abstractly"
			<> long "ia"
			<> help "Interpret each function over all possible values")
		<*> many (strOption
			(metavar "FUNCTION-TO-INTERPRET"
			<> long "ifa"
			<> long "interpret-function-abstract"
			<> help "Interpret a single function abstractly"))
		<*> optional (strOption
			(long "interpret-abstract-arguments"
			<> long "iaa"
			<> help "With abstract interpretation of a function, use this argument to interpret with"))
		<*> switch
			(long "interpret-relations-abstractly"
			<> long "ira"
			<> help "Interpret each relation over all possible values")
		<*> many (strOption
			(metavar "RELATION-TO-INTERPRET"
			<> long "ir"
			<> long "interpret-relation"
			<> help "Only run this relation abstractly"))
		<*> optional (strOption
			(metavar "SVG-PATH"
			<> long "lsvg"
			<> help "Create a SVG of the subset relationship between BNF-rules"))
		<*> optional (strOption
			(metavar "SVG-PATH"
			<> long "irasvg"
			<> help "Create a SVG of the subset relationship between BNF-rules, created by the abstract rule analysises"))
		<*> optional dynamizeArgsParser
		<*> strOption (
			metavar "STYLE-NAME"
			<> long "style"
			<> value "Terminal"
			<> help "Color scheme for parsetrees and svg files"
			<> completer (mkCompleter (\part -> knownStyles & M.keys & filter (part `isPrefixOf`) & return))
			)
		<*> optional (strOption
			(metavar "RULE-TO-INTERPRET"
			<> long "repl"
			<> long "interactive"
			<> short 'i'
			<> help "Run this rule interactively"))
		<*> switch(
			long "plain"
			<> long "no-makeup"
			<> help "Prints the parsetrees as flat text and not as colored output; usefull to capture output in e.g. LaTeX"
			<> hidden)
		<*> optional (strOption
			(long "short-proofs"
			<> metavar "DISTANCE-BETWEEN-PREDICATES"
			<> help "Prints proofs without their names and with given spaces in between"
			<> hidden))


		
dynamizeArgsParser	:: Parser DynamizeArgs
dynamizeArgsParser
	= DynamizeArgs
		<$> strOption
			(metavar "SYNTAX-RULE-EXPRESSION"
			<> long "dynamize-syntax"
			<> help "The type to add 'type-err' to")
		<*> strOption
			(metavar "STUCK-STATE"
			<> long "error"
			<> help "The literal representing a type error/stuck state")
		<*> many (strOption
			(metavar "REL-TO-ANALYZE"
			<> long "rel"
			<> help "The relation symbol for which stuck states should be introduced (e.g. 'smallstep')"))
		<*> many (strOption
			(metavar "REL-TO-ADD"
			<> long "reladd"
			<> help "The relation symbol for which stuck states should added trivially (e.g. 'is canonical')"))


mainArgs	:: String -> Parser MainArgs
mainArgs versionMsg
	= MainArgs <$> infoOption versionMsg
			(long "version"
			<> short 'v'
			<> help "Show the version number and text")
		<*> switch
			(long "manual-pdf"
			<> help "Save the manual file (pdf) to the working directory")
		<*> switch
			(long "manual-html"
			<> help "Save the manual file (html) to the working directory")
		<*> optional args
		<*> switch
			(long "test"
			<> help "Run the integration tests"
			<> hidden)
		<*> switch
			(long "install-gtk-sourceview"
			<> help "Saves the language spec for .language files. Move it to the language specs file for gtk-sourceview to enable syntax highlighting in editors using GTK-sourceview (GEdit, Pluma,...")
		<*> switch
			(long "styles"
			<> help "What styles are default?")
		<*> optional (strOption
			(metavar "STYLENAME"
			<> long "css"
			<> help "Create a css file out of the given stylefile (might be a builtin style)"
			))


This module defines parsing of the arguments and reading/writing of the config file

module Utils.ArgumentParser (parseArgs, Args(..), ExampleFile(..), Config(..), NeedsFiles(..), DynamizeArgs(..), getConfigFile, writeConfigFile, removeConfigFile, actionSpecified)where


import TypeSystem
import AssetsHelper as AH
import qualified Assets

import Utils.Utils
import Utils.PureIO hiding (writeFile, readFile, putStrLn)

import Data.Monoid ((<>))
import Data.List (intercalate, isPrefixOf, isSuffixOf)
import Data.Maybe
import qualified Data.Map as M

import SyntaxHighlighting.AsHTMLPt (cssFor)
import SyntaxHighlighting.Coloring

import Control.Monad

import Options.Applicative

import System.Directory
import System.Exit

import Assets
import qualified Data.ByteString as B




descriptionText	= "ALGT (Automated Language Generation Tool)- automatically parse, interpret and proof properties of aribtrary languages.\n\n"++
			"This tool parses a '.language'-file, where the syntax of your language is defined. With this, your target file is parsed."++
			"In the language file, rewrite rules (or functions) can be defined - or better, rules defining properties can be defined."++
			"These can be applied to your target language to interpret, typecheck or proof some other property."

showVersion (v, vId)	= (v |> show & intercalate ".") ++", "++show vId
headerText v
		= "Automated Language Generation Tool (version "++ showVersion v ++" )"


class ActionSpecified a where
	actionSpecified	:: a -> Bool


data MainArgs	= MainArgs 
			{ showVersionNr	:: () -> ()
			, manualPDF	:: Bool
			, manualHTML	:: Bool
			, realArgs	:: Maybe Args
			, runTests	:: Bool
			, saveGTKSourceview	:: Bool
			, styles	:: Bool
			, styleCSS	:: Maybe Name
			}

instance ActionSpecified MainArgs where
	actionSpecified args
		= [realArgs] |> (args &) |> isJust & or
			|| [styleCSS] |> (args &) |> isJust & or
			|| [manualPDF, manualHTML, runTests] |> (args &) & or

data Args = Args 	{ tsFile		:: String
			, exampleFiles		:: [ExampleFile]
			, changeFiles		:: [FilePath]
			, dumpTS		:: Bool
			, noCheck		:: Bool
			, numberOfQuickChecks	:: String
			, interpretAbstract	:: Bool
			, interpretFunctionAbs	:: [String]
			, interpretFunctionArgs	:: Maybe String
			, interpretRulesAbstract:: Bool
			, interpretRules	:: [String]
			, subtypingSVG		:: Maybe String
			, iraSVG		:: Maybe String
			, dynamizeArgs		:: Maybe DynamizeArgs
			, styleName		:: Name
			, interactiveArg	:: Maybe Symbol
			, noMakeupArg		:: Bool
			, shortProofs		:: Maybe String
			}
	deriving (Show)

instance NeedsFiles Args where
	filesNeeded args	
		= let	exFiles		= exampleFiles args >>= filesNeeded
			styleFile	= [styleName args | ".style" `isSuffixOf` styleName args]
			in tsFile args : (changeFiles args ++ exFiles ++ styleFile)

instance ActionSpecified Args where
	actionSpecified args
		= [interpretFunctionAbs, interpretRules] 		|> (args &) |> (not . null) & or
		  	|| [exampleFiles]				|> (args &) |> (not . null) & or
			|| [subtypingSVG, iraSVG] 	|> (args &) |> isJust & or
			|| [dynamizeArgs] 		|> (args &) |> isJust & or
			|| [dumpTS, interpretAbstract, interpretRulesAbstract]	|> (args &) & or

data ExampleFile	= ExFileArgs
	{ fileName	:: FilePath
	, parser	:: Name
	, lineByLine	:: Bool
	, ruleSymbol	:: Maybe Symbol
	, function	:: Maybe Name
	, stepByStep	:: Maybe Name
	, testProp	:: Maybe Name
	, testAllProps	:: Bool
	, verbose	:: Bool
	, ptSvg		:: Maybe Name
	, renderHTML	:: Bool
	, renderHTMLNoCss	:: Bool
	, renderLatex	:: Bool
	, renderParts	:: Bool
	} deriving (Show)

data DynamizeArgs	= DynamizeArgs
	{ typeRule	:: TypeName
	, stuckError	:: String
	, relsToErr	:: [Symbol]
	, relsToAdd	:: [Symbol]
	} deriving (Show)



instance ActionSpecified ExampleFile where
	actionSpecified args
		= [testAllProps, renderHTML, renderLatex, renderHTMLNoCss, renderParts] |> (args &) & or
			|| ([ruleSymbol, function, stepByStep, testProp, ptSvg] |> (args &) |> isJust & or)

	
instance NeedsFiles ExampleFile where
	filesNeeded exfile	= [fileName exfile | fileName exfile /= "."]


data Config	= Config 	
	{ autoSyntaxes	:: [Int] }
		deriving (Show, Read, Eq)

emptyConfig
	= Config []


parseArgs	:: ([Int], String) -> [String] -> IO (Bool, Maybe Args)
parseArgs version strs	
	= do	let result	= execParserPure defaultPrefs (parserInfo version) strs
		MainArgs doShowVersion saveManPDF saveManHTML args runTests saveGTKSourceview styles styleCSS
				<- handleParseResult result
		return $ doShowVersion ()
		when saveManPDF $ do
			B.writeFile "ALGT_Manual.pdf" _Manual_Output_ALGT_Manual_pdf
			putStrLn "Manual saved as ALGT_Manual.pdf"
			exitSuccess
		when saveManHTML $ do
			writeFile "ALGT_Manual.html" _Manual_Output_ALGT_Manual_html
			putStrLn "Manual saved as ALGT_Manual.html"
			exitSuccess
		when saveGTKSourceview $ do
			writeFile "language.lang" _language_lang
			putStrLn "Saved 'language.lang' to current directory. Move it to: '~/.local/share/gtksourceview-3.0/language-specs' to enable highlighting"
			exitSuccess
		when styles $ do
			putStrLn $ AH.knownStyles & M.keys & unlines
			exitSuccess
		when (isJust styleCSS) $ do
			style	<- createStyle $ fromJust styleCSS
			putStrLn $ cssFor style
			exitSuccess

		return (runTests, args)


createStyle styleName
	= 	if ".style" `isSuffixOf` styleName then do
			styleContents	<- readFile styleName
			parseColoringFile styleName styleContents & either error return
		else styleName & AH.fetchStyle & either error return


dataPath	= getXdgDirectory XdgData "ALGT"
configPath	= dataPath |> (++"/config")

getConfigFile	:: IO Config
getConfigFile	
	= do	fp	<- configPath
		exists	<- doesFileExist fp
		if exists then
			readFile fp |> read
		else
			return emptyConfig

writeConfigFile	:: Config -> IO ()
writeConfigFile config
 | config == emptyConfig	= removeConfigFile
 | otherwise
	= do	fp	<- dataPath
		createDirectoryIfMissing True fp
		cfp	<- configPath
		putStrLn $ "# Config updated ("++show cfp++")"
		writeFile cfp $ show config

removeConfigFile	:: IO ()
removeConfigFile
	= do	cfp	<- configPath
		exists	<- doesFileExist cfp
		when exists $ removeFile cfp

parserInfo	:: ([Int], String) -> ParserInfo MainArgs
parserInfo v	= parserInfo' (mainArgs $ showVersion v) v

parserInfo' parser v
	= info (helper <*> parser)
			(fullDesc <> progDesc descriptionText <> header (headerText v))




targetFile	:: Parser ExampleFile
targetFile
	= ExFileArgs <$> 
		argument str
			(metavar "TARGET-PROGRAM-FILE"
			<> help "Filepath of the target programming language; use . to read from stdIn"
			<> action "file")
		<*> argument str
			(metavar "PARSE-TYPE"
			<> help "Parse the target program with this bnf-rule as type")
		<*> switch
			(long "line-by-line"
			<> short 'l'
			<> help "Parse the target file line by line")
		<*> optional (strOption 
			 (metavar "RELATION"
			 <> long "relation"
			 <> short 'r'
			 <> help "Prove that this relation is applicable to the example file" ))
		<*> optional (strOption 
			(metavar "FUNCTION"
			 <> long "function"
			 <> short 'f'
			 <> help "Apply given function to the program"))
		<*> optional (strOption
			(metavar "FUNCTION"
			<> long "step-by-step"
			<> short 's'
			<> help "Apply the given function, step by step, until the result of the function is the same as the input"
			))
		<*> optional (strOption
			(metavar "PROPERTY"
			<> long "test-property"
			<> long "tp"
			<> help "Tests the given property on all the examples. The property should take exactly one PARSER-TYPE argument. Only reports failures (unless with ppp)"))
		<*> switch
			(long "test-all-properties"
			<> long "tap"
			<> long "tp*"
			<> long "tpa"
			<> help "Tests all properties on all the examples. The property should take exactly one PARSER-TYPE argument. Only reports failures (unless with ppp)")
		<*> switch
			(long "print-property-proofs"
			<> long "ppp"
			<> help "With 'test-property' and 'test-all-properties': print full proofs of each application of the properties")		
		<*> optional (strOption
			(metavar "svg-name"
			<> long "parstree-svg"
			<> long "ptsvg"
			<> help "Create a neat svg-image of each parsetree"
			))
		<*> switch
			(long "html"
			<> help "Render the file as styled HTML")
		<*> switch
			(long "html-no-css"
			<> help "Render the file as html, without css")
		<*> switch
			(long "latex"
			<> help "Render the file as styled LaTeX")
		<*> switch
			(long "parts"
			<> help "Render the file as parts, e.g. for other programs")

args	:: Parser Args
args	= Args <$> argument str
			(metavar "LANGUAGE-FILE"
			<> help "FilePath of the language-file"
			<> action "file")
		<*> many targetFile
		<*> many (strOption
			(metavar "LANGUAGE-CHANGES-FILE"
			<> long "changes"
			<> short 'c'
			<> help "Apply the given changes to the type-system file. These changes are applied before any other action"
			))
		<*> switch
			(long "dump-language-file"
			<> long "dlf"
			<> help "Dump the parsed type system, usefull for debugging purposes")
		<*> switch
			(long "no-check"
			<> long "nc"
			<> help "Supress liveabilitychecks, totality checker, quickcheck and others")
		<*> strOption
			(long "quickcheck-runs"
			<> metavar "NUMBER-OF-TESTS"
			<> value "8"
			<> help "Number of times each property is tested against random arguments. Default: 100")
		<*> switch
			(long "interpret-abstractly"
			<> long "ia"
			<> help "Interpret each function over all possible values")
		<*> many (strOption
			(metavar "FUNCTION-TO-INTERPRET"
			<> long "ifa"
			<> long "interpret-function-abstract"
			<> help "Interpret a single function abstractly"))
		<*> optional (strOption
			(long "interpret-abstract-arguments"
			<> long "iaa"
			<> help "With abstract interpretation of a function, use this argument to interpret with"))
		<*> switch
			(long "interpret-relations-abstractly"
			<> long "ira"
			<> help "Interpret each relation over all possible values")
		<*> many (strOption
			(metavar "RELATION-TO-INTERPRET"
			<> long "ir"
			<> long "interpret-relation"
			<> help "Only run this relation abstractly"))
		<*> optional (strOption
			(metavar "SVG-PATH"
			<> long "lsvg"
			<> help "Create a SVG of the subset relationship between BNF-rules"))
		<*> optional (strOption
			(metavar "SVG-PATH"
			<> long "irasvg"
			<> help "Create a SVG of the subset relationship between BNF-rules, created by the abstract rule analysises"))
		<*> optional dynamizeArgsParser
		<*> strOption (
			metavar "STYLE-NAME"
			<> long "style"
			<> value "Terminal"
			<> help "Color scheme for parsetrees and svg files"
			<> completer (mkCompleter (\part -> knownStyles & M.keys & filter (part `isPrefixOf`) & return))
			)
		<*> optional (strOption
			(metavar "RULE-TO-INTERPRET"
			<> long "repl"
			<> long "interactive"
			<> short 'i'
			<> help "Run this rule interactively"))
		<*> switch(
			long "plain"
			<> long "no-makeup"
			<> help "Prints the parsetrees as flat text and not as colored output; usefull to capture output in e.g. LaTeX"
			<> hidden)
		<*> optional (strOption
			(long "short-proofs"
			<> metavar "DISTANCE-BETWEEN-PREDICATES"
			<> help "Prints proofs without their names and with given spaces in between"
			<> hidden))


		
dynamizeArgsParser	:: Parser DynamizeArgs
dynamizeArgsParser
	= DynamizeArgs
		<$> strOption
			(metavar "SYNTAX-RULE-EXPRESSION"
			<> long "dynamize-syntax"
			<> help "The type to add 'type-err' to")
		<*> strOption
			(metavar "STUCK-STATE"
			<> long "error"
			<> help "The literal representing a type error/stuck state")
		<*> many (strOption
			(metavar "REL-TO-ANALYZE"
			<> long "rel"
			<> help "The relation symbol for which stuck states should be introduced (e.g. 'smallstep')"))
		<*> many (strOption
			(metavar "REL-TO-ADD"
			<> long "reladd"
			<> help "The relation symbol for which stuck states should added trivially (e.g. 'is canonical')"))


mainArgs	:: String -> Parser MainArgs
mainArgs versionMsg
	= MainArgs <$> infoOption versionMsg
			(long "version"
			<> short 'v'
			<> help "Show the version number and text")
		<*> switch
			(long "manual-pdf"
			<> help "Save the manual file (pdf) to the working directory")
		<*> switch
			(long "manual-html"
			<> help "Save the manual file (html) to the working directory")
		<*> optional args
		<*> switch
			(long "test"
			<> help "Run the integration tests"
			<> hidden)
		<*> switch
			(long "install-gtk-sourceview"
			<> help "Saves the language spec for .language files. Move it to the language specs file for gtk-sourceview to enable syntax highlighting in editors using GTK-sourceview (GEdit, Pluma,...")
		<*> switch
			(long "styles"
			<> help "What styles are default?")
		<*> optional (strOption
			(metavar "STYLENAME"
			<> long "css"
			<> help "Create a css file out of the given stylefile (might be a builtin style)"
			))
