#|
defun generates macros that check that the defined function is used only in 
operator position (or acl2-provide/contract).  Also does arity checking.
|#
(module defun mzscheme
  (require (file "constants.scm")
           (file "declare.scm")
           (all-except (lib "contract.ss") any/c)
           (lib "unit.ss"))
  
  (require-for-syntax (file "t-or-nil.scm")
                      "checking-proc.scm"
                      "defun-state.scm")
  
  (provide (rename defun/local defun)
           defun/local ;; still need this in case (local (defun ...)) shows up
           ;defun/local
           ;;defun-for-syntax
           defstub
           mutual-recursion)
  
  (define-syntax (defun/local stx)
    (syntax-case stx (declare)
      [(_ name (formals ...) doc-string (declare decls ...) ... body)
       (and (identifier? #'name)
            (when (t-or-nil? #'name)
              (raise-syntax-error #f "You may not redefine t or nil" stx #'name))
            (string? (syntax-e #'doc-string))
            (let ([params (syntax->list #'(formals ...))])
              (unless (andmap identifier? params)
                (raise-syntax-error #f "Formal paramters must all be names" stx #'(formals ...)))
              ;; check that formals ... don't contain t or nil.
              (for-each (lambda (p)
                          (when (t-or-nil? p)
                            (raise-syntax-error #f "t and nil may not be used as parameter names" stx p)))
                        params)
              (let ([duplicate (check-duplicate-identifier params)])
                (when duplicate
                  (raise-syntax-error #f "Found duplicate argument name" stx duplicate))))
            (when (already-defined? #'name)
              (raise-syntax-error 
               #f 
               (format "A function called ~a has already been defined"
                       (syntax-e #'name))
               stx
               #'name)))
       (with-syntax ([(prior-sig^ ...) (get-sigs)]
                     [(internal-name) (generate-temporaries #'(name))])
         #'(begin
             (define-signature name^ 
               [internal-name
                (define-syntaxes (name) 
                  (checking-proc internal-name (formals ...)))
                ])
             (begin-for-syntax (register-unit! #'name@ #'name^))
             (define-unit name@
               (import prior-sig^ ...)
               (export name^)
               (init-depend prior-sig^ ...)
               (define internal-name
                 (let-syntax ([name (checking-proc internal-name (formals ...))])
                   (lambda (formals ...) body))))))]
      
      [(_ name (formals ...) (declare decls ...) ... body)
       #'(defun/local name (formals ...) "<no documentation>" (declare decls ...) ... body)]))

  ;; Currently defstub supports only the old form, w/o doc-string:
  (define-syntax (defstub stx)
    (syntax-case stx ()
      [(_ name (formals ...) output)
       (syntax/loc stx
         (defun/local name (formals ...)
           (error 'name "cannot execute a stub implementation")))]))
  
  ;; FIX ME:
  (define-syntax (mutual-recursion stx)
    (syntax-case stx (defun/local declare)
      [(_ (defun/local f (x ...) e) ...)
       (with-syntax ([(prior-sig^ ...) (get-sigs)]
                     [(f-internal ...) (generate-temporaries #'(f ...))])
         (with-syntax ()
           #'(begin
               (define-signature murec^ 
                 [f-internal ...
                  (define-syntaxes (f ...) 
                    (values (checking-proc f-internal (x ...)) ...))])
               (begin-for-syntax (register-unit! #'murec@ #'murec^))
               (define-unit murec@
                 (import prior-sig^ ...)
                 (export murec^)
                 (init-depend prior-sig^ ...)
                 (define-values (f-internal ...)
                   (let-syntax ([f (checking-proc f-internal (x ...))] ...)
                     (values (lambda (x ...) e) 
                             ...)))))))]
      [_ (raise-syntax-error #f "mutual-recursion expected a sequence of defuns" stx)]
      ))
  )