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)
(msg "Option ~s0 needs a valid port number, but got ~x1" name (car 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
Making the explicit-value explicit lets us very easily support this without requiring, e.g., that every argument has exactly one value.