(module acl2-path-to-lisp-command mzscheme
  (require (lib "port.ss")
           (lib "list.ss"))
  (provide acl2-path->command-list)
  
  (define (read-last-line)
    (strip-shell-command-start (current-input-port))
    (let loop ([prior-line ""]
               [line (read-line)])
      (if (eof-object? line) prior-line (loop line (read-line)))))
  
  (define (windows-exe? acl2-path)
    (let-values ([(base name dir?) (split-path acl2-path)])
      (and (eq? (system-type 'os) 'windows)
           (not dir?)
           (path? name)
           (string=? (path->string name) "acl2.exe"))))
  
  (define (number->string/-i-special n)
    (let ([ip (imag-part n)])
      (cond [(negative? ip) "-I"]
            [(positive? ip) "+I"]
            [else (number->string n)])))
    
  ;; May throw exn:fail:read exception
  (define (parse-cmd-string s)
    (let ([p (open-input-string s)])
      (let loop ([words '()]
                 [next-word (read p)])
        (cond [(eof-object? next-word) 
               (filter (lambda (x) 
                         (not (or (string=? x "exec")
                                  (string=? x "$*"))))
                       (reverse! words))]
              [(symbol? next-word) (loop (cons (symbol->string next-word) words)
                                         (read p))]
              [(number? next-word) (loop (cons (number->string/-i-special next-word) words)
                                         (read p))]
              [(string? next-word) (loop (cons next-word words)
                                         (read p))]))))
  
  ;; On Unix, read the command string from the shell script that starts ACL2.
  ;; We do this to get the right PID for later process control.
  ;; On Windows, acl2.exe isn't a shell script.
  (define (acl2-path->command-list acl2-path)
    (if (windows-exe? acl2-path)
        (list (path->string acl2-path))
        (parse-cmd-string
         (with-input-from-file acl2-path read-last-line))))
  )