File: fast-and.lisp

package info (click to toggle)
acl2 6.5-2
  • links: PTS
  • area: main
  • in suites: jessie, jessie-kfreebsd
  • size: 108,856 kB
  • ctags: 110,136
  • sloc: lisp: 1,492,565; xml: 7,958; perl: 3,682; sh: 2,103; cpp: 1,477; makefile: 1,470; ruby: 453; ansic: 358; csh: 125; java: 24; haskell: 17
file content (26 lines) | stat: -rw-r--r-- 694 bytes parent folder | download | duplicates (13) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
 
(in-package "ACL2")

(defun split-list (lst lo hi)
  (cond ((endp lst) 
         (mv lo hi))
        ((endp (cdr lst)) 
         (mv (cons (car lst) lo) hi))
        (t
         (split-list (cddr lst)
                     (cons (car lst) lo)
                     (cons (cadr lst) hi)))))

(defun fast-and-fn (conjuncts)
  (declare (xargs :mode :program))
  (cond ((endp conjuncts) ''t)
        ((endp (cdr conjuncts)) (car conjuncts))
        (t
         (mv-let (hi lo)
             (split-list conjuncts () ())
           (list 'if
                 (fast-and-fn hi)
                 (fast-and-fn lo)
                 'nil)))))

(defmacro fast-and (&rest conjuncts)
  (fast-and-fn conjuncts))