(module acl2-app mzscheme
  (require-for-syntax "syntax-checks.scm"
                      "../modular/expansion/proof-syntax.scm")
  (provide acl2-app acl2-expr)
  (require-for-template mzscheme)

  (define-syntax (acl2-expr stx)
    (syntax-case stx ()
      [(ae expr)
       (case (syntax-local-context)
         [(module) (syntax/loc stx ((current-print) expr))]
         [else #'expr])]))
 
  (define-syntax (acl2-app stx)
    (syntax-case stx (unbox)
      [(_ (unbox id) args ...)
       (make-expr stx #'(#%app (unbox id) args ...))]
      [(_ id args ...)
       (and (identifier? #'id) (not (legal-constant-name? #'id)))
       (make-expr stx #'(acl2-expr (#%app id args ...)))]
      [(_ id args ...)
       (legal-constant-name? #'id)
       (raise-syntax-error #f "This is a constant name, but we expected a function name." stx #'id)]
      [(_ something args ...)
       (raise-syntax-error #f "Expected the name of a function here" stx #'something)]))
  )