Parse-stv2c-opts
Parse arguments from the command line into a stv2c-opts-p aggregate.
- Signature
(parse-stv2c-opts args &key (getopt::init '*default-stv2c-opts*))
→
(mv getopt::errmsg getopt::result getopt::extra)
- Arguments
- args — The command line arguments to parse, which is
typically derived from oslib::argv.
Guard (string-listp args).
- getopt::init — An initial stv2c-opts-p to start from, which
gives the default values for each field.
Guard (stv2c-opts-p getopt::init).
- Returns
- getopt::errmsg — NIL on success, or an error message produced by msg,
suitable for printing the fmt directive ~@.
- getopt::result — An updated version of init where the command-line
arguments have been applied. On any error, this may be
only partially updated.
Type (stv2c-opts-p getopt::result), given (force (stv2c-opts-p getopt::init)).
- getopt::extra — Any other arguments in args that were not recognized
as options. Typically this might include the "main"
arguments to a program, e.g., file names, etc., that aren't
associated with --options.
Type (string-listp getopt::extra), given (force (string-listp args)).
This is an ordinary command line parser, automatically
produced by getopt.
Definitions and Theorems
Function: parse-stv2c-opts-fn
(defun parse-stv2c-opts-fn (args getopt::init)
(declare (xargs :guard (and (string-listp args)
(stv2c-opts-p getopt::init))))
(let ((__function__ 'parse-stv2c-opts))
(declare (ignorable __function__))
(parse-stv2c-opts-aux args getopt::init nil nil)))
Theorem: stv2c-opts-p-of-parse-stv2c-opts.result
(defthm stv2c-opts-p-of-parse-stv2c-opts.result
(implies (force (stv2c-opts-p getopt::init))
(b* (((mv getopt::?errmsg
getopt::?result getopt::?extra)
(parse-stv2c-opts-fn args getopt::init)))
(stv2c-opts-p getopt::result)))
:rule-classes :rewrite)
Theorem: string-listp-of-parse-stv2c-opts.extra
(defthm string-listp-of-parse-stv2c-opts.extra
(implies (force (string-listp args))
(b* (((mv getopt::?errmsg
getopt::?result getopt::?extra)
(parse-stv2c-opts-fn args getopt::init)))
(string-listp getopt::extra)))
:rule-classes :rewrite)
Subtopics
- Parse-stv2c-opts-long
- Parse-stv2c-opts-aux
- Parse-stv2c-opts-bundle
- Parse-stv2c-opts-short->long-list
- Parse-stv2c-opts-short->long
