Demo-p
A basic demo of using getopt to parse command-line options.
(demo-p x) is a std::defaggregate of the following fields.
- help — Print a help message and exit with status 0.
Invariant (booleanp help).
- verbose — Turn on excessive debugging information.
Invariant (booleanp verbose).
- version — Print version information and exit with status 0.
Invariant (booleanp version).
- username — Change the username to something else.
Invariant (stringp username).
- port — Port to connect to.
Invariant (natp port).
- dirs — Directory list.
Invariant (string-listp dirs).
- extra-stuff — Hidden option that the user never sees, but that is part of
our aggregate.
- extra-stuff2 — Hidden option that the user never sees, but that is part of
our aggregate.
Invariant (stringp extra-stuff2).
Source link: demo-p
This is a basic demo of how to use getopt, and a collection of unit
tests to make sure getopt is working correctly.
Note: our focus in this demo is just on the command-line parsing piece. We
illustrate illustrates a lot of the things you can do with getopt, e.g., short
aliases, long names, default values, validating inputs, and accumulating
arguments. But we don't turn it into a working program. If you want to
understand how getopt and argv and save-exec fit together,
see demo2.
This defoptions call does two things:
- It introduces demo-p, an ordinary std::defaggregate with
various fields and well-formedness conditions. These demo-p structures
can be passed around throughout your program just like any ordinary ACL2
object.
- It introduces parse-demo, a function that can parse a command-line
into a demo-p. The command-line is represented as a list of strings; see
for instance argv to understand how to get the command-line
arguments given to ACL2.
Subtopics
- Parse-demo
- Parse arguments from the command line into a demo-p aggregate.
- Demo
- Raw constructor for demo-p structures.
- Make-demo
- Constructor macro for demo-p structures.
- Change-demo
- A copying macro that lets you create new demo-p structures, based on existing structures.
- Honsed-demo
- Raw constructor for honsed demo-p structures.
- Make-honsed-demo
- Constructor macro for honsed demo-p structures.
- *demo-usage*
- Automatically generated usage message.
- Demo->version
- Access the version field of a demo-p structure.
- Demo->verbose
- Access the verbose field of a demo-p structure.
- Demo->username
- Access the username field of a demo-p structure.
- Demo->port
- Access the port field of a demo-p structure.
- Demo->help
- Access the help field of a demo-p structure.
- Demo->extra-stuff2
- Access the extra-stuff2 field of a demo-p structure.
- Demo->extra-stuff
- Access the extra-stuff field of a demo-p structure.
- Demo->dirs
- Access the dirs field of a demo-p structure.
