(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)])))
(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))]))))
(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))))
)