|
|
|---|
|
|
|
|---|
Cause an error if a function or lambda expression or term does not have a given number of results.
(ensure-function/lambda/term-number-of-results
stobjs-out n description
error-erp error-val ctx state)
→
(mv erp val state)
The number of results of the function or lambda expression or term is checked
by examining the stobjs-out list
of the function or lambda expression or term.
This error-checking function is useful after calling
ensure-function/macro/lambda (for a function or lambda expression)
or ensure-value-is-untranslated-term (for a term),
both of which return the stobjs-out list,
to handle functions and lambda expressions and terms uniformly.
The
Function:
(defun ensure-function/lambda/term-number-of-results (stobjs-out n description error-erp error-val ctx state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (symbol-listp stobjs-out) (posp n) (msgp description)))) (b* (((unless (= (len stobjs-out) n)) (er-soft+ ctx error-erp error-val "~@0 must return ~x1 ~@2." description n (if (= n 1) "result" "results")))) (value nil)))
Theorem:
(defthm return-type-of-ensure-function/lambda/term-number-of-results.erp (b* (((mv ?erp ?val ?state) (ensure-function/lambda/term-number-of-results stobjs-out n description error-erp error-val ctx state))) (implies erp (equal erp error-erp))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-ensure-function/lambda/term-number-of-results.val (b* (((mv ?erp ?val ?state) (ensure-function/lambda/term-number-of-results stobjs-out n description error-erp error-val ctx state))) (and (implies erp (equal val error-val)) (implies (and (not erp) error-erp) (not val)))) :rule-classes :rewrite)