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

« back to all changes in this revision

Viewing changes to books/rtl/rel6/support/support/fast-and.lisp

• browse files at revision 7
• compare with another revision
• download diff
• download tarball
• view history from revision 7

Show diffs side-by-side

added

removed

books/rtl/rel6/support/support/fast-and.lisp

 

1

(in-package "ACL2")

 

2

 

 

3

(defun split-list (lst lo hi)

 

4

  (cond ((endp lst) 

 

5

         (mv lo hi))

 

6

        ((endp (cdr lst)) 

 

7

         (mv (cons (car lst) lo) hi))

 

8

        (t

 

9

         (split-list (cddr lst)

 

10

                     (cons (car lst) lo)

 

11

                     (cons (cadr lst) hi)))))

 

12

 

 

13

(defun fast-and-fn (conjuncts)

 

14

  (declare (xargs :mode :program))

 

15

  (cond ((endp conjuncts) ''t)

 

16

        ((endp (cdr conjuncts)) (car conjuncts))

 

17

        (t

 

18

         (mv-let (hi lo)

 

19

             (split-list conjuncts () ())

 

20

           (list 'if

 

21

                 (fast-and-fn hi)

 

22

                 (fast-and-fn lo)

 

23

                 'nil)))))

 

24

 

 

25

(defmacro fast-and (&rest conjuncts)

 

26

  (fast-and-fn conjuncts))

• Older »

Loggerhead is a web-based interface for Breezy
Version: 2.0.1