		Search-engine friendly clone of the ACL2 documentation.

Defdefparse-event-generation

Defdefparse-gen-repetition-alist

Generate an alist from alternations to symbols, used for the table of repetition parsing functions.

Signature
(defdefparse-gen-repetition-alist args prefix) → alist
Arguments: args — Guard (true-listp args).; prefix — Guard (common-lisp::symbolp prefix).
Returns: alist — Type (defdefparse-rep-symbol-alistp alist).

This is used by the defparse-name-repetition-table macros generated by defdefparse.

The args parameter of this ACL2 function consists of the arguments of the defparse-name-repetition-table, which must be an even number of alternating strings and symbols. Each adjacent string-symbol pair specifies an entry in the alist.

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.

Definitions and Theorems

Function: defdefparse-gen-repetition-alist

(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: defdefparse-rep-symbol-alistp-of-defdefparse-gen-repetition-alist

(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)