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