Generate an alist from alternations to symbols, used for the table of repetition parsing functions.
(defdefparse-gen-repetition-alist args prefix) → alist
This is used by the
The
The string of the entry must be parsable as an ABNF repetition, from which we obtain the repetition (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-repetition-alist (args prefix) (declare (xargs :guard (and (true-listp args) (common-lisp::symbolp prefix)))) (let ((__function__ 'defdefparse-gen-repetition-alist)) (declare (ignorable __function__)) (b* (((when (endp args)) nil) ((cons repetition args) args) ((when (endp args)) (raise "Found an odd number of arguments.")) ((cons sym args) args) ((unless (common-lisp::stringp repetition)) (raise "The ~x0 argument must be a string." repetition)) ((mv err tree rest) (parse-repetition (string=>nats repetition))) ((when err) (raise "Cannot parse repetition ~s0: ~@1." repetition 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 repetition ~s1." (nats=>string rest) repetition)) (rep (abstract-repetition 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-repetition-alist args prefix)) ((when (member-equal rep (strip-cars alist))) (raise "Duplicate repetition ~s0." repetition)) ((when (member-eq fn (strip-cdrs alist))) (raise "Duplicate function ~x0." fn))) (acons rep fn alist))))
Theorem:
(defthm defdefparse-rep-symbol-alistp-of-defdefparse-gen-repetition-alist (b* ((alist (defdefparse-gen-repetition-alist args prefix))) (defdefparse-rep-symbol-alistp alist)) :rule-classes :rewrite)