← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2007/dillinger-et-al/code/hacker.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2007/dillinger-et-al/code/hacker.lisp
 
1
#|$ACL2s-Preamble$;
 
2
;; hacker.lisp
 
3
;;
 
4
;; Functions for extending ACL2 in ways that are potentially unsound
 
5
;;
 
6
;; By Peter C. Dillinger with contributions by Matt Kaufmann
 
7
;;
 
8
;; Last modified: 
 
9
 
 
10
 
 
11
(ld ;; Newline to fool dependency scanner
 
12
  "hacker-pkg.lsp")
 
13
 
 
14
(begin-book);$ACL2s-Preamble$|#
 
15
 
 
16
(in-package "ACL2-HACKER")
 
17
 
 
18
(program)
 
19
(set-state-ok t)
 
20
 
 
21
;=========== some auxiliary definitions ===========
 
22
 
 
23
; the special progn! support for doing state-global bindings was changed between
 
24
; 3.2 and 3.2.1.  We define progn!-with-bindings to use the right one.
 
25
(make-event
 
26
 (if (earlier-acl2-versionp "ACL2 Version 3.2" (@ acl2-version)) ; >= 3.2.1
 
27
   (value
 
28
    '(defmacro progn!-with-bindings (bindings &rest rst)
 
29
       `(progn! :state-global-bindings ,bindings . ,rst)))
 
30
   (value
 
31
    '(defmacro progn!-with-bindings (bindings &rest rst)
 
32
       `(progn! (state-global-let* ,bindings (progn! . ,rst)))))))
 
33
 
 
34
; read a state global or return a default value (defaulting to nil) if unbound
 
35
(defmacro @opt (var &optional deflt)
 
36
  `(if (boundp-global ',var state)
 
37
     (f-get-global ',var state)
 
38
     ,deflt))
 
39
 
 
40
; like common lisp WHEN, but uses ACL2 error triples
 
41
(defmacro er-when (test form &rest more-forms)
 
42
  `(if ,test
 
43
     (er-progn ,form . ,more-forms)
 
44
     (value :invisible)))
 
45
 
 
46
; to enable definition of macros that use keyword arguments at the beginning
 
47
(defun transpose-keyword-args1 (args-rest kargs-sofar)
 
48
  (if (and (consp args-rest)
 
49
           (keywordp (car args-rest))
 
50
           (consp (cdr args-rest)))
 
51
    (transpose-keyword-args1 (cddr args-rest)
 
52
                            (list* (car args-rest)
 
53
                                   (cadr args-rest)
 
54
                                   kargs-sofar))
 
55
    (cons args-rest kargs-sofar)))
 
56
 
 
57
(defun transpose-keyword-args (args)
 
58
  (transpose-keyword-args1 args nil))
 
59
 
 
60
 
 
61
 
 
62
;=========== begin touchable stuff ===========
 
63
 
 
64
; union in the specification language of temp-untouchable-{vars,fns}
 
65
(defun union-eq-with-top (a b)
 
66
  (if (or (eq a t) (eq b t))
 
67
    t
 
68
    (union-eq a b)))
 
69
 
 
70
; used for temp-touchable specifications
 
71
(defun add-temp-touchable-aliases (spec sofar fn-p)
 
72
  (declare (xargs :guard (booleanp fn-p)))
 
73
  (if (null spec)
 
74
    sofar
 
75
    (let ((sym (if (consp spec) (car spec) spec))
 
76
          (rest (if (consp spec) (cdr spec) nil)))
 
77
      (add-temp-touchable-aliases
 
78
       rest
 
79
       (union-eq-with-top
 
80
        (cond ((eq sym :all)
 
81
               t)
 
82
              ((eq sym :initial)
 
83
               (if fn-p
 
84
                 acl2::*initial-untouchable-fns*
 
85
                 acl2::*initial-untouchable-vars*))
 
86
              (t
 
87
               (list sym)))
 
88
        sofar)
 
89
       fn-p))))
 
90
 
 
91
#|; flawed in terms of undoing
 
92
 
 
93
; defines a stack of saved untouchables
 
94
(defun push-temp-touchables (state)
 
95
  (f-put-global 'saved-temp-touchables
 
96
                (cons (cons (@ temp-touchable-vars)
 
97
                            (@ temp-touchable-fns))
 
98
                      (@opt saved-temp-touchables))
 
99
                state))
 
