(cst2ast-string-literal-content content double-quoted-p) → element
Function:
(defun cst2ast-string-literal-content (content double-quoted-p) (declare (xargs :guard (and (abnf::treep content) (booleanp double-quoted-p)))) (let ((__function__ 'cst2ast-string-literal-content)) (declare (ignorable __function__)) (b* (((unless (and (abnf::treep content) (abnf::tree-case content :nonleaf) (null (abnf::tree-nonleaf->rulename? content)))) (reserrf "bad structure for string literal content element")) (branches (abnf::tree-nonleaf->branches content)) ((unless (and (abnf::tree-list-listp branches) (equal (len branches) 1) (listp (car branches)) (equal (len (car branches)) 1))) (reserrf "bad structure for string literal content element 2")) (subtree (caar branches)) ((unless (and (abnf::treep subtree) (abnf::tree-case subtree :nonleaf))) (reserrf "bad structure for string literal content element 3")) (rulename (abnf::tree-nonleaf->rulename? subtree)) ((unless (or (and double-quoted-p (member-equal rulename *double-quoted-content-rulenames*)) (and (not double-quoted-p) (member-equal rulename *single-quoted-content-rulenames*)))) (reserrf "bad structure for string literal content element 4")) (string-element (cond ((equal rulename (abnf::rulename "escape-sequence")) (cst2ast-escape-sequence subtree)) (t (cst2ast-quoted-printable subtree double-quoted-p)))) ((when (reserrp string-element)) (reserrf "bad structure for string literal content element 4"))) string-element)))
Theorem:
(defthm string-element-resultp-of-cst2ast-string-literal-content (b* ((element (cst2ast-string-literal-content content double-quoted-p))) (string-element-resultp element)) :rule-classes :rewrite)