← Back to branch summary

~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to books/defexec/chapter3/records/inline.lisp

  • Committer: Bazaar Package Importer
  • Author(s): Camm Maguire
  • Date: 2006-12-04 10:35:42 UTC
  • mfrom: (1.1.5 upstream) (3.1.1 etch)
  • Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
Tags: 3.1-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/defexec/chapter3/records/inline.lisp
1
 
(in-package "ACL2")
2
 
 
3
 
;; We define some macros which can be used for performing function inlining in
4
 
;; a very basic sense (in particular the function exec-trm would need to be
5
 
;; extended to support cond, case, let, and any other macros the user might
6
 
;; utilize.) The goal here is not to define a one-size-fits-all solution for
7
 
;; supporting inlining, but to instead demonstrate how inlining can be
8
 
;; performed through macros and the use of mbe, while still allowing nice
9
 
;; functional decomposition and control in the logic. Note that one potential
10
 
;; difficulty that a full-fledged :inline support would need to handle is
11
 
;; control over the mbe guard proofs which should be equal but may require some
12
 
;; guidance to ACL2 to avoid unnecessary effort (i.e. preprocessing,
13
 
;; normalization, case-splitting, etc.). Another glaring omission is support
14
 
;; for stobjs which is hindered by the still awkward handling of stobj-named
15
 
