		Search-engine friendly clone of the ACL2 documentation.

Acre-internals

Preproc-legible-aux

Signature
(preproc-legible-aux x index acc) → new-x
Arguments: x — Guard (stringp x).; index — Guard (natp index).; acc — Guard (character-listp acc).
Returns: new-x — Type (stringp new-x).

Definitions and Theorems

Function: preproc-legible-aux

(defun preproc-legible-aux (x index acc)
 (declare (xargs :guard (and (stringp x)
                             (natp index)
                             (character-listp acc))))
 (declare (xargs :guard (<= index (strlen x))))
 (let ((__function__ 'preproc-legible-aux))
   (declare (ignorable __function__))
   (b*
    (((when (mbe :logic (zp (- (strlen x) (nfix index)))
                 :exec (eql index (strlen x))))
      (mbe :logic (reverse (coerce (make-character-list acc)
                                   'string))
           :exec (reverse (coerce acc 'string))))
     (x (lstrfix x))
     (index (lnfix index))
     (char (char x index))
     ((when (member char
                    '(#\Newline #\Space #\Tab #\Return #\Page)))
      (preproc-legible-aux x (+ 1 index) acc))
     ((when (eql char #\#))
      (b* ((index (find-substr (coerce '(#\Newline) 'string)
                               x index))
           ((unless index)
            (reverse (coerce acc 'string))))
        (preproc-legible-aux x (+ 1 index)
                             acc)))
     ((unless (and (eql char #\\)
                   (< (+ 1 index) (strlen x))))
      (preproc-legible-aux x (+ 1 index)
                           (cons char acc)))
     (char2 (char x (+ 1 index)))
     ((when (member (char x (+ 1 index))
                    '(#\Newline #\Space #\Tab #\Return #\Page #\#)))
      (preproc-legible-aux x (+ 2 index)
                           (cons char2 acc))))
    (preproc-legible-aux x (+ 2 index)
                         (cons char2 (cons char acc))))))

Theorem: stringp-of-preproc-legible-aux

(defthm stringp-of-preproc-legible-aux
  (b* ((new-x (preproc-legible-aux x index acc)))
    (stringp new-x))
  :rule-classes :type-prescription)

Theorem: preproc-legible-aux-of-str-fix-x

(defthm preproc-legible-aux-of-str-fix-x
  (equal (preproc-legible-aux (acl2::str-fix x)
                              index acc)
         (preproc-legible-aux x index acc)))

Theorem: preproc-legible-aux-streqv-congruence-on-x

(defthm preproc-legible-aux-streqv-congruence-on-x
  (implies (acl2::streqv x x-equiv)
           (equal (preproc-legible-aux x index acc)
                  (preproc-legible-aux x-equiv index acc)))
  :rule-classes :congruence)

Theorem: preproc-legible-aux-of-nfix-index

(defthm preproc-legible-aux-of-nfix-index
  (equal (preproc-legible-aux x (nfix index) acc)
         (preproc-legible-aux x index acc)))

Theorem: preproc-legible-aux-nat-equiv-congruence-on-index

(defthm preproc-legible-aux-nat-equiv-congruence-on-index
  (implies (acl2::nat-equiv index index-equiv)
           (equal (preproc-legible-aux x index acc)
                  (preproc-legible-aux x index-equiv acc)))
  :rule-classes :congruence)

Theorem: preproc-legible-aux-of-make-character-list-acc

(defthm preproc-legible-aux-of-make-character-list-acc
  (equal (preproc-legible-aux x index (make-character-list acc))
         (preproc-legible-aux x index acc)))

Theorem: preproc-legible-aux-charlisteqv-congruence-on-acc

(defthm preproc-legible-aux-charlisteqv-congruence-on-acc
  (implies (str::charlisteqv acc acc-equiv)
           (equal (preproc-legible-aux x index acc)
                  (preproc-legible-aux x index acc-equiv)))
  :rule-classes :congruence)