		Search-engine friendly clone of the ACL2 documentation.

Defsoft-implementation

Defsoft-fn

Generate the event submitted by defsoft.

Signature
(defsoft-fn fn ctx state) → (mv erp event state)

The defsoft macro records an ACL2 function as a (SOFT) second-order function. This macro will become the primary one to introduce second-order functions, and defun2, defchoose2, and defun-sk2 will be redefined as defun, defchoose, and defun-sk followed by defsoft.

The input fn must be a symbol that denotes an existing function that is introduced by defchoose, or otherwise is introduced by defun-sk, or otherwise has an unnormalized body (which implies that is is introduced by defun). Note that defun-sk functions are internally introduced by defun, so it is important to check for defun-sk first. Functions introduced by defun but without an unnormalized body (such as the built-in program-mode functions) are disallowed because we cannot calculate the function variables that such functions depend on. For the same reason, constrained functions introduced by encapsulate are disallowed.

We collect the function variables that the function depends on, directly or indirecty; there must be at least one. If the function is introduced by defun-sk, we also ensure that the associated rewrite rule does not depend on additional function variables. If the function is recursive, we also ensure that the well-founded relation is o<.

We print on screen an observation about the function being recorded and which function variables it depends on. This can be suppressed (e.g. when generating defsoft events programmatically) via (with-output :off observation ...).

Definitions and Theorems

Function: defsoft-fn

(defun defsoft-fn (fn ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard t))
 (let ((__function__ 'defsoft-fn))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    ((unless (symbolp fn))
     (er-soft+ ctx t nil
               "The input must be a symbol, but it is ~x0 instead."
               fn))
    ((unless (function-symbolp fn wrld))
     (er-soft+
      ctx t nil
      "The symbol ~x0 must be a function symbol, ~
                   but it is not."
      fn))
    ((unless (or (defchoosep fn wrld)
                 (defun-sk-p fn wrld)
                 (ubody fn wrld)))
     (er-soft+
      ctx t nil
      "The function ~x0 must ~
                   be introduced by DEFCHOOSE, ~
                   be introduced by DEFUN-SK, ~
                   or have a non-NIL unnormalized body."
      fn))
    (funvars (cond ((defchoosep fn wrld)
                    (funvars-of-choice-fn fn wrld))
                   ((defun-sk-p fn wrld)
                    (funvars-of-quantifier-fn fn wrld))
                   (t (funvars-of-plain-fn fn wrld))))
    (funvars (remove-duplicates-eq funvars))
    ((unless (consp funvars))
     (er-soft+
      ctx t nil
      "The function ~x0 is not second-order:
                   it depends on no function variables, directly or indirectly."
      fn))
    (table-event
         (cons 'table
               (cons 'second-order-functions
                     (cons (cons 'quote (cons fn 'nil))
                           (cons (cons 'quote (cons funvars 'nil))
                                 'nil)))))
    ((er &) (ensure-wfrel-o< fn ctx state))
    ((er &)
     (ensure-defun-sk-rule-same-funvars fn ctx state))
    (state
     (acl2::io?
      observation nil state (fn funvars)
      (fms
       "SOFT: ~
                               recorded ~x0 as a second-order function ~
                               that depends on the function variables ~x1.~%"
       (list (cons #\0 fn)
             (cons #\1 (acl2::sort-symbol-listp funvars)))
       *standard-co* state nil))))
   (value (cons 'progn
                (cons table-event
                      (cons (cons 'value-triple
                                  (cons (cons 'quote (cons fn 'nil))
                                        'nil))
                            'nil)))))))