Essentially treats
(vl-parse-cmdline-define x loc stickyp) → (mv okp name def)
BOZO we could do better sanity checking here.
Function:
(defun vl-parse-cmdline-define (x loc stickyp) (declare (xargs :guard (and (stringp x) (vl-location-p loc) (booleanp stickyp)))) (let ((__function__ 'vl-parse-cmdline-define)) (declare (ignorable __function__)) (b* ((x (string-fix x)) (pos (position #\= x)) ((unless pos) (mv t x (make-vl-define :formals nil :body "" :loc loc :stickyp stickyp))) ((unless (< (+ 1 pos) (length x))) (mv nil nil nil)) (name (subseq x 0 pos)) (body (subseq x (+ 1 pos) nil))) (mv t name (make-vl-define :formals nil :body body :loc loc :stickyp stickyp)))))
Theorem:
(defthm booleanp-of-vl-parse-cmdline-define.okp (b* (((mv ?okp ?name ?def) (vl-parse-cmdline-define x loc stickyp))) (booleanp okp)) :rule-classes :type-prescription)
Theorem:
(defthm return-type-of-vl-parse-cmdline-define.name (b* (((mv ?okp ?name ?def) (vl-parse-cmdline-define x loc stickyp))) (iff (stringp name) okp)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-parse-cmdline-define.def (b* (((mv ?okp ?name ?def) (vl-parse-cmdline-define x loc stickyp))) (iff (vl-define-p def) okp)) :rule-classes :rewrite)
Theorem:
(defthm vl-parse-cmdline-define-of-str-fix-x (equal (vl-parse-cmdline-define (str-fix x) loc stickyp) (vl-parse-cmdline-define x loc stickyp)))
Theorem:
(defthm vl-parse-cmdline-define-streqv-congruence-on-x (implies (streqv x x-equiv) (equal (vl-parse-cmdline-define x loc stickyp) (vl-parse-cmdline-define x-equiv loc stickyp))) :rule-classes :congruence)
Theorem:
(defthm vl-parse-cmdline-define-of-vl-location-fix-loc (equal (vl-parse-cmdline-define x (vl-location-fix loc) stickyp) (vl-parse-cmdline-define x loc stickyp)))
Theorem:
(defthm vl-parse-cmdline-define-vl-location-equiv-congruence-on-loc (implies (vl-location-equiv loc loc-equiv) (equal (vl-parse-cmdline-define x loc stickyp) (vl-parse-cmdline-define x loc-equiv stickyp))) :rule-classes :congruence)
Theorem:
(defthm vl-parse-cmdline-define-of-bool-fix-stickyp (equal (vl-parse-cmdline-define x loc (acl2::bool-fix stickyp)) (vl-parse-cmdline-define x loc stickyp)))
Theorem:
(defthm vl-parse-cmdline-define-iff-congruence-on-stickyp (implies (iff stickyp stickyp-equiv) (equal (vl-parse-cmdline-define x loc stickyp) (vl-parse-cmdline-define x loc stickyp-equiv))) :rule-classes :congruence)