		Search-engine friendly clone of the ACL2 documentation.

Expand.lisp

Svtv-parse-path-indices

Signature
(svtv-parse-path-indices bracketed-parts lastp orig-x) → (mv errmsg path range-msb range-lsb)
Arguments: bracketed-parts — strings of the form "[123".
Guard (string-listp bracketed-parts).; lastp — Guard (booleanp lastp).; orig-x — Guard (stringp orig-x).
Returns: path — Type (implies path (path-p path)).; range-msb — Type (or (not range-msb) (natp range-msb)).; range-lsb — Type (implies range-msb (natp range-lsb)).

Definitions and Theorems

Function: svtv-parse-path-indices

(defun svtv-parse-path-indices (bracketed-parts lastp orig-x)
 (declare (xargs :guard (and (string-listp bracketed-parts)
                             (booleanp lastp)
                             (stringp orig-x))))
 (declare (xargs :guard (consp bracketed-parts)))
 (let ((__function__ 'svtv-parse-path-indices))
  (declare (ignorable __function__))
  (b*
   ((orig-x (mbe :logic (str-fix orig-x)
                 :exec orig-x))
    ((mv err rest range-msb range-lsb)
     (if (atom (cdr bracketed-parts))
         (mv nil nil nil nil)
       (svtv-parse-path-indices (cdr bracketed-parts)
                                lastp orig-x)))
    ((when err) (mv err nil nil nil))
    (first (mbe :logic (str-fix (car bracketed-parts))
                :exec (car bracketed-parts)))
    ((unless (and (not (equal first ""))
                  (eql (char first 0) #\[)))
     (mv (msg "Missing [ at \"~s0]\" (inside \"~s1\""
              first orig-x)
         nil nil nil))
    ((mv first-index first-digits)
     (parse-nat-from-string first 0 0 1 (length first)))
    ((when (eql 0 first-digits))
     (mv (msg "Missing index in \"~s0]\" (inside \"~s1\""
              first orig-x)
         nil nil nil))
    ((when (equal (+ 1 first-digits)
                  (length first)))
     (mv nil
         (if rest (make-path-scope :namespace first-index
                                   :subpath rest)
           (make-path-wire :name first-index))
         range-msb range-lsb))
    ((unless (and lastp (atom (cdr bracketed-parts))))
     (mv
      (msg
       "Bad format for index: \"~s0]\" inside \"~s1\".  If this is ~
                  a partselect, they are only allowed last."
       first orig-x)
      nil nil nil))
    ((unless (eql (char first (+ 1 first-digits))
                  #\:))
     (mv (msg "Bad format for last index \"~s0]\" of \"~s1\"."
              first orig-x)
         nil nil nil))
    ((mv second-index second-digits)
     (parse-nat-from-string first 0 0 (+ 2 first-digits)
                            (length first)))
    ((when (eql 0 second-digits))
     (mv (msg "Missing index in \"~s0]\" (inside \"~s1\""
              first orig-x)
         nil nil nil))
    ((unless (eql (+ 2 first-digits second-digits)
                  (length first)))
     (mv
      (msg
       "Bad format for last index \"~s0]\" of \"~s1\" -- extra ~
                  stuff after second index."
       first orig-x)
      nil nil nil)))
   (mv nil nil first-index second-index))))

Theorem: return-type-of-svtv-parse-path-indices.path

(defthm return-type-of-svtv-parse-path-indices.path
  (b* (((mv ?errmsg ?path ?range-msb ?range-lsb)
        (svtv-parse-path-indices bracketed-parts lastp orig-x)))
    (implies path (path-p path)))
  :rule-classes :rewrite)

Theorem: return-type-of-svtv-parse-path-indices.range-msb

(defthm return-type-of-svtv-parse-path-indices.range-msb
  (b* (((mv ?errmsg ?path ?range-msb ?range-lsb)
        (svtv-parse-path-indices bracketed-parts lastp orig-x)))
    (or (not range-msb) (natp range-msb)))
  :rule-classes :type-prescription)

Theorem: return-type-of-svtv-parse-path-indices.range-lsb

(defthm return-type-of-svtv-parse-path-indices.range-lsb
  (b* (((mv ?errmsg ?path ?range-msb ?range-lsb)
        (svtv-parse-path-indices bracketed-parts lastp orig-x)))
    (implies range-msb (natp range-lsb)))
  :rule-classes :type-prescription)

Theorem: svtv-parse-path-indices-of-string-list-fix-bracketed-parts

(defthm svtv-parse-path-indices-of-string-list-fix-bracketed-parts
 (equal
     (svtv-parse-path-indices (str::string-list-fix bracketed-parts)
                              lastp orig-x)
     (svtv-parse-path-indices bracketed-parts lastp orig-x)))

Theorem: svtv-parse-path-indices-string-list-equiv-congruence-on-bracketed-parts

(defthm
 svtv-parse-path-indices-string-list-equiv-congruence-on-bracketed-parts
 (implies
  (str::string-list-equiv bracketed-parts bracketed-parts-equiv)
  (equal
      (svtv-parse-path-indices bracketed-parts lastp orig-x)
      (svtv-parse-path-indices bracketed-parts-equiv lastp orig-x)))
 :rule-classes :congruence)

Theorem: svtv-parse-path-indices-of-bool-fix-lastp

(defthm svtv-parse-path-indices-of-bool-fix-lastp
  (equal (svtv-parse-path-indices bracketed-parts (bool-fix lastp)
                                  orig-x)
         (svtv-parse-path-indices bracketed-parts lastp orig-x)))

Theorem: svtv-parse-path-indices-iff-congruence-on-lastp

(defthm svtv-parse-path-indices-iff-congruence-on-lastp
 (implies
  (iff lastp lastp-equiv)
  (equal
      (svtv-parse-path-indices bracketed-parts lastp orig-x)
      (svtv-parse-path-indices bracketed-parts lastp-equiv orig-x)))
 :rule-classes :congruence)

Theorem: svtv-parse-path-indices-of-str-fix-orig-x

(defthm svtv-parse-path-indices-of-str-fix-orig-x
 (equal
    (svtv-parse-path-indices bracketed-parts lastp (str-fix orig-x))
    (svtv-parse-path-indices bracketed-parts lastp orig-x)))

Theorem: svtv-parse-path-indices-streqv-congruence-on-orig-x

(defthm svtv-parse-path-indices-streqv-congruence-on-orig-x
 (implies
  (acl2::streqv orig-x orig-x-equiv)
  (equal
      (svtv-parse-path-indices bracketed-parts lastp orig-x)
      (svtv-parse-path-indices bracketed-parts lastp orig-x-equiv)))
 :rule-classes :congruence)