#lang scheme/base

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

         "dynamic-rep.ss"
         "../lang/defun.ss"
         "../lang/defthm.ss")

(provide invoke-macro)

(define-for-syntax (expand-invoke stx)
  (syntax-case stx ()
    [(_ mod)
     (let* ([module/static (syntax->meta #'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)
         (raise-syntax-error
          #f
          (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))
          stx
          #'mod))
       (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) ...)))))]))

(define-syntax invoke-macro expand-invoke)