(module expansion mzscheme

  (require "syntax-errors.scm"
           "syntax-indirection.scm"
           "metadata.scm"
           "proof-syntax.scm"
           "proof.scm"
           "idmap.scm"
           "checks.scm"
           (lib "list.ss")
           (lib "etc.ss")
           (planet "combinators.ss" ("cce" "combinators.plt" 1 4)))

  (require-for-template
   mzscheme
   "../../language/defun.scm"
   "implementation.scm"
   (planet "combinators.ss" ("cce" "combinators.plt" 1 4)))

  (provide expand-interface
           expand-module/impl
           expand-invoke
           expand-compound)

  (define (reject-repl! stx)
    (case (syntax-local-context)
      [( module ) (void)]
      [else (raise-syntax-error
             #f "valid only at top level of definitions window" stx)]))

  (define (certify-mode mode stx)
    (syntax-property stx 'certify-mode mode))

  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ;;
  ;;  interface
  ;;
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

  (define (expand-interface stx)
    (reject-repl! stx)
    (syntax-case/error stx ()
      [(i name sig/ctr ...)
       (with-syntax ([orig stx]
                     [(((sig f (arg ...)) ...) ((con th expr) ...))
                      (extract-signatures/contracts #'(sig/ctr ...))])
         (syntax/loc stx
           (begin

             (define-for-syntax metadata
               (interface-meta
                #'orig #'name
                (list (cons #'f (list #'arg ...)) ...)
                (list (cons #'th #'expr) ...)))

             (define-syntax (wrap-proof stx)
               (syntax-case stx ()
                 [(wp term)
                  (make-modular #'orig (interface-proof metadata) #'term)]))

             (wrap-proof
              (define-syntax name
                (make-syntax-indirection metadata))))))]))

  (define (extract-signatures/contracts stx)
    (let*-values ([(sigs ctrs)
                   (fold/values
                    add-signature/contract
                    (list null null)
                    (syntax->list stx))])
      (list (reverse sigs) (reverse ctrs))))

  (define (add-signature/contract stx sigs ctrs)
    (syntax-case/name
     stx (sig con)
     [(sig f (arg ...))
      (andmap identifier? (syntax->list #'(f arg ...)))
      (values (cons stx sigs) ctrs)]
     [(con th expr)
      (identifier? #'th)
      (values sigs (cons stx ctrs))]
     [_ (raise-syntax-error #f "expected a signature or contract" stx)]))

  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ;;
  ;;  module
  ;;
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

  (define (expand-module/impl stx)
    (reject-repl! stx)
    (syntax-case/error
     stx (import export assign sharing : <-)

     [(m/i impl orig name
           (import (itag : iface) ...)
           (export (etag : eface) ...)
           (sharing (shared ...) ...)
           def ...
           (assign (atag (external <- internal) ...) ...))

      (begin

       (check-identifier! #'name)
       (check-identifiers! #'(itag ... iface ...))
       (check-identifiers! #'(etag ... eface ...))
       (check-identifiers! #'(atag ... external ... ... internal ... ...))
       (check-identifiers! #'(shared ... ...))
       (check-unique-identifiers! #'(itag ... etag ...))
       (check-same-identifiers! #'(etag ...) #'(atag ...))
       (check-interface-identifiers! #'(iface ... eface ...))
       (check-sharing! #'(itag ... etag ...) #'(iface ... eface ...)
                       #'((shared ...) ...))
       (check-assigned-identifiers! #'(etag ...) #'(eface ...)
                                    #'((external ...) ...)))

      (certify-mode
       'transparent
       (quasisyntax/loc stx
         (begin

           (define-for-syntax metadata
             (module-meta
              #'orig #'name #'impl
              (list (cons #'itag (read-syntax-indirection #'iface)) ...)
              (list (cons #'etag (read-syntax-indirection #'eface)) ...)
              (list (list #'shared ...) ...)))

           (begin-for-syntax
            (check-primitive-sharing!
             metadata
             (list #'def ...)
             (list #'atag ...)
             (list (list #'external ...) ...)
             (list (list #'internal ...) ...)))

           (define-syntax (wrap-proof stx)
             (syntax-case stx ()
               [(wp term)
                (make-modular
                 #'orig
                 (primitive-proof
                  metadata
                  (list #'def ...)
                  (list #'atag ...)
                  (list (list #'external ...) ...)
                  (list (list #'internal ...) ...))
                 #'term)]))

           (wrap-proof
            (define (impl var)
              (define-tagged-imports itag iface var) ...
              def ...
              (build-module
               [etag (build-interface eface [external internal] ...)] ...)))

           (define-syntax name (make-syntax-indirection metadata)))))]))

  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ;;
  ;;  invoke
  ;;
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

  (define (expand-invoke stx)
    (reject-repl! stx)
    (syntax-case/error
     stx ()
     [(i mod)

      (begin
        (check-identifier! #'mod)
        (check-module-identifier! #'mod))

      (let* ([meta (read-syntax-indirection #'mod)]
             [imports (mod-imports meta)]
             [exports (mod-exports meta)]
             [ifcs (map ifc-name (map (curry mod-ifc meta) exports))])
        (unless (null? (mod-imports meta))
          (syntax-error #'mod "invoked module has unresolved imports"))
        (with-syntax ([orig stx]
                      [impl (mod-impl meta)]
                      [(tag ...) exports]
                      [(ifc ...) ifcs])
          (syntax/loc stx
            (begin

              (define-for-syntax metadata
                (read-syntax-indirection #'mod))

              (define-syntax (wrap-proof stx)
                (syntax-case stx ()
                  [(wp term)
                   (make-modular
                    #'orig
                    (invoke-proof metadata)
                    #'term)]))

              (wrap-proof
               (begin
                 (define invoked (impl (build-module)))

                 (define-tagged-imports tag ifc invoked) ...))))))]))

  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ;;
  ;;  compound
  ;;
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

  (define (expand-compound stx)
    (reject-repl! stx)
    (syntax-case/error
     stx (import export sharing link : <-)
     [(c name
         (import (itag : iface) ...)
         (export (etag : eface) ...)
         (sharing (shared ...) ...)
         (link (ltag ...) <- mod (arg ...)) ...)

      (begin

       (check-identifiers! #'(itag ... iface ...))
       (check-identifiers! #'(etag ... eface ...))
       (check-identifiers! #'(ltag ... ...))
       (check-identifiers! #'(arg ... ...))
       (check-identifiers! #'(shared ... ...))
       (check-interface-identifiers! #'(iface ... eface ...))
       (check-unique-identifiers! #'(itag ... ltag ... ...))
       (check-unique-identifiers! #'(etag ...))
       (check-identifier-subset! #'(etag ...) #'(ltag ... ...))
       (check-module-identifiers! #'(mod ...))
       (check-sharing! #'(itag ... etag ...) #'(iface ... eface ...)
                       #'((shared ...) ...))
       (check-linked-interfaces!
        #'(itag ...) #'(iface ...)
        #'(mod ...) #'((arg ...) ...) #'((ltag ...) ...)
        #'(etag ...) #'(eface ...)))

      (let* ([mods (syntax->list #'(mod ...))]
             [metas (map read-syntax-indirection mods)])
        (with-syntax ([orig stx]
                      [(modfun ...) (map mod-impl metas)]
                      [((itag* ...) ...) (map mod-imports metas)]
                      [((etag* ...) ...) (map mod-exports metas)])
          (syntax/loc stx
            (begin

              (define-for-syntax metadata
                (module-meta
                 #'orig #'name #'impl
                 (list (cons #'itag (read-syntax-indirection #'iface)) ...)
                 (list (cons #'etag (read-syntax-indirection #'eface)) ...)
                 (list (list #'shared ...) ...)))

              (begin-for-syntax
               (check-compound-sharing!
                metadata
                (list #'mod ...)
                (list (list #'arg ...) ...)
                (list (list #'ltag ...) ...)))

              (define-syntax (wrap-proof stx)
                (syntax-case stx ()
                  [(wp term)
                   (make-modular
                    #'orig
                    (compound-proof
                     metadata
                     (list #'mod ...)
                     (list (list #'arg ...) ...)
                     (list (list #'ltag ...) ...))
                    #'term)]))

              (wrap-proof
               (define (impl var)
                 (let*-values ([(itag ...) (get-interfaces var itag ...)]
                               [(ltag ...)
                                (get-interfaces
                                 (modfun (build-module [itag* arg] ...))
                                 etag* ...)]
                               ...)
                   (build-module [etag etag] ...))))

              (define-syntax name (make-syntax-indirection metadata))))))]))

  )