/usr/share/acl2-4.3/books/make-event/dotimes.lisp is in acl2-books-source 4.3-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 | #|
Dotimes, Version 0.2
Copyright (C) 2006 by David Rager <ragerdl@cs.utexas.edu>
This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License as
published by the Free Software Foundation; either version 2 of
the License, or (at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public Lic-
ense along with this program; if not, write to the Free Soft-
ware Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
02111-1307, USA.
dotimes.lisp
This file provides a dotimes$ macro for use at the top-level. I also needed
a version of dotimes that returned error triples so that I could run events
multiple times for performance benchmarking. Dotimes$-with-error-triple
meets these requirements. The use of dotimes$-with-error-triple requires an
active ttag.
Anyone should feel to cleanup or enhance these macros.
Jared Davis, Matt Kaufmann, and Sandip Ray contributed to this book.
|#
(in-package "ACL2")
(defmacro dotimes$ (var-limit-form form &key (name 'dotimes-default-name-foo))
(declare (xargs :guard (and (true-listp var-limit-form)
(equal (length var-limit-form) 2))))
(let ((var (car var-limit-form))
(limit (cadr var-limit-form)))
`(make-event
(with-output
:off summary
(progn
(with-output
:off :all
(defun ,name (,var)
(declare (xargs :measure (acl2-count ,var)))
(if (zp ,var)
(cw "Done with dotimes~%")
(prog2$ ,form
(,name (1- ,var))))))
(value-triple (,name ,limit))
(value-triple '(value-triple :invisible)))))))
(defmacro dotimes$-with-error-triple
(var-limit-form form &key (name 'dotimes-default-name-foo))
(declare (xargs :guard (and (true-listp var-limit-form)
(equal (length var-limit-form) 2))))
(let ((var (car var-limit-form))
(limit (cadr var-limit-form)))
`(make-event
(with-output
:off summary
(progn!
(with-output
:off :all
(progn
(set-state-ok t)
(defun ,name (,var state)
(declare (xargs :measure (acl2-count ,var)
:mode :program))
(if (zp ,var)
(mv nil (cw "Done with dotimes~%") state)
(mv-let (erp val state)
,form
; I don't have a need to recognize errors right now. Someone else can feel
; free to implement such a feature if they like.
(declare (ignore erp val))
(,name (1- ,var) state))))
(set-state-ok nil)))
(,name ,limit state)
(value-triple '(value-triple :invisible)))))))
; A test:
(local
(encapsulate
()
(defun fib (x)
(declare (xargs :guard (natp x)))
(cond ((mbe :logic (or (zp x) (<= x 0))
:exec (<= x 0))
0)
((= x 1)
1)
(t
(let ((a (fib (- x 1)))
(b (fib (- x 2))))
(+ a b)))))
(dotimes$ (i 4) (time$ (fib 25)) :name dotimes-foo)))
#|
; The following example works, but I have disabled it so that people can
; include this book without needing an active ttag. Note that the use of
; dotimes$-with-error-triple does require an active ttag.
(local
(encapsulate
()
(dotimes$-with-error-triple
(i 4)
(time$ (thm (equal 3 3))))))
|#
|