(module include-book mzscheme
(require (lib "include.ss")
(file "../define-below/define-below.ss"))
(require-for-syntax (file "acl2-module-v.scm")
(lib "moddep.ss" "syntax")
(file "literal-identifier=.scm"))
(provide include-book)
(define-syntax (include-book stx)
(syntax-case* stx (:dir :teachpacks) literal-identifier=?
[(_ name-stx :dir :teachpacks)
(string? (syntax-e #'name-stx))
(let ([name.scm (string-append (syntax-e #'name-stx) ".scm")]) (with-syntax ([teachpack-spec (make-teachpack-spec name.scm)])
(syntax/loc stx
(begin
(require (rename teachpack-spec tp@ teachpack@)
(rename teachpack-spec tp^ teachpack^))
(define-values/invoke-unit/below
tp@
(import)
(export tp^))))))]
[(_ name-stx :dir :system) #'(begin)]
[(_ name-stx)
(with-syntax ([name (string-append (syntax-e #'name-stx) ".lisp")])
#`(include-at/relative-to #,stx #,stx name))]))
)