#|
January 6, 2003 -- we will suspend implementation of `include-book' for now.
See notes/include-book.txt for details.
|#
(module include-book mzscheme
  (require (lib "include.ss"))
  (require-for-syntax
   "defun-state.scm"
   (file "acl2-module-v.scm")
   (lib "moddep.ss" "syntax")
   (file "literal-identifier=.scm"))
  
  (provide include-book
           include-book/local)
  
  (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")]) ;; .ss ?
         (with-syntax ([teachpack-spec 
                        (make-teachpack-spec name.scm)
                        #;(datum->syntax-object stx (make-teachpack-spec name.scm))]
                       [teachpack@
                        (string->symbol (string-append (syntax-e #'name-stx) "@"))]
                       [teachpack^
                        (string->symbol (string-append (syntax-e #'name-stx) "^"))])
           (if (file-exists? (resolve-module-path (syntax-object->datum #'teachpack-spec) #f))
               (syntax/loc stx
                 (begin 
                   (require teachpack-spec)
                   (begin-for-syntax (register-unit! #'teachpack@ #'teachpack^))
                   ))
               (raise-syntax-error #f "Cannot find specified Teachpack" stx #'name-stx))))]
      [(_ name-stx :dir :system) #'(begin)]
      [(_ name-stx)
       (with-syntax ([name (string-append (syntax-e #'name-stx) ".lisp")])
         #`(include-at/relative-to #,stx #,stx name))]))
  
  (define-syntax (include-book/local stx)
    (syntax-case stx ()
      [(_ forms ...) #'(include-book forms ...)]))

#|
   January 6, 2006 -- we will suspend implementation of `include-book' for now.
   See notes/include-book.txt for details.

  (require-for-syntax (file "book-to-module.scm")
                      (file "book-path-utilities.scm"))
  (define-for-syntax (book-path-stx->module-path include-book-stx path-stx system-book?)
    (let ([str (syntax-e path-stx)])
      (unless (string? str)
        (raise-syntax-error #f "Book path must be a string literal" 
                            include-book-stx path-stx))
      
      (let-values ([(base name dir?) (split-path (simplify-path (path-replace-suffix str ".scm") #f))])
        (unless (path? name)
          (raise-syntax-error #f "Book path must point to a file, not a directory" 
                              include-book-stx path-stx))
        (cond [system-book?
               (path->string 
                (simplify-path 
                 (build-path *system-module-root* (relative->same base) name) #f))]
              [(and (path? base) (absolute-path? base)
                    (points-inside-system-books? base))
               (path->string
                (build-path (system-book-prefix->system-module-prefix base) name))]
              [(and (path? base) (relative-path? base))
               (path->string (build-path base name))]
              [else (path->string name)]))))
  (define-for-syntax (book-path-stx->mname:: path)
    (let ([str (syntax-e path)])
      (let-values ([(base name dir?) (split-path str)])
        (string->symbol (string-append (path->string name) "::")))))
  
  (define-syntax (provide-book stx)
    (syntax-case stx (:dir :system)
      [(_ file-path :dir :system)
       (let ([module-path (book-path-stx->module-path stx #'file-path #t)])
         #`(provide #,(datum->syntax-object #'file-path
                                            `(all-from (file ,module-path)))))]
      [(_ file-path options ...)
       (let ([module-path (book-path-stx->module-path stx #'file-path #f)])
         #`(provide #,(datum->syntax-object #'file-path
                                            `(all-from (file ,module-path)))))]))
  
  (define-syntax (include-book/local stx)
    (syntax-case stx (:dir :system)
      [(_ file-path :dir :system)
       (let ([module-path ;:: Syntax[string literal]
              (book-path-stx->module-path stx #'file-path #t)]
             [mname:: (book-path-stx->mname:: #'file-path)])
         ;(book->module (build-path *system-book-root* (syntax-e #'file-path)))
         #`(require #,(datum->syntax-object #'file-path 
                                            `(file ,module-path))
                    #,(datum->syntax-object #'file-path
                                            `(prefix ,mname:: (file ,module-path)))))]
      [(_ file-path options ...)
       (let ([module-path ;:: Syntax[string literal]
              (book-path-stx->module-path stx #'file-path #f)]
             [mname:: (book-path-stx->mname:: #'file-path)])
         ;(book->module (build-path (syntax-e #'file-path)))
         #`(require #,(datum->syntax-object #'file-path
                                            `(file ,module-path))
                    #,(datum->syntax-object #'file-path
                                            `(prefix ,mname:: (file ,module-path)))))]))
  
  (define-syntax (include-book stx)
    (syntax-case stx ()
      [(_ file-path options ...)
       (with-syntax ([provide-form (if (eq? (syntax-local-context) 'module)
                                       #'(provide-book file-path options ...)
                                       #'(void))])
         #'(begin (include-book/local file-path options ...)
                  provide-form))]))
|#
  )