Recognize calls of a particular system function call, without any arity checking.
For instance, to see if
(vl-*ary-syscall-p "$size" x)
Function:
(defun vl-*ary-syscall-p (name x) (declare (xargs :guard (and (stringp name) (vl-expr-p x)))) (let ((__function__ 'vl-*ary-syscall-p)) (declare (ignorable __function__)) (b* (((when (vl-fast-atom-p x)) nil) ((vl-nonatom x)) ((unless (and (eq x.op :vl-syscall) (consp x.args))) nil) (fn (first x.args)) ((unless (vl-sysfunexpr-p fn)) nil)) (equal (vl-sysfunexpr->name fn) (string-fix name)))))
Theorem:
(defthm arity-stuff-about-vl-*ary-syscall-p (implies (vl-*ary-syscall-p name x) (and (not (equal (vl-expr-kind x) :atom)) (equal (vl-nonatom->op x) :vl-syscall) (consp (vl-nonatom->args x)))) :rule-classes :forward-chaining)
Theorem:
(defthm vl-*ary-syscall-p-of-str-fix-name (equal (vl-*ary-syscall-p (str-fix name) x) (vl-*ary-syscall-p name x)))
Theorem:
(defthm vl-*ary-syscall-p-streqv-congruence-on-name (implies (streqv name name-equiv) (equal (vl-*ary-syscall-p name x) (vl-*ary-syscall-p name-equiv x))) :rule-classes :congruence)
Theorem:
(defthm vl-*ary-syscall-p-of-vl-expr-fix-x (equal (vl-*ary-syscall-p name (vl-expr-fix x)) (vl-*ary-syscall-p name x)))
Theorem:
(defthm vl-*ary-syscall-p-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-*ary-syscall-p name x) (vl-*ary-syscall-p name x-equiv))) :rule-classes :congruence)