(module include-book mzscheme

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

  (require-for-syntax (lib "moddep.ss" "syntax")
                      (prefix acl2- "acl2-reader.scm")
                      "acl2-module-v.scm"
                      "../modular/expansion/proof-syntax.scm")
  (require-for-syntax-cce/scheme)
  
  (provide include-book)
  
  (define-syntax (include-book stx)
    (case (syntax-local-context)
      [( module module-begin )
       (make-event
        stx
        (syntax-case* stx (:dir :system :teachpacks) text=?
          [(_ 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)])
               (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/reader
                #,stx #,stx name acl2-read-syntax)))]))]
      [else
       (raise-syntax-error
        #f "only valid at top level of definitions window" stx)]))

  )