(module checking-proc mzscheme
  (require-for-template mzscheme
                        (only "acl2-app.ss" acl2-expr)
                        (lib "contract.ss"))
  (provide checking-proc)
  
  (define-syntax (checking-proc stx)
    (syntax-case stx ()
      [(_ internal-name (x ...))
       #'(lambda (syn)
           (syntax-case syn ()
             [(_ignore x ...)
              (quasisyntax/loc syn
                (acl2-expr (internal-name x ...)))]
             [(_ignore y (... ...))
              (raise-syntax-error 
               #f 
               (format "Expected ~a arguments, but got ~a"
                       (length '(x ...))
                       (length (syntax->list #'(y (... ...)))))
               syn)]
             [_else (raise-syntax-error 
                     #f "Functions may be used only in operator position." syn)]))]
      [(_ internal-name contract-expr pos neg (x ...))
       (with-syntax ([(y ...) (generate-temporaries #'(x ...))])
         #'(lambda (syn)
             (syntax-case syn ()
               [(_ignore y ...)
                (quasisyntax/loc syn
                  (acl2-expr
                   ((contract contract-expr internal-name pos neg)
                    y ...)))]
               [(_ignore z (... ...))
                (raise-syntax-error 
                 #f 
                 (format "Expected ~a arguments, but got ~a"
                         (length '(y ...))
                         (length (syntax->list #'(z (... ...)))))
                 syn)]
               [_else (raise-syntax-error 
                       #f "Functions may be used only in operator position." syn)])))
       ])))