		Search-engine friendly clone of the ACL2 documentation.

Acre-internals

Regex-concat2

Signature
(regex-concat2 x y) → res
Arguments: x — Guard (regex-p x).; y — Guard (regex-p y).
Returns: res — Type (regex-p res).

Definitions and Theorems

Function: regex-concat2

(defun regex-concat2 (x y)
 (declare (xargs :guard (and (regex-p x) (regex-p y))))
 (let ((__function__ 'regex-concat2))
  (declare (ignorable __function__))
  (regex-case
   x
   :exact
   (regex-case
    y :exact
    (regex-exact (concatenate 'string x.str y.str))
    :concat
    (b* (((when (atom y.lst)) (regex-fix x))
         (y1 (car y.lst)))
     (regex-case
         y1
         :exact
         (regex-concat
              (cons (regex-exact (concatenate 'string x.str y1.str))
                    (cdr y.lst)))
         :otherwise (regex-concat (cons x y.lst))))
    :otherwise (regex-concat (list x y)))
   :otherwise (regex-case y :exact
                          (if (equal y.str "")
                              (regex-fix x)
                            (regex-concat (list x y)))
                          :concat (regex-concat (cons x y.lst))
                          :otherwise (regex-concat (list x y))))))

Theorem: regex-p-of-regex-concat2

(defthm regex-p-of-regex-concat2
  (b* ((res (regex-concat2 x y)))
    (regex-p res))
  :rule-classes :rewrite)