← 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/redefun.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/redefun.lisp
 
1
#|$ACL2s-Preamble$;
 
2
(include-book "defcode" :ttags ((defcode)))
 
3
 
 
4
(acl2::begin-book t :ttags ((defcode)));$ACL2s-Preamble$|#
 
5
 
 
6
(in-package "ACL2")
 
7
; cert_param: (non-acl2r)
 
8
 
 
9
(program)
 
10
(set-state-ok t)
 
11
 
 
12
 
 
13
(defun chk-acceptable-redefun (def ctx wrld state)
 
14
  (er-let*
 
15
   ((tuple (chk-acceptable-defuns (list def) ctx wrld state)))
 
16
   (assert$
 
17
    (equal (length tuple) 23)
 
18
    (let* ((name (car def))
 
19
           (new-wrld (nth 18 tuple))
 
20
           (old-symbol-class
 
21
            (getprop name 'symbol-class 0 'current-acl2-world wrld))
 
22
           (new-symbol-class (nth 15 tuple))
 
23
           (old-formals
 
24
            (getprop name 'formals 0 'current-acl2-world wrld))  
 
25
           (new-formals
 
26
            (getprop name 'formals 0 'current-acl2-world new-wrld))  
 
27
           (old-stobjs-in
 
28
            (getprop name 'stobjs-in 0 'current-acl2-world wrld))  
 
29
           (new-stobjs-in
 
30
            (getprop name 'stobjs-in 0 'current-acl2-world new-wrld))  
 
31
           (old-stobjs-out
 
32
            (getprop name 'stobjs-out 0 'current-acl2-world wrld))  
 
33
           (new-stobjs-out
 
34
            (getprop name 'stobjs-out 0 'current-acl2-world new-wrld)))
 
35
      (cond ((eql old-symbol-class 0)
 
36
             (er soft ctx "No existing definition: ~x0" name))
 
37
            ((nth 19 tuple) ; non-executablep
 
38
             (er soft ctx
 
39
                 "Please do not redefun a non-executable function.  The ~
 
40
                  offending definition is: ~x0."
 
41
                 def))
 
42
            ((not (eq ':program old-symbol-class))
 
43
             (er soft ctx
 
44
                 "Old definition should have defun-mode :program.  Sorry."))
 
45
            ((not (eq ':program new-symbol-class))
 
46
             (er soft ctx
 
47
                 "New definition should have defun-mode :program.  Sorry."))
 
48
            ((not (equal new-formals old-formals))
 
49
             (er soft ctx
 
50
                 "Please use the same formal parameter list when redefining. ~
 
51
                  Previous formals: ~x0"
 
52
                 old-formals))
 
53
            ((not (equal new-stobjs-in old-stobjs-in))
 
54
             (er soft ctx
 
55
                 "New definition should have the same stobjs-in.Previously, ~
 
56
                  ~x0.  Specified, ~x1."
 
57
                 old-stobjs-in new-stobjs-in))
 
58
            ((not (equal new-stobjs-out old-stobjs-out))
 
59
             (er soft ctx
 
60
                 "New definition should have the same stobjs-out.Previously, ~
 
61
                  ~x0.  Specified, ~x1."
 
62
                 old-stobjs-out new-stobjs-out))
 
63
            (t ; okay
 
64
             (value :invisible)))))))
 
65
 
 
66
 
 
67
(include-book "rewrite-code")
 
68
 
 
69
; this is a safer version of doing defun with redefinition allowed.
 
70
;
 
71
; only :program mode functions may be used here, because the intent is to
 
72
; maintain sound reasoning.
 
73
;
 
74
; lots of checks are performed and actions are taken to prevent the logic from
 
75
; being tainted by the redefinition.
 
76
; 
 
77
(defmacro redefun (name ll &rest decls-and-body)
 
78
  (declare (xargs :guard (and (symbolp name)
 
79
                              (symbol-listp ll)
 
80
                              (consp decls-and-body))))
 
81
  (let ((def (list* name ll decls-and-body)))
 
82
    `(progn+redef
 
83
      (assert-include-defun-matches-certify-defun ,name)
 
84
      (defcode
 
85
       :loop (er-progn
 
86
              (assert-no-special-raw-definition ,name)
 
87
              (chk-acceptable-redefun ',def
 
88
                                      'redefun
 
89
                                      (w state)
 
90
                                      state)
 
91
              (ensure-program-only-flag ,name)
 
92
              (defun . ,def))
 
93
       :extend
 
94
       (in-raw-mode
 
95
        (defun-*1* ,name ,ll
 
96
                   (if (f-get-global 'safe-mode *the-live-state*)
 
97
                     (throw-raw-ev-fncall (list 'program-only-er ',name
 
98
                                                (list . ,ll) 't '(nil) t))
 
99
                     (,name . ,ll))))
 
100
       :compile
 
101
       (defun . ,def)))))
 
102
 
 
103
 
 
104
; this uses redefun and our code rewrite stuff (see rewrite-code.lisp,
 
105
; especially compute-copy-defun+rewrite) to redefine a :program mode
 
106
; function in terms of its existing definition.
 
107
; 
 
108
(defmacro redefun+rewrite (name &rest rewrite-spec)
 
109
  (declare (xargs :guard (symbolp name)))
 
110
  `(make-event
 
111
    (compute-copy-defun+rewrite
 
112
     ',name ',name ',rewrite-spec 'redefun state)))
 
113
 
 
114
 
 
115
; tests and stuff
 
116
#|
 
117
(include-book
 
118
 "defcode" :ttags ((defcode)))
 
119
 
 
120
(defttag t)
 
121
 
 
122
(redefun deflabel-fn (name state doc event-form)
 
123
         (declare (ignore doc event-form))
 
124
         (value name))
 
125
 
 
126
(set-guard-checking :none)
 
127
(deflabel moo)
 
128
(deflabel moo)
 
129
|#