Fresh-namep-msg
Return either nil or
a message indicating why the name is not a legal new name.
- Signature
(fresh-namep-msg name type wrld state)
→
(mv erp msg/nil state)
- Arguments
- name — Guard (symbolp name).
- wrld — Guard (plist-worldp wrld).
- Returns
- erp — Always nil.
- msg/nil — A message (see msg) or nil.
Returns an error triple
(mv nil msg/nil state),
where msg/nil is either nil or
a message (see msg) indicating why the given name
is not legal for a definition of the given type:
function for defun,
macro for defmacro,
const for defconst,
stobj for defstobj,
constrained-function for defchoose,
and otherwise nil (for other kinds of events,
for example defthm and deflabel).
See name.
WARNING: This is an incomplete check in the case of a stobj name,
because the field names required for a more complete check
are not supplied as inputs.
Implementation Note. This function modifies state,
because the check for legality of new definitions
(carried out by ACL2 source function chk-virgin-msg) modifies state.
That modification is necessary because for all we know,
raw Lisp is adding or removing function definitions
that we don't know about without our having modified state;
so logically, we pop the oracle when making this check.
End of Implementation Note.
Definitions and Theorems
Function: fresh-namep-msg
(defun fresh-namep-msg (name type wrld state)
(declare (xargs :stobjs (state)))
(declare (xargs :guard (and (symbolp name)
(plist-worldp wrld))))
(declare
(xargs
:guard
(member-eq type
'(function macro
const stobj constrained-function nil))))
(let ((__function__ 'fresh-namep-msg))
(declare (ignorable __function__))
(let ((msg (fresh-namep-msg-weak name type wrld)))
(cond (msg (value msg))
(t (mv-let (msg state)
(chk-virgin-msg name type wrld state)
(value msg)))))))
