		Search-engine friendly clone of the ACL2 documentation.

Defun-inst-implementation

Defun-inst-fn

Validate some of the inputs to defun-inst and generate the event form to submit.

Signature
(defun-inst-fn fun sofun-inst options ctx state) → (mv erp event state)
Arguments: ctx — Context for errors.
Returns: erp — booleanp flag of the error triple.; event — A maybe-pseudo-event-formp.

We directly check the name and instance designation, we directly check the correct presence of keyed options (we do that in defun-inst-plain-events, defun-inst-choice-events, and defun-inst-quant-events), and we directly check the correct value of the :print option (if present), but rely on defun, defchoose, and defun-sk to check the values of the other keyed options.

Prior to introducing fun, we generate local events to avoid errors due to ignored or irrelevant formals in fun (which may happen if sofun has ignored or irrelevant formals). We add fun to the table of instances of second-order functions.

Definitions and Theorems

Function: defun-inst-fn

(defun defun-inst-fn (fun sofun-inst options ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let ((__function__ 'defun-inst-fn))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    ((unless (symbolp fun))
     (er-soft+ ctx t nil
               "The first input must be a name, but ~x0 is not."
               fun))
    ((unless (check-sofun-inst sofun-inst wrld))
     (er-soft+
      ctx t nil
      "The second input must be ~
                   the name of a second-order function ~
                   followed by the pairs of an instantiation, ~
                   but ~x0 is not."
      sofun-inst))
    (sofun (car sofun-inst))
    (inst (cdr sofun-inst))
    ((unless (subsetp (alist-keys inst)
                      (sofun-funvars sofun wrld)))
     (er-soft+
      ctx t nil
      "Each function variable key of ~x0 must be ~
                   among the function variables ~x1 ~
                   that ~x2 depends on."
      inst (sofun-funvars sofun wrld)
      sofun))
    ((unless (keyword-value-listp options))
     (er-soft+
      ctx t nil
      "The inputs after the second input ~
                   must be a keyword-value list, ~
                   but ~x0 is not."
      options))
    (keywords (evens options))
    ((unless (no-duplicatesp keywords))
     (er-soft+ ctx t nil
               "The input keywords must be unique."))
    (print-pair (assoc-keyword :print options))
    (print (if print-pair (cadr print-pair)
             :result))
    ((unless (member-eq print '(nil :all :result)))
     (er-soft+
      ctx t nil
      "The :PRINT input must be NIL, :ALL, or :RESULT, ~
                   but ~x0 is not."
      print))
    ((er (list fun-intro-events result funvars))
     (case (sofun-kind sofun wrld)
      (plain
         (defun-inst-plain-events fun sofun inst options ctx state))
      (choice
        (defun-inst-choice-events fun sofun inst options ctx state))
      (quant
         (defun-inst-quant-events fun sofun inst options ctx state))
      (t (prog2$ (impossible)
                 (value (list nil nil))))))
    (instmap (sof-instances sofun wrld))
    (new-instmap (put-sof-instance inst fun instmap wrld))
    (encapsulate
     (cons
      'encapsulate
      (cons
       'nil
       (cons
        '(set-ignore-ok t)
        (cons
         '(set-irrelevant-formals-ok t)
         (append
          fun-intro-events
          (cons
           (cons
             'table
             (cons 'sof-instances
                   (cons (cons 'quote (cons sofun 'nil))
                         (cons (cons 'quote (cons new-instmap 'nil))
                               'nil))))
           'nil))))))
)
    (result-event (cons 'cw-event
                        (cons '"~x0~|"
                              (cons (cons 'quote (cons result 'nil))
                                    'nil))))
    (print-funvar-event
     (if funvars
      (cons
       'cw-event
       (cons
        '"The function ~x0 depends on the function variables ~x1.~%"
        (cons (cons 'quote (cons fun 'nil))
              (cons (cons 'quote (cons funvars 'nil))
                    'nil))))
      (cons
       'cw-event
       (cons '"The function ~x0 depends on no function variables.~%"
             (cons (cons 'quote (cons fun 'nil))
                   'nil)))))
    (return-value-event (cons 'value-triple
                              (cons (cons 'quote (cons fun 'nil))
                                    'nil)))
    (event
     (cond
        ((eq print nil)
         (cons 'progn
               (cons encapsulate
                     (cons print-funvar-event
                           (cons return-value-event 'nil)))))
        ((eq print :all)
         (restore-output
              (cons 'progn
                    (cons encapsulate
                          (cons print-funvar-event
                                (cons return-value-event 'nil))))))
        ((eq print :result)
         (cons 'progn
               (cons encapsulate
                     (cons result-event
                           (cons print-funvar-event
                                 (cons return-value-event 'nil))))))
        (t (impossible)))))
   (value event))))