/usr/share/acl2-7.2dfsg/books/misc/defun-plus.lisp is in acl2-books-source 7.2dfsg-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 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 | (in-package "ACL2")
;; Copyright Nathan Wetzler and David Rager.
;; ============================================================================
;; Introductions
;;
;; This file defines defun+, which is a macro for defun that allows the user to
;; specify an "output signature" as part of a function's definition. It works
;; by defining the function as if the output signature did not exist, and then
;; defining a theorem that describes the value[s] returned by calling the
;; function. The user may optionally pass in an argument :disable, which
;; indicates whether the function should be disabled after the theorem stating
;; the output type is proved.
;;
;; See the end of the file for ideas on how to further extend defun+.
;; ============================================================================
;; ============================================================================
;; The following definitions related to gathering declarations are taken from
;; the ACL2 source code. The only changes (as of August 2012) is the removal
;; of the guards and defining these functions in program mode. These changes
;; are necessary, because :output is not one of the fields allowed in an xargs
;; declaration, as tested by ACL2 function plausible-dclsp.
;; ============================================================================
(defun strip-dcls-program-mode1 (fields lst)
(declare (xargs :mode :program))
(cond ((endp lst) nil)
((member-eq (caar lst) '(type ignore ignorable))
(cond ((member-eq (caar lst) fields)
(strip-dcls-program-mode1 fields (cdr lst)))
(t (cons (car lst) (strip-dcls-program-mode1 fields (cdr lst))))))
(t
(let ((temp (strip-keyword-list fields (cdar lst))))
(cond ((null temp) (strip-dcls-program-mode1 fields (cdr lst)))
(t (cons (cons 'xargs temp)
(strip-dcls-program-mode1 fields (cdr lst)))))))))
(defun strip-dcls-program-mode (fields lst)
(declare (xargs :mode :program))
(cond ((endp lst) nil)
((stringp (car lst))
(cond ((member-eq 'comment fields)
(strip-dcls-program-mode fields (cdr lst)))
(t (cons (car lst)
(strip-dcls-program-mode fields (cdr lst))))))
(t (let ((temp (strip-dcls-program-mode1 fields (cdar lst))))
(cond ((null temp) (strip-dcls-program-mode fields (cdr lst)))
(t (cons (cons 'declare temp)
(strip-dcls-program-mode fields (cdr lst)))))))))
(defun fetch-dcl-fields-program-mode2 (field-names kwd-list acc)
(declare (xargs :mode :program))
(cond ((endp kwd-list) acc)
(t (let ((acc (fetch-dcl-fields-program-mode2 field-names
(cddr kwd-list)
acc)))
(if (member-eq (car kwd-list) field-names)
(cons (cadr kwd-list) acc)
acc)))))
(defun fetch-dcl-fields-program-mode1 (field-names lst)
(declare (xargs :mode :program))
(cond ((endp lst) nil)
((member-eq (caar lst) '(type ignore ignorable))
(if (member-eq (caar lst) field-names)
(cons (cdar lst)
(fetch-dcl-fields-program-mode1 field-names (cdr lst)))
(fetch-dcl-fields-program-mode1 field-names (cdr lst))))
(t (fetch-dcl-fields-program-mode2 field-names
(cdar lst)
(fetch-dcl-fields-program-mode1
field-names
(cdr lst))))))
(defun fetch-dcl-fields-program-mode (field-names lst)
(declare (xargs :mode :program))
(cond ((endp lst) nil)
((stringp (car lst))
(if (member-eq 'comment field-names)
(cons (car lst)
(fetch-dcl-fields-program-mode field-names (cdr lst)))
(fetch-dcl-fields-program-mode field-names (cdr lst))))
(t (append (fetch-dcl-fields-program-mode1 field-names (cdar lst))
(fetch-dcl-fields-program-mode field-names (cdr lst))))))
(defun fetch-dcl-field-program-mode (field-name lst)
(declare (xargs :mode :program))
(fetch-dcl-fields-program-mode (list field-name) lst))
;; ============================================================================
;; Some (more) helper functions for defun+
;; ============================================================================
(defun generate-output-lemma-name (name number)
(if (not number)
(intern-in-package-of-symbol
(concatenate 'string (symbol-name name)
"-OUTPUT-LEMMA")
name)
(intern-in-package-of-symbol
(concatenate 'string (symbol-name name)
"-OUTPUT-LEMMA-"
(coerce (explode-atom number 10)
'string))
name)))
(defun generate-output-lemma-single (name guards output output-hints)
`((defthm ,(generate-output-lemma-name name nil)
(implies ,guards
,output)
:hints ,output-hints)))
(defun generate-output-lemma-multiple (name guards output number)
(if (atom output)
nil
(cons `(defthm ,(generate-output-lemma-name name number)
(implies ,guards
,(car output)))
(generate-output-lemma-multiple name
guards
(cdr output)
(1+ number)))))
(defun generate-output-lemmas (name guards output output-hints)
(if (not (equal (car output) 'and))
(generate-output-lemma-single name guards output output-hints)
(generate-output-lemma-multiple name guards (cdr output) 1)))
;; ============================================================================
;; Definition of defun+
;; ============================================================================
(defmacro defun+ (name formals dcl body &key disable)
(let* ((guards (car (fetch-dcl-field-program-mode :guard (list dcl))))
(output (car (fetch-dcl-field-program-mode :output (list dcl))))
(output-hints (car (fetch-dcl-field-program-mode :output-hints (list dcl))))
(new-dcls (car (strip-dcls-program-mode '(:output) (list dcl))))
(new-dcls (car (strip-dcls-program-mode '(:output-hints) (list new-dcls)))))
`(progn
(defun ,name ,formals ,new-dcls ,body)
,@(if output
(generate-output-lemmas name guards output output-hints)
`((value-triple nil)))
,(if disable
`(in-theory (disable ,name))
'(value-triple nil)))))
;; ============================================================================
;; Some examples
;; ============================================================================
(local
(defun+ baz (x y z)
(declare (xargs :guard (and (integerp x)
(integerp y)
(integerp z))
:output (integerp (baz x y z))))
(+ x y z)))
(local
(defun+ baz (x y z)
(declare (xargs :guard (and (integerp x)
(integerp y)
(integerp z))
:output (integerp (baz x y z))
:output-hints (("Goal" :do-not-induct t))))
(+ x y z)))
(local
(defun+ faz (x y z)
(declare (xargs :guard (and (integerp x)
(integerp y)
(integerp z))
:output (integerp (faz x y z))))
(+ x y z)
:disable t))
(local
(defun+ foo (x y)
(declare (xargs :guard (and (integerp x) (integerp y))
:output (and (equal (mv-nth 0 (foo x y)) 0)
(integerp (mv-nth 1 (foo x y))))))
(mv 0 (+ x y))
:disable t))
;; ============================================================================
;; It would be nice to automatically generate lemmas about the functions. For
;; example, it might be nice to define opener lemmas that hinge off the input
;; to a recursive function being a consp. However, we think we could have a
;; more general approach to automatically generating lemmas. As such, for now,
;; we leave the use of this code disabled.
;; ============================================================================
#||
(defmacro generate-lemma-names (fn1 fn2 &optional car-cdr)
`(intern-in-package-of-symbol
(concatenate 'string
(symbol-name ,fn1)
"-IMPLIES-"
(symbol-name ,fn2)
(if ,car-cdr
(concatenate 'string "-" (symbol-name ,car-cdr))
""))
,fn1))
(defun generate-lemmas (name formals guards body)
(declare (ignore formals guards))
(case-match body
(('if ('atom x)
tbr
(and (fbr-car ('car x))
(!name ('cdr x))))
(list `(defthm ,(generate-lemma-names name fbr-car 'car)
(implies (and (,name ,x)
(consp ,x))
(,fbr-car (car ,x))))
`(defthm ,(generate-lemma-names name name 'cdr)
(implies (and (,name ,x)
(consp ,x))
(,name (cdr ,x))))))
(& nil)))
(generate-lemmas 'foo
nil
nil
'(if (atom x)
(null x)
(and (bar (car x))
(foo (cdr x)))))
(defmacro defun+ (name formals dcl body &key disable generate-lemmas)
(let* ((guards (car (fetch-dcl-field-program-mode :guard (list dcl))))
(output (car (fetch-dcl-field-program-mode :output (list dcl))))
(new-dcls (car (strip-dcls-program-mode '(:output) (list dcl)))))
`(progn
(defun ,name ,formals ,new-dcls ,body)
,@(if output
(generate-output-lemmas name guards output)
`((value-triple nil)))
,@(if generate-lemmas
(generate-lemmas name formals guards body)
`((value-triple nil)))
,(if disable
`(in-theory (disable ,name))
'(value-triple nil)))))
(defun barp (x) (declare (xargs :guard t)) (integerp x))
(defun+ foop (x)
(declare (xargs :guard t))
(if (atom x)
(null x)
(and (barp (car x))
(foop (cdr x))))
:generate-lemmas t)
||#
;; ============================================================================
;; Here are a couple more ideas on how to improve defun+.
;; Add some output to defun+ (and also suppress some of the output) that tells
;; the user the definitions of the lemmas that were produced.
;; Potentially add symbols to output lemma names so that users can quickly
;; identify when the output lemmas are being used by viewing the summary of a
;; proof attempt. We are uncertain of the consequences of having the output
;; rules automatically generated, so having this extra mechanism for flagging
;; the automatic use of these lemmas, would help us figure out whether they can
;; cause problems.
;; Come up with a way of allowing hints for the output lemmas when there is
;; more than one output lemma.
;; ============================================================================
|