(module checking-proc mzscheme
  (require "../modular/expansion/proof-syntax.scm")
  (require-for-template mzscheme
                        "acl2-app.scm"
                        (lib "contract.ss"))
  (provide checking-proc)
  
  (define-syntax (checking-proc stx)
    (syntax-case stx ()
      [(_ internal-name (x ...))
       #'(lambda (syn)
           (syntax-case syn ()
             [(_ignore x ...)
              (make-expr
               syn
               (syntax/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 ...)
                (make-expr
                 syn
                 (syntax/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)])))
       ])))