Find a base-case within an untranslated term.
(find-a-base-case-aux term fns prefer-then wrld state) → (mv erp all-base largest)
If none of
A term may have many base-cases. We bias our search toward larger
base-cases, and toward ``then'' branches if
If
Function:
(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))))))