#lang scheme

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

(require (for-syntax (lib "moddep.ss" "syntax")
                     (prefix-in acl2- "acl2-reader.ss")
                     "acl2-module-v.ss"
                     (cce text)))

(provide include-book)

(define-syntax (include-book stx)
  (case (syntax-local-context)
    [(expression)
     (raise-syntax-error
      #f "not valid as an expression" stx)]
    [else
     (syntax-case* stx (:dir :system :teachpacks) text=?
       [(_ name-stx :dir :teachpacks)
        (string? (syntax-e #'name-stx))
        (let ([name.ss (string-append (syntax-e #'name-stx) ".ss")])
          (with-syntax ([teachpack-spec (make-teachpack-spec name.ss)])
            (quasisyntax/loc stx
              (begin
                #,(syntax/loc stx
                    (require (rename-in teachpack-spec
                                        [teachpack@ tp@]
                                        [teachpack^ tp^])))
                #,(syntax/loc stx
                    (define-values/invoke-unit/below
                      tp@
                      (import)
                      (export tp^)))))))]
       [(_ name-stx :dir :system)
        (quasisyntax/loc stx (begin))]
       [(_ name-stx)
        (with-syntax ([name (string-append (syntax-e #'name-stx) ".lisp")])
          (quasisyntax/loc stx
            (include-at/relative-to/reader
             name-stx name-stx name acl2-read-syntax)))])]))