← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/coi/nary/skip-rewrite.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/coi/nary/skip-rewrite.lisp
1
 
#|-*-Lisp-*-=================================================================|#
2
 
#|                                                                           |#
3
 
#| coi: Computational Object Inference                                       |#
4
 
#|                                                                           |#
5
 
#|===========================================================================|#
 
1
; Computational Object Inference
 
2
; Copyright (C) 2005-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
 
6
31
(in-package "ACL2")
7
32
 
8
33
(defun unhide (x)
53
78
  (declare (type (satisfies true-listp) keys vals))
54
79
  (declare (xargs :guard (pseudo-termp-key arg term)))
55
80
  (cond
56
 
   (arg 
57
 
    (cond 
 
81
   (arg
 
82
    (cond
58
83
     ((endp term) nil)
59
84
     (t (cons (beta-reduce-term nil (car term) keys vals)
60
85
              (beta-reduce-term arg (cdr term) keys vals)))))
77
102
 
78
103
(defun unhide-eval-key (arg term alist)
79
104
  (cond
80
 
   (arg 
81
 
    (cond 
 
105
   (arg
 
106
    (cond
82
107
     ((endp term) nil)
83
108
     (t (cons (unhide-eval-key nil (car term) alist)
84
109
              (unhide-eval-key arg (cdr term) alist)))))
99
124
 
100
125
(defun wf-beta-term (arg term)
101
126
  (cond
102
 
   (arg 
103
 
    (cond 
 
127
   (arg
 
128
    (cond
104
129
     ((endp term) t)
105
130
     (t (and (wf-beta-term nil (car term))
106
131
             (wf-beta-term arg (cdr term))))))
136
161
          nil)))
137
162
 
138
163
;; DAG -- odd that we need these now, but not before.
139
 
(defthm car-quote-list 
 
164
(defthm car-quote-list
140
165
  (equal (car (quote-list list))
141
166
         (if (consp list) `(quote ,(car list)) nil)))
142
167
 
154
179
    (wf-beta-term arg term)
155
180
    (equal (len keys) (len vals)))
156
181
   (equal (unhide-eval-key arg (beta-reduce-term arg term keys vals) a1)
157
 
          (unhide-eval-key arg term (pairlis$ keys 
 
182
          (unhide-eval-key arg term (pairlis$ keys
158
183
                                              (unhide-eval-key t vals a1)))))
159
184
   :hints (("Goal" :do-not '(generalize eliminate-destructors)
160
185
            :do-not-induct t
212
237
   (lambda-expr-p term)
213
238
   (equal (unhide-eval-key nil term a1)
214
239
          (unhide-eval-key nil (CAR (CDR (CDR (CAR term))))
215
 
                           (pairlis$ (CAR (CDR (CAR term))) 
 
240
                           (pairlis$ (CAR (CDR (CAR term)))
216
241
                                     (unhide-eval-key t (cdr term) a1)))))
217
242
  :hints (("Goal" :in-theory (e/d (lambda-expr-p-to-para-lambda-expr-key-p) (unhide-eval-key)))))
218
243
 
221
246
   (lambda-expr-p term)
222
247
   (equal (unhide-eval term a1)
223
248
          (unhide-eval (CAR (CDR (CDR (CAR term))))
224
 
                       (pairlis$ (CAR (CDR (CAR term))) 
 
249
                       (pairlis$ (CAR (CDR (CAR term)))
225
250
                                 (unhide-eval-list (cdr term) a1)))))
226
251
  :hints (("Goal" :use unhide-eval-lambda-expr-helper
227
252
           :in-theory (enable unhide-eval-key-reduction))))
249
274
    (lambda-expr-p term)
250
275
    (pseudo-termp term))
251
276
   (equal (unhide-eval term a1)
252
 
          (unhide-eval (beta-reduce-term nil (CAR (CDR (CDR (CAR term)))) 
 
277
          (unhide-eval (beta-reduce-term nil (CAR (CDR (CDR (CAR term))))
253
278
                                         (CAR (CDR (CAR term)))
254
279
                                         (cdr term)) a1))))
255
280
 
335
360
  ;; watch this proof (and monitor unhide-hide-wrapper)
336
361
 
337
362
  (defun foo (x) (if (zp x) 2 (foo (1- x))))
338
 
  
 
363
 
339
364
  (defthm open-foo
340
365
    (implies
341
366
     (and
342
367
      (not (zp x))
343
368
      (equal v (1- x)))
344
369
     (equal (foo x) (skip-rewrite (foo v)))))
345
 
  
 
370
 
346
371
  (defthm foo-0
347
372
    (equal (foo 0) 2))
348
 
  
 
373
 
349
374
  (in-theory (disable foo (foo)))
350
 
  
 
375
 
351
376
  ;;(trace$ unhide-hide-wrapper)
352
 
  
 
377
 
353
378
  (defthm foo-10
354
379
    (equal (foo 10) 2))
355
380
 
406
431
  #+joe
407
432
  (defthmd unhide-eval2-constraint-0
408
433
    (implies
409
 
     (and (consp term) 
 
434
     (and (consp term)
410
435
          (syntaxp (not (equal a *nil*))) ; prevent looping
411
436
          (not (equal (car term) 'quote)))
412
437
     (equal (unhide-eval2 term a)
458
483
(skip-proofs
459
484
(defthmd unhide-eval2-constraint-0
460
485
    (implies
461
 
     (and (consp term) 
 
486
     (and (consp term)
462
487
          (syntaxp (not (equal a *nil*))) ; prevent looping
463
488
          (not (equal (car term) 'quote)))
464
489
     (equal (unhide-eval2 term a)
480
505
               '(:in-theory (enable UNHIDE-EVAL2-CONSTRAINT-0))))
481
506
;  :rule-classes ((:meta :trigger-fns (unhide))))
482
507
  )
483
 
|#
 
508
|#
 
 
b'\\ No newline at end of file'