		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-transformations

Fsublis-fn-rec

Variant of sublis-fn-rec that performs no simplification.

Signature
(fsublis-fn-rec alist term bound-vars allow-freevars-p) → (mv vars new-term)
Arguments: alist — Guard (symbol-alistp alist).; term — Guard (pseudo-termp term).; bound-vars — Guard (symbol-listp bound-vars).; allow-freevars-p — Guard (booleanp allow-freevars-p).
Returns: vars — A symbol-listp.; new-term — A pseudo-termp.

sublis-fn-rec is in the ACL2 source code.

The meaning of the starting f in the name of this utility is analogous to fcons-term compared to cons-term.

The definition of this utility is identical to sublis-fn-rec, except that cons-term and sublis-var are replaced by fcons-term and fsublis-var. We also use endp instead of null in the exit test of fsublis-fn-rec-lst so that termination can be proved and the function is in logic mode.

Function: fsublis-fn-rec

(defun fsublis-fn-rec (alist term bound-vars allow-freevars-p)
 (declare (xargs :guard (and (symbol-alistp alist)
                             (pseudo-termp term)
                             (symbol-listp bound-vars)
                             (booleanp allow-freevars-p))))
 (let ((__function__ 'fsublis-fn-rec))
  (declare (ignorable __function__))
  (cond
   ((variablep term) (mv nil term))
   ((fquotep term) (mv nil term))
   ((flambda-applicationp term)
    (let ((old-lambda-formals (lambda-formals (ffn-symb term))))
     (mv-let (erp new-lambda-body)
             (fsublis-fn-rec alist (lambda-body (ffn-symb term))
                             (append old-lambda-formals bound-vars)
                             allow-freevars-p)
      (cond
       (erp (mv erp new-lambda-body))
       (t
        (mv-let (erp args)
                (fsublis-fn-rec-lst alist (fargs term)
                                    bound-vars allow-freevars-p)
         (cond
          (erp (mv erp args))
          (t
           (let*
            ((body-vars (all-vars new-lambda-body))
             (extra-body-vars
                  (set-difference-eq body-vars old-lambda-formals)))
            (mv
               nil
               (fcons-term
                    (make-lambda
                         (append old-lambda-formals extra-body-vars)
                         new-lambda-body)
                    (append args extra-body-vars))))))))))))
   (t
    (let ((temp (assoc-eq (ffn-symb term) alist)))
     (cond
      (temp
       (cond
        ((symbolp (cdr temp))
         (mv-let (erp args)
                 (fsublis-fn-rec-lst alist (fargs term)
                                     bound-vars allow-freevars-p)
           (cond (erp (mv erp args))
                 (t (mv nil (fcons-term (cdr temp) args))))))
        (t
         (let
          ((bad
            (if allow-freevars-p
             (intersection-eq
              (set-difference-eq (all-vars (lambda-body (cdr temp)))
                                 (lambda-formals (cdr temp)))
              bound-vars)
             (set-difference-eq (all-vars (lambda-body (cdr temp)))
                                (lambda-formals (cdr temp))))))
          (cond
           (bad (mv bad term))
           (t
            (mv-let (erp args)
                    (fsublis-fn-rec-lst alist (fargs term)
                                        bound-vars allow-freevars-p)
             (cond
              (erp (mv erp args))
              (t
               (mv
                  nil
                  (fsublis-var (pairlis$ (lambda-formals (cdr temp))
                                         args)
                               (lambda-body (cdr temp)))))))))))))
      (t (mv-let (erp args)
                 (fsublis-fn-rec-lst alist (fargs term)
                                     bound-vars allow-freevars-p)
           (cond (erp (mv erp args))
                 (t (mv nil
                        (fcons-term (ffn-symb term)
                                    args))))))))))))

Function: fsublis-fn-rec-lst

(defun fsublis-fn-rec-lst (alist terms bound-vars allow-freevars-p)
 (declare (xargs :guard (and (symbol-alistp alist)
                             (pseudo-term-listp terms)
                             (symbol-listp bound-vars)
                             (booleanp allow-freevars-p))))
 (let ((__function__ 'fsublis-fn-rec-lst))
  (declare (ignorable __function__))
  (cond
   ((endp terms) (mv nil nil))
   (t
    (mv-let (erp term)
            (fsublis-fn-rec alist (car terms)
                            bound-vars allow-freevars-p)
     (cond
         (erp (mv erp term))
         (t (mv-let (erp tail)
                    (fsublis-fn-rec-lst alist (cdr terms)
                                        bound-vars allow-freevars-p)
              (cond (erp (mv erp tail))
                    (t (mv nil (cons term tail))))))))))))

Subtopics

Fsublis-fn-rec-lst