← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/projects/sidekick/demo/demo.lsp

  • 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/projects/sidekick/demo/demo.lsp
 
1
; ACL2 Sidekick
 
2
; Copyright (C) 2014 Kookamara LLC
 
3
;
 
4
; Contact:
 
5
;
 
6
;   Kookamara LLC
 
7
;   11410 Windermere Meadows
 
8
;   Austin, TX 78759, USA
 
9
;   http://www.kookamara.com/
 
10
;
 
11
; License: (An MIT/X11-style license)
 
12
;
 
13
;   Permission is hereby granted, free of charge, to any person obtaining a
 
14
;   copy of this software and associated documentation files (the "Software"),
 
15
;   to deal in the Software without restriction, including without limitation
 
16
;   the rights to use, copy, modify, merge, publish, distribute, sublicense,
 
17
;   and/or sell copies of the Software, and to permit persons to whom the
 
18
;   Software is furnished to do so, subject to the following conditions:
 
19
;
 
20
;   The above copyright notice and this permission notice shall be included in
 
21
;   all copies or substantial portions of the Software.
 
22
;
 
23
;   THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 
24
;   IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 
25
;   FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 
26
;   AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 
27
;   LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
 
28
;   FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
 
29
;   DEALINGS IN THE SOFTWARE.
 
30
;
 
31
; Original author: Jared Davis <jared@kookamara.com>
 
32
 
 
33
(in-package "ACL2")
 
34
 
 
35
(verify (implies (and (natp x)
 
36
                      (consp y)
 
37
                      (integerp z)
 
38
                      (<= x y)
 
39
                      (< z (expt 2 k)))
 
40
                 (equal (append x y)
 
41
                        (revappend z (floor k n)))))
 
42
 
 
43
; Note: the acl2-customization.lsp file in this directory loads the sidekick
 
44
; book.  When you start ACL2 in this directory, you should see a message such
 
45
; as:
 
46
;
 
47
; ----------------------------------------------------------------
 
48
;
 
49
;           Sidekick started, see http://localhost:9000/
 
50
;
 
51
; ----------------------------------------------------------------
 
52
;
 
53
; To try out the Sidekick, point your web browser to that address.  Some things
 
54
; to try:
 
55
;
 
56
;   - Go to the Session page.  Run through these events interactively, and see
 
57
;     how it follows along with what you're doing.
 
58
;
 
59
;   - Interactively run ``:show append''.  It should bring up the lookup page
 
60
;     with documentation, properties, etc.
 
61
;
 
62
;   - Try something like (include-book "std/top" :dir :system) and then take
 
63
;     a look at the :lint command.  You can get there by clicking or by typing
 
64
;     :lint.
 
65
;
 
66
; More to come later.
 
67
 
 
68
 
 
69
; This is just to test out the session viewer color stuff
 
70
 
 
71
(defun app (x y)
 
72
  (if (atom x)
 
73
      y
 
74
    (cons (car x)
 
75
          (app (cdr x) y))))
 
76
 
 
77
(defun app2 (x y)
 
78
  (declare (xargs :guard t))
 
79
  (if (atom x)
 
80
      y
 
81
    (cons (car x)
 
82
          (app2 (cdr x) y))))
 
83
 
 
84
(defthm app-of-app
 
85
  (equal (app (app x y) z)
 
86
         (app x (app y z))))
 
87
 
 
88
; We'll add a disabled event to see the color change.
 
89
 
 
90
(defthmd app-when-atom
 
91
  (implies (atom x)
 
92
           (equal (app x y)
 
93
                  y)))
 
94
 
 
95
; And partially disabled/enabled events get a slightly lighter color:
 
96
 
 
97
(defun fib (x)
 
98
  (declare (xargs :verify-guards nil))
 
99
  (if (zp x)
 
100
      1
 
101
    (if (equal x 1)
 
102
        1
 
103
      (+ (fib (- x 1)) (fib (- x 2))))))
 
