(module include-book mzscheme

  (require (lib "include.ss")
           "../define-below/define-below.ss")

  (require-for-syntax (lib "moddep.ss" "syntax")
                      "acl2-module-v.scm"
                      "../modular/expansion/proof-syntax.scm"
                      (file "literal-identifier=.scm"))
  
  (provide include-book)
  
  (define-syntax (include-book stx)
    (unless (eq? (syntax-local-context) 'module)
      (raise-syntax-error
       #f "only valid at top level of definitions window" stx))
    (make-event
     stx
     (syntax-case* stx (:dir :system :teachpacks) literal-identifier=?
       [(_ name-stx :dir :teachpacks)
        (string? (syntax-e #'name-stx))
        (let ([name.scm (string-append (syntax-e #'name-stx) ".scm")]) ;; .ss ?
          (with-syntax ([teachpack-spec (make-teachpack-spec name.scm)])
            (quasisyntax/loc stx
              (begin
                #,(syntax/loc stx
                    (require (rename teachpack-spec tp@ teachpack@)
                             (rename teachpack-spec tp^ teachpack^)))
                #,(syntax/loc stx
                    (define-values/invoke-unit/below
                      tp@
                      (import)
                      (export tp^)))))))]
       [(_ name-stx :dir :system) (syntax/loc stx (begin))]
       [(_ name-stx)
        (with-syntax ([name (string-append (syntax-e #'name-stx) ".lisp")])
          (quasisyntax/loc stx (include-at/relative-to #,stx #,stx name)))])))

  )