Parse-vl-pp-opts
Parse arguments from the command line into a vl-pp-opts-p aggregate.
- Signature
(parse-vl-pp-opts args &key (getopt::init '*default-vl-pp-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 vl-pp-opts-p to start from, which
gives the default values for each field.
Guard (vl-pp-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 (vl-pp-opts-p getopt::result), given (force (vl-pp-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-vl-pp-opts-fn
(defun parse-vl-pp-opts-fn (args getopt::init)
(declare (xargs :guard (and (string-listp args)
(vl-pp-opts-p getopt::init))))
(let ((__function__ 'parse-vl-pp-opts))
(declare (ignorable __function__))
(parse-vl-pp-opts-aux args getopt::init nil nil)))
Theorem: vl-pp-opts-p-of-parse-vl-pp-opts.result
(defthm vl-pp-opts-p-of-parse-vl-pp-opts.result
(implies (force (vl-pp-opts-p getopt::init))
(b* (((mv getopt::?errmsg
getopt::?result getopt::?extra)
(parse-vl-pp-opts-fn args getopt::init)))
(vl-pp-opts-p getopt::result)))
:rule-classes :rewrite)
Theorem: string-listp-of-parse-vl-pp-opts.extra
(defthm string-listp-of-parse-vl-pp-opts.extra
(implies (force (string-listp args))
(b* (((mv getopt::?errmsg
getopt::?result getopt::?extra)
(parse-vl-pp-opts-fn args getopt::init)))
(string-listp getopt::extra)))
:rule-classes :rewrite)
Subtopics
- Parse-vl-pp-opts-long
- Parse-vl-pp-opts-aux
- Parse-vl-pp-opts-bundle
- Parse-vl-pp-opts-short->long-list
- Parse-vl-pp-opts-short->long