;; parameters for defmacro :(
16
 
 
17
 
(defun symbol-binary-append (x y)
18
 
  (declare (xargs :guard (and (symbolp x) (symbolp y))))
19
 
  (intern (string-append (symbol-name x) (symbol-name y)) "ACL2"))
20
 
 
21
 
(defmacro symbol-append (symb &rest symbs)
22
 
  (if (endp symbs) symb
23
 
    `(symbol-binary-append ,symb (symbol-append ,@symbs))))
24
 
 
25
 
(defmacro bind (v a r)
26
 
  `(let ((,v ,a)) ,r))
27
 
 
28
 
;; obviously, the following would need to be extended (or replaced with a
29
 
;; different mechanism altogether -- i.e. packages or function prefixes) in
30
 
;; order to be of any practical use.
31
 
(defconst *exec-trm-built-ins*
32
 
  '(the signed-byte or not integerp consp
33
 
    and if car cdr + - * < > <= >= 1+ 1- zp
34
 
    bind eq eql g s true-listp nfix
35
 
    first second third fourth))
36
 
 
37
 
(defun prefix-match (x y)
38
 
  (declare (xargs :guard (and (stringp x) (stringp y))))
39
 
  (and (> (length x) (length y))
40
 
       (equal (subseq x 0 (length y)) y)))
41
 
 
42
 
(defun stobj-access-fn (fn)
43
 
  (declare (xargs :guard (symbolp fn)))
44
 
  (let* ((str (symbol-name fn)))
45
 
    (or (prefix-match str "GET-")
46
 
        (prefix-match str "UPDATE-"))))
47
 
 
48
 
(defun exec-call (fn in-fn)
49
 
  (declare (xargs :guard t))
50
 
  (not (or (not (symbolp fn))
51
 
           (eq fn in-fn)
52
 
           (member-eq fn *exec-trm-built-ins*)
53
 
           (stobj-access-fn fn))))
54
 
  
55
 
(defun exec-fnname (fn) 
56
 
  (declare (xargs :guard (symbolp fn)))
57
 
  (symbol-append fn '$exec))
58
 
 
59
 
;; I need to drop-stobjs in the exec portion of the inlined function because
60
 
;; of the unfortunate (and silly) restriction on not using stobj names as
61
 
;; parameter names for macros (yuck!).
62
 
 
63
 
(defun is-stobj-name (arg)
64
 
  (declare (xargs :guard t))
65
 
  (and (symbolp arg)
66
 
       (prefix-match (symbol-name arg) "STOBJ$")))
67
 
 
68
 
(defun drop-stobjs (args)
69
 
  (declare (xargs :guard t))
70
 
  (cond ((atom args) ())
71
 
        ((is-stobj-name (first args))
72
 
         (drop-stobjs (rest args)))
73
 
        (t (cons (first args)
74
 
                 (drop-stobjs (rest args))))))
75
 
 
76
 
(mutual-recursion
77
 
(defun exec-trm (trm in-fn)
78
 
  (declare (xargs :guard t))
79
 
  (cond
80
 
   ((or (atom trm) (quotep trm)) trm)
81
 
   ((exec-call (first trm) in-fn)
82
 
    (cons (exec-fnname (first trm))
83
 
          (drop-stobjs (exec-args (rest trm) in-fn))))
84
 
   (t
85
 
    (cons (first trm)
86
 
          (exec-args (rest trm) in-fn)))))
87
 
 
88
 
(defun exec-args (args in-fn)
89
 
  (declare (xargs :guard t))
90
 
  (if (atom args) ()
91
 
    (cons (exec-trm (first args) in-fn)
92
 
          (exec-args (rest args) in-fn))))
93
 
)
94
 
 
95
 
(defun is-exec-decl (decl)
96
 
  (declare (xargs :guard t))
97
 
  (and (consp decl)
98
 
       (symbolp (first decl))
99
 
       (member-eq (first decl) '(type ignore))))
100
 
 
101
 
(defun parse-exec-decls (decls)
102
 
  (declare (xargs :guard (true-listp decls)))
103
 
  (cond ((endp decls) ())
104
 
        ((is-exec-decl (first decls))
105
 
         (cons (list 'declare (first decls))
106
 
               (parse-exec-decls (rest decls))))
107
 
        (t (parse-exec-decls (rest decls)))))
108
 
 
109
 
(defun collect-exec-decls (aux)
110
 
  (declare (xargs :guard (true-listp aux)))
111
 
  (cond ((endp aux) ())
112
 
        ((stringp (first aux))
113
 
         (cons (first aux)
114
 
               (collect-exec-decls (rest aux))))
115
 
        ((and (consp (first aux))
116
 
              (true-listp (first aux))
117
 
              (eq (first (first aux)) 'declare))
118
 
         (append (parse-exec-decls (rest (first aux)))
119
 
                 (collect-exec-decls (rest aux))))
120
 
        (t (collect-exec-decls (rest aux)))))
121
 
 
122
 
(defmacro defun* (fn args &rest aux)
123
 
  (declare (xargs :guard (and (symbolp fn)
124
 
                              (symbol-listp args)
125
 
                              (consp aux)
126
 
                              (true-listp aux))))
127
 
  (let* ((inline (eq (first aux) :inline))
128
 
         (aux (if inline (rest aux) aux))
129
 
         (body (car (last aux)))
130
 
         (aux (butlast aux 1))
131
 
         (exec-decls (collect-exec-decls aux))
132
 
         (exec-fn (exec-fnname fn))
133
 
         (exec-args (drop-stobjs args)))
134
 
    `(progn (defun ,fn ,args ,@aux
135
 
              (mbe :logic ,body :exec ,(exec-trm body fn)))
136
 
            (defabbrev ,exec-fn ,exec-args ,@exec-decls
137
 
              ,(if inline body (cons fn args))))))
138
 
 
139
 
;; Ok, a simple contrived test. We define a simple countdown loop using defun*
140
 
;; with certain functions inlined versus a version written with defun.
141
 
 
142
 
(defun* decr-fast (n) :inline
143
 
  (declare (xargs :guard (natp n))
144
 
           (type (signed-byte 29) n))
145
 
  (the (signed-byte 29) (1- n)))
146
 
 
147
 
(defun* zp-fast (n) :inline
148
 
  (declare (xargs :guard (natp n))
149
 
           (type (signed-byte 29) n))
150
 
  (or (not (integerp n)) (<= n 0)))
151
 
 
152
 
(defun* loop-fast (n)
153
 
  (declare (xargs :guard (natp n))
154
 
           (type (signed-byte 29) n))
155
 
  (if (zp-fast n) n (loop-fast (decr-fast n))))
156
 
 
157
 
(defun decr-slow (n)
158
 
  (declare (xargs :guard (natp n))
159
 
           (type (signed-byte 29) n))
160
 
  (the (signed-byte 29) (1- n)))
161
 
 
162
 
(defun zp-slow (n)
163
 
  (declare (xargs :guard (natp n))
164
 
           (type (signed-byte 29) n))
165
 
  (or (not (integerp n)) (<= n 0)))
166
 
 
167
 
(defun loop-slow (n)
168
 
  (declare (xargs :guard (natp n))
169
 
           (type (signed-byte 29) n))
170
 
  (if (zp-slow n) n (loop-slow (decr-slow n))))
171
 
 
172
 
;; We end up with the following execution times under Franz Lisp on Linux/x86:
173
 
;;    (time (loop-fast 200000000)) = 0.7 seconds
174
 
;;    (time (loop-slow 200000000)) = 6.0 seconds
175
 
 
176
 
;; macros from the paper defined using defun*:
177
 
 
178
 
(defmacro defun-inline (name args &rest x)
179
 
  `(defun* ,name ,args :inline ,@x))
180
 
 
181
 
(defmacro defun-exec (name args &rest x)
182
 
  `(defun* ,name ,args ,@x))
183
 
 
184
 
 
185
 
 
186
 
 
187