(module defconst mzscheme
  (require (lib "unit.ss"))
  (require-for-syntax "syntax-checks.scm"
                      "defun-state.scm")
  (provide defconst)
  
  (define-syntax (defconst stx)
    (syntax-case stx ()
      [(_ name expr)
       (with-syntax (#;[provide-form (if (eq? (syntax-local-context) 'module)
                                         #`(provide (rename name #,(prefix #'name)))
                                         #'(begin))])
         #;(syntax (begin (defconst/local name expr)
                          provide-form))
         (syntax (defconst/local name expr)))]))
  
  #;
  (define-syntax (defconst/local stx)
    (syntax-case stx ()
      [(_ name value)
       (if (legal-constant-name? #'name)
           #`(begin #;(acl2-repl (quote #,(syntax-object->datum stx)))
                    (define* name value))
           (raise-syntax-error
            'defconst ;; hide defconst/local
            (string-append 
                "Constant names must be identifiers surrounded with asterisks (e.g., "
                (if (identifier? #'name)
                    (string-append "*" (symbol->string (syntax-object->datum #'name)) "*")
                    "*my-constant*")
                ")")
            stx #'name))]))
  
  (define-syntax (defconst/local stx)
    (syntax-case stx ()
      [(_ name expr)
       (if (legal-constant-name? #'name)
           (with-syntax ([(prior-sig^ ...) (get-sigs)]
                         [internal ((make-syntax-introducer) #'name)])
             #'(begin (define-signature name^ [name])
                      (begin-for-syntax (register-unit! #'name@ #'name^))
                      (define-unit name@
                        (import prior-sig^ ...)
                        (export name^)
                        (define name expr))))
           
           (raise-syntax-error
            'defconst ;; hide defconst/local
            (string-append 
                "Constant names must be identifiers surrounded with asterisks (e.g., "
                (if (identifier? #'name)
                    (string-append "*" (symbol->string (syntax-object->datum #'name)) "*")
                    "*my-constant*")
                ")")
            stx #'name))]))
  
  )