Generate an alist from alternations to symbols, used for the table of option parsing functions.
(defdefparse-gen-option-alist args prefix) → alist
This is used by the
The
The string of the entry must be parsable as an ABNF option, from which we extract the alternation (in ABNF abstract syntax). The symbol of the entry is used to form a function name, together with the prefix given as input to defdefparse.
Function:
(defun defdefparse-gen-option-alist (args prefix) (declare (xargs :guard (and (true-listp args) (common-lisp::symbolp prefix)))) (let ((__function__ 'defdefparse-gen-option-alist)) (declare (ignorable __function__)) (b* (((when (endp args)) nil) ((cons option args) args) ((when (endp args)) (raise "Found an odd number of arguments.")) ((cons sym args) args) ((unless (common-lisp::stringp option)) (raise "The ~x0 argument must be a string." option)) ((mv err tree rest) (parse-option (string=>nats option))) ((when err) (raise "Cannot parse option ~s0: ~@1." option err)) ((unless (unsigned-byte-listp 8 rest)) (raise "Internal error: ~ rest ~x0 not all consisting of unsigned 8-bit bytes." rest)) ((when (consp rest)) (raise "Extra parsing ~s0 in option ~s1." (nats=>string rest) option)) (alt (abstract-group/option tree)) ((unless (common-lisp::symbolp sym)) (raise "The ~x0 argument must be a symbol." sym)) (fn (packn-pos (list prefix '- sym) prefix)) (alist (defdefparse-gen-option-alist args prefix)) ((when (member-equal alt (strip-cars alist))) (raise "Duplicate option ~s0." option)) ((when (member-eq fn (strip-cdrs alist))) (raise "Duplicate function ~x0." fn))) (acons alt fn alist))))
Theorem:
(defthm defdefparse-alt-symbol-alistp-of-defdefparse-gen-option-alist (b* ((alist (defdefparse-gen-option-alist args prefix))) (defdefparse-alt-symbol-alistp alist)) :rule-classes :rewrite)