{-# LANGUAGE Safe #-} module RWE (main) where import Driver (driverMain) import Embedder.FrontEnd (embedFile) import ReWire.Flags (Flag (..)) import System.Console.GetOpt (OptDescr (..), ArgDescr (..)) options :: [OptDescr Flag] options :: [OptDescr Flag] options = [ [Char] -> [[Char]] -> ArgDescr Flag -> [Char] -> OptDescr Flag forall a. [Char] -> [[Char]] -> ArgDescr a -> [Char] -> OptDescr a Option [Char 'h'] [[Char] "help"] (Flag -> ArgDescr Flag forall a. a -> ArgDescr a NoArg Flag FlagHelp) [Char] "This help message." , [Char] -> [[Char]] -> ArgDescr Flag -> [Char] -> OptDescr Flag forall a. [Char] -> [[Char]] -> ArgDescr a -> [Char] -> OptDescr a Option [Char 'v'] [[Char] "verbose"] (Flag -> ArgDescr Flag forall a. a -> ArgDescr a NoArg Flag FlagVerbose) [Char] "More verbose output." , [Char] -> [[Char]] -> ArgDescr Flag -> [Char] -> OptDescr Flag forall a. [Char] -> [[Char]] -> ArgDescr a -> [Char] -> OptDescr a Option [Char 'w'] [[Char] "no-warn"] (Flag -> ArgDescr Flag forall a. a -> ArgDescr a NoArg Flag FlagNoWarn) [Char] "Suppress warnings." , [Char] -> [[Char]] -> ArgDescr Flag -> [Char] -> OptDescr Flag forall a. [Char] -> [[Char]] -> ArgDescr a -> [Char] -> OptDescr a Option [Char 'W'] [] (([Char] -> Flag) -> [Char] -> ArgDescr Flag forall a. ([Char] -> a) -> [Char] -> ArgDescr a ReqArg [Char] -> Flag FlagW [Char] "error") [Char] "-Werror: treat warnings as errors." , [Char] -> [[Char]] -> ArgDescr Flag -> [Char] -> OptDescr Flag forall a. [Char] -> [[Char]] -> ArgDescr a -> [Char] -> OptDescr a Option [Char 'd'] [[Char] "dump"] (([Char] -> Flag) -> [Char] -> ArgDescr Flag forall a. ([Char] -> a) -> [Char] -> ArgDescr a ReqArg [Char] -> Flag FlagDump [Char] "1,2,...") [Char] "Dump the intermediate form of the corresponding pass number (1-3; see -v output)." , [Char] -> [[Char]] -> ArgDescr Flag -> [Char] -> OptDescr Flag forall a. [Char] -> [[Char]] -> ArgDescr a -> [Char] -> OptDescr a Option [] [[Char] "dump-all"] (Flag -> ArgDescr Flag forall a. a -> ArgDescr a NoArg Flag FlagDumpAll) [Char] "Dump the intermediate form of every pass (see -d)." , [Char] -> [[Char]] -> ArgDescr Flag -> [Char] -> OptDescr Flag forall a. [Char] -> [[Char]] -> ArgDescr a -> [Char] -> OptDescr a Option [Char 'o'] [] (([Char] -> Flag) -> [Char] -> ArgDescr Flag forall a. ([Char] -> a) -> [Char] -> ArgDescr a ReqArg [Char] -> Flag FlagO [Char] "filename.thy") [Char] "Name for output file." , [Char] -> [[Char]] -> ArgDescr Flag -> [Char] -> OptDescr Flag forall a. [Char] -> [[Char]] -> ArgDescr a -> [Char] -> OptDescr a Option [] [[Char] "start"] (([Char] -> Flag) -> [Char] -> ArgDescr Flag forall a. ([Char] -> a) -> [Char] -> ArgDescr a ReqArg [Char] -> Flag FlagStart [Char] "name") [Char] "Symbol to use for the definition of the top-level module (default: Main.start)." , [Char] -> [[Char]] -> ArgDescr Flag -> [Char] -> OptDescr Flag forall a. [Char] -> [[Char]] -> ArgDescr a -> [Char] -> OptDescr a Option [] [[Char] "loadpath"] (([Char] -> Flag) -> [Char] -> ArgDescr Flag forall a. ([Char] -> a) -> [Char] -> ArgDescr a ReqArg [Char] -> Flag FlagLoadPath [Char] "dir1,dir2,...") [Char] "Additional directories for loadpath." , [Char] -> [[Char]] -> ArgDescr Flag -> [Char] -> OptDescr Flag forall a. [Char] -> [[Char]] -> ArgDescr a -> [Char] -> OptDescr a Option [] [[Char] "pretty"] (Flag -> ArgDescr Flag forall a. a -> ArgDescr a NoArg Flag FlagPretty) [Char] "Attempt to output a prettier Isabelle theory at the expense of performance." ] main :: IO () main :: IO () main = [Char] -> [OptDescr Flag] -> (Config -> [Char] -> IO ()) -> IO () driverMain [Char] "rwe" [OptDescr Flag] options Config -> [Char] -> IO () forall (m :: * -> *). MonadIO m => Config -> [Char] -> m () embedFile