#|
Provides a few of ACL2's file io primitives.
|#
(module acl2-io mzscheme
  
  (provide open-input-channel open-output-channel
           close-input-channel close-output-channel
           read-char$ princ$
           read-byte$ write-byte$)
  
  (define (open-input-channel file-name io-type state)
    (with-handlers ([exn:fail:filesystem? (lambda (e) (list '() state))])
      ;; Do I really want the port to leak out here?
      (list (open-input-file file-name) state)
      ))
  
  (define (open-output-channel file-name io-type state) 
    (with-handlers ([exn:fail:filesystem? (lambda (e) (list '() state))])
      (list (open-output-file file-name) state)))
  
  (define (close-input-channel channel state)
    (close-input-port channel)
    state)
  
  (define (close-output-channel channel state)
    (close-output-port channel)
    state)
  
  (define (read-char$ channel state) 
    (let ([c (read-char channel)])
      (list (if (eof-object? c) '() c)
            state)))
  
  (define (read-byte$ channel state)
    (let ([b (read-byte channel)])
      (list (if (eof-object? b) 
                '() 
                b)
            state)))
  
  (define (write-byte$ byte channel state)
    (write-byte byte channel)
    state)
  
  (define (princ$ obj channel state)
    (cond [(char? obj) (write-char obj channel)]
          [(string? obj) (write-string obj channel)]
          [(symbol? obj) (write obj channel)]
          [(number? obj) (write obj channel)]
          [else (error 'princ$ 
                       "Expected character, string, symbol, or number as first argument.  Given ~s" 
                       obj)])
    state)
  
  )