other
(in-package "ACL2")
other
(set-ignore-ok t)
other
(set-irrelevant-formals-ok t)
other
(set-state-ok t)
other
(program)
chk-common-lisp-compliant-subfunctions-cmp-testingfunction
(defun chk-common-lisp-compliant-subfunctions-cmp-testing (names0 names terms wrld str ctx) (cond ((null names) (value-cmp nil)) (t (let* ((fns (set-difference-eq (all-fnnames1-exec t (cons (car terms) (if (global-val 'boot-strap-flg wrld) nil (collect-guards-and-bodies (collect-certain-lambda-objects :well-formed (car terms) wrld nil)))) (if (global-val 'boot-strap-flg wrld) nil (all-fnnames! nil :inside nil (car terms) nil wrld nil))) names0)) (bad (collect-non-common-lisp-compliants fns wrld))) (cond (t (mv-let (warrants unwarranteds) (if (global-val 'boot-strap-flg wrld) (mv nil nil) (warrants-for-tamep-lambdap-lst (collect-certain-lambda-objects :well-formed (car terms) wrld nil) wrld nil nil)) (declare (ignore warrants)) (cond (unwarranteds (er-cmp ctx "The ~@0 for ~x1 applies the function~#2~[ ~ ~&2~/s ~&2~] which ~#2~[is~/are~] not yet ~ warranted. Lambda objects containing ~ unwarranted function symbols are not ~ provably tame and can't be applied. See ~ :DOC verify-guards." str (car names) unwarranteds)) (t (chk-common-lisp-compliant-subfunctions-cmp-testing names0 (cdr names) (cdr terms) wrld str ctx))))))))))
chk-acceptable-verify-guards-formula-cmp-testingfunction
(defun chk-acceptable-verify-guards-formula-cmp-testing (name x ctx wrld state-vars) (mv-let (erp term bindings) (translate1-cmp x :stobjs-out '((:stobjs-out . :stobjs-out)) t ctx wrld state-vars) (declare (ignore bindings)) (cond ((and erp (null name)) (mv-let (erp2 term2 bindings) (translate1-cmp x t nil t ctx wrld state-vars) (declare (ignore bindings term2)) (cond (erp2 (mv erp term)) (t (er-cmp ctx "The guards for the given formula cannot be verified ~ because it has the wrong syntactic form for evaluation, ~ perhaps due to multiple-value or stobj restrictions. ~ See :DOC verify-guards."))))) (erp (er-cmp ctx "The guards for ~x0 cannot be verified because its formula has ~ the wrong syntactic form for evaluation, perhaps due to ~ multiple-value or stobj restrictions. See :DOC verify-guards." (or name x))) (t (er-progn-cmp (chk-common-lisp-compliant-subfunctions-cmp-testing (list name) (list name) (list term) wrld "formula" ctx) (value-cmp (cons :term term)))))))
chk-acceptable-verify-guards-cmp-testingfunction
(defun chk-acceptable-verify-guards-cmp-testing (name rrp guard-simplify ctx wrld state-vars) (er-let*-cmp ((ignore (cond ((member-eq guard-simplify '(t :limited)) (value-cmp nil)) (t (er-cmp ctx "~@0" (guard-simplify-msg guard-simplify))))) (name (cond ((symbolp name) (value-cmp name)) ((and (consp name) (or (eq (car name) 'lambda) (eq (car name) 'lambda$))) (cond ((eq (car name) 'lambda) (cond ((well-formed-lambda-objectp name wrld) (mv-let (erp val) (hons-copy-lambda-object? (kwote name)) (cond (erp (er-cmp ctx "~@0" val)) (t (value-cmp (unquote val)))))) (t (er-cmp ctx "~x0 is not a well-formed LAMBDA expression. See :DOC ~ verify-guards." name)))) (t (mv-let (erp val bindings) (translate11-lambda-object name '(nil) nil nil nil name 'verify-guards wrld state-vars nil) (declare (ignore bindings)) (mv erp (if erp val (unquote val))))))) (t (er-cmp ctx "~x0 is not a symbol, a lambda object, or a lambda$ ~ expression. See :DOC verify-guards." name))))) (let ((symbol-class (cond ((symbolp name) (symbol-class name wrld)) ((member-equal name (global-val 'common-lisp-compliant-lambdas wrld)) :common-lisp-compliant) (t :program)))) (cond ((and rrp (eq symbol-class :common-lisp-compliant)) (value-cmp 'redundant)) ((consp name) (let* ((names (list name)) (guards (list (lambda-object-guard name))) (bodies (list (lambda-object-body name)))) (er-progn-cmp (chk-common-lisp-compliant-subfunctions-cmp-testing names names guards wrld "guard" ctx) (chk-common-lisp-compliant-subfunctions-cmp-testing names names bodies wrld "body" ctx) (value-cmp names)))) ((getpropc name 'theorem nil wrld) (er-progn-cmp (chk-acceptable-verify-guards-formula-cmp-testing name (getpropc name 'untranslated-theorem nil wrld) ctx wrld state-vars) (value-cmp (list name)))) ((function-symbolp name wrld) (case symbol-class (:program (er-cmp ctx "~x0 is in :program mode. Only :logic mode functions can ~ have their guards verified. See :DOC verify-guards." name)) ((:ideal :common-lisp-compliant) (let* ((recp (getpropc name 'recursivep nil wrld)) (names (cond ((null recp) (list name)) (t recp))) (bad-names (if (eq symbol-class :ideal) (collect-non-ideals names wrld) (collect-programs names wrld)))) (cond (bad-names (er-cmp ctx "One or more of the mutually-recursive peers of ~ ~x0 ~#1~[was not defined in :logic mode~/either ~ was not defined in :logic mode or has already had ~ its guards verified~]. The offending ~ function~#2~[ is~/s are~] ~&2. We thus cannot ~ verify the guards of ~x0. This situation can ~ arise only through redefinition." name (if (eq symbol-class :ideal) 1 0) bad-names)) (t (er-progn-cmp (chk-common-lisp-compliant-subfunctions-cmp-testing names names (guard-lst names nil wrld) wrld "guard" ctx) (chk-common-lisp-compliant-subfunctions-cmp-testing names names (getprop-x-lst names 'unnormalized-body wrld) wrld "body" ctx) (value-cmp names)))))) (otherwise (er-cmp ctx "Implementation error: Unexpected symbol-class, ~x0, for ~ the function symbol ~x1." symbol-class name)))) (t (let ((fn (deref-macro-name name (macro-aliases wrld)))) (er-cmp ctx "~x0 is not a function symbol or a theorem name in the ~ current ACL2 world. ~@1" name (cond ((eq fn name) "See :DOC verify-guards.") (t (msg "Note that ~x0 is a macro-alias for ~x1. ~ Consider calling verify-guards with ~ argument ~x1 instead, or use ~ verify-guards+. See :DOC verify-guards, ~ see :DOC verify-guards+, and see :DOC ~ macro-aliases-table." name fn))))))))))
guard-obligation-clauses-testingfunction
(defun guard-obligation-clauses-testing (x guard-debug ens wrld state) (mv-let (cl-set cl-set-ttree) (cond ((and (consp x) (eq (car x) :term)) (mv-let (cl-set cl-set-ttree) (guard-clauses+ (cdr x) (and guard-debug :top-level) nil nil ens wrld (f-get-global 'safe-mode state) (gc-off state) nil nil) (mv cl-set cl-set-ttree))) ((and (consp x) (null (cdr x)) (symbolp (car x)) (getpropc (car x) 'theorem nil wrld)) (mv-let (cl-set cl-set-ttree) (guard-clauses+ (getpropc (car x) 'theorem nil wrld) (and guard-debug (car x)) nil nil ens wrld (f-get-global 'safe-mode state) (gc-off state) nil nil) (mv cl-set cl-set-ttree))) (t (guard-clauses-for-clique x (cond ((null guard-debug) nil) ((cdr x) 'mut-rec) (t t)) ens wrld (f-get-global 'safe-mode state) nil nil))) (mv-let (cl-set cl-set-ttree) (clean-up-clause-set cl-set (if (eq ens :do-not-simplify) nil ens) wrld cl-set-ttree state) (mv cl-set cl-set-ttree))))
guard-obligation-testingfunction
(defun guard-obligation-testing (x rrp guard-debug guard-simplify ctx state) (let* ((wrld (w state)) (namep (and (symbolp x) (not (keywordp x)) (not (defined-constant x wrld))))) (er-let*-cmp ((y (cond (namep (chk-acceptable-verify-guards-cmp-testing x rrp guard-simplify ctx wrld (default-state-vars t))) (t (chk-acceptable-verify-guards-formula-cmp-testing nil x ctx wrld (default-state-vars t)))))) (cond ((and namep (eq y 'redundant)) (value-cmp :redundant)) (t (mv-let (cl-set cl-set-ttree) (guard-obligation-clauses-testing y guard-debug (if (guard-simplify-p guard-simplify ctx) (ens state) :do-not-simplify) wrld state) (value-cmp (list* y cl-set cl-set-ttree))))))))
other
(set-ignore-ok nil)
other
(set-irrelevant-formals-ok nil)
other
(set-state-ok nil)