(module acl2-app mzscheme
  (require-for-syntax "syntax-checks.ss")
  (provide (rename acl2-app #%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 (#%expression ((current-print) expr)))]
         [else (syntax/loc stx (#%expression expr))])]))

  (define-syntax (acl2-app stx)
    (syntax-case stx (unbox)
      [(_ (unbox id) args ...)
       (syntax/loc stx (#%app (unbox id) args ...))]
      [(_ id args ...)
       (and (identifier? #'id) (not (legal-constant-name? #'id)))
       (syntax/loc 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)]))
  )