Extend function substitutions for functional instantiation.
An instance
For example,
if
The following code extends a function substitution (initially an instantiation) to contain all those extra pairs. The starting point is a term; the bodies of second-order functions referenced in the term are recursively processed. The table of instances of second-order functions is searched, similarly to fun-subst-function.
Function:
(defun ext-fun-subst-term (term fsbs wrld) (declare (xargs :guard (and (pseudo-termp term) (fun-substp fsbs) (plist-worldp wrld)))) (let ((__function__ 'ext-fun-subst-term)) (declare (ignorable __function__)) (if (or (variablep term) (quotep term)) fsbs (let* ((fn (fn-symb term)) (fsbs (if (symbolp fn) (ext-fun-subst-function fn fsbs wrld) (ext-fun-subst-term (lambda-body fn) fsbs wrld)))) (ext-fun-subst-terms (fargs term) fsbs wrld)))))
Function:
(defun ext-fun-subst-terms (terms fsbs wrld) (declare (xargs :guard (and (pseudo-term-listp terms) (fun-substp fsbs) (plist-worldp wrld)))) (let ((__function__ 'ext-fun-subst-terms)) (declare (ignorable __function__)) (if (endp terms) fsbs (let ((fsbs (ext-fun-subst-term (car terms) fsbs wrld))) (ext-fun-subst-terms (cdr terms) fsbs wrld)))))
Function:
(defun ext-fun-subst-function (fun fsbs wrld) (declare (xargs :guard (and (symbolp fun) (fun-substp fsbs) (plist-worldp wrld)))) (let ((__function__ 'ext-fun-subst-function)) (declare (ignorable __function__)) (cond ((assoc fun fsbs) fsbs) ((sofunp fun wrld) (b* ((funvars (sofun-funvars fun wrld)) (subfsbs (restrict-alist funvars fsbs)) ((if (null subfsbs)) fsbs) (instmap (sof-instances fun wrld)) (funinst (get-sof-instance subfsbs instmap wrld)) ((unless funinst) (raise "~x0 has no instance for ~x1." fun fsbs)) (fsbs (acons fun funinst fsbs))) (case (sofun-kind fun wrld) ((plain quant) (ext-fun-subst-term (ubody fun wrld) fsbs wrld)) (choice (ext-fun-subst-term (defchoose-body fun wrld) fsbs wrld))))) (t fsbs))))
Function:
(defun ext-fun-subst-term (term fsbs wrld) (declare (xargs :guard (and (pseudo-termp term) (fun-substp fsbs) (plist-worldp wrld)))) (let ((__function__ 'ext-fun-subst-term)) (declare (ignorable __function__)) (if (or (variablep term) (quotep term)) fsbs (let* ((fn (fn-symb term)) (fsbs (if (symbolp fn) (ext-fun-subst-function fn fsbs wrld) (ext-fun-subst-term (lambda-body fn) fsbs wrld)))) (ext-fun-subst-terms (fargs term) fsbs wrld)))))
Function:
(defun ext-fun-subst-terms (terms fsbs wrld) (declare (xargs :guard (and (pseudo-term-listp terms) (fun-substp fsbs) (plist-worldp wrld)))) (let ((__function__ 'ext-fun-subst-terms)) (declare (ignorable __function__)) (if (endp terms) fsbs (let ((fsbs (ext-fun-subst-term (car terms) fsbs wrld))) (ext-fun-subst-terms (cdr terms) fsbs wrld)))))
Function:
(defun ext-fun-subst-function (fun fsbs wrld) (declare (xargs :guard (and (symbolp fun) (fun-substp fsbs) (plist-worldp wrld)))) (let ((__function__ 'ext-fun-subst-function)) (declare (ignorable __function__)) (cond ((assoc fun fsbs) fsbs) ((sofunp fun wrld) (b* ((funvars (sofun-funvars fun wrld)) (subfsbs (restrict-alist funvars fsbs)) ((if (null subfsbs)) fsbs) (instmap (sof-instances fun wrld)) (funinst (get-sof-instance subfsbs instmap wrld)) ((unless funinst) (raise "~x0 has no instance for ~x1." fun fsbs)) (fsbs (acons fun funinst fsbs))) (case (sofun-kind fun wrld) ((plain quant) (ext-fun-subst-term (ubody fun wrld) fsbs wrld)) (choice (ext-fun-subst-term (defchoose-body fun wrld) fsbs wrld))))) (t fsbs))))