		Search-engine friendly clone of the ACL2 documentation.

Parsers

Custom-parser

How to write custom argument-parsing functions.

You can extend getopt with new functions for parsing the arguments you care about.

Note that once you have introduced such a new parsing function, you can (optionally) register it as the default parser for a predicate using defparser.

Every argument-parsing function must have the following form:

(parse-foo name explicit-value args) 
  → 
(mv errmsg? value rest-args)

Inputs:

name is a string that is the name of the option the user typed in, e.g., it might be --verbose. This is included so that the parser can provide a nice error message.
explicit-value is nil unless the use types something like --foo=bar, in which case it is the value being assigned, e.g., "bar".
args is a string-listp with the full command line arguments that the user typed in after the name and, if applicable, the explicit-value. It may be the empty list if name was the last argument to the program.

Outputs

errmsg? should be nil if everything is okay, or an error message produced by msg. Typically it might be something like:
```
(msg "Option ~s0 needs a valid port number, but got ~x1"
       name (car args))
```
value is irrelevant if there was an error, but otherwise must be a valid foop, for whatever kind of data this parser is supposed to generate.
rest-args should be the remainder of args after the arguments to name have been removed. For termination, its length must be no greater than the length of args.

All of the built-in parsers fit into the above scheme, so you can see several examples of argument-parsing functions by just looking at the built-in parsers like parse-nat.

You might wonder why we have the explicit-value separate from args. The basic reason is that we want to support any mixture of the following syntaxes:

--color red ...
--color=red ...

Making the explicit-value explicit lets us very easily support this without requiring, e.g., that every argument has exactly one value.