#|
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 "constants.scm"
           "declare.scm"
           (all-except (lib "contract.ss") any/c)
           "../define-below/define-below.ss")
  
  (require-for-syntax (lib "function.ss" "scheme")
                      "t-or-nil.scm"
                      "checking-proc.scm"
                      "../modular/expansion/proof-syntax.scm")

  (provide defun
           defstub
           mutual-recursion)

  (define-for-syntax (enforce-valid-name! stx v)
    (unless (identifier? v)
      (raise-syntax-error #f "expected an identifier" stx v))
    (when (t-or-nil? v)
      (raise-syntax-error #f "cannot bind reserved name" stx v)))

  (define-for-syntax (expand-funs orig-stx funs-stx)
    (case (syntax-local-context)
      [( expression top-level module-begin )
       (raise-syntax-error #f "may not be used as an expression" orig-stx)]
      [else
       (syntax-case funs-stx ()
         [((function (arg ...) body) ...)
          (begin
            (for-each (curry enforce-valid-name! orig-stx)
                      (syntax->list #'(function ... arg ... ...)))
            (with-syntax ([(checked ...)
                           (generate-temporaries #'(function ...))])
              (make-event
               orig-stx
               (syntax/loc orig-stx
                 (begin
                   (define-syntaxes (function ...)
                     (values (checking-proc checked (arg ...)) ...))
                   (define-values-below (checked ...)
                     (let ([function (lambda (arg ...) body)] ...)
                       (values function ...))))))))])]))

  (define-syntax (defstub stx)
    (syntax-case stx ()
      [(ds function (arg ...) dummy)
       (expand-funs
        stx
        #'((function (arg ...)
                     (raise-user-error 'function "cannot execute a stub"))))]))

  (define-syntax (defun stx)
    (syntax-case stx ()
      [(df function (arg ...) doc/declare ... body)
       (expand-funs stx #'((function (arg ...) body)))]))

  (define-syntax (mutual-recursion stx)
    (syntax-case stx ()
      [(mr (defun function (arg ...) doc/declare ... body) ...)
       (expand-funs stx #'((function (arg ...) body) ...))]))

  )