Check-user-term
Recognize untranslated terms that are valid for evaluation.
- Signature
(check-user-term x wrld) → (mv term/message stobjs-out)
- Arguments
- wrld — Guard (plist-worldp wrld).
- Returns
- term/message — A pseudo-termp or msgp.
- stobjs-out — A symbol-listp.
An untranslated term is a term as entered by the user.
This function checks x by attempting to translate it.
If the translation succeeds, the translated term is returned,
along with the stobjs-out list of the term (see below for details).
Otherwise, a structured error message is returned (printable with ~@),
along with nil as stobjs-out list.
These two possible outcomes can be distinguished by the fact that
the former yields a pseudo-term while the latter does not.
The stobjs-out list of a term is the term analogous
of the stobjs-out property of a function,
namely a list of symbols that is like a ``mask'' for the result.
A nil in the list means that
the corresponding result is a non-stobj value,
while the name of a stobj in the list means that
the corresponding result is the named stobj.
The list is a singleton, unless the term returns multiple values.
We create a fresh function symbol fn
and pass it to translate1-cmp as stobjs-out and binding.
This means that we are checking that the term
can be used in a function body.
This is stricter than checking the term to be valid
for use in a defthm and defun-nx.
If translate1-cmp is successful,
it returns updated bindings that associate fn
to the output stobjs of the term.
The check-user-term function does not terminate
if the translation expands an ill-behaved macro that does not terminate.
Definitions and Theorems
Function: check-user-term
(defun check-user-term (x wrld)
(declare (xargs :guard (plist-worldp wrld)))
(let ((__function__ 'check-user-term))
(declare (ignorable __function__))
(let ((fn (gen-new-name '__fn__ wrld)))
(mv-let (ctx term/message bindings)
(translate1-cmp x fn (cons (cons fn fn) 'nil)
t __function__
wrld (default-state-vars nil))
(declare (ignore ctx))
(if (pseudo-termp term/message)
(mv term/message (cdr (assoc fn bindings)))
(mv term/message nil))))))
