other
(in-package "ACL2")
query-badge-userfn-structurefunction
(defun query-badge-userfn-structure (fn wrld) (cond ((not (symbolp fn)) (mv (msg "~x0 is not a symbol" fn) nil nil)) ((not (function-symbolp fn wrld)) (mv (msg "~x0 is not a known function symbol" fn) nil nil)) (t (mv-let (badge warrantp) (get-badge-and-warrantp fn wrld) (let ((needs-warrant (and (not warrantp) (or (null *aokp*) (logicp fn wrld))))) (cond ((null badge) (mv (msg "~x0 has not been ~s1" fn (if needs-warrant "warranted" "badged")) nil nil)) (needs-warrant (mv (msg "~x0 has not been warranted, and its badge is insufficient ~ because it is in :logic mode" fn) badge warrantp)) (t (mv nil badge warrantp))))))))
other
(progn (push 'doppelganger-badge-userfn *defun-overrides*) (defun doppelganger-badge-userfn (fn) (cond ((and (null *aokp*) (null *warrant-reqs*)) (throw-raw-ev-fncall (list* 'ev-fncall-null-body-er nil 'doppelganger-badge-userfn (replace-live-stobjs-in-list (list fn))))) (t (mv-let (bad-fn-msg badge warrantp) (query-badge-userfn-structure fn (w *the-live-state*)) (cond ((null bad-fn-msg) (or (not warrantp) (maybe-extend-warrant-reqs fn nil 'badge-userfn)) badge) (t (throw-raw-ev-fncall (list* 'ev-fncall-null-body-er nil (msg "The value of ~x0 is not specified on ~x1 because ~ ~@2.~@3" 'badge-userfn fn (cond (bad-fn-msg bad-fn-msg) (t (msg "~x0 has not been warranted" fn))) (if *inside-do$* (msg " This error has occurred in the scope of ~ a call of ~x0, which generally comes from ~ an expression of the form (loop$ with ~ ...). See :DOC loop$ and :DOC apply$." 'do$) "")) (replace-live-stobjs-in-list (list fn)))))))))) (defun-*1* doppelganger-badge-userfn (fn) (doppelganger-badge-userfn fn)))
concrete-check-apply$-hyp-tamep-hypfunction
(defun concrete-check-apply$-hyp-tamep-hyp (ilks args wrld) (declare (ftype (function (t t) (values t)) executable-tamep executable-tamep-functionp)) (cond ((endp ilks) t) ((eq (car ilks) :fn) (and (executable-tamep-functionp (car args) wrld) (concrete-check-apply$-hyp-tamep-hyp (cdr ilks) (cdr args) wrld))) ((eq (car ilks) :expr) (and (executable-tamep (car args) wrld) (concrete-check-apply$-hyp-tamep-hyp (cdr ilks) (cdr args) wrld))) (t (concrete-check-apply$-hyp-tamep-hyp (cdr ilks) (cdr args) wrld))))
maybe-extend-warrant-reqsfunction
(defun maybe-extend-warrant-reqs (fn args caller) (let ((warrant-reqs *warrant-reqs*)) (cond ((null warrant-reqs) nil) ((eq t warrant-reqs) (setq *warrant-reqs* (list fn))) ((eq :nil! warrant-reqs) (setq *warrant-reqs* fn) (throw-raw-ev-fncall (list* 'ev-fncall-null-body-er nil (msg "The value of ~x0 is not specified on ~x1 because the ~ use of warrants is not permitted in this context." caller fn) (replace-live-stobjs-in-list (list fn args))))) ((symbolp warrant-reqs) (er hard! 'maybe-extend-warrant-reqs "Implementation error: *warrant-reqs* has an input value of ~ ~x0." warrant-reqs)) ((member fn warrant-reqs :test (function eq)) nil) (t (push fn *warrant-reqs*)))))
other
(progn (push 'doppelganger-apply$-userfn *defun-overrides*) (defun raw-apply-for-badged-fn (fn arity args) (cond ((and (eq (symbol-class fn (w *the-live-state*)) :program) (not (f-get-global 'safe-mode *the-live-state*))) (state-free-global-let* ((safe-mode t)) (apply (*1*-symbol fn) (if (= arity (length args)) args (take arity args))))) (t (apply (*1*-symbol fn) (if (= arity (length args)) args (take arity args)))))) (defun doppelganger-apply$-userfn (fn args) (cond ((and (null *aokp*) (null *warrant-reqs*)) (throw-raw-ev-fncall (list* 'ev-fncall-null-body-er nil 'doppelganger-apply$-userfn (replace-live-stobjs-in-list (list fn args))))) (t (mv-let (bad-fn-msg badge warrantp) (query-badge-userfn-structure fn (w *the-live-state*)) (cond (bad-fn-msg (throw-raw-ev-fncall (list* 'ev-fncall-null-body-er nil (msg "The value of ~x0 is not specified on ~x1 because ~@2." 'apply$-userfn fn (cond (bad-fn-msg bad-fn-msg) (t (msg "~x0 has not been warranted" fn)))) (replace-live-stobjs-in-list (list fn args))))) ((eq (access apply$-badge badge :ilks) t) (or (not warrantp) (maybe-extend-warrant-reqs fn args 'apply$-userfn)) (if (int= (access apply$-badge badge :out-arity) 1) (raw-apply-for-badged-fn fn (access apply$-badge badge :arity) args) (multiple-value-list (raw-apply-for-badged-fn fn (access apply$-badge badge :arity) args)))) ((concrete-check-apply$-hyp-tamep-hyp (access apply$-badge badge :ilks) args (w *the-live-state*)) (or (not warrantp) (maybe-extend-warrant-reqs fn args 'apply$-userfn)) (if (int= (access apply$-badge badge :out-arity) 1) (raw-apply-for-badged-fn fn (access apply$-badge badge :arity) args) (multiple-value-list (raw-apply-for-badged-fn fn (access apply$-badge badge :arity) args)))) (t (throw-raw-ev-fncall (list* 'ev-fncall-null-body-er nil (msg "The value of ~x0 is not specified when the first ~ argument, fn, is ~x1, and the second argument, args, ~ is ~x2. Fn has badge ~x3 and args is not known to ~ satisfy the tameness requirement of that badge." 'apply$-userfn fn args badge) (replace-live-stobjs-in-list (list fn args)))))))))) (defun-*1* doppelganger-apply$-userfn (fn args) (doppelganger-apply$-userfn fn args)))
access-cl-cachemacro
(defmacro access-cl-cache (c field) (case field (:alist `(car ,C)) (:size `(cadr ,C)) (:last `(cddr ,C)) (otherwise (er hard 'access-cl-cache "Illegal field name, ~x0." field))))
other
(defrec cl-cache-line (((lambda-object . status) absolute-event-number . extracts) (problem . hits) guard-code . lambda-code) t)
access-cl-cache-linemacro
(defmacro access-cl-cache-line (line field) (case field (:lambda-object `(caaar ,LINE)) (:status `(cdaar ,LINE)) (:absolute-event-number `(cadar ,LINE)) (:extracts `(cddar ,LINE)) (:problem `(caadr ,LINE)) (:hits `(cdadr ,LINE)) (:guard-code `(caddr ,LINE)) (:lambda-code `(cdddr ,LINE)) (otherwise (er hard 'access-cl-cache-line "Illegal field name, ~x0." field))))
other
(defparameter *cl-cache-size-default* 1000)
other
(defvar *cl-cache* *cl-cache-size-default*)
cl-cache-initfunction
(defun cl-cache-init (size) (declare (type (integer 3 *) size)) (progn$ (or (and (integerp size) (<= 3 size)) (er hard! 'set-cl-cache "Illegal argument (should be nil or integer not less than 3), ~ ~x0, for cl-cache-init." size)) (setq *cl-cache* size) t))
make-circular-listfunction
(defun make-circular-list (n) (let* ((lst (make-list n)) (last (last lst))) (setf (cdr last) lst) (mv lst last)))
make-cl-cachefunction
(defun make-cl-cache (size) (mv-let (alist last) (make-circular-list size) (make cl-cache :alist alist :size size :last last)))
cl-cache-sizefunction
(defun cl-cache-size (cl-cache) (cond ((consp cl-cache) (access cl-cache cl-cache :size)) (t (assert (natp cl-cache)) cl-cache)))
prettyify-splo-extracts-tuplesfunction
(defun prettyify-splo-extracts-tuples (extracts) (cond ((endp extracts) nil) (t (cons `(splo-extracts-tuple :gflg ,(ACCESS SPLO-EXTRACTS-TUPLE (CAR EXTRACTS) :GFLG) :satisfies-exprs ,(ACCESS SPLO-EXTRACTS-TUPLE (CAR EXTRACTS) :SATISFIES-EXPRS) :guard ,(ACCESS SPLO-EXTRACTS-TUPLE (CAR EXTRACTS) :GUARD) :body ,(ACCESS SPLO-EXTRACTS-TUPLE (CAR EXTRACTS) :BODY)) (prettyify-splo-extracts-tuples (cdr extracts))))))
print-cl-cache-linefunction
(defun print-cl-cache-line (i line) (let ((lambda-object (access cl-cache-line line :lambda-object)) (status (access cl-cache-line line :status)) (absolute-event-number (access cl-cache-line line :absolute-event-number)) (extracts (access cl-cache-line line :extracts)) (problem (access cl-cache-line line :problem)) (hits (access cl-cache-line line :hits)) (guard-code (access cl-cache-line line :guard-code)) (lambda-code (access cl-cache-line line :lambda-code))) (cw "(~c0. :lambda-object ~y1 ~t2:status ~x3 ~t2:abs-event-no ~x4 ~t2:extracts ~y5 ~t2:problem ~y6 ~t2:hits ~x7~%~ ~t2:guard-code ~s8~%~ ~t2:lambda-code ~s9)~%" (cons i 4) lambda-object 7 status absolute-event-number (prettyify-splo-extracts-tuples extracts) problem hits (if guard-code "<code>" "NIL") (if lambda-code "<code>" "NIL"))))
print-cl-cache-fnfunction
(defun print-cl-cache-fn (i j) (let ((cl-cache *cl-cache*)) (cond ((consp cl-cache) (cw "See the defun of print-cl-cache for a comment containing ~ reminders about the cache!~%~%") (let* ((min (cond ((and (natp i) (< i (access cl-cache cl-cache :size))) i) (t 0))) (max (cond ((and (natp j) (<= min j) (< j (access cl-cache cl-cache :size))) j) ((and i (null j)) i) (t (- (access cl-cache cl-cache :size) 1))))) (loop for i from 0 to (- (access cl-cache cl-cache :size) 1) as line in (access cl-cache cl-cache :alist) until (null line) when (and (<= min i) (<= i max)) do (print-cl-cache-line i line))) nil) (t (cw "Cl-cache is uninitialized with size ~x0.~%" *cl-cache*) nil))))
cl-cache-add-entryfunction
(defun cl-cache-add-entry (cl-cache line tail previous-tail) (let ((alist (access cl-cache cl-cache :alist))) (setf (cdr previous-tail) (cdr tail)) (setf (car tail) line) (setf (cdr tail) alist) (let ((new-alist tail) (last (access cl-cache cl-cache :last))) (setf (access-cl-cache cl-cache :alist) tail) (setf (cdr last) new-alist)) line))
invalidate-some-cl-cache-linesfunction
(defun invalidate-some-cl-cache-lines (flg wrld) (and (consp *cl-cache*) (let ((cl-cache *cl-cache*) (lines (access cl-cache *cl-cache* :alist)) (evno (if (eq flg 'retraction) (max-absolute-event-number wrld) nil))) (setq *cl-cache* (access cl-cache *cl-cache* :size)) (cond ((eq flg 'extension) (loop for line in lines until (null line) when (eq (access cl-cache-line line :status) :bad) do (setf (access-cl-cache-line line :status) :unknown))) (t (loop for line in lines until (null line) when (and (eq (access cl-cache-line line :status) :good) (< evno (access cl-cache-line line :absolute-event-number))) do (setf (access-cl-cache-line line :absolute-event-number) nil) (setf (access-cl-cache-line line :status) :unknown)))) (setq *cl-cache* cl-cache) nil)))
collect-from-extractsfunction
(defun collect-from-extracts (key extracts acc) (cond ((endp extracts) acc) (t (collect-from-extracts key (cdr extracts) (case key (:satisfies-exprs (union-equal-removing-duplicates (access splo-extracts-tuple (car extracts) :satisfies-exprs) acc)) (:guard (add-to-set-equal (access splo-extracts-tuple (car extracts) :guard) acc)) (:body (add-to-set-equal (access splo-extracts-tuple (car extracts) :body) acc)) (otherwise (er hard 'collect-from-extracts "We cannot collect values of key ~x0." key)))))))
maybe-re-validate-cl-cache-linefunction
(defun maybe-re-validate-cl-cache-line (line w state) (let* ((ens (ens state)) (extracts (access cl-cache-line line :extracts))) (assert (eq (access-cl-cache-line line :status) :unknown)) (setf (access-cl-cache-line line :problem) 're-validation-interrupted) (cond ((well-formed-lambda-objectp1 extracts w) (let* ((non-compliant-fns1 (collect-non-common-lisp-compliants (all-fnnames1-exec t (collect-from-extracts :guard extracts nil) nil) w)) (non-compliant-fns2 (or non-compliant-fns1 (collect-non-common-lisp-compliants (all-fnnames1-exec t (collect-from-extracts :body extracts nil) nil) w))) (bad-fns (or non-compliant-fns2 (mv-let (warrants unwarranteds) (warrants-for-tamep-lambdap (collect-from-extracts :body extracts nil) w nil nil) (declare (ignore warrants)) unwarranteds)))) (cond ((null bad-fns) (mv-let (cl-set ttree) (if (member-equal (access cl-cache-line line :lambda-object) (global-val 'common-lisp-compliant-lambdas w)) (mv nil nil) (guard-clauses-for-fn (access cl-cache-line line :lambda-object) nil ens w nil nil nil)) (declare (ignore ttree)) (mv-let (cl-set1 ttree calist) (tau-clausep-lst cl-set ens w nil nil state nil) (declare (ignore ttree calist)) (cond ((null cl-set1) (mv-let (guard-lambda body-lambda) (make-compileable-guard-and-body-lambdas (access cl-cache-line line :lambda-object) state) (setf (access-cl-cache-line line :guard-code) (compile nil guard-lambda)) (setf (access-cl-cache-line line :lambda-code) (compile nil body-lambda)) (setf (access-cl-cache-line line :problem) nil) (setf (access-cl-cache-line line :absolute-event-number) (max-absolute-event-number w)) (setf (access-cl-cache-line line :status) :good) line)) (t (setf (access-cl-cache-line line :problem) (cons 'unproved-guard-clauses cl-set1)) (setf (access-cl-cache-line line :status) :bad) line))))) (t (setf (access-cl-cache-line line :problem) (cond (non-compliant-fns1 (cons 'guard-uses-non-compliant-fns non-compliant-fns1)) (non-compliant-fns2 (cons 'body-uses-non-compliant-fns non-compliant-fns2)) (t (cons 'body-uses-unwarranted-fns bad-fns)))) (setf (access-cl-cache-line line :status) :bad) line)))) (t (setf (access-cl-cache-line line :problem) 'not-well-formed) (setf (access-cl-cache-line line :status) :bad) line))))
valid-cl-cache-linefunction
(defun valid-cl-cache-line (line w state) (let ((status (access cl-cache-line line :status))) (setf (access-cl-cache-line line :hits) (1+ (access cl-cache-line line :hits))) (cond ((eq status :unknown) (maybe-re-validate-cl-cache-line line w state)) (t line))))
potential-function-namepfunction
(defun potential-function-namep (x w) (and (symbolp x) (not (getpropc x 'predefined nil w)) (mv-let (erp msg) (chk-all-but-new-name-cmp x 'potential-function-namep 'function w) (declare (ignore msg)) (null erp))))
potential-termpmutual-recursion
(mutual-recursion (defun potential-termp (x arity-alist w) (declare (xargs :guard (plist-worldp-with-formals w))) (cond ((atom x) (if (legal-variablep x) arity-alist :illegal)) ((eq (car x) 'quote) (if (and (consp (cdr x)) (null (cddr x))) arity-alist :illegal)) ((symbolp (car x)) (let ((arity-alist (potential-term-listp (cdr x) arity-alist w))) (cond ((eq arity-alist :illegal) :illegal) ((and (getpropc (car x) 'predefined nil w) (arity (car x) w)) (if (eql (length (cdr x)) (arity (car x) w)) arity-alist :illegal)) ((potential-function-namep (car x) w) (let* ((temp (assoc-eq (car x) arity-alist)) (n (length (cdr x))) (arity (if temp (cdr temp) n)) (arity-alist (if temp arity-alist (cons (cons (car x) n) arity-alist)))) (if (eql n arity) arity-alist :illegal))) (t :illegal)))) ((and (consp (car x)) (true-listp (car x)) (eq (car (car x)) 'lambda) (eql 3 (length (car x))) (arglistp (cadr (car x)))) (let* ((arity-alist1 (potential-termp (caddr (car x)) arity-alist w)) (arity-alist (if (eq arity-alist1 :illegal) :illegal (potential-term-listp (cdr x) arity-alist1 w)))) (if (and (not (eq arity-alist :illegal)) (null (set-difference-eq (all-vars (caddr (car x))) (cadr (car x)))) (eql (length (cadr (car x))) (length (cdr x)))) arity-alist :illegal))) (t :illegal))) (defun potential-term-listp (x arity-alist w) (declare (xargs :guard (plist-worldp-with-formals w))) (cond ((atom x) (if (eq x nil) arity-alist :illegal)) (t (let ((arity-alist (potential-termp (car x) arity-alist w))) (cond ((eq arity-alist :illegal) :illegal) (t (potential-term-listp (cdr x) arity-alist w))))))))
make-new-cl-cache-linefunction
(defun make-new-cl-cache-line (fn status w state) (cond ((eq status :ugly) (make cl-cache-line :lambda-object fn :status :ugly :absolute-event-number nil :extracts nil :problem nil :hits 1 :guard-code nil :lambda-code nil)) (t (let ((extracts (syntactically-plausible-lambda-objectp nil fn))) (cond ((null extracts) (cond ((or (eq status :good) (eq status :bad)) (er hard 'make-new-cl-cache-line "The caller of make-new-cl-cache-line said the status of ~ ~x0 is ~x1 but we have determined that it is actually ~ :UGLY. Please contact the ACL2 developers." fn status)) (t (make cl-cache-line :lambda-object fn :status :ugly :absolute-event-number nil :extracts nil :problem nil :hits 1 :guard-code nil :lambda-code nil)))) ((eq status :good) (mv-let (guard-lambda body-lambda) (make-compileable-guard-and-body-lambdas fn state) (make cl-cache-line :lambda-object fn :status status :absolute-event-number (+ 1 (max-absolute-event-number w)) :extracts extracts :problem nil :hits 1 :guard-code (compile nil guard-lambda) :lambda-code (compile nil body-lambda)))) ((eq status :bad) (make cl-cache-line :lambda-object fn :status :bad :absolute-event-number nil :extracts extracts :problem nil :hits 1 :guard-code nil :lambda-code nil)) ((well-formed-lambda-objectp1 extracts w) (maybe-re-validate-cl-cache-line (make cl-cache-line :lambda-object fn :status :unknown :absolute-event-number nil :extracts extracts :problem nil :hits 1 :guard-code nil :lambda-code nil) w state)) ((eq (potential-term-listp (collect-from-extracts :satisfies-exprs extracts (collect-from-extracts :guard extracts (collect-from-extracts :body extracts nil))) nil w) :illegal) (make cl-cache-line :lambda-object fn :status :ugly :absolute-event-number nil :extracts nil :problem nil :hits 1 :guard-code nil :lambda-code nil)) (t (make cl-cache-line :lambda-object fn :status :bad :absolute-event-number nil :extracts extracts :problem 'not-well-formed :hits 1 :guard-code nil :lambda-code nil)))))))
fetch-cl-cache-linefunction
(defun fetch-cl-cache-line (fn vline) (let* ((cl-cache *cl-cache*) (state *the-live-state*) (w (w state)) (valid-p (consp cl-cache)) (valid-cl-alist (and valid-p (access cl-cache cl-cache :alist)))) (cond ((car valid-cl-alist) (prog1 (progn (setq *cl-cache* (access cl-cache cl-cache :size)) (cond ((hons-equal-lite (access cl-cache-line (car valid-cl-alist) :lambda-object) fn) (if vline (progn (setf (access-cl-cache-line vline :hits) (access cl-cache-line (car valid-cl-alist) :hits)) (setf (car valid-cl-alist) vline)) (valid-cl-cache-line (car valid-cl-alist) w state))) (t (loop for i from 1 to (- (access cl-cache cl-cache :size) 2) as tail on (cdr valid-cl-alist) as previous-tail on valid-cl-alist when (or (null (car tail)) (hons-equal-lite (access cl-cache-line (car tail) :lambda-object) fn)) do (let ((line (if (null (car tail)) (or vline (make-new-cl-cache-line fn :unknown w state)) (if vline (progn (setf (access-cl-cache-line vline :hits) (access cl-cache-line (car tail) :hits)) vline) (valid-cl-cache-line (car tail) w state))))) (return (cl-cache-add-entry cl-cache line tail previous-tail))) finally (progn (setq tail (cdr tail) previous-tail (cdr previous-tail)) (assert (eq tail (access cl-cache cl-cache :last))) (let* ((found (hons-equal-lite (access cl-cache-line (car tail) :lambda-object) fn)) (line (if vline (if found (progn (setf (access-cl-cache-line vline :hits) (access cl-cache-line (car tail) :hits)) vline) vline) (cond (found (valid-cl-cache-line (car tail) w state)) (t (make-new-cl-cache-line fn :unknown w state)))))) (when (or vline (not found)) (setf (car tail) line)) (setf (access-cl-cache cl-cache :alist) tail) (setf (access-cl-cache cl-cache :last) previous-tail) (return line))))))) (setq *cl-cache* cl-cache))) (t (let ((size (cl-cache-size cl-cache))) (when (not valid-p) (setq *cl-cache* size) (setq cl-cache (cond ((consp cl-cache) (loop for i from 1 to size as tail on (access cl-cache cl-cache :alist) do (setf (car tail) nil))) (t (make-cl-cache size))))) (prog1 (let ((cl-alist (access cl-cache cl-cache :alist)) (line (or vline (make-new-cl-cache-line fn :unknown w state)))) (setf (car cl-alist) line)) (setq *cl-cache* cl-cache)))))))
add-good-lambda-objects-to-cl-cachefunction
(defun add-good-lambda-objects-to-cl-cache (lambda-objects wrld state) (if (not (global-val 'boot-strap-flg wrld)) (loop for obj in lambda-objects do (fetch-cl-cache-line obj (make-new-cl-cache-line obj :good wrld state))) nil))
ping-cl-cache-linefunction
(defun ping-cl-cache-line (i) (access cl-cache-line (fetch-cl-cache-line (access cl-cache-line (nth i (access cl-cache *cl-cache* :alist)) :lambda-object) nil) :status))
prettyify-cl-cache-linefunction
(defun prettyify-cl-cache-line (line) (list (access cl-cache-line line :lambda-object) (access cl-cache-line line :status) (prettyify-splo-extracts-tuples (access cl-cache-line line :extracts)) (access cl-cache-line line :problem) (and (access cl-cache-line line :guard-code) '<guard-code>) (and (access cl-cache-line line :lambda-code) '<lambda-code>)))
apply$-lambdafunction
(defun apply$-lambda (fn args) (declare (ftype (function (t t) (values t)) ev$)) (let* ((state *the-live-state*) (w (w state)) (fn (if (and (consp fn) (eq (car fn) *lambda$-marker*)) (cdr (or (assoc-equal (cdr fn) (global-val 'lambda$-alist w)) (er hard 'apply$-lambda "Apply$-lambda has encountered an untranslated ~ lambda$ expression, ~x0, not resolved by ~ lambda-alist$. We suspect this has occurred ~ during the pre-loading of a certified book. ~ Lambda$ should not used in functions or terms ~ that might be evaluated during pre-loading of ~ books. We check that there are no lambda$ ~ expressions ancestrally used in DEFCONST, ~ DEFPKG, and DEFMACRO events. But we have ~ apparently not checked it for some other ~ context and so we have allowed a book to be ~ certified despite the use of a lambda$ in some ~ sensitive context. Please advise the ACL2 ~ developers so we can catch this violation ~ earlier. Meanwhile, you can work around this ~ by replacing the offending lambda$ expression ~ by its quoted translation and then recertify ~ the offending book. One way to find the fully ~ translated form of this lambda$ expression is ~ to evaluate~%:trans ~x1~%and grab the quoted ~ lambda object in the result. We can't do this ~ for you because we do not have access to the ~ logical world in which the lambda$ is supposed ~ to be translated. Sorry!" (cdr fn) `(apply$ ,(CDR FN) args)))) fn)) (line (and *aokp* (fetch-cl-cache-line fn nil)))) (cond ((and line (not (eq (f-get-global 'guard-checking-on *the-live-state*) :none))) (cond ((eq (access cl-cache-line line :status) :good) (cond ((apply (access cl-cache-line line :guard-code) args) (return-from apply$-lambda (apply (access cl-cache-line line :lambda-code) args))) ((f-get-global 'guard-checking-on *the-live-state*) (throw-raw-ev-fncall (list 'ev-fncall-guard-er fn args (untranslate (access splo-extracts-tuple (car (access cl-cache-line line :extracts)) :guard) t (w *the-live-state*)) (make-list (length (lambda-formals fn))) nil))))) ((eq (access cl-cache-line line :status) :bad) (let ((guard (access splo-extracts-tuple (car (access cl-cache-line line :extracts)) :guard)) (wrld (w *the-live-state*))) (cond ((termp guard wrld) (mv-let (erp val) (ev-w guard (pairlis$ (lambda-formals fn) args) wrld nil t nil nil nil) (cond ((and (null erp) val) (return-from apply$-lambda (apply$-lambda-logical fn args))) ((f-get-global 'guard-checking-on *the-live-state*) (throw-raw-ev-fncall (list 'ev-fncall-guard-er fn args (untranslate guard t wrld) (make-list (length (lambda-formals fn))) nil)))))) ((f-get-global 'guard-checking-on *the-live-state*) (throw-raw-ev-fncall (list 'ev-fncall-guard-er fn args (cons :not-a-term guard) (make-list (length (lambda-formals fn))) nil))))))))) (apply$-lambda-logical fn args)))