#|
Defines a class that whose instances manage connections to the external
ACL2 process.
|#

#| NOTES:
The interrupt method in acl2-process% is broken.

In principle, we could trigger an interrupt signal using
(*acl2-control* 'interrupt), but that would only send the signal
to the shell script process that has spawned the ACL2/LISP process.
Also, on Windows, MzScheme doesn't guarantee that 'interrupt would do anything.
|#
(module acl2-process mzscheme
  (require (lib "async-channel.ss")
           (lib "process.ss")
           (lib "class.ss")
           (lib "port.ss")
           (lib "etc.ss")
           (lib "moddep.ss" "syntax")
           (lib "mred.ss" "mred")) ;; for yield
  (require "../language/find-acl2.scm"
           "../language/acl2-module-v.scm"
           "windows-interrupt.scm"
           "../language/acl2-path-to-lisp-command.scm")
  (provide acl2-process%)

  (error-print-width 500)

  #|(require (file "eprintf.scm"))|#
  (define err-port (current-error-port))

  (define stars-re "\\*\\*\\*\\*\\*\\*\\*\\*") ;; matches "********"
  (define failure-re
    (string-append stars-re " FAILED " stars-re
                   "  See :DOC failure  "
                   stars-re " FAILED " stars-re))
  (define failure-str
    "******** FAILED ********  See :DOC failure  ******** FAILED ********")
  (define error-re "ACL2 Error in")
  (define raw-lisp-re "RAW LISP")

  (define raw-lisp-bytes #"RAW LISP")

  (define prompt-re "ACL2(\\(r\\))? [ps!]*>+")

  (define proof-tree-start-re "#<\\\\<0")
  (define proof-tree-start-bytes #"#<\\<0")
  (define proof-tree-stop-re "#>\\\\>")

  (define done-str "|||this-symbol-indicates-that-ACL2-is-done|||")
  (define done-bytes #"|\\|\\|\\|this-symbol-indicates-that-ACL2-is-done\\|\\|\\||")
  (define done-sym (string->symbol done-str))
  (define done-re "\\|\\\\\\|\\\\\\|\\\\\\|this-symbol-indicates-that-ACL2-is-done\\\\\\|\\\\\\|\\\\\\|\\|")

  (define (send-done port)
    (write `(intern ,done-str "ACL2") port))

  #|(define fail-or-error-or-prompt-re
      (regexp (string-append failure-re "|" error-re "|" prompt-re)))|#

  #|(define fail-or-error-or-done-re
      (regexp (string-append failure-re "|" error-re "|" done-re)))|#

  (define pftree/done-re
    (regexp (string-append proof-tree-start-re "|" done-re)))

  (define fail/error/pftree/done-re
    (regexp (string-append failure-re "|"
                           error-re "|"
                           ;; raw-lisp-re "|"
                           proof-tree-start-re "|" done-re)))

  (define (copy-rest in-> ->out)
    (regexp-match done-re in-> 0 #f ->out)
    (regexp-match prompt-re in-> 0 #f ->out)
    #|(let ([tid (thread (lambda () (copy-port in-> ->out)))])
        (sync/timeout/enable-break 2 tid)
        (kill-thread tid))|#)

  (define (extract-prooftree from->)
    (let ([proof-tree-port (open-output-string)])
      (regexp-match proof-tree-stop-re from-> 0 #f proof-tree-port)
      (get-output-string proof-tree-port)))

  (define (spawn/connect-output status-channel acl2-> ->console send-new-prooftree)
    (thread
     (lambda ()
       ;; Throw away banner text from "Initialized with" to the prompt
       (regexp-match "Initialized with" acl2-> 0 #f ->console)
       (regexp-match prompt-re acl2-> 0 #f)
       (let loop ()
         (let* ([matched
                 (let ([m (regexp-match fail/error/pftree/done-re
                                        acl2-> 0 #f ->console)])
                   (if m
                       (car m)
                       (raise-user-error
                        'acl2-output-thread
                        "Output matches none of fail|error|pftree|done")))]

                [status
                 (cond [(equal? matched done-bytes) #t]
                       [(equal? matched proof-tree-start-bytes) 'proof-tree-start]
                       #|[(equal? matched raw-lisp-bytes) 'raw-lisp]|#
                         [else #f])])
           (case status
             [(proof-tree-start)
              (send-new-prooftree (extract-prooftree acl2->))]
             #|[(raw-lisp) '???]|#
             [(#t) (async-channel-put status-channel #t)]
             [(#f) (begin
                     (display matched ->console)
                     (flush-acl2-input acl2-> ->console send-new-prooftree)
                     (async-channel-put status-channel #f))])
           (loop))))))

  (define (flush-acl2-input acl2-> ->console send-new-prooftree)
    (let loop ()
      (let* ([matched (car (regexp-match pftree/done-re
                                         acl2-> 0 #f ->console))]
             [status (cond [(equal? matched done-bytes) 'done]
                           [(equal? matched proof-tree-start-bytes) 'proof-tree-start])])
        (case status
          [(done) 'done]
          [(proof-tree-start)
           (begin (send-new-prooftree (extract-prooftree acl2->))
                  (loop))]))))

  (define acl2-process%
    (class object% ()
      (init-field send-new-prooftree)
      (init-field [acl2-output-port err-port])
      (init-field [path (find-acl2)])

      (field [status-channel (make-async-channel)])

      (define process-alive? #f)

      (define-values (*acl2->me* *me->acl2* *PID* *acl2-error->me* *acl2-control*)
        (values #f #f #f #f #f))

      (define output-thread #f)

      (define/private (initialize-acl2-environment!)
        (for-each (lambda (x) (send this send-to-repl x))
                  `(:start-proof-tree
                    (set-ld-pre-eval-print t state)
                    (add-include-book-dir :teachpacks ,teachpack-path))))

      ;; -> pid or raises exn.
      (define/public (start!)
        (when (not process-alive?)
          (set!-values (*acl2->me* *me->acl2* *PID* *acl2-error->me* *acl2-control*)
                       (apply values
                              (apply process* (acl2-path->command-list path))))
          (case (*acl2-control* 'status)
            [(running)
             (begin
               (set! process-alive? #t)
               (set! output-thread
                     (spawn/connect-output status-channel *acl2->me* acl2-output-port
                                           send-new-prooftree))
               (initialize-acl2-environment!))]
            [else (raise-user-error 'acl2-process%::start
                                    "Failed to start ACL2 (using this path: ~a)"
                                    path)])
          *PID*))

      (define/public (stop!)
        (when *acl2-control*
          (when output-thread (kill-thread output-thread))
          (*acl2-control* 'kill)
          #|
          (write-string "#. :q (good-bye)" *me->acl2*)
          (newline *me->acl2*)
          (flush-output *me->acl2*)
          |#

          (close-input-port *acl2->me*)
          (close-input-port *acl2-error->me*)
          (close-output-port *me->acl2*)
          (set!-values (process-alive? *acl2->me* *me->acl2* *PID*
                                       *acl2-error->me* *acl2-control*)
                       (apply values (build-list 6 (lambda _ #f))))
          ))

      (define error-str
        (string-append
         "Dracula currently only works on Windows, Unix, and "
         "Mac OS X.  You appear to be running on ~a.  Please file"
         " a bug report and include this message!"))

      (define/public (interrupt)
        (case (system-type 'os)
          [(windows)
           (begin (windows-interrupt path *PID*)
                  (send-to-repl "#."))]
          [(unix macosx)
           (begin (*acl2-control* 'interrupt)
                  (send-to-repl "#."))]
          [else (raise-user-error 'Interrupt-ACL2
                                  error-str
                                  (system-type 'os))]))

      (define/public (undo-last)
        (send-to-repl ':u))

      (define/public (reset-acl2)
        (string->repl ":ubt! 1")
        (initialize-acl2-environment!))

      (define/public (send-to-repl s-exp)
        (when (not process-alive?)
          (start!))
        (if (string? s-exp)
            (string->repl s-exp)
            (s-exp->repl s-exp)))

      (define/private (string->repl str)
        (write-string str *me->acl2*)
        (newline *me->acl2*)
        (send-done *me->acl2*)
        (newline *me->acl2*)
        (flush-output *me->acl2*)
        (yield status-channel))

      (define/public (repl-event expr)
        (write expr *me->acl2*)
        (newline *me->acl2*)
        (send-done *me->acl2*)
        (newline *me->acl2*)
        (flush-output *me->acl2*)
        status-channel)

      (define/public (s-exp->repl s-exp)
        (yield (repl-event s-exp)))

      (super-new)))

  )