		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abstract-quoted-string

A quoted-string parse tree is abstracted to its character string.

Signature
(abstract-quoted-string tree) → charstring
Arguments: tree — Guard (treep tree).
Returns: charstring — Type (common-lisp::stringp charstring).

Definitions and Theorems

Function: abstract-quoted-string

(defun abstract-quoted-string (tree)
  (declare (xargs :guard (treep tree)))
  (b* (((fun (fail))
        (prog2$ (abstract-fail) ""))
       ((unless (tree-case tree :nonleaf))
        (fail))
       (treess (tree-nonleaf->branches tree))
       ((unless (and (consp treess)
                     (consp (cdr treess))
                     (consp (cddr treess))))
        (fail))
       (trees (cadr treess))
       (nats (abstract-*-grouped-terminal trees))
       ((unless (unsigned-byte-listp 8 nats))
        (fail)))
    (nats=>string nats)))

Theorem: stringp-of-abstract-quoted-string

(defthm stringp-of-abstract-quoted-string
  (b* ((charstring (abstract-quoted-string tree)))
    (common-lisp::stringp charstring))
  :rule-classes :rewrite)