#lang scheme/base

(require "../private/planet.ss"
         "../teachpacks/testing.ss"
         "../teachpacks/doublecheck.ss"
         "dynamic-rep.ss"
         "../lang/defun.ss"
         "../lang/defthm.ss")

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

(provide invoke-macro)

(define-for-syntax (expand-invoke stx)
  (parameterize ([current-syntax stx])
    (syntax-case stx ()
      [(_ mod)
       (begin
         (unless (and (identifier? #'mod)
                      (syntax-meta? (syntax-local-value #'mod (lambda () #f)))
                      (module/static? (syntax->meta #'mod)))
           (syntax-error #'mod "expected the name of a module here"))
         (let* ([module/static (syntax->meta #:message "not a module" #'mod)]
                [module/dynamic (module/static-dynamic module/static)]
                [imports/static (module/static-imports module/static)]
                [exports/static (module/static-exports module/static)])
           (unless (null? imports/static)
             (syntax-error
              #'mod
              (format "unresolved imports:\n~s\nfrom exports:\n~s\n"
                      (map (lambda (port)
                             (map syntax-e (port/static-sig-names/external port)))
                           imports/static)
                      (map (lambda (port)
                             (map syntax-e (port/static-sig-names/external port)))
                           exports/static))))
           (let* ([fns (map port/static-sig-names/external exports/static)]
                  [args (map port/static-sig-args exports/static)]
                  [ths (map port/static-con-names/external exports/static)])
             (with-syntax ([dynamic module/dynamic]
                           [(fn ...) (map refresh-identifier (apply append fns))]
                           [(tmp ...) (generate-temporaries (apply append fns))]
                           [((arg ...) ...) (apply append args)]
                           [(th ...) (map refresh-identifier (apply append ths))])
               (syntax/loc stx
                 (begin
                   (define impl
                     ((module/dynamic-implementation dynamic)
                      (empty-interface/dynamic)))
                   (define tmp (interface/dynamic-get-function impl 'fn)) ...
                   (defun fn (arg ...) (tmp arg ...)) ...
                   (defaxiom th 't) ...
                   (generate-report!)
                   (check-properties!)))))))])))

(define-syntax invoke-macro expand-invoke)