module Options import Quox.Pretty import Quox.Log import Data.DPair import Data.SortedMap import System import System.Console.GetOpt import System.File import System.Term import Derive.Prelude %default total %language ElabReflection public export data OutFile = File String | Console | NoOut %name OutFile f %runElab derive "OutFile" [Eq, Show] public export data Phase = Parse | Check | Erase | Scheme | End %name Phase p %runElab derive "Phase" [Eq, Show] ||| a list of all intermediate `Phase`s (excluding `End`) public export %inline allPhases : List Phase allPhases = %runElab do cs <- getCons $ fst !(lookupName "Phase") traverse (check . var) $ fromMaybe [] $ init' cs ||| `Guess` is `Term` for a terminal and `NoHL` for a file public export data HLType = Guess | NoHL | Term | Html %runElab derive "HLType" [Eq, Show] public export record Dump where constructor MkDump parse, check, erase, scheme : OutFile %name Dump dump %runElab derive "Dump" [Show] public export record Options where constructor MkOpts include : List String dump : Dump outFile : OutFile until : Maybe Phase hlType : HLType flavor : Pretty.Flavor width : Nat logLevels : LogLevels logFile : OutFile %name Options opts %runElab derive "Options" [Show] export defaultWidth : IO Nat defaultWidth = do w <- cast {to = Nat} <$> getTermCols pure $ if w == 0 then 80 else w export defaultOpts : IO Options defaultOpts = pure $ MkOpts { include = ["."], dump = MkDump NoOut NoOut NoOut NoOut, outFile = Console, until = Nothing, hlType = Guess, flavor = Unicode, width = !defaultWidth, logLevels = defaultLogLevels, logFile = Console } private data HelpType = Common | All private data OptAction = ShowHelp HelpType | Err String | Ok (Options -> Options) %name OptAction act private toOutFile : String -> OutFile toOutFile "" = NoOut toOutFile "-" = Console toOutFile f = File f private toPhase : String -> OptAction toPhase str = let lstr = toLower str in case find (\p => toLower (show p) == lstr) allPhases of Just p => Ok $ setPhase p Nothing => Err "unknown phase name \{show str}\nphases: \{phaseNames}" where phaseNames = joinBy ", " $ map (toLower . show) allPhases defConsole : OutFile -> OutFile defConsole NoOut = Console defConsole f = f setPhase : Phase -> Options -> Options setPhase Parse = {until := Just Parse, dump.parse $= defConsole} setPhase Check = {until := Just Check, dump.check $= defConsole} setPhase Erase = {until := Just Erase, dump.erase $= defConsole} setPhase Scheme = {until := Just Scheme, dump.scheme $= defConsole} setPhase End = id private toWidth : String -> OptAction toWidth s = case parsePositive s of Just n => Ok {width := n} Nothing => Err "invalid width: \{show s}" private toHLType : String -> OptAction toHLType str = case toLower str of "none" => Ok {hlType := NoHL} "term" => Ok {hlType := Term} "html" => Ok {hlType := Html} _ => Err "unknown highlighting type \{show str}\ntypes: term, html, none" ||| like ghc, `-i ""` clears the search path; ||| `-i a:b:c` adds `a`, `b`, `c` to the end private dirListFlag : String -> List String -> List String dirListFlag "" val = [] dirListFlag dirs val = val ++ toList (split (== ':') dirs) private splitLogFlag : String -> Either String (List (Maybe LogCategory, LogLevel)) splitLogFlag = traverse flag1 . toList . split (== ':') where parseLogCategory : String -> Either String LogCategory parseLogCategory cat = do let Just cat = toLogCategory cat | _ => let catList = joinBy ", " logCategories in Left "unknown log category. categories are:\n\{catList}" pure cat parseLogLevel : String -> Either String LogLevel parseLogLevel lvl = do let Just lvl = parsePositive lvl | _ => Left "log level \{lvl} not a number" let Just lvl = toLogLevel lvl | _ => Left "log level \{show lvl} out of range 0–\{show maxLogLevel}" pure lvl flag1 : String -> Either String (Maybe LogCategory, LogLevel) flag1 str = do let (first, second) = break (== '=') str case strM second of StrCons '=' lvl => do cat <- parseLogCategory first lvl <- parseLogLevel lvl pure (Just cat, lvl) StrNil => (Nothing,) <$> parseLogLevel first _ => Left "invalid log flag \{str}" private setLogFlag : LogLevels -> (Maybe LogCategory, LogLevel) -> LogLevels setLogFlag lvls (Nothing, lvl) = {defLevel := lvl} lvls setLogFlag lvls (Just name, lvl) = {levels $= ((name, lvl) ::)} lvls private logFlag : String -> OptAction logFlag str = case splitLogFlag str of Left err => Err err Right flags => Ok $ \o => {logLevels := foldl setLogFlag o.logLevels flags} o private commonOptDescrs' : List (OptDescr OptAction) commonOptDescrs' = [ MkOpt ['i'] ["include"] (ReqArg (\is => Ok {include $= dirListFlag is}) ":...") "add directories to look for source files", MkOpt ['o'] ["output"] (ReqArg (\s => Ok {outFile := toOutFile s}) "") "output file (\"-\" for stdout, \"\" for no output)", MkOpt ['P'] ["phase"] (ReqArg toPhase "") "stop after the given phase", MkOpt ['l'] ["log"] (ReqArg logFlag "[=]:...") "set log level", MkOpt ['L'] ["log-file"] (ReqArg (\s => Ok {logFile := toOutFile s}) "") "set log output file" ] private extraOptDescrs : List (OptDescr OptAction) extraOptDescrs = [ MkOpt [] ["unicode"] (NoArg $ Ok {flavor := Unicode}) "use unicode syntax when printing (default)", MkOpt [] ["ascii"] (NoArg $ Ok {flavor := Ascii}) "use ascii syntax when printing", MkOpt [] ["width"] (ReqArg toWidth "") "max output width (defaults to terminal width)", MkOpt [] ["color", "colour"] (ReqArg toHLType "") "select highlighting type", MkOpt [] ["dump-parse"] (ReqArg (\s => Ok {dump.parse := toOutFile s}) "") "dump AST", MkOpt [] ["dump-check"] (ReqArg (\s => Ok {dump.check := toOutFile s}) "") "dump typechecker output", MkOpt [] ["dump-erase"] (ReqArg (\s => Ok {dump.erase := toOutFile s}) "") "dump erasure output", MkOpt [] ["dump-scheme"] (ReqArg (\s => Ok {dump.scheme := toOutFile s}) "") "dump scheme output (without prelude)" ] private helpOptDescrs : List (OptDescr OptAction) helpOptDescrs = [ MkOpt ['h'] ["help"] (NoArg $ ShowHelp Common) "show common options", MkOpt [] ["help-all"] (NoArg $ ShowHelp All) "show all options" ] commonOptDescrs = commonOptDescrs' ++ helpOptDescrs allOptDescrs = commonOptDescrs' ++ extraOptDescrs ++ helpOptDescrs export usageHeader : String usageHeader = trim """ quox [options] [file.quox ...] rawr """ export usage : List (OptDescr _) -> IO a usage ds = do ignore $ fPutStr stderr $ usageInfo usageHeader ds exitSuccess private applyAction : Options -> OptAction -> IO Options applyAction opts (ShowHelp Common) = usage commonOptDescrs applyAction opts (ShowHelp All) = usage allOptDescrs applyAction opts (Err err) = die err applyAction opts (Ok f) = pure $ f opts export options : IO (String, Options, List String) options = do app :: args <- getArgs | [] => die "couldn't get command line arguments" let res = getOpt Permute allOptDescrs args unless (null res.errors) $ die $ trim $ concat res.errors unless (null res.unrecognized) $ die "unrecognised options: \{joinBy ", " res.unrecognized}" opts <- foldlM applyAction !defaultOpts res.options pure (app, opts, res.nonOptions)