104
 
 
105
(make-event
 
106
 `(defthm fib-of-36
 
107
    (equal (fib 36) ,(fib 36))))
 
108
 
 
109
(defsection partially-disabled
 
110
 
 
111
  (defthmd disabled-lemma
 
112
    (implies (atom x)
 
113
             (equal (app x y) y)))
 
114
 
 
115
  (defthm enabled-lemma
 
116
    (implies (atom x)
 
117
             (equal (app x y) y))))
 
118
 
 
119
(defun <foo> (x)
 
120
  "Stupid test of encoding"
 
121
  x)
 
122
 
 
123
(defun f (x)
 
124
  (declare (xargs :mode :program :guard (natp x)))
 
125
  (+ 1 x))
 
126
 
 
127
(verify-termination f (declare (xargs :verify-guards nil)))
 
128
 
 
129
(verify-guards f)
 
130
 
 
131
(defsection mixed-program/logic
 
132
 
 
133
  (defun f-program (x)
 
134
    (declare (xargs :mode :program))
 
135
    x)
 
136
 
 
137
  (defun f-logic (x)
 
138
    (declare (xargs :mode :logic))
 
139
    x))
 
140
 
 
141
(defsection mixed-verified/unverified
 
142
 
 
143
  (defun f-unverified (x)
 
144
    (declare (xargs :verify-guards nil))
 
145
    x)
 
146
 
 
147
  (defun f-verified (x)
 
148
    (declare (xargs :verify-guards t))
 
149
    x))
 
150
 
 
151
(defsection two-program
 
152
 
 
153
  (defun f-program1 (x)
 
154
    (declare (xargs :mode :program))
 
155
    x)
 
156
 
 
157
  (defun f-program2 (x)
 
158
    (declare (xargs :mode :program))
 
159
    x))
 
160
 
 
161
(defsection two-unverified
 
162
 
 
163
  (defun f-unverified1 (x)
 
164
    (declare (xargs :verify-guards nil))
 
165
    x)
 
166
 
 
167
  (defun f-unverified2 (x)
 
168
    (declare (xargs :verify-guards nil))
 
169
    x))
 
170
 
 
171
(defsection two-verified
 
172
 
 
173
  (defun f-verified1 (x)
 
174
    (declare (xargs :verify-guards t))
 
175
    x)
 
176
 
 
177
  (defun f-verified2 (x)
 
178
    (declare (xargs :verify-guards t))
 
179
    x))
 
180
 
 
181
 
 
182
(defsection program-section
 
183
  (defun g-program (x)
 
184
    (declare (xargs :mode :program))
 
185
    x))
 
186
 
 
187
(defsection logic-section
 
188
  (defun g-logic (x)
 
189
    (declare (xargs :verify-guards nil))
 
190
    x))
 
191
 
 
192
(defsection verified-section
 
193
  (defun g-verified (x)
 
194
    (declare (xargs :verify-guards t))
 
195
    x))
 
196
 
 
197
 
 
198
(defthm app-of-app3
 
199
  (equal (app (app x y) z)
 
200
         (app x (app y z))))
 
201
 
 
202
(defthm app-of-app4
 
203
  (equal (app (app x y) z)
 
204
         (app x (app y z))))
 
205
 
 
206
(defthm app-of-app5
 
207
  (equal (app (app x y) z)
 
208
         (app x (app y z))))
 
209
 
 
210
(defthm app-of-app6
 
211
  (equal (app (app x y) z)
 
212
         (app x (app y z))))
 
213
 
 
214
(defthm app-of-app7
 
215
  (equal (app (app x y) z)
 
216
         (app x (app y z))))
 
217
 
 
218
(defthm app-of-app8
 
219
  (equal (app (app x y) z)
 
220
         (app x (app y z))))
 
221
 
 
222
(defthm app-of-app9
 
223
  (equal (app (app x y) z)
 
224
         (app x (app y z))))
 
225
 
 
226
(defthm app-of-app10
 
227
  (equal (app (app x y) z)
 
228
         (app x (app y z))))
 
229
 
 
230
(defun h0 (x) x)
 
231
(defun h1 (x)
 
232
  (declare (xargs :verify-guards t))
 
233
  x)
 
234
 
 
235
(define h2 (x) x)
 
236
 
 
237
(define h3 (x) x)
 
238
 
 
239
(define h4 (x) :mode :program x)
 
240
 
 
241
 
 
242
(defsection nesting-test
 
243
  (defun n1 (x) x)
 
244
  (defsection n23
 
245
    (defun n2 (x) x)
 
246
    (defun n3 (x) x))
 
247
  (encapsulate ()
 
248
    (defun n4 (x) x))
 
249
  (defsection n56
 
250
    (defsection n5
 
251
      (defun n5 (x) x))
 
252
    (defsection n6
 
253
      (defun n6 (x) x))))
 
254
 
 
255
(define h5 (x) x)
 
256
(define h6 (x) x)
 
257