		Search-engine friendly clone of the ACL2 documentation.

Defdefparse-event-generation

Defdefparse-gen-option-alist

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

Signature
(defdefparse-gen-option-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-option-table macros generated by defdefparse.

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

Definitions and Theorems

Function: defdefparse-gen-option-alist

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

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