		Search-engine friendly clone of the ACL2 documentation.

Defun-inst-implementation

Defun-inst-quant-events

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

Signature
(defun-inst-quant-events fun sofun inst options ctx state) → (mv erp events+result+funvars state)
Arguments: fun — Guard (symbolp fun).; sofun — Guard (quant-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 defun-sk2 or defun-sk event form. This is printed when :print is :result.

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

Only the :verify-guards, :enable, :skolem-name, :thm-name, :rewrite, :constrain, and :print options may be present.

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

Definitions and Theorems

Function: defun-inst-quant-events

(defun defun-inst-quant-events (fun sofun inst options ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp fun)
                             (keyword-value-listp options)
                             (quant-sofunp sofun (w state)))))
 (let ((__function__ 'defun-inst-quant-events))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    ((unless (subsetp (evens options)
                      '(:verify-guards :enable :skolem-name
                                       :thm-name :rewrite
                                       :constrain :print)))
     (er-soft+
      ctx t nil
      "Only the input keywords ~
                   :VERIFY-GUARDS, ~
                   :ENABLE, ~
                   :SKOLEM-NAME, ~
                   :THM-NAME,  ~
                   :REWRITE, ~
                   :CONSTRAIN and ~
                   :PRINT ~
                   are allowed, ~
                   because ~x0 is a quantifier second-order function."
      sofun))
    (enable (let ((enable-option (assoc-keyword :enable options)))
              (if enable-option (cadr enable-option)
                (fundef-enabledp sofun state))))
    (verify-guards
         (let ((verify-guards-option
                    (assoc-keyword :verify-guards options)))
           (if verify-guards-option (cadr verify-guards-option)
             (guard-verified-p sofun wrld))))
    (bound-vars (defun-sk-bound-vars sofun wrld))
    (quant (defun-sk-quantifier sofun wrld))
    (sofun-matrix (defun-sk-matrix sofun wrld))
    (fun-matrix (fun-subst-term inst sofun-matrix wrld))
    (fun-matrix-funvars (funvars-of-term fun-matrix wrld))
    (fun-matrix (untranslate fun-matrix nil wrld))
    (rewrite-option (assoc-keyword :rewrite options))
    (rewrite
     (if rewrite-option (cadr rewrite-option)
      (let ((qrkind (defun-sk-rewrite-kind sofun wrld)))
        (case qrkind
          (:default :default)
          (:direct :direct)
          (:custom
               (let* ((fsbs (acons sofun fun inst))
                      (rule-name (defun-sk-rewrite-name sofun wrld))
                      (term (formula rule-name nil wrld)))
                 (fun-subst-term fsbs term wrld)))))))
    (skolem-name
      (let
         ((skolem-name-option (assoc-keyword :skolem-name options)))
        (if skolem-name-option
            (cons ':skolem-name
                  (cons (cadr skolem-name-option) 'nil))
          nil)))
    (thm-name
     (let ((thm-name-option (assoc-keyword :thm-name options)))
       (if thm-name-option (cons ':thm-name
                                 (cons (cadr thm-name-option) 'nil))
         nil)))
    (constrain
        (let ((constrain-option (assoc-keyword :constrain options)))
          (if constrain-option
              (cons ':constrain
                    (cons (cadr constrain-option) 'nil))
            nil)))
    (sofun-guard (uguard sofun wrld))
    (fun-guard (fun-subst-term inst sofun-guard wrld))
    (fun-guard-funvars (funvars-of-term fun-guard wrld))
    (fun-guard (untranslate fun-guard t wrld))
    (formals (formals sofun wrld))
    (strengthen (defun-sk-strengthen sofun wrld))
    (body (list quant bound-vars fun-matrix))
    (rest
     (cons
      ':strengthen
      (cons
       strengthen
       (cons
            ':quant-ok
            (cons 't
                  (append (and (eq quant 'forall)
                               (list :rewrite rewrite))
                          (append skolem-name
                                  (append thm-name constrain))))))))
    (funvars (remove-duplicates
                  (append fun-matrix-funvars fun-guard-funvars)))
    (defun-sk-event
     (cons
      'defun-sk
      (cons
       fun
       (cons
        formals
        (cons
         (cons
          'declare
          (cons
               (cons 'xargs
                     (cons ':guard
                           (cons fun-guard
                                 (cons ':verify-guards
                                       (cons verify-guards 'nil)))))
               'nil))
         (cons body rest))))))
    (result (cons (if funvars 'defun-sk2 'defun-sk)
                  (cons fun (cons formals (cons body rest)))))
    (disable-event?
     (if enable nil
      (let ((fn/defrule (cond ((eq constrain nil) fun)
                              ((eq constrain t)
                               (add-suffix fun "-DEFINITION"))
                              (t constrain)))
            (rwrule (if thm-name (cadr thm-name)
                      (if (eq quant 'forall)
                          (add-suffix fun "-NECC")
                        (add-suffix fun "-SUFF")))))
       (cons (cons 'in-theory
                   (cons (cons 'disable
                               (cons fn/defrule (cons rwrule 'nil)))
                         'nil))
             '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))
    (check-event
     (cons
      'make-event-terse
      (cons
       (cons
        'b*
        (cons
         (cons
             (cons 'err-msg?
                   (cons (cons 'check-qrewrite-rule-funvars
                               (cons (cons 'quote (cons sofun 'nil))
                                     '((w state))))
                         'nil))
             'nil)
         (cons
          (cons
           'if
           (cons
            'err-msg?
            (cons
             (cons
               'er-soft+
               (cons (cons 'cons
                           (cons ''defun-inst
                                 (cons (cons 'quote (cons fun 'nil))
                                       'nil)))
                     '(t nil "~@0" err-msg?)))
             '((value '(value-triple :invisible))))))
          'nil)))
       'nil))))
   (value
    (list
       (cons defun-sk-event
             (append disable-event?
                     (append table-event? (cons check-event 'nil))))
       result funvars)))))