← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/coi/util/recursion-support.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/util/recursion-support.lisp
 
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
 
1
31
(in-package "DEFUN")
2
32
 
3
33
(include-book "mv-nth")
11
41
       (consp (cdr x))
12
42
       (not (equal (cadr x) 'nil))))
13
43
 
14
 
(defun syn-true () 
 
44
(defun syn-true ()
15
45
  (declare (xargs :guard t))
16
46
  acl2::*t*)
17
47
 
36
66
  (cond
37
67
   ((syn-falsep x) z)
38
68
   ((syn-truep x)  y)
39
 
   (t 
 
69
   (t
40
70
    (syn-if x y z))))
41
71
 
42
72
(defun syn-not (x)
130
160
                      (mv (syn-and bcase case bthen) then))
131
161
                     (t ; belse
132
162
                      (mv (syn-and bcase (syn-not case) belse) else)))))))
133
 
    
 
163
 
134
164
    (t
135
165
     (met ((base args) (lift-base-args flist (cdr term) vars))
136
166
          (if (syn-falsep base) (mv (syn-false) :ignore)
137
167
            (mv base `(,(car term) ,@args)))))))
138
 
     
 
168
 
139
169
 (defun lift-base-args (flist args vars)
140
170
   (declare (xargs :measure (acl2-count args)))
141
171
   (if (consp args)
173
203
    (syn-lazy-if case body base)))
174
204
 
175
205
;; duplo is intended to assist in defining induction schema for use in
176
 
;; congruence proofs.  
 
206
;; congruence proofs.
177
207
 
178
208
(mutual-recursion
179
209
 
208
238
         (met ((term nterm) (duplo flist valist (car args)))
209
239
           (mv (cons term oargs) (cons nterm nargs))))
210
240
     (mv nil nil)))
211
 
 
 
241
 
212
242
 )
213
243
 
214
244
(defun value-pair (x y)
260
290
   (if (endp args) res
261
291
     (let ((res (term-vars (car args) res)))
262
292
       (term-vars-args (cdr args) res))))
263
 
 
 
293
 
264
294
 )
265
295
 
266
296
(mutual-recursion
283
313
   (if (endp args) nil
284
314
     (cons (term-var-sub (car args) valist)
285
315
           (term-var-sub-args (cdr args) valist))))
286
 
 
 
316
 
287
317
 )
288
318
 
289
319
;; So .. we need gensym in order to do this well.  Perhaps we can get