		Search-engine friendly clone of the ACL2 documentation.

Acre-internals

Parse-octal-charcode

Signature
(parse-octal-charcode x index) → (mv err char new-index)
Arguments: x — Guard (stringp x).; index — Guard (natp index).
Returns: err — Type (acl2::maybe-stringp err).; char — Type (characterp char).; new-index — Type (natp new-index).

Definitions and Theorems

Function: parse-octal-charcode

(defun parse-octal-charcode (x index)
 (declare (xargs :guard (and (stringp x) (natp index))))
 (let ((__function__ 'parse-octal-charcode))
   (declare (ignorable __function__))
   (b*
     ((index (lnfix index))
      ((unless (< (+ 2 index) (strlen x)))
       (mv "String ended within octal charcode"
           (code-char 0)
           index))
      (octal0 (char x index))
      (octal1 (char x (+ 1 index)))
      (octal2 (char x (+ 2 index)))
      ((unless (and (str::oct-digit-char-p octal0)
                    (str::oct-digit-char-p octal1)
                    (str::oct-digit-char-p octal2)))
       (mv "Malformed octal charcode" (code-char 0)
           index))
      (val (str::oct-digit-chars-value (list octal0 octal1 octal2)))
      ((when (<= 256 val))
       (mv "Octal charcodes greater than 256 not supported"
           (code-char 0)
           index)))
     (mv nil (code-char val) (+ 3 index)))))

Theorem: maybe-stringp-of-parse-octal-charcode.err

(defthm maybe-stringp-of-parse-octal-charcode.err
  (b* (((mv ?err common-lisp::?char ?new-index)
        (parse-octal-charcode x index)))
    (acl2::maybe-stringp err))
  :rule-classes :type-prescription)

Theorem: characterp-of-parse-octal-charcode.char

(defthm characterp-of-parse-octal-charcode.char
  (b* (((mv ?err common-lisp::?char ?new-index)
        (parse-octal-charcode x index)))
    (characterp char))
  :rule-classes :rewrite)

Theorem: natp-of-parse-octal-charcode.new-index

(defthm natp-of-parse-octal-charcode.new-index
  (b* (((mv ?err common-lisp::?char ?new-index)
        (parse-octal-charcode x index)))
    (natp new-index))
  :rule-classes :type-prescription)

Theorem: new-index-of-parse-octal-charcode

(defthm new-index-of-parse-octal-charcode
  (b* (((mv ?err common-lisp::?char ?new-index)
        (parse-octal-charcode x index)))
    (<= (nfix index) new-index))
  :rule-classes :linear)

Theorem: new-index-of-parse-octal-charcode-strong

(defthm new-index-of-parse-octal-charcode-strong
  (b* (((mv ?err common-lisp::?char ?new-index)
        (parse-octal-charcode x index)))
    (implies (not err)
             (< (nfix index) new-index)))
  :rule-classes :linear)

Theorem: new-index-of-parse-octal-charcode-less-than-length

(defthm new-index-of-parse-octal-charcode-less-than-length
  (b* (((mv ?err common-lisp::?char ?new-index)
        (parse-octal-charcode x index)))
    (implies (<= (nfix index)
                 (len (acl2::explode x)))
             (<= new-index (len (acl2::explode x)))))
  :rule-classes :linear)

Theorem: parse-octal-charcode-of-str-fix-x

(defthm parse-octal-charcode-of-str-fix-x
  (equal (parse-octal-charcode (acl2::str-fix x)
                               index)
         (parse-octal-charcode x index)))

Theorem: parse-octal-charcode-streqv-congruence-on-x

(defthm parse-octal-charcode-streqv-congruence-on-x
  (implies (acl2::streqv x x-equiv)
           (equal (parse-octal-charcode x index)
                  (parse-octal-charcode x-equiv index)))
  :rule-classes :congruence)

Theorem: parse-octal-charcode-of-nfix-index

(defthm parse-octal-charcode-of-nfix-index
  (equal (parse-octal-charcode x (nfix index))
         (parse-octal-charcode x index)))

Theorem: parse-octal-charcode-nat-equiv-congruence-on-index

(defthm parse-octal-charcode-nat-equiv-congruence-on-index
  (implies (acl2::nat-equiv index index-equiv)
           (equal (parse-octal-charcode x index)
                  (parse-octal-charcode x index-equiv)))
  :rule-classes :congruence)