other
(in-package "ACL2")
include-book
(include-book "std/util/bstar" :dir :system)
include-book
(include-book "xdoc/top" :dir :system)
other
(program)
run-and-record-failuremacro
(defmacro run-and-record-failure (event) `(make-event '(:or (with-output :stack :pop ,EVENT) (make-event (b* ((state (f-put-global 'failed-events (cons ',EVENT (@ failed-events)) state))) (value '(value-triple :failed)))))))
run-and-record-failure-listfunction
(defun run-and-record-failure-list (events) (if (atom events) nil (cons `(run-and-record-failure ,(CAR EVENTS)) (run-and-record-failure-list (cdr events)))))
run-events-record-failuresmacro
(defmacro run-events-record-failures (events &key (with-output '(:off :all))) (b* ((events (run-and-record-failure-list events))) `(with-output ,@WITH-OUTPUT :stack :push (progn (make-event (b* ((state (f-put-global 'failed-events nil state))) (value '(value-triple :invisible)))) . ,EVENTS))))
encapsulate
(encapsulate nil (logic) (local (progn (make-event (if (and (equal (fgetprop 'foo 'formals :none (w state)) :none) (equal (fgetprop 'bar 'formals :none (w state)) :none) (not (formula 'not-foo nil (w state))) (not (formula 'foo-identity nil (w state)))) (value '(value-triple :ok)) (er soft 'run-events-record-failures-test "Foo, bar, not-foo, and foo-identity should not be defined beforehand!"))) (with-output :off (prove event warning observation error) :gag-mode nil (run-events-record-failures ((defun foo (x) x) (defthm not-foo (not (foo (foo x)))) (defun bar (x) y) (defthm foo-identity (equal (foo (foo x)) (foo x)))) :with-output (:off :all :on (error)))) (make-event (if (and (equal (@ failed-events) '((defun bar (x) y) (defthm not-foo (not (foo (foo x)))))) (equal (fgetprop 'bar 'formals :none (w state)) :none) (not (formula 'not-foo nil (w state))) (equal (fgetprop 'foo 'formals :none (w state)) '(x)) (formula 'foo-identity nil (w state))) '(value-triple :ok) (er soft 'run-events-record-failures-test "Unexpected result from run-events-record-failures"))))))
encapsulate
(encapsulate nil (logic) (local (progn (defun generate-lots-of-identity-fns (n) (declare (xargs :mode :program)) (if (zp n) nil (cons `(defun ,(INTERN-IN-PACKAGE-OF-SYMBOL (CONCATENATE 'STRING "FOO" (COERCE (EXPLODE-ATOM N 10) 'STRING)) 'FOO) (x) x) (generate-lots-of-identity-fns (1- n))))) (make-event `(with-output :off (prove event warning observation summary error) :gag-mode nil (run-events-record-failures ,(GENERATE-LOTS-OF-IDENTITY-FNS 100) :with-output (:off :all :on (error))))) (make-event (if (and (equal (@ failed-events) nil) (equal (formals 'foo100 (w state)) '(x)) (equal (formals 'foo10 (w state)) '(x))) '(value-triple :ok) (er soft 'run-events-record-failures-test "Unexpected result from run-events-record-failures"))))))
run-and-continue-if-successfulmacro
(defmacro run-and-continue-if-successful (event1 event2) `(progn (make-event (b* ((event ',EVENT1)) ,'`(:OR (WITH-OUTPUT :STACK :POP ,EVENT) (MAKE-EVENT (B* ((STATE (F-PUT-GLOBAL 'FAILED-EVENT ',EVENT STATE))) (VALUE '(VALUE-TRIPLE :FAILED))))))) (make-event (if (@ failed-event) '(value-triple :invisible) ',EVENT2))))
run-events-stop-on-failure-fnfunction
(defun run-events-stop-on-failure-fn (events) (if (atom events) '(value-triple :invisible) `(run-and-continue-if-successful ,(CAR EVENTS) ,(RUN-EVENTS-STOP-ON-FAILURE-FN (CDR EVENTS)))))
run-events-stop-on-failuremacro
(defmacro run-events-stop-on-failure (events &key (with-output '(:off :all))) `(with-output ,@WITH-OUTPUT :stack :push (progn ,'(MAKE-EVENT (B* ((STATE (F-PUT-GLOBAL 'FAILED-EVENT NIL STATE))) (VALUE '(VALUE-TRIPLE :INVISIBLE)))) ,(RUN-EVENTS-STOP-ON-FAILURE-FN EVENTS))))
encapsulate
(encapsulate nil (logic) (local (progn (make-event (if (and (equal (fgetprop 'foo 'formals :none (w state)) :none) (equal (fgetprop 'bar 'formals :none (w state)) :none) (not (formula 'not-foo nil (w state))) (not (formula 'foo-identity nil (w state)))) (value '(value-triple :ok)) (er soft 'run-events-stop-on-failure "Foo, bar, not-foo, and foo-identity should not be defined beforehand!"))) (with-output :off (prove event warning observation error) :gag-mode nil (run-events-stop-on-failure ((defun foo (x) x) (defthm not-foo (not (foo (foo x)))) (defun bar (x) y) (defthm foo-identity (equal (foo (foo x)) (foo x)))) :with-output (:off :all :on (error)))) (make-event (if (and (equal (@ failed-event) '(defthm not-foo (not (foo (foo x))))) (equal (formals 'foo (w state)) '(x)) (not (formula 'foo-identity nil (w state)))) '(value-triple :ok) (er soft 'run-events-stop-on-failure "Unexpected result"))))))
encapsulate
(encapsulate nil (logic) (local (progn (defun generate-lots-of-identity-fns (n) (declare (xargs :mode :program)) (if (zp n) nil (cons `(defun ,(INTERN-IN-PACKAGE-OF-SYMBOL (CONCATENATE 'STRING "FOO" (COERCE (EXPLODE-ATOM N 10) 'STRING)) 'FOO) (x) x) (generate-lots-of-identity-fns (1- n))))) (make-event (b* ((state (f-put-global 'my-events (generate-lots-of-identity-fns 100) state))) (value '(value-triple :invisible)))) (with-output :off (prove event warning observation summary error) :gag-mode nil (make-event `(run-events-stop-on-failure ,(@ MY-EVENTS) :with-output (:off :all :on (error))))) (make-event (if (and (equal (@ failed-event) nil) (equal (formals 'foo100 (w state)) '(x)) (equal (formals 'foo10 (w state)) '(x))) '(value-triple :ok) (er soft 'run-events-stop-on-failure-test "Unexpected result"))))))