teachpacks/list-theory.scm
#ci
(module list-theory mzscheme
  (require (prefix acl2: (file "../language/conditionals.scm"))
           (prefix srfi: (lib "1.ss" "srfi"))
           (lib "unit.ss"))
  
  (provide teachpack@ teachpack^)
  
  (define-for-syntax (literal=? i j)
    (and (identifier? i) (identifier? j)
         (eq? (syntax-e i) (syntax-e j))))
  
  (define-signature teachpack^ 
    [(define-syntaxes (deflist)
       (lambda (stx)
         ;; we don't currently support extra args b/c ACL2 is broken.
         (syntax-case* stx (l) literal=?
           [(_ predicate-name (l) item-predicate/acl2)
            #'(define (predicate-name l)
                (let loop ([items l])
                  (cond [(null? items) 't]
                        [else (if (null? (item-predicate/acl2 (car items)))
                                  '()
                                  (loop (cdr items)))])))])))])
  
  (define-unit teachpack@
    (import)
    (export teachpack^))
  )