		Search-engine friendly clone of the ACL2 documentation.

Convenience-constructors

/_

Construct a concatenation from a variable number of repetitions.

If an element is supplied, it is promoted to a repetition of one instance of the element. If a rule name is supplied, it is promoted first to a rule element and then to a repetition of one instance of that element. If a character string is supplied, it is promoted first to a case-insensitive character value notation element and then to a repetition of one instance of that element.

The name of this macro is inspired by the fact that the concatenations of an alternation are separated by / in ABNF: when writing a sequence of concatenations (i.e. when writing an alternation) with this macro, the resulting sequence will have a / separating the concatenations (plus an extra / at the beginning). See the core rules and the concrete syntax rules.

Macro: /_

(defmacro /_ (&rest xs)
  (cons '/_-fn
        (cons (cons 'list xs) 'nil)))

Definitions and Theorems

Function: /_-fn

(defun /_-fn (xs)
 (declare
   (xargs :guard (repetition/element/rulename/charstring-listp xs)))
 (cond
  ((endp xs) nil)
  (t
   (b*
    ((x (car xs))
     (range1 (make-repeat-range :min 1
                                :max (nati-finite 1)))
     (repetition
      (cond
       ((elementp x)
        (make-repetition :range range1
                         :element x))
       ((rulenamep x)
        (make-repetition :range range1
                         :element (element-rulename x)))
       ((common-lisp::stringp x)
        (make-repetition
          :range range1
          :element (element-char-val (char-val-insensitive nil x))))
       (t (repetition-fix x)))))
    (cons repetition (/_-fn (cdr xs)))))))

Theorem: concatenationp-of-/_-fn

(defthm concatenationp-of-/_-fn
  (b* ((concatenation (/_-fn xs)))
    (concatenationp concatenation))
  :rule-classes :rewrite)