#lang scheme/base

#|
(require "static-rep.ss"
         "syntax-meta.ss"
         "../proof/wrapper.ss"
         "../private/hash.ss"
         syntax/boundmap

         (for-template scheme/base
                       "dynamic-rep.ss"
                       "../lang/defun.ss"
                       "../lang/defthm.ss"))

(provide expand-import
         expand-export)

(define (make-mapping ins outs)
  (let* ([hash
          (make-immutable-hasheq
           (map cons
                (map syntax-e (syntax->list ins))
                (syntax->list outs)))])
    (lambda (id)
      (hash-ref/default hash (syntax-e id) id))))

(define ((expand-import interface/dynamic-id) stx)
  (syntax-case stx ()
    [(_ ifc-id [from-id to-id] ...)
     (let* ([interface/static (syntax->meta #'ifc-id)]
            [from->to (make-mapping #'(from-id ...) #'(to-id ...))]
            [abs (interface/static-abstract from->to interface/static stx)]
            [fns (interface/static-sig-names interface/static)]
            [args (interface/static-sig-args interface/static)]
            [ths (interface/static-con-names interface/static)])
       (with-syntax ([imp interface/dynamic-id]
                     [(get ...) fns]
                     [(put ...) (map from->to (map refresh-identifier fns))]
                     [(tmp ...) (generate-temporaries fns)]
                     [((arg ...) ...) args]
                     [(th ...) (map refresh-identifier ths)])
         (dracula-special-event
          abs
          (syntax/loc stx
            (begin
              (define tmp (interface/dynamic-get-function imp 'get)) ...
              (defun put (arg ...) (tmp arg ...)) ...
              (defaxiom th 't) ...)))))]))

(define ((expand-export interface/dynamic-id) stx)
  (syntax-case stx ()
    [(_ ifc-id [from-id to-id] ...)
     (let* ([interface/static (syntax->meta #'ifc-id)]
            [from->to (make-mapping #'(from-id ...) #'(to-id ...))]
            [con (interface/static-concrete from->to interface/static stx)]
            [fns (interface/static-sig-names interface/static)]
            [args (interface/static-sig-args interface/static)])
       (with-syntax ([exp interface/dynamic-id]
                     [(put ...) fns]
                     [(get ...) (map from->to (map refresh-identifier fns))]
                     [((arg ...) ...) args])
         (dracula-special-event
          con
          (syntax/loc stx
            (define-values ()
              (begin
                (interface/dynamic-put-function!
                 exp 'put (lambda (arg ...) (get arg ...)))
                ...
                (values)))))))]))
|#