		Search-engine friendly clone of the ACL2 documentation.

Soft-implementation-core

Fun-subst-function

Apply a function substitution to an individual function.

Signature
(fun-subst-function fsbs fun wrld) → new-fun
Arguments: fsbs — Guard (fun-substp fsbs).; fun — Guard (symbolp fun).; wrld — Guard (plist-worldp wrld).
Returns: new-fun — A symbolp.

Applying an instantiation to a term involves replacing not only the function variables that are keys of the instantiation and that occur explicitly in the term, but also the ones that occur implicitly in the term via occurrences of second-order functions that depend on those function variables. For example, if ff is a second-order function with function parameter f, and an instantiation I replaces f with g, applying I to the term (cons (f x) (ff y)) should yield the term (cons (g x) (gg y)), where gg is the instance that results form applying I to ff. The sof-instances table is used to find gg: I is restricted to the function parameters of ff before searching the map of instances of ff; if the restriction is empty, gg is ff, i.e. no replacement takes place. If gg does not exist, the application of I to (cons (f x) (ff y)) fails; the user must create gg and try applying I to (cons (f x) (ff y)) again.

When an instantiation is applied to the body of a recursive second-order function sofun to obtain an instance fun, occurrences of sofun in the body must be replaced with fun, but at that time fun does not exist yet, and thus the table of second-order function instances of sofun has no entries for fun yet. Thus, it is convenient to use function substitutions (not just instantiations) to instantiate terms.

The following code applies a function substitution to an individual function, in the manner explained above. It is used by fun-subst-term, which applies a function substitution to a term. If a needed second-order function instance does not exist, an error occurs.

Definitions and Theorems

Function: fun-subst-function

(defun fun-subst-function (fsbs fun wrld)
 (declare (xargs :guard (and (fun-substp fsbs)
                             (symbolp fun)
                             (plist-worldp wrld))))
 (let ((__function__ 'fun-subst-function))
  (declare (ignorable __function__))
  (let ((pair (assoc-eq fun fsbs)))
   (if pair (cdr pair)
     (if
       (sofunp fun wrld)
       (let* ((funvars (sofun-funvars fun wrld))
              (subfsbs (restrict-alist funvars fsbs)))
         (if (null subfsbs)
             fun
           (let* ((instmap (sof-instances fun wrld))
                  (new-fun (get-sof-instance subfsbs instmap wrld)))
             (if new-fun new-fun
               (raise "~x0 has no instance for ~x1."
                      fun fsbs)))))
       fun)))))