#lang scheme

(require (for-syntax "../proof/wrapper.ss")
         "../proof/provide.ss")

(provide/dracula
 "dracula-core.ss"
 [ dracula-keyword
   declare disable enable]
 [ dracula-event
   defun defstub mutual-recursion defconst defthm defaxiom deftheory defequiv
   include-book
   set-ignore-ok set-state-ok set-irrelevant-formals-ok set-compile-fns
   set-well-founded-relation
   with-prover-time-limit skip-proofs
   in-theory theory-invariant]
 [ dracula-expr
   if cond case and or t nil in-package
   set-guard-checking state
   open-input-channel open-output-channel
   close-input-channel close-output-channel
   read-char$ princ$ read-byte$ write-byte$
   let let* quote quasiquote unquote unquote-splicing
   case-match assert$
   mv mv-let
   #%datum])

(provide/dracula "defstructure.ss" [dracula-event defstructure])
(provide/dracula "deflist.ss" [dracula-event deflist])

(provide/dracula
 "primitive-procedures/acl2-prims.ss"
 [dracula-expr

  ;; from Scheme
  * + - list list* append / not
  eqlablep eq eql equal symbolp
  cons make-list endp null consp true-listp car cdr
  len concatenate revappend reverse
  intersectp-eq intersectp-equal
  lognot logand logior logorc1 logorc2 logeqv logxor
  expt
  characterp alpha-char-p char-equal
  char< char<= char>= char> char-code code-char digit-char-p
  make-character-list stringp standard-char-p standard-char-listp
  string-equal string< string<= string>= string>
  nth coerce explode-nonnegative-integer
  acl2-numberp natp complex-rationalp zp evenp oddp minusp plusp posp
  integerp rationalp real/rationalp integer-range-p min max
  unary-/ nonnegative-integer-quotient
  = < <= >= > fix floor mod
  alistp alphorder
  second caar cadr cdar cddr
  third caaar caadr cadar caddr cdaar cdadr cddar cdddr
  fourth
  caaaar caaadr caadar caaddr cadaar cadadr caddar cadddr
  cdaaar cdaadr cdadar cdaddr cddaar cddadr cdddar cddddr

  ;; from Dracula
  booleanp implies iff
  o-finp o-infp o-first-coeff o-first-expt o-rst o-p
  o< o<= o>= o> make-ord
  complex/complex-rationalp int= /= zerop zip zpf
  integer-listp rational-listp
  abs signum nfix ifix rfix realfix
  ash integer-length numerator denominator ceiling round truncate
  rem 1+ 1- unary-- binary-+ binary-*
  complex imagpart realpart conjugate
  logandc1 logandc2 logbitp logcount lognand lognor logtest
  keywordp symbol-name symbol-package-name symbol-<
  symbol-listp symbol-alistp keyword-value-listp
  character-listp digit-to-char
  upper-case-p lower-case-p char-upcase char-downcase
  string char string-listp standard-string-alistp string-append
  string-upcase string-downcase length subseq
  position position-eq position-equal
  listp proper-consp improper-consp
  eqlable-listp true-list-listp
  first rest fifth sixth seventh eighth ninth tenth
  nthcdr update-nth take binary-append
  member member-eq member-equal
  remove remove-eq remove-equal
  remove1 remove1-eq remove1-equal
  remove-duplicates remove-duplicates-eql remove-duplicates-equal
  no-duplicatesp no-duplicatesp-equal
  pairlis$ fix-true-list butlast last
  acons assoc assoc-eq assoc-equal assoc-keyword assoc-string-equal
  put-assoc-eq put-assoc-eql put-assoc-equal
  rassoc rassoc-eq rassoc-equal
  strip-cars strip-cdrs domain range
  eqlable-alistp add-to-set-eq add-to-set-eql add-to-set-equal
  set-difference-eq set-difference-equal
  subsetp subsetp-equal union-eq union-equal
  atom atom-listp identity
  subst substitute sublis
  lexorder acl2-count
  ])

(provide/dracula "acl2-top.ss" [dracula-expr #%top])

(provide/dracula "acl2-app.ss" [dracula-expr #%app])