#|
defun generates macros that check that the defined function is used only in 
operator position (or acl2-provide/contract).  Also does arity checking.
|#
#lang scheme

(require "constants.ss"
         "declare.ss"
         "../private/planet.ss"
         "../private/define-below.ss")

(require (for-syntax "t-or-nil.ss"
                     "checking-proc.ss"
                     (cce function)))

(provide defun
         defund
         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 )
     (raise-syntax-error #f "may not be used as an expression" orig-stx)]
    [else
     (syntax-case funs-stx ()
       [((function (arg ...) body) ...)
        (begin
          (for-each (papply enforce-valid-name! orig-stx)
                    (syntax->list #'(function ... arg ... ...)))
          (with-syntax ([(checked ...)
                         (generate-temporaries #'(function ...))])
            (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 (defund 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) ...))]))