		Search-engine friendly clone of the ACL2 documentation.

Defun-inst-implementation

Defun-inst-choice-events

Generate a list of events to submit, when instantiating a choice second-order function.

Signature
(defun-inst-choice-events fun sofun inst options ctx state) → (mv erp events+result+funvars state)
Arguments: fun — Guard (symbolp fun).; sofun — Guard (choice-sofunp sofun (w state)).; options — Guard (keyword-value-listp options).; ctx — Context for errors.
Returns: erp — booleanp flag of the error triple.; events+result+funvars — A tuple (events result funvars) where events is a pseudo-event-form-listp, result is a maybe-pseudo-event-formp, and funvars is a funvar-listp.

Also return the defchoose2 or defchoose event form. This is printed when :print is :result.

Also return the function variables that the new function depends on.

Only the :print option may be present.

We add fun to the table of second-order functions iff it is second-order.

Definitions and Theorems

Function: defun-inst-choice-events

(defun defun-inst-choice-events (fun sofun inst options ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp fun)
                             (keyword-value-listp options)
                             (choice-sofunp sofun (w state)))))
 (let ((__function__ 'defun-inst-choice-events))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    ((unless (subsetp (evens options) '(:print)))
     (er-soft+
      ctx t nil
      "Only the input keyword :PRINT is allowed, ~
                   because ~x0 is a choice second-order function."
      sofun))
    (bound-vars (defchoose-bound-vars sofun wrld))
    (sofun-body (defchoose-body sofun wrld))
    (fun-body (fun-subst-term inst sofun-body wrld))
    (funvars (funvars-of-term fun-body wrld))
    (fun-body (untranslate fun-body nil wrld))
    (formals (formals sofun wrld))
    (strengthen (defchoose-strengthen sofun wrld))
    (funvars (remove-duplicates funvars))
    (defchoose-event
     (cons
         'defchoose
         (cons fun
               (cons bound-vars
                     (cons formals
                           (cons fun-body
                                 (cons ':strengthen
                                       (cons strengthen 'nil))))))))
    (result
     (cons
         (if funvars 'defchoose2 'defchoose)
         (cons fun
               (cons bound-vars
                     (cons formals
                           (cons fun-body
                                 (cons ':strengthen
                                       (cons strengthen 'nil))))))))
    (table-event?
     (if funvars
      (cons
           (cons 'table
                 (cons 'second-order-functions
                       (cons (cons 'quote (cons fun 'nil))
                             (cons (cons 'quote (cons funvars 'nil))
                                   'nil))))
           'nil)
      nil)))
   (value (list (cons defchoose-event table-event?)
                result funvars)))))