100
 
 
101
(defun pop-temp-touchables (state)
 
102
  (if (and (boundp-global 'saved-temp-touchables state)
 
103
           (consp (@ saved-temp-touchables)))
 
104
    (let ((result (car (@ saved-temp-touchables))))
 
105
      (pprogn (f-put-global 'saved-temp-touchables
 
106
                            (cdr (@ saved-temp-touchables))
 
107
                            state)
 
108
              (value result)))
 
109
    (er soft 'pop-temp-touchables
 
110
        "Stack of temp-touchables is empty.")))
 
111
 
 
112
(push-untouchable saved-temp-touchables nil)
 
113
 
 
114
;for export
 
115
(defmacro push+touchable (&key vars fns)
 
116
 
 
117
;;; This legacy doc string was replaced Nov. 2014 by a corresponding
 
118
;;; auto-generated defxdoc form in file dillinger-et-al-xdoc.lisp.
 
119
 
 
120
; ":Doc-Section hacker
 
121
; 
 
122
; add some fns/vars to those temporarily touchable, remembering previous setting.~/
 
123
 
 
124
; ~bv[]
 
125
; Examples:
 
126
; (push+touchable :fns :all :vars :all)  ; like push-all-touchable
 
127
; (push+touchable :fns set-w :vars :initial)
 
128
; (push+touchable :vars (foo :initial bar))
 
129
; ~ev[] ~/
 
130
; 
 
131
; This event first pushes the previous temporary touchable settings
 
132
; (functions and variables) onto a stack (stored in a global variable)
 
133
; and then adds all those that meet the specification passed in.
 
134
; 
 
135
; ~ilc[pop-touchable] reinstates the previous setting.
 
136
; 
 
137
; An active ttag is required to use this form (~l[defttag]) because it
 
138
; can render ACL2 unsound (~l[remove-untouchable]).
 
139
; ~/"
 
140
  `(progn! (push-temp-touchables state)
 
141
           (set-temp-touchable-vars
 
142
            (add-temp-touchable-aliases ',vars (@ temp-touchable-vars) nil)
 
143
            state)
 
144
           (set-temp-touchable-fns
 
145
            (add-temp-touchable-aliases ',fns (@ temp-touchable-fns) t)
 
146
            state)))
 
147
 
 
148
;for export
 
149
(defmacro push=touchable (&key vars fns)
 
150
 
 
151
;;; This legacy doc string was replaced Nov. 2014 by a corresponding
 
152
;;; auto-generated defxdoc form in file dillinger-et-al-xdoc.lisp.
 
153
 
 
154
; ":Doc-Section hacker
 
155
; 
 
156
; set which fns/vars are temporarily touchable, remembering previous setting.~/
 
157
 
 
158
; ~bv[]
 
159
; Examples:
 
160
; (push=touchable :fns :all :vars :all)  ; like push-all-touchable
 
161
; (push=touchable :fns set-w :vars :initial)
 
162
; (push=touchable :vars (foo :initial bar)) ;``:fns ()'' default
 
163
; ~ev[] ~/
 
164
; 
 
165
; This event first pushes the previous temporary touchable settings
 
166
; (functions and variables) onto a stack (stored in a global variable)
 
167
; and then sets them to the specification passed in.
 
168
; 
 
169
; ~ilc[pop-touchable] reinstates the previous setting.
 
170
; 
 
171
; An active ttag is required to use this form (~l[defttag]) because it
 
172
; can render ACL2 unsound (~l[remove-untouchable]).
 
173
; ~/"
 
174
  `(progn! (push-temp-touchables state)
 
175
           (set-temp-touchable-vars
 
176
            (add-temp-touchable-aliases ',vars nil nil)
 
177
            state)
 
178
           (set-temp-touchable-fns
 
179
            (add-temp-touchable-aliases ',fns nil t)
 
180
            state)))
 
181
 
 
182
;for export
 
183
(defmacro push-all-touchable ()
 
184
 
 
185
;;; This legacy doc string was replaced Nov. 2014 by a corresponding
 
186
;;; auto-generated defxdoc form in file dillinger-et-al-xdoc.lisp.
 
187
 
 
188
; ":Doc-Section hacker
 
189
; 
 
190
; make all fns/vars temporarily touchable, remembering previous setting.~/
 
191
 
 
192
; ~bv[]
 
193
; Usage:
 
194
; (push-all-touchable)
 
195
; ~ev[] ~/
 
196
; 
 
197
; This event first pushes the previous temporary touchable settings
 
198
; (functions and variables) onto a stack (stored in a global variable)
 
199
; and then sets them to make everything temporarily touchable.
 
200
; 
 
201
; ~ilc[pop-touchable] reinstates the previous setting.  ~ilc[push+touchable]
 
202
; and ~ilc[push=touchable] allow more more specification of what should be
 
203
; permitted.
 
204
; 
 
205
; An active ttag is required to use this form (~l[defttag]) because it
 
206
; can render ACL2 unsound (~l[remove-untouchable]).
 
207
; ~/"
 
208
  `(progn! (push-temp-touchables state)
 
209
           (set-temp-touchable-vars t state)
 
210
           (set-temp-touchable-fns t state)))
 
211
 
 
212
;for export
 
213
(defmacro pop-touchable ()
 
214
 
 
215
;;; This legacy doc string was replaced Nov. 2014 by a corresponding
 
216
;;; auto-generated defxdoc form in file dillinger-et-al-xdoc.lisp.
 
217
 
 
218
; ":Doc-Section hacker
 
219
; 
 
220
; revert the effect of a push+touchable, push=touchable, or push-all-touchable.~/
 
221
 
 
222
; ~bv[]
 
223
; Usage:
 
224
; (pop-touchable)
 
225
; ~ev[] ~/
 
226
; 
 
227
; This event pops of the stack of saved temporary touchable settings,
 
228
; reverting the effect of a ~ilc[push+touchable], ~ilc[push=touchable], or
 
229
; ~ilc[push-all-touchable].
 
230
; 
 
231
; An active ttag is required to use this form (~l[defttag]) because it
 
232
; can render ACL2 unsound (~l[remove-untouchable]).
 
233
; ~/"
 
234
  `(progn! (er-let*
 
235
        ((to-restore (pop-temp-touchables state)))
 
236
        (pprogn (set-temp-touchable-vars (car to-restore) state)
 
237
            (set-temp-touchable-fns  (cdr to-restore) state)
 
238
            (value ':invisible)))))
 
239
;|#
 
240
 
 
241
;helper for progn+touchable and progn=touchable
 
242
(defmacro progn-touchable-keyword (bangp addp form-lst &key vars fns)
 
243
  (declare (xargs :guard form-lst))
 
244
  `(progn!-with-bindings
 
245
            ((temp-touchable-vars
 
246
              (add-temp-touchable-aliases ',vars
 
247
                                          ,(if addp
 
248
                                             '(@ temp-touchable-vars)
 
249
                                             'nil)
 
250
                                          nil)
 
251
              set-temp-touchable-vars)
 
252
             (temp-touchable-fns
 
253
              (add-temp-touchable-aliases ',fns
 
254
                                          ,(if addp
 
255
                                             '(@ temp-touchable-fns)
 
256
                                             'nil)
 
257
                                          't)
 
258
              set-temp-touchable-fns))
 
259
            . ,(if bangp
 
260
                 form-lst
 
261
                 `((progn . ,form-lst)))))
 
262
 
 
263
;for export
 
264
(defmacro progn+touchable (&rest args)
 
265
 
 
266
;;; This legacy doc string was replaced Nov. 2014 by a corresponding
 
267
;;; auto-generated defxdoc form in file dillinger-et-al-xdoc.lisp.
 
268
 
 
269
; ":Doc-Section hacker
 
270
; 
 
271
; execute some events with some additional fns and/or vars made temporarily touchable.~/
 
272
 
 
273
; ~bv[]
 
274
; Examples:
 
275
; (progn+touchable :all ; same as :fns :all :vars :all
 
276
;   (defun foo ...)
 
277
;   (defun bar ...))
 
278
; (progn+touchable :vars (current-package ld-skip-proofsp)
 
279
;   ...)
 
280
; (progn+touchable :fns :all
 
281
;   ...)
 
282
; (progn+touchable :fns set-w :vars :all
 
283
;   ...)
 
284
; ~ev[] ~/
 
285
 
 
286
; This is like ~ilc[progn] except that it surrounds the events with code to
 
287
; add certain fns and/or vars to those that are temporarily touchable.
 
288
; 
 
289
; Related to ~ilc[progn=touchable].
 
290
; 
 
291
; An active ttag is required to use this form (~l[defttag]) because it
 
292
; can render ACL2 unsound (~l[remove-untouchable]).
 
293
; 
 
294
; Note that the syntax for this macro is not quite like traditional
 
295
; keyword arguments, which would come at the end of the argument list.
 
296
; ~/"
 
297
  (declare (xargs :guard (and (consp args)
 
298
                              (keywordp (car args)))))
 
299
  (if (not (member-eq (car args) '(:vars :fns)))
 
300
    `(progn-touchable-keyword nil t ,(cdr args)
 
301
                              :vars ,(car args)
 
302
                              :fns ,(car args))
 
303
    `(progn-touchable-keyword nil t . ,(transpose-keyword-args args))))
 
304
 
 
305
(defmacro progn=touchable (&rest args)
 
306
 
 
307
;;; This legacy doc string was replaced Nov. 2014 by a corresponding
 
308
;;; auto-generated defxdoc form in file dillinger-et-al-xdoc.lisp.
 
309
 
 
310
; ":Doc-Section hacker
 
311
; 
 
312
; execute some events with only the specified fns and/or vars temporarily touchable.~/
 
313
 
 
314
; ~bv[]
 
315
; Examples:
 
316
; (progn=touchable :all ; same as :fns :all :vars :all
 
317
;   (defun foo ...)
 
318
;   (defun bar ...))
 
319
; (progn=touchable :vars (current-package ld-skip-proofsp) ; :fns ()  implied
 
320
;   ...)  
 
321
; (progn=touchable :fns :all    ; :vars ()  implied
 
322
;   ...)
 
323
; (progn=touchable :fns set-w :vars :all
 
324
;   ...)
 
325
; ~ev[] ~/
 
326
 
 
327
; This is like ~ilc[progn] except that it surrounds the events with code to
 
328
; set only certain fns and/or vars as temporarily touchable.
 
329
; 
 
330
; Related to ~ilc[progn+touchable].
 
331
; 
 
332
; An active ttag is required to use this form (~l[defttag]) because it
 
333
; can render ACL2 unsound (~l[remove-untouchable]).
 
334
; 
 
335
; Note that the syntax for this macro is not quite like traditional
 
336
; keyword arguments, which would come at the end of the argument list.
 
337
; ~/"
 
338
  (declare (xargs :guard (and (consp args)
 
339
                              (keywordp (car args)))))
 
340
  (if (not (member-eq (car args) '(:vars :fns)))
 
341
    `(progn-touchable-keyword nil nil ,(cdr args)
 
342
                              :vars ,(car args)
 
343
                              :fns ,(car args))
 
344
    `(progn-touchable-keyword nil nil . ,(transpose-keyword-args args))))
 
345
 
 
346
; for export
 
347
(defmacro progn!+touchable (&rest args)
 
348
  (declare (xargs :guard (and (consp args)
 
349
                              (keywordp (car args)))))
 
350
  (if (not (member-eq (car args) '(:vars :fns)))
 
351
    `(progn-touchable-keyword t t ,(cdr args)
 
352
                              :vars ,(car args)
 
353
                              :fns ,(car args))
 
354
    `(progn-touchable-keyword t t . ,(transpose-keyword-args args))))
 
355
 
 
356
; for export
 
357
(defmacro progn!=touchable (&rest args)
 
358
  (declare (xargs :guard (and (consp args)
 
359
                              (keywordp (car args)))))
 
360
  (if (not (member-eq (car args) '(:vars :fns)))
 
361
    `(progn-touchable-keyword t nil ,(cdr args)
 
362
                              :vars ,(car args)
 
363
                              :fns ,(car args))
 
364
    `(progn-touchable-keyword t nil . ,(transpose-keyword-args args))))
 
365
 
 
366
; for export
 
367
(defmacro with-touchable (&rest args)
 
368
 
 
369
;;; This legacy doc string was replaced Nov. 2014 by a corresponding
 
370
;;; auto-generated defxdoc form in file dillinger-et-al-xdoc.lisp.
 
371
 
 
372
; ":Doc-Section hacker
 
373
; 
 
374
; execute some events but with certain untouchables removed.
 
375
; ~/~/
 
376
; Same as ~c[progn+touchable]. ~l[progn+touchable]."
 
377
  `(progn+touchable . ,args))
 
378
 
 
379
 
 
380
 
 
381
;=========== begin redef stuff ===========
 
382
 
 
383
(defun put-ld-redefinition-action (v state)
 
384
  (mv-let (erp v state)
 
385
      (set-ld-redefinition-action v state)
 
386
      (declare (ignore v))
 
387
      (prog2$
 
388
       (and erp
 
389
        (hard-error 'put-ld-redefinition-action
 
390
                "~x0 returned an error."
 
391
                '((#\0 . set-ld-redefinition-action))))
 
392
       state)))
 
393
 
 
394
(defun expand-redef-action-aliases (spec)
 
395
  (cond ((equal spec t)
 
396
         '(:doit! . :overwrite))
 
397
        (t
 
398
         spec)))
 
399
 
 
400
(defmacro progn+redef-action (spec &rest form-lst)
 
401
  (declare (xargs :guard form-lst))
 
402
  `(progn!-with-bindings
 
403
    ((ld-redefinition-action
 
404
      ,(if (eq spec :unspecified)
 
405
         '(@ ld-redefinition-action)
 
406
         `(expand-redef-action-aliases ',spec))
 
407
      put-ld-redefinition-action))
 
408
    (progn . ,form-lst)))
 
409
 
 
410
; for export
 
411
(defmacro progn+redef (&rest args)
 
412
 
 
413
;;; This legacy doc string was replaced Nov. 2014 by a corresponding
 
414
;;; auto-generated defxdoc form in file dillinger-et-al-xdoc.lisp.
 
415
 
 
416
; ":Doc-Section hacker
 
417
; 
 
418
; execute some events but with redefinition enabled.~/
 
419
 
 
420
; ~bv[]
 
421
; Examples (all equivalent):
 
422
; (progn+redef
 
423
;   (defun foo ...)
 
424
;   (defun bar ...))
 
425
; (progn+redef :action t 
 
426
;   ...)
 
427
; (progn+redef :action (:doit! . :overwrite)
 
428
;   ...)
 
429
; ~ev[] ~/
 
430
; 
 
431
; This is like ~ilc[progn] except that it sets the
 
432
; ~ilc[ld-redefinition-action] as (optionally) specified for the
 
433
; given events.  An ~c[:action] of ~c[t] is a shortcut for
 
434
; ~c[(:doit! . :overwrite)].  ~ilc[make-event] is used to save and restore
 
435
; the old value of ~ilc[ld-redefinition-action].
 
436
; 
 
437
; An active ttag is required to use this form (~l[defttag]).
 
438
; 
 
439
; Note that the syntax for this macro is not quite like traditional
 
440
; keyword arguments, which would come at the end of the argument list.
 
441
; ~/"
 
442
  (declare (xargs :guard (consp args)))
 
443
  (if (and (equal (car args) :action)
 
444
           (consp (cdr args)))
 
445
    `(progn+redef-action ,(cadr args) . ,(cddr args))
 
446
    `(progn+redef-action t . ,args)))
 
447
 
 
448
; for export
 
449
(defmacro with-redef-allowed (&rest args)
 
450
 
 
451
;;; This legacy doc string was replaced Nov. 2014 by a corresponding
 
452
;;; auto-generated defxdoc form in file dillinger-et-al-xdoc.lisp.
 
453
 
 
454
; ":Doc-Section hacker
 
455
; 
 
456
; execute some events but with redefinition enabled.
 
457
; ~/~/
 
458
; Same as ~c[progn+redef]. ~l[progn+redef]."
 
459
  `(progn+redef . ,args))
 
460
 
 
461
; for export
 
462
; this is a wart from an older version of hacker.lisp
 
463
(defmacro acl2::temporary-redef (&rest forms)
 
464
  (declare (ignore forms))
 
465
  (hard-error 'acl2::temporary-redef "Old implementation of ~x0 was flawed.  Adapt solution to use ~x1 (See :DOC ~x1)."
 
466
              '((#\0 . acl2::temporary-redef)
 
467
                (#\1 . progn+redef))))
 
468
 
 
469
 
 
470
 
 
471
;=========== begin raw mode stuff ===========
 
472
 
 
473
; for export
 
474
(defmacro in-raw-mode (&rest form-lst)
 
475
 
 
476
;;; This legacy doc string was replaced Nov. 2014 by a corresponding
 
477
;;; auto-generated defxdoc form in file dillinger-et-al-xdoc.lisp.
 
478
 
 
479
; ":Doc-Section hacker
 
480
; 
 
481
; embed some raw lisp code as an event.~/
 
482
 
 
483
; ~bv[]
 
484
; Example Form:
 
485
; (in-raw-mode
 
486
;   (format t \"Preparing to load file...~~%\")
 
487
;   (load \"my-file.lisp\"))~/
 
488
 
 
489
; General Form:
 
490
; (in-raw-mode form1 form2 ... formk)
 
491
; ~ev[]
 
492
; where each ~c[formi] is processed as though all the forms are preceded by
 
493
; ~c[:]~ilc[set-raw-mode]~c[ t].  Thus, the forms need not be ~il[events]; they
 
494
; need not even be legal ACL2 forms.  ~l[set-raw-mode] for a discussion of the
 
495
; so-called ``raw mode'' under which the forms are evaluated ~-[] unless raw
 
496
; mode is disabled by one of the forms, for example, ~c[(set-raw-mode nil)], in
 
497
; which case evaluation resumes in non-raw mode.
 
498
 
 
499
; WARNING: Thus, an ~c[in-raw-mode] form is potentially very dangerous!  For
 
500
; example, you can use it to call the Common Lisp ~c[load] function to load
 
501
; arbitrary Common Lisp code, perhaps even overwriting definitions of ACL2
 
502
; system functions!  Thus, as with ~ilc[set-raw-mode], ~ilc[in-raw-mode] may
 
503
; not be evaluated unless there is an active trust tag in effect.  ~l[defttag].
 
504
 
 
505
; Note that the normal undoing mechanism (~pl[ubt]) is not supported when raw
 
506
; mode is used.
 
507
; ~/"
 
508
  `(progn! (with-output :off observation (set-raw-mode-on state))
 
509
           (progn
 
510
             ,@form-lst
 
511
             nil)
 
512
           ;;acl2-raw-mode-p is restored by progn!-fn
 
513
           ))
 
514
 
 
515
; for export
 
516
(defmacro with-raw-mode (&rest args)
 
517
 
 
518
;;; This legacy doc string was replaced Nov. 2014 by a corresponding
 
519
;;; auto-generated defxdoc form in file dillinger-et-al-xdoc.lisp.
 
520
 
 
521
; ":Doc-Section hacker
 
522
; 
 
523
; embed some raw lisp code as an event.
 
524
; ~/~/
 
525
; Same as ~c[in-raw-mode]. ~l[in-raw-mode]."
 
526
  `(in-raw-mode . ,args))
 
527
 
 
528
 
 
529
;=========== begin program-only stuff ===========
 
530
 
 
531
; for export
 
532
(defmacro ensure-program-only-flag (&rest fn-lst)
 
533
 
 
534
;;; This legacy doc string was replaced Nov. 2014 by a corresponding
 
535
;;; auto-generated defxdoc form in file dillinger-et-al-xdoc.lisp.
 
536
 
 
537
; ":Doc-Section hacker
 
538
; 
 
539
; ensure that given function names remain in :PROGRAM mode.~/
 
540
 
 
541
; ~bv[]
 
542
; Example Form:
 
543
; (ensure-program-only-flag my-fn your-fn)~/
 
544
 
 
545
; General Form:
 
546
; (ensure-program-only-flag fn1 fn2 ... fnk)
 
547
; ~ev[]
 
548
; where each ~c[fni] is a literal symbol which should have a ~ilc[program] mode
 
549
; definition. Each ~c[fni] not already flagged as \"program only\" is flagged
 
550
; as such.  This prevents it from being migrated to ~ilc[logic] mode or being 
 
551
; used in a macro.
 
552
; 
 
553
; This is a pseudo-event, meaning it can be used in an event context but does
 
554
; not (ever) change the world.
 
555
; 
 
556
; Note that the normal undoing mechanism (~pl[ubt]) does not undo the effects
 
557
; of this pseudo-event.
 
558
; ~/"
 
559
  (declare (xargs :guard (and fn-lst
 
560
                              (symbol-listp fn-lst))))
 
561
  `(progn!=touchable :vars program-fns-with-raw-code
 
562
     (assign program-fns-with-raw-code
 
563
       (union-eq (@ program-fns-with-raw-code) ',fn-lst))))
 
564
 
 
565
; test whether a function is in :PROGRAM mode
 
566
(defun program-mode-p (fn wrld)
 
567
  (eq ':program
 
568
      (getprop fn 'symbol-class nil 'current-acl2-world wrld)))
 
569
 
 
570
; test whether all functions in a list are in :PROGRAM mode
 
571
(defun program-mode-p-lst (fn-lst wrld)
 
572
  (or (endp fn-lst)
 
573
      (and (program-mode-p     (car fn-lst) wrld)
 
574
           (program-mode-p-lst (cdr fn-lst) wrld))))
 
575
 
 
576
; for export
 
577
(defmacro assert-program-mode (&rest fn-lst)
 
578
 
 
579
;;; This legacy doc string was replaced Nov. 2014 by a corresponding
 
580
;;; auto-generated defxdoc form in file dillinger-et-al-xdoc.lisp.
 
581
 
 
582
; ":Doc-Section hacker
 
583
; 
 
584
; assert that given symbols name :PROGRAM mode functions.~/
 
585
 
 
586
; ~bv[]
 
587
; Example Form:
 
588
; (assert-program-mode my-fn your-fn)~/
 
589
 
 
590
; General Form:
 
591
; (assert-program-mode fn1 fn2 ... fnk)
 
592
; ~ev[]
 
593
; where each ~c[fni] is a literal symbol which should have a ~ilc[program] mode
 
594
; definition. An error is raised if any ~c[fni] is not a program mode function.
 
595
; 
 
596
; This is a pseudo-event, meaning it can be used in an event context but does
 
597
; not (ever) change the world.
 
598
; ~/"
 
599
  (declare (xargs :guard (and fn-lst
 
600
                              (symbol-listp fn-lst))))
 
601
  `(assert-event
 
602
    (program-mode-p-lst ',fn-lst (w state))
 
603
    :msg (msg "Assertion failed.  At least one not :program mode:~%~x0"
 
604
              ',fn-lst)
 
605
    :on-skip-proofs t))
 
606
 
 
607
; for export
 
608
(defmacro ensure-program-only (&rest fn-lst)
 
609
 
 
610
;;; This legacy doc string was replaced Nov. 2014 by a corresponding
 
611
;;; auto-generated defxdoc form in file dillinger-et-al-xdoc.lisp.
 
612
 
 
613
; ":Doc-Section hacker
 
614
; 
 
615
; ensure that named functions are and remain in :PROGRAM mode.~/
 
616
 
 
617
; ~bv[]
 
618
; Example Form:
 
619
; (ensure-program-only my-fn your-fn)~/
 
620
 
 
621
; General Form:
 
622
; (ensure-program-only fn1 fn2 ... fnk)
 
623
; ~ev[]
 
624
; where each ~c[fni] is a literal symbol which should have a ~ilc[program] mode
 
625
; definition. An error is raised if any ~c[fni] is not a program mode function.
 
626
; Also, each ~c[fni] not already flagged as \"program only\" is flagged
 
627
; as such.  This prevents it from being migrated to ~ilc[logic] mode or being 
 
628
; used in a macro.
 
629
; 
 
630
; This is actually a combination of ~ilc[assert-program-mode] and
 
631
; ~ilc[ensure-program-only-flag].
 
632
; 
 
633
; This is a pseudo-event, meaning it can be used in an event context but does
 
634
; not (ever) change the world.
 
635
; 
 
636
; Note that the normal undoing mechanism (~pl[ubt]) does not undo the effects
 
637
; of this pseudo-event.
 
638
; ~/"
 
639
  (declare (xargs :guard (and fn-lst
 
640
                              (symbol-listp fn-lst))))
 
641
  `(progn (assert-program-mode . ,fn-lst)
 
642
          (ensure-program-only-flag . ,fn-lst)))
 
643
 
 
644
 
 
645
 
 
646
;=========== begin special-raw-definition stuff ===========
 
647
 
 
648
; Here we introduce the notion of a "special raw definition",
 
649
; which is somewhat related to the notion of "program only" but
 
650
; importantly different.  The intended difference is this:
 
651
; - A function should be "program only" if bad things could happen as
 
652
;   a result of it migrating to logic mode (with verify-termination)
 
653
;   or by use in macro expansion.
 
654
; - A function should be considered to have a "special raw definition"
 
655
;   if bad things could happen as a result of replacing its raw
 
656
;   definition with the raw counterpart of its "loop" definition.
 
657
;TODO: more
 
658
 
 
659
(defconst *bootstrap-special-raw-definitions*
 
660
  '(
 
661
    ;;-- from axioms.lisp --
 
662
    ;;len         #|not special, just fast|#
 
663
    ;;strip-cars  #|not special, just fast|#
 
664
    ;;strip-cdrs  #|not special, just fast|#
 
665
    acl2::complex-rationalp
 
666
    acl2::must-be-equal
 
667
    acl2::zp
 
668
    acl2::zip
 
669
    acl2::prog2$
 
670
    acl2::time$
 
671
    acl2::hard-error
 
672
    acl2::intern-in-package-of-symbol
 
673
    acl2::pkg-witness
 
674
    acl2::with-output
 
675
    acl2::value-triple-fn
 
676
    acl2::value-triple
 
677
    acl2::pprogn
 
678
    acl2::acl2-unwind-protect
 
679
    acl2::defund
 
680
    acl2::plist-worldp
 
681
    acl2::getprop-default
 
682
    acl2::fgetprop
 
683
    acl2::sgetprop
 
684
    acl2::getprops
 
685
    acl2::has-propsp
 
686
    acl2::extend-world
 
687
    acl2::retract-world
 
688
    acl2::array-1p
 
689
    acl2::array-2pz
 
690
    acl2::header
 
691
    acl2::aref1
 
692
    acl2::compress1
 
693
    acl2::aset1
 
694
    acl2::aref2
 
695
    acl2::compress2
 
696
    acl2::aset2
 
697
    acl2::flush-compress
 
698
    acl2::state-p1
 
699
    acl2::global-table-cars1
 
700
    acl2::boundp-global1
 
701
    acl2::fboundp-global
 
702
    acl2::makunbound-global
 
703
    acl2::get-global
 
704
    acl2::f-get-global
 
705
    acl2::put-global
 
706
    acl2::f-put-global
 
707
    acl2::zpf
 
708
    acl2::open-input-channel-p1
 
709
    acl2::open-output-channel-p1
 
710
    acl2::princ$
 
711
    acl2::write-byte$
 
712
    acl2::print-object$-ser ; Matt K. change shortly after v4-3
 
713
    acl2::open-input-channel
 
714
    acl2::close-input-channel
 
715
    acl2::open-output-channel
 
716
    acl2::close-output-channel
 
717
    acl2::read-char$
 
718
    acl2::peek-char$
 
719
    acl2::read-byte$
 
720
    acl2::read-object
 
721
    acl2::prin1-with-slashes
 
722
    acl2::may-need-slashes
 
723
    acl2::t-stack-length1
 
724
    acl2::extend-t-stack
 
725
    acl2::shrink-t-stack
 
726
    acl2::aref-t-stack
 
727
    acl2::aset-t-stack
 
728
    acl2::32-bit-integer-stack-length1
 
729
    acl2::extend-32-bit-integer-stack
 
730
    acl2::shrink-32-bit-integer-stack
 
731
    acl2::aref-32-bit-integer-stack
 
732
    acl2::aset-32-bit-integer-stack
 
733
    acl2::f-big-clock-negative-p
 
734
    acl2::f-decrement-big-clock
 
735
    acl2::big-clock-negative-p
 
736
    acl2::decrement-big-clock
 
737
    acl2::list-all-package-names
 
738
    acl2::user-stobj-alist
 
739
    acl2::update-user-stobj-alist
 
740
    acl2::read-idate
 
741
    acl2::read-run-time
 
742
    acl2::read-acl2-oracle
 
743
    acl2::getenv$
 
744
    acl2::setenv$
 
745
    acl2::prin1$
 
746
    acl2::the-mv
 
747
    acl2::set-enforce-redundancy
 
748
    acl2::set-verify-guards-eagerness
 
749
    acl2::set-compile-fns
 
750
    acl2::set-measure-function
 
751
    acl2::set-well-founded-relation
 
752
    acl2::logic
 
753
    acl2::program
 
754
    acl2::set-bogus-mutual-recursion-ok
 
755
    acl2::set-irrelevant-formals-ok
 
756
    acl2::set-ignore-ok
 
757
    acl2::set-inhibit-warnings
 
758
    acl2::set-inhibit-output-lst
 
759
    acl2::set-state-ok
 
760
    acl2::set-let*-abstractionp
 
761
    acl2::set-backchain-limit
 
762
    acl2::set-default-backchain-limit
 
763
    acl2::set-rewrite-stack-limit
 
764
    acl2::set-case-split-limitations
 
765
    acl2::set-match-free-default
 
766
    acl2::add-match-free-override
 
767
    acl2::add-include-book-dir
 
768
    acl2::delete-include-book-dir
 
769
    acl2::set-non-linearp
 
770
    acl2::defttag
 
771
    acl2::set-default-hints!
 
772
    acl2::add-default-hints!
 
773
    acl2::remove-default-hints!
 
774
    acl2::with-prover-time-limit
 
775
    acl2::catch-time-limit4
 
776
    acl2::time-limit4-reached-p
 
777
    acl2::wormhole1
 
778
    acl2::wormhole-p
 
779
    acl2::abort!
 
780
    acl2::er
 
781
    acl2::mfc-clause
 
782
    acl2::mfc-rdepth
 
783
    acl2::mfc-type-alist
 
784
    acl2::mfc-ancestors
 
785
    acl2::bad-atom<=
 
786
    acl2::alphorder
 
787
    
 
788
    ;;-- from translate.lisp --
 
789
    acl2::latch-stobjs1
 
790
    acl2::big-n
 
791
    acl2::decrement-big-n
 
792
    acl2::zp-big-n
 
793
    acl2::w-of-any-state
 
794
    acl2::ev-fncall-rec
 
795
    acl2::ev-rec
 
796
    acl2::ev-rec-acl2-unwind-protect
 
797
    acl2::ev-fncall
 
798
    acl2::ev
 
799
    acl2::ev-lst
 
800
    acl2::ev-fncall-w
 
801
    acl2::untranslate
 
802
    acl2::untranslate-lst
 
803
    acl2::ev-w
 
804
    acl2::ev-w-lst
 
805
    acl2::user-stobj-alist-safe
 
806
    
 
807
    ;;-- from history-management.lisp --
 
808
    acl2::start-proof-tree
 
809
    acl2::initialize-summary-accumulators
 
810
    acl2::print-summary
 
811
    acl2::set-w
 
812
    acl2::longest-common-tail-length-rec
 
813
    acl2::chk-virgin
 
814
    
 
815
    ;;-- from other-events.lisp --
 
816
    in-package
 
817
    defpkg
 
818
    defchoose
 
819
    defun
 
820
    defuns
 
821
    verify-termination
 
822
    verify-guards
 
823
    defmacro
 
824
    defconst
 
825
    defstobj
 
826
    defthm
 
827
    defaxiom
 
828
    deflabel
 
829
    defdoc
 
830
    deftheory
 
831
    in-theory
 
832
    in-arithmetic-theory
 
833
    push-untouchable
 
834
    reset-prehistory
 
835
    set-body
 
836
    table
 
837
    progn
 
838
    encapsulate
 
839
    include-book
 
840
    local
 
841
    
 
842
    acl2::chk-package-reincarnation-import-restrictions
 
843
    acl2::theory-invariant
 
844
    acl2::acl2-raw-eval
 
845
    acl2::protected-eval-with-proofs
 
846
    acl2::include-book-fn
 
847
    acl2::write-expansion-file
 
848
    acl2::certify-book-fn
 
849
    acl2::defstobj-field-fns-raw-defs
 
850
    acl2::open-trace-file-fn
 
851
    acl2::close-trace-file-fn
 
852
    acl2::with-error-trace-fn
 
853
    acl2::trace$-fn-general
 
854
    acl2::trace$-fn-simple
 
855
    acl2::untrace$-fn
 
856
    acl2::break-on-error-fn
 
857
    
 
858
    ;;-- from ld.lisp --
 
859
    acl2::ld-print-results
 
860
    acl2::print-newline-for-time$
 
861
    acl2::good-bye-fn
 
862
    acl2::ld-loop
 
863
    acl2::ld-fn-body
 
864
    acl2::ld-fn
 
865
    acl2::compile-function
 
866
    acl2::comp-fn
 
867
    acl2::comp
 
868
    acl2::break$
 
869
    acl2::set-debugger-enable-fn
 
870
    acl2::mfc-ts
 
871
    acl2::mfc-rw
 
872
    acl2::mfc-rw+
 
873
    acl2::mfc-relieve-hyp
 
874
    acl2::mfc-ap
 
875
    acl2::save-exec
 
876
    
 
877
    ))
 
878
 
 
879
#|| Removed by Matt K. after ACL2 Version 3.6.1 in favor of the defmacro just
 
880
    below,  because make-event expansion does not take place during (early)
 
881
    loading of compiled files.
 
882
(make-event ; used here like progn! without a ttag
 
883
 (er-progn
 
884
  (if (member-eq 'has-special-raw-definition
 
885
                 (global-val 'untouchable-vars (w state)))
 
886
    (value nil) ; assume we're already good
 
887
    (assign has-special-raw-definition
 
888
      (union-eq (@opt has-special-raw-definition)
 
889
                *bootstrap-special-raw-definitions*)))
 
890
  (value '(value-triple 'has-special-raw-definition)))
 
891
 :check-expansion t)
 
892
||#
 
893
 
 
894
(defmacro update-has-special-raw-definition (fn-lst)
 
895
  `(pprogn (if (boundp-global 'has-special-raw-definition state)
 
896
               state
 
897
             (f-put-global 'has-special-raw-definition
 
898
                           *bootstrap-special-raw-definitions*
 
899
                           state))
 
900
           (assign has-special-raw-definition
 
901
                   (union-eq (@ has-special-raw-definition)
 
902
                             ,fn-lst))))
 
903
 
 
904
(push-untouchable has-special-raw-definition nil)
 
905
 
 
906
; for export
 
907
(defmacro ensure-special-raw-definition-flag (&rest fn-lst)
 
908
 
 
909
;;; This legacy doc string was replaced Nov. 2014 by a corresponding
 
910
;;; auto-generated defxdoc form in file dillinger-et-al-xdoc.lisp.
 
911
 
 
912
; ":Doc-Section hacker
 
913
; 
 
914
; ensure that named functions are flagged as having special raw definitions.~/
 
915
 
 
916
; ~bv[]
 
917
; Example Form:
 
918
; (ensure-special-raw-definition-flag my-fn your-fn)~/
 
919
 
 
920
; General Form:
 
921
; (ensure-special-raw-definition-flag fn1 fn2 ... fnk)
 
922
; ~ev[]
 
923
; where each ~c[fni] is a literal symbol which should have a function
 
924
; definition. Each ~c[fni] not already flagged as having a special raw
 
925
; definition is flagged as such.  This idicates to interested parties that
 
926
; the \"loop\" definition of the function doesn't fully characterize the
 
927
; effects it has in raw lisp.
 
928
; 
 
929
; This is a pseudo-event, meaning it can be used in an event context but does
 
930
; not (ever) change the world.
 
931
; 
 
932
; Note that the normal undoing mechanism (~pl[ubt]) does not undo the effects
 
933
; of this pseudo-event.
 
934
; ~/"
 
935
  (declare (xargs :guard (and fn-lst
 
936
                              (symbol-listp fn-lst))))
 
937
  `(progn!=touchable :vars has-special-raw-definition
 
938
     (update-has-special-raw-definition ',fn-lst)))
 
939
 
 
940
; for export
 
941
(defmacro assert-no-special-raw-definition (&rest fn-lst)
 
942
 
 
943
;;; This legacy doc string was replaced Nov. 2014 by a corresponding
 
944
;;; auto-generated defxdoc form in file dillinger-et-al-xdoc.lisp.
 
945
 
 
946
; ":Doc-Section hacker
 
947
; 
 
948
; assert that given symbols do not have a special raw function definition.~/
 
949
 
 
950
; ~bv[]
 
951
; Example Form:
 
952
; (assert-no-special-raw-definition my-fn your-fn)~/
 
953
 
 
954
; General Form:
 
955
; (assert-no-special-raw-definition fn1 fn2 ... fnk)
 
956
; ~ev[]
 
957
; where each ~c[fni] is a literal symbol.  An error is raised if any ~c[fni]
 
958
; is is flagged as having a special raw definition.
 
959
; ~l[ensure-special-raw-definition-flag].
 
960
; 
 
961
; This is a pseudo-event, meaning it can be used in an event context but does
 
962
; not (ever) change the world.
 
963
; ~/"
 
964
  (declare (xargs :guard (and fn-lst
 
965
                              (symbol-listp fn-lst))))
 
966
  `(assert-event
 
967
    (not (intersectp-eq (@opt has-special-raw-definition)
 
968
                        ',fn-lst))
 
969
    :msg (msg "Assertion failed.  Flagged as having special raw definition:~%~x0"
 
970
              (intersection-eq (@opt has-special-raw-definition)
 
971
                               ',fn-lst))
 
972
    :on-skip-proofs t))
 
973
 
 
974
 
 
975
 
 
976
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
977
; modify-raw-defun-permanent
 
978
;
 
979
; for permanently installing some changes (supporting defcode)
 
980
;
 
981
 
 
982
; for export
 
983
(defmacro modify-raw-defun-permanent
 
984
  (name name-for-old ll &rest decls-and-body)
 
985
  (declare (xargs :guard (and (symbolp name)
 
986
                              (symbolp name-for-old)
 
987
                              (symbol-listp ll)
 
988
                              (consp decls-and-body))))
 
989
  `(progn
 
990
    (in-raw-mode
 
991
     (unless (fboundp ',name-for-old)
 
992
             ; if the name-for-old already has a definition, we don't override
 
993
             ; it. this provides idempotency for modify-raw-defun-permanent
 
994
             ; but means this code doesn't know the first time whether
 
995
             ; name-for-old is fresh/unused.
 
996
             (setf (symbol-function ',name-for-old)
 
997
                   (symbol-function ',name)))
 
998
     (defun ,name ,ll
 
999
       ,@ (and ll `((declare (ignorable . ,ll))))
 
1000
       . ,decls-and-body))
 
1001
    (ensure-special-raw-definition-flag ,name)))
 
1002
 
 
1003
 
 
1004
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
1005
; deflabels
 
1006
;
 
1007
; for stubbing out ACL2 names
 
1008
;
 
1009
 
 
1010
(defun build-deflabels (names)
 
1011
  (if (endp names)
 
1012
    nil
 
1013
    (cons (list 'deflabel (car names))
 
1014
          (build-deflabels (cdr names)))))
 
1015
 
 
1016
; for export
 
1017
(defmacro deflabels (&rest names)
 
1018
  `(progn
 
1019
     (with-output :off summary
 
1020
                  (progn . ,(build-deflabels names)))
 
1021
     (value-triple ',names)))
 
1022
 
 
1023
 
 
1024
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
1025
; allow other ttags
 
1026
;
 
1027
; this should only be used in subsuming hacker stuff, like so:
 
1028
;
 
1029
#|
 
1030
(include-book
 
1031
 "hacker/hacker")
 
1032
(progn+all-ttags-allowed
 
1033
 (include-book
 
1034
  "hacker/all" :ttags ((defcode) (table-guard))))
 
1035
(subsume-ttags-since-defttag) ; see subsumption.lisp
 
1036
|#
 
1037
;
 
1038
; this is a work-around for subsuming before progn+subsume-ttags is available.
 
1039
;
 
1040
 
 
1041
; for export
 
1042
(defmacro progn+all-ttags-allowed (&rest form-lst)
 
1043
  `(progn!-with-bindings
 
1044
    ((temp-touchable-vars (if (eq (@ temp-touchable-vars) t)
 
1045
                            t
 
1046
                            (cons 'acl2::ttags-allowed (@ temp-touchable-vars)))
 
1047
                          set-temp-touchable-vars))
 
1048
    (progn!-with-bindings
 
1049
     ((acl2::ttags-allowed :all))
 
1050
     (progn!-with-bindings
 
1051
      ((temp-touchable-vars (if (eq (@ temp-touchable-vars) t)
 
1052
                              t
 
1053
                              (cdr (@ temp-touchable-vars)))
 
1054
                            set-temp-touchable-vars))
 
1055
      (progn . ,form-lst)))))
 
1056
 
 
1057
 
 
1058
#|; some tests
 
1059
(defttag test1)
 
1060
(progn+allow-ttags
 
1061
 :all
 
1062
 (defttag test2)
 
1063
 (progn+touchable :all
 
1064
                  (defun foo (x) (1+ x)))
 
1065
 (progn! (cw "Hi!~%")))
 
1066
(progn+allow-ttags
 
1067
 nil
 
1068
 (defttag test3)
 
1069
 (progn+touchable :all
 
1070
                  (defun foo (x) (1+ x)))
 
1071
 (progn! (cw "Hi!~%")))
 
1072
;|#
 
1073
 
 
1074
 
 
1075
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
1076
; ttag-skip-proofs
 
1077
;
 
1078
; uses a ttag to skip proofs without the ordinary record that
 
1079
; proofs were skipped.
 
1080
;
 
1081
 
 
1082
(defun put-ld-skip-proofsp (v state)
 
1083
  (mv-let (erp v state)
 
1084
      (set-ld-skip-proofsp v state)
 
1085
      (declare (ignore v))
 
1086
      (prog2$
 
1087
       (and erp
 
1088
        (hard-error 'set-ld-skip-proofsp
 
1089
                "~x0 returned an error."
 
1090
                '((#\0 . set-ld-skip-proofsp))))
 
1091
       state)))
 
1092
 
 
1093
; for export
 
1094
(defmacro ttag-skip-proofs (x)
 
1095
  `(progn!-with-bindings
 
1096
    ((ld-skip-proofsp 'include-book put-ld-skip-proofsp))
 
1097
    (progn ,x)))
 
1098
 
 
1099
; for export
 
1100
(defmacro progn+ttag-skip-proofs (&rest args)
 
1101
  `(progn!-with-bindings
 
1102
    ((ld-skip-proofsp 'include-book put-ld-skip-proofsp))
 
1103
    (progn . ,args)))
 
1104