#|
ACL2 quote, quasiquote, unquote, unquote-splicing.

I lifted quasiquote from http://www.cs.indiana.edu/chezscheme/syntax-case/.
|#
(module quote mzscheme
  (require (file "constants.scm")) ;; for nil
  (require-for-syntax "../modular/expansion/proof-syntax.scm"
                      (lib "stx.ss" "syntax"))

  (provide
   (rename acl2-quote quote)
   (rename acl2-quasiquote quasiquote)
   unquote
   unquote-splicing)

  (define-for-syntax (nil->empty stx)
    (cond [(stx-pair? stx)
           (let ([car-stx (stx-car stx)]
                 [cdr-stx (stx-cdr stx)])
             (let ([new-car (nil->empty (stx-car stx))]
                   [new-cdr (nil->empty (stx-cdr stx))])
               (if (and (eq? car-stx new-car) (eq? cdr-stx new-cdr))
                   stx
                   #`(#,new-car . #,new-cdr))))]
          [(and (identifier? stx)
                (module-identifier=? stx #'nil)) #'()]
          [else stx]))
  
  (define-syntax (acl2-quote stx)
    (syntax-case stx ()
      [(_ body) (make-expr stx #`(quote #,(nil->empty #'body)))]))

  ;; DV: Jan 6, 2006
  ;; I lifted this code from Dybvig and Waddell's portable syntax-case
  ;; implementation at http://www.cs.indiana.edu/chezscheme/syntax-case/
  ;; Version 7.0 (9/2/2005)
  ;; There are two small modifications in the definition of `quasilist*'
  ;; 1.  stx-car was originally just `car'
  ;; 2.  stx-cdr was originally just `cdr'
  (define-syntax acl2-quasiquote
   (letrec
     ; these are here because syntax-case uses bound-identifier=?,
     ; and we want the more precise free-identifier=?
      ((isquote? (lambda (x)
                   (and (identifier? x)
                        (module-identifier=? x (syntax acl2-quote)))))
       (islist? (lambda (x)
                  (and (identifier? x)
                       (module-identifier=? x (syntax list)))))
       (iscons? (lambda (x)
                  (and (identifier? x)
                       (module-identifier=? x (syntax cons)))))
       (quote-nil? (lambda (x)
                    (syntax-case x ()
                      ((quote? ()) (isquote? (syntax quote?)))
                      (_ #f))))
       (stx-list (lambda args (quasisyntax ((unsyntax-splicing args)))))
       (stx-cons (lambda (a b) (with-syntax ([a a] [b b]) (syntax (a . b)))))
       (quasilist*
        (lambda (x y)
          (let f ((x x))
            (if (null? x)
                y
                ;; DV: Jan 6, 2006
                ;; The original source used car and cdr instead of
                ;; stx-car and stx-cdr here.
                (quasicons (stx-car x) (f (stx-cdr x)))))))
       (quasicons
        (lambda (x y)
          (with-syntax ((x x) (y y))
            (syntax-case (syntax y) ()
              ((quote? dy)
               (isquote? (syntax quote?))
               (syntax-case (syntax x) ()
                 ((quote? dx)
                  (isquote? (syntax quote?))
                  (syntax (acl2-quote (dx . dy))))
                 (_ (if (null? (syntax dy))
                        (syntax (list x))
                        (syntax (cons x y))))))
              ((listp . stuff)
               (islist? (syntax listp))
               (syntax (list x . stuff)))
              (else (syntax (cons x y)))))))
       (quasiappend
        (lambda (x y)
          (let ((ls (let f ((x x))
                      (if (stx-null? x)
                          (if (quote-nil? y)
                              '()
                              (stx-list y))
                          (if (quote-nil? (stx-car x))
                              (f (stx-cdr x))
                              (stx-cons (stx-car x) (f (stx-cdr x))))))))
            (cond
              ((stx-null? ls) (syntax (acl2-quote ())))
              ((stx-null? (stx-cdr ls)) (stx-car ls))
              (else (with-syntax (((p ...) ls))
                      (syntax (append p ...))))))))
       (quasivector
        (lambda (x)
          (with-syntax ((pat-x x))
            (syntax-case (syntax pat-x) ()
              ((quote? (x ...))
               (isquote? (syntax quote?))
               (syntax (acl2-quote #(x ...))))
              (_ (let f ((x x) (k (lambda (ls) `(,(syntax vector) ,@ls))))
                   (syntax-case x ()
                     ((quote? (x ...))
                      (isquote? (syntax quote?))
                      (k (syntax ((acl2-quote x) ...))))
                     ((listp x ...)
                      (islist? (syntax listp))
                      (k (syntax (x ...))))
                     ((cons? x y)
                      (iscons? (syntax cons?))
                      (f (syntax y) (lambda (ls) (k (cons (syntax x) ls)))))
                     (else
                      (syntax (list->vector pat-x))))))))))
       (vquasi
        (lambda (p lev)
           (syntax-case p ()
              ((p . q)
               (syntax-case #'p (unquote unquote-splicing)
                 ((unquote p ...)
                  (if (= lev 0)
                      (quasilist* (syntax (p ...)) (vquasi (syntax q) lev))
                      (quasicons (quasicons (syntax (acl2-quote unquote))
                                            (quasi (syntax (p ...)) (- lev 1)))
                                 (vquasi (syntax q) lev))))
                 ((unquote-splicing p ...)
                  (if (= lev 0)
                      (quasiappend (syntax (p ...)) (vquasi (syntax q) lev))
                      (quasicons (quasicons (syntax (acl2-quote unquote-splicing))
                                            (quasi (syntax (p ...)) (- lev 1)))
                                 (vquasi (syntax q) lev))))
                 (p (quasicons (quasi (syntax p) lev) (vquasi (syntax q) lev)))))
              (() (syntax (acl2-quote ()))))))
       (quasi
        (lambda (p lev)
           (syntax-case p (unquote unquote-splicing acl2-quasiquote)
              ((unquote p)
               (if (= lev 0)
                   (syntax p)
                   (quasicons (syntax (acl2-quote unquote))
                              (quasi (syntax (p)) (- lev 1)))))
              (((unquote p ...) . q)
               (if (= lev 0)
                   (quasilist* (syntax (p ...)) (quasi (syntax q) lev))
                   (quasicons (quasicons (syntax (acl2-quote unquote))
                                         (quasi (syntax (p ...)) (- lev 1)))
                              (quasi (syntax q) lev))))
              (((unquote-splicing p ...) . q)
               (if (= lev 0)
                   (quasiappend (syntax (p ...)) (quasi (syntax q) lev))
                   (quasicons (quasicons (syntax (acl2-quote unquote-splicing))
                                         (quasi (syntax (p ...)) (- lev 1)))
                              (quasi (syntax q) lev))))
              ((acl2-quasiquote p)
               (quasicons (syntax (acl2-quote quasiquote))
                          (quasi (syntax (p)) (+ lev 1))))
              ((p . q)
               (quasicons (quasi (syntax p) lev) (quasi (syntax q) lev)))
              (#(x ...) (quasivector (vquasi (syntax (x ...)) lev)))
              (p (syntax (acl2-quote p)))))))
    (lambda (x)
      (syntax-case x ()
        ((_ e) (make-expr x (quasi (syntax e) 0)))))))
  )