#lang scheme/base

(require "../private/planet.ss"
         "module.ss")

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

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

(define-for-syntax (expand-top-interaction stx)
  (parameterize ([current-syntax 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)
  (parameterize ([current-syntax 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 #:message "not a module" 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)