#lang scheme/base

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

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

         mzlib/etc
         "keywords.ss"
         "dynamic-rep.ss"
         "../lang/defun.ss"
         "../lang/defthm.ss"
         "../proof/event.ss")

(provide module-macro)

(define-for-syntax (matcher . ids)
  (let* ([table (make-free-identifier-mapping)])
    (for ([id ids])
      (free-identifier-mapping-put! table id #t))
    (lambda (stx)
      (syntax-case stx ()
        [(name . _)
         (identifier? #'name)
         (free-identifier-mapping-get table #'name (lambda () #f))]
        [_ #f]))))

(define-for-syntax (expand-export port id)
  (let* ([source (port/static-source port)]
         [concrete (port/static-concrete port)]
         [internals (port/static-sig-names/internal port)]
         [externals (port/static-sig-names/external port)]
         [arguments (port/static-sig-args port)])
    (with-syntax ([exp/dynamic id]
                  [(put ...) externals]
                  [(get ...) internals]
                  [(tmp ...) (generate-temporaries externals)]
                  [((arg ...) ...) arguments])
      (dracula-special-event
       concrete
       (syntax/loc source
         (define-values ()
           (begin
             (interface/dynamic-put-function!
              exp/dynamic 'put
              (lambda (arg ...) (get arg ...)))
             ...
             (values))))))))

(define-for-syntax (expand-import port id)
  (let* ([source (port/static-source port)]
         [abstract (port/static-abstract port)]
         [internals (port/static-sig-names/internal port)]
         [externals (port/static-sig-names/external port)]
         [arguments (port/static-sig-args port)]
         [axioms (port/static-con-names/internal port)])
    (with-syntax ([imp/dynamic id]
                  [(get ...) externals]
                  [(put ...) internals]
                  [(tmp ...) (generate-temporaries externals)]
                  [((arg ...) ...) arguments]
                  [(ax ...) axioms])
      (dracula-special-event
       abstract
       (syntax/loc source
         (begin
           (define tmp (interface/dynamic-get-function imp/dynamic 'get)) ...
           (defun put (arg ...) (tmp arg ...)) ...
           (defaxiom ax 't) ...))))))

(define-for-syntax (expand-definition def)
  def)

(define-for-syntax (expand-exports mod id)
  (map (lambda (port) (expand-export port id))
       (module/static-exports mod)))

(define-for-syntax (expand-imports mod id)
  (map (lambda (port) (expand-import port id))
       (module/static-imports mod)))

(define-for-syntax (expand-definitions mod)
  (map expand-definition (module/static-definitions mod)))

(define-for-syntax (expand-dynamic stx)
  (syntax-case stx ()
    [(_ static-name)
     (let* ([import-name #'imp/dynamic]
            [export-name #'exp/dynamic]
            [mod/static (syntax->meta #'static-name)]
            [source (module/static-source mod/static)])
       (with-syntax ([(imp ...) (expand-imports mod/static import-name)]
                     [(exp ...) (expand-exports mod/static export-name)]
                     [(def ...) (expand-definitions mod/static)]
                     [original source]
                     [dynamic-name (refresh-identifier
                                    (module/static-dynamic mod/static))])
         (syntax/loc source
           (define dynamic-name
             (make-module/dynamic
              (lambda (imp/dynamic)
                (#%annotate-part
                 static-name original
                 (let ([exp/dynamic (empty-interface/dynamic)])
                   (begin-with-definitions
                    (#%annotate-term imp) ...
                    (#%annotate-term def) ...
                    (#%annotate-term exp) ...
                    (interface/dynamic-join exp/dynamic imp/dynamic))))))))))]))

(define-for-syntax (parse-port rev-ports stx)
  (syntax-case stx ()
    [(_ ifc [ext int] ...)
     (let* ([ifc (syntax->meta #'ifc)])
       (make-port/static
        stx
        ifc
        (map cons
             (syntax->list #'(ext ...))
             (syntax->list #'(int ...)))
        (map (lambda (inc)
               (or
                (findf (lambda (port)
                         (interface/static-external=?
                          inc (port/static-interface port)))
                       rev-ports)
                (syntax-error stx
                              "no im/export of ~a (required by ~a)"
                              (syntax-e (interface/static-name inc))
                              (syntax-e (interface/static-name ifc)))))
             (interface/static-includes ifc))))]))

(define-for-syntax (parse-ports prior stx-list)
  (if (null? stx-list)
      null
      (let* ([port (parse-port prior (car stx-list))])
      (cons port (parse-ports (cons port prior) (cdr stx-list))))))

(define-for-syntax (parse-exports imports stx-list)
  (parse-ports imports stx-list))

(define-for-syntax (parse-imports stx-list)
  (parse-ports null stx-list))

(define-for-syntax (expand-static stx)
  (syntax-case stx ()
    [(_ static-name original . body)
     (let* ([forms (syntax->list #'body)]
            [imps (filter (matcher #'import) forms)]
            [exps (filter (matcher #'export) forms)]
            [defs (filter-not (matcher #'import #'export) forms)])
       (with-syntax ([(imp ...) imps]
                     [(exp ...) exps]
                     [(def ...) defs])
         (syntax/loc #'original
           (define-syntax static-name
             (make-syntax-meta
              (let* ([imports (#%app parse-imports (list #'imp ...))]
                     [exports (#%app parse-exports imports (list #'exp ...))]
                     [definitions (list #'def ...)])
                (make-module/static #'static-name
                                    #'dynamic-name
                                    #'original
                                    imports
                                    exports
                                    definitions))
              (expand-keyword "cannot be used as an expression"))))))]))

(define-for-syntax (expand-module stx)
  (syntax-case stx ()
    [(_ static-name body ...)
     (parameterize ([current-syntax stx])
       (with-syntax ([original stx])
         (syntax/loc stx
           (begin
             (define-syntaxes (define-static) expand-static)
             (define-syntaxes (define-dynamic) expand-dynamic)
             (define-static static-name original body ...)
             (define-dynamic static-name)))))]))

(define-syntax module-macro expand-module)