#lang scheme/base

(require (for-syntax scheme/base
                     scheme/list
                     "static-rep.ss"
                     "syntax-meta.ss"
                     "../proof/proof.ss"
                     "../proof/syntax.ss")
         "module.ss")

(provide top-interaction-macro module-begin-macro)

(define-for-syntax (expand-top-interaction stx)
  (syntax-case stx ()
    [(_ . body) (syntax/loc stx (#%top-interaction . body))]))

(define-for-syntax (get-module-name stx)
  (syntax-case stx (module-macro)
    [(module-macro name . _) (identifier? #'name) #'name]
    [_ #f]))

(define-for-syntax (expand-module-begin stx)
  (syntax-case stx ()
    [(_ body ...)
     (with-syntax ([exports (datum->syntax stx `(,#'all-defined-out))]
                   [(name ...)
                    (filter-map get-module-name
                                (syntax->list #'(body ...)))])
       (syntax/loc stx
         (#%plain-module-begin
          (provide exports)
          body ...
          (define-values ()
            (annotate-modules
             [name ...]
             (values))))))]))

(define-for-syntax (module/static->part id mod)
  (make-part
   (syntax-e id)
   (syntax->loc (module/static-source mod))
   (map syntax->term
        (append
         (map port/static-abstract (module/static-imports mod))
         (module/static-definitions mod)
         (map port/static-concrete (module/static-exports mod))))))

(define-for-syntax (identifier->part id)
  (module/static->part id (syntax->meta id)))

(define-syntax (annotate-modules stx)
  (syntax-case stx ()
    [(_ [name ...] expr)
     (annotate-proof
      (apply make-proof
             (map identifier->part
                  (syntax->list #'(name ...))))
      #'expr)]))

(define-syntax top-interaction-macro expand-top-interaction)
(define-syntax module-begin-macro expand-module-begin)