Generate the function and the macro.
(def-error-checker-fn name xs returns returns-supplied-p conditions-messages result mode verify-guards verify-guards-supplied-p parents parents-supplied-p short short-supplied-p long long-supplied-p def-error-checker-call state) → function+macro
Function:
(defun def-error-checker-fn (name xs returns returns-supplied-p conditions-messages result mode verify-guards verify-guards-supplied-p parents parents-supplied-p short short-supplied-p long long-supplied-p def-error-checker-call state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (symbolp name) (true-listp xs) (booleanp returns-supplied-p) (true-list-listp conditions-messages) (member-eq mode '(:logic :program)) (booleanp verify-guards) (booleanp verify-guards-supplied-p) (symbol-listp parents) (booleanp parents-supplied-p) (booleanp short-supplied-p) (booleanp long-supplied-p) (pseudo-event-formp def-error-checker-call)))) (let ((__function__ 'def-error-checker-fn)) (declare (ignorable __function__)) (b* (((when (assoc-equal def-error-checker-call (table-alist 'def-error-checker-calls (w state)))) '(value-triple :redundant)) (function-name name) (macro-name (add-suffix name "$")) (description (intern-in-package-of-symbol "DESCRIPTION" name)) (error-erp (intern-in-package-of-symbol "ERROR-ERP" name)) (error-val (intern-in-package-of-symbol "ERROR-VAL" name)) (erp (intern-in-package-of-symbol "ERP" name)) (val (intern-in-package-of-symbol "VAL" name)) (function (cons 'define (cons function-name (cons (append xs (cons (cons description '(msgp)) (cons (cons error-erp '("Flag to return in case of error.")) (cons (cons error-val '("Value to return in case of error.")) '((ctx "Context for errors.") state))))) (cons ':returns (cons (cons 'mv (cons (case mode (:logic (cons erp (cons (cons 'implies (cons erp (cons (cons 'equal (cons erp (cons error-erp 'nil))) 'nil))) 'nil))) (:program (cons erp '("@('nil') or @('error-erp')."))) (t (impossible))) (cons (if returns-supplied-p returns (case mode (:logic (cons val (cons (cons 'and (cons (cons 'implies (cons erp (cons (cons 'equal (cons val (cons error-val 'nil))) 'nil))) (cons (cons 'implies (cons (cons 'and (cons (cons 'not (cons erp 'nil)) (cons error-erp 'nil))) (cons (cons 'not (cons val 'nil)) 'nil))) 'nil))) 'nil))) (:program (cons val '("@('nil') if @('erp') is @('nil'), otherwise @('error-val')."))) (t (impossible)))) '(state)))) (cons ':mode (cons mode (append (and verify-guards-supplied-p (list :verify-guards verify-guards)) (append (and parents-supplied-p (list :parents parents)) (append (and short-supplied-p (list :short short)) (append (and long-supplied-p (list :long long)) (cons (cons 'b* (cons (def-error-checker-bindings conditions-messages error-erp error-val) (cons (cons 'value (cons result 'nil)) 'nil))) '(:no-function t)))))))))))))) (x-symbols (def-error-checker-x-symbols xs)) (macro (cons 'defmacro (cons macro-name (cons (append x-symbols (cons description (cons error-erp (cons error-val 'nil)))) (cons (cons 'list (cons (cons 'quote (cons function-name 'nil)) (append x-symbols (cons description (cons error-erp (cons error-val '('ctx 'state))))))) 'nil))))) (section-short (concatenate 'string "Calls @(tsee " (string-downcase (symbol-name function-name)) ") with @('ctx') and @('state')" " as the last two arguments.")) (section-long (concatenate 'string "@(def " (string-downcase (symbol-name macro-name)) ")")) (section (cons 'defsection (cons macro-name (cons ':parents (cons (cons function-name 'nil) (cons ':short (cons section-short (cons ':long (cons section-long (cons macro 'nil))))))))))) (cons 'progn (cons function (cons section 'nil))))))
Theorem:
(defthm pseudo-event-formp-of-def-error-checker-fn (b* ((function+macro (def-error-checker-fn name xs returns returns-supplied-p conditions-messages result mode verify-guards verify-guards-supplied-p parents parents-supplied-p short short-supplied-p long long-supplied-p def-error-checker-call state))) (pseudo-event-formp function+macro)) :rule-classes :rewrite)