|
definition:
|
options :: [OptDescr (Options -> Options)]
options =
[ Option "h?" ["help"] (NoArg (\opts -> opts { optHelp = True }))
"print help and exit"
, Option "q" ["quiet"] (NoArg (\opts -> opts { optVerb = 0 }))
"run quietly (no output, only exit code)"
, Option "v" ["verbosity"]
(OptArg (maybe (checkVerb 2) (safeReadNat checkVerb)) "<n>")
"verbosity level:\n0: quiet (same as `-q')\n1: show progress (default)\n2: show generated output (same as `-v')\n3: show more details about translation"
, Option "p" ["property"]
(ReqArg addPropName "<n>")
"name of property to be translated as theorem\n(default: translate all properties in module)"
, Option "n" ["nostore"]
(NoArg (\opts -> opts { optStore = False }))
"do not store translation (show only)"
, Option "t" ["target"]
(ReqArg checkTarget "<t>")
"translation target:\nAgda (default)"
, Option "s" ["scheme"]
(ReqArg checkScheme "<s>")
"translation scheme:\nfor target Agda: 'choice' (default) or 'nondet'"
]
where
safeReadNat opttrans s opts = case readNat s of
[(n,"")] -> opttrans n opts
_ -> error "Illegal number argument (try `-h' for help)"
checkVerb n opts = if n>=0 && n<4
then opts { optVerb = n }
else error "Illegal verbosity level (try `-h' for help)"
checkTarget s opts =
if map toLower s `elem` ["agda"]
then opts { optTarget = map toLower s }
else error $ "Illegal target `" ++ s ++ "' (try `-h' for help)"
checkScheme s opts =
if map toLower s `elem` ["choice","nondet"]
then opts { optScheme = map toLower s }
else error $ "Illegal scheme `" ++ s ++ "' (try `-h' for help)"
-- support also qualified names:
addPropName name opts =
let nameparts = splitOn "." name
partnums = length nameparts
qname = if partnums < 2
then ("",name)
else (intercalate "." (take (partnums - 1) nameparts),
last nameparts)
in opts { optTheorems = qname : optTheorems opts }
|