Arity+
Enhanced variant of arity.
- Signature
(arity+ fn wrld) → arity
- Arguments
- fn — Guard (pseudo-termfnp fn).
- wrld — Guard (plist-worldp wrld).
- Returns
- arity — Type (natp arity).
This returns the same result as arity
on named functions and lambda expressions,
but it causes an error on symbols that do not name functions
(while arity returns nil in this case).
Compared to arity,
arity+ has a slightly stronger guard on fn
but a weaker guard on wrld.
The reason for weakening the guard on wrld,
from plist-worldp-with-formals to plist-worldp
is a practical one:
when doing system programming,
currently plist-worldp is normally used for the ACL2 world,
so using plist-worldp-with-formals in some system utilities
(like arity+ here)
would essentially force its use in many or all the other utilities.
Since arity has a stronger guard on the world,
in order for arity+ to be guard-verified,
it cannot call arity.
Thus, here we replicate the (simple) code of arity,
with the only slight difference that, logically,
we return 0 if fn does not name a function
(but in this case an error actually occurs),
so that the return type theorem is simpler.
Definitions and Theorems
Function: arity+
(defun arity+ (fn wrld)
(declare (xargs :guard (and (pseudo-termfnp fn)
(plist-worldp wrld))))
(let ((__function__ 'arity+))
(declare (ignorable __function__))
(cond
((flambdap fn)
(len (lambda-formals fn)))
(t (len (b* ((formals (getpropc fn 'formals t wrld)))
(if (eq formals t)
(raise "The symbol ~x0 does not name a function."
fn)
formals)))))))
Theorem: natp-of-arity+
(defthm natp-of-arity+
(b* ((arity (arity+ fn wrld)))
(natp arity))
:rule-classes :rewrite)
