259 lines
7.5 KiB
Idris
259 lines
7.5 KiB
Idris
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}) "<dir>:<dir>...")
|
||
"add directories to look for source files",
|
||
MkOpt ['o'] ["output"] (ReqArg (\s => Ok {outFile := toOutFile s}) "<file>")
|
||
"output file (\"-\" for stdout, \"\" for no output)",
|
||
MkOpt ['P'] ["phase"] (ReqArg toPhase "<phase>")
|
||
"stop after the given phase",
|
||
MkOpt ['l'] ["log"] (ReqArg logFlag "[<cat>=]<n>:...")
|
||
"set log level",
|
||
MkOpt ['L'] ["log-file"] (ReqArg (\s => Ok {logFile := toOutFile s}) "<file>")
|
||
"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 "<width>")
|
||
"max output width (defaults to terminal width)",
|
||
MkOpt [] ["color", "colour"] (ReqArg toHLType "<type>")
|
||
"select highlighting type",
|
||
|
||
MkOpt [] ["dump-parse"]
|
||
(ReqArg (\s => Ok {dump.parse := toOutFile s}) "<file>")
|
||
"dump AST",
|
||
MkOpt [] ["dump-check"]
|
||
(ReqArg (\s => Ok {dump.check := toOutFile s}) "<file>")
|
||
"dump typechecker output",
|
||
MkOpt [] ["dump-erase"]
|
||
(ReqArg (\s => Ok {dump.erase := toOutFile s}) "<file>")
|
||
"dump erasure output",
|
||
MkOpt [] ["dump-scheme"]
|
||
(ReqArg (\s => Ok {dump.scheme := toOutFile s}) "<file>")
|
||
"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)
|