		Search-engine friendly clone of the ACL2 documentation.

Find-base-cases

Find-a-base-case-aux

Find a base-case within an untranslated term.

Signature
(find-a-base-case-aux term fns prefer-then wrld state) → (mv erp all-base largest)
Arguments: fns — Guard (symbol-listp fns).; prefer-then — Guard (booleanp prefer-then).; wrld — Guard (plist-worldp wrld).
Returns: erp — nil when a base-case is found.; all-base — A booleanp. t when term is a base-case.; largest — Apseudo-termp. If (or erp all-base), then this is nil. Otherwise, it is the largest (proper) subterm which is a base-case.

If none of fns appear in term, term is a base-case of itself. If term macro-expands to an if call, then all base-cases of the ``then'' and ``else'' branches are base-cases of term.

A term may have many base-cases. We bias our search toward larger base-cases, and toward ``then'' branches if prefer-then, and ``else'' branches otherwise.

If term is a base-case, we return it. If either of its branches are base-cases, we return one of those, with the aforementioned biases. Otherwise, we pick the largest base-case in the biased branch.

Definitions and Theorems

Function: find-a-base-case-aux

(defun find-a-base-case-aux (term fns prefer-then wrld state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbol-listp fns)
                             (booleanp prefer-then)
                             (plist-worldp wrld))))
 (let ((__function__ 'find-a-base-case-aux))
  (declare (ignorable __function__))
  (b* (((unless (consp term)) (mv nil t nil))
       ((mv erp term)
        (acl2::magic-macroexpand term 'find-a-base-case
                                 wrld state))
       ((when erp) (mv erp nil nil))
       ((unless (consp term)) (mv nil t nil))
       ((unless (eq 'if (ffn-symb term)))
        (if (untranslated-expr-calls-some-fn fns term wrld)
            (mv t nil nil)
          (mv nil t nil)))
       ((mv erp-then all-base-then largest-then)
        (find-a-base-case-aux (farg2 term)
                              fns prefer-then wrld state))
       ((mv erp-else all-base-else largest-else)
        (find-a-base-case-aux (farg3 term)
                              fns prefer-then wrld state)))
   (cond
    (erp-then (if erp-else (mv erp-else nil nil)
                (mv nil nil
                    (if all-base-else (farg3 term)
                      largest-else))))
    (erp-else (mv nil nil
                  (if all-base-then (farg2 term)
                    largest-then)))
    (all-base-then
      (if all-base-else
          (if (not (untranslated-expr-calls-some-fn fns (farg1 term)
                                                    wrld))
              (mv nil t nil)
            (mv nil nil
                (if prefer-then (farg2 term)
                  (farg3 term))))
        (mv nil nil (farg2 term))))
    (all-base-else (mv nil nil (farg3 term)))
    (prefer-then (mv nil nil largest-then))
    (t (mv nil nil largest-else))))))