		Search-engine friendly clone of the ACL2 documentation.

Defdefparse-event-generation

Defdefparse-gen-group-alist

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

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

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

The args parameter of this ACL2 function consists of the arguments of the defparse-name-group-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 group, 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.

Definitions and Theorems

Function: defdefparse-gen-group-alist

(defun defdefparse-gen-group-alist (args prefix)
 (declare (xargs :guard (and (true-listp args)
                             (common-lisp::symbolp prefix))))
 (let ((__function__ 'defdefparse-gen-group-alist))
  (declare (ignorable __function__))
  (b*
   (((when (endp args)) nil)
    ((cons group args) args)
    ((when (endp args))
     (raise "Found an odd number of arguments."))
    ((cons sym args) args)
    ((unless (common-lisp::stringp group))
     (raise "The ~x0 argument must be a string."
            group))
    ((mv err tree rest)
     (parse-group (string=>nats group)))
    ((when err)
     (raise "Cannot parse group ~s0: ~@1."
            group 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 group ~s1."
            (nats=>string rest)
            group))
    (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-group-alist args prefix))
    ((when (member-equal alt (strip-cars alist)))
     (raise "Duplicate group ~s0." group))
    ((when (member-eq fn (strip-cdrs alist)))
     (raise "Duplicate function ~x0." fn)))
   (acons alt fn alist))))

Theorem: defdefparse-alt-symbol-alistp-of-defdefparse-gen-group-alist

(defthm defdefparse-alt-symbol-alistp-of-defdefparse-gen-group-alist
  (b* ((alist (defdefparse-gen-group-alist args prefix)))
    (defdefparse-alt-symbol-alistp alist))
  :rule-classes :rewrite)