(svtv-parse-path-indices bracketed-parts lastp orig-x) → (mv errmsg path range-msb range-lsb)
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)