#|
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)
           (file "../define-below/define-below.ss"))
  
  (require-for-syntax (file "t-or-nil.scm")
                      (file "checking-proc.scm"))
  
  (provide defun
           defstub
           mutual-recursion)

  ;; Currently defstub supports only the old form, w/o doc-string:
  (define-syntax (defstub stx)
    (syntax-case stx ()
      [(_ name (formals ...) dummy)
       (syntax/loc stx
         (defun name (formals ...)
           (raise-user-error 'name "cannot execute a stub implementation")))]))

  (define-syntax (defun stx)
    (quasisyntax/loc stx (mutual-recursion (unsyntax stx))))

  (define-syntax (mutual-recursion stx)
    (syntax-case stx ()
      [(m-r (defun function (arg ...) doc/declare ... body) ...)
       (with-syntax ([(checked ...) (generate-temporaries #'(function ...))])
         (syntax/loc stx
           (begin
             (define-syntax function (checking-proc checked (arg ...)))
             ...
             (define-values-below (checked ...)
               (let ([function (lambda (arg ...) body)] ...)
                 (values function ...))))))]))

  )