#|
Reject #t and #f, allow #c for complex numbers.
Also hack around some ACL2 preprocessor directives.  This was necessary
for `include-book', but support of include-book has been dropped for now.
|#
(module acl2-readtable mzscheme
  (require (lib "readerr.ss" "syntax")
           (lib "port.ss"))
  
  (provide acl2-readtable)
  
  ;; I've hard-coded some preprocessor definitions here.
  ;; #+expr1 expr2 -- expr1 and expr2 are never evaluated.
  ;; #-expr1 expr2 -- gcl non-standard-analysis :non-standard-analysis are all undefined
  (define (hash-minus char port w x y z)
    (parameterize ([read-case-sensitive #f])
      (let ([test-expr (read port)])
        (if (memq test-expr '(gcl non-standard-analysis :non-standard-analysis))
            (make-special-comment test-expr)
            (make-special-comment (list test-expr (read port)))))))
  
  (define (hash-plus char port w x y z)
    (parameterize ([read-case-sensitive #f])
      (let ([test-expr (read port)])
        (if (memq test-expr '(non-standard-analysis :non-standard-analysis))
            (make-special-comment (list test-expr (read port)))
            (make-special-comment (list test-expr (read port)))))))
  
  ;; Raise an error on #t and #f
  (define hash-bool
    (lambda (char port w x y z)
      (parameterize ([read-case-sensitive #f])
        (raise-read-error (string-append (string #\# char)  " is not a valid ACL2 datum.  "
                                         "The booleans are t and nil.")
                          w x y z 2))))
  
  ;; #C(M N) is a complex number when M and N are numerals
  (define (hash-c char port w x y z)
    (parameterize ([read-case-sensitive #f])
      (case (peek-char port)
        [(#\() (let ([expr (read port)])
                 (if (and (list? expr) (= 2 (length expr)))
                     (let ([fst (car expr)]
                           [snd (cadr expr)])
                       (if (and (number? fst) (number? snd))
                           (+ fst (* snd 0+i))
                           (raise-read-error "Expected #c(x y) where x and y are both numerals"
                                             w x y z 1)))
                     (raise-read-error "Expected #c(x y) where x and y are both numerals"
                                       w x y z 1)))]
        [else (read-syntax/recursive w (input-port-append #f (open-input-string (string char)) port)
                                     #\# #f)])))
  
  (define (hash-double-quote char port w x y z)
    (raise-read-error (string-append (string #\# char) " is not a valid ACL2 reader syntax.  ")
                      w x y z 2))
  
  (define (hash-semicolon char port w x y z)
    (raise-read-error (string-append (string #\# char) " cannot be used for ACL2 comments.  ")
                      w x y z 2))
  
  (define check-infinity
    (let ([inf-str "inf.0"])
      (lambda (char port src x y z)
        (parameterize ([read-case-sensitive #f])
          (let* ([next-ch (peek-char port)]
                 [next (if (and (char? next-ch) (char-ci=? next-ch #\i)) (read port) #f)])
            (cond [(and (symbol? next) (string-ci=? inf-str (symbol->string next)))
                   (raise-read-error "ACL2 cannot perform floating-point arithmetic"
                                     src x y z 6)]
                  [(eof-object? next) (read-syntax/recursive src port char #f)]
                  [(char-ci=? next-ch #\i)
                   (let ([prefix (open-input-string (let ([x (open-output-string)])
                                                      (write next x)
                                                      (get-output-string x)))])
                     (read-syntax/recursive src (input-port-append #f prefix port) char #f))]
                  [else (read-syntax/recursive src port char #f)])))
        )))
  
  (define acl2-readtable
    (make-readtable (current-readtable)
                    #\; 'dispatch-macro hash-semicolon
                    #\t 'dispatch-macro hash-bool
                    #\T 'dispatch-macro hash-bool
                    #\f 'dispatch-macro hash-bool
                    #\F 'dispatch-macro hash-bool
                    #\" 'dispatch-macro hash-double-quote
                    #\c 'dispatch-macro hash-c
                    #\C 'dispatch-macro hash-c
                    #\- 'dispatch-macro hash-minus
                    #\+ 'dispatch-macro hash-plus
                    #\+ 'non-terminating-macro check-infinity
                    #\- 'non-terminating-macro check-infinity
                    ))
  )