(module encapsulate mzscheme

  ;; Does not work for include-book, leaving out for now.

  #|
  (require-for-syntax "../modular/expansion/proof-syntax.scm")
  (require (lib "stxparam.ss")
           "defun.scm")

  (provide local encapsulate)

  (define-syntax (local stx)
    (syntax-case stx ()
      [(l term) (make-event stx #'term)]))

  (define-syntax (strip-local stx)
    (syntax-case stx (local)
      [(sl (local term)) (syntax/loc stx (begin))]
      [(sl term) #'term]))

  (define-syntax (encapsulate stx)
    (syntax-case stx ()
      [(e ((f (arg ...) result) ...) body ...)
       (make-event
        stx
        (quasisyntax/loc stx
          (begin
            (let* ()
              body ...
              (void (lambda (arg ...) (f arg ...)) ...))
            (defstub f (arg ...) result) ...
            (strip-local body) ...)))]))
  |#

  )