(module audio mzscheme (require (lib "mred.ss" "mred") (file "audio-glue.scm") (lib "unit.ss")) (provide teachpack@ teachpack^) (define (boolean->acl2 b) (if b 't '())) (define (acl2->boolean a) (if (or (equal? a 'nil) (equal? a '())) #f #t)) (define-signature teachpack^ [play-wav]) (define-unit teachpack@ (import) (export teachpack^) (define (play-wav file async) (boolean->acl2 (play-sound file (acl2->boolean async))))))