#lang scheme

(require "../private/define-below.ss"
         "../teachpacks/testing.ss"
         "../teachpacks/doublecheck.ss"
         (for-syntax "../proof/proof.ss" "../proof/syntax.ss"))

(provide dracula-module-begin)

(define-syntax (dracula-module-begin stx)
  (syntax-case stx ()
    [(_ form ...)
     (with-syntax ([exports (datum->syntax stx `(,#'all-defined-out))])
       (quasisyntax/loc stx
         (#%module-begin
          (define-values []
            #,(annotate-proof
               (make-proof
                (make-part
                 'Dracula
                 (syntax->loc stx)
                 (map syntax->term (syntax->list #'(form ...)))))
               (syntax/loc stx (values))))
          (provide exports)
          (begin-below form ...)
          (generate-report!)
          (check-properties!))))]))