other
(in-package "ACL2")
tails-acfunction
(defun tails-ac (lst ac) (declare (xargs :guard (true-listp ac) :mode :program)) (cond ((atom lst) (revappend ac nil)) (t (tails-ac (cdr lst) (cons lst ac)))))
tailsfunction
(defun tails (lst) (declare (xargs :guard t :mode :program)) (mbe :logic (cond ((atom lst) nil) (t (cons lst (tails (cdr lst))))) :exec (tails-ac lst nil)))
empty-loop$-as-tuplepfunction
(defun empty-loop$-as-tuplep (tuple) (declare (xargs :guard (true-list-listp tuple) :mode :program)) (cond ((endp tuple) nil) ((endp (car tuple)) t) (t (empty-loop$-as-tuplep (cdr tuple)))))
car-loop$-as-tuplefunction
(defun car-loop$-as-tuple (tuple) (declare (xargs :guard (true-list-listp tuple) :mode :program)) (cond ((endp tuple) nil) (t (cons (caar tuple) (car-loop$-as-tuple (cdr tuple))))))
cdr-loop$-as-tuplefunction
(defun cdr-loop$-as-tuple (tuple) (declare (xargs :guard (true-list-listp tuple) :mode :program)) (cond ((endp tuple) nil) (t (cons (cdar tuple) (cdr-loop$-as-tuple (cdr tuple))))))
loop$-as-acfunction
(defun loop$-as-ac (tuple ac) (declare (xargs :guard (and (true-list-listp tuple) (true-listp ac)) :mode :program)) (cond ((endp tuple) (revappend ac nil)) ((empty-loop$-as-tuplep tuple) (revappend ac nil)) (t (loop$-as-ac (cdr-loop$-as-tuple tuple) (cons (car-loop$-as-tuple tuple) ac)))))
loop$-asfunction
(defun loop$-as (tuple) (declare (xargs :guard (true-list-listp tuple) :mode :program)) (mbe :logic (cond ((endp tuple) nil) ((empty-loop$-as-tuplep tuple) nil) (t (cons (car-loop$-as-tuple tuple) (loop$-as (cdr-loop$-as-tuple tuple))))) :exec (loop$-as-ac tuple nil)))
from-to-by-measurefunction
(defun from-to-by-measure (i j) (declare (xargs :guard t)) (if (and (integerp i) (integerp j) (<= i j)) (+ 1 (- j i)) 0))
from-to-by-acfunction
(defun from-to-by-ac (i j k ac) (declare (xargs :guard (and (integerp i) (integerp j) (integerp k) (< 0 k) (true-listp ac)) :mode :program)) (cond ((mbt (and (integerp i) (integerp j) (integerp k) (< 0 k))) (cond ((<= i j) (from-to-by-ac i (- j k) k (cons j ac))) (t ac))) (t nil)))
from-to-byfunction
(defun from-to-by (i j k) (declare (xargs :guard (and (integerp i) (integerp j) (integerp k) (< 0 k)) :mode :program)) (mbe :logic (cond ((mbt (and (integerp i) (integerp j) (integerp k) (< 0 k))) (cond ((<= i j) (cons i (from-to-by (+ i k) j k))) (t nil))) (t nil)) :exec (if (< j i) nil (from-to-by-ac i (+ i (* k (floor (- j i) k))) k nil))))
*apply$-userfn-callers*constant
(defconst *apply$-userfn-callers* '(apply$ ev$ apply$-userfn))
*blacklisted-apply$-fns*constant
(defconst *blacklisted-apply$-fns* (union-eq '(synp wormhole1 wormhole-eval sync-ephemeral-whs-with-persistent-whs set-persistent-whs-and-ephemeral-whs sys-call hons-clear! hons-wash! untouchable-marker aset1-trusted coerce-object-to-state create-state init-iprint-fal update-iprint-fal-rec update-iprint-fal) *avoid-oneify-fns*))
split-system-verify-guards-alistfunction
(defun split-system-verify-guards-alist (alist wrld alist1 alist2) (declare (xargs :guard (and (symbol-alistp alist) (plist-worldp wrld) (true-listp alist1) (true-listp alist2)))) (cond ((endp alist) (mv (reverse alist1) (reverse alist2))) (t (let ((fn (caar alist))) (cond ((getpropc fn 'absolute-event-number nil wrld) (split-system-verify-guards-alist (cdr alist) wrld (cons (car alist) alist1) alist2)) (t (split-system-verify-guards-alist (cdr alist) wrld alist1 (cons (car alist) alist2))))))))
*system-verify-guards-alist*constant
(defconst *system-verify-guards-alist* '((abbrev-evisc-tuple) (abstract-pat) (abstract-pat1 acl2-count pat) (abstract-pat1-lst acl2-count pats) (access-command-tuple-number) (add-suffix-to-fn) (alist-to-doublets acl2-count alist) (alistp-listp acl2-count x) (all-fnnames1 acl2-count x) (always$ acl2-count lst) (always$+ acl2-count lst) (append$ acl2-count lst) (append$+ acl2-count lst) (append$+-ac acl2-count lst) (append$-ac acl2-count lst) (apply$ :? args fn) (apply$-badge-alistp-ilks-t acl2-count alist) (apply$-badge-p) (apply$-lambda :? args fn) (apply$-prim) (arglistp) (arglistp1 acl2-count lst) (arities-okp acl2-count user-table) (arity) (arity-alistp acl2-count alist) (aset1-lst acl2-count alist) (attach-stobj-guard) (attach-stobj-guard-msg) (backchain-limit-listp acl2-count lst) (badge) (badge-userfn-structure-alistp acl2-count x) (bind-macro-args) (bind-macro-args-after-rest) (bind-macro-args-keys) (bind-macro-args-keys1 acl2-count args) (bind-macro-args-optional acl2-count args) (bind-macro-args1 acl2-count args) (brr-criteria-alistp acl2-count alist) (built-in-brr-near-missp) (car-loop$-as-tuple acl2-count tuple) (cdr-loop$-as-tuple acl2-count tuple) (cert-annotationsp) (char?) (chk-all-but-new-name-cmp) (chk-length-and-keys acl2-count actuals) (collect$ acl2-count lst) (collect$+ acl2-count lst) (collect$+-ac acl2-count lst) (collect$-ac acl2-count lst) (collect-by-position acl2-count full-domain) (collect-lambda-keywordps acl2-count lst) (collect-non-x acl2-count lst) (collect-posp-indices-to-header acl2-count ar) (comment-string-p) (comment-string-p1 nfix (binary-+ end (unary-- i))) (cons-ppr1) (cons-ppr1-guardp) (cons-term1-mv2) (def-body) (defstobj-fnname) (defstobj-fnname-key2) (defun-mode) (disabledp-fn) (disabledp-fn-lst acl2-count runic-mapping-pairs) (doublet-listp acl2-count x) (duplicate-keys-action) (empty-loop$-as-tuplep acl2-count tuple) (enabled-numep) (enabled-runep) (enabled-structure-p) (ens) (equal-x-constant) (er-cmp-fn) (er-off-p) (er-off-p1) (error-fms) (error-fms-channel) (error1) (error1-safe) (error1-state-p) (ev$ :? a x) (ev$-list :? a x) (evisc-tuple) (eviscerate) (eviscerate-simple) (eviscerate-top) (eviscerate-top-state-p) (eviscerate1 binary-+ '1 (binary-* '2 (acl2-count x))) (eviscerate1-lst binary-* '2 (acl2-count lst)) (eviscerate1p binary-+ '1 (binary-* '2 (acl2-count x))) (eviscerate1p-lst binary-* '2 (acl2-count lst)) (executable-badge) (executable-suitably-tamep-listp acl2-count args) (executable-tamep acl2-count x) (executable-tamep-functionp acl2-count fn) (expand-all-lambdas acl2-count term) (expand-all-lambdas-lst acl2-count terms) (ffnnamep acl2-count term) (ffnnamep-lst acl2-count l) (filename-to-book-name) (filename-to-book-name-1) (find-alternative-skip nfix (binary-+ maximum (unary-- i))) (find-alternative-start) (find-alternative-start1 nfix (binary-+ maximum (unary-- i))) (find-alternative-stop nfix (binary-+ (binary-+ '1 maximum) (unary-- i))) (find-dot-dot nfix (binary-+ (length full-pathname) (unary-- i))) (find-first-bad-arg acl2-count args) (find-warrant-function-name) (flatten-ands-in-lit-lst acl2-count x) (flpr) (flpr1 binary-+ '1 (binary-* '2 (acl2-count x))) (flpr11 binary-* '2 (acl2-count x)) (flsz) (flsz-atom if (not (fixnat-guard acc)) '0 (acl2-count x)) (flsz-integer if (not (if (integerp x) (if (natp acc) (if (< acc '1152921504606846975) (print-base-p print-base) 'nil) 'nil) 'nil)) '0 (if (< x '0) (binary-+ '1 (unary-- x)) (if (< x print-base) '0 x))) (flsz1 acl2-count x) (fms) (fms!) (fmt) (fmt!) (fmt-abbrev) (fmt-abbrev1) (fmt-char) (fmt-ctx) (fmt-hard-right-margin) (fmt-in-ctx) (fmt-ppr) (fmt-soft-right-margin) (fmt-state-p) (fmt-tilde-cap-s nfix clk) (fmt-tilde-cap-s1 if (not (if (fmt-state-p state) (if (fixnat-guard i) (if (fixnat-guard maximum) (if (fixnat-guard col) (if (stringp s) (if (not (< (length s) maximum)) (if (open-output-channel-p channel ':character state) (< i maximum) 'nil) 'nil) 'nil) 'nil) 'nil) 'nil) 'nil)) '0 (nfix (binary-+ maximum (unary-- i)))) (fmt-tilde-s nfix clk) (fmt-tilde-s1 if (not (if (fmt-state-p state) (if (fixnat-guard i) (if (fixnat-guard maximum) (if (fixnat-guard col) (if (stringp s) (if (not (< (length s) maximum)) (if (open-output-channel-p channel ':character state) (< i maximum) 'nil) 'nil) 'nil) 'nil) 'nil) 'nil) 'nil)) '0 (if (if (< (fmt-hard-right-margin state) col) (not (write-for-read state)) 'nil) (binary-+ '2 (nfix (binary-* '2 (binary-+ maximum (unary-- i))))) (binary-+ '1 (nfix (binary-* '2 (binary-+ maximum (unary-- i))))))) (fmt-var) (fmt0 nfix clk) (fmt0&v nfix clk) (fmt0* nfix clk) (fmt1) (fmt1!) (fmx!-cw-fn) (fmx-cw-fn) (fmx-cw-fn-guard) (fmx-cw-msg) (fmx-cw-msg-1 nfix clk) (fnume) (formalized-varlistp acl2-count varlist) (from-to-by from-to-by-measure i j) (from-to-by-ac from-to-by-measure i j) (fsubcor-var acl2-count form) (fsubcor-var-lst acl2-count forms) (gag-mode-evisc-tuple) (genvar) (genvar-guardp) (genvar1 :? cnt avoid-lst char-lst pkg-witness) (genvar1-guardp) (get-brr-one-way-unify-info) (get-sharp-atsign) (gsym) (ilks-per-argument-slot) (ilks-plist-worldp) (illegal-fmt-string) (implicate) (include-book-dir) (init-iprint-fal) (iprint-alistp) (iprint-alistp1 acl2-count x) (iprint-alistp1-weak acl2-count x) (iprint-ar-aref1) (iprint-ar-illegal-index) (iprint-blockedp) (iprint-eager-p) (iprint-enabledp) (iprint-fal-name) (iprint-hard-bound) (iprint-last-index) (iprint-oracle-updates?) (iprint-soft-bound) (keyword-param-valuep) (lambda-keywordp) (lambda-subtermp acl2-count term) (lambda-subtermp-lst acl2-count termlist) (latest-body) (left-pad-with-blanks) (legal-constantp) (legal-initp) (legal-variable-or-constant-namep) (legal-variablep) (logic-fns-list-listp acl2-count x) (logic-fns-listp acl2-count lst) (logic-fnsp acl2-count term) (logic-term-list-listp) (logic-term-listp) (logic-termp) (logical-name-type) (logical-namep) (loop$-as acl2-count tuple) (loop$-as-ac acl2-count tuple) (macro-arglist-after-restp) (macro-arglist-keysp acl2-count args) (macro-arglist-optionalp acl2-count args) (macro-arglist1p acl2-count args) (macro-args) (macro-args-er-cmp) (macro-args-structurep) (macro-vars acl2-count args) (macro-vars-after-rest) (macro-vars-key acl2-count args) (macro-vars-optional acl2-count args) (make-built-in-brr-near-miss-msg) (make-lambda-application) (make-sharp-atsign) (match-clause) (match-clause-list acl2-count clauses) (match-tests-and-bindings acl2-count pat) (max-width acl2-count lst) (merge-sort-symbol< acl2-count l) (merge-sort-term-order acl2-count l) (merge-symbol< binary-+ (len l1) (len l2)) (merge-term-order binary-+ (acl2-count l1) (acl2-count l2)) (meta-extract-contextual-fact) (meta-extract-global-fact+) (meta-extract-rw+-term) (new-namep) (newline) (number-of-digits if (not (if (integerp n) (print-base-p print-base) 'nil)) '0 (if (< n '0) (binary-+ '1 (unary-- n)) n)) (observation1-cw) (one-way-unify) (one-way-unify-restrictions) (one-way-unify-restrictions1 acl2-count restrictions) (one-way-unify1 make-ord '1 (binary-+ '1 (acl2-count pat)) '2) (one-way-unify1-equal make-ord '1 (binary-+ '2 (binary-+ (acl2-count pat1) (acl2-count pat2))) '1) (one-way-unify1-equal1 make-ord '1 (binary-+ '2 (binary-+ (acl2-count pat1) (acl2-count pat2))) '0) (one-way-unify1-lst make-ord '1 (binary-+ '1 (acl2-count pl)) '2) (one-way-unify1-quotep-subproblems) (out-of-time-the2s) (override-hints) (partition-rest-and-keyword-args) (partition-rest-and-keyword-args1 acl2-count x) (partition-rest-and-keyword-args2 acl2-count keypart) (plist-worldp-with-formals acl2-count alist) (possibly-dirty-lambda-objectp) (possibly-dirty-lambda-objectp1 acl2-count x) (possibly-dirty-lambda-objectp1-lst acl2-count x) (ppr) (ppr-tuple-lst-p acl2-count lst) (ppr-tuple-p acl2-count x) (ppr1 binary-* '2 (acl2-count x)) (ppr1-lst binary-+ '1 (binary-* '2 (acl2-count lst))) (ppr2 acl2-count x) (ppr2-column acl2-count lst) (ppr2-flat acl2-count x) (print-control-p) (project-dir-prefix-entry acl2-count project-dir-alist) (punctp) (push-io-record) (remove-guard-holders-weak) (remove-guard-holders1 acl2-count term) (remove-guard-holders1-lst acl2-count lst) (remove-lambdas) (remove-lambdas-lst acl2-count termlist) (remove-lambdas1 acl2-count term) (rollover-iprint-ar) (runep) (saved-output-token-p) (scan-past-empty-fmt-directives) (scan-past-empty-fmt-directives1 acl2-count clk) (scan-past-whitespace nfix (binary-+ maximum (unary-- i))) (scan-to-cltl-command acl2-count wrld) (silent-error) (spaces) (spaces1 nfix (binary-+ (binary-* '2 n) col)) (special-term-num) (spell-number nfix clk) (splat binary-+ '1 (binary-* '2 (acl2-count x))) (splat-atom) (splat-atom!) (splat-string) (splat1 binary-* '2 (acl2-count x)) (standard-co) (state-p+) (stobjp) (strip-caddrs acl2-count x) (strip-non-hidden-package-names acl2-count known-package-alist) (subcor-var acl2-count form) (subcor-var-lst acl2-count forms) (subcor-var1 acl2-count vars) (sublis-var) (sublis-var-lst) (sublis-var1 acl2-count form) (sublis-var1-lst acl2-count l) (subsequencep acl2-count lst1) (subst-each-for-var acl2-count new-lst) (subst-expr) (subst-expr-error) (subst-expr1 acl2-count term) (subst-expr1-lst acl2-count args) (subst-var acl2-count form) (subst-var-lst acl2-count l) (suitably-tamep-listp acl2-count args) (sum$ acl2-count lst) (sum$+ acl2-count lst) (sum$+-ac acl2-count lst) (sum$-ac acl2-count lst) (symbol-alist-to-keyword-value-list acl2-count alist) (symbol-to-fixnat-alistp acl2-count x) (syntactically-plausible-lambda-objectp acl2-count x) (syntactically-plausible-lambda-objectp1 acl2-count edcls) (syntactically-plausible-lambda-objectsp-within acl2-count body) (syntactically-plausible-lambda-objectsp-within-lst acl2-count args) (tails acl2-count lst) (tails-ac acl2-count lst) (tamep acl2-count x) (tamep-functionp acl2-count fn) (term-evisc-tuple) (term-list-listp acl2-count l) (term-listp acl2-count x) (term-order) (term-order1) (termify-clause-set acl2-count clauses) (termp acl2-count x) (the-live-var) (theory-invariant-table-guard) (thereis$ acl2-count lst) (thereis$+ acl2-count lst) (throw-nonexec-error-p) (throw-nonexec-error-p1) (translate-abbrev-rune) (translate-declaration-to-guard-gen acl2-count x) (translate-declaration-to-guard-gen-lst acl2-count l) (translate-declaration-to-guard/integer-gen) (translate-declaration-to-guard1-gen) (ttag-alistp acl2-count x) (type-expressions-from-type-spec) (until$ acl2-count lst) (until$+ acl2-count lst) (until$+-ac acl2-count lst) (until$-ac acl2-count lst) (update-iprint-alist-fal) (update-iprint-ar-fal) (update-iprint-fal) (update-iprint-fal-rec acl2-count iprint-fal-new) (warning-off-p1) (warning1-cw) (warrants-for-suitably-tamep-listp acl2-count args) (warrants-for-tamep acl2-count x) (warrants-for-tamep-functionp acl2-count fn) (weak-badge-userfn-structure-alistp acl2-count x) (weak-splo-extracts-tuple-listp acl2-count x) (well-formed-lambda-objectp) (well-formed-lambda-objectp1 acl2-count extracts) (when$ acl2-count lst) (when$+ acl2-count lst) (when$+-ac acl2-count lst) (when$-ac acl2-count lst) (world-evisceration-alist) (write-for-read) (zero-one-or-more)))
other
(when-pass-2 (make-event (mv-let (old new) (split-system-verify-guards-alist *system-verify-guards-alist* (w state) nil nil) `(progn (defconst *system-verify-guards-alist-1* ',OLD) (defconst *system-verify-guards-alist-2* ',NEW)))) (defun first-order-like-terms-and-out-arities1 (fns avoid-fns wrld ans) (declare (xargs :mode :program)) (cond ((endp fns) ans) (t (let ((fn (car fns))) (cond ((and (acl2-system-namep fn wrld) (not (member-eq fn avoid-fns)) (all-nils-or-dfs (getpropc fn 'stobjs-in nil wrld)) (all-nils-or-dfs (getpropc fn 'stobjs-out nil wrld))) (first-order-like-terms-and-out-arities1 (cdr fns) avoid-fns wrld (cons (cons (cons fn (formals fn wrld)) (length (getpropc fn 'stobjs-out nil wrld))) ans))) (t (first-order-like-terms-and-out-arities1 (cdr fns) avoid-fns wrld ans))))))) (defun first-order-like-terms-and-out-arities (world) (declare (xargs :mode :program)) (first-order-like-terms-and-out-arities1 (union-eq (strip-cars *system-verify-guards-alist-1*) (strip-base-symbols (function-theory :here))) *blacklisted-apply$-fns* world nil)) (make-event `(defconst *first-order-like-terms-and-out-arities* ',(FIRST-ORDER-LIKE-TERMS-AND-OUT-ARITIES (W STATE)))))
compute-badge-of-primitivesfunction
(defun compute-badge-of-primitives (terms-and-out-arities) (declare (xargs :mode :program)) (cond ((endp terms-and-out-arities) nil) (t (let* ((term (car (car terms-and-out-arities))) (fn (ffn-symb term)) (formals (fargs term)) (output-arity (cdr (car terms-and-out-arities)))) (hons-acons fn (make apply$-badge :arity (length formals) :out-arity output-arity :ilks t) (compute-badge-of-primitives (cdr terms-and-out-arities)))))))
other
(when-pass-2 (defconst *badge-prim-falist* (compute-badge-of-primitives *first-order-like-terms-and-out-arities*)) (defun apply$-primp (fn) (declare (xargs :mode :logic :guard t)) (and (hons-get fn *badge-prim-falist*) t)) (defun badge-prim (fn) (declare (xargs :mode :logic :guard t)) (cdr (hons-get fn *badge-prim-falist*))))
apply$-badgepfunction
(defun apply$-badgep (x) (declare (xargs :guard t)) (and (weak-apply$-badge-p x) (natp (access apply$-badge x :arity)) (natp (access apply$-badge x :out-arity)) (or (eq (access apply$-badge x :ilks) t) (and (true-listp (access apply$-badge x :ilks)) (equal (len (access apply$-badge x :ilks)) (access apply$-badge x :arity)) (not (all-nils (access apply$-badge x :ilks))) (subsetp (access apply$-badge x :ilks) '(nil :fn :expr))))))
n-car-cadr-caddr-etcfunction
(defun n-car-cadr-caddr-etc (n x) (declare (xargs :guard (natp n))) (if (zp n) nil (cons `(car ,X) (n-car-cadr-caddr-etc (- n 1) `(cdr ,X)))))
make-apply$-prim-body-fnfunction
(defun make-apply$-prim-body-fn (falist acc) (declare (xargs :mode :program)) (cond ((endp falist) (reverse acc)) (t (let* ((fn (car (car falist))) (badge (cdr (car falist))) (call1 `(,FN ,@(N-CAR-CADR-CADDR-ETC (ACCESS APPLY$-BADGE BADGE :ARITY) 'ARGS))) (call2 (if (member-eq fn *ec-call-bad-ops*) (cond ((eq fn 'return-last) '(caddr args)) ((eq fn 'mv-list) '(cadr args)) (t call1)) `(ec-call ,CALL1))) (call3 (if (int= (access apply$-badge badge :out-arity) 1) call2 `(mv-list ',(ACCESS APPLY$-BADGE BADGE :OUT-ARITY) ,CALL2)))) (make-apply$-prim-body-fn (cdr falist) (cons `(,FN ,CALL3) acc))))))
in-theory
(in-theory (disable (:e break$) (:e good-bye-fn)))
other
(when-pass-2 (set-raw-mode t) (make-apply$-prim-body-fn-raw *badge-prim-falist* *apply$-prim-ht*) (set-raw-mode nil) (defmacro make-apply$-prim-body nil `(case fn ,@(MAKE-APPLY$-PRIM-BODY-FN *BADGE-PRIM-FALIST* NIL) (otherwise nil))) (defun apply$-prim (fn args) (declare (xargs :guard (true-listp args) :mode :program)) (non-exec (make-apply$-prim-body))))