(module proof mzscheme

  (require (planet "combinators.ss" ("cce" "combinators.plt" 1 4))
           (only (lib "1.ss" "srfi") filter-map)
           "metadata.scm"
           "sharing.scm"
           "idmap.scm"
           "tags.scm"
           "syntax-errors.scm")

  (provide interface-proof primitive-proof compound-proof invoke-proof)

  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ;;
  ;;  Interface annotation
  ;;
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

  (define (interface-proof imeta)
    (append (interface-stubs imeta)
            (interface-axioms imeta)))

  (define (interface-stubs imeta)
    (let* ([funs (ifc-funs imeta)]
           [args (map (curry ifc-args imeta) funs)])
      (with-syntax ([(f ...) funs]
                    [((arg ...) ...) args])
        (syntax->list
         (syntax/loc (ifc-original imeta)
           ((defstub f (arg ...) t) ...))))))

  (define (interface-axioms imeta)
    (let* ([thms (ifc-thms imeta)]
           [exprs (map (curry ifc-rule imeta) thms)])
      (with-syntax ([(th ...) thms]
                    [(expr ...) exprs])
        (syntax->list
         (syntax/loc (ifc-original imeta)
           ((defaxiom th expr) ...))))))

  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ;;
  ;;  Primitive module annotation
  ;;
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

  (define (primitive-proof meta defs tags externals internals)
    (append (primitive-imports meta)
            (primitive-body meta defs)
            (primitive-exports meta tags externals internals)))

  (define (primitive-imports meta)
    (append (primitive-stubs meta)
            (primitive-axioms meta)))

  (define (primitive-stubs meta)
    (let* ([sharing (mod-import-sharing meta)]
           [imports (mod-imports meta)])
      (apply append
             (map (lambda (tag)
                    (tagged-stubs sharing tag (mod-ifc meta tag)))
                  imports))))

  (define (tagged-stubs sharing tag ifc)
    (filter-map (lambda (id) (make-stub sharing tag id (ifc-args ifc id)))
                (ifc-funs ifc)))

  (define (make-stub sharing tag id args)
    (let* ([f (tag-id tag id)])
      (and (sharing-representative? sharing f)
           (quasisyntax/loc tag (defstub #,f #,args t)))))

  (define (primitive-axioms meta)
    (let* ([sharing (mod-import-sharing meta)]
           [imports (mod-imports meta)])
      (apply append
             (map (lambda (tag)
                    (tagged-axioms sharing tag (mod-ifc meta tag)))
                  imports))))

  (define (tagged-axioms sharing tag ifc)
    (let* ([funs (ifc-funs ifc)]
           [tagged-funs (map (curry tag-id tag) funs)]
           [tagged-reps (map (curry sharing-representative sharing)
                             tagged-funs)]
           [renaming (alist->idmap (map cons funs tagged-reps))]
           [thms (ifc-thms ifc)]
           [exprs (map (curry ifc-rule ifc) thms)])
      (map (curry make-axiom renaming tag) thms exprs)))

  (define (make-axiom renaming tag id expr)
    (quasisyntax/loc tag
      (defaxiom #,(tag-id tag id)
        #,(deep-renaming renaming expr))))

  (define (primitive-body meta defs)
    (map (curry deep-renaming
                (sharing->renaming
                 (mod-import-sharing meta)))
         defs))

  (define (primitive-exports meta tags externals internals)
    (apply append (map (curry primitive-exports/tag meta)
                       tags externals internals)))

  (define (primitive-exports/tag meta tag externals internals)
    (let* ([ifc (mod-ifc meta tag)]
           [thms (ifc-thms ifc)]
           [exprs (map (curry ifc-rule ifc) thms)]
           [sharing (mod-import-sharing meta)]
           [renaming
            (alist->idmap
             (map
              (lambda (int ext)
                (cons ext (sharing-representative sharing int)))
              internals externals))])
      (with-syntax ([(th ...) (map (curry tag-id tag) thms)]
                    [(expr ...) (map (curry deep-renaming renaming) exprs)])
        (syntax->list
         (syntax/loc tag
           ((defthm th expr) ...))))))

  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ;;
  ;;  Compound module annotation
  ;;
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

  (define (compound-proof meta mods args ltags)
    null)

  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  ;;
  ;;  Invocation annotation
  ;;
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

  (define (invoke-proof meta)
    null)

  (define (deep-renaming idmap v)
    (cond
     [(identifier? v) (idmap-get idmap v (lambda () v))]
     [(syntax? v)
      (let* ([datum (deep-renaming idmap (syntax-e v))])
        (datum->syntax-object v datum v v v))]
     [(pair? v)
      (cons (deep-renaming idmap (car v)) (deep-renaming idmap (cdr v)))]
     [else v]))

  )