		Search-engine friendly clone of the ACL2 documentation.

Parser

Parse-string-literal

Parse a string-literal.

Signature
(parse-string-literal token input) → (mv tree next-token rest-input)
Arguments: token — Guard (abnf::tree-optionp token).; input — Guard (abnf::tree-listp input).
Returns: tree — Type (abnf::tree-resultp tree).; next-token — Type (abnf::tree-optionp next-token).; rest-input — Type (abnf::tree-listp rest-input).

This is used when parsing console statements. We check if the next token is an atomic-literal that wraps a string-literal, and in that case we return the underlying string-literal.

Definitions and Theorems

Function: parse-string-literal

(defun parse-string-literal (token input)
  (declare (xargs :guard (and (abnf::tree-optionp token)
                              (abnf::tree-listp input))))
  (let ((__function__ 'parse-string-literal))
    (declare (ignorable __function__))
    (b* (((unless (abnf::tree-option-case token :some))
          (perr (list :found :no-token)))
         (tree (abnf::tree-option-some->val token))
         ((unless (and (abnf::tree-case tree :nonleaf)
                       (equal (abnf::tree-nonleaf->rulename? tree)
                              (abnf::rulename "atomic-literal"))))
          (perr (list :found tree)))
         (treess (abnf::tree-nonleaf->branches tree))
         ((unless (and (consp treess)
                       (not (consp (cdr treess)))))
          (perr :impossible))
         (trees (car treess))
         ((unless (and (consp trees)
                       (not (consp (cdr trees)))))
          (perr :impossible))
         (tree (car trees))
         ((mv token input) (parse-token input)))
      (mv tree token input))))

Theorem: tree-resultp-of-parse-string-literal.tree

(defthm tree-resultp-of-parse-string-literal.tree
  (b* (((mv ?tree ?next-token ?rest-input)
        (parse-string-literal token input)))
    (abnf::tree-resultp tree))
  :rule-classes :rewrite)

Theorem: tree-optionp-of-parse-string-literal.next-token

(defthm tree-optionp-of-parse-string-literal.next-token
  (b* (((mv ?tree ?next-token ?rest-input)
        (parse-string-literal token input)))
    (abnf::tree-optionp next-token))
  :rule-classes :rewrite)

Theorem: tree-listp-of-parse-string-literal.rest-input

(defthm tree-listp-of-parse-string-literal.rest-input
  (b* (((mv ?tree ?next-token ?rest-input)
        (parse-string-literal token input)))
    (abnf::tree-listp rest-input))
  :rule-classes :rewrite)

Theorem: parsize-of-parse-string-literal-<=

(defthm parsize-of-parse-string-literal-<=
  (b* (((mv ?tree ?next-token ?rest-input)
        (parse-string-literal token input)))
    (<= (parsize next-token rest-input)
        (parsize token input)))
  :rule-classes :linear)

Theorem: parsize-of-parse-string-literal-<

(defthm parsize-of-parse-string-literal-<
  (b* (((mv ?tree ?next-token ?rest-input)
        (parse-string-literal token input)))
    (implies (not (reserrp tree))
             (< (parsize next-token rest-input)
                (parsize token input))))
  :rule-classes :linear)

Theorem: parse-string-literal-of-tree-option-fix-token

(defthm parse-string-literal-of-tree-option-fix-token
  (equal (parse-string-literal (abnf::tree-option-fix token)
                               input)
         (parse-string-literal token input)))

Theorem: parse-string-literal-tree-option-equiv-congruence-on-token

(defthm parse-string-literal-tree-option-equiv-congruence-on-token
  (implies (abnf::tree-option-equiv token token-equiv)
           (equal (parse-string-literal token input)
                  (parse-string-literal token-equiv input)))
  :rule-classes :congruence)

Theorem: parse-string-literal-of-tree-list-fix-input

(defthm parse-string-literal-of-tree-list-fix-input
  (equal (parse-string-literal token (abnf::tree-list-fix input))
         (parse-string-literal token input)))

Theorem: parse-string-literal-tree-list-equiv-congruence-on-input

(defthm parse-string-literal-tree-list-equiv-congruence-on-input
  (implies (abnf::tree-list-equiv input input-equiv)
           (equal (parse-string-literal token input)
                  (parse-string-literal token input-equiv)))
  :rule-classes :congruence)