(svtv-parse-path/select-aux dotted-parts orig-x) → (mv errmsg path range-msb range-lsb)
Function:
(defun svtv-parse-path/select-aux (dotted-parts orig-x) (declare (xargs :guard (and (string-listp dotted-parts) (stringp orig-x)))) (let ((__function__ 'svtv-parse-path/select-aux)) (declare (ignorable __function__)) (b* ((orig-x (mbe :logic (str-fix orig-x) :exec orig-x)) ((when (atom dotted-parts)) (mv (msg "Error -- empty wire path? \"~s0\"" orig-x) nil nil nil)) (lastp (atom (cdr dotted-parts))) (part1 (mbe :logic (str-fix (car dotted-parts)) :exec (car dotted-parts))) ((unless (and (not (equal part1 "")) (eql (char part1 (1- (length part1))) #\]))) (b* (((when lastp) (mv nil (make-path-wire :name part1) nil nil)) ((mv errmsg rest range-msb range-lsb) (svtv-parse-path/select-aux (cdr dotted-parts) orig-x)) ((when errmsg) (mv errmsg nil nil nil))) (mv nil (make-path-scope :subpath rest :namespace part1) range-msb range-lsb))) (lbrack-pos (strpos "[" part1)) ((unless lbrack-pos) (mv (msg "Found ] without previous [: \"~s0\" inside \"~s1\"" part1 orig-x) nil nil nil)) (name-part (subseq part1 0 lbrack-pos)) (bracketed-part (subseq part1 lbrack-pos nil)) (bracketed-parts (strtok bracketed-part '(#\]))) ((unless bracketed-parts) (mv "This shouldn't happen." nil nil nil)) ((mv err index-path range-msb range-lsb) (svtv-parse-path-indices bracketed-parts lastp orig-x)) ((when err) (mv err nil nil nil)) ((when lastp) (mv nil (if index-path (make-path-scope :namespace name-part :subpath index-path) (make-path-wire :name name-part)) range-msb range-lsb)) ((mv err rest-path range-msb range-lsb) (svtv-parse-path/select-aux (cdr dotted-parts) orig-x)) ((when err) (mv err nil nil nil))) (mv nil (make-path-scope :namespace name-part :subpath (if index-path (path-append index-path rest-path) rest-path)) range-msb range-lsb))))
Theorem:
(defthm return-type-of-svtv-parse-path/select-aux.path (b* (((mv ?errmsg ?path ?range-msb ?range-lsb) (svtv-parse-path/select-aux dotted-parts orig-x))) (implies (not errmsg) (path-p path))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-svtv-parse-path/select-aux.range-msb (b* (((mv ?errmsg ?path ?range-msb ?range-lsb) (svtv-parse-path/select-aux dotted-parts orig-x))) (or (not range-msb) (natp range-msb))) :rule-classes :type-prescription)
Theorem:
(defthm return-type-of-svtv-parse-path/select-aux.range-lsb (b* (((mv ?errmsg ?path ?range-msb ?range-lsb) (svtv-parse-path/select-aux dotted-parts orig-x))) (implies range-msb (natp range-lsb))) :rule-classes :type-prescription)
Theorem:
(defthm svtv-parse-path/select-aux-of-string-list-fix-dotted-parts (equal (svtv-parse-path/select-aux (str::string-list-fix dotted-parts) orig-x) (svtv-parse-path/select-aux dotted-parts orig-x)))
Theorem:
(defthm svtv-parse-path/select-aux-string-list-equiv-congruence-on-dotted-parts (implies (str::string-list-equiv dotted-parts dotted-parts-equiv) (equal (svtv-parse-path/select-aux dotted-parts orig-x) (svtv-parse-path/select-aux dotted-parts-equiv orig-x))) :rule-classes :congruence)
Theorem:
(defthm svtv-parse-path/select-aux-of-str-fix-orig-x (equal (svtv-parse-path/select-aux dotted-parts (str-fix orig-x)) (svtv-parse-path/select-aux dotted-parts orig-x)))
Theorem:
(defthm svtv-parse-path/select-aux-streqv-congruence-on-orig-x (implies (acl2::streqv orig-x orig-x-equiv) (equal (svtv-parse-path/select-aux dotted-parts orig-x) (svtv-parse-path/select-aux dotted-parts orig-x-equiv))) :rule-classes :congruence)