		Search-engine friendly clone of the ACL2 documentation.

Format-strings

Parse-format-chars

Signature
(parse-format-chars chars parse-state) → (mv erp chars/containers)
Arguments: chars — Guard (char-listp chars).; parse-state — Guard (symbolp parse-state).
Returns: erp — Type (booleanp erp).; chars/containers — Type (char/container-listp chars/containers).

Definitions and Theorems

Function: parse-format-chars

(defun parse-format-chars (chars parse-state)
 (declare (xargs :guard (and (char-listp chars)
                             (symbolp parse-state))))
 (let ((__function__ 'parse-format-chars))
  (declare (ignorable __function__))
  (b*
   (((when (endp chars))
     (case parse-state
      (:base (mv nil nil))
      (:open{ (mv t nil))
      (:close} (mv t nil))
      (t
       (mv
         t
         (er hard? 'top-level
             "parse-state should be :base or :open{ or :close}")))))
    (first-char (first chars))
    (code (char->codepoint first-char))
    (rest-chars (rest chars)))
   (case parse-state
    (:base
         (if (= code 123)
             (parse-format-chars rest-chars :open{)
           (if (= code 125)
               (parse-format-chars rest-chars :close})
             (b* (((mv rest-erp rest-parsed)
                   (parse-format-chars rest-chars :base))
                  ((when rest-erp) (mv t nil)))
               (mv nil
                   (cons (make-char/container-char :get first-char)
                         rest-parsed))))))
    (:open{
         (if (= code 123)
             (b* (((mv rest-erp rest-parsed)
                   (parse-format-chars rest-chars :base))
                  ((when rest-erp) (mv t nil)))
               (mv nil
                   (cons (make-char/container-char :get first-char)
                         rest-parsed)))
           (if (= code 125)
               (b* (((mv rest-erp rest-parsed)
                     (parse-format-chars rest-chars :base))
                    ((when rest-erp) (mv t nil)))
                 (mv nil
                     (cons (make-char/container-container)
                           rest-parsed)))
             (mv t nil))))
    (:close}
         (if (= code 125)
             (b* (((mv rest-erp rest-parsed)
                   (parse-format-chars rest-chars :base))
                  ((when rest-erp) (mv t nil)))
               (mv nil
                   (cons (make-char/container-char :get first-char)
                         rest-parsed)))
           (mv t nil)))
    (t
     (mv
       t
       (er hard? 'top-level
           "parse-state should be :base or :open{ or :close}")))))))

Theorem: booleanp-of-parse-format-chars.erp

(defthm booleanp-of-parse-format-chars.erp
  (b* (((mv ?erp ?chars/containers)
        (parse-format-chars chars parse-state)))
    (booleanp erp))
  :rule-classes :rewrite)

Theorem: char/container-listp-of-parse-format-chars.chars/containers

(defthm char/container-listp-of-parse-format-chars.chars/containers
  (b* (((mv ?erp ?chars/containers)
        (parse-format-chars chars parse-state)))
    (char/container-listp chars/containers))
  :rule-classes :rewrite)