#|
Gathers all the modules together and provides the core forms (more or less).
A few more forms are defined at provided toward the end.
|#
(module dracula-core mzscheme
  (require (lib "plt-match.ss")
           #;(file "book-path-utilities.scm"))
  #;(require-for-syntax (only (file "prefix.scm") prefix))
  
  (provide (rename time time$)
           display collect-garbage expand)
  (provide require require-for-syntax) ;; for acl2-prims
  
  (require (prefix acl2- (file "conditionals.scm"))
           (file "constants.scm")
           (file "declare.scm")
           (file "defun.scm")
           ;(file "defmacro.scm")
           (file "defconst.scm")
           (file "defthm.scm")
           ;(file "defevaluator.scm")
           ;(file "defstructure.scm")
           ;(file "local.scm")
           ;(file "encapsulate.scm")
           (file "include-book.scm")
           (file "in-package.scm")
           ;(file "table.scm")
           (file "parameters.scm")
           (file "acl2-io.scm")
           (prefix acl2- (file "let.scm"))
           (prefix acl2- (file "quote.scm"))
           
           "with-prover-time-limit.scm"
           
           ;(file "set-default-hints.scm")
           ;(file "deflist.scm")
           (file "case-match.scm")
           (file "acl2-top.scm")
           (file "acl2-app.scm"))
  
  (provide ;;;;(all-from (file "conditionals.scm"))
           (rename acl2-if if) (rename acl2-cond cond) (rename acl2-case case)
           (rename acl2-and and) (rename acl2-or or)
           ;;;;
           
           (all-from (file "constants.scm"))
           (all-from (file "declare.scm"))
           (all-from (file "defun.scm"))
           ;(all-from-except (file "defmacro.scm") defmacro/local)
           (all-from (file "defconst.scm"))
           (all-from-except (file "defthm.scm") defthm/local)
           ;(all-from-except (file "defevaluator.scm"))
           ;(all-from (file "defstructure.scm"))
           ;(all-from (file "local.scm"))
           ;(all-from (file "encapsulate.scm"))
           (all-from (file "include-book.scm"))
           (all-from (file "in-package.scm"))
           ;(all-from (file "table.scm"))
           (all-from (file "parameters.scm"))
           (all-from (file "acl2-io.scm"))
           ;;;(all-from (file "let.scm"))
           (rename acl2-let let)
           (rename acl2-let* let*)
           ;;; (all-from (file "quote.scm"))
           (rename acl2-quote quote)
           (rename acl2-quasiquote quasiquote)
           (rename acl2-unquote unquote)
           (rename acl2-unquote-splicing unquote-splicing)
           
           (all-from "with-prover-time-limit.scm")
           
           ;(all-from (file "set-default-hints.scm"))
           ;(all-from (file "deflist.scm"))
           (all-from (file "case-match.scm"))
           #;defpkg  deflabel deftheory
           (rename acl2-assert$ assert$)
           
           in-theory disable enable theory-invariant
           
           (rename acl2-top #%top)
           (rename acl2-app #%app)
           #%datum
           
           #%module-begin ;; from mzscheme...
           
           (rename acl2-mv mv)
           (rename acl2-mv-let mv-let)
           )
  
  (define-syntax (disable stx)
    (syntax-case stx ()
      [(_ stuff ...) #'(void)]))
  (define-syntax (enable stx)
    (syntax-case stx ()
      [(_ stuff ...) #'(void)]))
  (define-syntax (in-theory stx)
    (syntax-case stx ()
      [(_ spec)
       #'(void)]))
  
  (define-syntax (theory-invariant stx)
    #'(void))
  
  (define-syntax (defpkg stx) #'(begin))
  (define-syntax (deflabel stx) #'(begin))
  
  (define-syntax (acl2-assert$ stx)
    (syntax-case stx ()
      [(_ test form) 
       #'(acl2-if test form (error 'assert$ "Assertion failed!~n~a" (quote stx)))]))
  
  (define-syntax (acl2-mv stx)
    (syntax-case stx ()
      [(_ expr1 expr2 exprs ...)
       #'(list expr1 expr2 exprs ...)]))
  
  (define-syntax (acl2-mv-let stx)
    (syntax-case stx ()
      [(_ (ids ...) expr body)
       #'(match-let ([(list ids ...) expr]) body)]))
  
  #;(define-syntax (acl2-case-match stx) ...)
  
  
  ;;;;; LOGICAL EVENTS ;;;;
  ;  (define-for-syntax table (make-module-identifier-mapping))
  ;  (define-for-syntax (record-name! id)
  ;    (module-identifier-mapping-put! table id #t))
  ;  (define-for-syntax (already-defined? id)
  ;    (module-identifier-mapping-get table id (lambda () #f)))
  
  (define-syntax (deftheory stx)
    (syntax-case stx (:doc)
      [(_ name expr :doc doc-string) #'(define name '(theory: expr))]
      [(_ name expr) #'(deftheory name expr :doc "")]))
  
  
  )